---

Step * 2 1 of Lemma ratio-test


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]↑
BY
{ (Assert ∀n:ℕ. ((c^n * |x[N + 1]|) ≤ |x[(N + 1) + n]|) BY
         (InductionOnNat
          THEN Reduce 0
          THEN Try ((Subst' (N + 1) + 0 ~ N + 1 0 THEN Auto THEN nRNorm 0 THEN Auto))
          THEN ((RWO "rnexp_unroll" 0 THENM AutoSplit) THENA Auto)))⋅ }

1
.....aux..... 
1. x : ℕ ⟶ ℝ
2. N : ℕ
3. c : {c:ℝ| r1 < c} 
4. r1 < c
5. r0 ≤ c
6. ∀n:{N...}. ((c * |x[n]|) < |x[n + 1]|)
7. n : ℤ
8. n ≠ 0
9. 0 < n
10. (c^n - 1 * |x[N + 1]|) ≤ |x[(N + 1) + (n - 1)]|
⊢ (|x[N + 1]| * if (n =z 1) then c else c^n - 1 * c fi ) ≤ |x[(N + 1) + n]|

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

---

Latex:

---

Latex:

1.  x  :  \mBbbN{}  {}\mrightarrow{}  \mBbbR{}
2.  N  :  \mBbbN{}
3.  c  :  \{c:\mBbbR{}|  r1  <  c\} 
4.  r1  <  c
5.  r0  \mleq{}  c
6.  \mforall{}n:\{N...\}.  ((c  *  |x[n]|)  <  |x[n  +  1]|)
\mvdash{}  \mSigma{}n.x[n]\muparrow{}


By

---

Latex:
(Assert  \mforall{}n:\mBbbN{}.  ((c\^{}n  *  |x[N  +  1]|)  \mleq{}  |x[(N  +  1)  +  n]|)  BY
              (InductionOnNat
                THEN  Reduce  0
                THEN  Try  ((Subst'  (N  +  1)  +  0  \msim{}  N  +  1  0  THEN  Auto  THEN  nRNorm  0  THEN  Auto))
                THEN  ((RWO  "rnexp\_unroll"  0  THENM  AutoSplit)  THENA  Auto)))\mcdot{}

---

Home Index