---

Step * 1 1 1 of Lemma rsine_wf


1. x : ℝ
2. n : ℤ
3. |x - r(n) * π/2| ≤ r(2)
4. -(r(2)) ≤ (x - n * π/2)
5. (x - n * π/2) ≤ r(2)
6. v : ℝ
7. v = sine(x - n * π/2)
8. v1 : ℝ
9. v1 = cosine(x - n * π/2)
⊢ 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)
BY
{ ((RWO "rsin-is-sine<" (-3) THENA Auto)
   THEN (RWO "rsin-reduce-half-pi" (-3) THENA Auto)
   THEN (RWO "rcos-is-cosine<" (-1) THENA Auto)
   THEN (RWO "rcos-reduce-half-pi" (-1) THENA Auto)) }

1
1. x : ℝ
2. n : ℤ
3. |x - r(n) * π/2| ≤ r(2)
4. -(r(2)) ≤ (x - n * π/2)
5. (x - n * π/2) ≤ r(2)
6. v : ℝ
7. v
= if (n mod 4 =z 0) then rsin(x)
  if (n mod 4 =z 2) then -(rsin(x))
  if (n mod 4 =z 1) then -(rcos(x))
  else rcos(x)
  fi 
8. v1 : ℝ
9. v1
= if (n mod 4 =z 0) then rcos(x)
  if (n mod 4 =z 2) then -(rcos(x))
  if (n mod 4 =z 1) then rsin(x)
  else -(rsin(x))
  fi 
⊢ 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.  -(r(2))  \mleq{}  (x  -  n  *  \mpi{}/2)
5.  (x  -  n  *  \mpi{}/2)  \mleq{}  r(2)
6.  v  :  \mBbbR{}
7.  v  =  sine(x  -  n  *  \mpi{}/2)
8.  v1  :  \mBbbR{}
9.  v1  =  cosine(x  -  n  *  \mpi{}/2)
\mvdash{}  if  (n  mod  4  =\msubz{}  0)  then  v
if  (n  mod  4  =\msubz{}  2)  then  -(v)
if  (n  mod  4  =\msubz{}  1)  then  v1
else  -(v1)
fi 
=  rsin(x)


By

---

Latex:
((RWO  "rsin-is-sine<"  (-3)  THENA  Auto)
  THEN  (RWO  "rsin-reduce-half-pi"  (-3)  THENA  Auto)
  THEN  (RWO  "rcos-is-cosine<"  (-1)  THENA  Auto)
  THEN  (RWO  "rcos-reduce-half-pi"  (-1)  THENA  Auto))

---

Home Index