let x be Real; :: thesis: ( x <= 0 implies sinh x <= 0 )

assume A1: x <= 0 ; :: thesis: sinh x <= 0

assume A1: x <= 0 ; :: thesis: sinh x <= 0

per cases
( x < 0 or x = 0 )
by A1, XXREAL_0:1;

end;

suppose A2:
x < 0
; :: thesis: sinh x <= 0

then
- x > 0
by XREAL_1:58;

then A3: exp_R . (- x) >= 1 by SIN_COS:52;

exp_R . x <= 1 by A2, SIN_COS:53;

then (exp_R . x) - (exp_R . (- x)) <= 1 - 1 by A3, XREAL_1:13;

then ((exp_R . x) - (exp_R . (- x))) / 2 <= 0 by XREAL_1:138;

then sinh . x <= 0 by SIN_COS2:def 1;

hence sinh x <= 0 by SIN_COS2:def 2; :: thesis: verum

end;then A3: exp_R . (- x) >= 1 by SIN_COS:52;

exp_R . x <= 1 by A2, SIN_COS:53;

then (exp_R . x) - (exp_R . (- x)) <= 1 - 1 by A3, XREAL_1:13;

then ((exp_R . x) - (exp_R . (- x))) / 2 <= 0 by XREAL_1:138;

then sinh . x <= 0 by SIN_COS2:def 1;

hence sinh x <= 0 by SIN_COS2:def 2; :: thesis: verum