---

Step * of Lemma power-series-converges-to

∀a:ℕ ⟶ ℝ. ∀b:ℝ. ∀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))))
BY
{ (InstLemma `power-series-converges` []
   THEN RepeatFor 5 (ParallelLast')
   THEN Auto
   THEN BLemma `fun-converges-converges-to`
   THEN Auto) }

1
1. a : ℕ ⟶ ℝ
2. b : ℝ
3. r : {r:ℝ| r0 < r} 
4. N : ℕ
5. ∀n:{N...}. (|a[n + 1]| ≤ (|a[n]|/r))
6. Σn.a[n] * x - b^n↓ absolutely for x ∈ (b - r, b + r)
7. g : (b - r, b + r) ⟶ℝ
8. ∀x:{x:ℝ| x ∈ (b - r, b + r)} . Σi.a[i] * x - b^i = g[x]
⊢ λn.Σ{a[i] * x - b^i | 0≤i≤n}↓ for x ∈ (b - r, b + r))

---

Latex:

---

Latex:
\mforall{}a:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}.  \mforall{}b:\mBbbR{}.  \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))))


By

---

Latex:
(InstLemma  `power-series-converges`  []
  THEN  RepeatFor  5  (ParallelLast')
  THEN  Auto
  THEN  BLemma  `fun-converges-converges-to`
  THEN  Auto)

---

Home Index