sin_cos8.miz



    begin

    reserve x,y,z,w for Real;

    reserve n for Element of NAT ;

    

     Lm1: ( cosh x) >= 1 & ( cosh 0 ) = 1 & ( sinh 0 ) = 0

    proof

      ( cosh . x) >= 1 by SIN_COS2: 37;

      hence thesis by SIN_COS2: 15, SIN_COS2: 16, SIN_COS2:def 2, SIN_COS2:def 4;

    end;

    

     Lm2: ( 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

      

       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 thesis by A1, A2, XCMPLX_1: 55;

    end;

    

     Lm3: ((( cosh x) ^2 ) - (( sinh x) ^2 )) = 1 & ((( cosh x) * ( cosh x)) - (( sinh x) * ( sinh x))) = 1

    proof

      ((( 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 thesis;

    end;

    theorem :: SIN_COS8:1

    

     Th1: ( tanh x) = (( sinh x) / ( cosh x)) & ( tanh 0 ) = 0

    proof

      

       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 thesis by A1;

    end;

    

     Lm4: x <> 0 implies ( sinh x) <> 0 & ( tanh x) <> 0

    proof

      

       A1: ( exp_R x) > 0 by SIN_COS: 55;

      assume 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 thesis by Th1;

    end;

    

     Lm5: (y - z) <> 0 implies ( sinh ((y / 2) - (z / 2))) <> 0

    proof

      assume (y - z) <> 0 ;

      then ((y - z) / 2) <> 0 ;

      hence thesis by Lm4;

    end;

    

     Lm6: (y + z) <> 0 implies ( sinh ((y / 2) + (z / 2))) <> 0

    proof

      assume (y + z) <> 0 ;

      then ((y + z) / 2) <> 0 ;

      hence thesis by Lm4;

    end;

    

     Lm7: (( sinh x) ^2 ) = ((1 / 2) * (( cosh (2 * x)) - 1)) & (( cosh x) ^2 ) = ((1 / 2) * (( cosh (2 * x)) + 1))

    proof

      

       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 thesis by A1, SIN_COS2:def 4;

    end;

    

     Lm8: ( 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

      

       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 thesis by A2, A4, A1, A5, A3;

    end;

    theorem :: SIN_COS8:2

    

     Th2: ( sinh x) = (1 / ( cosech x)) & ( cosh x) = (1 / ( sech x)) & ( tanh x) = (1 / ( coth x))

    proof

      

       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 thesis by A1, A2;

    end;

    

     Lm9: (( exp_R x) + ( exp_R ( - x))) >= 2

    proof

      ( 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 thesis by A1, A2, SIN_COS2: 1;

    end;

    theorem :: SIN_COS8:3

    

     Th3: ( sech x) <= 1 & 0 < ( sech x) & ( sech 0 ) = 1

    proof

      

       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 thesis by A2, A1, SIN_COS5: 36, SIN_COS5:def 2;

    end;

    theorem :: SIN_COS8:4

    x >= 0 implies ( tanh x) >= 0

    proof

      

       A1: ( cosh x) >= 1 by Lm1;

      assume

       A2: x >= 0 ;

      per cases by A2;

        suppose x > 0 ;

        then ( sinh x) >= 0 by SIN_COS5: 46;

        then (( sinh x) / ( cosh x)) >= 0 by A1;

        hence thesis by Th1;

      end;

        suppose x = 0 ;

        hence thesis by Th1;

      end;

    end;

    theorem :: SIN_COS8:5

    ( cosh x) = (1 / ( sqrt (1 - (( tanh x) ^2 )))) & ( sinh x) = (( tanh x) / ( sqrt (1 - (( tanh x) ^2 ))))

    proof

      

       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 thesis by A3;

    end;

    theorem :: SIN_COS8:6

    ((( cosh x) + ( sinh x)) |^ n) = (( cosh (n * x)) + ( sinh (n * x))) & ((( cosh x) - ( sinh x)) |^ n) = (( cosh (n * x)) - ( sinh (n * x)))

    proof

      

       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 thesis by A1;

    end;

    theorem :: SIN_COS8:7

    

     Th7: ( 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

      

       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 thesis by A6, A5, A8, A3, A4;

    end;

    theorem :: SIN_COS8:8

    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))

    proof

      assume x <> 0 ;

      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 thesis by A4;

    end;

    theorem :: SIN_COS8:9

    ((( cosh x) + ( sinh x)) / (( cosh x) - ( sinh x))) = ((1 + ( tanh x)) / (1 - ( tanh x)))

    proof

      

       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 thesis by A1;

    end;

    

     Lm10: ( 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

      

       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 thesis by A1, A2, A5, A4, A3;

    end;

    theorem :: SIN_COS8:10

    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)))

    proof

      assume

       A1: y <> 0 ;

      

       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 thesis by A3;

    end;

    theorem :: SIN_COS8:11

    

     Th11: (( 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

      

       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 thesis by A1, A2, A3;

    end;

    theorem :: SIN_COS8:12

    ((( sinh y) ^2 ) - (( cosh z) ^2 )) = ((( sinh (y + z)) * ( sinh (y - z))) - 1)

    proof

      ((( 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 thesis;

    end;

    

     Lm11: (( 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

      

       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 thesis by A1, A2, A5, A4, A3;

    end;

    theorem :: SIN_COS8:13

    (((( 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

      

       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 thesis by A1;

    end;

    theorem :: SIN_COS8:14

    ((( sinh y) + ( sinh z)) / (( sinh y) - ( sinh z))) = (( tanh ((y + z) / 2)) * ( coth ((y - z) / 2)))

    proof

      ((( 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 thesis;

    end;

    theorem :: SIN_COS8:15

    ((( cosh y) + ( cosh z)) / (( cosh y) - ( cosh z))) = (( coth ((y + z) / 2)) * ( coth ((y - z) / 2)))

    proof

      ((( 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 thesis;

    end;

    theorem :: SIN_COS8:16

    (y - z) <> 0 implies ((( sinh y) + ( sinh z)) / (( cosh y) + ( cosh z))) = ((( cosh y) - ( cosh z)) / (( sinh y) - ( sinh z)))

    proof

      assume

       A1: (y - z) <> 0 ;

      

       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 thesis;

    end;

    theorem :: SIN_COS8:17

    (y + z) <> 0 implies ((( sinh y) - ( sinh z)) / (( cosh y) + ( cosh z))) = ((( cosh y) - ( cosh z)) / (( sinh y) + ( sinh z)))

    proof

      assume

       A1: (y + z) <> 0 ;

      

       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 thesis;

    end;

    theorem :: SIN_COS8:18

    ((( 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

      

       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 thesis by A3;

    end;

    theorem :: SIN_COS8:19

    ((( tanh y) + ( tanh z)) / (( tanh y) - ( tanh z))) = (( sinh (y + z)) / ( sinh (y - z)))

    proof

      

       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 thesis;

    end;

    

     Lm12: (1 + (( cosh x) + ( cosh x))) <> 0

    proof

      ( cosh . x) > 0 by SIN_COS2: 15;

      then ( cosh x) > 0 by SIN_COS2:def 4;

      hence thesis;

    end;

    

     Lm13: (( cosh x) + 1) > 0 & (( cosh x) - 1) >= 0 & ((( cosh x) + 2) + ( cosh x)) <> 0

    proof

      ( 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 thesis by A1;

    end;

    theorem :: SIN_COS8:20

    (((( sinh (y - z)) + ( sinh y)) + ( sinh (y + z))) / ((( cosh (y - z)) + ( cosh y)) + ( cosh (y + z)))) = ( tanh y)

    proof

      (((( 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 thesis;

    end;

    

     Lm14: ((( 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

      

       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 thesis by A4, A2;

    end;

    theorem :: SIN_COS8:21

    

     Th21: ( 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

      

       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 thesis by A4, A3;

    end;

    theorem :: SIN_COS8:22

    (((( 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

      (((( 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 thesis;

    end;

    theorem :: SIN_COS8:23

    (((((( 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

      (((((( 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 thesis;

    end;

    theorem :: SIN_COS8:24

    

     Th24: x >= 0 implies ( sinh (x / 2)) = ( sqrt ((( cosh x) - 1) / 2))

    proof

      assume x >= 0 ;

      

      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 thesis;

    end;

    theorem :: SIN_COS8:25

    

     Th25: x < 0 implies ( sinh (x / 2)) = ( - ( sqrt ((( cosh x) - 1) / 2)))

    proof

      assume x < 0 ;

      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 thesis;

    end;

    theorem :: SIN_COS8:26

    

     Th26: ( 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

      

       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 thesis by A1, A2;

    end;

    theorem :: SIN_COS8:27

    

     Th27: ( 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

      

       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))

      .= (((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))))

      .= (((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))

      .= (( 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 thesis by A2, A9, A4, A7, A8, A3, A5;

    end;

    theorem :: SIN_COS8:28

    (((( 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

      (((( 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 thesis;

    end;

    theorem :: SIN_COS8:29

    x >= 0 implies ( tanh (x / 2)) = ( sqrt ((( cosh x) - 1) / (( cosh x) + 1)))

    proof

      assume

       A1: x >= 0 ;

      

       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 thesis;

    end;

    theorem :: SIN_COS8:30

    x < 0 implies ( tanh (x / 2)) = ( - ( sqrt ((( cosh x) - 1) / (( cosh x) + 1))))

    proof

      assume

       A1: x < 0 ;

      

       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 thesis;

    end;

    theorem :: SIN_COS8:31

    (( 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

      

       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 thesis by A1, A2, A3, A4, A5;

    end;

    theorem :: SIN_COS8:32

    (( 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

      

       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)

      .= ((((( 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 thesis by A1, A2, A3, A4, A5;

    end;

    theorem :: SIN_COS8:33

    (( 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

      

       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 thesis by A1;

    end;