Lemma: MrTheorem18_SixthPowers_e8fb6433.no_two_to_five_sixth_powers

A sum of two through five natural-number sixth powers, with every base not divisible by 7, cannot equal any natural-number sixth power. Only this restricted k = 6 case is proved.

Exact formal statement

∀ (n b : Nat) (a : Fin n → Nat),
  LE.le.{0} 2 n →
    LE.le.{0} n 5 →
      (∀ (i : Fin n), Not (Dvd.dvd.{0} 7 (a i))) →
        Ne.{1} (Finset.sum.{0, 0} Finset.univ.{0} fun i => HPow.hPow.{0, 0, 0} (a i) 6) (HPow.hPow.{0, 0, 0} b 6)

This is a published formal lemma. Its scope is the exact statement above.

Environment availability: available.

Public JSON record