---

Step * 1 of Lemma req-rcos-and-rsin-implies


1. x : ℝ
2. y : ℝ
3. rsin(x) = rsin(y)
4. rcos(x) = rcos(y)
⊢ rcos(x - y) = r1
BY
{ (RWW "rcos-rsub -1 -2 rnexp2<" 0 THEN Auto THEN RWO "radd_comm" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  y  :  \mBbbR{}
3.  rsin(x)  =  rsin(y)
4.  rcos(x)  =  rcos(y)
\mvdash{}  rcos(x  -  y)  =  r1


By

---

Latex:
(RWW  "rcos-rsub  -1  -2  rnexp2<"  0  THEN  Auto  THEN  RWO  "radd\_comm"  0  THEN  Auto)

---

Home Index