---

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


1. a : ℕ ⟶ ℝ
2. g : ℝ ⟶ ℝ
3. ∀x:ℝ. Σi.a[i] * x^i = g[x]
4. ∀r:{r:ℝ| r0 < r} . ∃N:ℕ. ∀n:{N...}. (|a[n + 1]| ≤ (|a[n]|/r))
5. lim n→∞.Σ{a[i] * x - r0^i | 0≤i≤n} = λx.g[x] for x ∈ (-∞, ∞)
⊢ lim n→∞.Σ{a[i] * x^i | 0≤i≤n} = λx.g[x] for x ∈ (-∞, ∞)
BY
{ (MoveToConcl (-1)
   THEN BLemma `fun-converges-to_functionality`
   THEN Auto
   THEN (BLemma `rsum_functionality` THEN Auto)
   THEN D 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  \mBbbN{}  {}\mrightarrow{}  \mBbbR{}
2.  g  :  \mBbbR{}  {}\mrightarrow{}  \mBbbR{}
3.  \mforall{}x:\mBbbR{}.  \mSigma{}i.a[i]  *  x\^{}i  =  g[x]
4.  \mforall{}r:\{r:\mBbbR{}|  r0  <  r\}  .  \mexists{}N:\mBbbN{}.  \mforall{}n:\{N...\}.  (|a[n  +  1]|  \mleq{}  (|a[n]|/r))
5.  lim  n\mrightarrow{}\minfty{}.\mSigma{}\{a[i]  *  x  -  r0\^{}i  |  0\mleq{}i\mleq{}n\}  =  \mlambda{}x.g[x]  for  x  \mmember{}  (-\minfty{},  \minfty{})
\mvdash{}  lim  n\mrightarrow{}\minfty{}.\mSigma{}\{a[i]  *  x\^{}i  |  0\mleq{}i\mleq{}n\}  =  \mlambda{}x.g[x]  for  x  \mmember{}  (-\minfty{},  \minfty{})


By

---

Latex:
(MoveToConcl  (-1)
  THEN  BLemma  `fun-converges-to\_functionality`
  THEN  Auto
  THEN  (BLemma  `rsum\_functionality`  THEN  Auto)
  THEN  D  0
  THEN  Auto)

---

Home Index