---

Step * 1 1 2 2 of Lemma power-series-converges-everywhere-to


1. a : ℕ ⟶ ℝ
2. b : ℝ
3. ∀r:{r:ℝ| r0 < r} . ∀N:ℕ.
     ((∀n:{N...}. (|a[n + 1]| ≤ (|a[n]|/r)))
     ⇒ (∀g:(b - r, b + r) ⟶ℝ
           ((∀x:{x:ℝ| x ∈ (b - r, b + r)} . Σi.a[i] * x - b^i = g[x])
           ⇒ lim n→∞.Σ{a[i] * x - b^i | 0≤i≤n} = λx.g[x] for x ∈ (b - r, b + r))))
4. g : ℝ ⟶ ℝ
5. ∀x:ℝ. Σi.a[i] * x - b^i = g[x]
6. ∀r:{r:ℝ| r0 < r} . ∃N:ℕ. ∀n:{N...}. (|a[n + 1]| ≤ (|a[n]|/r))
7. m : {m:ℕ+| icompact([r(-m), r(m)])} 
8. r : ℝ
9. r(-m) ≤ r
10. r ≤ r(m)
11. (b - rmax(b + r(m + 1);r(m + 1) - b)) < r
⊢ r < (b + rmax(b + r(m + 1);r(m + 1) - b))
BY
{ (RWO "-2" 0 THENA Auto) }

1
1. a : ℕ ⟶ ℝ
2. b : ℝ
3. ∀r:{r:ℝ| r0 < r} . ∀N:ℕ.
     ((∀n:{N...}. (|a[n + 1]| ≤ (|a[n]|/r)))
     ⇒ (∀g:(b - r, b + r) ⟶ℝ
           ((∀x:{x:ℝ| x ∈ (b - r, b + r)} . Σi.a[i] * x - b^i = g[x])
           ⇒ lim n→∞.Σ{a[i] * x - b^i | 0≤i≤n} = λx.g[x] for x ∈ (b - r, b + r))))
4. g : ℝ ⟶ ℝ
5. ∀x:ℝ. Σi.a[i] * x - b^i = g[x]
6. ∀r:{r:ℝ| r0 < r} . ∃N:ℕ. ∀n:{N...}. (|a[n + 1]| ≤ (|a[n]|/r))
7. m : {m:ℕ+| icompact([r(-m), r(m)])} 
8. r : ℝ
9. r(-m) ≤ r
10. r ≤ r(m)
11. (b - rmax(b + r(m + 1);r(m + 1) - b)) < r
⊢ r(m) < (b + rmax(b + r(m + 1);r(m + 1) - b))

---

Latex:

---

Latex:

1.  a  :  \mBbbN{}  {}\mrightarrow{}  \mBbbR{}
2.  b  :  \mBbbR{}
3.  \mforall{}r:\{r:\mBbbR{}|  r0  <  r\}  .  \mforall{}N:\mBbbN{}.
          ((\mforall{}n:\{N...\}.  (|a[n  +  1]|  \mleq{}  (|a[n]|/r)))
          {}\mRightarrow{}  (\mforall{}g:(b  -  r,  b  +  r)  {}\mrightarrow{}\mBbbR{}
                      ((\mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  (b  -  r,  b  +  r)\}  .  \mSigma{}i.a[i]  *  x  -  b\^{}i  =  g[x])
                      {}\mRightarrow{}  lim  n\mrightarrow{}\minfty{}.\mSigma{}\{a[i]  *  x  -  b\^{}i  |  0\mleq{}i\mleq{}n\}  =  \mlambda{}x.g[x]  for  x  \mmember{}  (b  -  r,  b  +  r))))
4.  g  :  \mBbbR{}  {}\mrightarrow{}  \mBbbR{}
5.  \mforall{}x:\mBbbR{}.  \mSigma{}i.a[i]  *  x  -  b\^{}i  =  g[x]
6.  \mforall{}r:\{r:\mBbbR{}|  r0  <  r\}  .  \mexists{}N:\mBbbN{}.  \mforall{}n:\{N...\}.  (|a[n  +  1]|  \mleq{}  (|a[n]|/r))
7.  m  :  \{m:\mBbbN{}\msupplus{}|  icompact([r(-m),  r(m)])\} 
8.  r  :  \mBbbR{}
9.  r(-m)  \mleq{}  r
10.  r  \mleq{}  r(m)
11.  (b  -  rmax(b  +  r(m  +  1);r(m  +  1)  -  b))  <  r
\mvdash{}  r  <  (b  +  rmax(b  +  r(m  +  1);r(m  +  1)  -  b))


By

---

Latex:
(RWO  "-2"  0  THENA  Auto)

---

Home Index