---

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

.....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) 
BY
{ (D 0 With ⌜rmax(b + r(m + 1);r(m + 1) - b)⌝  THEN Auto) }

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

---

Latex:

---

Latex:
.....assertion..... 
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{}  \mexists{}r:\{r:\mBbbR{}|  r0  <  r\}  .  [r(-m),  r(m)]  \msubseteq{}  (b  -  r,  b  +  r) 


By

---

Latex:
(D  0  With  \mkleeneopen{}rmax(b  +  r(m  +  1);r(m  +  1)  -  b)\mkleeneclose{}    THEN  Auto)

---

Home Index