English
There exists a minimal solution to a^4 + b^4 = c^2 with a odd.
Русский
Существует минимальное решение с нечетным a.
LaTeX
$$$\\exists a_0,b_0,c_0:\\ Fermat42.Minimal\\ a_0\\ b_0\\ c_0 \\land a_0 \\equiv 1 \\pmod{2}$$$
Lean4
/-- a minimal solution to `a ^ 4 + b ^ 4 = c ^ 2` must have `a` and `b` coprime. -/
theorem coprime_of_minimal {a b c : ℤ} (h : Minimal a b c) : IsCoprime a b :=
by
apply Int.isCoprime_iff_gcd_eq_one.mpr
by_contra hab
obtain ⟨p, hp, hpa, hpb⟩ := Nat.Prime.not_coprime_iff_dvd.mp hab
obtain ⟨a1, rfl⟩ := Int.natCast_dvd.mpr hpa
obtain ⟨b1, rfl⟩ := Int.natCast_dvd.mpr hpb
have hpc : (p : ℤ) ^ 2 ∣ c := by
rw [← Int.pow_dvd_pow_iff two_ne_zero, ← h.1.2.2]
apply Dvd.intro (a1 ^ 4 + b1 ^ 4)
ring
obtain ⟨c1, rfl⟩ := hpc
have hf : Fermat42 a1 b1 c1 := (Fermat42.mul (Int.natCast_ne_zero.mpr (Nat.Prime.ne_zero hp))).mpr h.1
apply Nat.le_lt_asymm (h.2 _ _ _ hf)
rw [Int.natAbs_mul, lt_mul_iff_one_lt_left, Int.natAbs_pow, Int.natAbs_natCast]
· exact Nat.one_lt_pow two_ne_zero (Nat.Prime.one_lt hp)
· exact Nat.pos_of_ne_zero (Int.natAbs_ne_zero.2 (ne_zero hf))
