:: SIN_COS8 semantic presentation begin Lm1: for x being real number holds ( cosh x >= 1 & cosh 0 = 1 & sinh 0 = 0 ) proof let x be real number ; ::_thesis: ( cosh x >= 1 & cosh 0 = 1 & sinh 0 = 0 ) cosh . x >= 1 by SIN_COS2:37; hence ( cosh x >= 1 & cosh 0 = 1 & sinh 0 = 0 ) by SIN_COS2:15, SIN_COS2:16, SIN_COS2:def_2, SIN_COS2:def_4; ::_thesis: verum end; Lm2: for x being real number holds ( 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))) ) proof let x be real number ; ::_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 end; Lm3: for x being real number holds ( ((cosh x) ^2) - ((sinh x) ^2) = 1 & ((cosh x) * (cosh x)) - ((sinh x) * (sinh x)) = 1 ) proof let x be real number ; ::_thesis: ( ((cosh x) ^2) - ((sinh x) ^2) = 1 & ((cosh x) * (cosh x)) - ((sinh x) * (sinh x)) = 1 ) ((cosh x) ^2) - ((sinh x) ^2) = ((cosh x) ^2) - ((sinh . x) ^2) by SIN_COS2:def_2 .= ((cosh . x) ^2) - ((sinh . x) ^2) by SIN_COS2:def_4 .= 1 by SIN_COS2:14 ; hence ( ((cosh x) ^2) - ((sinh x) ^2) = 1 & ((cosh x) * (cosh x)) - ((sinh x) * (sinh x)) = 1 ) ; ::_thesis: verum end; theorem Th1: :: SIN_COS8:1 for x being real number holds ( tanh x = (sinh x) / (cosh x) & tanh 0 = 0 ) proof let x be real number ; ::_thesis: ( tanh x = (sinh x) / (cosh x) & tanh 0 = 0 ) A1: tanh 0 = tanh . 0 by SIN_COS2:def_6 .= (sinh . 0) / (cosh . 0) by SIN_COS2:17 .= 0 by SIN_COS2:16 ; 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 .= (sinh x) / (cosh x) by SIN_COS2:def_4 ; hence ( tanh x = (sinh x) / (cosh x) & tanh 0 = 0 ) by A1; ::_thesis: verum end; Lm4: for x being real number st x <> 0 holds ( sinh x <> 0 & tanh x <> 0 ) proof let x be real number ; ::_thesis: ( x <> 0 implies ( sinh x <> 0 & tanh x <> 0 ) ) A1: exp_R x > 0 by SIN_COS:55; assume x <> 0 ; ::_thesis: ( sinh x <> 0 & tanh x <> 0 ) then 1 / (exp_R x) <> exp_R x by A1, SIN_COS7:29, XCMPLX_1:199; then ((exp_R x) - (exp_R (- x))) / 2 <> 0 by TAYLOR_1:4; then A2: sinh x <> 0 by Lm2; cosh x <> 0 by Lm1; then (sinh x) / (cosh x) <> 0 by A2, XCMPLX_1:50; hence ( sinh x <> 0 & tanh x <> 0 ) by Th1; ::_thesis: verum end; Lm5: for y, z being real number st y - z <> 0 holds sinh ((y / 2) - (z / 2)) <> 0 proof let y, z be real number ; ::_thesis: ( y - z <> 0 implies sinh ((y / 2) - (z / 2)) <> 0 ) assume y - z <> 0 ; ::_thesis: sinh ((y / 2) - (z / 2)) <> 0 then (y - z) / 2 <> 0 ; hence sinh ((y / 2) - (z / 2)) <> 0 by Lm4; ::_thesis: verum end; Lm6: for y, z being real number st y + z <> 0 holds sinh ((y / 2) + (z / 2)) <> 0 proof let y, z be real number ; ::_thesis: ( y + z <> 0 implies sinh ((y / 2) + (z / 2)) <> 0 ) assume y + z <> 0 ; ::_thesis: sinh ((y / 2) + (z / 2)) <> 0 then (y + z) / 2 <> 0 ; hence sinh ((y / 2) + (z / 2)) <> 0 by Lm4; ::_thesis: verum end; Lm7: for x being real number holds ( (sinh x) ^2 = (1 / 2) * ((cosh (2 * x)) - 1) & (cosh x) ^2 = (1 / 2) * ((cosh (2 * x)) + 1) ) proof let x be real number ; ::_thesis: ( (sinh x) ^2 = (1 / 2) * ((cosh (2 * x)) - 1) & (cosh x) ^2 = (1 / 2) * ((cosh (2 * x)) + 1) ) A1: (cosh x) ^2 = (cosh . x) ^2 by SIN_COS2:def_4 .= (1 / 2) * ((cosh . (2 * x)) + 1) by SIN_COS2:18 ; (sinh x) ^2 = (sinh . x) ^2 by SIN_COS2:def_2 .= (1 / 2) * ((cosh . (2 * x)) - 1) by SIN_COS2:18 .= (1 / 2) * ((cosh (2 * x)) - 1) by SIN_COS2:def_4 ; hence ( (sinh x) ^2 = (1 / 2) * ((cosh (2 * x)) - 1) & (cosh x) ^2 = (1 / 2) * ((cosh (2 * x)) + 1) ) by A1, SIN_COS2:def_4; ::_thesis: verum end; Lm8: for x being real number holds ( sinh (- x) = - (sinh x) & cosh (- x) = cosh x & tanh (- x) = - (tanh x) & coth (- x) = - (coth x) & sech (- x) = sech x & cosech (- x) = - (cosech x) ) proof 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: 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 end; theorem Th2: :: SIN_COS8:2 for x being real number holds ( sinh x = 1 / (cosech x) & cosh x = 1 / (sech x) & tanh x = 1 / (coth x) ) proof let x be real number ; ::_thesis: ( sinh x = 1 / (cosech x) & cosh x = 1 / (sech x) & tanh x = 1 / (coth x) ) A1: sinh x = 1 / (1 / (sinh x)) by XCMPLX_1:56 .= 1 / (cosech x) by SIN_COS5:def_3 ; A2: cosh x = 1 / (1 / (cosh x)) by XCMPLX_1:56 .= 1 / (sech x) by SIN_COS5:def_2 ; tanh x = (sinh x) / (cosh x) by Th1 .= 1 / ((cosh x) / (sinh x)) by XCMPLX_1:57 .= 1 / (coth x) by SIN_COS5:def_1 ; hence ( sinh x = 1 / (cosech x) & cosh x = 1 / (sech x) & tanh x = 1 / (coth x) ) by A1, A2; ::_thesis: verum end; Lm9: for x being real number holds (exp_R x) + (exp_R (- x)) >= 2 proof let x be real number ; ::_thesis: (exp_R x) + (exp_R (- x)) >= 2 exp_R . x >= 0 by SIN_COS:54; then A1: exp_R x >= 0 by SIN_COS:def_23; exp_R . (- x) >= 0 by SIN_COS:54; then A2: exp_R (- x) >= 0 by SIN_COS:def_23; 2 * (sqrt ((exp_R x) * (exp_R (- x)))) = 2 * (sqrt ((exp_R x) * (exp_R . (- x)))) by SIN_COS:def_23 .= 2 * (sqrt ((exp_R . x) * (exp_R . (- x)))) by SIN_COS:def_23 .= 2 * (sqrt (exp_R . (x + (- x)))) by SIN_COS2:12 .= 2 * 1 by SIN_COS:51, SIN_COS:def_23, SQUARE_1:18 ; hence (exp_R x) + (exp_R (- x)) >= 2 by A1, A2, SIN_COS2:1; ::_thesis: verum end; theorem Th3: :: SIN_COS8:3 for x being real number holds ( sech x <= 1 & 0 < sech x & sech 0 = 1 ) proof let x be real number ; ::_thesis: ( sech x <= 1 & 0 < sech x & sech 0 = 1 ) A1: 2 / 2 >= 2 / ((exp_R x) + (exp_R (- x))) by Lm9, XREAL_1:183; 0 < cosh . x by SIN_COS2:15; then 0 < cosh x by SIN_COS2:def_4; then A2: 0 < 1 / (cosh x) by XREAL_1:139; sech 0 = 1 / 1 by Lm1, SIN_COS5:def_2 .= 1 ; hence ( sech x <= 1 & 0 < sech x & sech 0 = 1 ) by A2, A1, SIN_COS5:36, SIN_COS5:def_2; ::_thesis: verum end; theorem :: SIN_COS8:4 for x being real number st x >= 0 holds tanh x >= 0 proof let x be real number ; ::_thesis: ( x >= 0 implies tanh x >= 0 ) A1: cosh x >= 1 by Lm1; assume A2: x >= 0 ; ::_thesis: tanh x >= 0 percases ( x > 0 or x = 0 ) by A2; suppose x > 0 ; ::_thesis: tanh x >= 0 then sinh x >= 0 by SIN_COS5:46; then (sinh x) / (cosh x) >= 0 by A1; hence tanh x >= 0 by Th1; ::_thesis: verum end; suppose x = 0 ; ::_thesis: tanh x >= 0 hence tanh x >= 0 by Th1; ::_thesis: verum end; end; end; theorem :: SIN_COS8:5 for x being real number holds ( cosh x = 1 / (sqrt (1 - ((tanh x) ^2))) & sinh x = (tanh x) / (sqrt (1 - ((tanh x) ^2))) ) proof let x be real number ; ::_thesis: ( cosh x = 1 / (sqrt (1 - ((tanh x) ^2))) & sinh x = (tanh x) / (sqrt (1 - ((tanh x) ^2))) ) A1: (sech x) ^2 = (((sech x) ^2) + ((tanh x) ^2)) - ((tanh x) ^2) .= 1 - ((tanh x) ^2) by SIN_COS5:38 ; A2: sech x > 0 by Th3; A3: cosh x = 1 / (1 / (cosh x)) by XCMPLX_1:56 .= 1 / (sech x) by SIN_COS5:def_2 .= 1 / (sqrt (1 - ((tanh x) ^2))) by A1, A2, SQUARE_1:22 ; cosh x <> 0 by Lm1; then sinh x = ((sinh x) / (cosh x)) * (cosh x) by XCMPLX_1:87 .= (tanh x) * (1 / (sqrt (1 - ((tanh x) ^2)))) by A3, Th1 .= (tanh x) / (sqrt (1 - ((tanh x) ^2))) by XCMPLX_1:99 ; hence ( cosh x = 1 / (sqrt (1 - ((tanh x) ^2))) & sinh x = (tanh x) / (sqrt (1 - ((tanh x) ^2))) ) by A3; ::_thesis: verum end; theorem :: SIN_COS8:6 for x being real number for n being Element of NAT holds ( ((cosh x) + (sinh x)) |^ n = (cosh (n * x)) + (sinh (n * x)) & ((cosh x) - (sinh x)) |^ n = (cosh (n * x)) - (sinh (n * x)) ) proof let x be real number ; ::_thesis: for n being Element of NAT holds ( ((cosh x) + (sinh x)) |^ n = (cosh (n * x)) + (sinh (n * x)) & ((cosh x) - (sinh x)) |^ n = (cosh (n * x)) - (sinh (n * x)) ) let n be Element of NAT ; ::_thesis: ( ((cosh x) + (sinh x)) |^ n = (cosh (n * x)) + (sinh (n * x)) & ((cosh x) - (sinh x)) |^ n = (cosh (n * x)) - (sinh (n * x)) ) A1: ((cosh x) + (sinh x)) |^ n = ((cosh . x) + (sinh x)) |^ n by SIN_COS2:def_4 .= ((cosh . x) + (sinh . x)) |^ n by SIN_COS2:def_2 .= (cosh . (n * x)) + (sinh . (n * x)) by SIN_COS2:29 .= (cosh (n * x)) + (sinh . (n * x)) by SIN_COS2:def_4 .= (cosh (n * x)) + (sinh (n * x)) by SIN_COS2:def_2 ; ((cosh x) - (sinh x)) |^ n = ((cosh x) + (- (sinh x))) |^ n .= ((cosh x) + (sinh (- x))) |^ n by Lm8 .= ((cosh . x) + (sinh (- x))) |^ n by SIN_COS2:def_4 .= ((cosh . x) + (sinh . (- x))) |^ n by SIN_COS2:def_2 .= ((cosh . (- x)) + (sinh . (- x))) |^ n by SIN_COS2:19 .= (cosh . (n * (- x))) + (sinh . (- (n * x))) by SIN_COS2:29 .= (cosh . (n * x)) + (sinh . (- (n * x))) by SIN_COS2:19 .= (cosh . (n * x)) + (- (sinh . (n * x))) by SIN_COS2:19 .= (cosh . (n * x)) - (sinh . (n * x)) .= (cosh (n * x)) - (sinh . (n * x)) by SIN_COS2:def_4 .= (cosh (n * x)) - (sinh (n * x)) by SIN_COS2:def_2 ; hence ( ((cosh x) + (sinh x)) |^ n = (cosh (n * x)) + (sinh (n * x)) & ((cosh x) - (sinh x)) |^ n = (cosh (n * x)) - (sinh (n * x)) ) by A1; ::_thesis: verum end; theorem Th7: :: SIN_COS8:7 for x being real number holds ( 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))) ) proof let x be real number ; ::_thesis: ( 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))) ) 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: verum end; theorem :: SIN_COS8:8 for x being real number st x <> 0 holds ( exp_R x = ((coth (x / 2)) + 1) / ((coth (x / 2)) - 1) & exp_R (- x) = ((coth (x / 2)) - 1) / ((coth (x / 2)) + 1) ) proof let x be real number ; ::_thesis: ( x <> 0 implies ( exp_R x = ((coth (x / 2)) + 1) / ((coth (x / 2)) - 1) & exp_R (- x) = ((coth (x / 2)) - 1) / ((coth (x / 2)) + 1) ) ) assume x <> 0 ; ::_thesis: ( exp_R x = ((coth (x / 2)) + 1) / ((coth (x / 2)) - 1) & exp_R (- x) = ((coth (x / 2)) - 1) / ((coth (x / 2)) + 1) ) then A1: x / 2 <> 0 ; A2: (coth (x / 2)) - 1 = (1 / (1 / (coth (x / 2)))) - 1 by XCMPLX_1:56 .= (1 / (tanh (x / 2))) - 1 by Th2 .= (1 / (tanh (x / 2))) - ((tanh (x / 2)) / (tanh (x / 2))) by A1, Lm4, XCMPLX_1:60 .= (1 - (tanh (x / 2))) / (tanh (x / 2)) by XCMPLX_1:120 ; A3: (coth (x / 2)) + 1 = (1 / (1 / (coth (x / 2)))) + 1 by XCMPLX_1:56 .= (1 / (tanh (x / 2))) + 1 by Th2 .= (1 / (tanh (x / 2))) + ((tanh (x / 2)) / (tanh (x / 2))) by A1, Lm4, XCMPLX_1:60 .= (1 + (tanh (x / 2))) / (tanh (x / 2)) by XCMPLX_1:62 ; A4: exp_R (- x) = (1 - (tanh (x / 2))) / (1 + (tanh (x / 2))) by Th7 .= ((coth (x / 2)) - 1) / ((coth (x / 2)) + 1) by A1, A3, A2, Lm4, XCMPLX_1:55 ; exp_R x = (1 + (tanh (x / 2))) / (1 - (tanh (x / 2))) by Th7 .= ((coth (x / 2)) + 1) / ((coth (x / 2)) - 1) by A1, A3, A2, Lm4, XCMPLX_1:55 ; hence ( exp_R x = ((coth (x / 2)) + 1) / ((coth (x / 2)) - 1) & exp_R (- x) = ((coth (x / 2)) - 1) / ((coth (x / 2)) + 1) ) by A4; ::_thesis: verum end; theorem :: SIN_COS8:9 for x being real number holds ((cosh x) + (sinh x)) / ((cosh x) - (sinh x)) = (1 + (tanh x)) / (1 - (tanh x)) proof let x be real number ; ::_thesis: ((cosh x) + (sinh x)) / ((cosh x) - (sinh x)) = (1 + (tanh x)) / (1 - (tanh x)) A1: exp_R (2 * x) = (1 + (tanh x)) / (1 - (tanh ((2 * x) / 2))) by Th7 .= (1 + (tanh x)) / (1 - (tanh x)) ; exp_R (2 * x) = ((cosh ((2 * x) / 2)) + (sinh ((2 * x) / 2))) / ((cosh ((2 * x) / 2)) - (sinh ((2 * x) / 2))) by Th7 .= ((cosh x) + (sinh x)) / ((cosh x) - (sinh x)) ; hence ((cosh x) + (sinh x)) / ((cosh x) - (sinh x)) = (1 + (tanh x)) / (1 - (tanh x)) by A1; ::_thesis: verum end; Lm10: for y, z being real number holds ( cosh (y + z) = ((cosh y) * (cosh z)) + ((sinh y) * (sinh z)) & cosh (y - z) = ((cosh y) * (cosh z)) - ((sinh y) * (sinh z)) & sinh (y + z) = ((sinh y) * (cosh z)) + ((cosh y) * (sinh z)) & sinh (y - z) = ((sinh y) * (cosh z)) - ((cosh y) * (sinh z)) & tanh (y + z) = ((tanh y) + (tanh z)) / (1 + ((tanh y) * (tanh z))) & tanh (y - z) = ((tanh y) - (tanh z)) / (1 - ((tanh y) * (tanh z))) ) proof let y, z be real number ; ::_thesis: ( cosh (y + z) = ((cosh y) * (cosh z)) + ((sinh y) * (sinh z)) & cosh (y - z) = ((cosh y) * (cosh z)) - ((sinh y) * (sinh z)) & sinh (y + z) = ((sinh y) * (cosh z)) + ((cosh y) * (sinh z)) & sinh (y - z) = ((sinh y) * (cosh z)) - ((cosh y) * (sinh z)) & tanh (y + z) = ((tanh y) + (tanh z)) / (1 + ((tanh y) * (tanh z))) & tanh (y - z) = ((tanh y) - (tanh z)) / (1 - ((tanh y) * (tanh z))) ) A1: ((cosh y) * (cosh z)) - ((sinh y) * (sinh z)) = ((cosh . y) * (cosh z)) - ((sinh y) * (sinh z)) by SIN_COS2:def_4 .= ((cosh . y) * (cosh . z)) - ((sinh y) * (sinh z)) by SIN_COS2:def_4 .= ((cosh . y) * (cosh . z)) - ((sinh . y) * (sinh z)) by SIN_COS2:def_2 .= ((cosh . y) * (cosh . z)) - ((sinh . y) * (sinh . z)) by SIN_COS2:def_2 .= cosh . (y - z) by SIN_COS2:20 .= cosh (y - z) by SIN_COS2:def_4 ; A2: ((sinh y) * (cosh z)) + ((cosh y) * (sinh z)) = ((sinh . y) * (cosh z)) + ((cosh y) * (sinh z)) by SIN_COS2:def_2 .= ((sinh . y) * (cosh z)) + ((cosh y) * (sinh . z)) by SIN_COS2:def_2 .= ((sinh . y) * (cosh . z)) + ((cosh y) * (sinh . z)) by SIN_COS2:def_4 .= ((sinh . y) * (cosh . z)) + ((cosh . y) * (sinh . z)) by SIN_COS2:def_4 .= sinh . (y + z) by SIN_COS2:21 .= sinh (y + z) by SIN_COS2:def_2 ; A3: tanh (y - z) = tanh . (y - z) by SIN_COS2:def_6 .= ((tanh . y) - (tanh . z)) / (1 - ((tanh . y) * (tanh . z))) by SIN_COS2:22 .= ((tanh y) - (tanh . z)) / (1 - ((tanh . y) * (tanh . z))) by SIN_COS2:def_6 .= ((tanh y) - (tanh z)) / (1 - ((tanh . y) * (tanh . z))) by SIN_COS2:def_6 .= ((tanh y) - (tanh z)) / (1 - ((tanh y) * (tanh . z))) by SIN_COS2:def_6 .= ((tanh y) - (tanh z)) / (1 - ((tanh y) * (tanh z))) by SIN_COS2:def_6 ; A4: tanh (y + z) = tanh . (y + z) by SIN_COS2:def_6 .= ((tanh . y) + (tanh . z)) / (1 + ((tanh . y) * (tanh . z))) by SIN_COS2:22 .= ((tanh y) + (tanh . z)) / (1 + ((tanh . y) * (tanh . z))) by SIN_COS2:def_6 .= ((tanh y) + (tanh z)) / (1 + ((tanh . y) * (tanh . z))) by SIN_COS2:def_6 .= ((tanh y) + (tanh z)) / (1 + ((tanh y) * (tanh . z))) by SIN_COS2:def_6 .= ((tanh y) + (tanh z)) / (1 + ((tanh y) * (tanh z))) by SIN_COS2:def_6 ; A5: ((sinh y) * (cosh z)) - ((cosh y) * (sinh z)) = ((sinh . y) * (cosh z)) - ((cosh y) * (sinh z)) by SIN_COS2:def_2 .= ((sinh . y) * (cosh z)) - ((cosh y) * (sinh . z)) by SIN_COS2:def_2 .= ((sinh . y) * (cosh . z)) - ((cosh y) * (sinh . z)) by SIN_COS2:def_4 .= ((sinh . y) * (cosh . z)) - ((cosh . y) * (sinh . z)) by SIN_COS2:def_4 .= sinh . (y - z) by SIN_COS2:21 .= sinh (y - z) by SIN_COS2:def_2 ; ((cosh y) * (cosh z)) + ((sinh y) * (sinh z)) = ((cosh . y) * (cosh z)) + ((sinh y) * (sinh z)) by SIN_COS2:def_4 .= ((cosh . y) * (cosh . z)) + ((sinh y) * (sinh z)) by SIN_COS2:def_4 .= ((cosh . y) * (cosh . z)) + ((sinh . y) * (sinh z)) by SIN_COS2:def_2 .= ((cosh . y) * (cosh . z)) + ((sinh . y) * (sinh . z)) by SIN_COS2:def_2 .= cosh . (y + z) by SIN_COS2:20 .= cosh (y + z) by SIN_COS2:def_4 ; hence ( cosh (y + z) = ((cosh y) * (cosh z)) + ((sinh y) * (sinh z)) & cosh (y - z) = ((cosh y) * (cosh z)) - ((sinh y) * (sinh z)) & sinh (y + z) = ((sinh y) * (cosh z)) + ((cosh y) * (sinh z)) & sinh (y - z) = ((sinh y) * (cosh z)) - ((cosh y) * (sinh z)) & tanh (y + z) = ((tanh y) + (tanh z)) / (1 + ((tanh y) * (tanh z))) & tanh (y - z) = ((tanh y) - (tanh z)) / (1 - ((tanh y) * (tanh z))) ) by A1, A2, A5, A4, A3; ::_thesis: verum end; theorem :: SIN_COS8:10 for y, z being real number st y <> 0 holds ( (coth y) + (tanh z) = (cosh (y + z)) / ((sinh y) * (cosh z)) & (coth y) - (tanh z) = (cosh (y - z)) / ((sinh y) * (cosh z)) ) proof let y, z be real number ; ::_thesis: ( y <> 0 implies ( (coth y) + (tanh z) = (cosh (y + z)) / ((sinh y) * (cosh z)) & (coth y) - (tanh z) = (cosh (y - z)) / ((sinh y) * (cosh z)) ) ) assume A1: y <> 0 ; ::_thesis: ( (coth y) + (tanh z) = (cosh (y + z)) / ((sinh y) * (cosh z)) & (coth y) - (tanh z) = (cosh (y - z)) / ((sinh y) * (cosh z)) ) A2: cosh z <> 0 by Lm1; A3: (coth y) - (tanh z) = ((cosh y) / (sinh y)) - (tanh z) by SIN_COS5:def_1 .= (((cosh y) * (cosh z)) / ((sinh y) * (cosh z))) - (tanh z) by A2, XCMPLX_1:91 .= (((cosh y) * (cosh z)) / ((sinh y) * (cosh z))) - ((sinh z) / (cosh z)) by Th1 .= (((cosh y) * (cosh z)) / ((sinh y) * (cosh z))) - (((sinh y) * (sinh z)) / ((sinh y) * (cosh z))) by A1, Lm4, XCMPLX_1:91 .= (((cosh y) * (cosh z)) - ((sinh y) * (sinh z))) / ((sinh y) * (cosh z)) by XCMPLX_1:120 .= (cosh (y - z)) / ((sinh y) * (cosh z)) by Lm10 ; (coth y) + (tanh z) = ((cosh y) / (sinh y)) + (tanh z) by SIN_COS5:def_1 .= (((cosh y) * (cosh z)) / ((sinh y) * (cosh z))) + (tanh z) by A2, XCMPLX_1:91 .= (((cosh y) * (cosh z)) / ((sinh y) * (cosh z))) + ((sinh z) / (cosh z)) by Th1 .= (((cosh y) * (cosh z)) / ((sinh y) * (cosh z))) + (((sinh y) * (sinh z)) / ((sinh y) * (cosh z))) by A1, Lm4, XCMPLX_1:91 .= (((cosh y) * (cosh z)) + ((sinh y) * (sinh z))) / ((sinh y) * (cosh z)) by XCMPLX_1:62 .= (cosh (y + z)) / ((sinh y) * (cosh z)) by Lm10 ; hence ( (coth y) + (tanh z) = (cosh (y + z)) / ((sinh y) * (cosh z)) & (coth y) - (tanh z) = (cosh (y - z)) / ((sinh y) * (cosh z)) ) by A3; ::_thesis: verum end; theorem Th11: :: SIN_COS8:11 for y, z being real number holds ( (sinh y) * (sinh z) = (1 / 2) * ((cosh (y + z)) - (cosh (y - z))) & (sinh y) * (cosh z) = (1 / 2) * ((sinh (y + z)) + (sinh (y - z))) & (cosh y) * (sinh z) = (1 / 2) * ((sinh (y + z)) - (sinh (y - z))) & (cosh y) * (cosh z) = (1 / 2) * ((cosh (y + z)) + (cosh (y - z))) ) proof let y, z be real number ; ::_thesis: ( (sinh y) * (sinh z) = (1 / 2) * ((cosh (y + z)) - (cosh (y - z))) & (sinh y) * (cosh z) = (1 / 2) * ((sinh (y + z)) + (sinh (y - z))) & (cosh y) * (sinh z) = (1 / 2) * ((sinh (y + z)) - (sinh (y - z))) & (cosh y) * (cosh z) = (1 / 2) * ((cosh (y + z)) + (cosh (y - z))) ) A1: (sinh y) * (cosh z) = (1 / 2) * ((((sinh y) * (cosh z)) + ((cosh y) * (sinh z))) + (((sinh y) * (cosh z)) - ((cosh y) * (sinh z)))) .= (1 / 2) * ((sinh (y + z)) + (((sinh y) * (cosh z)) - ((cosh y) * (sinh z)))) by Lm10 .= (1 / 2) * ((sinh (y + z)) + (sinh (y - z))) by Lm10 ; A2: (cosh y) * (sinh z) = (1 / 2) * ((((sinh y) * (cosh z)) + ((cosh y) * (sinh z))) - (((sinh y) * (cosh z)) - ((cosh y) * (sinh z)))) .= (1 / 2) * ((sinh (y + z)) - (((sinh y) * (cosh z)) - ((cosh y) * (sinh z)))) by Lm10 .= (1 / 2) * ((sinh (y + z)) - (sinh (y - z))) by Lm10 ; A3: (cosh y) * (cosh z) = (1 / 2) * ((((cosh y) * (cosh z)) + ((sinh y) * (sinh z))) + (((cosh y) * (cosh z)) - ((sinh y) * (sinh z)))) .= (1 / 2) * ((cosh (y + z)) + (((cosh y) * (cosh z)) - ((sinh y) * (sinh z)))) by Lm10 .= (1 / 2) * ((cosh (y + z)) + (cosh (y - z))) by Lm10 ; (sinh y) * (sinh z) = (1 / 2) * ((((cosh y) * (cosh z)) + ((sinh y) * (sinh z))) - (((cosh y) * (cosh z)) - ((sinh y) * (sinh z)))) .= (1 / 2) * ((cosh (y + z)) - (((cosh y) * (cosh z)) - ((sinh y) * (sinh z)))) by Lm10 .= (1 / 2) * ((cosh (y + z)) - (cosh (y - z))) by Lm10 ; hence ( (sinh y) * (sinh z) = (1 / 2) * ((cosh (y + z)) - (cosh (y - z))) & (sinh y) * (cosh z) = (1 / 2) * ((sinh (y + z)) + (sinh (y - z))) & (cosh y) * (sinh z) = (1 / 2) * ((sinh (y + z)) - (sinh (y - z))) & (cosh y) * (cosh z) = (1 / 2) * ((cosh (y + z)) + (cosh (y - z))) ) by A1, A2, A3; ::_thesis: verum end; theorem :: SIN_COS8:12 for y, z being real number holds ((sinh y) ^2) - ((cosh z) ^2) = ((sinh (y + z)) * (sinh (y - z))) - 1 proof let y, z be real number ; ::_thesis: ((sinh y) ^2) - ((cosh z) ^2) = ((sinh (y + z)) * (sinh (y - z))) - 1 ((sinh y) ^2) - ((cosh z) ^2) = ((sinh y) ^2) - (((cosh z) ^2) * 1) .= ((sinh y) ^2) - (((cosh z) ^2) * (((cosh y) ^2) - ((sinh y) ^2))) by Lm3 .= ((sinh y) ^2) + ((((cosh z) ^2) * ((sinh y) ^2)) - (((cosh y) ^2) * ((((cosh z) ^2) - ((sinh z) ^2)) + ((sinh z) ^2)))) .= ((sinh y) ^2) + ((((cosh z) ^2) * ((sinh y) ^2)) - (((cosh y) ^2) * (1 + ((sinh z) ^2)))) by Lm3 .= ((sinh y) ^2) + (((((sinh y) * (cosh z)) + ((cosh y) * (sinh z))) * (((sinh y) * (cosh z)) - ((cosh y) * (sinh z)))) - ((cosh y) ^2)) .= ((sinh y) ^2) + (((sinh (y + z)) * (((sinh y) * (cosh z)) - ((cosh y) * (sinh z)))) - ((cosh y) ^2)) by Lm10 .= (((sinh (y + z)) * (sinh (y - z))) - ((cosh y) ^2)) + ((sinh y) ^2) by Lm10 .= ((sinh (y + z)) * (sinh (y - z))) - (((cosh y) ^2) - ((sinh y) ^2)) .= ((sinh (y + z)) * (sinh (y - z))) - 1 by Lm3 ; hence ((sinh y) ^2) - ((cosh z) ^2) = ((sinh (y + z)) * (sinh (y - z))) - 1 ; ::_thesis: verum end; Lm11: for y, z being real number holds ( (sinh y) + (sinh z) = (2 * (sinh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2))) & (sinh y) - (sinh z) = (2 * (sinh ((y / 2) - (z / 2)))) * (cosh ((y / 2) + (z / 2))) & (cosh y) + (cosh z) = (2 * (cosh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2))) & (cosh y) - (cosh z) = (2 * (sinh ((y / 2) - (z / 2)))) * (sinh ((y / 2) + (z / 2))) & (tanh y) + (tanh z) = (sinh (y + z)) / ((cosh y) * (cosh z)) & (tanh y) - (tanh z) = (sinh (y - z)) / ((cosh y) * (cosh z)) ) proof let y, z be real number ; ::_thesis: ( (sinh y) + (sinh z) = (2 * (sinh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2))) & (sinh y) - (sinh z) = (2 * (sinh ((y / 2) - (z / 2)))) * (cosh ((y / 2) + (z / 2))) & (cosh y) + (cosh z) = (2 * (cosh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2))) & (cosh y) - (cosh z) = (2 * (sinh ((y / 2) - (z / 2)))) * (sinh ((y / 2) + (z / 2))) & (tanh y) + (tanh z) = (sinh (y + z)) / ((cosh y) * (cosh z)) & (tanh y) - (tanh z) = (sinh (y - z)) / ((cosh y) * (cosh z)) ) A1: (2 * (sinh ((y / 2) - (z / 2)))) * (cosh ((y / 2) + (z / 2))) = (2 * (sinh . ((y / 2) - (z / 2)))) * (cosh ((y / 2) + (z / 2))) by SIN_COS2:def_2 .= (2 * (sinh . ((y / 2) - (z / 2)))) * (cosh . ((y / 2) + (z / 2))) by SIN_COS2:def_4 .= (sinh . y) - (sinh . z) by SIN_COS2:26 .= (sinh y) - (sinh . z) by SIN_COS2:def_2 .= (sinh y) - (sinh z) by SIN_COS2:def_2 ; A2: (2 * (cosh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2))) = (2 * (cosh . ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2))) by SIN_COS2:def_4 .= (2 * (cosh . ((y / 2) + (z / 2)))) * (cosh . ((y / 2) - (z / 2))) by SIN_COS2:def_4 .= (cosh . y) + (cosh . z) by SIN_COS2:27 .= (cosh y) + (cosh . z) by SIN_COS2:def_4 .= (cosh y) + (cosh z) by SIN_COS2:def_4 ; A3: (sinh (y - z)) / ((cosh y) * (cosh z)) = (sinh . (y - z)) / ((cosh y) * (cosh z)) by SIN_COS2:def_2 .= (sinh . (y - z)) / ((cosh . y) * (cosh z)) by SIN_COS2:def_4 .= (sinh . (y - z)) / ((cosh . y) * (cosh . z)) by SIN_COS2:def_4 .= (tanh . y) - (tanh . z) by SIN_COS2:28 .= (tanh y) - (tanh . z) by SIN_COS2:def_6 .= (tanh y) - (tanh z) by SIN_COS2:def_6 ; A4: (sinh (y + z)) / ((cosh y) * (cosh z)) = (sinh . (y + z)) / ((cosh y) * (cosh z)) by SIN_COS2:def_2 .= (sinh . (y + z)) / ((cosh . y) * (cosh z)) by SIN_COS2:def_4 .= (sinh . (y + z)) / ((cosh . y) * (cosh . z)) by SIN_COS2:def_4 .= (tanh . y) + (tanh . z) by SIN_COS2:28 .= (tanh y) + (tanh . z) by SIN_COS2:def_6 .= (tanh y) + (tanh z) by SIN_COS2:def_6 ; A5: (2 * (sinh ((y / 2) - (z / 2)))) * (sinh ((y / 2) + (z / 2))) = (2 * (sinh . ((y / 2) - (z / 2)))) * (sinh ((y / 2) + (z / 2))) by SIN_COS2:def_2 .= (2 * (sinh . ((y / 2) - (z / 2)))) * (sinh . ((y / 2) + (z / 2))) by SIN_COS2:def_2 .= (cosh . y) - (cosh . z) by SIN_COS2:27 .= (cosh y) - (cosh . z) by SIN_COS2:def_4 .= (cosh y) - (cosh z) by SIN_COS2:def_4 ; (2 * (sinh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2))) = (2 * (sinh . ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2))) by SIN_COS2:def_2 .= (2 * (sinh . ((y / 2) + (z / 2)))) * (cosh . ((y / 2) - (z / 2))) by SIN_COS2:def_4 .= (sinh . y) + (sinh . z) by SIN_COS2:26 .= (sinh y) + (sinh . z) by SIN_COS2:def_2 .= (sinh y) + (sinh z) by SIN_COS2:def_2 ; hence ( (sinh y) + (sinh z) = (2 * (sinh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2))) & (sinh y) - (sinh z) = (2 * (sinh ((y / 2) - (z / 2)))) * (cosh ((y / 2) + (z / 2))) & (cosh y) + (cosh z) = (2 * (cosh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2))) & (cosh y) - (cosh z) = (2 * (sinh ((y / 2) - (z / 2)))) * (sinh ((y / 2) + (z / 2))) & (tanh y) + (tanh z) = (sinh (y + z)) / ((cosh y) * (cosh z)) & (tanh y) - (tanh z) = (sinh (y - z)) / ((cosh y) * (cosh z)) ) by A1, A2, A5, A4, A3; ::_thesis: verum end; theorem :: SIN_COS8:13 for y, z being real number holds ( (((sinh y) - (sinh z)) ^2) - (((cosh y) - (cosh z)) ^2) = 4 * ((sinh ((y - z) / 2)) ^2) & (((cosh y) + (cosh z)) ^2) - (((sinh y) + (sinh z)) ^2) = 4 * ((cosh ((y - z) / 2)) ^2) ) proof let y, z be real number ; ::_thesis: ( (((sinh y) - (sinh z)) ^2) - (((cosh y) - (cosh z)) ^2) = 4 * ((sinh ((y - z) / 2)) ^2) & (((cosh y) + (cosh z)) ^2) - (((sinh y) + (sinh z)) ^2) = 4 * ((cosh ((y - z) / 2)) ^2) ) A1: (((cosh y) + (cosh z)) ^2) - (((sinh y) + (sinh z)) ^2) = (((2 * (cosh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2)))) ^2) - (((sinh y) + (sinh z)) ^2) by Lm11 .= ((2 * ((cosh ((y / 2) + (z / 2))) * (cosh ((y / 2) - (z / 2))))) ^2) - (((2 * (sinh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2)))) ^2) by Lm11 .= 4 * (((cosh ((y / 2) - (z / 2))) ^2) * (((cosh ((y / 2) + (z / 2))) ^2) - ((sinh ((y / 2) + (z / 2))) ^2))) .= 4 * (((cosh ((y / 2) - (z / 2))) ^2) * 1) by Lm3 .= 4 * ((cosh ((y - z) / 2)) ^2) ; (((sinh y) - (sinh z)) ^2) - (((cosh y) - (cosh z)) ^2) = (((2 * (sinh ((y / 2) - (z / 2)))) * (cosh ((y / 2) + (z / 2)))) ^2) - (((cosh y) - (cosh z)) ^2) by Lm11 .= (((2 * (cosh ((y / 2) + (z / 2)))) * (sinh ((y / 2) - (z / 2)))) ^2) - (((2 * (sinh ((y / 2) - (z / 2)))) * (sinh ((y + z) / 2))) ^2) by Lm11 .= 4 * (((sinh ((y / 2) - (z / 2))) ^2) * (((cosh ((y / 2) + (z / 2))) ^2) - ((sinh ((y / 2) + (z / 2))) ^2))) .= 4 * (((sinh ((y / 2) - (z / 2))) ^2) * 1) by Lm3 .= 4 * ((sinh ((y - z) / 2)) ^2) ; hence ( (((sinh y) - (sinh z)) ^2) - (((cosh y) - (cosh z)) ^2) = 4 * ((sinh ((y - z) / 2)) ^2) & (((cosh y) + (cosh z)) ^2) - (((sinh y) + (sinh z)) ^2) = 4 * ((cosh ((y - z) / 2)) ^2) ) by A1; ::_thesis: verum end; theorem :: SIN_COS8:14 for y, z being real number holds ((sinh y) + (sinh z)) / ((sinh y) - (sinh z)) = (tanh ((y + z) / 2)) * (coth ((y - z) / 2)) proof let y, z be real number ; ::_thesis: ((sinh y) + (sinh z)) / ((sinh y) - (sinh z)) = (tanh ((y + z) / 2)) * (coth ((y - z) / 2)) ((sinh y) + (sinh z)) / ((sinh y) - (sinh z)) = ((2 * (sinh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2)))) / ((sinh y) - (sinh z)) by Lm11 .= ((2 * (sinh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2)))) / ((2 * (sinh ((y / 2) - (z / 2)))) * (cosh ((y / 2) + (z / 2)))) by Lm11 .= ((2 * (sinh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2)))) / ((2 * (cosh ((y / 2) + (z / 2)))) * (sinh ((y / 2) - (z / 2)))) .= ((2 * (sinh ((y / 2) + (z / 2)))) / (2 * (cosh ((y / 2) + (z / 2))))) * ((cosh ((y / 2) - (z / 2))) / (sinh ((y / 2) - (z / 2)))) by XCMPLX_1:76 .= ((2 * (sinh ((y / 2) + (z / 2)))) / (2 * (cosh ((y / 2) + (z / 2))))) * (coth ((y / 2) - (z / 2))) by SIN_COS5:def_1 .= ((2 / 2) * ((sinh ((y / 2) + (z / 2))) / (cosh ((y / 2) + (z / 2))))) * (coth ((y / 2) - (z / 2))) by XCMPLX_1:76 .= (tanh ((y + z) / 2)) * (coth ((y - z) / 2)) by Th1 ; hence ((sinh y) + (sinh z)) / ((sinh y) - (sinh z)) = (tanh ((y + z) / 2)) * (coth ((y - z) / 2)) ; ::_thesis: verum end; theorem :: SIN_COS8:15 for y, z being real number holds ((cosh y) + (cosh z)) / ((cosh y) - (cosh z)) = (coth ((y + z) / 2)) * (coth ((y - z) / 2)) proof let y, z be real number ; ::_thesis: ((cosh y) + (cosh z)) / ((cosh y) - (cosh z)) = (coth ((y + z) / 2)) * (coth ((y - z) / 2)) ((cosh y) + (cosh z)) / ((cosh y) - (cosh z)) = ((2 * (cosh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2)))) / ((cosh y) - (cosh z)) by Lm11 .= ((2 * (cosh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2)))) / ((2 * (sinh ((y / 2) - (z / 2)))) * (sinh ((y + z) / 2))) by Lm11 .= ((2 * (cosh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2)))) / ((2 * (sinh ((y / 2) + (z / 2)))) * (sinh ((y - z) / 2))) .= ((2 * (cosh ((y / 2) + (z / 2)))) / (2 * (sinh ((y / 2) + (z / 2))))) * ((cosh ((y / 2) - (z / 2))) / (sinh ((y / 2) - (z / 2)))) by XCMPLX_1:76 .= ((2 * (cosh ((y / 2) + (z / 2)))) / (2 * (sinh ((y / 2) + (z / 2))))) * (coth ((y / 2) - (z / 2))) by SIN_COS5:def_1 .= ((2 / 2) * ((cosh ((y / 2) + (z / 2))) / (sinh ((y / 2) + (z / 2))))) * (coth ((y / 2) - (z / 2))) by XCMPLX_1:76 .= (coth ((y + z) / 2)) * (coth ((y - z) / 2)) by SIN_COS5:def_1 ; hence ((cosh y) + (cosh z)) / ((cosh y) - (cosh z)) = (coth ((y + z) / 2)) * (coth ((y - z) / 2)) ; ::_thesis: verum end; theorem :: SIN_COS8:16 for y, z being real number st y - z <> 0 holds ((sinh y) + (sinh z)) / ((cosh y) + (cosh z)) = ((cosh y) - (cosh z)) / ((sinh y) - (sinh z)) proof let y, z be real number ; ::_thesis: ( y - z <> 0 implies ((sinh y) + (sinh z)) / ((cosh y) + (cosh z)) = ((cosh y) - (cosh z)) / ((sinh y) - (sinh z)) ) assume A1: y - z <> 0 ; ::_thesis: ((sinh y) + (sinh z)) / ((cosh y) + (cosh z)) = ((cosh y) - (cosh z)) / ((sinh y) - (sinh z)) A2: cosh ((y / 2) - (z / 2)) <> 0 by Lm1; ((sinh y) + (sinh z)) / ((cosh y) + (cosh z)) = ((2 * (sinh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2)))) / ((cosh y) + (cosh z)) by Lm11 .= ((2 * (sinh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2)))) / ((2 * (cosh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2)))) by Lm11 .= ((2 * (sinh ((y / 2) + (z / 2)))) / (2 * (cosh ((y / 2) + (z / 2))))) * ((cosh ((y / 2) - (z / 2))) / (cosh ((y / 2) - (z / 2)))) by XCMPLX_1:76 .= ((2 * (sinh ((y / 2) + (z / 2)))) / (2 * (cosh ((y / 2) + (z / 2))))) * 1 by A2, XCMPLX_1:60 .= ((2 * (sinh ((y + z) / 2))) * (sinh ((y - z) / 2))) / ((2 * (cosh ((y / 2) + (z / 2)))) * (sinh ((y / 2) - (z / 2)))) by A1, Lm5, XCMPLX_1:91 .= ((2 * (sinh ((y - z) / 2))) * (sinh ((y + z) / 2))) / ((2 * (cosh ((y / 2) + (z / 2)))) * (sinh ((y / 2) - (z / 2)))) .= ((cosh y) - (cosh z)) / ((2 * (sinh ((y / 2) - (z / 2)))) * (cosh ((y / 2) + (z / 2)))) by Lm11 .= ((cosh y) - (cosh z)) / ((sinh y) - (sinh z)) by Lm11 ; hence ((sinh y) + (sinh z)) / ((cosh y) + (cosh z)) = ((cosh y) - (cosh z)) / ((sinh y) - (sinh z)) ; ::_thesis: verum end; theorem :: SIN_COS8:17 for y, z being real number st y + z <> 0 holds ((sinh y) - (sinh z)) / ((cosh y) + (cosh z)) = ((cosh y) - (cosh z)) / ((sinh y) + (sinh z)) proof let y, z be real number ; ::_thesis: ( y + z <> 0 implies ((sinh y) - (sinh z)) / ((cosh y) + (cosh z)) = ((cosh y) - (cosh z)) / ((sinh y) + (sinh z)) ) assume A1: y + z <> 0 ; ::_thesis: ((sinh y) - (sinh z)) / ((cosh y) + (cosh z)) = ((cosh y) - (cosh z)) / ((sinh y) + (sinh z)) A2: cosh ((y / 2) + (z / 2)) <> 0 by Lm1; ((sinh y) - (sinh z)) / ((cosh y) + (cosh z)) = ((2 * (sinh ((y / 2) - (z / 2)))) * (cosh ((y / 2) + (z / 2)))) / ((cosh y) + (cosh z)) by Lm11 .= ((2 * (cosh ((y / 2) + (z / 2)))) * (sinh ((y / 2) - (z / 2)))) / ((2 * (cosh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2)))) by Lm11 .= ((2 * (cosh ((y / 2) + (z / 2)))) / (2 * (cosh ((y / 2) + (z / 2))))) * ((sinh ((y / 2) - (z / 2))) / (cosh ((y / 2) - (z / 2)))) by XCMPLX_1:76 .= ((cosh ((y / 2) + (z / 2))) / (cosh ((y / 2) + (z / 2)))) * ((sinh ((y / 2) - (z / 2))) / (cosh ((y / 2) - (z / 2)))) by XCMPLX_1:91 .= 1 * ((sinh ((y / 2) - (z / 2))) / (cosh ((y / 2) - (z / 2)))) by A2, XCMPLX_1:60 .= ((sinh ((y / 2) + (z / 2))) * (sinh ((y / 2) - (z / 2)))) / ((sinh ((y / 2) + (z / 2))) * (cosh ((y / 2) - (z / 2)))) by A1, Lm6, XCMPLX_1:91 .= (2 * ((sinh ((y / 2) + (z / 2))) * (sinh ((y / 2) - (z / 2))))) / (2 * ((sinh ((y / 2) + (z / 2))) * (cosh ((y / 2) - (z / 2))))) by XCMPLX_1:91 .= ((2 * (sinh ((y - z) / 2))) * (sinh ((y + z) / 2))) / ((2 * (sinh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2)))) .= ((cosh y) - (cosh z)) / ((2 * (sinh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2)))) by Lm11 .= ((cosh y) - (cosh z)) / ((sinh y) + (sinh z)) by Lm11 ; hence ((sinh y) - (sinh z)) / ((cosh y) + (cosh z)) = ((cosh y) - (cosh z)) / ((sinh y) + (sinh z)) ; ::_thesis: verum end; theorem :: SIN_COS8:18 for y, z being real number holds ( ((sinh y) + (sinh z)) / ((cosh y) + (cosh z)) = tanh ((y / 2) + (z / 2)) & ((sinh y) - (sinh z)) / ((cosh y) + (cosh z)) = tanh ((y / 2) - (z / 2)) ) proof let y, z be real number ; ::_thesis: ( ((sinh y) + (sinh z)) / ((cosh y) + (cosh z)) = tanh ((y / 2) + (z / 2)) & ((sinh y) - (sinh z)) / ((cosh y) + (cosh z)) = tanh ((y / 2) - (z / 2)) ) A1: cosh ((y / 2) - (z / 2)) <> 0 by Lm1; A2: cosh ((y / 2) + (z / 2)) <> 0 by Lm1; A3: ((sinh y) - (sinh z)) / ((cosh y) + (cosh z)) = ((2 * (sinh ((y / 2) - (z / 2)))) * (cosh ((y / 2) + (z / 2)))) / ((cosh y) + (cosh z)) by Lm11 .= (2 * ((sinh ((y / 2) - (z / 2))) * (cosh ((y / 2) + (z / 2))))) / ((2 * (cosh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2)))) by Lm11 .= (2 * ((sinh ((y / 2) - (z / 2))) * (cosh ((y / 2) + (z / 2))))) / (2 * ((cosh ((y / 2) + (z / 2))) * (cosh ((y / 2) - (z / 2))))) .= ((cosh ((y / 2) + (z / 2))) * (sinh ((y / 2) - (z / 2)))) / ((cosh ((y / 2) + (z / 2))) * (cosh ((y / 2) - (z / 2)))) by XCMPLX_1:91 .= ((cosh ((y / 2) + (z / 2))) / (cosh ((y / 2) + (z / 2)))) * ((sinh ((y / 2) - (z / 2))) / (cosh ((y / 2) - (z / 2)))) by XCMPLX_1:76 .= 1 * ((sinh ((y / 2) - (z / 2))) / (cosh ((y / 2) - (z / 2)))) by A2, XCMPLX_1:60 .= tanh ((y / 2) - (z / 2)) by Th1 ; ((sinh y) + (sinh z)) / ((cosh y) + (cosh z)) = ((2 * (sinh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2)))) / ((cosh y) + (cosh z)) by Lm11 .= ((2 * (sinh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2)))) / ((2 * (cosh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2)))) by Lm11 .= ((2 * (sinh ((y / 2) + (z / 2)))) / (2 * (cosh ((y / 2) + (z / 2))))) * ((cosh ((y / 2) - (z / 2))) / (cosh ((y / 2) - (z / 2)))) by XCMPLX_1:76 .= ((2 * (sinh ((y / 2) + (z / 2)))) / (2 * (cosh ((y / 2) + (z / 2))))) * 1 by A1, XCMPLX_1:60 .= (2 / 2) * ((sinh ((y / 2) + (z / 2))) / (cosh ((y / 2) + (z / 2)))) by XCMPLX_1:76 .= tanh ((y / 2) + (z / 2)) by Th1 ; hence ( ((sinh y) + (sinh z)) / ((cosh y) + (cosh z)) = tanh ((y / 2) + (z / 2)) & ((sinh y) - (sinh z)) / ((cosh y) + (cosh z)) = tanh ((y / 2) - (z / 2)) ) by A3; ::_thesis: verum end; theorem :: SIN_COS8:19 for y, z being real number holds ((tanh y) + (tanh z)) / ((tanh y) - (tanh z)) = (sinh (y + z)) / (sinh (y - z)) proof let y, z be real number ; ::_thesis: ((tanh y) + (tanh z)) / ((tanh y) - (tanh z)) = (sinh (y + z)) / (sinh (y - z)) A1: ( cosh y <> 0 & cosh z <> 0 ) by Lm1; ((tanh y) + (tanh z)) / ((tanh y) - (tanh z)) = ((sinh (y + z)) / ((cosh y) * (cosh z))) / ((tanh y) - (tanh z)) by Lm11 .= ((sinh (y + z)) / ((cosh y) * (cosh z))) / ((sinh (y - z)) / ((cosh y) * (cosh z))) by Lm11 .= (sinh (y + z)) / (sinh (y - z)) by A1, XCMPLX_1:6, XCMPLX_1:55 ; hence ((tanh y) + (tanh z)) / ((tanh y) - (tanh z)) = (sinh (y + z)) / (sinh (y - z)) ; ::_thesis: verum end; Lm12: for x being real number holds 1 + ((cosh x) + (cosh x)) <> 0 proof let x be real number ; ::_thesis: 1 + ((cosh x) + (cosh x)) <> 0 cosh . x > 0 by SIN_COS2:15; then cosh x > 0 by SIN_COS2:def_4; hence 1 + ((cosh x) + (cosh x)) <> 0 ; ::_thesis: verum end; Lm13: for x being real number holds ( (cosh x) + 1 > 0 & (cosh x) - 1 >= 0 & ((cosh x) + 2) + (cosh x) <> 0 ) proof let x be real number ; ::_thesis: ( (cosh x) + 1 > 0 & (cosh x) - 1 >= 0 & ((cosh x) + 2) + (cosh x) <> 0 ) cosh . x > 0 by SIN_COS2:15; then A1: cosh x > 0 by SIN_COS2:def_4; cosh x >= 1 by Lm1; then (cosh x) - 1 >= 1 - 1 by XREAL_1:13; hence ( (cosh x) + 1 > 0 & (cosh x) - 1 >= 0 & ((cosh x) + 2) + (cosh x) <> 0 ) by A1; ::_thesis: verum end; theorem :: SIN_COS8:20 for y, z being real number holds (((sinh (y - z)) + (sinh y)) + (sinh (y + z))) / (((cosh (y - z)) + (cosh y)) + (cosh (y + z))) = tanh y proof let y, z be real number ; ::_thesis: (((sinh (y - z)) + (sinh y)) + (sinh (y + z))) / (((cosh (y - z)) + (cosh y)) + (cosh (y + z))) = tanh y (((sinh (y - z)) + (sinh y)) + (sinh (y + z))) / (((cosh (y - z)) + (cosh y)) + (cosh (y + z))) = (((((sinh y) * (cosh z)) - ((cosh y) * (sinh z))) + (sinh y)) + (sinh (y + z))) / (((cosh (y - z)) + (cosh y)) + (cosh (y + z))) by Lm10 .= (((sinh y) + (((sinh y) * (cosh z)) - ((cosh y) * (sinh z)))) + (((sinh y) * (cosh z)) + ((cosh y) * (sinh z)))) / (((cosh y) + (cosh (y - z))) + (cosh (y + z))) by Lm10 .= ((sinh y) * (1 + ((cosh z) + (cosh z)))) / (((cosh y) + (((cosh y) * (cosh z)) - ((sinh y) * (sinh z)))) + (cosh (y + z))) by Lm10 .= ((sinh y) * (1 + ((cosh z) + (cosh z)))) / (((cosh y) + (((cosh y) * (cosh z)) - ((sinh y) * (sinh z)))) + (((cosh y) * (cosh z)) + ((sinh y) * (sinh z)))) by Lm10 .= ((sinh y) * (1 + ((cosh z) + (cosh z)))) / ((cosh y) * (1 + ((cosh z) + (cosh z)))) .= ((sinh y) / (cosh y)) * ((1 + ((cosh z) + (cosh z))) / (1 + ((cosh z) + (cosh z)))) by XCMPLX_1:76 .= ((sinh y) / (cosh y)) * 1 by Lm12, XCMPLX_1:60 .= tanh y by Th1 ; hence (((sinh (y - z)) + (sinh y)) + (sinh (y + z))) / (((cosh (y - z)) + (cosh y)) + (cosh (y + z))) = tanh y ; ::_thesis: verum end; Lm14: for y, z being real number holds ( ((sinh y) * (cosh z)) / ((cosh y) * (cosh z)) = tanh y & (sinh y) * (cosh z) = (tanh y) * ((cosh y) * (cosh z)) & sinh y = (tanh y) * (cosh y) & (sinh y) * (sinh z) = ((tanh y) * (tanh z)) * ((cosh y) * (cosh z)) ) proof let y, z be real number ; ::_thesis: ( ((sinh y) * (cosh z)) / ((cosh y) * (cosh z)) = tanh y & (sinh y) * (cosh z) = (tanh y) * ((cosh y) * (cosh z)) & sinh y = (tanh y) * (cosh y) & (sinh y) * (sinh z) = ((tanh y) * (tanh z)) * ((cosh y) * (cosh z)) ) A1: cosh y <> 0 by Lm1; then A2: sinh y = ((sinh y) / (cosh y)) * (cosh y) by XCMPLX_1:87 .= (tanh y) * (cosh y) by Th1 ; A3: cosh z <> 0 by Lm1; then A4: ((sinh y) * (cosh z)) / ((cosh y) * (cosh z)) = (sinh y) / (cosh y) by XCMPLX_1:91 .= tanh y by Th1 ; (sinh y) * (sinh z) = (((sinh y) * (sinh z)) / ((cosh y) * (cosh z))) * ((cosh y) * (cosh z)) by A1, A3, XCMPLX_1:6, XCMPLX_1:87 .= (((sinh y) / (cosh y)) * ((sinh z) / (cosh z))) * ((cosh y) * (cosh z)) by XCMPLX_1:76 .= ((tanh y) * ((sinh z) / (cosh z))) * ((cosh y) * (cosh z)) by Th1 .= ((tanh y) * (tanh z)) * ((cosh y) * (cosh z)) by Th1 ; hence ( ((sinh y) * (cosh z)) / ((cosh y) * (cosh z)) = tanh y & (sinh y) * (cosh z) = (tanh y) * ((cosh y) * (cosh z)) & sinh y = (tanh y) * (cosh y) & (sinh y) * (sinh z) = ((tanh y) * (tanh z)) * ((cosh y) * (cosh z)) ) by A4, A2; ::_thesis: verum end; theorem Th21: :: SIN_COS8:21 for y, z, w being real number holds ( sinh ((y + z) + w) = ((((((tanh y) + (tanh z)) + (tanh w)) + (((tanh y) * (tanh z)) * (tanh w))) * (cosh y)) * (cosh z)) * (cosh w) & cosh ((y + z) + w) = (((((1 + ((tanh y) * (tanh z))) + ((tanh z) * (tanh w))) + ((tanh w) * (tanh y))) * (cosh y)) * (cosh z)) * (cosh w) & tanh ((y + z) + w) = ((((tanh y) + (tanh z)) + (tanh w)) + (((tanh y) * (tanh z)) * (tanh w))) / (((1 + ((tanh z) * (tanh w))) + ((tanh w) * (tanh y))) + ((tanh y) * (tanh z))) ) proof let y, z, w be real number ; ::_thesis: ( sinh ((y + z) + w) = ((((((tanh y) + (tanh z)) + (tanh w)) + (((tanh y) * (tanh z)) * (tanh w))) * (cosh y)) * (cosh z)) * (cosh w) & cosh ((y + z) + w) = (((((1 + ((tanh y) * (tanh z))) + ((tanh z) * (tanh w))) + ((tanh w) * (tanh y))) * (cosh y)) * (cosh z)) * (cosh w) & tanh ((y + z) + w) = ((((tanh y) + (tanh z)) + (tanh w)) + (((tanh y) * (tanh z)) * (tanh w))) / (((1 + ((tanh z) * (tanh w))) + ((tanh w) * (tanh y))) + ((tanh y) * (tanh z))) ) A1: cosh w <> 0 by Lm1; ( cosh y <> 0 & cosh z <> 0 ) by Lm1; then A2: (cosh y) * (cosh z) <> 0 by XCMPLX_1:6; A3: cosh ((y + z) + w) = ((cosh (y + z)) * (cosh w)) + ((sinh (y + z)) * (sinh w)) by Lm10 .= ((((cosh y) * (cosh z)) + ((sinh y) * (sinh z))) * (cosh w)) + ((sinh (y + z)) * (sinh w)) by Lm10 .= ((((cosh y) * (cosh z)) * (cosh w)) + (((sinh y) * (sinh z)) * (cosh w))) + ((((sinh y) * (cosh z)) + ((cosh y) * (sinh z))) * (sinh w)) by Lm10 .= ((((cosh y) * (cosh z)) * (cosh w)) + ((((tanh y) * (tanh z)) * ((cosh y) * (cosh z))) * (cosh w))) + ((((sinh y) * (sinh w)) * (cosh z)) + (((sinh z) * (sinh w)) * (cosh y))) by Lm14 .= ((((cosh y) * (cosh z)) * (cosh w)) + ((((tanh y) * (tanh z)) * ((cosh y) * (cosh z))) * (cosh w))) + (((((tanh w) * (tanh y)) * ((cosh w) * (cosh y))) * (cosh z)) + (((sinh z) * (sinh w)) * (cosh y))) by Lm14 .= ((1 + ((tanh y) * (tanh z))) * (((cosh y) * (cosh z)) * (cosh w))) + (((((tanh z) * (tanh w)) * ((cosh z) * (cosh w))) * (cosh y)) + (((tanh w) * (tanh y)) * (((cosh y) * (cosh z)) * (cosh w)))) by Lm14 .= (((((1 + ((tanh y) * (tanh z))) + ((tanh z) * (tanh w))) + ((tanh w) * (tanh y))) * (cosh y)) * (cosh z)) * (cosh w) ; A4: sinh ((y + z) + w) = ((sinh (y + z)) * (cosh w)) + ((cosh (y + z)) * (sinh w)) by Lm10 .= ((((sinh y) * (cosh z)) + ((cosh y) * (sinh z))) * (cosh w)) + ((cosh (y + z)) * (sinh w)) by Lm10 .= ((((sinh y) * (cosh z)) + ((cosh y) * (sinh z))) * (cosh w)) + ((((cosh y) * (cosh z)) + ((sinh y) * (sinh z))) * (sinh w)) by Lm10 .= ((((tanh y) * ((cosh y) * (cosh z))) + ((cosh y) * (sinh z))) * (cosh w)) + ((((cosh y) * (cosh z)) + ((sinh y) * (sinh z))) * (sinh w)) by Lm14 .= ((((tanh y) * ((cosh y) * (cosh z))) + ((tanh z) * ((cosh y) * (cosh z)))) * (cosh w)) + ((((cosh y) * (cosh z)) + ((sinh y) * (sinh z))) * (sinh w)) by Lm14 .= (((tanh y) + (tanh z)) * (((cosh y) * (cosh z)) * (cosh w))) + (((cosh y) * ((cosh z) * (sinh w))) + (((sinh y) * (sinh z)) * (sinh w))) .= (((tanh y) + (tanh z)) * (((cosh y) * (cosh z)) * (cosh w))) + (((cosh y) * ((tanh w) * ((cosh z) * (cosh w)))) + (((sinh y) * (sinh z)) * (sinh w))) by Lm14 .= (((tanh y) + (tanh z)) * (((cosh y) * (cosh z)) * (cosh w))) + ((((tanh w) * ((cosh y) * (cosh z))) * (cosh w)) + ((((tanh y) * (cosh y)) * (sinh z)) * (sinh w))) by Lm14 .= (((tanh y) + (tanh z)) * (((cosh y) * (cosh z)) * (cosh w))) + ((((tanh w) * ((cosh y) * (cosh z))) * (cosh w)) + ((((tanh y) * (cosh y)) * ((tanh z) * (cosh z))) * (sinh w))) by Lm14 .= (((tanh y) + (tanh z)) * (((cosh y) * (cosh z)) * (cosh w))) + ((((tanh w) * ((cosh y) * (cosh z))) * (cosh w)) + ((((tanh y) * (tanh z)) * ((cosh y) * (cosh z))) * ((tanh w) * (cosh w)))) by Lm14 .= ((((((tanh y) + (tanh z)) + (tanh w)) + (((tanh y) * (tanh z)) * (tanh w))) * (cosh y)) * (cosh z)) * (cosh w) ; then tanh ((y + z) + w) = (((((tanh y) + (tanh z)) + (tanh w)) + (((tanh y) * (tanh z)) * (tanh w))) * (((cosh y) * (cosh z)) * (cosh w))) / ((((1 + ((tanh y) * (tanh z))) + ((tanh z) * (tanh w))) + ((tanh w) * (tanh y))) * (((cosh y) * (cosh z)) * (cosh w))) by A3, Th1 .= ((((tanh y) + (tanh z)) + (tanh w)) + (((tanh y) * (tanh z)) * (tanh w))) / (((1 + ((tanh y) * (tanh z))) + ((tanh z) * (tanh w))) + ((tanh w) * (tanh y))) by A1, A2, XCMPLX_1:6, XCMPLX_1:91 ; hence ( sinh ((y + z) + w) = ((((((tanh y) + (tanh z)) + (tanh w)) + (((tanh y) * (tanh z)) * (tanh w))) * (cosh y)) * (cosh z)) * (cosh w) & cosh ((y + z) + w) = (((((1 + ((tanh y) * (tanh z))) + ((tanh z) * (tanh w))) + ((tanh w) * (tanh y))) * (cosh y)) * (cosh z)) * (cosh w) & tanh ((y + z) + w) = ((((tanh y) + (tanh z)) + (tanh w)) + (((tanh y) * (tanh z)) * (tanh w))) / (((1 + ((tanh z) * (tanh w))) + ((tanh w) * (tanh y))) + ((tanh y) * (tanh z))) ) by A4, A3; ::_thesis: verum end; theorem :: SIN_COS8:22 for y, z, w being real number holds (((cosh (2 * y)) + (cosh (2 * z))) + (cosh (2 * w))) + (cosh (2 * ((y + z) + w))) = ((4 * (cosh (z + w))) * (cosh (w + y))) * (cosh (y + z)) proof let y, z, w be real number ; ::_thesis: (((cosh (2 * y)) + (cosh (2 * z))) + (cosh (2 * w))) + (cosh (2 * ((y + z) + w))) = ((4 * (cosh (z + w))) * (cosh (w + y))) * (cosh (y + z)) (((cosh (2 * y)) + (cosh (2 * z))) + (cosh (2 * w))) + (cosh (2 * ((y + z) + w))) = 2 * (((1 / 2) * ((cosh (2 * ((y + z) + w))) + (cosh (2 * y)))) + ((1 / 2) * ((cosh (2 * w)) + (cosh (2 * z))))) .= 2 * (((1 / 2) * ((2 * (cosh (((2 * ((y + z) + w)) / 2) + ((2 * y) / 2)))) * (cosh (((2 * ((y + z) + w)) / 2) - ((2 * y) / 2))))) + ((1 / 2) * ((cosh (2 * w)) + (cosh (2 * z))))) by Lm11 .= 2 * (((cosh (z + w)) * (cosh (((y + z) + w) + y))) + ((1 / 2) * ((2 * (cosh (((2 * w) / 2) + ((2 * z) / 2)))) * (cosh (((2 * w) / 2) - ((2 * z) / 2)))))) by Lm11 .= 2 * ((cosh (z + w)) * ((cosh ((2 * y) + (z + w))) + (cosh (w - z)))) .= 2 * ((cosh (z + w)) * ((2 * (cosh ((((2 * y) + (z + w)) / 2) + ((w - z) / 2)))) * (cosh ((((2 * y) + (z + w)) / 2) - ((w - z) / 2))))) by Lm11 .= ((4 * (cosh (z + w))) * (cosh (w + y))) * (cosh (y + z)) ; hence (((cosh (2 * y)) + (cosh (2 * z))) + (cosh (2 * w))) + (cosh (2 * ((y + z) + w))) = ((4 * (cosh (z + w))) * (cosh (w + y))) * (cosh (y + z)) ; ::_thesis: verum end; theorem :: SIN_COS8:23 for y, z, w being real number holds (((((sinh y) * (sinh z)) * (sinh (z - y))) + (((sinh z) * (sinh w)) * (sinh (w - z)))) + (((sinh w) * (sinh y)) * (sinh (y - w)))) + (((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w))) = 0 proof let y, z, w be real number ; ::_thesis: (((((sinh y) * (sinh z)) * (sinh (z - y))) + (((sinh z) * (sinh w)) * (sinh (w - z)))) + (((sinh w) * (sinh y)) * (sinh (y - w)))) + (((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w))) = 0 (((((sinh y) * (sinh z)) * (sinh (z - y))) + (((sinh z) * (sinh w)) * (sinh (w - z)))) + (((sinh w) * (sinh y)) * (sinh (y - w)))) + (((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w))) = (((((1 / 2) * ((cosh (y + z)) - (cosh (y - z)))) * (sinh (z - y))) + (((sinh z) * (sinh w)) * (sinh (w - z)))) + (((sinh w) * (sinh y)) * (sinh (y - w)))) + (((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w))) by Th11 .= ((((1 / 2) * (((cosh (y + z)) * (sinh (z - y))) - ((cosh (y - z)) * (sinh (z - y))))) + (((sinh z) * (sinh w)) * (sinh (w - z)))) + (((sinh w) * (sinh y)) * (sinh (y - w)))) + (((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w))) .= ((((1 / 2) * (((1 / 2) * ((sinh ((y + z) + (z - y))) - (sinh ((y + z) - (z - y))))) - ((cosh (y - z)) * (sinh (z - y))))) + (((sinh z) * (sinh w)) * (sinh (w - z)))) + (((sinh w) * (sinh y)) * (sinh (y - w)))) + (((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w))) by Th11 .= ((((1 / 2) * (((1 / 2) * ((sinh (2 * z)) - (sinh (y + y)))) - ((1 / 2) * ((sinh ((y - z) + (- (y - z)))) - (sinh ((y - z) - (z - y))))))) + (((sinh z) * (sinh w)) * (sinh (w - z)))) + (((sinh w) * (sinh y)) * (sinh (y - w)))) + (((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w))) by Th11 .= ((((1 / 2) * (((1 / 2) * ((sinh (2 * z)) - (sinh (2 * y)))) - ((1 / 2) * ((sinh . 0) - (sinh (2 * (y - z))))))) + (((sinh z) * (sinh w)) * (sinh (w - z)))) + (((sinh w) * (sinh y)) * (sinh (y - w)))) + (((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w))) by SIN_COS2:def_2 .= ((((1 / 2) * ((1 / 2) * (((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z))))))) + (((1 / 2) * ((cosh (z + w)) - (cosh (z - w)))) * (sinh (w - z)))) + (((sinh w) * (sinh y)) * (sinh (y - w)))) + (((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w))) by Th11, SIN_COS2:16 .= (((1 / 2) * (((1 / 2) * (((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z)))))) + (((cosh (z + w)) * (sinh (w - z))) - ((cosh (z - w)) * (sinh (w - z)))))) + (((sinh w) * (sinh y)) * (sinh (y - w)))) + (((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w))) .= (((1 / 2) * (((1 / 2) * (((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z)))))) + (((1 / 2) * ((sinh ((z + w) + (w - z))) - (sinh ((z + w) - (w - z))))) - ((cosh (z - w)) * (sinh (w - z)))))) + (((sinh w) * (sinh y)) * (sinh (y - w)))) + (((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w))) by Th11 .= (((1 / 2) * (((1 / 2) * (((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z)))))) + (((1 / 2) * ((sinh (2 * w)) - (sinh (2 * z)))) - ((1 / 2) * ((sinh ((z - w) + (w - z))) - (sinh ((z - w) - (w - z)))))))) + (((sinh w) * (sinh y)) * (sinh (y - w)))) + (((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w))) by Th11 .= (((1 / 2) * (((1 / 2) * (((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z)))))) + (((1 / 2) * ((sinh (2 * w)) - (sinh (2 * z)))) - ((1 / 2) * (0 - (sinh ((z - w) - (w - z)))))))) + (((sinh w) * (sinh y)) * (sinh (y - w)))) + (((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w))) by SIN_COS2:16, SIN_COS2:def_2 .= (((1 / 2) * ((1 / 2) * ((((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z))))) + (((sinh (2 * w)) - (sinh (2 * z))) - (- (sinh (2 * (z - w)))))))) + (((1 / 2) * ((cosh (w + y)) - (cosh (w - y)))) * (sinh (y - w)))) + (((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w))) by Th11 .= ((1 / 2) * (((1 / 2) * ((((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z))))) + (((sinh (2 * w)) - (sinh (2 * z))) - (- (sinh (2 * (z - w))))))) + (((cosh (w + y)) * (sinh (y - w))) - ((cosh (w - y)) * (sinh (y - w)))))) + (((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w))) .= ((1 / 2) * (((1 / 2) * ((((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z))))) + (((sinh (2 * w)) - (sinh (2 * z))) - (- (sinh (2 * (z - w))))))) + (((1 / 2) * ((sinh ((w + y) + (y - w))) - (sinh ((w + y) - (y - w))))) - ((cosh (w - y)) * (sinh (y - w)))))) + (((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w))) by Th11 .= ((1 / 2) * (((1 / 2) * ((((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z))))) + (((sinh (2 * w)) - (sinh (2 * z))) - (- (sinh (2 * (z - w))))))) + (((1 / 2) * ((sinh (2 * y)) - (sinh (2 * w)))) - ((1 / 2) * ((sinh ((w - y) + (- (w - y)))) - (sinh ((w - y) - (- (w - y))))))))) + (((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w))) by Th11 .= ((1 / 2) * (((1 / 2) * ((((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z))))) + (((sinh (2 * w)) - (sinh (2 * z))) - (- (sinh (2 * (z - w))))))) + (((1 / 2) * ((sinh (2 * y)) - (sinh (2 * w)))) - ((1 / 2) * (0 - (sinh (2 * (w - y)))))))) + (((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w))) by SIN_COS2:16, SIN_COS2:def_2 .= ((1 / 2) * ((1 / 2) * (((sinh (2 * (y - z))) + (sinh (2 * (z - w)))) + (sinh (2 * (w - y)))))) + (((1 / 2) * ((cosh ((z - y) + (- (z - w)))) - (cosh ((z - y) - (w - z))))) * (sinh (y - w))) by Th11 .= (1 / 2) * (((1 / 2) * (((sinh (2 * (y - z))) + (sinh (2 * (z - w)))) + (sinh (2 * (w - y))))) + (((cosh (w - y)) * (sinh (y - w))) - ((cosh ((z - y) - (w - z))) * (sinh (y - w))))) .= (1 / 2) * (((1 / 2) * (((sinh (2 * (y - z))) + (sinh (2 * (z - w)))) + (sinh (2 * (w - y))))) + (((1 / 2) * ((sinh ((w - y) + (- (w - y)))) - (sinh ((w - y) - (y - w))))) - ((cosh ((z - y) - (w - z))) * (sinh (y - w))))) by Th11 .= (1 / 2) * (((1 / 2) * (((sinh (2 * (y - z))) + (sinh (2 * (z - w)))) + (sinh (2 * (w - y))))) + (((1 / 2) * (0 - (sinh ((w - y) - (y - w))))) - ((cosh ((z - y) - (w - z))) * (sinh (y - w))))) by SIN_COS2:16, SIN_COS2:def_2 .= (1 / 2) * (((1 / 2) * (((sinh (2 * (y - z))) + (sinh (2 * (z - w)))) + (sinh (2 * (w - y))))) + (((1 / 2) * (- (sinh (2 * (w - y))))) - ((1 / 2) * ((sinh (((z - y) + (z - w)) + (y - w))) - (sinh (((z - y) + (z - w)) - (y - w))))))) by Th11 .= (1 / 2) * (((1 / 2) * (((sinh (2 * (y - z))) + (sinh (2 * (z - w)))) + (sinh (2 * (w - y))))) + ((1 / 2) * (((sinh (- (2 * (y - z)))) - (sinh (2 * (z - w)))) + (- (sinh (2 * (w - y))))))) .= (1 / 2) * (((1 / 2) * (((sinh (2 * (y - z))) + (sinh (2 * (z - w)))) + (sinh (2 * (w - y))))) + ((1 / 2) * (((- (sinh (2 * (y - z)))) - (sinh (2 * (z - w)))) + (- (sinh (2 * (w - y))))))) by Lm8 ; hence (((((sinh y) * (sinh z)) * (sinh (z - y))) + (((sinh z) * (sinh w)) * (sinh (w - z)))) + (((sinh w) * (sinh y)) * (sinh (y - w)))) + (((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w))) = 0 ; ::_thesis: verum end; theorem Th24: :: SIN_COS8:24 for x being real number st x >= 0 holds sinh (x / 2) = sqrt (((cosh x) - 1) / 2) proof let x be real number ; ::_thesis: ( x >= 0 implies sinh (x / 2) = sqrt (((cosh x) - 1) / 2) ) assume x >= 0 ; ::_thesis: sinh (x / 2) = sqrt (((cosh x) - 1) / 2) then sinh (x / 2) = sqrt ((sinh (x / 2)) ^2) by SIN_COS5:46, SQUARE_1:22 .= sqrt ((sinh . (x / 2)) ^2) by SIN_COS2:def_2 .= sqrt ((1 / 2) * ((cosh . (2 * (x / 2))) - 1)) by SIN_COS2:18 .= sqrt (((cosh . x) - 1) / 2) .= sqrt (((cosh x) - 1) / 2) by SIN_COS2:def_4 ; hence sinh (x / 2) = sqrt (((cosh x) - 1) / 2) ; ::_thesis: verum end; theorem Th25: :: SIN_COS8:25 for x being real number st x < 0 holds sinh (x / 2) = - (sqrt (((cosh x) - 1) / 2)) proof let x be real number ; ::_thesis: ( x < 0 implies sinh (x / 2) = - (sqrt (((cosh x) - 1) / 2)) ) assume x < 0 ; ::_thesis: sinh (x / 2) = - (sqrt (((cosh x) - 1) / 2)) then A1: x / 2 < 0 by XREAL_1:141; sinh (x / 2) = - (- (sinh (x / 2))) .= - (sqrt ((sinh (x / 2)) ^2)) by A1, SIN_COS5:47, SQUARE_1:23 .= - (sqrt ((sinh . (x / 2)) ^2)) by SIN_COS2:def_2 .= - (sqrt ((1 / 2) * ((cosh . (2 * (x / 2))) - 1))) by SIN_COS2:18 .= - (sqrt (((cosh . x) - 1) / 2)) .= - (sqrt (((cosh x) - 1) / 2)) by SIN_COS2:def_4 ; hence sinh (x / 2) = - (sqrt (((cosh x) - 1) / 2)) ; ::_thesis: verum end; theorem Th26: :: SIN_COS8:26 for x being real number holds ( sinh (2 * x) = (2 * (sinh x)) * (cosh x) & cosh (2 * x) = (2 * ((cosh x) ^2)) - 1 & tanh (2 * x) = (2 * (tanh x)) / (1 + ((tanh x) ^2)) ) proof let x be real number ; ::_thesis: ( sinh (2 * x) = (2 * (sinh x)) * (cosh x) & cosh (2 * x) = (2 * ((cosh x) ^2)) - 1 & tanh (2 * x) = (2 * (tanh x)) / (1 + ((tanh x) ^2)) ) A1: cosh (2 * x) = cosh . (2 * x) by SIN_COS2:def_4 .= (2 * ((cosh . x) ^2)) - 1 by SIN_COS2:23 .= (2 * ((cosh x) ^2)) - 1 by SIN_COS2:def_4 ; A2: tanh (2 * x) = tanh . (2 * x) by SIN_COS2:def_6 .= (2 * (tanh . x)) / (1 + ((tanh . x) ^2)) by SIN_COS2:23 .= (2 * (tanh x)) / (1 + ((tanh . x) ^2)) by SIN_COS2:def_6 .= (2 * (tanh x)) / (1 + ((tanh x) ^2)) by SIN_COS2:def_6 ; sinh (2 * x) = sinh . (2 * x) by SIN_COS2:def_2 .= (2 * (sinh . x)) * (cosh . x) by SIN_COS2:23 .= (2 * (sinh x)) * (cosh . x) by SIN_COS2:def_2 .= (2 * (sinh x)) * (cosh x) by SIN_COS2:def_4 ; hence ( sinh (2 * x) = (2 * (sinh x)) * (cosh x) & cosh (2 * x) = (2 * ((cosh x) ^2)) - 1 & tanh (2 * x) = (2 * (tanh x)) / (1 + ((tanh x) ^2)) ) by A1, A2; ::_thesis: verum end; theorem Th27: :: SIN_COS8:27 for x being real number holds ( sinh (2 * x) = (2 * (tanh x)) / (1 - ((tanh x) ^2)) & sinh (3 * x) = (sinh x) * ((4 * ((cosh x) ^2)) - 1) & sinh (3 * x) = (3 * (sinh x)) - ((2 * (sinh x)) * (1 - (cosh (2 * x)))) & cosh (2 * x) = 1 + (2 * ((sinh x) ^2)) & cosh (2 * x) = ((cosh x) ^2) + ((sinh x) ^2) & cosh (2 * x) = (1 + ((tanh x) ^2)) / (1 - ((tanh x) ^2)) & cosh (3 * x) = (cosh x) * ((4 * ((sinh x) ^2)) + 1) & tanh (3 * x) = ((3 * (tanh x)) + ((tanh x) |^ 3)) / (1 + (3 * ((tanh x) ^2))) ) proof let x be real number ; ::_thesis: ( sinh (2 * x) = (2 * (tanh x)) / (1 - ((tanh x) ^2)) & sinh (3 * x) = (sinh x) * ((4 * ((cosh x) ^2)) - 1) & sinh (3 * x) = (3 * (sinh x)) - ((2 * (sinh x)) * (1 - (cosh (2 * x)))) & cosh (2 * x) = 1 + (2 * ((sinh x) ^2)) & cosh (2 * x) = ((cosh x) ^2) + ((sinh x) ^2) & cosh (2 * x) = (1 + ((tanh x) ^2)) / (1 - ((tanh x) ^2)) & cosh (3 * x) = (cosh x) * ((4 * ((sinh x) ^2)) + 1) & tanh (3 * x) = ((3 * (tanh x)) + ((tanh x) |^ 3)) / (1 + (3 * ((tanh x) ^2))) ) A1: cosh x <> 0 by Lm1; A2: sinh (2 * x) = (2 * (sinh x)) * (cosh x) by Th26 .= ((2 * (sinh x)) * (cosh x)) * ((cosh x) / (cosh x)) by A1, XCMPLX_1:88 .= (((2 * (sinh x)) * (cosh x)) * (cosh x)) / (cosh x) by XCMPLX_1:74 .= ((2 * (sinh x)) * ((cosh x) * (cosh x))) / (cosh x) .= ((2 * (sinh x)) / (cosh x)) * ((cosh x) * (cosh x)) by XCMPLX_1:74 .= (2 * ((sinh x) / (cosh x))) * ((cosh x) * (cosh x)) by XCMPLX_1:74 .= (2 * (tanh x)) * ((cosh x) * (cosh x)) by Th1 .= (2 * (tanh x)) / (1 / ((cosh x) * (cosh x))) by XCMPLX_1:100 .= (2 * (tanh x)) / ((((cosh x) * (cosh x)) - ((sinh x) ^2)) / ((cosh x) * (cosh x))) by Lm3 .= (2 * (tanh x)) / ((((cosh x) * (cosh x)) / ((cosh x) * (cosh x))) - (((sinh x) * (sinh x)) / ((cosh x) * (cosh x)))) by XCMPLX_1:120 .= (2 * (tanh x)) / ((((cosh x) / (cosh x)) * ((cosh x) / (cosh x))) - (((sinh x) * (sinh x)) / ((cosh x) * (cosh x)))) by XCMPLX_1:76 .= (2 * (tanh x)) / ((1 * ((cosh x) / (cosh x))) - (((sinh x) * (sinh x)) / ((cosh x) * (cosh x)))) by A1, XCMPLX_1:60 .= (2 * (tanh x)) / (1 - (((sinh x) * (sinh x)) / ((cosh x) * (cosh x)))) by A1, XCMPLX_1:60 .= (2 * (tanh x)) / (1 - (((sinh x) / (cosh x)) * ((sinh x) / (cosh x)))) by XCMPLX_1:76 .= (2 * (tanh x)) / (1 - ((tanh x) * ((sinh x) / (cosh x)))) by Th1 .= (2 * (tanh x)) / (1 - ((tanh x) ^2)) by Th1 ; A3: cosh (3 * x) = (4 * ((cosh x) |^ (2 + 1))) - (3 * (cosh x)) by SIN_COS5:44 .= (4 * (((cosh x) |^ 2) * (cosh x))) - (3 * (cosh x)) by NEWTON:6 .= ((4 * ((cosh x) |^ (1 + 1))) - 3) * (cosh x) .= ((4 * (((cosh x) |^ 1) * (cosh x))) - 3) * (cosh x) by NEWTON:6 .= ((4 * ((((cosh x) ^2) - ((sinh x) ^2)) + ((sinh x) ^2))) - 3) * (cosh x) by NEWTON:5 .= ((4 * (1 + ((sinh x) ^2))) - 3) * (cosh x) by Lm3 .= (cosh x) * ((4 * ((sinh x) ^2)) + 1) ; A4: cosh (2 * x) = (2 * ((((cosh x) ^2) - ((sinh x) ^2)) + ((sinh x) ^2))) - 1 by Th26 .= (2 * (1 + ((sinh x) ^2))) - 1 by Lm3 .= 1 + (2 * ((sinh x) ^2)) ; A5: tanh (3 * x) = tanh ((x + x) + x) .= ((((tanh x) + (tanh x)) + (tanh x)) + (((tanh x) * (tanh x)) * (tanh x))) / (((1 + ((tanh x) * (tanh x))) + ((tanh x) * (tanh x))) + ((tanh x) * (tanh x))) by Th21 .= ((3 * (tanh x)) + ((((tanh x) |^ 1) * (tanh x)) * (tanh x))) / (((1 + ((tanh x) * (tanh x))) + ((tanh x) * (tanh x))) + ((tanh x) * (tanh x))) by NEWTON:5 .= ((3 * (tanh x)) + (((tanh x) |^ (1 + 1)) * (tanh x))) / (((1 + ((tanh x) * (tanh x))) + ((tanh x) * (tanh x))) + ((tanh x) * (tanh x))) by NEWTON:6 .= ((3 * (tanh x)) + ((tanh x) |^ ((1 + 1) + 1))) / (((1 + ((tanh x) * (tanh x))) + ((tanh x) * (tanh x))) + ((tanh x) * (tanh x))) by NEWTON:6 .= ((3 * (tanh x)) + ((tanh x) |^ 3)) / (1 + (3 * ((tanh x) ^2))) ; A6: cosh x <> 0 by Lm1; A7: cosh (2 * x) = (2 * ((cosh x) ^2)) - 1 by Th26 .= (2 * ((cosh x) ^2)) - (((cosh x) ^2) - ((sinh x) ^2)) by Lm3 .= ((cosh x) ^2) + ((sinh x) ^2) ; then A8: cosh (2 * x) = ((1 / (sech x)) ^2) + ((sinh x) ^2) by Th2 .= (1 / ((sech x) ^2)) + (((sinh x) ^2) * (1 ^2)) by XCMPLX_1:76 .= (1 / ((sech x) ^2)) + ((((sinh x) ^2) / ((cosh x) ^2)) * ((cosh x) ^2)) by A6, XCMPLX_1:6, XCMPLX_1:87 .= (1 / ((sech x) ^2)) + ((((sinh x) / (cosh x)) ^2) * ((cosh x) ^2)) by XCMPLX_1:76 .= (1 / ((sech x) ^2)) + (((tanh x) ^2) * ((cosh x) ^2)) by Th1 .= (1 / ((sech x) ^2)) + (((tanh x) ^2) / ((1 ^2) / ((cosh x) ^2))) by XCMPLX_1:100 .= (1 / ((sech x) ^2)) + (((tanh x) ^2) / ((1 / (cosh x)) ^2)) by XCMPLX_1:76 .= (1 / ((sech x) ^2)) + (((tanh x) ^2) / ((sech x) ^2)) by SIN_COS5:def_2 .= (1 + ((tanh x) ^2)) / ((((sech x) ^2) + ((tanh x) ^2)) - ((tanh x) ^2)) by XCMPLX_1:62 .= (1 + ((tanh x) ^2)) / (1 - ((tanh x) ^2)) by SIN_COS5:38 ; A9: sinh (3 * x) = (4 * ((sinh x) |^ (2 + 1))) + (3 * (sinh x)) by SIN_COS5:43 .= (4 * (((sinh x) |^ 2) * (sinh x))) + (3 * (sinh x)) by NEWTON:6 .= (sinh x) * ((4 * ((sinh x) |^ (1 + 1))) + 3) .= (sinh x) * ((4 * (((sinh x) |^ 1) * (sinh x))) + 3) by NEWTON:6 .= (sinh x) * ((4 * (((cosh x) ^2) - (((cosh x) ^2) - ((sinh x) ^2)))) + 3) by NEWTON:5 .= (sinh x) * ((4 * (((cosh x) ^2) - 1)) + 3) by Lm3 .= (sinh x) * ((4 * ((cosh x) ^2)) - 1) ; then sinh (3 * x) = ((sinh x) * (4 * ((((cosh x) ^2) - ((sinh x) ^2)) + ((sinh x) ^2)))) - (sinh x) .= ((sinh x) * (4 * (1 + ((sinh x) ^2)))) - (sinh x) by Lm3 .= ((4 * (sinh x)) + ((sinh x) * ((2 * (((cosh x) ^2) - (((cosh x) ^2) - ((sinh x) ^2)))) + (2 * ((sinh x) ^2))))) - (sinh x) .= ((4 * (sinh x)) + ((sinh x) * ((2 * (((cosh x) ^2) - 1)) + (2 * ((sinh x) ^2))))) - (sinh x) by Lm3 .= ((4 * (sinh x)) + ((sinh x) * (2 * ((((cosh x) * (cosh x)) + ((sinh x) ^2)) - 1)))) - (sinh x) .= ((4 * (sinh x)) + ((sinh x) * (2 * ((cosh (x + x)) - 1)))) - (sinh x) by Lm10 .= (3 * (sinh x)) - ((2 * (sinh x)) * (1 - (cosh (2 * x)))) ; hence ( sinh (2 * x) = (2 * (tanh x)) / (1 - ((tanh x) ^2)) & sinh (3 * x) = (sinh x) * ((4 * ((cosh x) ^2)) - 1) & sinh (3 * x) = (3 * (sinh x)) - ((2 * (sinh x)) * (1 - (cosh (2 * x)))) & cosh (2 * x) = 1 + (2 * ((sinh x) ^2)) & cosh (2 * x) = ((cosh x) ^2) + ((sinh x) ^2) & cosh (2 * x) = (1 + ((tanh x) ^2)) / (1 - ((tanh x) ^2)) & cosh (3 * x) = (cosh x) * ((4 * ((sinh x) ^2)) + 1) & tanh (3 * x) = ((3 * (tanh x)) + ((tanh x) |^ 3)) / (1 + (3 * ((tanh x) ^2))) ) by A2, A9, A4, A7, A8, A3, A5; ::_thesis: verum end; theorem :: SIN_COS8:28 for x being real number holds (((sinh (5 * x)) + (2 * (sinh (3 * x)))) + (sinh x)) / (((sinh (7 * x)) + (2 * (sinh (5 * x)))) + (sinh (3 * x))) = (sinh (3 * x)) / (sinh (5 * x)) proof let x be real number ; ::_thesis: (((sinh (5 * x)) + (2 * (sinh (3 * x)))) + (sinh x)) / (((sinh (7 * x)) + (2 * (sinh (5 * x)))) + (sinh (3 * x))) = (sinh (3 * x)) / (sinh (5 * x)) (((sinh (5 * x)) + (2 * (sinh (3 * x)))) + (sinh x)) / (((sinh (7 * x)) + (2 * (sinh (5 * x)))) + (sinh (3 * x))) = (((sinh ((3 * x) + (2 * x))) + (2 * (sinh (3 * x)))) + (sinh x)) / (((sinh ((5 + 2) * x)) + (2 * (sinh (5 * x)))) + (sinh (3 * x))) .= (((((sinh (3 * x)) * (cosh (2 * x))) + ((cosh (3 * x)) * (sinh (2 * x)))) + (2 * (sinh (3 * x)))) + (sinh x)) / (((sinh ((5 + 2) * x)) + (2 * (sinh (5 * x)))) + (sinh (3 * x))) by Lm10 .= (((sinh (3 * x)) * ((cosh (2 * x)) + 2)) + (((cosh ((2 * x) + (1 * x))) * (sinh (2 * x))) + (sinh x))) / (((sinh ((5 * x) + (2 * x))) + (2 * (sinh (5 * x)))) + (sinh (3 * x))) .= (((sinh (3 * x)) * ((cosh (2 * x)) + 2)) + (((((cosh (2 * x)) * (cosh x)) + ((sinh (2 * x)) * (sinh x))) * (sinh (2 * x))) + (sinh x))) / (((sinh ((5 * x) + (2 * x))) + (2 * (sinh (5 * x)))) + (sinh (3 * x))) by Lm10 .= (((sinh (3 * x)) * ((cosh (2 * x)) + 2)) + ((((cosh (2 * x)) * (cosh x)) * (sinh (2 * x))) + ((((sinh (2 * x)) ^2) + 1) * (sinh x)))) / (((sinh ((5 * x) + (2 * x))) + (2 * (sinh (5 * x)))) + (sinh (3 * x))) .= (((sinh (3 * x)) * ((cosh (2 * x)) + 2)) + ((((cosh (2 * x)) * (cosh x)) * (sinh (2 * x))) + (((((cosh (2 * x)) ^2) - ((sinh (2 * x)) ^2)) + ((sinh (2 * x)) ^2)) * (sinh x)))) / (((sinh ((5 * x) + (2 * x))) + (2 * (sinh (5 * x)))) + (sinh (3 * x))) by Lm3 .= (((sinh (3 * x)) * ((cosh (2 * x)) + 2)) + ((cosh (2 * x)) * (((sinh (2 * x)) * (cosh x)) + ((cosh (2 * x)) * (sinh x))))) / (((sinh ((5 * x) + (2 * x))) + (2 * (sinh (5 * x)))) + (sinh (3 * x))) .= (((sinh (3 * x)) * ((cosh (2 * x)) + 2)) + ((cosh (2 * x)) * (sinh ((2 * x) + (1 * x))))) / (((sinh ((5 * x) + (2 * x))) + (2 * (sinh (5 * x)))) + (sinh (3 * x))) by Lm10 .= ((sinh (3 * x)) * (((cosh (2 * x)) + 2) + (cosh (2 * x)))) / (((((sinh (5 * x)) * (cosh (2 * x))) + ((cosh (5 * x)) * (sinh (2 * x)))) + ((sinh (5 * x)) * 2)) + (sinh (3 * x))) by Lm10 .= ((sinh (3 * x)) * (((cosh (2 * x)) + 2) + (cosh (2 * x)))) / (((sinh (5 * x)) * ((cosh (2 * x)) + 2)) + (((cosh ((3 * x) + (2 * x))) * (sinh (2 * x))) + (sinh (3 * x)))) .= ((sinh (3 * x)) * (((cosh (2 * x)) + 2) + (cosh (2 * x)))) / (((sinh (5 * x)) * ((cosh (2 * x)) + 2)) + (((((cosh (3 * x)) * (cosh (2 * x))) + ((sinh (3 * x)) * (sinh (2 * x)))) * (sinh (2 * x))) + (sinh (3 * x)))) by Lm10 .= ((sinh (3 * x)) * (((cosh (2 * x)) + 2) + (cosh (2 * x)))) / (((sinh (5 * x)) * ((cosh (2 * x)) + 2)) + ((((cosh (3 * x)) * (cosh (2 * x))) * (sinh (2 * x))) + ((sinh (3 * x)) * (((sinh (2 * x)) ^2) + 1)))) .= ((sinh (3 * x)) * (((cosh (2 * x)) + 2) + (cosh (2 * x)))) / (((sinh (5 * x)) * ((cosh (2 * x)) + 2)) + ((((cosh (3 * x)) * (cosh (2 * x))) * (sinh (2 * x))) + ((sinh (3 * x)) * ((((cosh (2 * x)) ^2) - ((sinh (2 * x)) ^2)) + ((sinh (2 * x)) ^2))))) by Lm3 .= ((sinh (3 * x)) * (((cosh (2 * x)) + 2) + (cosh (2 * x)))) / (((sinh (5 * x)) * ((cosh (2 * x)) + 2)) + ((cosh (2 * x)) * (((sinh (2 * x)) * (cosh (3 * x))) + ((cosh (2 * x)) * (sinh (3 * x)))))) .= ((sinh (3 * x)) * (((cosh (2 * x)) + 2) + (cosh (2 * x)))) / (((sinh (5 * x)) * ((cosh (2 * x)) + 2)) + ((cosh (2 * x)) * (sinh ((2 * x) + (3 * x))))) by Lm10 .= ((sinh (3 * x)) * (((cosh (2 * x)) + 2) + (cosh (2 * x)))) / ((sinh (5 * x)) * (((cosh (2 * x)) + 2) + (cosh (2 * x)))) .= (sinh (3 * x)) / (sinh (5 * x)) by Lm13, XCMPLX_1:91 ; hence (((sinh (5 * x)) + (2 * (sinh (3 * x)))) + (sinh x)) / (((sinh (7 * x)) + (2 * (sinh (5 * x)))) + (sinh (3 * x))) = (sinh (3 * x)) / (sinh (5 * x)) ; ::_thesis: verum end; theorem :: SIN_COS8:29 for x being real number st x >= 0 holds tanh (x / 2) = sqrt (((cosh x) - 1) / ((cosh x) + 1)) proof let x be real number ; ::_thesis: ( x >= 0 implies tanh (x / 2) = sqrt (((cosh x) - 1) / ((cosh x) + 1)) ) assume A1: x >= 0 ; ::_thesis: tanh (x / 2) = sqrt (((cosh x) - 1) / ((cosh x) + 1)) A2: ( (cosh x) + 1 > 0 & (cosh x) - 1 >= 0 ) by Lm13; tanh (x / 2) = (sinh (x / 2)) / (cosh (x / 2)) by Th1 .= (sqrt (((cosh x) - 1) / 2)) / (cosh (x / 2)) by A1, Th24 .= (sqrt (((cosh x) - 1) / 2)) / (sqrt (((cosh x) + 1) / 2)) by SIN_COS5:48 .= sqrt ((((cosh x) - 1) / 2) / (((cosh x) + 1) / 2)) by A2, SQUARE_1:30 .= sqrt (((cosh x) - 1) / ((cosh x) + 1)) by XCMPLX_1:55 ; hence tanh (x / 2) = sqrt (((cosh x) - 1) / ((cosh x) + 1)) ; ::_thesis: verum end; theorem :: SIN_COS8:30 for x being real number st x < 0 holds tanh (x / 2) = - (sqrt (((cosh x) - 1) / ((cosh x) + 1))) proof let x be real number ; ::_thesis: ( x < 0 implies tanh (x / 2) = - (sqrt (((cosh x) - 1) / ((cosh x) + 1))) ) assume A1: x < 0 ; ::_thesis: tanh (x / 2) = - (sqrt (((cosh x) - 1) / ((cosh x) + 1))) A2: ( (cosh x) + 1 > 0 & (cosh x) - 1 >= 0 ) by Lm13; tanh (x / 2) = (sinh (x / 2)) / (cosh (x / 2)) by Th1 .= (- (sqrt (((cosh x) - 1) / 2))) / (cosh (x / 2)) by A1, Th25 .= - ((sqrt (((cosh x) - 1) / 2)) / (cosh (x / 2))) by XCMPLX_1:187 .= - ((sqrt (((cosh x) - 1) / 2)) / (sqrt (((cosh x) + 1) / 2))) by SIN_COS5:48 .= - (sqrt ((((cosh x) - 1) / 2) / (((cosh x) + 1) / 2))) by A2, SQUARE_1:30 .= - (sqrt (((cosh x) - 1) / ((cosh x) + 1))) by XCMPLX_1:55 ; hence tanh (x / 2) = - (sqrt (((cosh x) - 1) / ((cosh x) + 1))) ; ::_thesis: verum end; theorem :: SIN_COS8:31 for x being real number holds ( (sinh x) |^ 3 = ((sinh (3 * x)) - (3 * (sinh x))) / 4 & (sinh x) |^ 4 = (((cosh (4 * x)) - (4 * (cosh (2 * x)))) + 3) / 8 & (sinh x) |^ 5 = (((sinh (5 * x)) - (5 * (sinh (3 * x)))) + (10 * (sinh x))) / 16 & (sinh x) |^ 6 = ((((cosh (6 * x)) - (6 * (cosh (4 * x)))) + (15 * (cosh (2 * x)))) - 10) / 32 & (sinh x) |^ 7 = ((((sinh (7 * x)) - (7 * (sinh (5 * x)))) + (21 * (sinh (3 * x)))) - (35 * (sinh x))) / 64 & (sinh x) |^ 8 = (((((cosh (8 * x)) - (8 * (cosh (6 * x)))) + (28 * (cosh (4 * x)))) - (56 * (cosh (2 * x)))) + 35) / 128 ) proof let x be real number ; ::_thesis: ( (sinh x) |^ 3 = ((sinh (3 * x)) - (3 * (sinh x))) / 4 & (sinh x) |^ 4 = (((cosh (4 * x)) - (4 * (cosh (2 * x)))) + 3) / 8 & (sinh x) |^ 5 = (((sinh (5 * x)) - (5 * (sinh (3 * x)))) + (10 * (sinh x))) / 16 & (sinh x) |^ 6 = ((((cosh (6 * x)) - (6 * (cosh (4 * x)))) + (15 * (cosh (2 * x)))) - 10) / 32 & (sinh x) |^ 7 = ((((sinh (7 * x)) - (7 * (sinh (5 * x)))) + (21 * (sinh (3 * x)))) - (35 * (sinh x))) / 64 & (sinh x) |^ 8 = (((((cosh (8 * x)) - (8 * (cosh (6 * x)))) + (28 * (cosh (4 * x)))) - (56 * (cosh (2 * x)))) + 35) / 128 ) A1: (sinh x) |^ 3 = (((4 * ((sinh x) |^ 3)) + (3 * (sinh x))) - (3 * (sinh x))) / 4 .= ((sinh (3 * x)) - (3 * (sinh x))) / 4 by SIN_COS5:43 ; then A2: (sinh x) |^ 4 = (((sinh (3 * x)) - (3 * (sinh x))) / 4) * (sinh x) by POLYEQ_2:4 .= (((sinh (3 * x)) * (sinh x)) - (3 * ((sinh x) * (sinh x)))) / 4 .= (((1 / 2) * ((cosh ((3 * x) + (1 * x))) - (cosh ((3 * x) - (1 * x))))) - (3 * ((sinh x) * (sinh x)))) / 4 by Th11 .= (((1 / 2) * ((cosh (4 * x)) - (cosh (2 * x)))) - (((sinh x) ^2) * 3)) / 4 .= (((1 / 2) * ((cosh (4 * x)) - (cosh (2 * x)))) - (((1 / 2) * ((cosh (2 * x)) - 1)) * 3)) / 4 by Lm7 .= (((cosh (4 * x)) - (4 * (cosh (2 * x)))) + 3) / 8 ; A3: (sinh x) |^ 5 = (sinh x) |^ (4 + 1) .= ((((cosh (4 * x)) - (4 * (cosh (2 * x)))) + 3) / 8) * (sinh x) by A2, NEWTON:6 .= ((((cosh (4 * x)) * (sinh x)) - (4 * ((cosh (2 * x)) * (sinh x)))) + (3 * (sinh x))) / 8 .= ((((1 / 2) * ((sinh ((4 * x) + (1 * x))) - (sinh ((4 * x) - (1 * x))))) - (4 * ((cosh (2 * x)) * (sinh x)))) + (3 * (sinh x))) / 8 by Th11 .= ((((1 / 2) * ((sinh (5 * x)) - (sinh (3 * x)))) - (4 * ((1 / 2) * ((sinh ((2 * x) + (1 * x))) - (sinh ((2 * x) - (1 * x))))))) + (3 * (sinh x))) / 8 by Th11 .= (((sinh (5 * x)) - (5 * (sinh (3 * x)))) + (10 * (sinh x))) / 16 ; A4: (sinh x) |^ 6 = (sinh x) |^ (5 + 1) .= ((((sinh (5 * x)) - (5 * (sinh (3 * x)))) + (10 * (sinh x))) / 16) * (sinh x) by A3, NEWTON:6 .= ((((sinh (5 * x)) * (sinh x)) - (5 * ((sinh (3 * x)) * (sinh x)))) + (10 * ((sinh x) * (sinh x)))) / 16 .= ((((1 / 2) * ((cosh ((5 * x) + (1 * x))) - (cosh ((5 * x) - (1 * x))))) - (5 * ((sinh (3 * x)) * (sinh x)))) + (10 * ((sinh x) * (sinh x)))) / 16 by Th11 .= ((((1 / 2) * ((cosh (6 * x)) - (cosh (4 * x)))) - (((1 / 2) * ((cosh ((3 * x) + (1 * x))) - (cosh ((3 * x) - (1 * x))))) * 5)) + (10 * ((sinh x) * (sinh x)))) / 16 by Th11 .= (((1 / 2) * (((cosh (6 * x)) - (6 * (cosh (4 * x)))) + ((cosh (2 * x)) * 5))) + (10 * ((sinh x) ^2))) / 16 .= (((1 / 2) * (((cosh (6 * x)) - (6 * (cosh (4 * x)))) + ((cosh (2 * x)) * 5))) + (((1 / 2) * ((cosh (2 * x)) - 1)) * 10)) / 16 by Lm7 .= ((((cosh (6 * x)) - (6 * (cosh (4 * x)))) + (15 * (cosh (2 * x)))) - 10) / 32 ; A5: (sinh x) |^ 7 = (sinh x) |^ (6 + 1) .= (((((cosh (6 * x)) - (6 * (cosh (4 * x)))) + (15 * (cosh (2 * x)))) - 10) / 32) * (sinh x) by A4, NEWTON:6 .= (((((cosh (6 * x)) * (sinh x)) - ((6 * (cosh (4 * x))) * (sinh x))) + ((15 * (cosh (2 * x))) * (sinh x))) - (10 * (sinh x))) / 32 .= (((((1 / 2) * ((sinh ((6 * x) + (1 * x))) - (sinh ((6 * x) - (1 * x))))) - ((6 * (cosh (4 * x))) * (sinh x))) + ((15 * (cosh (2 * x))) * (sinh x))) - (10 * (sinh x))) / 32 by Th11 .= (((((1 / 2) * ((sinh (7 * x)) - (sinh (5 * x)))) - (6 * ((cosh (4 * x)) * (sinh x)))) + ((15 * (cosh (2 * x))) * (sinh x))) - (10 * (sinh x))) / 32 .= (((((1 / 2) * ((sinh (7 * x)) - (sinh (5 * x)))) - (6 * ((1 / 2) * ((sinh ((4 * x) + (1 * x))) - (sinh ((4 * x) - (1 * x))))))) + ((15 * (cosh (2 * x))) * (sinh x))) - (10 * (sinh x))) / 32 by Th11 .= ((((1 / 2) * (((sinh (7 * x)) - (7 * (sinh (5 * x)))) + ((sinh (3 * x)) * 6))) + (15 * ((cosh (2 * x)) * (sinh x)))) - (10 * (sinh x))) / 32 .= ((((1 / 2) * (((sinh (7 * x)) - (7 * (sinh (5 * x)))) + ((sinh (3 * x)) * 6))) + (15 * ((1 / 2) * ((sinh ((2 * x) + (1 * x))) - (sinh ((2 * x) - (1 * x))))))) - (10 * (sinh x))) / 32 by Th11 .= ((((sinh (7 * x)) - (7 * (sinh (5 * x)))) + (21 * (sinh (3 * x)))) - (35 * (sinh x))) / 64 ; (sinh x) |^ 8 = (sinh x) |^ (7 + 1) .= (((((sinh (7 * x)) - (7 * (sinh (5 * x)))) + (21 * (sinh (3 * x)))) - (35 * (sinh x))) / 64) * (sinh x) by A5, NEWTON:6 .= (((((sinh (7 * x)) * (sinh x)) - (7 * ((sinh (5 * x)) * (sinh x)))) + (21 * ((sinh (3 * x)) * (sinh x)))) - (35 * ((sinh x) * (sinh x)))) / 64 .= (((((1 / 2) * ((cosh ((7 * x) + (1 * x))) - (cosh ((7 * x) - (1 * x))))) - (7 * ((sinh (5 * x)) * (sinh x)))) + (21 * ((sinh (3 * x)) * (sinh x)))) - (35 * ((sinh x) * (sinh x)))) / 64 by Th11 .= (((((1 / 2) * ((cosh (8 * x)) - (cosh (6 * x)))) - (((1 / 2) * ((cosh ((5 * x) + (1 * x))) - (cosh ((5 * x) - (1 * x))))) * 7)) + (21 * ((sinh (3 * x)) * (sinh x)))) - (35 * ((sinh x) * (sinh x)))) / 64 by Th11 .= ((((1 / 2) * (((cosh (8 * x)) - (8 * (cosh (6 * x)))) + ((cosh (4 * x)) * 7))) + (((1 / 2) * ((cosh ((3 * x) + (1 * x))) - (cosh ((3 * x) - (1 * x))))) * 21)) - (35 * ((sinh x) * (sinh x)))) / 64 by Th11 .= (((1 / 2) * ((((cosh (8 * x)) - (8 * (cosh (6 * x)))) + (28 * (cosh (4 * x)))) + (- ((cosh (2 * x)) * 21)))) - (35 * ((sinh x) ^2))) / 64 .= (((1 / 2) * ((((cosh (8 * x)) - (8 * (cosh (6 * x)))) + (28 * (cosh (4 * x)))) + (- ((cosh (2 * x)) * 21)))) - (((1 / 2) * ((cosh (2 * x)) - 1)) * 35)) / 64 by Lm7 .= (((((cosh (8 * x)) - (8 * (cosh (6 * x)))) + (28 * (cosh (4 * x)))) - (56 * (cosh (2 * x)))) + 35) / 128 ; hence ( (sinh x) |^ 3 = ((sinh (3 * x)) - (3 * (sinh x))) / 4 & (sinh x) |^ 4 = (((cosh (4 * x)) - (4 * (cosh (2 * x)))) + 3) / 8 & (sinh x) |^ 5 = (((sinh (5 * x)) - (5 * (sinh (3 * x)))) + (10 * (sinh x))) / 16 & (sinh x) |^ 6 = ((((cosh (6 * x)) - (6 * (cosh (4 * x)))) + (15 * (cosh (2 * x)))) - 10) / 32 & (sinh x) |^ 7 = ((((sinh (7 * x)) - (7 * (sinh (5 * x)))) + (21 * (sinh (3 * x)))) - (35 * (sinh x))) / 64 & (sinh x) |^ 8 = (((((cosh (8 * x)) - (8 * (cosh (6 * x)))) + (28 * (cosh (4 * x)))) - (56 * (cosh (2 * x)))) + 35) / 128 ) by A1, A2, A3, A4, A5; ::_thesis: verum end; theorem :: SIN_COS8:32 for x being real number holds ( (cosh x) |^ 3 = ((cosh (3 * x)) + (3 * (cosh x))) / 4 & (cosh x) |^ 4 = (((cosh (4 * x)) + (4 * (cosh (2 * x)))) + 3) / 8 & (cosh x) |^ 5 = (((cosh (5 * x)) + (5 * (cosh (3 * x)))) + (10 * (cosh x))) / 16 & (cosh x) |^ 6 = ((((cosh (6 * x)) + (6 * (cosh (4 * x)))) + (15 * (cosh (2 * x)))) + 10) / 32 & (cosh x) |^ 7 = ((((cosh (7 * x)) + (7 * (cosh (5 * x)))) + (21 * (cosh (3 * x)))) + (35 * (cosh x))) / 64 & (cosh x) |^ 8 = (((((cosh (8 * x)) + (8 * (cosh (6 * x)))) + (28 * (cosh (4 * x)))) + (56 * (cosh (2 * x)))) + 35) / 128 ) proof let x be real number ; ::_thesis: ( (cosh x) |^ 3 = ((cosh (3 * x)) + (3 * (cosh x))) / 4 & (cosh x) |^ 4 = (((cosh (4 * x)) + (4 * (cosh (2 * x)))) + 3) / 8 & (cosh x) |^ 5 = (((cosh (5 * x)) + (5 * (cosh (3 * x)))) + (10 * (cosh x))) / 16 & (cosh x) |^ 6 = ((((cosh (6 * x)) + (6 * (cosh (4 * x)))) + (15 * (cosh (2 * x)))) + 10) / 32 & (cosh x) |^ 7 = ((((cosh (7 * x)) + (7 * (cosh (5 * x)))) + (21 * (cosh (3 * x)))) + (35 * (cosh x))) / 64 & (cosh x) |^ 8 = (((((cosh (8 * x)) + (8 * (cosh (6 * x)))) + (28 * (cosh (4 * x)))) + (56 * (cosh (2 * x)))) + 35) / 128 ) A1: (cosh x) |^ 3 = (cosh x) |^ ((1 + 1) + 1) .= ((cosh x) |^ (1 + 1)) * (cosh x) by NEWTON:6 .= (((cosh x) |^ 1) * (cosh x)) * (cosh x) by NEWTON:6 .= ((((cosh x) ^2) * (cosh x)) + (3 * ((cosh x) * ((((cosh x) ^2) - ((sinh x) ^2)) + ((sinh x) ^2))))) / 4 by NEWTON:5 .= ((((cosh x) ^2) * (cosh x)) + (3 * ((cosh x) * (1 + ((sinh x) ^2))))) / 4 by Lm3 .= ((((cosh x) * (((cosh x) * (cosh x)) + ((sinh x) ^2))) + (2 * ((cosh x) * ((sinh x) ^2)))) + (3 * (cosh x))) / 4 .= ((((cosh x) * (cosh (x + x))) + (2 * ((cosh x) * ((sinh x) ^2)))) + (3 * (cosh x))) / 4 by Lm10 .= ((((cosh x) * (cosh (2 * x))) + (((2 * (sinh x)) * (cosh x)) * (sinh x))) + (3 * (cosh x))) / 4 .= ((((cosh (2 * x)) * (cosh x)) + ((sinh (2 * x)) * (sinh x))) + (3 * (cosh x))) / 4 by Th26 .= ((cosh ((x + x) + x)) + (3 * (cosh x))) / 4 by Lm10 .= ((cosh (3 * x)) + (3 * (cosh x))) / 4 ; then A2: (cosh x) |^ 4 = (((cosh (3 * x)) + (3 * (cosh x))) / 4) * (cosh x) by POLYEQ_2:4 .= (((cosh (3 * x)) * (cosh x)) + (3 * ((cosh x) * (cosh x)))) / 4 .= (((1 / 2) * ((cosh ((3 * x) + (1 * x))) + (cosh ((3 * x) - x)))) + (3 * ((cosh x) * (cosh x)))) / 4 by Th11 .= (((1 / 2) * ((cosh (4 * x)) + (cosh (2 * x)))) + (3 * ((1 / 2) * ((cosh (x + x)) + (cosh (x - x)))))) / 4 by Th11 .= (((1 / 2) * ((cosh (4 * x)) + (cosh (2 * x)))) + (((1 / 2) * ((cosh (2 * x)) + 1)) * 3)) / 4 by SIN_COS2:15, SIN_COS2:def_4 .= (((cosh (4 * x)) + (4 * (cosh (2 * x)))) + 3) / 8 ; A3: (cosh x) |^ 5 = (cosh x) |^ (4 + 1) .= ((((cosh (4 * x)) + (4 * (cosh (2 * x)))) + 3) / 8) * (cosh x) by A2, NEWTON:6 .= ((((cosh (4 * x)) * (cosh x)) + (4 * ((cosh (2 * x)) * (cosh x)))) + (3 * (cosh x))) / 8 .= ((((1 / 2) * ((cosh ((4 * x) + (1 * x))) + (cosh ((4 * x) - x)))) + (4 * ((cosh (2 * x)) * (cosh x)))) + (3 * (cosh x))) / 8 by Th11 .= ((((1 / 2) * ((cosh (5 * x)) + (cosh (3 * x)))) + (4 * ((1 / 2) * ((cosh ((2 * x) + (1 * x))) + (cosh ((2 * x) - x)))))) + (3 * (cosh x))) / 8 by Th11 .= (((cosh (5 * x)) + (5 * (cosh (3 * x)))) + (10 * (cosh x))) / 16 ; A4: (cosh x) |^ 6 = (cosh x) |^ (5 + 1) .= ((((cosh (5 * x)) + (5 * (cosh (3 * x)))) + (10 * (cosh x))) / 16) * (cosh x) by A3, NEWTON:6 .= ((((cosh (5 * x)) * (cosh x)) + (5 * ((cosh (3 * x)) * (cosh x)))) + (10 * ((cosh x) * (cosh x)))) / 16 .= ((((1 / 2) * ((cosh ((5 * x) + x)) + (cosh ((5 * x) - x)))) + (5 * ((cosh (3 * x)) * (cosh x)))) + (10 * ((cosh x) * (cosh x)))) / 16 by Th11 .= ((((1 / 2) * ((cosh ((5 * x) + x)) + (cosh ((5 * x) - x)))) + (((1 / 2) * ((cosh ((3 * x) + x)) + (cosh ((3 * x) - x)))) * 5)) + (10 * ((cosh x) * (cosh x)))) / 16 by Th11 .= (((1 / 2) * (((cosh (6 * x)) + (6 * (cosh (4 * x)))) + ((cosh (2 * x)) * 5))) + (10 * ((cosh x) ^2))) / 16 .= (((1 / 2) * (((cosh (6 * x)) + (6 * (cosh (4 * x)))) + ((cosh (2 * x)) * 5))) + (((1 / 2) * ((cosh (2 * x)) + 1)) * 10)) / 16 by Lm7 .= ((((cosh (6 * x)) + (6 * (cosh (4 * x)))) + (15 * (cosh (2 * x)))) + 10) / 32 ; A5: (cosh x) |^ 7 = (cosh x) |^ (6 + 1) .= (((((cosh (6 * x)) + (6 * (cosh (4 * x)))) + (15 * (cosh (2 * x)))) + 10) / 32) * (cosh x) by A4, NEWTON:6 .= (((((cosh (6 * x)) * (cosh x)) + (6 * ((cosh (4 * x)) * (cosh x)))) + (15 * ((cosh (2 * x)) * (cosh x)))) + (10 * (cosh x))) / 32 .= (((((1 / 2) * ((cosh ((6 * x) + (1 * x))) + (cosh ((6 * x) - (1 * x))))) + (6 * ((cosh (4 * x)) * (cosh x)))) + (15 * ((cosh (2 * x)) * (cosh x)))) + (10 * (cosh x))) / 32 by Th11 .= (((((1 / 2) * ((cosh (7 * x)) + (cosh (5 * x)))) + (((1 / 2) * ((cosh ((4 * x) + x)) + (cosh ((4 * x) - x)))) * 6)) + (15 * ((cosh (2 * x)) * (cosh x)))) + (10 * (cosh x))) / 32 by Th11 .= ((((1 / 2) * (((cosh (7 * x)) + (7 * (cosh (5 * x)))) + ((cosh (3 * x)) * 6))) + (((1 / 2) * ((cosh ((2 * x) + x)) + (cosh ((2 * x) - x)))) * 15)) + (10 * (cosh x))) / 32 by Th11 .= ((((cosh (7 * x)) + (7 * (cosh (5 * x)))) + (21 * (cosh (3 * x)))) + (35 * (cosh x))) / 64 ; (cosh x) |^ 8 = (cosh x) |^ (7 + 1) .= (((((cosh (7 * x)) + (7 * (cosh (5 * x)))) + (21 * (cosh (3 * x)))) + (35 * (cosh x))) / 64) * (cosh x) by A5, NEWTON:6 .= (((((cosh (7 * x)) * (cosh x)) + ((7 * (cosh (5 * x))) * (cosh x))) + ((21 * (cosh (3 * x))) * (cosh x))) + (35 * ((cosh x) ^2))) / 64 .= (((((1 / 2) * ((cosh ((7 * x) + (1 * x))) + (cosh ((7 * x) - x)))) + ((7 * (cosh (5 * x))) * (cosh x))) + ((21 * (cosh (3 * x))) * (cosh x))) + (35 * ((cosh x) ^2))) / 64 by Th11 .= (((((1 / 2) * ((cosh (8 * x)) + (cosh (6 * x)))) + (7 * ((cosh (5 * x)) * (cosh x)))) + ((21 * (cosh (3 * x))) * (cosh x))) + (35 * ((cosh x) ^2))) / 64 .= (((((1 / 2) * ((cosh (8 * x)) + (cosh (6 * x)))) + (7 * ((1 / 2) * ((cosh ((5 * x) + (1 * x))) + (cosh ((5 * x) - (1 * x))))))) + ((21 * (cosh (3 * x))) * (cosh x))) + (35 * ((cosh x) ^2))) / 64 by Th11 .= ((((1 / 2) * (((cosh (8 * x)) + (8 * (cosh (6 * x)))) + ((cosh (4 * x)) * 7))) + (21 * ((cosh (3 * x)) * (cosh x)))) + (35 * ((cosh x) ^2))) / 64 .= ((((1 / 2) * (((cosh (8 * x)) + (8 * (cosh (6 * x)))) + ((cosh (4 * x)) * 7))) + (21 * ((1 / 2) * ((cosh ((3 * x) + (1 * x))) + (cosh ((3 * x) - x)))))) + (35 * ((cosh x) ^2))) / 64 by Th11 .= (((1 / 2) * ((((cosh (8 * x)) + (8 * (cosh (6 * x)))) + (28 * (cosh (4 * x)))) + ((cosh (2 * x)) * 21))) + (((1 / 2) * ((cosh (2 * x)) + 1)) * 35)) / 64 by Lm7 .= (((((cosh (8 * x)) + (8 * (cosh (6 * x)))) + (28 * (cosh (4 * x)))) + (56 * (cosh (2 * x)))) + 35) / 128 ; hence ( (cosh x) |^ 3 = ((cosh (3 * x)) + (3 * (cosh x))) / 4 & (cosh x) |^ 4 = (((cosh (4 * x)) + (4 * (cosh (2 * x)))) + 3) / 8 & (cosh x) |^ 5 = (((cosh (5 * x)) + (5 * (cosh (3 * x)))) + (10 * (cosh x))) / 16 & (cosh x) |^ 6 = ((((cosh (6 * x)) + (6 * (cosh (4 * x)))) + (15 * (cosh (2 * x)))) + 10) / 32 & (cosh x) |^ 7 = ((((cosh (7 * x)) + (7 * (cosh (5 * x)))) + (21 * (cosh (3 * x)))) + (35 * (cosh x))) / 64 & (cosh x) |^ 8 = (((((cosh (8 * x)) + (8 * (cosh (6 * x)))) + (28 * (cosh (4 * x)))) + (56 * (cosh (2 * x)))) + 35) / 128 ) by A1, A2, A3, A4, A5; ::_thesis: verum end; theorem :: SIN_COS8:33 for y, z being real number holds ( (cosh (2 * y)) + (cos (2 * z)) = 2 + (2 * (((sinh y) ^2) - ((sin z) ^2))) & (cosh (2 * y)) - (cos (2 * z)) = 2 * (((sinh y) ^2) + ((sin z) ^2)) ) proof let y, z be real number ; ::_thesis: ( (cosh (2 * y)) + (cos (2 * z)) = 2 + (2 * (((sinh y) ^2) - ((sin z) ^2))) & (cosh (2 * y)) - (cos (2 * z)) = 2 * (((sinh y) ^2) + ((sin z) ^2)) ) A1: (cosh (2 * y)) - (cos (2 * z)) = (1 + (2 * ((sinh y) ^2))) - (cos (2 * z)) by Th27 .= (1 + (2 * ((sinh y) ^2))) - (1 - (2 * ((sin z) ^2))) by SIN_COS5:7 .= 2 * (((sinh y) ^2) + ((sin z) ^2)) ; (cosh (2 * y)) + (cos (2 * z)) = (1 + (2 * ((sinh y) ^2))) + (cos (2 * z)) by Th27 .= (1 + (2 * ((sinh y) ^2))) + (1 - (2 * ((sin z) ^2))) by SIN_COS5:7 .= 2 + (2 * (((sinh y) ^2) - ((sin z) ^2))) ; hence ( (cosh (2 * y)) + (cos (2 * z)) = 2 + (2 * (((sinh y) ^2) - ((sin z) ^2))) & (cosh (2 * y)) - (cos (2 * z)) = 2 * (((sinh y) ^2) + ((sin z) ^2)) ) by A1; ::_thesis: verum end;