---

Step * 1 1 1 1 1 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
⊢ ∀n,m:ℕ.  ((J ≤ n) ⇒ (J ≤ m) ⇒ (|(a[n] * x[n]) - a[m] * x[m]| < (c/r(k))))
BY
{ (RepeatFor 4 (Thin  (-1))
   THEN Auto
   THEN (Assert |(a[n] * x[n]) - r0| ≤ (r1/r(2 * M)) BY
               Auto)
   THEN (Assert |(a[m] * x[m]) - r0| ≤ (r1/r(2 * M)) BY
               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 : ℕ
17. m : ℕ
18. J ≤ n
19. J ≤ m
20. |(a[n] * x[n]) - r0| ≤ (r1/r(2 * M))
21. |(a[m] * x[m]) - r0| ≤ (r1/r(2 * M))
⊢ |(a[n] * x[n]) - a[m] * x[m]| < (c/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
\mvdash{}  \mforall{}n,m:\mBbbN{}.    ((J  \mleq{}  n)  {}\mRightarrow{}  (J  \mleq{}  m)  {}\mRightarrow{}  (|(a[n]  *  x[n])  -  a[m]  *  x[m]|  <  (c/r(k))))


By

---

Latex:
(RepeatFor  4  (Thin    (-1))
  THEN  Auto
  THEN  (Assert  |(a[n]  *  x[n])  -  r0|  \mleq{}  (r1/r(2  *  M))  BY
                          Auto)
  THEN  (Assert  |(a[m]  *  x[m])  -  r0|  \mleq{}  (r1/r(2  *  M))  BY
                          Auto))

---

Home Index