---

Step * 2 of Lemma ratio-test


1. x : ℕ ⟶ ℝ
2. N : ℕ
3. ∀c:{c:ℝ| (r0 ≤ c) ∧ (c < r1)} . ((∀n:{N...}. (|x[n + 1]| ≤ (c * |x[n]|))) ⇒ Σn.x[n]↓)
4. c : {c:ℝ| r1 < c} 
5. ∀n:{N...}. ((c * |x[n]|) < |x[n + 1]|)
⊢ Σn.x[n]↑
BY
{ ((Thin (-3) THEN (Assert r1 < c BY (DVar `c'⋅ THEN Unhide THEN Auto)))
   THEN (Assert r0 ≤ c BY
               (RWO "-1<" 0 THEN Auto))
   THEN RepeatFor 2 (PromoteHyp (-1) (-3)⋅)) }

1
1. x : ℕ ⟶ ℝ
2. N : ℕ
3. c : {c:ℝ| r1 < c} 
4. r1 < c
5. r0 ≤ c
6. ∀n:{N...}. ((c * |x[n]|) < |x[n + 1]|)
⊢ Σn.x[n]↑

---

Latex:

---

Latex:

1.  x  :  \mBbbN{}  {}\mrightarrow{}  \mBbbR{}
2.  N  :  \mBbbN{}
3.  \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{})
4.  c  :  \{c:\mBbbR{}|  r1  <  c\} 
5.  \mforall{}n:\{N...\}.  ((c  *  |x[n]|)  <  |x[n  +  1]|)
\mvdash{}  \mSigma{}n.x[n]\muparrow{}


By

---

Latex:
((Thin  (-3)  THEN  (Assert  r1  <  c  BY  (DVar  `c'\mcdot{}  THEN  Unhide  THEN  Auto)))
  THEN  (Assert  r0  \mleq{}  c  BY
                          (RWO  "-1<"  0  THEN  Auto))
  THEN  RepeatFor  2  (PromoteHyp  (-1)  (-3)\mcdot{}))

---

Home Index