let x be real number ; :: thesis: ( x < 0 implies sinh" x = cosh2" (sqrt ((x ^2 ) + 1)) )
assume A1: x < 0 ; :: thesis: sinh" x = cosh2" (sqrt ((x ^2 ) + 1))
A2: (sqrt ((x ^2 ) + 1)) + x > 0 by Th5;
A3: 1 / ((sqrt ((x ^2 ) + 1)) + x) = ((sqrt ((x ^2 ) + 1)) + x) to_power (- 1) by Th1, Th5;
x ^2 >= 0 by XREAL_1:65;
then A4: (x ^2 ) + 1 >= 0 + 1 by XREAL_1:9;
then cosh2" (sqrt ((x ^2 ) + 1)) = - (log number_e ,((sqrt ((x ^2 ) + 1)) + (sqrt (((x ^2 ) + 1) - 1)))) by SQUARE_1:def 4
.= - (log number_e ,((sqrt ((x ^2 ) + 1)) + (- x))) by A1, SQUARE_1:90
.= - (log number_e ,((((sqrt ((x ^2 ) + 1)) - x) * ((sqrt ((x ^2 ) + 1)) + x)) / ((sqrt ((x ^2 ) + 1)) + x))) by A2, XCMPLX_1:90
.= - (log number_e ,((((sqrt ((x ^2 ) + 1)) ^2 ) - (x ^2 )) / ((sqrt ((x ^2 ) + 1)) + x)))
.= - (log number_e ,((((x ^2 ) + 1) - (x ^2 )) / ((sqrt ((x ^2 ) + 1)) + x))) by A4, SQUARE_1:def 4
.= - ((- 1) * (log number_e ,((sqrt ((x ^2 ) + 1)) + x))) by A2, A3, Lm2, POWER:63
.= log number_e ,((sqrt ((x ^2 ) + 1)) + x) ;
hence sinh" x = cosh2" (sqrt ((x ^2 ) + 1)) ; :: thesis: verum