Step
*
2
of Lemma
sinh-rleq
1. x : {x:ℝ| x ∈ (-∞, ∞)}
⊢ r0 ≤ cosh(x)
BY
{ (RWO "cosh-ge-1<" 0 THEN Auto) }
Latex:
Latex:
1. x : \{x:\mBbbR{}| x \mmember{} (-\minfty{}, \minfty{})\}
\mvdash{} r0 \mleq{} cosh(x)
By
Latex:
(RWO "cosh-ge-1<" 0 THEN Auto)
Home
Index