---

Step * 2 1 2 1 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]|)
7. ∀n:ℕ. ((c^n * |x[N + 1]|) ≤ |x[(N + 1) + n]|)
8. n : ℕ
9. (N + 1) ≤ n
⊢ |x[N + 1]| ≤ |x[n]|
BY
{ ((InstHyp [⌜n - N + 1⌝] (-3)⋅ THENA Auto')
   THEN Subst ⌜(N + 1) + (n - N + 1) ~ n⌝ (-1)⋅
   THEN Auto
   THEN (RWO "-1<" 0 THENA Auto))⋅ }

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]|)
7. ∀n:ℕ. ((c^n * |x[N + 1]|) ≤ |x[(N + 1) + n]|)
8. n : ℕ
9. (N + 1) ≤ n
10. (c^n - N + 1 * |x[N + 1]|) ≤ |x[n]|
⊢ |x[N + 1]| ≤ (c^n - N + 1 * |x[N + 1]|)

---

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]|)
7.  \mforall{}n:\mBbbN{}.  ((c\^{}n  *  |x[N  +  1]|)  \mleq{}  |x[(N  +  1)  +  n]|)
8.  n  :  \mBbbN{}
9.  (N  +  1)  \mleq{}  n
\mvdash{}  |x[N  +  1]|  \mleq{}  |x[n]|


By

---

Latex:
((InstHyp  [\mkleeneopen{}n  -  N  +  1\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto')
  THEN  Subst  \mkleeneopen{}(N  +  1)  +  (n  -  N  +  1)  \msim{}  n\mkleeneclose{}  (-1)\mcdot{}
  THEN  Auto
  THEN  (RWO  "-1<"  0  THENA  Auto))\mcdot{}

---

Home Index