let
x
be
Real
;
:: thesis:
(
x
>=
0
implies
sinh
x
>=
0
)
assume
A1
:
x
>=
0
;
:: thesis:
sinh
x
>=
0
per
cases
(
x
>
0
or
x
=
0
)
by
A1
,
XXREAL_0:1
;
suppose
x
>
0
;
:: thesis:
sinh
x
>=
0
hence
sinh
x
>=
0
by
Lm4
;
:: thesis:
verum
end;
suppose
x
=
0
;
:: thesis:
sinh
x
>=
0
hence
sinh
x
>=
0
by
SIN_COS2:16
,
SIN_COS2:def 2
;
:: thesis:
verum
end;
end;