let a, b be Real; :: thesis: ( b <= 0 & a <= b implies a * (sqrt (1 + (b ^2))) <= b * (sqrt (1 + (a ^2))) )

assume that

A1: b <= 0 and

A2: a <= b ; :: thesis: a * (sqrt (1 + (b ^2))) <= b * (sqrt (1 + (a ^2)))

A3: a ^2 >= 0 by XREAL_1:63;

then A4: (- b) * (sqrt (1 + (a ^2))) = sqrt (((- b) ^2) * (1 + (a ^2))) by A1, SQUARE_1:54;

A5: (- a) * (sqrt (1 + (b ^2))) = sqrt (((- a) ^2) * (1 + (b ^2))) by A1, A2, SQUARE_1:54;

( a < b or a = b ) by A2, XXREAL_0:1;

then ( b ^2 < a ^2 or a = b ) by A1, SQUARE_1:44;

then A6: ((b ^2) * 1) + ((b ^2) * (a ^2)) <= ((a ^2) * 1) + ((a ^2) * (b ^2)) by XREAL_1:7;

b ^2 >= 0 by XREAL_1:63;

then - (a * (sqrt (1 + (b ^2)))) >= - (b * (sqrt (1 + (a ^2)))) by A3, A4, A5, A6, SQUARE_1:26;

hence a * (sqrt (1 + (b ^2))) <= b * (sqrt (1 + (a ^2))) by XREAL_1:24; :: thesis: verum

assume that

A1: b <= 0 and

A2: a <= b ; :: thesis: a * (sqrt (1 + (b ^2))) <= b * (sqrt (1 + (a ^2)))

A3: a ^2 >= 0 by XREAL_1:63;

then A4: (- b) * (sqrt (1 + (a ^2))) = sqrt (((- b) ^2) * (1 + (a ^2))) by A1, SQUARE_1:54;

A5: (- a) * (sqrt (1 + (b ^2))) = sqrt (((- a) ^2) * (1 + (b ^2))) by A1, A2, SQUARE_1:54;

( a < b or a = b ) by A2, XXREAL_0:1;

then ( b ^2 < a ^2 or a = b ) by A1, SQUARE_1:44;

then A6: ((b ^2) * 1) + ((b ^2) * (a ^2)) <= ((a ^2) * 1) + ((a ^2) * (b ^2)) by XREAL_1:7;

b ^2 >= 0 by XREAL_1:63;

then - (a * (sqrt (1 + (b ^2)))) >= - (b * (sqrt (1 + (a ^2)))) by A3, A4, A5, A6, SQUARE_1:26;

hence a * (sqrt (1 + (b ^2))) <= b * (sqrt (1 + (a ^2))) by XREAL_1:24; :: thesis: verum