let a, b be Real; :: thesis: ( - 1 <= a & a <= 1 & - 1 <= b & b <= 1 implies ( (- b) * (sqrt (1 + (a ^2))) <= sqrt (1 + (b ^2)) & - (sqrt (1 + (b ^2))) <= b * (sqrt (1 + (a ^2))) ) )
assume that
A1: - 1 <= a and
A2: a <= 1 and
A3: - 1 <= b and
A4: b <= 1 ; :: thesis: ( (- b) * (sqrt (1 + (a ^2))) <= sqrt (1 + (b ^2)) & - (sqrt (1 + (b ^2))) <= b * (sqrt (1 + (a ^2))) )
A5: a ^2 >= 0 by XREAL_1:63;
then A6: 1 + (a ^2) >= 1 + 0 by XREAL_1:7;
b ^2 >= 0 by XREAL_1:63;
then A7: sqrt (1 + (b ^2)) >= 0 by Def2;
A8: sqrt (1 + (a ^2)) >= 0 by A5, Def2;

A9: now :: thesis: (- b) * (sqrt (1 + (a ^2))) <= sqrt (1 + (b ^2))

per cases ( b >= 0 or b < 0 ) ;

suppose b >= 0 ; :: thesis: (- b) * (sqrt (1 + (a ^2))) <= sqrt (1 + (b ^2))

hence (- b) * (sqrt (1 + (a ^2))) <= sqrt (1 + (b ^2)) by A8, A7; :: thesis: verum

end;

suppose A10: b < 0 ; :: thesis: (- b) * (sqrt (1 + (a ^2))) <= sqrt (1 + (b ^2))

A11: (- b) ^2 >= 0 by XREAL_1:63;
(- b) * (sqrt (1 + (a ^2))) = sqrt (((- b) ^2) * (1 + (a ^2))) by A5, A10, Th54;
hence (- b) * (sqrt (1 + (a ^2))) <= sqrt (1 + (b ^2)) by A1, A2, A3, A4, A6, A11, Lm6, Th26; :: thesis: verum

end;

end;

end;

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