---

Step * of Lemma Raabe-test

∀x:ℕ ⟶ ℝ. ∀L:ℝ.
  ((∀n:ℕ. (r0 < x[n]))
  ⇒ lim n→∞.r(n) * ((x[n]/x[n + 1]) - r1) = L
  ⇒ (((r1 < L) ⇒ Σn.x[n]↓) ∧ ((L < r1) ⇒ Σn.x[n]↑)))
BY
{ ((InstLemma `Kummer-criterion` [⌜λ2n.r(n)⌝]⋅ THENA Auto)
   THEN ParallelLast'
   THEN Auto
   THEN Try ((OrRight THEN Auto))
   THEN BackThruSomeHyp
   THEN Try (((InstLemma `small-reciprocal-real` [⌜L - r1⌝]⋅
               THENA Complete ((Auto THEN MemTypeCD THEN Auto THEN nRAdd ⌜r1⌝ 0⋅ THEN Auto))
               )
              THEN ExRepD
              THEN (Assert r0 < (L - r1 - (r1/r(k))) BY
                          (MoveToConcl (-1)
                           THEN GenConclTerms Auto [ ⌜L - r1⌝;⌜(r1/r(k))⌝]⋅
                           THEN Auto
                           THEN nRAdd ⌜v1⌝ 0⋅
                           THEN Auto))))) }

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

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

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

---

Latex:

---

Latex:
\mforall{}x:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}.  \mforall{}L:\mBbbR{}.
    ((\mforall{}n:\mBbbN{}.  (r0  <  x[n]))
    {}\mRightarrow{}  lim  n\mrightarrow{}\minfty{}.r(n)  *  ((x[n]/x[n  +  1])  -  r1)  =  L
    {}\mRightarrow{}  (((r1  <  L)  {}\mRightarrow{}  \mSigma{}n.x[n]\mdownarrow{})  \mwedge{}  ((L  <  r1)  {}\mRightarrow{}  \mSigma{}n.x[n]\muparrow{})))


By

---

Latex:
((InstLemma  `Kummer-criterion`  [\mkleeneopen{}\mlambda{}\msubtwo{}n.r(n)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ParallelLast'
  THEN  Auto
  THEN  Try  ((OrRight  THEN  Auto))
  THEN  BackThruSomeHyp
  THEN  Try  (((InstLemma  `small-reciprocal-real`  [\mkleeneopen{}L  -  r1\mkleeneclose{}]\mcdot{}
                          THENA  Complete  ((Auto  THEN  MemTypeCD  THEN  Auto  THEN  nRAdd  \mkleeneopen{}r1\mkleeneclose{}  0\mcdot{}  THEN  Auto))
                          )
                        THEN  ExRepD
                        THEN  (Assert  r0  <  (L  -  r1  -  (r1/r(k)))  BY
                                                (MoveToConcl  (-1)
                                                  THEN  GenConclTerms  Auto  [  \mkleeneopen{}L  -  r1\mkleeneclose{};\mkleeneopen{}(r1/r(k))\mkleeneclose{}]\mcdot{}
                                                  THEN  Auto
                                                  THEN  nRAdd  \mkleeneopen{}v1\mkleeneclose{}  0\mcdot{}
                                                  THEN  Auto)))))

---

Home Index