FLT/Basic/Lemmas.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Pinned FLT blueprint introduction

3 declarations, 0 contain sorry, 0 declared as axioms

The reduction of FLT to the p>=5 prime case.

Imports (3)
Imported by 3 files
  1. theorem Nat.three_dvd_or_four_dvd_or_prime_dvd line 22 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, LE.le, OfNat.ofNat, Or, Dvd.dvd, Exists, And, Nat.Prime

    Proof uses: Odd, Nat.four_dvd_or_exists_odd_prime_and_dvd_of_two_lt, Eq, Ne, eq_or_ne, Eq.symm, Or.inr, Exists.intro, And.intro

    14 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

    Open to load the checked before-and-after goal states.

  2. lemma FermatLastTheorem.of_p_ge_5 It suffices to prove FLT for primes at least 5 line 38 source

    Source documentation

    If Fermat's Last Theorem is true for primes p ≥ 5, then FLT is true.

    L4DEL explanation

    Any exponent n at least 3 is divisible by 3, by 4, or by a prime at least 5, and FLT for a divisor implies FLT for the multiple.

    1. Split on the arithmetic fact that n is divisible by 3, or by 4, or by some prime p at least 5.
    2. If 3 divides n, use Euler's theorem fermatLastTheoremThree from Mathlib and monotonicity along divisibility.
    3. If 4 divides n, use Fermat's theorem fermatLastTheoremFour from Mathlib in the same way.
    4. Otherwise a prime p at least 5 divides n and the hypothesis H gives FLT for p, which passes up to n.

    Prerequisites: Nat.three_dvd_or_four_dvd_or_prime_dvd

    See also: FLT.Bosses.B2_implies_B1

    Sources and attribution: Pinned Lean source (f6c6a2fe9796)

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, GE.ge, OfNat.ofNat, Nat.Prime, FermatLastTheoremFor, FermatLastTheorem

    Proof uses: Dvd.dvd, Or, Exists, And, LE.le, Nat.three_dvd_or_four_dvd_or_prime_dvd, FermatLastTheoremFor.mono, fermatLastTheoremThree, fermatLastTheoremFour

    8 instances, coercions and auxiliary constants left out.

    Tactic trace: 11 steps

    Open to load the checked before-and-after goal states.

    lemma FermatLastTheorem.of_p_ge_5 (H : ∀ p ≥ 5, p.Prime → FermatLastTheoremFor p) :
    FermatLastTheorem := by
…
  3. theorem PNat.pow_add_pow_ne_pow_of_FermatLastTheorem Fermat's Last Theorem as stated in mathlib (a statement FermatLastTheorem about naturals) implies Fermat's Last Theorem stated in terms of positive integers line 60 source

    Source documentation

    Fermat's Last Theorem as stated in mathlib (a statement FermatLastTheorem about naturals) implies Fermat's Last Theorem stated in terms of positive integers.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: FermatLastTheorem, PNat, Nat, GT.gt, OfNat.ofNat, Ne, HAdd.hAdd, HPow.hPow

    Proof uses: id, Eq.mp, Not, Eq, congrArg, of_eq_true, Eq.trans, False, True, not_false_eq_true

    28 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

    Open to load the checked before-and-after goal states.

    theorem PNat.pow_add_pow_ne_pow_of_FermatLastTheorem :
    FermatLastTheorem → ∀ (a b c : ℕ+) (n : ℕ) (_ : n > 2),
    a ^ n + b ^ n ≠ c ^ n := by
…