let x be Real; :: thesis: ( x ^2 > 1 implies coth" x = tanh" (1 / x) )
assume x ^2 > 1 ; :: thesis: coth" x = tanh" (1 / x)
then A1: x <> 0 ;
then tanh" (1 / x) = (1 / 2) * (log (number_e,(((1 + (x * 1)) / x) / (1 - (1 / x))))) by XCMPLX_1:113
.= (1 / 2) * (log (number_e,(((1 + (x * 1)) / x) / (((1 * x) - 1) / x)))) by A1, XCMPLX_1:127
.= (1 / 2) * (log (number_e,((1 + x) / (x - 1)))) by A1, XCMPLX_1:55 ;
hence coth" x = tanh" (1 / x) ; :: thesis: verum