Lemma: MrTheorem18_SixthPowers_e8fb6433.summand_count_mod_seven

If a sum of n natural-number sixth powers equals a sixth power, and none of the n bases is divisible by 7, then n is congruent to 0 or 1 modulo 7. This is a restricted modular obstruction, not the general Euler conjecture.

Exact formal statement

∀ (n b : Nat) (a : Fin n → Nat),
  (∀ (i : Fin n), Not (Dvd.dvd.{0} 7 (a i))) →
    Eq.{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) →
      Or (Eq.{1} (HMod.hMod.{0, 0, 0} n 7) 0) (Eq.{1} (HMod.hMod.{0, 0, 0} n 7) 1)

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

Environment availability: available.

Public JSON record