---

Step * 3 1 of Lemma Raabe-test


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
9. k : ℕ+
10. (r1/r(k)) < (r1 - L)
⊢ ∃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))↑)
BY
{ ((D -5 With ⌜k⌝  THENA Auto)
   THEN D -1
   THEN InstConcl [⌜N + 1⌝]⋅
   THEN Auto
   THEN Try ((Assert r0 < x[n + 1] BY Auto))
   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. (r1 < L) ⇒ Σn.x[n]↓
7. L < r1
8. k : ℕ+
9. (r1/r(k)) < (r1 - L)
10. N : ℕ
11. ∀n:ℕ. ((N ≤ n) ⇒ (|(r(n) * ((x[n]/x[n + 1]) - r1)) - L| ≤ (r1/r(k))))
12. ∀n:{N + 1...}. ((r0 < r(n)) ∧ (r0 < x[n]))
13. n : {N + 1...}
14. r0 < x[n + 1]
⊢ ((r(n) * x[n]/x[n + 1]) - r(n + 1)) ≤ 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. (r1 < L) ⇒ Σn.x[n]↓
7. L < r1
8. k : ℕ+
9. (r1/r(k)) < (r1 - L)
10. N : ℕ
11. [%13] : ∀n:ℕ. ((N ≤ n) ⇒ (|(r(n) * ((x[n]/x[n + 1]) - r1)) - L| ≤ (r1/r(k))))
12. ∀n:{N + 1...}. ((r0 < r(n)) ∧ (r0 < x[n]))
13. ∀n:{N + 1...}. (((r(n) * x[n]/x[n + 1]) - r(n + 1)) ≤ r0)
⊢ Σn.(r1/r((N + 1) + n))↑

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. (r1 < L) ⇒ Σn.x[n]↓
7. L < r1
8. k : ℕ+
9. (r1/r(k)) < (r1 - L)
10. N : ℕ
11. ∀n:ℕ. ((N ≤ n) ⇒ (|(r(n) * ((x[n]/x[n + 1]) - r1)) - L| ≤ (r1/r(k))))
12. N1 : ℕ
13. x1 : ∀n:{N1...}. ((r0 < r(n)) ∧ (r0 < x[n]))
14. x2 : ∀n:{N1...}. (((r(n) * x[n]/x[n + 1]) - r(n + 1)) ≤ r0)
15. n : ℕ
16. r0 < x[n + 1]
⊢ ¬((N1 + n) = 0 ∈ ℤ)

---

Latex:

---

Latex:

1.  x  :  \mBbbN{}  {}\mrightarrow{}  \mBbbR{}
2.  lim  n\mrightarrow{}\minfty{}.r(n)  *  x[n]  =  r0
{}\mRightarrow{}  (\mexists{}c:\{c:\mBbbR{}|  r0  <  c\} 
          \mexists{}N:\mBbbN{}
            ((\mforall{}n:\{N...\}.  ((r0  <  r(n))  \mwedge{}  (r0  <  x[n])))
            \mwedge{}  (\mforall{}n:\{N...\}.  ((r0  <  r(n))  \mwedge{}  (c  \mleq{}  ((r(n)  *  x[n]/x[n  +  1])  -  r(n  +  1)))))))
{}\mRightarrow{}  \mSigma{}n.x[n]\mdownarrow{}
3.  (\mexists{}N:\mBbbN{}
          ((\mforall{}n:\{N...\}.  ((r0  <  r(n))  \mwedge{}  (r0  <  x[n])))
          \mwedge{}  (\mforall{}n:\{N...\}.  (((r(n)  *  x[n]/x[n  +  1])  -  r(n  +  1))  \mleq{}  r0))
          \mwedge{}  \mSigma{}n.(r1/r(N  +  n))\muparrow{}))
{}\mRightarrow{}  \mSigma{}n.x[n]\muparrow{}
4.  L  :  \mBbbR{}
5.  \mforall{}n:\mBbbN{}.  (r0  <  x[n])
6.  lim  n\mrightarrow{}\minfty{}.r(n)  *  ((x[n]/x[n  +  1])  -  r1)  =  L
7.  (r1  <  L)  {}\mRightarrow{}  \mSigma{}n.x[n]\mdownarrow{}
8.  L  <  r1
9.  k  :  \mBbbN{}\msupplus{}
10.  (r1/r(k))  <  (r1  -  L)
\mvdash{}  \mexists{}N:\mBbbN{}
      ((\mforall{}n:\{N...\}.  ((r0  <  r(n))  \mwedge{}  (r0  <  x[n])))
      \mwedge{}  (\mforall{}n:\{N...\}.  (((r(n)  *  x[n]/x[n  +  1])  -  r(n  +  1))  \mleq{}  r0))
      \mwedge{}  \mSigma{}n.(r1/r(N  +  n))\muparrow{})


By

---

Latex:
((D  -5  With  \mkleeneopen{}k\mkleeneclose{}    THENA  Auto)
  THEN  D  -1
  THEN  InstConcl  [\mkleeneopen{}N  +  1\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  Try  ((Assert  r0  <  x[n  +  1]  BY  Auto))
  THEN  Auto)

---

Home Index