---

Step * 1 of Lemma Kummer-criterion


1. a : ℕ ⟶ ℝ
2. x : ℕ ⟶ ℝ
3. lim n→∞.a[n] * x[n] = r0
4. c : {c:ℝ| r0 < c} 
5. N : ℕ
6. ∀n:{N...}. ((r0 < a[n]) ∧ (r0 < x[n]))
7. ∀n:{N...}. ((r0 < a[n]) ∧ (c ≤ ((a[n] * x[n]/x[n + 1]) - a[n + 1])))
⊢ Σn.x[n]↓
BY
{ (UnfoldTopAb 0
   THEN Unfold `series-sum` 0
   THEN Fold `converges` 0
   THEN (BLemma `converges-iff-cauchy-ext` THENA Auto)
   THEN (D 0 THENA Auto)) }

1
1. a : ℕ ⟶ ℝ
2. x : ℕ ⟶ ℝ
3. lim n→∞.a[n] * x[n] = r0
4. c : {c:ℝ| r0 < c} 
5. N : ℕ
6. ∀n:{N...}. ((r0 < a[n]) ∧ (r0 < x[n]))
7. ∀n:{N...}. ((r0 < a[n]) ∧ (c ≤ ((a[n] * x[n]/x[n + 1]) - a[n + 1])))
8. k : ℕ+
⊢ ∃N:ℕ [(∀n,m:ℕ.  ((N ≤ n) ⇒ (N ≤ m) ⇒ (|Σ{x[i] | 0≤i≤n} - Σ{x[i] | 0≤i≤m}| ≤ (r1/r(k)))))]

---

Latex:

---

Latex:

1.  a  :  \mBbbN{}  {}\mrightarrow{}  \mBbbR{}
2.  x  :  \mBbbN{}  {}\mrightarrow{}  \mBbbR{}
3.  lim  n\mrightarrow{}\minfty{}.a[n]  *  x[n]  =  r0
4.  c  :  \{c:\mBbbR{}|  r0  <  c\} 
5.  N  :  \mBbbN{}
6.  \mforall{}n:\{N...\}.  ((r0  <  a[n])  \mwedge{}  (r0  <  x[n]))
7.  \mforall{}n:\{N...\}.  ((r0  <  a[n])  \mwedge{}  (c  \mleq{}  ((a[n]  *  x[n]/x[n  +  1])  -  a[n  +  1])))
\mvdash{}  \mSigma{}n.x[n]\mdownarrow{}


By

---

Latex:
(UnfoldTopAb  0
  THEN  Unfold  `series-sum`  0
  THEN  Fold  `converges`  0
  THEN  (BLemma  `converges-iff-cauchy-ext`  THENA  Auto)
  THEN  (D  0  THENA  Auto))

---

Home Index