---

Step * 1 1 of Lemma Kummer-criterion


1. a : ℕ ⟶ ℝ
2. x : ℕ ⟶ ℝ
3. lim n→∞.a[n] * x[n] = r0
4. c : {c:ℝ| r0 < c} 
5. N : ℕ
6. ∀n:{N...}. ((r0 < a[n]) ∧ (r0 < x[n]))
7. ∀n:{N...}. ((r0 < a[n]) ∧ (c ≤ ((a[n] * x[n]/x[n + 1]) - a[n + 1])))
8. k : ℕ+
⊢ ∃N:ℕ [(∀n,m:ℕ.  ((N ≤ n) ⇒ (N ≤ m) ⇒ (|Σ{x[i] | 0≤i≤n} - Σ{x[i] | 0≤i≤m}| ≤ (r1/r(k)))))]
BY
{ ((InstLemma `small-reciprocal-real` [⌜(c/r(k))⌝]⋅
    THENA (Auto THEN MemTypeCD THEN Auto THEN nRMul ⌜r(k)⌝ 0⋅ THEN Auto THEN Subst' 0 * k ~ 0 0 THEN Auto)
    )
   THEN ExRepD
   ) }

1
1. a : ℕ ⟶ ℝ
2. x : ℕ ⟶ ℝ
3. lim n→∞.a[n] * x[n] = r0
4. c : {c:ℝ| r0 < c} 
5. N : ℕ
6. ∀n:{N...}. ((r0 < a[n]) ∧ (r0 < x[n]))
7. ∀n:{N...}. ((r0 < a[n]) ∧ (c ≤ ((a[n] * x[n]/x[n + 1]) - a[n + 1])))
8. k : ℕ+
9. k@0 : ℕ+
10. (r1/r(k@0)) < (c/r(k))
⊢ ∃N:ℕ [(∀n,m:ℕ.  ((N ≤ n) ⇒ (N ≤ 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.  lim  n\mrightarrow{}\minfty{}.a[n]  *  x[n]  =  r0
4.  c  :  \{c:\mBbbR{}|  r0  <  c\} 
5.  N  :  \mBbbN{}
6.  \mforall{}n:\{N...\}.  ((r0  <  a[n])  \mwedge{}  (r0  <  x[n]))
7.  \mforall{}n:\{N...\}.  ((r0  <  a[n])  \mwedge{}  (c  \mleq{}  ((a[n]  *  x[n]/x[n  +  1])  -  a[n  +  1])))
8.  k  :  \mBbbN{}\msupplus{}
\mvdash{}  \mexists{}N:\mBbbN{}  [(\mforall{}n,m:\mBbbN{}.    ((N  \mleq{}  n)  {}\mRightarrow{}  (N  \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:
((InstLemma  `small-reciprocal-real`  [\mkleeneopen{}(c/r(k))\mkleeneclose{}]\mcdot{}
    THENA  (Auto
                  THEN  MemTypeCD
                  THEN  Auto
                  THEN  nRMul  \mkleeneopen{}r(k)\mkleeneclose{}  0\mcdot{}
                  THEN  Auto
                  THEN  Subst'  0  *  k  \msim{}  0  0
                  THEN  Auto)
    )
  THEN  ExRepD
  )

---

Home Index