ne_zero_of_coprime — Mathlib

English

If gcd x y = 1 for a Pythagorean triple, then z ≠ 0.

Русский

Если gcd(x,y) = 1 в Пифагоровой тройке, то z ≠ 0.

LaTeX

$$$z \neq 0$$$

Lean4

theorem ne_zero_of_coprime (hc : Int.gcd x y = 1) : z ≠ 0 :=
  by
  suffices 0 < z * z by
    rintro rfl
    norm_num at this
  rw [← h.eq, ← sq, ← sq]
  have hc' : Int.gcd x y ≠ 0 := by
    rw [hc]
    exact one_ne_zero
  rcases Int.ne_zero_of_gcd hc' with hxz | hyz
  · apply lt_add_of_pos_of_le (sq_pos_of_ne_zero hxz) (sq_nonneg y)
  · apply lt_add_of_le_of_pos (sq_nonneg x) (sq_pos_of_ne_zero hyz)

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