Step
*
1
of Lemma
rcos_wf1
1. x : ℝ
2. x1 : ℝ
⊢ |-(sine(x1))| ≤ r1
BY
{ (RWO "rabs-rminus" 0 THEN Auto) }
Latex:
Latex:
1. x : \mBbbR{}
2. x1 : \mBbbR{}
\mvdash{} |-(sine(x1))| \mleq{} r1
By
Latex:
(RWO "rabs-rminus" 0 THEN Auto)
Home
Index