let a, b be real number ; :: thesis: ( - 1 <= a & a <= 1 & - 1 <= b & b <= 1 implies b * (sqrt (1 + (a ^2 ))) <= sqrt (1 + (b ^2 )) )
assume A1: ( - 1 <= a & a <= 1 & - 1 <= b & b <= 1 ) ; :: thesis: b * (sqrt (1 + (a ^2 ))) <= sqrt (1 + (b ^2 ))
then A2: - (- 1) >= - b by XREAL_1:26;
- 1 <= - b by A1, XREAL_1:26;
then (- (- b)) * (sqrt (1 + (a ^2 ))) <= sqrt (1 + ((- b) ^2 )) by A1, A2, Th125;
hence b * (sqrt (1 + (a ^2 ))) <= sqrt (1 + (b ^2 )) ; :: thesis: verum