---

Step * 1 of Lemma sine-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) + 1)/((2 * i) + 1)! | 0≤i≤i} - sine(x)| ≤ (r1/r(k1))))
8. |Σ{-1^i * (x^(2 * i) + 1)/((2 * i) + 1)! | 0≤i≤N} - sine(x)| ≤ (r1/r(k1))
9. N ≤ k
10. |Σ{-1^i * (x^(2 * i) + 1)/((2 * i) + 1)! | 0≤i≤k} - sine(x)| ≤ (r1/r(k1))
⊢ (r1/r(k1)) ≤ ((x^(2 * k) + 3/r(((2 * k) + 3)!)) + e)
BY
{ (Assert r0 ≤ (x^(2 * k) + 3/r(((2 * k) + 3)!)) BY
         (nRMul ⌜r(((2 * k) + 3)!)⌝ 0⋅ THEN Auto)) }

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) + 1)/((2 * i) + 1)! | 0≤i≤i} - sine(x)| ≤ (r1/r(k1))))
8. |Σ{-1^i * (x^(2 * i) + 1)/((2 * i) + 1)! | 0≤i≤N} - sine(x)| ≤ (r1/r(k1))
9. N ≤ k
10. |Σ{-1^i * (x^(2 * i) + 1)/((2 * i) + 1)! | 0≤i≤k} - sine(x)| ≤ (r1/r(k1))
11. r0 ≤ (x^(2 * k) + 3/r(((2 * k) + 3)!))
⊢ (r1/r(k1)) ≤ ((x^(2 * k) + 3/r(((2 * k) + 3)!)) + e)

---

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)  +  1)/((2  *  i)  +  1)!  |  0\mleq{}i\mleq{}i\}  -  sine(x)|  \mleq{}  (r1/r(k1))))
8.  |\mSigma{}\{-1\^{}i  *  (x\^{}(2  *  i)  +  1)/((2  *  i)  +  1)!  |  0\mleq{}i\mleq{}N\}  -  sine(x)|  \mleq{}  (r1/r(k1))
9.  N  \mleq{}  k
10.  |\mSigma{}\{-1\^{}i  *  (x\^{}(2  *  i)  +  1)/((2  *  i)  +  1)!  |  0\mleq{}i\mleq{}k\}  -  sine(x)|  \mleq{}  (r1/r(k1))
\mvdash{}  (r1/r(k1))  \mleq{}  ((x\^{}(2  *  k)  +  3/r(((2  *  k)  +  3)!))  +  e)


By

---

Latex:
(Assert  r0  \mleq{}  (x\^{}(2  *  k)  +  3/r(((2  *  k)  +  3)!))  BY
              (nRMul  \mkleeneopen{}r(((2  *  k)  +  3)!)\mkleeneclose{}  0\mcdot{}  THEN  Auto))

---

Home Index