prime_two_or_dvd_of_dvd_two_mul_pow_self_two

English

If p is a prime and p divides 2 m^2 in ℤ, then either p = 2 or p divides |m|.

Русский

Пусть p — простое и p делит 2 m^2 в ℤ. Тогда либо p = 2, либо p делит |m|.

LaTeX

$$$\\text{Nat.Prime}(p) \\land p \\mid 2 m^2 \\Rightarrow (p=2) \\lor p \\mid |m|.$$$

Lean4

theorem prime_two_or_dvd_of_dvd_two_mul_pow_self_two {m : ℤ} {p : ℕ} (hp : Nat.Prime p) (h : (p : ℤ) ∣ 2 * m ^ 2) :
    p = 2 ∨ p ∣ Int.natAbs m := by
  rcases Int.Prime.dvd_mul hp h with hp2 | hpp
  · apply Or.intro_left
    exact le_antisymm (Nat.le_of_dvd zero_lt_two hp2) (Nat.Prime.two_le hp)
  · apply Or.intro_right
    rw [sq, Int.natAbs_mul] at hpp
    exact or_self_iff.mp ((Nat.Prime.dvd_mul hp).mp hpp)

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