let x be Real; :: thesis: ( sinh x = ((exp_R x) - (exp_R (- x))) / 2 & cosh x = ((exp_R x) + (exp_R (- x))) / 2 & tanh x = ((exp_R x) - (exp_R (- x))) / ((exp_R x) + (exp_R (- x))) )
A1: sinh x = sinh . x by SIN_COS2:def 2
.= ((exp_R . x) - (exp_R . (- x))) / 2 by SIN_COS2:def 1
.= ((exp_R x) - (exp_R . (- x))) / 2 by SIN_COS:def 23
.= ((exp_R x) - (exp_R (- x))) / 2 by SIN_COS:def 23 ;
A2: cosh x = cosh . x by SIN_COS2:def 4
.= ((exp_R . x) + (exp_R . (- x))) / 2 by SIN_COS2:def 3
.= ((exp_R x) + (exp_R . (- x))) / 2 by SIN_COS:def 23
.= ((exp_R x) + (exp_R (- x))) / 2 by SIN_COS:def 23 ;
tanh x = tanh . x by SIN_COS2:def 6
.= (sinh . x) / (cosh . x) by SIN_COS2:17
.= (sinh x) / (cosh . x) by SIN_COS2:def 2
.= (((exp_R x) - (exp_R (- x))) / 2) / (((exp_R x) + (exp_R (- x))) / 2) by A1, A2, SIN_COS2:def 4 ;
hence ( sinh x = ((exp_R x) - (exp_R (- x))) / 2 & cosh x = ((exp_R x) + (exp_R (- x))) / 2 & tanh x = ((exp_R x) - (exp_R (- x))) / ((exp_R x) + (exp_R (- x))) ) by A1, A2, XCMPLX_1:55; :: thesis: verum