mul_eq_prime_sq_iff — Mathlib

English

If p is prime and x ≠ 1, y ≠ 1, then xy = p^2 iff x = p and y = p.

Русский

Пусть p — простое, x ≠ 1, y ≠ 1. Тогда xy = p^2 эквивалентно x = p и y = p.

LaTeX

$$$$ \forall x,y,p \in \mathbb{N},\ \text{Prime}(p) \land x \neq 1 \land y \neq 1 \Rightarrow (xy = p^2 \iff x = p \land y = p). $$$$

Lean4

theorem mul_eq_prime_sq_iff {x y p : ℕ} (hp : p.Prime) (hx : x ≠ 1) (hy : y ≠ 1) : x * y = p ^ 2 ↔ x = p ∧ y = p :=
  by
  refine ⟨fun h => ?_, fun ⟨h₁, h₂⟩ => h₁.symm ▸ h₂.symm ▸ (sq _).symm⟩
  have pdvdxy : p ∣ x * y := by rw [h];
    simp [sq]
      -- Could be `wlog := hp.dvd_mul.1 pdvdxy using x y`, but that imports more than we want.

  suffices ∀ x' y' : ℕ, x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p by
    obtain hx | hy := hp.dvd_mul.1 pdvdxy <;> [skip; rw [And.comm]] <;> [skip; rw [mul_comm] at h pdvdxy] <;>
        apply this <;>
      assumption
  rintro x y hx hy h ⟨a, ha⟩
  have : a ∣ p := ⟨y, by rwa [ha, sq, mul_assoc, mul_right_inj' hp.ne_zero, eq_comm] at h⟩
  obtain ha1 | hap := (Nat.dvd_prime hp).mp ‹a ∣ p›
  · subst ha1
    rw [mul_one] at ha
    subst ha
    simp only [sq, mul_right_inj' hp.ne_zero] at h
    subst h
    exact ⟨rfl, rfl⟩
  · refine (hy ?_).elim
    subst hap
    subst ha
    rw [sq, Nat.mul_eq_left (Nat.mul_ne_zero hp.ne_zero hp.ne_zero)] at h
    exact h

Похожие утверждения