---

Step * of Lemma rabs-rsin-rleq

∀x:ℝ. (|rsin(x)| ≤ r1)
BY
{ (Auto THEN RWO "rsin-is-sine rcos-is-cosine" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}x:\mBbbR{}.  (|rsin(x)|  \mleq{}  r1)


By

---

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

---

Home Index