---

Step * of Lemma geom-sum-int

∀[a:ℤ]. ∀[n:ℕ].  (((1 - a) * Σ(a^i | i < n)) = (1 - a^n) ∈ ℤ)
BY
{ (Auto
   THEN (InstLemma `sum_of_geometric_prog` [⌜ℤ-rng⌝;⌜a⌝;⌜n⌝]⋅ THENA Auto)
   THEN (RWO "rng_sum-int" (-1) THENA Auto)
   THEN (RWO "rng_nexp-int" (-1) THENA Auto)
   THEN RepUR ``int_ring`` -1) }

1
1. a : ℤ
2. n : ℕ
3. ((1 + (-a)) * Σ(a^(0 + i) | i < n - 0)) = (1 + (-a^n)) ∈ ℤ
⊢ ((1 - a) * Σ(a^i | i < n)) = (1 - a^n) ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[a:\mBbbZ{}].  \mforall{}[n:\mBbbN{}].    (((1  -  a)  *  \mSigma{}(a\^{}i  |  i  <  n))  =  (1  -  a\^{}n))


By

---

Latex:
(Auto
  THEN  (InstLemma  `sum\_of\_geometric\_prog`  [\mkleeneopen{}\mBbbZ{}-rng\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "rng\_sum-int"  (-1)  THENA  Auto)
  THEN  (RWO  "rng\_nexp-int"  (-1)  THENA  Auto)
  THEN  RepUR  ``int\_ring``  -1)

---

Home Index