---

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


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))
BY
{ ((FLemma `fun-series-converges-absolutely-converges` [-3] THENA Auto) THEN UnfoldTopAb (-1) THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
((FLemma  `fun-series-converges-absolutely-converges`  [-3]  THENA  Auto)
  THEN  UnfoldTopAb  (-1)
  THEN  Auto)

---

Home Index