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)))

assume that

A1: a <= 0 and

A2: a <= b ; :: thesis: a * (sqrt (1 + (b ^2))) <= b * (sqrt (1 + (a ^2)))

now :: thesis: ( ( b <= 0 & a * (sqrt (1 + (b ^2))) <= b * (sqrt (1 + (a ^2))) ) or ( b > 0 & a * (sqrt (1 + (b ^2))) <= b * (sqrt (1 + (a ^2))) ) )end;

hence
a * (sqrt (1 + (b ^2))) <= b * (sqrt (1 + (a ^2)))
; :: thesis: verumper cases
( b <= 0 or b > 0 )
;

end;

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

b ^2 >= 0
by XREAL_1:63;

then sqrt (1 + (b ^2)) > 0 by SQUARE_1:25;

then A4: a * (sqrt (1 + (b ^2))) <= 0 by A1;

a ^2 >= 0 by XREAL_1:63;

then sqrt (1 + (a ^2)) > 0 by SQUARE_1:25;

hence a * (sqrt (1 + (b ^2))) <= b * (sqrt (1 + (a ^2))) by A3, A4; :: thesis: verum

end;then sqrt (1 + (b ^2)) > 0 by SQUARE_1:25;

then A4: a * (sqrt (1 + (b ^2))) <= 0 by A1;

a ^2 >= 0 by XREAL_1:63;

then sqrt (1 + (a ^2)) > 0 by SQUARE_1:25;

hence a * (sqrt (1 + (b ^2))) <= b * (sqrt (1 + (a ^2))) by A3, A4; :: thesis: verum