English
Let a, b, c be integers solving a^4 + b^4 = c^2. There exists a minimal such triple (a0, b0, c0) with a0 odd and c0 > 0.
Русский
Пусть целые числа a, b, c удовлетворяют a^4 + b^4 = c^2. Существует минимальное по начальному определению тройку (a0, b0, c0), для которой a0 нечетно и c0 > 0.
LaTeX
$$$\exists a_0,b_0,c_0 \in \mathbb{Z},\; \text{Minimal}(a_0,b_0,c_0) \wedge a_0 \equiv 1 \pmod 2 \wedge 0 < c_0$$$
Lean4
/-- We can assume that a minimal solution to `a ^ 4 + b ^ 4 = c ^ 2` has
`a` odd and `c` positive. -/
theorem exists_pos_odd_minimal {a b c : ℤ} (h : Fermat42 a b c) : ∃ a0 b0 c0, Minimal a0 b0 c0 ∧ a0 % 2 = 1 ∧ 0 < c0 :=
by
obtain ⟨a0, b0, c0, hf, hc⟩ := exists_odd_minimal h
rcases lt_trichotomy 0 c0 with (h1 | h1 | h1)
· use a0, b0, c0
· exfalso
exact ne_zero hf.1 h1.symm
· use a0, b0, -c0, neg_of_minimal hf, hc
exact neg_pos.mpr h1
