---

Step * 2 2 1 1 1 1 1 1 1 of Lemma cosine-poly-approx-1


1. x : {x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} 
2. k : ℕ
3. e : {e:ℝ| r0 < e} 
4. k1 : ℕ+
5. (r1/r(k1)) < e
6. N : ℕ
7. ∀i:ℕ. ((N ≤ i) ⇒ (|Σ{-1^i * (x^2 * i)/(2 * i)! | 0≤i≤i} - cosine(x)| ≤ (r1/r(k1))))
8. |cosine(x) - Σ{-1^i * (x^2 * i)/(2 * i)! | 0≤i≤N}| ≤ (r1/r(k1))
9. ¬(N ≤ k)
10. n : ℕ
11. 0 ≤ n
12. r0 ≤ (x^2 * n)/(2 * n)!
13. M : ℕ+
14. (2 * n)! = M ∈ ℕ+
15. A : ℕ+
16. ((2 * n) + 2) = A ∈ ℕ+
17. B : ℕ+
18. ((2 * n) + 1) = B ∈ ℕ+
19. i : ℕ
20. (2 * n) = i ∈ ℕ
21. C : ℕ+
22. (A * B) = C ∈ ℕ+
23. v : ℝ
24. x^i = v ∈ ℝ
⊢ (x^2 * v/r(C)) ≤ v
BY
{ (Assert r0 ≤ v BY
         (RWO "-1<" 0 THEN EAuto 1)) }

1
1. x : {x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} 
2. k : ℕ
3. e : {e:ℝ| r0 < e} 
4. k1 : ℕ+
5. (r1/r(k1)) < e
6. N : ℕ
7. ∀i:ℕ. ((N ≤ i) ⇒ (|Σ{-1^i * (x^2 * i)/(2 * i)! | 0≤i≤i} - cosine(x)| ≤ (r1/r(k1))))
8. |cosine(x) - Σ{-1^i * (x^2 * i)/(2 * i)! | 0≤i≤N}| ≤ (r1/r(k1))
9. ¬(N ≤ k)
10. n : ℕ
11. 0 ≤ n
12. r0 ≤ (x^2 * n)/(2 * n)!
13. M : ℕ+
14. (2 * n)! = M ∈ ℕ+
15. A : ℕ+
16. ((2 * n) + 2) = A ∈ ℕ+
17. B : ℕ+
18. ((2 * n) + 1) = B ∈ ℕ+
19. i : ℕ
20. (2 * n) = i ∈ ℕ
21. C : ℕ+
22. (A * B) = C ∈ ℕ+
23. v : ℝ
24. x^i = v ∈ ℝ
25. r0 ≤ v
⊢ (x^2 * v/r(C)) ≤ v

---

Latex:

---

Latex:

1.  x  :  \{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\} 
2.  k  :  \mBbbN{}
3.  e  :  \{e:\mBbbR{}|  r0  <  e\} 
4.  k1  :  \mBbbN{}\msupplus{}
5.  (r1/r(k1))  <  e
6.  N  :  \mBbbN{}
7.  \mforall{}i:\mBbbN{}.  ((N  \mleq{}  i)  {}\mRightarrow{}  (|\mSigma{}\{-1\^{}i  *  (x\^{}2  *  i)/(2  *  i)!  |  0\mleq{}i\mleq{}i\}  -  cosine(x)|  \mleq{}  (r1/r(k1))))
8.  |cosine(x)  -  \mSigma{}\{-1\^{}i  *  (x\^{}2  *  i)/(2  *  i)!  |  0\mleq{}i\mleq{}N\}|  \mleq{}  (r1/r(k1))
9.  \mneg{}(N  \mleq{}  k)
10.  n  :  \mBbbN{}
11.  0  \mleq{}  n
12.  r0  \mleq{}  (x\^{}2  *  n)/(2  *  n)!
13.  M  :  \mBbbN{}\msupplus{}
14.  (2  *  n)!  =  M
15.  A  :  \mBbbN{}\msupplus{}
16.  ((2  *  n)  +  2)  =  A
17.  B  :  \mBbbN{}\msupplus{}
18.  ((2  *  n)  +  1)  =  B
19.  i  :  \mBbbN{}
20.  (2  *  n)  =  i
21.  C  :  \mBbbN{}\msupplus{}
22.  (A  *  B)  =  C
23.  v  :  \mBbbR{}
24.  x\^{}i  =  v
\mvdash{}  (x\^{}2  *  v/r(C))  \mleq{}  v


By

---

Latex:
(Assert  r0  \mleq{}  v  BY
              (RWO  "-1<"  0  THEN  EAuto  1))

---

Home Index