let a, b be real number ; :: thesis: ( a >= 0 & a >= b implies a * (sqrt (1 + (b ^2 ))) >= b * (sqrt (1 + (a ^2 ))) )
assume A1: ( a >= 0 & a >= b ) ; :: thesis: a * (sqrt (1 + (b ^2 ))) >= b * (sqrt (1 + (a ^2 )))
then A2: - a <= 0 ;
- a <= - b by A1, XREAL_1:26;
then (- a) * (sqrt (1 + ((- b) ^2 ))) <= (- b) * (sqrt (1 + ((- a) ^2 ))) by A2, Lm9;
then - (a * (sqrt (1 + (b ^2 )))) <= - (b * (sqrt (1 + (a ^2 )))) ;
hence a * (sqrt (1 + (b ^2 ))) >= b * (sqrt (1 + (a ^2 ))) by XREAL_1:26; :: thesis: verum