---

Step * of Lemma sine-approx-property

∀[x:ℝ]. ∀[k:ℕ]. ∀[N:ℕ+].
  ((|x| ≤ (r1/r(2))) ⇒ 1-approx(Σ{-1^i * (x^(2 * i) + 1)/((2 * i) + 1)! | 0≤i≤k};N;sine-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) + 1)!⌝;⌜x^2⌝;⌜2 * N⌝]⋅
         THENA Auto
         )
   THEN Reduce -1
   THEN (Assert Σ{(r(if (i rem 2 =z 0) then 1 else -1 fi ))/((2 * i) + 1)! * x^2^i | 0≤i≤k}
               = Σ{-1^i * (x^2 * i)/((2 * i) + 1)! | 0≤i≤k} BY
               ((BLemma `rsum_functionality` THENM D 0)
                THEN Auto
                THEN (GenConcl ⌜((2 * i) + 1)! = 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))) }

1
1. x : ℝ
2. k : ℕ
3. N : ℕ+
4. |x| ≤ (r1/r(2))
5. |x^2| ≤ (r1/r(4))
6. 1-approx(Σ{(r(if (i rem 2 =z 0) then 1 else -1 fi ))/((2 * i) + 1)! * x^2^i | 0≤i≤k};2
* N;poly-approx(λi.(r(if (i rem 2 =z 0) then 1 else -1 fi ))/((2 * i) + 1)!;x^2;k;2 * N))
7. Σ{(r(if (i rem 2 =z 0) then 1 else -1 fi ))/((2 * i) + 1)! * x^2^i | 0≤i≤k}
= Σ{-1^i * (x^2 * i)/((2 * i) + 1)! | 0≤i≤k}
⊢ 1-approx(Σ{-1^i * (x^(2 * i) + 1)/((2 * i) + 1)! | 0≤i≤k};N;sine-approx(x;k;N))

---

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)  +  1)/((2  *  i)  +  1)!  |  0\mleq{}i\mleq{}k\};N;sine-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)  +  1)!\mkleeneclose{};\mkleeneopen{}x\^{}2\mkleeneclose{};\mkleeneopen{}2  *  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)  +  1)!  *  x\^{}2\^{}i  |  0\mleq{}i\mleq{}k\}
                          =  \mSigma{}\{-1\^{}i  *  (x\^{}2  *  i)/((2  *  i)  +  1)!  |  0\mleq{}i\mleq{}k\}  BY
                          ((BLemma  `rsum\_functionality`  THENM  D  0)
                            THEN  Auto
                            THEN  (GenConcl  \mkleeneopen{}((2  *  i)  +  1)!  =  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)))

---

Home Index