---

Step * 1 of Lemma rsine_wf


1. x : ℝ
2. n : ℤ
3. |x - r(n) * π/2| ≤ r(2)
4. p : ℝ
5. p = π/2
6. |x - n * p| ≤ r(2)
7. -(r(2)) ≤ (x - n * p)
8. (x - n * p) ≤ r(2)
⊢ if (n mod 4 =z 0) then sine-medium(x - n * p)
if (n mod 4 =z 2) then -(sine-medium(x - n * p))
if (n mod 4 =z 1) then cosine-medium(x - n * p)
else -(cosine-medium(x - n * p))
fi 
= rsin(x)
BY
{ (GenConclTerms  Auto [⌜sine-medium(x - n * p)⌝;⌜cosine-medium(x - n * p)⌝]⋅
   THEN Thin (-3)
   THEN Thin (-1)
   THEN D -2
   THEN D -1
   THEN (Unhide THENA Auto)) }

1
1. x : ℝ
2. n : ℤ
3. |x - r(n) * π/2| ≤ r(2)
4. p : ℝ
5. p = π/2
6. |x - n * p| ≤ r(2)
7. -(r(2)) ≤ (x - n * p)
8. (x - n * p) ≤ r(2)
9. v : ℝ
10. v = sine(x - n * p)
11. v1 : ℝ
12. v1 = cosine(x - n * p)
⊢ if (n mod 4 =z 0) then v if (n mod 4 =z 2) then -(v) if (n mod 4 =z 1) then v1 else -(v1) fi  = rsin(x)

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  n  :  \mBbbZ{}
3.  |x  -  r(n)  *  \mpi{}/2|  \mleq{}  r(2)
4.  p  :  \mBbbR{}
5.  p  =  \mpi{}/2
6.  |x  -  n  *  p|  \mleq{}  r(2)
7.  -(r(2))  \mleq{}  (x  -  n  *  p)
8.  (x  -  n  *  p)  \mleq{}  r(2)
\mvdash{}  if  (n  mod  4  =\msubz{}  0)  then  sine-medium(x  -  n  *  p)
if  (n  mod  4  =\msubz{}  2)  then  -(sine-medium(x  -  n  *  p))
if  (n  mod  4  =\msubz{}  1)  then  cosine-medium(x  -  n  *  p)
else  -(cosine-medium(x  -  n  *  p))
fi 
=  rsin(x)


By

---

Latex:
(GenConclTerms    Auto  [\mkleeneopen{}sine-medium(x  -  n  *  p)\mkleeneclose{};\mkleeneopen{}cosine-medium(x  -  n  *  p)\mkleeneclose{}]\mcdot{}
  THEN  Thin  (-3)
  THEN  Thin  (-1)
  THEN  D  -2
  THEN  D  -1
  THEN  (Unhide  THENA  Auto))

---

Home Index