let a, b be Real; :: thesis: ( - 1 <= a & a <= 1 & - 1 <= b & b <= 1 implies b * (sqrt (1 + (a ^2))) <= sqrt (1 + (b ^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))

A5: - 1 <= - b by A4, XREAL_1:24;

- (- 1) >= - b by A3, XREAL_1:24;

then (- (- b)) * (sqrt (1 + (a ^2))) <= sqrt (1 + ((- b) ^2)) by A1, A2, A5, Th55;

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

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

A5: - 1 <= - b by A4, XREAL_1:24;

- (- 1) >= - b by A3, XREAL_1:24;

then (- (- b)) * (sqrt (1 + (a ^2))) <= sqrt (1 + ((- b) ^2)) by A1, A2, A5, Th55;

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