---

Step * 2 1 1 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. (L < r1) ⇒ Σn.x[n]↓
6. r1 < L
7. k : ℕ+
8. (r1/r(k)) < (L - r1)
9. r1 < (L - (r1/r(k)))
10. N : ℕ@i
11. ∀n:ℕ. ((N ≤ n) ⇒ (||(x[n + 1]/x[n])| - L| ≤ (r1/r(k + 1))))
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
15. ((L - (r1/r(k + 1))) ≤ (|x[n + 1]|/|x[n]|)) ∧ ((|x[n + 1]|/|x[n]|) ≤ (L + (r1/r(k + 1))))
16. r0 < |x[n]|
⊢ ((L - (r1/r(k))) * |x[n]|) < |x[n + 1]|
BY
{ (D -2
   THEN MoveToConcl (-3)
   THEN MoveToConcl (-1)
   THEN (GenConclTerm ⌜|x[n]|⌝⋅ THENA Auto)
   THEN (Assert ⌜(r1/r(k + 1)) < (r1/r(k))⌝⋅ THENA Auto)
   THEN MoveToConcl (-1)
   THEN GenConclTerms Auto [⌜(r1/r(k))⌝;⌜(r1/r(k + 1))⌝;⌜|x[n + 1]|⌝]⋅
   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) ⇒ Σn.x[n]↓
6. r1 < L
7. k : ℕ+
8. (r1/r(k)) < (L - r1)
9. r1 < (L - (r1/r(k)))
10. N : ℕ@i
11. ∀n:ℕ. ((N ≤ n) ⇒ (||(x[n + 1]/x[n])| - L| ≤ (r1/r(k + 1))))
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
15. (|x[n + 1]|/|x[n]|) ≤ (L + (r1/r(k + 1)))
16. v : ℝ@i
17. |x[n]| = v ∈ ℝ
18. v1 : ℝ@i
19. (r1/r(k)) = v1 ∈ ℝ
20. v2 : ℝ@i
21. (r1/r(k + 1)) = v2 ∈ ℝ
22. v3 : ℝ@i
23. |x[n + 1]| = v3 ∈ ℝ
24. v2 < v1
25. r0 < v
26. (L - v2) ≤ (v3/v)
⊢ ((L - v1) * v) < v3

---

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.  (L  <  r1)  {}\mRightarrow{}  \mSigma{}n.x[n]\mdownarrow{}
6.  r1  <  L
7.  k  :  \mBbbN{}\msupplus{}
8.  (r1/r(k))  <  (L  -  r1)
9.  r1  <  (L  -  (r1/r(k)))
10.  N  :  \mBbbN{}@i
11.  \mforall{}n:\mBbbN{}.  ((N  \mleq{}  n)  {}\mRightarrow{}  (||(x[n  +  1]/x[n])|  -  L|  \mleq{}  (r1/r(k  +  1))))
12.  \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{})
13.  \mforall{}c:\{c:\mBbbR{}|  r1  <  c\}  .  ((\mforall{}n:\{N...\}.  ((c  *  |x[n]|)  <  |x[n  +  1]|))  {}\mRightarrow{}  \mSigma{}n.x[n]\muparrow{})
14.  n  :  \{N...\}@i
15.  ((L  -  (r1/r(k  +  1)))  \mleq{}  (|x[n  +  1]|/|x[n]|))  \mwedge{}  ((|x[n  +  1]|/|x[n]|)  \mleq{}  (L  +  (r1/r(k  +  1))))
16.  r0  <  |x[n]|
\mvdash{}  ((L  -  (r1/r(k)))  *  |x[n]|)  <  |x[n  +  1]|


By

---

Latex:
(D  -2
  THEN  MoveToConcl  (-3)
  THEN  MoveToConcl  (-1)
  THEN  (GenConclTerm  \mkleeneopen{}|x[n]|\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}(r1/r(k  +  1))  <  (r1/r(k))\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  GenConclTerms  Auto  [\mkleeneopen{}(r1/r(k))\mkleeneclose{};\mkleeneopen{}(r1/r(k  +  1))\mkleeneclose{};\mkleeneopen{}|x[n  +  1]|\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index