let x, y be real number ; :: thesis: ( 1 <= x & 1 <= y & abs y <= abs x implies 0 <= (y * (sqrt ((x ^2 ) - 1))) - (x * (sqrt ((y ^2 ) - 1))) )
assume A1: ( 1 <= x & 1 <= y & abs y <= abs x ) ; :: thesis: 0 <= (y * (sqrt ((x ^2 ) - 1))) - (x * (sqrt ((y ^2 ) - 1)))
A2: ( (abs x) ^2 = x ^2 & (abs y) ^2 = y ^2 ) by COMPLEX1:161;
A3: ( 0 <= x ^2 & 0 <= y ^2 ) by XREAL_1:65;
A4: ( 0 <= (x ^2 ) - 1 & 0 <= (y ^2 ) - 1 ) by A1, Lm4;
( 1 ^2 <= x ^2 & 1 ^2 <= y ^2 ) by A1, SQUARE_1:77;
then A5: 1 * ((y ^2 ) - 1) <= (x ^2 ) * ((y ^2 ) - 1) by A4, XREAL_1:66;
1 <= abs y by A1, ABSVALUE:def 1;
then y ^2 <= x ^2 by A1, A2, SQUARE_1:77;
then (- 1) * (x ^2 ) <= (- 1) * (y ^2 ) by XREAL_1:67;
then (- (x ^2 )) + ((x ^2 ) * (y ^2 )) <= (- (y ^2 )) + ((x ^2 ) * (y ^2 )) by XREAL_1:8;
then sqrt ((x ^2 ) * ((y ^2 ) - 1)) <= sqrt ((y ^2 ) * ((x ^2 ) - 1)) by A4, A5, SQUARE_1:94;
then (sqrt (x ^2 )) * (sqrt ((y ^2 ) - 1)) <= sqrt ((y ^2 ) * ((x ^2 ) - 1)) by A3, A4, SQUARE_1:97;
then x * (sqrt ((y ^2 ) - 1)) <= sqrt ((y ^2 ) * ((x ^2 ) - 1)) by A1, SQUARE_1:89;
then x * (sqrt ((y ^2 ) - 1)) <= (sqrt (y ^2 )) * (sqrt ((x ^2 ) - 1)) by A3, A4, SQUARE_1:97;
then x * (sqrt ((y ^2 ) - 1)) <= y * (sqrt ((x ^2 ) - 1)) by A1, SQUARE_1:89;
then (x * (sqrt ((y ^2 ) - 1))) - (x * (sqrt ((y ^2 ) - 1))) <= (y * (sqrt ((x ^2 ) - 1))) - (x * (sqrt ((y ^2 ) - 1))) by XREAL_1:15;
hence 0 <= (y * (sqrt ((x ^2 ) - 1))) - (x * (sqrt ((y ^2 ) - 1))) ; :: thesis: verum