let x, y be real number ; :: thesis: ( 1 <= x & 1 <= y & abs y <= abs x implies (cosh1" x) - (cosh1" y) = cosh1" ((x * y) - (sqrt (((x ^2 ) - 1) * ((y ^2 ) - 1)))) )
assume A1: ( 1 <= x & 1 <= y & abs y <= abs x ) ; :: thesis: (cosh1" x) - (cosh1" y) = cosh1" ((x * y) - (sqrt (((x ^2 ) - 1) * ((y ^2 ) - 1))))
then A2: y - (sqrt ((y ^2 ) - 1)) > 0 by Th25;
A3: ( 0 < x + (sqrt ((x ^2 ) - 1)) & 0 < y + (sqrt ((y ^2 ) - 1)) ) by A1, Th23;
A4: ( 0 <= (x ^2 ) - 1 & 0 <= (y ^2 ) - 1 ) by A1, Lm4;
then A5: 0 * ((y ^2 ) - 1) <= ((x ^2 ) - 1) * ((y ^2 ) - 1) ;
A6: (cosh1" x) - (cosh1" y) = log number_e ,((x + (sqrt ((x ^2 ) - 1))) / (y + (sqrt ((y ^2 ) - 1)))) by A3, Lm2, POWER:62
.= log number_e ,(((x + (sqrt ((x ^2 ) - 1))) * (y - (sqrt ((y ^2 ) - 1)))) / ((y + (sqrt ((y ^2 ) - 1))) * (y - (sqrt ((y ^2 ) - 1))))) by A2, XCMPLX_1:92
.= log number_e ,(((x + (sqrt ((x ^2 ) - 1))) * (y - (sqrt ((y ^2 ) - 1)))) / ((y ^2 ) - ((sqrt ((y ^2 ) - 1)) ^2 )))
.= log number_e ,(((x + (sqrt ((x ^2 ) - 1))) * (y - (sqrt ((y ^2 ) - 1)))) / ((y ^2 ) - ((y ^2 ) - 1))) by A4, SQUARE_1:def 4
.= log number_e ,((((x * y) - (x * (sqrt ((y ^2 ) - 1)))) + (y * (sqrt ((x ^2 ) - 1)))) - ((sqrt ((x ^2 ) - 1)) * (sqrt ((y ^2 ) - 1))))
.= log number_e ,((((x * y) - (x * (sqrt ((y ^2 ) - 1)))) + (y * (sqrt ((x ^2 ) - 1)))) - (sqrt (((x ^2 ) - 1) * ((y ^2 ) - 1)))) by A4, SQUARE_1:97
.= log number_e ,((((x * y) - (sqrt (((x ^2 ) - 1) * ((y ^2 ) - 1)))) + (y * (sqrt ((x ^2 ) - 1)))) - (x * (sqrt ((y ^2 ) - 1)))) ;
set t = (y * (sqrt ((x ^2 ) - 1))) - (x * (sqrt ((y ^2 ) - 1)));
A7: (y * (sqrt ((x ^2 ) - 1))) - (x * (sqrt ((y ^2 ) - 1))) = sqrt (((y * (sqrt ((x ^2 ) - 1))) - (x * (sqrt ((y ^2 ) - 1)))) ^2 ) by A1, Th26, SQUARE_1:89
.= sqrt ((((y ^2 ) * ((sqrt ((x ^2 ) - 1)) ^2 )) - ((2 * (y * (sqrt ((x ^2 ) - 1)))) * (x * (sqrt ((y ^2 ) - 1))))) + ((x * (sqrt ((y ^2 ) - 1))) ^2 ))
.= sqrt ((((y ^2 ) * ((x ^2 ) - 1)) - ((2 * (y * (sqrt ((x ^2 ) - 1)))) * (x * (sqrt ((y ^2 ) - 1))))) + ((x * (sqrt ((y ^2 ) - 1))) ^2 )) by A4, SQUARE_1:def 4
.= sqrt (((((x * y) ^2 ) - (y ^2 )) - ((2 * (y * (sqrt ((x ^2 ) - 1)))) * (x * (sqrt ((y ^2 ) - 1))))) + ((x ^2 ) * ((sqrt ((y ^2 ) - 1)) ^2 )))
.= sqrt (((((x * y) ^2 ) - (y ^2 )) - ((2 * (y * (sqrt ((x ^2 ) - 1)))) * (x * (sqrt ((y ^2 ) - 1))))) + ((x ^2 ) * ((y ^2 ) - 1))) by A4, SQUARE_1:def 4
.= sqrt ((((2 * ((x * y) ^2 )) - (x ^2 )) - (y ^2 )) - (((2 * x) * y) * ((sqrt ((x ^2 ) - 1)) * (sqrt ((y ^2 ) - 1)))))
.= sqrt ((((2 * ((x * y) ^2 )) - (x ^2 )) - (y ^2 )) - (((2 * x) * y) * (sqrt (((x ^2 ) - 1) * ((y ^2 ) - 1))))) by A4, SQUARE_1:97 ;
cosh1" ((x * y) - (sqrt (((x ^2 ) - 1) * ((y ^2 ) - 1)))) = log number_e ,(((x * y) - (sqrt (((x ^2 ) - 1) * ((y ^2 ) - 1)))) + (sqrt (((((x * y) ^2 ) - ((2 * (x * y)) * (sqrt (((x ^2 ) - 1) * ((y ^2 ) - 1))))) + ((sqrt (((x ^2 ) - 1) * ((y ^2 ) - 1))) ^2 )) - 1)))
.= log number_e ,(((x * y) - (sqrt (((x ^2 ) - 1) * ((y ^2 ) - 1)))) + (sqrt (((((x * y) ^2 ) - ((2 * (x * y)) * (sqrt (((x ^2 ) - 1) * ((y ^2 ) - 1))))) + (((x ^2 ) - 1) * ((y ^2 ) - 1))) - 1))) by A5, SQUARE_1:def 4
.= log number_e ,(((x * y) - (sqrt (((x ^2 ) - 1) * ((y ^2 ) - 1)))) + (sqrt ((((2 * ((x * y) ^2 )) - (x ^2 )) - (y ^2 )) - (((2 * x) * y) * (sqrt (((x ^2 ) - 1) * ((y ^2 ) - 1))))))) ;
hence (cosh1" x) - (cosh1" y) = cosh1" ((x * y) - (sqrt (((x ^2 ) - 1) * ((y ^2 ) - 1)))) by A6, A7; :: thesis: verum