---

Step * 1 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)
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)
BY
{ ((RWO "5" (-3) THENA Auto)
   THEN (RWO "5" (-1) THENA Auto)
   THEN (RWO "5" (7) THENA Auto)
   THEN (RWO "5" (8) THENA Auto)
   THEN ThinVar `p') }

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 = 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)

---

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)
9.  v  :  \mBbbR{}
10.  v  =  sine(x  -  n  *  p)
11.  v1  :  \mBbbR{}
12.  v1  =  cosine(x  -  n  *  p)
\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  "5"  (-3)  THENA  Auto)
  THEN  (RWO  "5"  (-1)  THENA  Auto)
  THEN  (RWO  "5"  (7)  THENA  Auto)
  THEN  (RWO  "5"  (8)  THENA  Auto)
  THEN  ThinVar  `p')

---

Home Index