---

Step * 1 3 2 of Lemma ratio-test


1. x : ℕ ⟶ ℝ
2. N : ℕ
3. c : {c:ℝ| (r0 ≤ c) ∧ (c < r1)} 
4. ∀n:{N...}. (|x[n + 1]| ≤ (c * |x[n]|))
5. ∀n:ℕ. (|x[N + n]| ≤ (c^n * |x[N]|))
6. n : ℕ
⊢ |x[n]| ≤ if N ≤z n then c^n - N * |x[N]| else |x[n]| fi 
BY
{ (AutoSplit⋅ THEN RWO "-3<" 0 THEN Auto' THEN Subst ⌜N + (n - N) ~ n⌝ 0⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  x  :  \mBbbN{}  {}\mrightarrow{}  \mBbbR{}
2.  N  :  \mBbbN{}
3.  c  :  \{c:\mBbbR{}|  (r0  \mleq{}  c)  \mwedge{}  (c  <  r1)\} 
4.  \mforall{}n:\{N...\}.  (|x[n  +  1]|  \mleq{}  (c  *  |x[n]|))
5.  \mforall{}n:\mBbbN{}.  (|x[N  +  n]|  \mleq{}  (c\^{}n  *  |x[N]|))
6.  n  :  \mBbbN{}
\mvdash{}  |x[n]|  \mleq{}  if  N  \mleq{}z  n  then  c\^{}n  -  N  *  |x[N]|  else  |x[n]|  fi 


By

---

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

---

Home Index