Step
*
1
1
of Lemma
fun-ratio-test
.....aux.....
1. c : ℝ
2. r0 ≤ c
3. c < r1
4. N : ℕ
5. I : Interval
6. g : ℕ ⟶ I ⟶ℝ
7. ∀n:ℕ. g[n;x] continuous for x ∈ I
8. icompact(I)
9. ∀n:{N...}. ∀x:{x:ℝ| x ∈ I} . (|g[n + 1;x]| ≤ (c * |g[n;x]|))
10. n : ℤ
⊢ ∀x:{x:ℝ| x ∈ I} . (|g[N + 0;x]| ≤ (c^0 * |g[N;x]|))
BY
{ (Reduce 0 THEN Auto)⋅ }
1
1. c : ℝ
2. r0 ≤ c
3. c < r1
4. N : ℕ
5. I : Interval
6. g : ℕ ⟶ I ⟶ℝ
7. ∀n:ℕ. g[n;x] continuous for x ∈ I
8. icompact(I)
9. ∀n:{N...}. ∀x:{x:ℝ| x ∈ I} . (|g[n + 1;x]| ≤ (c * |g[n;x]|))
10. n : ℤ
11. x : {x:ℝ| x ∈ I}
⊢ |g[N + 0;x]| ≤ (r1 * |g[N;x]|)
Latex:
Latex:
.....aux.....
1. c : \mBbbR{}
2. r0 \mleq{} c
3. c < r1
4. N : \mBbbN{}
5. I : Interval
6. g : \mBbbN{} {}\mrightarrow{} I {}\mrightarrow{}\mBbbR{}
7. \mforall{}n:\mBbbN{}. g[n;x] continuous for x \mmember{} I
8. icompact(I)
9. \mforall{}n:\{N...\}. \mforall{}x:\{x:\mBbbR{}| x \mmember{} I\} . (|g[n + 1;x]| \mleq{} (c * |g[n;x]|))
10. n : \mBbbZ{}
\mvdash{} \mforall{}x:\{x:\mBbbR{}| x \mmember{} I\} . (|g[N + 0;x]| \mleq{} (c\^{}0 * |g[N;x]|))
By
Latex:
(Reduce 0 THEN Auto)\mcdot{}
Home
Index