let a, b be real number ; :: thesis: ( b <= 0 & a <= b implies a * (sqrt (1 + (b ^2 ))) <= b * (sqrt (1 + (a ^2 ))) )
assume A1: ( b <= 0 & a <= b ) ; :: thesis: a * (sqrt (1 + (b ^2 ))) <= b * (sqrt (1 + (a ^2 )))
a ^2 >= 0 by XREAL_1:65;
then A2: 1 + (a ^2 ) >= 1 + 0 by XREAL_1:9;
b ^2 >= 0 by XREAL_1:65;
then A3: 1 + (b ^2 ) >= 1 + 0 by XREAL_1:9;
- (- b) <= 0 by A1;
then - b >= 0 ;
then A4: (- b) * (sqrt (1 + (a ^2 ))) = sqrt (((- b) ^2 ) * (1 + (a ^2 ))) by A2, SQUARE_1:124;
- (- a) <= 0 by A1;
then - a >= 0 ;
then A5: (- a) * (sqrt (1 + (b ^2 ))) = sqrt (((- a) ^2 ) * (1 + (b ^2 ))) by A3, SQUARE_1:124;
( a < b or a = b ) by A1, XXREAL_0:1;
then ( b ^2 < a ^2 or a = b ) by A1, SQUARE_1:114;
then A6: ((b ^2 ) * 1) + ((b ^2 ) * (a ^2 )) <= ((a ^2 ) * 1) + ((a ^2 ) * (b ^2 )) by XREAL_1:9;
b ^2 >= 0 by XREAL_1:65;
then (b ^2 ) * (1 + (a ^2 )) >= 0 by A2;
then - (a * (sqrt (1 + (b ^2 )))) >= - (b * (sqrt (1 + (a ^2 )))) by A4, A5, A6, SQUARE_1:94;
hence a * (sqrt (1 + (b ^2 ))) <= b * (sqrt (1 + (a ^2 ))) by XREAL_1:26; :: thesis: verum