let x be Real; :: thesis: ( coth x = ((exp_R x) + (exp_R (- x))) / ((exp_R x) - (exp_R (- x))) & sech x = 2 / ((exp_R x) + (exp_R (- x))) & cosech x = 2 / ((exp_R x) - (exp_R (- x))) )
A1: sech x = 1 / (cosh . x) by SIN_COS2:def 4
.= 1 / (((exp_R . x) + (exp_R . (- x))) / 2) by SIN_COS2:def 3
.= (1 * 2) / ((((exp_R . x) + (exp_R . (- x))) / 2) * 2) by XCMPLX_1:91
.= 2 / ((exp_R . x) + (exp_R (- x))) by SIN_COS:def 23
.= 2 / ((exp_R x) + (exp_R (- x))) by SIN_COS:def 23 ;
A2: cosech x = 1 / (sinh . x) by SIN_COS2:def 2
.= 1 / (((exp_R . x) - (exp_R . (- x))) / 2) by SIN_COS2:def 1
.= (1 * 2) / ((((exp_R . x) - (exp_R . (- x))) / 2) * 2) by XCMPLX_1:91
.= 2 / ((exp_R . x) - (exp_R (- x))) by SIN_COS:def 23 ;
coth x = (cosh . x) / (sinh x) by SIN_COS2:def 4
.= (cosh . x) / (sinh . x) by SIN_COS2:def 2
.= (((exp_R . x) + (exp_R . (- x))) / 2) / (sinh . x) by SIN_COS2:def 3
.= (((exp_R . x) + (exp_R . (- x))) / 2) / (((exp_R . x) - (exp_R . (- x))) / 2) by SIN_COS2:def 1
.= ((((exp_R . x) + (exp_R . (- x))) / 2) * 2) / ((((exp_R . x) - (exp_R . (- x))) / 2) * 2) by XCMPLX_1:91
.= ((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))) by SIN_COS:def 23
.= ((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))) by SIN_COS:def 23 ;
hence ( coth x = ((exp_R x) + (exp_R (- x))) / ((exp_R x) - (exp_R (- x))) & sech x = 2 / ((exp_R x) + (exp_R (- x))) & cosech x = 2 / ((exp_R x) - (exp_R (- x))) ) by A1, A2, SIN_COS:def 23; :: thesis: verum