---

Step * of Lemma power-series-converges-everywhere

No Annotations
∀a:ℕ ⟶ ℝ. ∀g:ℝ ⟶ ℝ.
  ((∀x:ℝ. Σi.a[i] * x^i = g[x])
  ⇒ (∀r:{r:ℝ| r0 < r} . ∃N:ℕ. ∀n:{N...}. (|a[n + 1]| ≤ (|a[n]|/r)))
  ⇒ lim n→∞.Σ{a[i] * x^i | 0≤i≤n} = λx.g[x] for x ∈ (-∞, ∞))
BY
{ ((InstLemma `power-series-converges-everywhere-to` [] THEN ParallelLast')
   THEN (D -1 With ⌜r0⌝  THENA Auto)
   THEN RepeatFor 2 (ParallelLast')
   THEN Auto) }

1
1. a : ℕ ⟶ ℝ
2. g : ℝ ⟶ ℝ
3. ∀x:ℝ. Σi.a[i] * x^i = g[x]
4. x : ℝ
⊢ Σi.a[i] * x - r0^i = g[x]

2
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 ∈ (-∞, ∞)

---

Latex:

---

Latex:
No  Annotations
\mforall{}a:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}.  \mforall{}g:\mBbbR{}  {}\mrightarrow{}  \mBbbR{}.
    ((\mforall{}x:\mBbbR{}.  \mSigma{}i.a[i]  *  x\^{}i  =  g[x])
    {}\mRightarrow{}  (\mforall{}r:\{r:\mBbbR{}|  r0  <  r\}  .  \mexists{}N:\mBbbN{}.  \mforall{}n:\{N...\}.  (|a[n  +  1]|  \mleq{}  (|a[n]|/r)))
    {}\mRightarrow{}  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:
((InstLemma  `power-series-converges-everywhere-to`  []  THEN  ParallelLast')
  THEN  (D  -1  With  \mkleeneopen{}r0\mkleeneclose{}    THENA  Auto)
  THEN  RepeatFor  2  (ParallelLast')
  THEN  Auto)

---

Home Index