---

Step * 1 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)])} 
⊢ ∀k:ℕ+. ∃N:ℕ+. ∀x:{x:ℝ| (r(-m) ≤ x) ∧ (x ≤ r(m))} . ∀n:{N...}.  (|Σ{a[i] * x - b^i | 0≤i≤n} - g[x]| ≤ (r1/r(k)))
BY
{ Assert ⌜∃r:{r:ℝ| r0 < r} . [r(-m), r(m)] ⊆ (b - r, b + r) ⌝⋅ }

1
.....assertion..... 
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)])} 
⊢ ∃r:{r:ℝ| r0 < r} . [r(-m), r(m)] ⊆ (b - r, b + r) 

2
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:{r:ℝ| r0 < r} . [r(-m), r(m)] ⊆ (b - r, b + r) 
⊢ ∀k:ℕ+. ∃N:ℕ+. ∀x:{x:ℝ| (r(-m) ≤ x) ∧ (x ≤ r(m))} . ∀n:{N...}.  (|Σ{a[i] * x - b^i | 0≤i≤n} - g[x]| ≤ (r1/r(k)))

---

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)])\} 
\mvdash{}  \mforall{}k:\mBbbN{}\msupplus{}
        \mexists{}N:\mBbbN{}\msupplus{}
          \mforall{}x:\{x:\mBbbR{}|  (r(-m)  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r(m))\}  .  \mforall{}n:\{N...\}.
              (|\mSigma{}\{a[i]  *  x  -  b\^{}i  |  0\mleq{}i\mleq{}n\}  -  g[x]|  \mleq{}  (r1/r(k)))


By

---

Latex:
Assert  \mkleeneopen{}\mexists{}r:\{r:\mBbbR{}|  r0  <  r\}  .  [r(-m),  r(m)]  \msubseteq{}  (b  -  r,  b  +  r)  \mkleeneclose{}\mcdot{}

---

Home Index