---

Step * 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))))
⊢ ∀n,m:ℕ.  ((imax(N;N1) ≤ n) ⇒ (imax(N;N1) ≤ m) ⇒ (|Σ{x[i] | 0≤i≤n} - Σ{x[i] | 0≤i≤m}| ≤ (r1/r(k))))
BY
{ ((Assert (N ≤ imax(N;N1)) ∧ (N1 ≤ imax(N;N1)) BY
          Auto)
   THEN MoveToConcl (-1)
   THEN GenConcl ⌜imax(N;N1) = J ∈ ℤ⌝⋅
   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 : ℕ
17. m : ℕ
18. J ≤ n
19. J ≤ m
⊢ |Σ{x[i] | 0≤i≤n} - Σ{x[i] | 0≤i≤m}| ≤ (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))))
\mvdash{}  \mforall{}n,m:\mBbbN{}.
        ((imax(N;N1)  \mleq{}  n)  {}\mRightarrow{}  (imax(N;N1)  \mleq{}  m)  {}\mRightarrow{}  (|\mSigma{}\{x[i]  |  0\mleq{}i\mleq{}n\}  -  \mSigma{}\{x[i]  |  0\mleq{}i\mleq{}m\}|  \mleq{}  (r1/r(k))))


By

---

Latex:
((Assert  (N  \mleq{}  imax(N;N1))  \mwedge{}  (N1  \mleq{}  imax(N;N1))  BY
                Auto)
  THEN  MoveToConcl  (-1)
  THEN  GenConcl  \mkleeneopen{}imax(N;N1)  =  J\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index