---

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

.....antecedent..... 
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[k] ≤ (r1/c) * ((a[k - 1] * x[k - 1]) - a[k] * x[k]) for k ∈ [m + 1,n]
BY
{ (D 0 THEN 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...}
19. k1 : ℤ
20. (m + 1) ≤ k1
21. k1 ≤ n
⊢ x[k1] ≤ ((r1/c) * ((a[k1 - 1] * x[k1 - 1]) - a[k1] * x[k1]))

---

Latex:

---

Latex:
.....antecedent..... 
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.  \mforall{}n,m:\mBbbN{}.    ((J  \mleq{}  n)  {}\mRightarrow{}  (J  \mleq{}  m)  {}\mRightarrow{}  (|(a[n]  *  x[n])  -  a[m]  *  x[m]|  <  (c/r(k))))
17.  m  :  \{J...\}
18.  n  :  \{m...\}
\mvdash{}  x[k]  \mleq{}  (r1/c)  *  ((a[k  -  1]  *  x[k  -  1])  -  a[k]  *  x[k])  for  k  \mmember{}  [m  +  1,n]


By

---

Latex:
(D  0  THEN  Auto)

---

Home Index