let x, y be real number ; ( 1 <= x & 1 <= y & abs y <= abs x implies 0 <= (y * (sqrt ((x ^2 ) - 1))) - (x * (sqrt ((y ^2 ) - 1))) )
assume that
A1:
1 <= x
and
A2:
1 <= y
and
A3:
abs y <= abs x
; 0 <= (y * (sqrt ((x ^2 ) - 1))) - (x * (sqrt ((y ^2 ) - 1)))
A4:
0 <= (y ^2 ) - 1
by A2, Lm3;
A5:
( (abs x) ^2 = x ^2 & (abs y) ^2 = y ^2 )
by COMPLEX1:161;
1 <= abs y
by A2, ABSVALUE:def 1;
then
y ^2 <= x ^2
by A3, A5, 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
( 0 <= x ^2 & sqrt ((x ^2 ) * ((y ^2 ) - 1)) <= sqrt ((y ^2 ) * ((x ^2 ) - 1)) )
by A1, A4, SQUARE_1:94, XREAL_1:65;
then
(sqrt (x ^2 )) * (sqrt ((y ^2 ) - 1)) <= sqrt ((y ^2 ) * ((x ^2 ) - 1))
by A4, SQUARE_1:97;
then A6:
x * (sqrt ((y ^2 ) - 1)) <= sqrt ((y ^2 ) * ((x ^2 ) - 1))
by A1, SQUARE_1:89;
( 0 <= y ^2 & 0 <= (x ^2 ) - 1 )
by A1, Lm3, XREAL_1:65;
then
x * (sqrt ((y ^2 ) - 1)) <= (sqrt (y ^2 )) * (sqrt ((x ^2 ) - 1))
by A6, SQUARE_1:97;
then
x * (sqrt ((y ^2 ) - 1)) <= y * (sqrt ((x ^2 ) - 1))
by A2, 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)))
; verum