---

Step * of Lemma sum_of_geometric_prog

∀[r:CRng]. ∀[a:|r|]. ∀[n:ℕ].  (((1 +r (-r a)) * (Σ(r) 0 ≤ i < n. a ↑r i)) = (1 +r (-r (a ↑r n))) ∈ |r|)
BY
{ ((RepD THENM OnVar `n' NatInd) THENA Auto) }

1
.....basecase..... 
1. r : CRng
2. a : |r|
3. n : ℤ
⊢ ((1 +r (-r a)) * (Σ(r) 0 ≤ i < 0. a ↑r i)) = (1 +r (-r (a ↑r 0))) ∈ |r|

2
.....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|

---

Latex:

---

Latex:
\mforall{}[r:CRng].  \mforall{}[a:|r|].  \mforall{}[n:\mBbbN{}].    (((1  +r  (-r  a))  *  (\mSigma{}(r)  0  \mleq{}  i  <  n.  a  \muparrow{}r  i))  =  (1  +r  (-r  (a  \muparrow{}r  n))))


By

---

Latex:
((RepD  THENM  OnVar  `n'  NatInd)  THENA  Auto)

---

Home Index