let x be real number ; :: thesis: ( sinh x <> 0 implies coth (2 * x) = (1 + ((coth x) ^2 )) / (2 * (coth x)) )
assume sinh x <> 0 ; :: thesis: coth (2 * x) = (1 + ((coth x) ^2 )) / (2 * (coth x))
then A1: sinh . x <> 0 by SIN_COS2:def 2;
then A2: (sinh . x) ^2 <> 0 by SQUARE_1:74;
coth (2 * x) = (cosh . (2 * x)) / (sinh (2 * x)) by SIN_COS2:def 4
.= (cosh . (2 * x)) / (sinh . (2 * x)) by SIN_COS2:def 2
.= ((2 * ((cosh . x) ^2 )) - 1) / (sinh . (2 * x)) by SIN_COS2:23
.= ((2 * ((cosh . x) ^2 )) - 1) / ((2 * (sinh . x)) * (cosh . x)) by SIN_COS2:23
.= (((2 * ((cosh . x) ^2 )) - 1) / ((sinh . x) ^2 )) / (((2 * (sinh . x)) * (cosh . x)) / ((sinh . x) ^2 )) by A2, XCMPLX_1:55
.= (((2 * ((cosh . x) ^2 )) - (((cosh . x) ^2 ) - ((sinh . x) ^2 ))) / ((sinh . x) ^2 )) / (((2 * (sinh . x)) * (cosh . x)) / ((sinh . x) ^2 )) by SIN_COS2:14
.= ((((2 - 1) * ((cosh . x) ^2 )) + ((sinh . x) ^2 )) / ((sinh . x) ^2 )) / (((2 * (sinh . x)) * (cosh . x)) / ((sinh . x) ^2 ))
.= ((((cosh . x) ^2 ) / ((sinh . x) ^2 )) + (((sinh . x) ^2 ) / ((sinh . x) ^2 ))) / (((2 * (sinh . x)) * (cosh . x)) / ((sinh . x) ^2 )) by XCMPLX_1:63
.= ((((cosh . x) / (sinh . x)) ^2 ) + (((sinh . x) ^2 ) / ((sinh . x) ^2 ))) / (((2 * (sinh . x)) * (cosh . x)) / ((sinh . x) ^2 )) by XCMPLX_1:77
.= ((((cosh . x) / (sinh . x)) ^2 ) + (((sinh . x) / (sinh . x)) ^2 )) / (((2 * (sinh . x)) * (cosh . x)) / ((sinh . x) ^2 )) by XCMPLX_1:77
.= ((((cosh . x) / (sinh . x)) ^2 ) + (1 ^2 )) / (((2 * (cosh . x)) * (sinh . x)) / ((sinh . x) * (sinh . x))) by A1, XCMPLX_1:60
.= ((((cosh . x) / (sinh . x)) ^2 ) + 1) / ((((2 * (cosh . x)) * (sinh . x)) / (sinh . x)) / (sinh . x)) by XCMPLX_1:79
.= ((((cosh . x) / (sinh . x)) ^2 ) + 1) / ((2 * (cosh . x)) / (sinh . x)) by A1, XCMPLX_1:90
.= ((((cosh . x) / (sinh . x)) ^2 ) + 1) / (2 * ((cosh . x) / (sinh . x))) by XCMPLX_1:75
.= ((((cosh x) / (sinh . x)) ^2 ) + 1) / (2 * ((cosh . x) / (sinh . x))) by SIN_COS2:def 4
.= ((((cosh x) / (sinh . x)) ^2 ) + 1) / (2 * ((cosh x) / (sinh . x))) by SIN_COS2:def 4
.= ((((cosh x) / (sinh x)) ^2 ) + 1) / (2 * ((cosh x) / (sinh . x))) by SIN_COS2:def 2
.= (((coth x) ^2 ) + 1) / (2 * ((cosh x) / (sinh x))) by SIN_COS2:def 2 ;
hence coth (2 * x) = (1 + ((coth x) ^2 )) / (2 * (coth x)) ; :: thesis: verum