Step
*
1
1
1
1
of Lemma
power-series-converges-everywhere-to
.....set predicate..... 
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)])} 
⊢ r0 < rmax(b + r(m + 1);r(m + 1) - b)
BY
{ (InstLemma `rless-cases` [⌜r(-(m + 1))⌝;⌜r(m + 1)⌝;⌜b⌝]⋅ 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(-(m + 1)) < b) ∨ (b < r(m + 1))
⊢ r0 < rmax(b + r(m + 1);r(m + 1) - b)
Latex:
Latex:
.....set  predicate..... 
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{}  r0  <  rmax(b  +  r(m  +  1);r(m  +  1)  -  b)
By
Latex:
(InstLemma  `rless-cases`  [\mkleeneopen{}r(-(m  +  1))\mkleeneclose{};\mkleeneopen{}r(m  +  1)\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
Home
Index