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:12;
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:62
.= ((((cosh . x) / (sinh . x)) ^2) + (((sinh . x) ^2) / ((sinh . x) ^2))) / (((2 * (sinh . x)) * (cosh . x)) / ((sinh . x) ^2)) by XCMPLX_1:76
.= ((((cosh . x) / (sinh . x)) ^2) + (((sinh . x) / (sinh . x)) ^2)) / (((2 * (sinh . x)) * (cosh . x)) / ((sinh . x) ^2)) by XCMPLX_1:76
.= ((((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:78
.= ((((cosh . x) / (sinh . x)) ^2) + 1) / ((2 * (cosh . x)) / (sinh . x)) by A1, XCMPLX_1:89
.= ((((cosh . x) / (sinh . x)) ^2) + 1) / (2 * ((cosh . x) / (sinh . x))) by XCMPLX_1:74
.= ((((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