---

Step * of Lemma rabs-sine-rleq

∀x:ℝ. (|sine(x)| ≤ r1)
BY
{ (InstLemma `sine-cosine-pythag` [] THEN ParallelLast') }

1
1. x : ℝ
2. (sine(x)^2 + cosine(x)^2) = r1
⊢ |sine(x)| ≤ r1

---

Latex:

---

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


By

---

Latex:
(InstLemma  `sine-cosine-pythag`  []  THEN  ParallelLast')

---

Home Index