---

Step * of Lemma ratio-test-corollary

∀x:ℕ ⟶ ℝ
  ((∀n:ℕ. x[n] ≠ r0) ⇒ (∀L:ℝ. (lim n→∞.|(x[n + 1]/x[n])| = L ⇒ (((L < r1) ⇒ Σn.x[n]↓) ∧ ((r1 < L) ⇒ Σn.x[n]↑)))))
BY
{ (InstLemma `ratio-test-ext` [] THEN ParallelLast' 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. lim n→∞.|(x[n + 1]/x[n])| = L
6. L < r1
⊢ Σn.x[n]↓

2
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) ⇒ Σn.x[n]↓
7. r1 < L
⊢ Σn.x[n]↑

---

Latex:

---

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


By

---

Latex:
(InstLemma  `ratio-test-ext`  []  THEN  ParallelLast'  THEN  Auto)

---

Home Index