let
x
be
Real
;
:: thesis:
(
x
>=
0
implies
tanh
x
>=
0
)
A1
:
cosh
x
>=
1
by
Lm1
;
assume
A2
:
x
>=
0
;
:: thesis:
tanh
x
>=
0
per
cases
(
x
>
0
or
x
=
0
)
by
A2
;
suppose
x
>
0
;
:: thesis:
tanh
x
>=
0
then
sinh
x
>=
0
by
SIN_COS5:46
;
then
(
sinh
x
)
/
(
cosh
x
)
>=
0
by
A1
;
hence
tanh
x
>=
0
by
Th1
;
:: thesis:
verum
end;
suppose
x
=
0
;
:: thesis:
tanh
x
>=
0
hence
tanh
x
>=
0
by
Th1
;
:: thesis:
verum
end;
end;