not_fermat_42 — Mathlib

English

There are no nontrivial integer solutions to a^4 + b^4 = c^2 when a and b are nonzero.

Русский

Не существует нетривиальных целочисленных решений уравнения $a^4+b^4=c^2$ при $a,b\neq 0$.

LaTeX

$$$\forall a,b,c \in \mathbb{Z}, \; a\neq 0, b\neq 0 \Rightarrow a^4 + b^4 \neq c^2$$$

Lean4

theorem not_fermat_42 {a b c : ℤ} (ha : a ≠ 0) (hb : b ≠ 0) : a ^ 4 + b ^ 4 ≠ c ^ 2 :=
  by
  intro h
  obtain ⟨a0, b0, c0, ⟨hf, h2, hp⟩⟩ := Fermat42.exists_pos_odd_minimal (And.intro ha (And.intro hb h))
  apply Fermat42.not_minimal hf h2 hp

Похожие утверждения