let a, b be Real; :: thesis: ( a >= 0 & a >= b implies a * (sqrt (1 + (b ^2))) >= b * (sqrt (1 + (a ^2))) )
assume that
A1: a >= 0 and
A2: a >= b ; :: thesis: a * (sqrt (1 + (b ^2))) >= b * (sqrt (1 + (a ^2)))
- a <= - b by A2, XREAL_1:24;
then (- a) * (sqrt (1 + ((- b) ^2))) <= (- b) * (sqrt (1 + ((- a) ^2))) by A1, Lm2;
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:24; :: thesis: verum