let a, b be Real; ( b <= 0 & a <= b implies a * (sqrt (1 + (b ^2))) <= b * (sqrt (1 + (a ^2))) )
assume that
A1:
b <= 0
and
A2:
a <= b
; a * (sqrt (1 + (b ^2))) <= b * (sqrt (1 + (a ^2)))
A3:
(- a) * (sqrt (1 + (b ^2))) = sqrt (((- a) ^2) * (1 + (b ^2)))
by A1, A2, Th54;
( a < b or a = b )
by A2, XXREAL_0:1;
then
( b ^2 < a ^2 or a = b )
by A1, Th44;
then A4:
((b ^2) * 1) + ((b ^2) * (a ^2)) <= ((a ^2) * 1) + ((a ^2) * (b ^2))
by XREAL_1:7;
A5:
b ^2 >= 0
by XREAL_1:63;
A6:
a ^2 >= 0
by XREAL_1:63;
then
(- b) * (sqrt (1 + (a ^2))) = sqrt (((- b) ^2) * (1 + (a ^2)))
by A1, Th54;
then
- (a * (sqrt (1 + (b ^2)))) >= - (b * (sqrt (1 + (a ^2))))
by A6, A3, A4, A5, Th26;
hence
a * (sqrt (1 + (b ^2))) <= b * (sqrt (1 + (a ^2)))
by XREAL_1:24; verum