English
If gcd(x, y) = 1 for a Pythagorean triple, then either x is even and y is odd, or x is odd and y is even.
Русский
Если gcd(x, y) = 1 для Пифагоровой тройки, то либо xчетно и y нечетно, либо наоборот.
LaTeX
$$$(x \bmod 2 = 0) \land (y \bmod 2 = 1) \lor (x \bmod 2 = 1) \land (y \bmod 2 = 0)$$$
Lean4
theorem even_odd_of_coprime (hc : Int.gcd x y = 1) : x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ y % 2 = 0 :=
by
rcases Int.emod_two_eq_zero_or_one x with hx | hx <;> rcases Int.emod_two_eq_zero_or_one y with hy | hy
· exfalso
apply Nat.not_coprime_of_dvd_of_dvd (by decide : 1 < 2) _ _ hc
· apply Int.natCast_dvd.1
apply Int.dvd_of_emod_eq_zero hx
· apply Int.natCast_dvd.1
apply Int.dvd_of_emod_eq_zero hy
· left
exact
⟨hx, hy⟩
-- x odd, y even
· right
exact
⟨hx, hy⟩
-- x odd, y odd
· exfalso
obtain ⟨x0, y0, rfl, rfl⟩ : ∃ x0 y0, x = x0 * 2 + 1 ∧ y = y0 * 2 + 1 :=
by
obtain ⟨x0, hx2⟩ := exists_eq_mul_left_of_dvd (Int.dvd_self_sub_of_emod_eq hx)
obtain ⟨y0, hy2⟩ := exists_eq_mul_left_of_dvd (Int.dvd_self_sub_of_emod_eq hy)
rw [sub_eq_iff_eq_add] at hx2 hy2
exact ⟨x0, y0, hx2, hy2⟩
apply Int.sq_ne_two_mod_four z
rw [show z * z = 4 * (x0 * x0 + x0 + y0 * y0 + y0) + 2
by
rw [← h.eq]
ring]
simp only [Int.add_emod, Int.mul_emod_right, zero_add]
decide
