fermatLastTheoremWith'_nat_int_tfae

English

For every natural n, the three propositions FermatLastTheoremFor n, FermatLastTheoremWith' ℕ n, and FermatLastTheoremWith' ℤ n are mutually equivalent (a three-way equivalence).

Русский

Для каждого натурального n три утверждения FermatLastTheoremFor n, FermatLastTheoremWith' ℕ n и FermatLastTheoremWith' ℤ n взаимно эквивалентны.

LaTeX

$$$\\forall n:\\mathbb{N},\\ (FermatLastTheoremFor\\ n) \\iff (FermatLastTheoremWith'\\ Nat\\ n) \\iff (FermatLastTheoremWith'\\ Int\\ n)$$$

Lean4

theorem fermatLastTheoremWith'_nat_int_tfae (n : ℕ) :
    TFAE [FermatLastTheoremFor n, FermatLastTheoremWith' ℕ n, FermatLastTheoremWith' ℤ n] :=
  by
  tfae_have 2 ↔ 1 := by
    apply fermatLastTheoremWith'_iff_fermatLastTheoremWith
    simp only [Nat.isUnit_iff]
    intro _ _ _ ha hb hc
    rw [ha, hb, hc]
    simp only [one_pow, Nat.reduceAdd, ne_eq, OfNat.ofNat_ne_one, not_false_eq_true]
  tfae_have 3 ↔ 1 := by
    rw [fermatLastTheoremFor_iff_int]
    apply fermatLastTheoremWith'_iff_fermatLastTheoremWith
    intro a b c ha hb hc
    by_cases hn : n = 0
    · subst hn
      simp only [pow_zero, Int.reduceAdd, ne_eq, OfNat.ofNat_ne_one, not_false_eq_true]
    · rw [← isUnit_pow_iff hn, Int.isUnit_iff] at ha hb hc
      rcases ha with ha | ha <;> rcases hb with hb | hb <;> rcases hc with hc | hc <;> rw [ha, hb, hc] <;> decide
  tfae_finish

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