fermatLastTheoremWith_nat_int_rat_tfae

English

For every natural n, the statements FermatLastTheoremWith Nat n, FermatLastTheoremWith Int n, and FermatLastTheoremWith Rat n are all equivalent.

Русский

Пусть для данного натурального n тождество FermatLastTheoremWith Nat n, FermatLastTheoremWith Int n и FermatLastTheoremWith Rat n взаимно эквивалентны.

LaTeX

$$$\\forall n \\in \\mathbb{N},\\ (FermatLastTheoremWith\\ Nat\\ n) \\iff (FermatLastTheoremWith\\ Int\\ n) \\iff (FermatLastTheoremWith\\ Rat\\ n)$$$

Lean4

theorem fermatLastTheoremWith_nat_int_rat_tfae (n : ℕ) :
    TFAE [FermatLastTheoremWith ℕ n, FermatLastTheoremWith ℤ n, FermatLastTheoremWith ℚ n] :=
  by
  tfae_have 1 → 2
    | h, a, b, c, ha, hb, hc, habc => by
      obtain hn | hn := n.even_or_odd
      · refine h a.natAbs b.natAbs c.natAbs (by positivity) (by positivity) (by positivity) (Int.natCast_inj.1 ?_)
        push_cast
        simp only [hn.pow_abs, habc]
      obtain ha | ha := ha.lt_or_gt <;> obtain hb | hb := hb.lt_or_gt <;> obtain hc | hc := hc.lt_or_gt
      · refine h a.natAbs b.natAbs c.natAbs (by positivity) (by positivity) (by positivity) (Int.natCast_inj.1 ?_)
        push_cast
        simp only [abs_of_neg, neg_pow a, neg_pow b, neg_pow c, ← mul_add, *]
      · exact (by positivity : 0 < c ^ n).not_gt <| habc.symm.trans_lt <| add_neg (hn.pow_neg ha) <| hn.pow_neg hb
      · refine h b.natAbs c.natAbs a.natAbs (by positivity) (by positivity) (by positivity) (Int.natCast_inj.1 ?_)
        push_cast
        simp only [abs_of_pos, abs_of_neg, hn.neg_pow, add_neg_eq_iff_eq_add, eq_neg_add_iff_add_eq, *]
      · refine h a.natAbs c.natAbs b.natAbs (by positivity) (by positivity) (by positivity) (Int.natCast_inj.1 ?_)
        push_cast
        simp only [abs_of_pos, abs_of_neg, hn.neg_pow, neg_add_eq_iff_eq_add, *]
      · refine h c.natAbs a.natAbs b.natAbs (by positivity) (by positivity) (by positivity) (Int.natCast_inj.1 ?_)
        push_cast
        simp only [abs_of_pos, abs_of_neg, hn.neg_pow, neg_add_eq_iff_eq_add, eq_add_neg_iff_add_eq, *]
      · refine h c.natAbs b.natAbs a.natAbs (by positivity) (by positivity) (by positivity) (Int.natCast_inj.1 ?_)
        push_cast
        simp only [abs_of_pos, abs_of_neg, hn.neg_pow, add_neg_eq_iff_eq_add, *]
      · exact (by positivity : 0 < a ^ n + b ^ n).not_gt <| habc.trans_lt <| hn.pow_neg hc
      · refine h a.natAbs b.natAbs c.natAbs (by positivity) (by positivity) (by positivity) (Int.natCast_inj.1 ?_)
        push_cast
        simp only [abs_of_pos, *]
  tfae_have 2 → 3
    | h, a, b, c, ha, hb, hc, habc => by
      rw [← Rat.num_ne_zero] at ha hb hc
      refine
        h (a.num * b.den * c.den) (a.den * b.num * c.den) (a.den * b.den * c.num) (by positivity) (by positivity)
          (by positivity) ?_
      have : (a.den * b.den * c.den : ℚ) ^ n ≠ 0 := by positivity
      refine Int.cast_injective <| (div_left_inj' this).1 ?_
      push_cast
      simp only [add_div, ← div_pow, mul_div_mul_comm, div_self (by positivity : (a.den : ℚ) ≠ 0),
        div_self (by positivity : (b.den : ℚ) ≠ 0), div_self (by positivity : (c.den : ℚ) ≠ 0), one_mul, mul_one,
        Rat.num_div_den, habc]
  tfae_have 3 → 1
    | h, a, b, c => mod_cast h a b c
  tfae_finish

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