---

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

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

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)])} 
⊢ ∀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:
No  Annotations
\mforall{}a:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}.  \mforall{}b:\mBbbR{}.  \mforall{}g:\mBbbR{}  {}\mrightarrow{}  \mBbbR{}.
    ((\mforall{}x:\mBbbR{}.  \mSigma{}i.a[i]  *  x  -  b\^{}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  -  b\^{}i  |  0\mleq{}i\mleq{}n\}  =  \mlambda{}x.g[x]  for  x  \mmember{}  (-\minfty{},  \minfty{}))


By

---

Latex:
(InstLemma  `power-series-converges-to`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  Auto
  THEN  (D  0  THENA  Auto)
  THEN  RepUR  ``i-approx``  -1
  THEN  RepUR  ``i-approx``  0)

---

Home Index