---

Step * of Lemma geometric-series-converges

No Annotations
∀c:{c:ℝ| (r0 ≤ c) ∧ (c < r1)} . Σn.c^n = (r1/r1 - c)
BY
{ ((Auto THEN D 0 THEN Auto)
   THEN (Assert lim n→∞.c^n = r0 BY
               (BLemma `rnexp-converges-ext` THEN Auto THEN (RWO "rabs-of-nonneg" 0 THEN Auto)⋅))
   THEN (Assert r0 < (r1 - c) BY
               (nRAdd ⌜c⌝ 0⋅ THEN Auto))
   THEN DupHyp (-1)
   THEN (RW (nRMul2C ⌜(r1/r(k))⌝) (-1)⋅ THENA Auto)
   THEN (RWO "rmul-zero-both.2" (-1) THENA Auto)) }

1
1. c : {c:ℝ| (r0 ≤ c) ∧ (c < r1)} 
2. k : ℕ+
3. lim n→∞.c^n = r0
4. r0 < (r1 - c)
5. r0 < ((r1 - c) * (r1/r(k)))
⊢ ∃N:ℕ [(∀n:ℕ. ((N ≤ n) ⇒ (|Σ{c^i | 0≤i≤n} - (r1/r1 - c)| ≤ (r1/r(k)))))]

---

Latex:

---

Latex:
No  Annotations
\mforall{}c:\{c:\mBbbR{}|  (r0  \mleq{}  c)  \mwedge{}  (c  <  r1)\}  .  \mSigma{}n.c\^{}n  =  (r1/r1  -  c)


By

---

Latex:
((Auto  THEN  D  0  THEN  Auto)
  THEN  (Assert  lim  n\mrightarrow{}\minfty{}.c\^{}n  =  r0  BY
                          (BLemma  `rnexp-converges-ext`  THEN  Auto  THEN  (RWO  "rabs-of-nonneg"  0  THEN  Auto)\mcdot{}))
  THEN  (Assert  r0  <  (r1  -  c)  BY
                          (nRAdd  \mkleeneopen{}c\mkleeneclose{}  0\mcdot{}  THEN  Auto))
  THEN  DupHyp  (-1)
  THEN  (RW  (nRMul2C  \mkleeneopen{}(r1/r(k))\mkleeneclose{})  (-1)\mcdot{}  THENA  Auto)
  THEN  (RWO  "rmul-zero-both.2"  (-1)  THENA  Auto))

---

Home Index