---

Step * 1 1 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])))
8. k : ℕ+
9. k@0 : ℕ+
10. (r1/r(k@0)) < (c/r(k))
⊢ ∃N:ℕ [(∀n,m:ℕ.  ((N ≤ n) ⇒ (N ≤ m) ⇒ (|Σ{x[i] | 0≤i≤n} - Σ{x[i] | 0≤i≤m}| ≤ (r1/r(k)))))]
BY
{ (RenameVar `M' (-2) THEN (D 3 With ⌜2 * M⌝  THENA Auto) THEN ExRepD THEN (D 0 With ⌜imax(N;N1)⌝  THENA Auto)) }

1
1. a : ℕ ⟶ ℝ
2. x : ℕ ⟶ ℝ
3. c : {c:ℝ| r0 < c} 
4. N : ℕ
5. ∀n:{N...}. ((r0 < a[n]) ∧ (r0 < x[n]))
6. ∀n:{N...}. ((r0 < a[n]) ∧ (c ≤ ((a[n] * x[n]/x[n + 1]) - a[n + 1])))
7. k : ℕ+
8. M : ℕ+
9. (r1/r(M)) < (c/r(k))
10. N1 : ℕ
11. ∀n:ℕ. ((N1 ≤ n) ⇒ (|(a[n] * x[n]) - r0| ≤ (r1/r(2 * M))))
⊢ ∀n,m:ℕ.  ((imax(N;N1) ≤ n) ⇒ (imax(N;N1) ≤ 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])))
8.  k  :  \mBbbN{}\msupplus{}
9.  k@0  :  \mBbbN{}\msupplus{}
10.  (r1/r(k@0))  <  (c/r(k))
\mvdash{}  \mexists{}N:\mBbbN{}  [(\mforall{}n,m:\mBbbN{}.    ((N  \mleq{}  n)  {}\mRightarrow{}  (N  \mleq{}  m)  {}\mRightarrow{}  (|\mSigma{}\{x[i]  |  0\mleq{}i\mleq{}n\}  -  \mSigma{}\{x[i]  |  0\mleq{}i\mleq{}m\}|  \mleq{}  (r1/r(k)))))]


By

---

Latex:
(RenameVar  `M'  (-2)
  THEN  (D  3  With  \mkleeneopen{}2  *  M\mkleeneclose{}    THENA  Auto)
  THEN  ExRepD
  THEN  (D  0  With  \mkleeneopen{}imax(N;N1)\mkleeneclose{}    THENA  Auto))

---

Home Index