ne_zero — Mathlib

English

If a, b ≠ 0 and Fermat42 a b c holds, then c ≠ 0.

Русский

Если a ≠ 0 и b ≠ 0 и Fermat42 a b c, то c ≠ 0.

LaTeX

$$$\\forall a,b,c\\in \\mathbb{Z},\\ Fermat42\\ a\\ b\\ c \\rightarrow c \\neq 0$$$

Lean4

theorem ne_zero {a b c : ℤ} (h : Fermat42 a b c) : c ≠ 0 :=
  by
  apply ne_zero_pow two_ne_zero _; apply ne_of_gt
  rw [← h.2.2, (by ring : a ^ 4 + b ^ 4 = (a ^ 2) ^ 2 + (b ^ 2) ^ 2)]
  exact add_pos (sq_pos_of_ne_zero (pow_ne_zero 2 h.1)) (sq_pos_of_ne_zero (pow_ne_zero 2 h.2.1))

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