---

Step * 1 1 of Lemma rcosine_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
= 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 v1 if (n mod 4 =z 2) then -(v1) if (n mod 4 =z 1) then -(v) else v fi  = rcos(x)
BY
{ (MoveToConcl (-1)
   THEN MoveToConcl (-2)
   THEN RepeatFor 2 (AutoSplit)
   THEN (AutoSplit ORELSE (Auto THEN RWO  "-1" 0 THEN Auto))
   THEN Auto
   THEN RWO  "-2" 0
   THEN Auto) }

---

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
=  if  (n  mod  4  =\msubz{}  0)  then  rsin(x)
    if  (n  mod  4  =\msubz{}  2)  then  -(rsin(x))
    if  (n  mod  4  =\msubz{}  1)  then  -(rcos(x))
    else  rcos(x)
    fi 
8.  v1  :  \mBbbR{}
9.  v1
=  if  (n  mod  4  =\msubz{}  0)  then  rcos(x)
    if  (n  mod  4  =\msubz{}  2)  then  -(rcos(x))
    if  (n  mod  4  =\msubz{}  1)  then  rsin(x)
    else  -(rsin(x))
    fi 
\mvdash{}  if  (n  mod  4  =\msubz{}  0)  then  v1
if  (n  mod  4  =\msubz{}  2)  then  -(v1)
if  (n  mod  4  =\msubz{}  1)  then  -(v)
else  v
fi 
=  rcos(x)


By

---

Latex:
(MoveToConcl  (-1)
  THEN  MoveToConcl  (-2)
  THEN  RepeatFor  2  (AutoSplit)
  THEN  (AutoSplit  ORELSE  (Auto  THEN  RWO    "-1"  0  THEN  Auto))
  THEN  Auto
  THEN  RWO    "-2"  0
  THEN  Auto)

---

Home Index