let a, b be real number ; :: 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:26;
then (- a) * (sqrt (1 + ((- b) ^2 ))) <= (- b) * (sqrt (1 + ((- a) ^2 ))) by A1, Lm8;
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