Lemma: Agent19_73d4b932d6e3.sum_range_pow_lt

For p≥2 and a≥1, the partial geometric sum 1+p+…+p^(a-1) is strictly less than p^a.

Exact formal statement

∀ {p a : Nat},
  LE.le.{0} 2 p →
    LT.lt.{0} 0 a →
      LT.lt.{0} (Finset.sum.{0, 0} (Finset.range a) fun i => HPow.hPow.{0, 0, 0} p i) (HPow.hPow.{0, 0, 0} p a)

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

Environment availability: available.

Public JSON record