---

Step * 2 1 of Lemma sum_of_geometric_prog


1. r : CRng
2. a : |r|
3. n : ℤ
4. 0 < n
⊢ ((1 +r (-r (a ↑r (n - 1)))) +r ((1 +r (-r a)) * (a ↑r (n - 1)))) = (1 +r (-r (a ↑r n))) ∈ |r|
BY
{ ((RW (NthC 3 (LemmaC `rng_nexp_unroll`) ANDTHENC CRngNormC) 0) THEN Auto) }

---

Latex:

---

Latex:

1.  r  :  CRng
2.  a  :  |r|
3.  n  :  \mBbbZ{}
4.  0  <  n
\mvdash{}  ((1  +r  (-r  (a  \muparrow{}r  (n  -  1))))  +r  ((1  +r  (-r  a))  *  (a  \muparrow{}r  (n  -  1))))  =  (1  +r  (-r  (a  \muparrow{}r  n)))


By

---

Latex:
((RW  (NthC  3  (LemmaC  `rng\_nexp\_unroll`)  ANDTHENC  CRngNormC)  0)  THEN  Auto)

---

Home Index