English
There exists a minimal odd-a solution to a^4 + b^4 = c^2; a repeated variant as in prior lemma ensures a minimal odd-a exists.
Русский
Существует минимальное решение с нечетным a; повторение леммы подтверждает существование такого решения.
LaTeX
$$$\\exists a,b,c:\\ Fermat42.Minimal\\ a\\ b\\ c \\land a\\equiv 1\\ (mod\\ 2)$$$
Lean4
/-- We can assume that a minimal solution to `a ^ 4 + b ^ 4 = c ^ 2` has `a` odd. -/
theorem exists_odd_minimal {a b c : ℤ} (h : Fermat42 a b c) : ∃ a0 b0 c0, Minimal a0 b0 c0 ∧ a0 % 2 = 1 :=
by
obtain ⟨a0, b0, c0, hf⟩ := exists_minimal h
rcases Int.emod_two_eq_zero_or_one a0 with hap | hap
· rcases Int.emod_two_eq_zero_or_one b0 with hbp | hbp
· exfalso
have h1 : 2 ∣ (Int.gcd a0 b0 : ℤ) := Int.dvd_coe_gcd (Int.dvd_of_emod_eq_zero hap) (Int.dvd_of_emod_eq_zero hbp)
rw [Int.isCoprime_iff_gcd_eq_one.mp (coprime_of_minimal hf)] at h1
revert h1
decide
· exact ⟨b0, ⟨a0, ⟨c0, minimal_comm hf, hbp⟩⟩⟩
exact ⟨a0, ⟨b0, ⟨c0, hf, hap⟩⟩⟩
