---

Step * of Lemma partial-geometric-series

No Annotations
∀n:ℕ. ∀c:ℝ.  (c ≠ r1 ⇒ (Σ{c^i | 0≤i≤n} = (r1 - c^n + 1/r1 - c)))
BY
{ (Auto THEN (Assert r0 ≠ r1 - c BY (RepeatFor 2 (ParallelLast) THEN nRAdd ⌜c⌝ 0⋅ THEN Auto))) }

1
1. n : ℕ
2. c : ℝ
3. c ≠ r1
4. r0 ≠ r1 - c
⊢ Σ{c^i | 0≤i≤n} = (r1 - c^n + 1/r1 - c)

---

Latex:

---

Latex:
No  Annotations
\mforall{}n:\mBbbN{}.  \mforall{}c:\mBbbR{}.    (c  \mneq{}  r1  {}\mRightarrow{}  (\mSigma{}\{c\^{}i  |  0\mleq{}i\mleq{}n\}  =  (r1  -  c\^{}n  +  1/r1  -  c)))


By

---

Latex:
(Auto  THEN  (Assert  r0  \mneq{}  r1  -  c  BY  (RepeatFor  2  (ParallelLast)  THEN  nRAdd  \mkleeneopen{}c\mkleeneclose{}  0\mcdot{}  THEN  Auto)))

---

Home Index