let x be Real; :: thesis:
A1: exp_R (x / 2) > 0 by SIN_COS:55;
A2: cosh (x / 2) <> 0 by Lm1;
A3: exp_R (- x) = exp_R ((- (x / 2)) + (- (x / 2)))
.= (exp_R (- (x / 2))) * (exp_R (- (x / 2))) by SIN_COS:50
.= ((exp_R (- (x / 2))) * (exp_R (x / 2))) * ((exp_R (- (x / 2))) / (exp_R (x / 2))) by A1, XCMPLX_1:90
.= (exp_R ((- (x / 2)) + (x / 2))) * ((exp_R (- (x / 2))) / (exp_R (x / 2))) by SIN_COS:50
.= ((((exp_R (x / 2)) + (exp_R (- (x / 2)))) / 2) - (((exp_R (x / 2)) - (exp_R (- (x / 2)))) / 2)) / (exp_R (x / 2)) by SIN_COS:51
.= ((((exp_R (x / 2)) + (exp_R (- (x / 2)))) / 2) - (sinh (x / 2))) / (exp_R (x / 2)) by Lm2
.= ((cosh (x / 2)) - (sinh (x / 2))) / ((((exp_R (x / 2)) + (exp_R (- (x / 2)))) / 2) + (((exp_R (x / 2)) / 2) - ((exp_R (- (x / 2))) / 2))) by Lm2
.= ((cosh (x / 2)) - (sinh (x / 2))) / ((cosh (x / 2)) + (((exp_R (x / 2)) - (exp_R (- (x / 2)))) / 2)) by Lm2
.= ((cosh (x / 2)) - (sinh (x / 2))) / ((cosh (x / 2)) + (sinh (x / 2))) by Lm2 ;
then A4: exp_R (- x) = (((cosh (x / 2)) - (sinh (x / 2))) / (cosh (x / 2))) / (((cosh (x / 2)) + (sinh (x / 2))) / (cosh (x / 2))) by A2, XCMPLX_1:55
.= (((cosh (x / 2)) / (cosh (x / 2))) - ((sinh (x / 2)) / (cosh (x / 2)))) / (((cosh (x / 2)) + (sinh (x / 2))) / (cosh (x / 2))) by XCMPLX_1:120
.= (1 - ((sinh (x / 2)) / (cosh (x / 2)))) / (((cosh (x / 2)) + (sinh (x / 2))) / (cosh (x / 2))) by A2, XCMPLX_1:60
.= (1 - (tanh (x / 2))) / (((cosh (x / 2)) + (sinh (x / 2))) / (cosh (x / 2))) by Th1
.= (1 - (tanh (x / 2))) / (((cosh (x / 2)) / (cosh (x / 2))) + ((sinh (x / 2)) / (cosh (x / 2)))) by XCMPLX_1:62
.= (1 - (tanh (x / 2))) / (1 + ((sinh (x / 2)) / (cosh (x / 2)))) by A2, XCMPLX_1:60
.= (1 - (tanh (x / 2))) / (1 + (tanh (x / 2))) by Th1 ;
A5: exp_R (- x) = (((exp_R x) + (exp_R (- x))) / 2) - (((exp_R x) - (exp_R (- x))) / 2)
.= (cosh x) - (((exp_R x) - (exp_R (- x))) / 2) by Lm2
.= (cosh x) - (sinh x) by Lm2 ;
A6: exp_R x = (((exp_R x) + (exp_R (- x))) / 2) + (((exp_R x) - (exp_R (- x))) / 2)
.= (cosh x) + (((exp_R x) - (exp_R (- x))) / 2) by Lm2
.= (cosh x) + (sinh x) by Lm2 ;
A7: exp_R (- (x / 2)) > 0 by SIN_COS:55;
A8: exp_R x = exp_R ((x / 2) + (x / 2))
.= (exp_R (x / 2)) * (exp_R (x / 2)) by SIN_COS:50
.= ((exp_R (x / 2)) * (exp_R (- (x / 2)))) * ((exp_R (x / 2)) / (exp_R (- (x / 2)))) by A7, XCMPLX_1:90
.= (exp_R ((x / 2) + (- (x / 2)))) * ((exp_R (x / 2)) / (exp_R (- (x / 2)))) by SIN_COS:50
.= ((((exp_R (x / 2)) + (exp_R (- (x / 2)))) / 2) + (((exp_R (x / 2)) - (exp_R (- (x / 2)))) / 2)) / (exp_R (- (x / 2))) by SIN_COS:51
.= ((cosh (x / 2)) + (((exp_R (x / 2)) - (exp_R (- (x / 2)))) / 2)) / (exp_R (- (x / 2))) by Lm2
.= ((cosh (x / 2)) + (sinh (x / 2))) / ((((exp_R (- (x / 2))) + (exp_R (x / 2))) / 2) - (((exp_R (x / 2)) - (exp_R (- (x / 2)))) / 2)) by Lm2
.= ((cosh (x / 2)) + (sinh (x / 2))) / ((((exp_R (x / 2)) + (exp_R (- (x / 2)))) / 2) - (sinh (x / 2))) by Lm2
.= ((cosh (x / 2)) + (sinh (x / 2))) / ((cosh (x / 2)) - (sinh (x / 2))) by Lm2 ;
then exp_R x = (((cosh (x / 2)) + (sinh (x / 2))) / (cosh (x / 2))) / (((cosh (x / 2)) - (sinh (x / 2))) / (cosh (x / 2))) by A2, XCMPLX_1:55
.= (((cosh (x / 2)) / (cosh (x / 2))) + ((sinh (x / 2)) / (cosh (x / 2)))) / (((cosh (x / 2)) - (sinh (x / 2))) / (cosh (x / 2))) by XCMPLX_1:62
.= (1 + ((sinh (x / 2)) / (cosh (x / 2)))) / (((cosh (x / 2)) - (sinh (x / 2))) / (cosh (x / 2))) by A2, XCMPLX_1:60
.= (1 + (tanh (x / 2))) / (((cosh (x / 2)) - (sinh (x / 2))) / (cosh (x / 2))) by Th1
.= (1 + (tanh (x / 2))) / (((cosh (x / 2)) / (cosh (x / 2))) - ((sinh (x / 2)) / (cosh (x / 2)))) by XCMPLX_1:120
.= (1 + (tanh (x / 2))) / (1 - ((sinh (x / 2)) / (cosh (x / 2)))) by A2, XCMPLX_1:60
.= (1 + (tanh (x / 2))) / (1 - (tanh (x / 2))) by Th1 ;
hence ( exp_R x = (cosh x) + (sinh x) & exp_R (- x) = (cosh x) - (sinh x) & exp_R x = ((cosh (x / 2)) + (sinh (x / 2))) / ((cosh (x / 2)) - (sinh (x / 2))) & exp_R (- x) = ((cosh (x / 2)) - (sinh (x / 2))) / ((cosh (x / 2)) + (sinh (x / 2))) & exp_R x = (1 + (tanh (x / 2))) / (1 - (tanh (x / 2))) & exp_R (- x) = (1 - (tanh (x / 2))) / (1 + (tanh (x / 2))) ) by A6, A5, A8, A3, A4; :: thesis: