---

Step * 1 1 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. v : ℝ
9. Σ{-1^i * (x^2 * i)/((2 * i) + 1)! | 0≤i≤k} = v ∈ ℝ
10. w : ℝ
11. Σ{-1^i * (x^(2 * i) + 1)/((2 * i) + 1)! | 0≤i≤k} = w ∈ ℝ
⊢ 1-approx(v;2 * N;u)
⇒ ((x * v) = w)
⇒ 1-approx(w;N;eval u = u in
                eval b = |u| + 1 in
                eval z = x b in
                  (u * z) ÷ 4 * b)
BY
{ ((CallByValueReduce 0 THENA Auto)
   THEN (GenConcl ⌜(|u| + 1) = b ∈ ℕ+⌝⋅ THENA Auto)
   THEN (CallByValueReduce 0 THENA Auto)
   THEN (InstLemma `ireal-approx-1` [⌜x⌝;⌜b⌝]⋅ THENA Auto)
   THEN MoveToConcl (-1)
   THEN GenConcl ⌜(x b) = z ∈ ℤ⌝⋅
   THEN Auto
   THEN (CallByValueReduce 0 THENA 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. v : ℝ
9. Σ{-1^i * (x^2 * i)/((2 * i) + 1)! | 0≤i≤k} = v ∈ ℝ
10. w : ℝ
11. Σ{-1^i * (x^(2 * i) + 1)/((2 * i) + 1)! | 0≤i≤k} = w ∈ ℝ
12. b : ℕ+
13. (|u| + 1) = b ∈ ℕ+
14. z : ℤ
15. (x b) = z ∈ ℤ
16. 1-approx(x;b;z)
17. 1-approx(v;2 * N;u)
18. (x * v) = w
⊢ 1-approx(w;N;(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.  v  :  \mBbbR{}
9.  \mSigma{}\{-1\^{}i  *  (x\^{}2  *  i)/((2  *  i)  +  1)!  |  0\mleq{}i\mleq{}k\}  =  v
10.  w  :  \mBbbR{}
11.  \mSigma{}\{-1\^{}i  *  (x\^{}(2  *  i)  +  1)/((2  *  i)  +  1)!  |  0\mleq{}i\mleq{}k\}  =  w
\mvdash{}  1-approx(v;2  *  N;u)
{}\mRightarrow{}  ((x  *  v)  =  w)
{}\mRightarrow{}  1-approx(w;N;eval  u  =  u  in
                                eval  b  =  |u|  +  1  in
                                eval  z  =  x  b  in
                                    (u  *  z)  \mdiv{}  4  *  b)


By

---

Latex:
((CallByValueReduce  0  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}(|u|  +  1)  =  b\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  (InstLemma  `ireal-approx-1`  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  GenConcl  \mkleeneopen{}(x  b)  =  z\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  (CallByValueReduce  0  THENA  Auto))

---

Home Index