---

Step * 1 of Lemma sine-approx-property


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))
BY
{ ((RWO  "-1" (-2) THENA Auto)
   THEN Thin (-1)
   THEN MoveToConcl (-1)
   THEN Unfold `sine-approx` 0
   THEN GenConcl ⌜poly-approx(λi.(r(if (i rem 2 =z 0) then 1 else -1 fi ))/((2 * i) + 1)!;x^2;k;2 * N) = u ∈ ℤ⌝⋅
   THEN Auto) }

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

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  k  :  \mBbbN{}
3.  N  :  \mBbbN{}\msupplus{}
4.  |x|  \mleq{}  (r1/r(2))
5.  |x\^{}2|  \mleq{}  (r1/r(4))
6.  1-approx(\mSigma{}\{(r(if  (i  rem  2  =\msubz{}  0)  then  1  else  -1  fi  ))/((2  *  i)  +  1)!  *  x\^{}2\^{}i  |  0\mleq{}i\mleq{}k\};2
*  N;poly-approx(\mlambda{}i.(r(if  (i  rem  2  =\msubz{}  0)  then  1  else  -1  fi  ))/((2  *  i)  +  1)!;x\^{}2;k;2  *  N))
7.  \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\}
\mvdash{}  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:
((RWO    "-1"  (-2)  THENA  Auto)
  THEN  Thin  (-1)
  THEN  MoveToConcl  (-1)
  THEN  Unfold  `sine-approx`  0
  THEN  GenConcl  \mkleeneopen{}poly-approx(\mlambda{}i.(r(if  (i  rem  2  =\msubz{}  0)  then  1  else  -1  fi  ))/((2  *  i)  +  1)!;x\^{}2;k;2  *  N)
                                =  u\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index