---

Step * 2 1 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 : ℤ
8. n ≠ 0
9. 0 < n
10. (|x[N + 1]| * c^n - 1 * c) ≤ (|x[(N + 1) + (n - 1)]| * c)
⊢ (|x[N + 1]| * if (n =z 1) then c else c^n - 1 * c fi ) ≤ |x[(N + 1) + n]|
BY
{ ((Subst ⌜(N + 1) + (n - 1) ~ N + n⌝ (-1)⋅ THENA Auto)
   THEN (InstHyp [⌜N + n⌝] (-5)⋅ THENA Auto')
   THEN (nRNorm (-1) 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 : ℤ
8. n ≠ 0
9. 0 < n
10. (|x[N + 1]| * c^n - 1 * c) ≤ (|x[N + n]| * c)
11. (|x[N + n]| * c) < |x[(N + n) + 1]|
⊢ (|x[N + 1]| * if (n =z 1) then c else c^n - 1 * c fi ) ≤ |x[(N + 1) + 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]|)
7.  n  :  \mBbbZ{}
8.  n  \mneq{}  0
9.  0  <  n
10.  (|x[N  +  1]|  *  c\^{}n  -  1  *  c)  \mleq{}  (|x[(N  +  1)  +  (n  -  1)]|  *  c)
\mvdash{}  (|x[N  +  1]|  *  if  (n  =\msubz{}  1)  then  c  else  c\^{}n  -  1  *  c  fi  )  \mleq{}  |x[(N  +  1)  +  n]|


By

---

Latex:
((Subst  \mkleeneopen{}(N  +  1)  +  (n  -  1)  \msim{}  N  +  n\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}N  +  n\mkleeneclose{}]  (-5)\mcdot{}  THENA  Auto')
  THEN  (nRNorm  (-1)  THENA  Auto'))\mcdot{}

---

Home Index