---

Step * 2 1 2 2 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:ℕ. (((N + 1) ≤ n) ⇒ (|x[N + 1]| ≤ |x[n]|))) ∧ (r0 < |x[N + 1]|)
⊢ Σn.x[n]↑
BY
{ ((InstLemma `series-diverges-trivially` [⌜|x[N + 1]|⌝]⋅ THENA Auto) THEN BHyp (-1) THEN 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:ℕ. (((N + 1) ≤ n) ⇒ (|x[N + 1]| ≤ |x[n]|))
9. r0 < |x[N + 1]|
10. ∀x@0:ℕ ⟶ ℝ. ((∀k:ℕ. ∃n:ℕ. ((k ≤ n) ∧ (|x[N + 1]| ≤ |x@0[n]|))) ⇒ Σn.x@0[n]↑)
11. k : ℕ
⊢ ∃n:ℕ. ((k ≤ n) ∧ (|x[N + 1]| ≤ |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]|)
7.  \mforall{}n:\mBbbN{}.  ((c\^{}n  *  |x[N  +  1]|)  \mleq{}  |x[(N  +  1)  +  n]|)
8.  (\mforall{}n:\mBbbN{}.  (((N  +  1)  \mleq{}  n)  {}\mRightarrow{}  (|x[N  +  1]|  \mleq{}  |x[n]|)))  \mwedge{}  (r0  <  |x[N  +  1]|)
\mvdash{}  \mSigma{}n.x[n]\muparrow{}


By

---

Latex:
((InstLemma  `series-diverges-trivially`  [\mkleeneopen{}|x[N  +  1]|\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  BHyp  (-1)  THEN  Auto)

---

Home Index