---

Step * of Lemma rsin-rcos-pythag

∀x:ℝ. ((rsin(x)^2 + rcos(x)^2) = r1)
BY
{ (Auto THEN RWO "rsin-is-sine rcos-is-cosine" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}x:\mBbbR{}.  ((rsin(x)\^{}2  +  rcos(x)\^{}2)  =  r1)


By

---

Latex:
(Auto  THEN  RWO  "rsin-is-sine  rcos-is-cosine"  0  THEN  Auto)

---

Home Index