---

Step * of Lemma cosine-approx-property

∀[x:ℝ]. ∀[k:ℕ]. ∀[N:ℕ+].  ((|x| ≤ (r1/r(2))) ⇒ 1-approx(Σ{-1^i * (x^2 * i)/(2 * i)! | 0≤i≤k};N;cosine-approx(x;k;N)))
BY
{ (Auto
   THEN (Assert |x^2| ≤ (r1/r(4)) BY
               ((RWO "rabs-rnexp" 0 THENA Auto)
                THEN (Assert (r1/r(4)) = (r1/r(2))^2 BY
                            ((RWO  "rnexp-rdiv<" 0 THENA Auto) THEN RepeatFor 2 ((RWO  "rnexp-int" 0 THEN Auto))))
                THEN RWO  "-1" 0
                THEN Auto))
   THEN (InstLemma `poly-approx-property` 
         [⌜k⌝;⌜λi.(r(if (i rem 2 =z 0) then 1 else -1 fi ))/(2 * i)!⌝;⌜x^2⌝;⌜N⌝]⋅
         THENA Auto
         )
   THEN Reduce -1
   THEN (Assert Σ{(r(if (i rem 2 =z 0) then 1 else -1 fi ))/(2 * i)! * x^2^i | 0≤i≤k}
               = Σ{-1^i * (x^2 * i)/(2 * i)! | 0≤i≤k} BY
               ((BLemma `rsum_functionality` THENM D 0)
                THEN Auto
                THEN (GenConcl ⌜(2 * i)! = M ∈ ℕ+⌝⋅ THENA Auto)
                THEN (Subst' if (i rem 2 =z 0) then 1 else -1 fi  ~ (-1)^i 0 THENA Auto)
                THEN (RWW "int-rdiv-req int-rmul-req" 0 THENM nRMul ⌜r(M)⌝ 0⋅)
                THEN Auto
                THEN RWO "rnexp-mul" 0
                THEN Auto
                THEN RWO "exp-fastexp" 0
                THEN Auto))
   THEN Fold `cosine-approx` (-2)
   THEN RWO  "-1" (-2)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[x:\mBbbR{}].  \mforall{}[k:\mBbbN{}].  \mforall{}[N:\mBbbN{}\msupplus{}].
    ((|x|  \mleq{}  (r1/r(2)))  {}\mRightarrow{}  1-approx(\mSigma{}\{-1\^{}i  *  (x\^{}2  *  i)/(2  *  i)!  |  0\mleq{}i\mleq{}k\};N;cosine-approx(x;k;N)))


By

---

Latex:
(Auto
  THEN  (Assert  |x\^{}2|  \mleq{}  (r1/r(4))  BY
                          ((RWO  "rabs-rnexp"  0  THENA  Auto)
                            THEN  (Assert  (r1/r(4))  =  (r1/r(2))\^{}2  BY
                                                    ((RWO    "rnexp-rdiv<"  0  THENA  Auto)
                                                      THEN  RepeatFor  2  ((RWO    "rnexp-int"  0  THEN  Auto))
                                                      ))
                            THEN  RWO    "-1"  0
                            THEN  Auto))
  THEN  (InstLemma  `poly-approx-property` 
              [\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}\mlambda{}i.(r(if  (i  rem  2  =\msubz{}  0)  then  1  else  -1  fi  ))/(2  *  i)!\mkleeneclose{};\mkleeneopen{}x\^{}2\mkleeneclose{};\mkleeneopen{}N\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  Reduce  -1
  THEN  (Assert  \mSigma{}\{(r(if  (i  rem  2  =\msubz{}  0)  then  1  else  -1  fi  ))/(2  *  i)!  *  x\^{}2\^{}i  |  0\mleq{}i\mleq{}k\}
                          =  \mSigma{}\{-1\^{}i  *  (x\^{}2  *  i)/(2  *  i)!  |  0\mleq{}i\mleq{}k\}  BY
                          ((BLemma  `rsum\_functionality`  THENM  D  0)
                            THEN  Auto
                            THEN  (GenConcl  \mkleeneopen{}(2  *  i)!  =  M\mkleeneclose{}\mcdot{}  THENA  Auto)
                            THEN  (Subst'  if  (i  rem  2  =\msubz{}  0)  then  1  else  -1  fi    \msim{}  (-1)\^{}i  0  THENA  Auto)
                            THEN  (RWW  "int-rdiv-req  int-rmul-req"  0  THENM  nRMul  \mkleeneopen{}r(M)\mkleeneclose{}  0\mcdot{})
                            THEN  Auto
                            THEN  RWO  "rnexp-mul"  0
                            THEN  Auto
                            THEN  RWO  "exp-fastexp"  0
                            THEN  Auto))
  THEN  Fold  `cosine-approx`  (-2)
  THEN  RWO    "-1"  (-2)
  THEN  Auto)

---

Home Index