Step
*
1
1
1
1
1
2
1
1
1
1
1
1
1
1
1
1
1
1
of Lemma
Kummer-criterion
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
22. v : ℝ
23. x[k1 - 1] = v ∈ ℝ
24. v1 : ℝ
25. a[k1 - 1] = v1 ∈ ℝ
26. v2 : ℝ
27. x[k1] = v2 ∈ ℝ
28. v3 : ℝ
29. a[k1] = v3 ∈ ℝ
30. r0 < v2
31. (c * v2) ≤ ((v * v1) + -(v2 * v3))
32. v4 : ℝ
33. ((v1 * v) - v3 * v2) = v4 ∈ ℝ
⊢ ((v * v1) + -(v2 * v3)) ≤ ((v1 * v) - v3 * v2)
BY
{ (nRNorm 0 THEN Auto) }
Latex:
Latex:
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...\}
19. k1 : \mBbbZ{}
20. (m + 1) \mleq{} k1
21. k1 \mleq{} n
22. v : \mBbbR{}
23. x[k1 - 1] = v
24. v1 : \mBbbR{}
25. a[k1 - 1] = v1
26. v2 : \mBbbR{}
27. x[k1] = v2
28. v3 : \mBbbR{}
29. a[k1] = v3
30. r0 < v2
31. (c * v2) \mleq{} ((v * v1) + -(v2 * v3))
32. v4 : \mBbbR{}
33. ((v1 * v) - v3 * v2) = v4
\mvdash{} ((v * v1) + -(v2 * v3)) \mleq{} ((v1 * v) - v3 * v2)
By
Latex:
(nRNorm 0 THEN Auto)
Home
Index