---

Step * 1 1 1 1 1 2 1 of Lemma Kummer-criterion

.....assertion..... 
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))))
12. J : ℤ
13. imax(N;N1) = J ∈ ℤ
14. N ≤ J
15. N1 ≤ J
16. n : ℕ
17. m : ℕ
18. J ≤ n
19. J ≤ m
20. ∀n,m:ℕ.  ((J ≤ n) ⇒ (J ≤ m) ⇒ (|(a[n] * x[n]) - a[m] * x[m]| < (c/r(k))))
⊢ ∀m:{J...}. ∀n:{m...}.  (|Σ{x[i] | 0≤i≤n} - Σ{x[i] | 0≤i≤m}| ≤ (r1/r(k)))
BY
{ (RepeatFor 4 (Thin (-2)) THEN Auto THEN (RWO  "rsum-difference" 0 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))))
12. J : ℤ
13. imax(N;N1) = J ∈ ℤ
14. N ≤ J
15. N1 ≤ J
16. ∀n,m:ℕ.  ((J ≤ n) ⇒ (J ≤ m) ⇒ (|(a[n] * x[n]) - a[m] * x[m]| < (c/r(k))))
17. m : {J...}
18. n : {m...}
⊢ |Σ{x[i] | m + 1≤i≤n}| ≤ (r1/r(k))

---

Latex:

---

Latex:
.....assertion..... 
1.  a  :  \mBbbN{}  {}\mrightarrow{}  \mBbbR{}
2.  x  :  \mBbbN{}  {}\mrightarrow{}  \mBbbR{}
3.  c  :  \{c:\mBbbR{}|  r0  <  c\} 
4.  N  :  \mBbbN{}
5.  \mforall{}n:\{N...\}.  ((r0  <  a[n])  \mwedge{}  (r0  <  x[n]))
6.  \mforall{}n:\{N...\}.  ((r0  <  a[n])  \mwedge{}  (c  \mleq{}  ((a[n]  *  x[n]/x[n  +  1])  -  a[n  +  1])))
7.  k  :  \mBbbN{}\msupplus{}
8.  M  :  \mBbbN{}\msupplus{}
9.  (r1/r(M))  <  (c/r(k))
10.  N1  :  \mBbbN{}
11.  \mforall{}n:\mBbbN{}.  ((N1  \mleq{}  n)  {}\mRightarrow{}  (|(a[n]  *  x[n])  -  r0|  \mleq{}  (r1/r(2  *  M))))
12.  J  :  \mBbbZ{}
13.  imax(N;N1)  =  J
14.  N  \mleq{}  J
15.  N1  \mleq{}  J
16.  n  :  \mBbbN{}
17.  m  :  \mBbbN{}
18.  J  \mleq{}  n
19.  J  \mleq{}  m
20.  \mforall{}n,m:\mBbbN{}.    ((J  \mleq{}  n)  {}\mRightarrow{}  (J  \mleq{}  m)  {}\mRightarrow{}  (|(a[n]  *  x[n])  -  a[m]  *  x[m]|  <  (c/r(k))))
\mvdash{}  \mforall{}m:\{J...\}.  \mforall{}n:\{m...\}.    (|\mSigma{}\{x[i]  |  0\mleq{}i\mleq{}n\}  -  \mSigma{}\{x[i]  |  0\mleq{}i\mleq{}m\}|  \mleq{}  (r1/r(k)))


By

---

Latex:
(RepeatFor  4  (Thin  (-2))  THEN  Auto  THEN  (RWO    "rsum-difference"  0  THENA  Auto))

---

Home Index