let x be real number ; :: 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: sinh (- x) = sinh . (- x) by SIN_COS2:def 2
.= - (sinh . x) by SIN_COS2:19
.= - (sinh x) by SIN_COS2:def 2 ;
A2: cosh (- x) = cosh . (- x) by SIN_COS2:def 4
.= cosh . x by SIN_COS2:19
.= cosh x by SIN_COS2:def 4 ;
A3: tanh (- x) = tanh . (- x) by SIN_COS2:def 6
.= - (tanh . x) by SIN_COS2:19
.= - (tanh x) by SIN_COS2:def 6 ;
A4: coth (- x) = (cosh x) / (- (sinh x)) by A1, A2, SIN_COS5:def 1
.= - ((cosh x) / (sinh x)) by XCMPLX_1:189
.= - (coth x) by SIN_COS5:def 1 ;
A5: sech (- x) = 1 / (cosh x) by A2, SIN_COS5:def 2
.= sech x by SIN_COS5:def 2 ;
cosech (- x) = 1 / (- (sinh x)) by A1, SIN_COS5:def 3
.= - (1 / (sinh x)) by XCMPLX_1:189
.= - (cosech x) by SIN_COS5:def 3 ;
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 A1, A2, A3, A4, A5; :: thesis: verum