---

Step * 1 of Lemma geometric-series-converges


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)))))]
BY
{ ((InstLemma `small-reciprocal-real` [⌜(r1 - c) * (r1/r(k))⌝]⋅ THENA Auto)
   THEN ExRepD
   THEN RenameVar `m' (-2)
   THEN With ⌜m⌝ (D (-5))⋅
   THEN Auto
   THEN ParallelLast
   THEN Auto
   THEN (InstHyp [⌜n + 1⌝] (-3)⋅ THENA Auto))⋅ }

1
1. c : {c:ℝ| (r0 ≤ c) ∧ (c < r1)} 
2. k : ℕ+
3. r0 < (r1 - c)
4. r0 < ((r1 - c) * (r1/r(k)))
5. m : ℕ+
6. (r1/r(m)) < ((r1 - c) * (r1/r(k)))
7. N : ℕ
8. ∀n:ℕ. ((N ≤ n) ⇒ (|c^n - r0| ≤ (r1/r(m))))
9. n : ℕ
10. N ≤ n
11. |c^n + 1 - r0| ≤ (r1/r(m))
⊢ |Σ{c^i | 0≤i≤n} - (r1/r1 - c)| ≤ (r1/r(k))

---

Latex:

---

Latex:

1.  c  :  \{c:\mBbbR{}|  (r0  \mleq{}  c)  \mwedge{}  (c  <  r1)\} 
2.  k  :  \mBbbN{}\msupplus{}
3.  lim  n\mrightarrow{}\minfty{}.c\^{}n  =  r0
4.  r0  <  (r1  -  c)
5.  r0  <  ((r1  -  c)  *  (r1/r(k)))
\mvdash{}  \mexists{}N:\mBbbN{}  [(\mforall{}n:\mBbbN{}.  ((N  \mleq{}  n)  {}\mRightarrow{}  (|\mSigma{}\{c\^{}i  |  0\mleq{}i\mleq{}n\}  -  (r1/r1  -  c)|  \mleq{}  (r1/r(k)))))]


By

---

Latex:
((InstLemma  `small-reciprocal-real`  [\mkleeneopen{}(r1  -  c)  *  (r1/r(k))\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  RenameVar  `m'  (-2)
  THEN  With  \mkleeneopen{}m\mkleeneclose{}  (D  (-5))\mcdot{}
  THEN  Auto
  THEN  ParallelLast
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}n  +  1\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto))\mcdot{}

---

Home Index