---

Step * of Lemma rcos-bounds

∀x:ℝ. (rcos(x) ∈ [r(-1), r1])
BY
{ (Intro THEN ((InstLemma `rabs-rcos-rleq` [⌜x⌝]⋅ THENA Auto) THEN Reduce 0) THEN RWO"rabs-rleq-iff" (-1) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}x:\mBbbR{}.  (rcos(x)  \mmember{}  [r(-1),  r1])


By

---

Latex:
(Intro
  THEN  ((InstLemma  `rabs-rcos-rleq`  [\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  Reduce  0)
  THEN  RWO"rabs-rleq-iff"  (-1)
  THEN  Auto)

---

Home Index