---

Step * 1 1 of Lemma sine-approx-property


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)
BY
{ (Assert (x * Σ{-1^i * (x^2 * i)/((2 * i) + 1)! | 0≤i≤k}) = Σ{-1^i * (x^(2 * i) + 1)/((2 * i) + 1)! | 0≤i≤k} BY
         ((RWO "rsum_linearity2<" 0 THENA Auto)
          THEN BLemma `rsum_functionality`
          THEN Auto
          THEN D 0
          THEN Auto
          THEN (GenConcl ⌜((2 * i) + 1)! = D ∈ ℕ+⌝⋅ THENA Auto)
          THEN (GenConcl ⌜(2 * i) = m ∈ ℕ⌝⋅ THENA Auto)
          THEN (GenConcl ⌜-1^i = a ∈ ℤ⌝⋅ THENA Auto)
          THEN All Thin
          THEN (RWW "int-rmul-req int-rdiv-req" 0 THENA Auto)
          THEN (RWW "rnexp-add1" 0 THENA Auto)
          THEN nRMul ⌜r(D)⌝ 0⋅
          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)
9. (x * Σ{-1^i * (x^2 * i)/((2 * i) + 1)! | 0≤i≤k}) = Σ{-1^i * (x^(2 * i) + 1)/((2 * i) + 1)! | 0≤i≤k}
⊢ 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.  u  :  \mBbbZ{}
7.  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
8.  1-approx(\mSigma{}\{-1\^{}i  *  (x\^{}2  *  i)/((2  *  i)  +  1)!  |  0\mleq{}i\mleq{}k\};2  *  N;u)
\mvdash{}  1-approx(\mSigma{}\{-1\^{}i  *  (x\^{}(2  *  i)  +  1)/((2  *  i)  +  1)!  |  0\mleq{}i\mleq{}k\};N;eval  u  =  u  in
                                                                                                                            eval  b  =  |u|  +  1  in
                                                                                                                            eval  z  =  x  b  in
                                                                                                                                (u  *  z)  \mdiv{}  4  *  b)


By

---

Latex:
(Assert  (x  *  \mSigma{}\{-1\^{}i  *  (x\^{}2  *  i)/((2  *  i)  +  1)!  |  0\mleq{}i\mleq{}k\})
              =  \mSigma{}\{-1\^{}i  *  (x\^{}(2  *  i)  +  1)/((2  *  i)  +  1)!  |  0\mleq{}i\mleq{}k\}  BY
              ((RWO  "rsum\_linearity2<"  0  THENA  Auto)
                THEN  BLemma  `rsum\_functionality`
                THEN  Auto
                THEN  D  0
                THEN  Auto
                THEN  (GenConcl  \mkleeneopen{}((2  *  i)  +  1)!  =  D\mkleeneclose{}\mcdot{}  THENA  Auto)
                THEN  (GenConcl  \mkleeneopen{}(2  *  i)  =  m\mkleeneclose{}\mcdot{}  THENA  Auto)
                THEN  (GenConcl  \mkleeneopen{}-1\^{}i  =  a\mkleeneclose{}\mcdot{}  THENA  Auto)
                THEN  All  Thin
                THEN  (RWW  "int-rmul-req  int-rdiv-req"  0  THENA  Auto)
                THEN  (RWW  "rnexp-add1"  0  THENA  Auto)
                THEN  nRMul  \mkleeneopen{}r(D)\mkleeneclose{}  0\mcdot{}
                THEN  Auto))

---

Home Index