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