let x be real number ; :: thesis: ( x ^2 > 1 implies coth" x = tanh" (1 / x) )
assume x ^2 > 1 ; :: thesis: coth" x = tanh" (1 / x)
then A1: ( (1 / x) ^2 < 1 & x <> 0 ) by Th21;
then tanh" (1 / x) = (1 / 2) * (log number_e ,(((1 + (x * 1)) / x) / (1 - (1 / x)))) by XCMPLX_1:114
.= (1 / 2) * (log number_e ,(((1 + (x * 1)) / x) / (((1 * x) - 1) / x))) by A1, XCMPLX_1:128
.= (1 / 2) * (log number_e ,((1 + x) / (x - 1))) by A1, XCMPLX_1:55 ;
hence coth" x = tanh" (1 / x) ; :: thesis: verum