---

Step * of Lemma power-series-converges

No Annotations
∀a:ℕ ⟶ ℝ. ∀b:ℝ. ∀r:{r:ℝ| r0 < r} . ∀N:ℕ.
  ((∀n:{N...}. (|a[n + 1]| ≤ (|a[n]|/r))) ⇒ Σn.a[n] * x - b^n↓ absolutely for x ∈ (b - r, b + r))
BY
{ (Auto THEN BLemma `fun-ratio-test` THEN Auto THEN Try ((ProveRealContinuous THEN Auto)) THEN RepUR ``i-approx`` 0) }

1
1. a : ℕ ⟶ ℝ
2. b : ℝ
3. r : {r:ℝ| r0 < r} 
4. N : ℕ
5. ∀n:{N...}. (|a[n + 1]| ≤ (|a[n]|/r))
6. m : {m:ℕ+| icompact(i-approx((b - r, b + r);m))} 
⊢ ∃c:ℝ
   ((r0 ≤ c)
   ∧ (c < r1)
   ∧ (∃N:ℕ
       ∀n:{N...}. ∀x:{x:ℝ| (((b - r) + (r1/r(m))) ≤ x) ∧ (x ≤ ((b + r) - (r1/r(m))))} .
         (|a[n + 1] * x - b^n + 1| ≤ (c * |a[n] * x - b^n|))))

---

Latex:

---

Latex:
No  Annotations
\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{}  \mSigma{}n.a[n]  *  x  -  b\^{}n\mdownarrow{}  absolutely  for  x  \mmember{}  (b  -  r,  b  +  r))


By

---

Latex:
(Auto
  THEN  BLemma  `fun-ratio-test`
  THEN  Auto
  THEN  Try  ((ProveRealContinuous  THEN  Auto))
  THEN  RepUR  ``i-approx``  0)

---

Home Index