---

Step * of Lemma Kummer-criterion

∀a,x:ℕ ⟶ ℝ.
  ((lim n→∞.a[n] * x[n] = r0
  ⇒ (∃c:{c:ℝ| r0 < c} 
       ∃N:ℕ
        ((∀n:{N...}. ((r0 < a[n]) ∧ (r0 < x[n])))
        ∧ (∀n:{N...}. ((r0 < a[n]) ∧ (c ≤ ((a[n] * x[n]/x[n + 1]) - a[n + 1]))))))
  ⇒ Σn.x[n]↓)
  ∧ ((∃N:ℕ
       ((∀n:{N...}. ((r0 < a[n]) ∧ (r0 < x[n])))
       ∧ (∀n:{N...}. (((a[n] * x[n]/x[n + 1]) - a[n + 1]) ≤ r0))
       ∧ Σn.(r1/a[N + n])↑))
    ⇒ Σn.x[n]↑))
BY
{ (Auto THEN Try ((OrRight 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])))
⊢ Σn.x[n]↓

2
1. a : ℕ ⟶ ℝ
2. x : ℕ ⟶ ℝ
3. lim n→∞.a[n] * x[n] = r0
⇒ (∃c:{c:ℝ| r0 < c} 
     ∃N:ℕ
      ((∀n:{N...}. ((r0 < a[n]) ∧ (r0 < x[n])))
      ∧ (∀n:{N...}. ((r0 < a[n]) ∧ (c ≤ ((a[n] * x[n]/x[n + 1]) - a[n + 1]))))))
⇒ Σn.x[n]↓
4. N : ℕ
5. ∀n:{N...}. ((r0 < a[n]) ∧ (r0 < x[n]))
6. ∀n:{N...}. (((a[n] * x[n]/x[n + 1]) - a[n + 1]) ≤ r0)
7. Σn.(r1/a[N + n])↑
⊢ Σn.x[n]↑

---

Latex:

---

Latex:
\mforall{}a,x:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}.
    ((lim  n\mrightarrow{}\minfty{}.a[n]  *  x[n]  =  r0
    {}\mRightarrow{}  (\mexists{}c:\{c:\mBbbR{}|  r0  <  c\} 
              \mexists{}N:\mBbbN{}
                ((\mforall{}n:\{N...\}.  ((r0  <  a[n])  \mwedge{}  (r0  <  x[n])))
                \mwedge{}  (\mforall{}n:\{N...\}.  ((r0  <  a[n])  \mwedge{}  (c  \mleq{}  ((a[n]  *  x[n]/x[n  +  1])  -  a[n  +  1]))))))
    {}\mRightarrow{}  \mSigma{}n.x[n]\mdownarrow{})
    \mwedge{}  ((\mexists{}N:\mBbbN{}
              ((\mforall{}n:\{N...\}.  ((r0  <  a[n])  \mwedge{}  (r0  <  x[n])))
              \mwedge{}  (\mforall{}n:\{N...\}.  (((a[n]  *  x[n]/x[n  +  1])  -  a[n  +  1])  \mleq{}  r0))
              \mwedge{}  \mSigma{}n.(r1/a[N  +  n])\muparrow{}))
        {}\mRightarrow{}  \mSigma{}n.x[n]\muparrow{}))


By

---

Latex:
(Auto  THEN  Try  ((OrRight  THEN  Auto))  THEN  ExRepD)

---

Home Index