---

Step * 1 1 1 1 1 2 1 1 2 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. Σ{x[k] | m + 1≤k≤n} ≤ Σ{(r1/c) * ((a[k - 1] * x[k - 1]) - a[k] * x[k]) | m + 1≤k≤n}
⊢ |Σ{x[i] | m + 1≤i≤n}| ≤ (r1/r(k))
BY
{ (RWO  "rabs-of-nonneg" 0
   THENA (Auto THEN (BLemma `rsum_nonneg` THEN Auto) THEN D 0 THEN Auto THEN (Assert r0 < x[i] BY Auto) 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. Σ{x[k] | m + 1≤k≤n} ≤ Σ{(r1/c) * ((a[k - 1] * x[k - 1]) - a[k] * x[k]) | m + 1≤k≤n}
⊢ Σ{x[i] | m + 1≤i≤n} ≤ (r1/r(k))

---

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.  \mSigma{}\{x[k]  |  m  +  1\mleq{}k\mleq{}n\}  \mleq{}  \mSigma{}\{(r1/c)  *  ((a[k  -  1]  *  x[k  -  1])  -  a[k]  *  x[k])  |  m  +  1\mleq{}k\mleq{}n\}
\mvdash{}  |\mSigma{}\{x[i]  |  m  +  1\mleq{}i\mleq{}n\}|  \mleq{}  (r1/r(k))


By

---

Latex:
(RWO    "rabs-of-nonneg"  0
  THENA  (Auto
                THEN  (BLemma  `rsum\_nonneg`  THEN  Auto)
                THEN  D  0
                THEN  Auto
                THEN  (Assert  r0  <  x[i]  BY
                                        Auto)
                THEN  Auto)
  )

---

Home Index