Step
*
1
1
1
2
1
1
1
1
2
2
1
1
1
1
1
1
2
2
1
1
1
1
1
1
1
of Lemma
fun-converges-to-cosine
1. ∀x:ℝ. Σi.-1^i * (x^2 * i)/(2 * i)! = cosine(x)
2. m : ℕ+
3. r0 ≤ (r1/r(4))
4. (r1/r(4)) < r1
5. x : {x:ℝ| |x| ≤ r(m)}
6. 1 ≤ m
7. n : ℕ
8. m ≤ n
9. r0 < r((2 * n)!)
10. r0 < r(((2 * n) + 1)!)
11. |r((2 * (n + 1))!)| = r((2 * (n + 1))!)
12. |r((2 * n)!)| = r((2 * n)!)
13. v : ℝ
14. |r((2 * (n + 1))!)| = v ∈ ℝ
15. v1 : ℝ
16. |r((2 * n)!)| = v1 ∈ ℝ
17. v = (r(((2 * n) + 2) * ((2 * n) + 1)) * v1)
18. r0 < v
19. r0 < v1
20. |x| ≤ r(n)
21. (r(4) * |x|^2 * v1) ≤ (r(4) * r(n)^2 * v1)
22. (r(4) * r(n)^2 * v1) < ((r(2) * v1) + (r(6) * r(n) * v1) + (r(4) * r(n) * r(n) * v1))
23. |x^2 * (n + 1)| = (|x|^2 * |x^2 * n|)
24. X : ℝ
25. |x^2 * n| = X ∈ ℝ
26. r0 ≤ X
⊢ ((r(2) * v1) + (r(6) * r(n) * v1) + (r(4) * r(n) * r(n) * v1)) ≤ v
BY
{ (RWO "-10" 0 THEN Auto) }
1
1. ∀x:ℝ. Σi.-1^i * (x^2 * i)/(2 * i)! = cosine(x)
2. m : ℕ+
3. r0 ≤ (r1/r(4))
4. (r1/r(4)) < r1
5. x : {x:ℝ| |x| ≤ r(m)}
6. 1 ≤ m
7. n : ℕ
8. m ≤ n
9. r0 < r((2 * n)!)
10. r0 < r(((2 * n) + 1)!)
11. |r((2 * (n + 1))!)| = r((2 * (n + 1))!)
12. |r((2 * n)!)| = r((2 * n)!)
13. v : ℝ
14. |r((2 * (n + 1))!)| = v ∈ ℝ
15. v1 : ℝ
16. |r((2 * n)!)| = v1 ∈ ℝ
17. v = (r(((2 * n) + 2) * ((2 * n) + 1)) * v1)
18. r0 < v
19. r0 < v1
20. |x| ≤ r(n)
21. (r(4) * |x|^2 * v1) ≤ (r(4) * r(n)^2 * v1)
22. (r(4) * r(n)^2 * v1) < ((r(2) * v1) + (r(6) * r(n) * v1) + (r(4) * r(n) * r(n) * v1))
23. |x^2 * (n + 1)| = (|x|^2 * |x^2 * n|)
24. X : ℝ
25. |x^2 * n| = X ∈ ℝ
26. r0 ≤ X
⊢ ((r(2) * v1) + (r(6) * r(n) * v1) + (r(4) * r(n) * r(n) * v1)) ≤ (r(((2 * n) + 2) * ((2 * n) + 1)) * v1)
Latex:
Latex:
1. \mforall{}x:\mBbbR{}. \mSigma{}i.-1\^{}i * (x\^{}2 * i)/(2 * i)! = cosine(x)
2. m : \mBbbN{}\msupplus{}
3. r0 \mleq{} (r1/r(4))
4. (r1/r(4)) < r1
5. x : \{x:\mBbbR{}| |x| \mleq{} r(m)\}
6. 1 \mleq{} m
7. n : \mBbbN{}
8. m \mleq{} n
9. r0 < r((2 * n)!)
10. r0 < r(((2 * n) + 1)!)
11. |r((2 * (n + 1))!)| = r((2 * (n + 1))!)
12. |r((2 * n)!)| = r((2 * n)!)
13. v : \mBbbR{}
14. |r((2 * (n + 1))!)| = v
15. v1 : \mBbbR{}
16. |r((2 * n)!)| = v1
17. v = (r(((2 * n) + 2) * ((2 * n) + 1)) * v1)
18. r0 < v
19. r0 < v1
20. |x| \mleq{} r(n)
21. (r(4) * |x|\^{}2 * v1) \mleq{} (r(4) * r(n)\^{}2 * v1)
22. (r(4) * r(n)\^{}2 * v1) < ((r(2) * v1) + (r(6) * r(n) * v1) + (r(4) * r(n) * r(n) * v1))
23. |x\^{}2 * (n + 1)| = (|x|\^{}2 * |x\^{}2 * n|)
24. X : \mBbbR{}
25. |x\^{}2 * n| = X
26. r0 \mleq{} X
\mvdash{} ((r(2) * v1) + (r(6) * r(n) * v1) + (r(4) * r(n) * r(n) * v1)) \mleq{} v
By
Latex:
(RWO "-10" 0 THEN Auto)
Home
Index