---

Step * 1 1 2 1 1 of Lemma ratio-test-corollary


1. x : ℕ ⟶ ℝ@i
2. ∀N:ℕ
     ((∀c:{c:ℝ| (r0 ≤ c) ∧ (c < r1)} . ((∀n:{N...}. (|x[n + 1]| ≤ (c * |x[n]|))) ⇒ Σn.x[n]↓))
     ∧ (∀c:{c:ℝ| r1 < c} . ((∀n:{N...}. ((c * |x[n]|) < |x[n + 1]|)) ⇒ Σn.x[n]↑)))
3. ∀n:ℕ. x[n] ≠ r0
4. L : ℝ@i
5. lim n→∞.|(x[n + 1]/x[n])| = L
6. L < r1
7. k : ℕ+
8. ((r1/r(k)) + L) < r1
9. r0 ≤ L
10. r0 ≤ ((r1/r(k)) + L)
⊢ Σn.x[n]↓
BY
{ ((D -6 With ⌜k⌝  THENA Auto)
   THEN ExRepD
   THEN (InstHyp [⌜N⌝] 2⋅ THENA Auto)
   THEN D -1
   THEN InstHyp [⌜(r1/r(k)) + L⌝] (-2)⋅
   THEN Auto) }

1
1. x : ℕ ⟶ ℝ@i
2. ∀N:ℕ
     ((∀c:{c:ℝ| (r0 ≤ c) ∧ (c < r1)} . ((∀n:{N...}. (|x[n + 1]| ≤ (c * |x[n]|))) ⇒ Σn.x[n]↓))
     ∧ (∀c:{c:ℝ| r1 < c} . ((∀n:{N...}. ((c * |x[n]|) < |x[n + 1]|)) ⇒ Σn.x[n]↑)))
3. ∀n:ℕ. x[n] ≠ r0
4. L : ℝ@i
5. L < r1
6. k : ℕ+
7. ((r1/r(k)) + L) < r1
8. r0 ≤ L
9. r0 ≤ ((r1/r(k)) + L)
10. N : ℕ@i
11. ∀n:ℕ. ((N ≤ n) ⇒ (||(x[n + 1]/x[n])| - L| ≤ (r1/r(k))))
12. ∀c:{c:ℝ| (r0 ≤ c) ∧ (c < r1)} . ((∀n:{N...}. (|x[n + 1]| ≤ (c * |x[n]|))) ⇒ Σn.x[n]↓)
13. ∀c:{c:ℝ| r1 < c} . ((∀n:{N...}. ((c * |x[n]|) < |x[n + 1]|)) ⇒ Σn.x[n]↑)
14. n : {N...}@i
⊢ |x[n + 1]| ≤ (((r1/r(k)) + L) * |x[n]|)

---

Latex:

---

Latex:

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


By

---

Latex:
((D  -6  With  \mkleeneopen{}k\mkleeneclose{}    THENA  Auto)
  THEN  ExRepD
  THEN  (InstHyp  [\mkleeneopen{}N\mkleeneclose{}]  2\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  InstHyp  [\mkleeneopen{}(r1/r(k))  +  L\mkleeneclose{}]  (-2)\mcdot{}
  THEN  Auto)

---

Home Index