let x, y be Real; ( 1 <= x & 1 <= y & |.y.| <= |.x.| implies 0 <= (y * (sqrt ((x ^2) - 1))) - (x * (sqrt ((y ^2) - 1))) )
assume that
A1:
1 <= x
and
A2:
1 <= y
and
A3:
|.y.| <= |.x.|
; 0 <= (y * (sqrt ((x ^2) - 1))) - (x * (sqrt ((y ^2) - 1)))
A4:
0 <= (y ^2) - 1
by A2, Lm3;
A5:
( |.x.| ^2 = x ^2 & |.y.| ^2 = y ^2 )
by COMPLEX1:75;
1 <= |.y.|
by A2, ABSVALUE:def 1;
then
y ^2 <= x ^2
by A3, A5, SQUARE_1:15;
then
(- 1) * (x ^2) <= (- 1) * (y ^2)
by XREAL_1:65;
then
(- (x ^2)) + ((x ^2) * (y ^2)) <= (- (y ^2)) + ((x ^2) * (y ^2))
by XREAL_1:6;
then
( 0 <= x ^2 & sqrt ((x ^2) * ((y ^2) - 1)) <= sqrt ((y ^2) * ((x ^2) - 1)) )
by A1, A4, SQUARE_1:26;
then
(sqrt (x ^2)) * (sqrt ((y ^2) - 1)) <= sqrt ((y ^2) * ((x ^2) - 1))
by A4, SQUARE_1:29;
then A6:
x * (sqrt ((y ^2) - 1)) <= sqrt ((y ^2) * ((x ^2) - 1))
by A1, SQUARE_1:22;
( 0 <= y ^2 & 0 <= (x ^2) - 1 )
by A1, Lm3, XREAL_1:63;
then
x * (sqrt ((y ^2) - 1)) <= (sqrt (y ^2)) * (sqrt ((x ^2) - 1))
by A6, SQUARE_1:29;
then
x * (sqrt ((y ^2) - 1)) <= y * (sqrt ((x ^2) - 1))
by A2, SQUARE_1:22;
then
(x * (sqrt ((y ^2) - 1))) - (x * (sqrt ((y ^2) - 1))) <= (y * (sqrt ((x ^2) - 1))) - (x * (sqrt ((y ^2) - 1)))
by XREAL_1:13;
hence
0 <= (y * (sqrt ((x ^2) - 1))) - (x * (sqrt ((y ^2) - 1)))
; verum