English
From any solution to a^4 + b^4 = c^2, there exists a minimal solution (in terms of |c|).
Русский
Любое решение a^4 + b^4 = c^2 порождает минимальное решение по |c|.
LaTeX
$$$\\exists a_0,b_0,c_0,\\ Fermat42\\ a_0\\ b_0\\ c_0 \\land Fermat42.Minimal\\ a_0\\ b_0\\ c_0$$$
Lean4
/-- if we have a solution to `a ^ 4 + b ^ 4 = c ^ 2` then there must be a minimal one. -/
theorem exists_minimal {a b c : ℤ} (h : Fermat42 a b c) : ∃ a0 b0 c0, Minimal a0 b0 c0 := by
classical
let S : Set ℕ := {n | ∃ s : ℤ × ℤ × ℤ, Fermat42 s.1 s.2.1 s.2.2 ∧ n = Int.natAbs s.2.2}
have S_nonempty : S.Nonempty := by
use Int.natAbs c
rw [Set.mem_setOf_eq]
use ⟨a, ⟨b, c⟩⟩
let m : ℕ := Nat.find S_nonempty
have m_mem : m ∈ S := Nat.find_spec S_nonempty
rcases m_mem with ⟨s0, hs0, hs1⟩
use s0.1, s0.2.1, s0.2.2, hs0
intro a1 b1 c1 h1
rw [← hs1]
apply Nat.find_min'
use ⟨a1, ⟨b1, c1⟩⟩
