let x, y be real number ; :: thesis: ( 1 <= x & 1 <= y implies (cosh2" x) + (cosh2" y) = cosh2" ((x * y) + (sqrt (((x ^2 ) - 1) * ((y ^2 ) - 1)))) )
assume A1: ( 1 <= x & 1 <= y ) ; :: thesis: (cosh2" x) + (cosh2" y) = cosh2" ((x * y) + (sqrt (((x ^2 ) - 1) * ((y ^2 ) - 1))))
then A2: ( (x ^2 ) - 1 >= 0 & (y ^2 ) - 1 >= 0 ) by Lm4;
then A3: ((x ^2 ) - 1) * ((y ^2 ) - 1) >= 0 * ((y ^2 ) - 1) ;
A4: ( 0 < x + (sqrt ((x ^2 ) - 1)) & 0 < y + (sqrt ((y ^2 ) - 1)) ) by A1, Th23;
A5: (cosh2" x) + (cosh2" y) = (- 1) * ((log number_e ,(x + (sqrt ((x ^2 ) - 1)))) + (log number_e ,(y + (sqrt ((y ^2 ) - 1)))))
.= (- 1) * (log number_e ,((x + (sqrt ((x ^2 ) - 1))) * (y + (sqrt ((y ^2 ) - 1))))) by A4, Lm2, POWER:61
.= - (log number_e ,((((x * (sqrt ((y ^2 ) - 1))) + (y * (sqrt ((x ^2 ) - 1)))) + ((sqrt ((x ^2 ) - 1)) * (sqrt ((y ^2 ) - 1)))) + (x * y)))
.= - (log number_e ,((((x * (sqrt ((y ^2 ) - 1))) + (y * (sqrt ((x ^2 ) - 1)))) + (sqrt (((x ^2 ) - 1) * ((y ^2 ) - 1)))) + (x * y))) by A2, SQUARE_1:97 ;
set t = (x * (sqrt ((y ^2 ) - 1))) + (y * (sqrt ((x ^2 ) - 1)));
(x * (sqrt ((y ^2 ) - 1))) + (y * (sqrt ((x ^2 ) - 1))) = sqrt (((x * (sqrt ((y ^2 ) - 1))) + (y * (sqrt ((x ^2 ) - 1)))) ^2 ) by A1, Th24, SQUARE_1:89
.= sqrt ((((x ^2 ) * ((sqrt ((y ^2 ) - 1)) ^2 )) + ((2 * (x * (sqrt ((y ^2 ) - 1)))) * (y * (sqrt ((x ^2 ) - 1))))) + ((y * (sqrt ((x ^2 ) - 1))) ^2 ))
.= sqrt ((((x ^2 ) * ((y ^2 ) - 1)) + ((2 * (x * (sqrt ((y ^2 ) - 1)))) * (y * (sqrt ((x ^2 ) - 1))))) + ((y * (sqrt ((x ^2 ) - 1))) ^2 )) by A2, SQUARE_1:def 4
.= sqrt (((((x ^2 ) * (y ^2 )) - (x ^2 )) + ((2 * (x * (sqrt ((y ^2 ) - 1)))) * (y * (sqrt ((x ^2 ) - 1))))) + ((y ^2 ) * ((sqrt ((x ^2 ) - 1)) ^2 )))
.= sqrt (((((x ^2 ) * (y ^2 )) - (x ^2 )) + ((2 * (x * (sqrt ((y ^2 ) - 1)))) * (y * (sqrt ((x ^2 ) - 1))))) + ((y ^2 ) * ((x ^2 ) - 1))) by A2, SQUARE_1:def 4
.= sqrt ((((2 * ((x * y) ^2 )) - (x ^2 )) - (y ^2 )) + ((2 * (x * (sqrt ((y ^2 ) - 1)))) * (y * (sqrt ((x ^2 ) - 1))))) ;
then A6: - (log number_e ,((((x * (sqrt ((y ^2 ) - 1))) + (y * (sqrt ((x ^2 ) - 1)))) + (sqrt (((x ^2 ) - 1) * ((y ^2 ) - 1)))) + (x * y))) = - (log number_e ,(((sqrt ((((2 * ((x * y) ^2 )) - (x ^2 )) - (y ^2 )) + (((2 * x) * y) * ((sqrt ((y ^2 ) - 1)) * (sqrt ((x ^2 ) - 1)))))) + (sqrt (((x ^2 ) - 1) * ((y ^2 ) - 1)))) + (x * y)))
.= - (log number_e ,(((sqrt ((((2 * ((x * y) ^2 )) - (x ^2 )) - (y ^2 )) + (((2 * x) * y) * (sqrt (((y ^2 ) - 1) * ((x ^2 ) - 1)))))) + (sqrt (((x ^2 ) - 1) * ((y ^2 ) - 1)))) + (x * y))) by A2, SQUARE_1:97 ;
cosh2" ((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 A3, SQUARE_1:def 4
.= - (log number_e ,((sqrt ((((2 * ((x * y) ^2 )) - (x ^2 )) - (y ^2 )) + (((2 * x) * y) * (sqrt (((y ^2 ) - 1) * ((x ^2 ) - 1)))))) + ((sqrt (((x ^2 ) - 1) * ((y ^2 ) - 1))) + (x * y)))) ;
hence (cosh2" x) + (cosh2" y) = cosh2" ((x * y) + (sqrt (((x ^2 ) - 1) * ((y ^2 ) - 1)))) by A5, A6; :: thesis: verum