let x be Real; :: thesis: ( (exp_R x) - (exp_R (- x)) <> 0 implies (tanh x) * (coth x) = 1 )
assume A1: (exp_R x) - (exp_R (- x)) <> 0 ; :: thesis: (tanh x) * (coth x) = 1
exp_R x > 0 by SIN_COS:55;
then A2: (exp_R x) + (exp_R (- x)) > 0 + 0 by SIN_COS:55, XREAL_1:8;
(tanh x) * (coth x) = (tanh . x) * (coth x) by SIN_COS2:def 6
.= (((exp_R . x) - (exp_R . (- x))) / ((exp_R . x) + (exp_R . (- x)))) * (coth x) by SIN_COS2:def 5
.= (((exp_R . x) - (exp_R . (- x))) / ((exp_R . x) + (exp_R . (- x)))) * (((exp_R x) + (exp_R (- x))) / ((exp_R x) - (exp_R (- x)))) by Th36
.= (((exp_R . x) - (exp_R . (- x))) / ((exp_R . x) + (exp_R (- x)))) * (((exp_R x) + (exp_R (- x))) / ((exp_R x) - (exp_R (- x)))) by SIN_COS:def 23
.= (((exp_R x) - (exp_R . (- x))) / ((exp_R . x) + (exp_R (- x)))) * (((exp_R x) + (exp_R (- x))) / ((exp_R x) - (exp_R (- x)))) by SIN_COS:def 23
.= (((exp_R x) - (exp_R (- x))) / ((exp_R . x) + (exp_R (- x)))) * (((exp_R x) + (exp_R (- x))) / ((exp_R x) - (exp_R (- x)))) by SIN_COS:def 23
.= (((exp_R x) - (exp_R (- x))) / ((exp_R x) + (exp_R (- x)))) * (((exp_R x) + (exp_R (- x))) / ((exp_R x) - (exp_R (- x)))) by SIN_COS:def 23
.= ((((exp_R x) - (exp_R (- x))) / ((exp_R x) + (exp_R (- x)))) * ((exp_R x) + (exp_R (- x)))) / ((exp_R x) - (exp_R (- x))) by XCMPLX_1:74 ;
then (tanh x) * (coth x) = ((exp_R x) - (exp_R (- x))) / ((exp_R x) - (exp_R (- x))) by A2, XCMPLX_1:87
.= 1 by A1, XCMPLX_1:60 ;
hence (tanh x) * (coth x) = 1 ; :: thesis: verum