---

Step * 2 of Lemma sum_of_geometric_prog

.....upcase..... 
1. r : CRng
2. a : |r|
3. n : ℤ
4. 0 < n
5. ((1 +r (-r a)) * (Σ(r) 0 ≤ i < n - 1. a ↑r i)) = (1 +r (-r (a ↑r (n - 1)))) ∈ |r|
⊢ ((1 +r (-r a)) * (Σ(r) 0 ≤ i < n. a ↑r i)) = (1 +r (-r (a ↑r n))) ∈ |r|
BY
{ % Slightly ugly, since working over a ring rather than field % 
 
((RWH (LemmaC `rng_sum_unroll_hi`) 0 
THENM RWH (GenLemmaC 1 `rng_times_over_plus`  
           ANDTHENC HigherC (HypC 5)) 0) THENA Auto) 
THEN Thin 5 }

1
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|

---

Latex:

---

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


By

---

Latex:
\%  Slightly  ugly,  since  working  over  a  ring  rather  than  field  \% 
 
((RWH  (LemmaC  `rng\_sum\_unroll\_hi`)  0 
THENM  RWH  (GenLemmaC  1  `rng\_times\_over\_plus`   
                      ANDTHENC  HigherC  (HypC  5))  0)  THENA  Auto) 
THEN  Thin  5

---

Home Index