let x be Real; :: thesis: ( sinh (- x) = - (sinh x) & cosh (- x) = cosh x & tanh (- x) = - (tanh x) & coth (- x) = - (coth x) & sech (- x) = sech x & cosech (- x) = - (cosech x) )
A1: tanh (- x) = tanh . (- x) by SIN_COS2:def 6
.= - (tanh . x) by SIN_COS2:19
.= - (tanh x) by SIN_COS2:def 6 ;
A2: sinh (- x) = sinh . (- x) by SIN_COS2:def 2
.= - (sinh . x) by SIN_COS2:19
.= - (sinh x) by SIN_COS2:def 2 ;
then A3: cosech (- x) = 1 / (- (sinh x)) by SIN_COS5:def 3
.= - (1 / (sinh x)) by XCMPLX_1:188
.= - (cosech x) by SIN_COS5:def 3 ;
A4: cosh (- x) = cosh . (- x) by SIN_COS2:def 4
.= cosh . x by SIN_COS2:19
.= cosh x by SIN_COS2:def 4 ;
then A5: sech (- x) = 1 / (cosh x) by SIN_COS5:def 2
.= sech x by SIN_COS5:def 2 ;
coth (- x) = (cosh x) / (- (sinh x)) by A2, A4, SIN_COS5:def 1
.= - ((cosh x) / (sinh x)) by XCMPLX_1:188
.= - (coth x) by SIN_COS5:def 1 ;
hence ( sinh (- x) = - (sinh x) & cosh (- x) = cosh x & tanh (- x) = - (tanh x) & coth (- x) = - (coth x) & sech (- x) = sech x & cosech (- x) = - (cosech x) ) by A2, A4, A1, A5, A3; :: thesis: verum