11.5. Assembly🔗

Theorem11.5.1

Statement uses 4

Statement dependency previews

Preview

Theorem 11.2.5

Loading preview

Statement dependency preview content is loaded from the Blueprint HTML cache.

used by 0✓L∃∀N

If (1) every case-I solution (a,b,c) at \ell = 37 satisfies \mathrm{MirimanoffBernoulliConclusion}\ 37\ a\ b, and (2) \mathrm{VandiverLemma1Thirtyseven} holds, then \mathrm{FermatLastTheoremFor}\ 37.

Theorem 11.3.4 Theorem 11.4.3 Theorem 11.2.5 Theorem 11.4.1

Lean code for Theorem11.5.1●1 theorem

theoremdefined in BernoulliRegular/FLT37/Final.lean

complete

theorem BernoulliRegular.FLT37.fermatLastTheoremFor_thirtyseven_of_conclusion_and_vandiverLemma1
  (h_conclusion :
    ∀ ⦃a b c : ℤ⦄,
      a ^ 37 + b ^ 37 = c ^ 37 →
        ¬37 ∣ b →
          ¬37 ∣ c →
            BernoulliRegular.FLT37.MirimanoffBernoulliConclusion 37 a b)
  (h_caseII : BernoulliRegular.FLT37.VandiverLemma1Thirtyseven) :
  FermatLastTheoremFor 37

theorem BernoulliRegular.FLT37.fermatLastTheoremFor_thirtyseven_of_conclusion_and_vandiverLemma1
  (h_conclusion :
    ∀ ⦃a b c : ℤ⦄,
      a ^ 37 + b ^ 37 = c ^ 37 →
        ¬37 ∣ b →
          ¬37 ∣ c →
            BernoulliRegular.FLT37.MirimanoffBernoulliConclusion
              37 a b)
  (h_caseII :
    BernoulliRegular.FLT37.VandiverLemma1Thirtyseven) :
  FermatLastTheoremFor 37

**ℓ = 37 final assembly via 37-specific predicates.** Uses the 37-specific
case II predicate `VandiverLemma1Thirtyseven` (instead of the universal
`VandiverIIICaseII`), giving a tighter conditional statement.