---

Step * 2 3 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. lim n→∞.(|x|^n/r((n + 1)!)) = r0
11. ∀y:ℕ ⟶ ℝ
      ((∃N:ℕ. ∀n:ℕ. ∃m:ℕ. ((n ≤ m) ∧ (y[n] = (|x|^m/r((m)!)))) supposing N ≤ n)
      ⇒ lim n→∞.(|x|^n/r((n)!)) = r0
      ⇒ lim n→∞.y[n] = r0)
⊢ ∃N:ℕ. ∀n:ℕ. ∃m:ℕ. ((n ≤ m) ∧ ((x^2 * n)/(2 * n)! = (|x|^m/r((m)!)))) supposing N ≤ n
BY
{ (With ⌜0⌝ (D 0)⋅
   THEN Auto
   THEN With ⌜2 * n⌝ (D 0)⋅
   THEN Auto
   THEN RWO "int-rdiv-req" 0
   THEN Auto
   THEN nRMul ⌜r((2 * n)!)⌝ 0⋅
   THEN Auto) }

---

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.  lim  n\mrightarrow{}\minfty{}.(|x|\^{}n/r((n  +  1)!))  =  r0
11.  \mforall{}y:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}
            ((\mexists{}N:\mBbbN{}.  \mforall{}n:\mBbbN{}.  \mexists{}m:\mBbbN{}.  ((n  \mleq{}  m)  \mwedge{}  (y[n]  =  (|x|\^{}m/r((m)!))))  supposing  N  \mleq{}  n)
            {}\mRightarrow{}  lim  n\mrightarrow{}\minfty{}.(|x|\^{}n/r((n)!))  =  r0
            {}\mRightarrow{}  lim  n\mrightarrow{}\minfty{}.y[n]  =  r0)
\mvdash{}  \mexists{}N:\mBbbN{}.  \mforall{}n:\mBbbN{}.  \mexists{}m:\mBbbN{}.  ((n  \mleq{}  m)  \mwedge{}  ((x\^{}2  *  n)/(2  *  n)!  =  (|x|\^{}m/r((m)!))))  supposing  N  \mleq{}  n


By

---

Latex:
(With  \mkleeneopen{}0\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  With  \mkleeneopen{}2  *  n\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  RWO  "int-rdiv-req"  0
  THEN  Auto
  THEN  nRMul  \mkleeneopen{}r((2  *  n)!)\mkleeneclose{}  0\mcdot{}
  THEN  Auto)

---

Home Index