Step
*
1
2
1
1
1
1
1
1
2
of Lemma
Raabe-lemma
1. y : ℕ ⟶ ℝ
2. c : ℝ
3. r0 < c
4. N : ℕ+
5. ∀n:{N...}. (r0 < y[n])
6. ∀n:{N...}. (c ≤ (r(n) * ((y[n]/y[n + 1]) - r1)))
7. k : ℕ+
8. ∀n:{N...}. y[n] ≠ r0
9. ∀d:ℕ. ((r1 + (c * Σ{(r1/r(k)) | N≤k≤N + (d - 1)})) ≤ (y[N]/y[N + d]))
10. ∀n:ℕ. ((r1 + (r(n)/r(2))) ≤ Σ{(r1/r(i)) | 1≤i≤2^n})
11. n : ℕ
12. r(-n) ≤ (r(2) * (((y[N] * r(k)/c) + Σ{(r1/r(i)) | 1≤i≤N - 1}) - r1))
13. (r(2) * (((y[N] * r(k)/c) + Σ{(r1/r(i)) | 1≤i≤N - 1}) - r1)) ≤ r(n)
14. (r1 + (r(n)/r(2))) ≤ Σ{(r1/r(i)) | 1≤i≤2^n}
15. (N - 1) ≤ 2^n
16. ¬(N = 1 ∈ ℤ)
⊢ (y[N] * r(k)/c) ≤ Σ{(r1/r(k)) | N≤k≤2^n}
BY
{ (InstLemma `rsum-split` [⌜1⌝;⌜2^n⌝;⌜λ2i.(r1/r(i))⌝;⌜N - 1⌝]⋅ THENA Auto) }
1
1. y : ℕ ⟶ ℝ
2. c : ℝ
3. r0 < c
4. N : ℕ+
5. ∀n:{N...}. (r0 < y[n])
6. ∀n:{N...}. (c ≤ (r(n) * ((y[n]/y[n + 1]) - r1)))
7. k : ℕ+
8. ∀n:{N...}. y[n] ≠ r0
9. ∀d:ℕ. ((r1 + (c * Σ{(r1/r(k)) | N≤k≤N + (d - 1)})) ≤ (y[N]/y[N + d]))
10. ∀n:ℕ. ((r1 + (r(n)/r(2))) ≤ Σ{(r1/r(i)) | 1≤i≤2^n})
11. n : ℕ
12. r(-n) ≤ (r(2) * (((y[N] * r(k)/c) + Σ{(r1/r(i)) | 1≤i≤N - 1}) - r1))
13. (r(2) * (((y[N] * r(k)/c) + Σ{(r1/r(i)) | 1≤i≤N - 1}) - r1)) ≤ r(n)
14. (r1 + (r(n)/r(2))) ≤ Σ{(r1/r(i)) | 1≤i≤2^n}
15. (N - 1) ≤ 2^n
16. ¬(N = 1 ∈ ℤ)
17. Σ{(r1/r(i)) | 1≤i≤2^n} = (Σ{(r1/r(i)) | 1≤i≤N - 1} + Σ{(r1/r(i)) | (N - 1) + 1≤i≤2^n})
⊢ (y[N] * r(k)/c) ≤ Σ{(r1/r(k)) | N≤k≤2^n}
Latex:
Latex:
1. y : \mBbbN{} {}\mrightarrow{} \mBbbR{}
2. c : \mBbbR{}
3. r0 < c
4. N : \mBbbN{}\msupplus{}
5. \mforall{}n:\{N...\}. (r0 < y[n])
6. \mforall{}n:\{N...\}. (c \mleq{} (r(n) * ((y[n]/y[n + 1]) - r1)))
7. k : \mBbbN{}\msupplus{}
8. \mforall{}n:\{N...\}. y[n] \mneq{} r0
9. \mforall{}d:\mBbbN{}. ((r1 + (c * \mSigma{}\{(r1/r(k)) | N\mleq{}k\mleq{}N + (d - 1)\})) \mleq{} (y[N]/y[N + d]))
10. \mforall{}n:\mBbbN{}. ((r1 + (r(n)/r(2))) \mleq{} \mSigma{}\{(r1/r(i)) | 1\mleq{}i\mleq{}2\^{}n\})
11. n : \mBbbN{}
12. r(-n) \mleq{} (r(2) * (((y[N] * r(k)/c) + \mSigma{}\{(r1/r(i)) | 1\mleq{}i\mleq{}N - 1\}) - r1))
13. (r(2) * (((y[N] * r(k)/c) + \mSigma{}\{(r1/r(i)) | 1\mleq{}i\mleq{}N - 1\}) - r1)) \mleq{} r(n)
14. (r1 + (r(n)/r(2))) \mleq{} \mSigma{}\{(r1/r(i)) | 1\mleq{}i\mleq{}2\^{}n\}
15. (N - 1) \mleq{} 2\^{}n
16. \mneg{}(N = 1)
\mvdash{} (y[N] * r(k)/c) \mleq{} \mSigma{}\{(r1/r(k)) | N\mleq{}k\mleq{}2\^{}n\}
By
Latex:
(InstLemma `rsum-split` [\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}2\^{}n\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}i.(r1/r(i))\mkleeneclose{};\mkleeneopen{}N - 1\mkleeneclose{}]\mcdot{} THENA Auto)
Home
Index