sin_cos5.miz



    begin

    reserve x,x1,x2,x3 for Real;

    theorem :: SIN_COS5:1

    

     Th1: ( cos x) <> 0 implies ( cosec x) = (( sec x) / ( tan x))

    proof

      assume

       A1: ( cos x) <> 0 ;

      

      then (( sec x) / ( tan x)) = (((1 / ( cos x)) * ( cos x)) / ((( sin x) / ( cos x)) * ( cos x))) by XCMPLX_1: 91

      .= (1 / ((( sin x) / ( cos x)) * ( cos x))) by A1, XCMPLX_1: 87

      .= (1 / ( sin x)) by A1, XCMPLX_1: 87;

      hence thesis;

    end;

    theorem :: SIN_COS5:2

    

     Th2: ( sin x) <> 0 implies ( cos x) = (( sin x) * ( cot x))

    proof

      assume ( sin x) <> 0 ;

      

      then ( cos x) = ((( sin x) / ( sin x)) * ( cos x)) by XCMPLX_1: 88

      .= (( sin x) * ( cot x)) by XCMPLX_1: 75;

      hence thesis;

    end;

    theorem :: SIN_COS5:3

    ( sin x1) <> 0 & ( sin x2) <> 0 & ( sin x3) <> 0 implies ( sin ((x1 + x2) + x3)) = (((( sin x1) * ( sin x2)) * ( sin x3)) * ((((( cot x2) * ( cot x3)) + (( cot x1) * ( cot x3))) + (( cot x1) * ( cot x2))) - 1))

    proof

      assume that

       A1: ( sin x1) <> 0 and

       A2: ( sin x2) <> 0 and

       A3: ( sin x3) <> 0 ;

      ( sin ((x1 + x2) + x3)) = ( sin (x1 + (x2 + x3)))

      .= ((( sin x1) * ( cos (x2 + x3))) + (( cos x1) * ( sin (x2 + x3)))) by SIN_COS: 75

      .= ((( sin x1) * ((( cos x2) * ( cos x3)) - (( sin x2) * ( sin x3)))) + (( cos x1) * ( sin (x2 + x3)))) by SIN_COS: 75

      .= (((( sin x1) * (( cos x2) * ( cos x3))) - (( sin x1) * (( sin x2) * ( sin x3)))) + (( cos x1) * ((( sin x2) * ( cos x3)) + (( cos x2) * ( sin x3))))) by SIN_COS: 75

      .= ((((( sin x1) * ( cos x2)) * ( cos x3)) - ((( sin x1) * ( sin x2)) * ( sin x3))) + (((( cos x1) * ( sin x2)) * ( cos x3)) + ((( cos x1) * ( cos x2)) * ( sin x3))))

      .= ((((( sin x1) * (( sin x2) * ( cot x2))) * ( cos x3)) - ((( sin x1) * ( sin x2)) * ( sin x3))) + (((( cos x1) * ( sin x2)) * ( cos x3)) + ((( cos x1) * ( cos x2)) * ( sin x3)))) by A2, Th2

      .= ((((( sin x1) * (( sin x2) * ( cot x2))) * (( sin x3) * ( cot x3))) - ((( sin x1) * ( sin x2)) * ( sin x3))) + (((( cos x1) * ( sin x2)) * ( cos x3)) + ((( cos x1) * ( cos x2)) * ( sin x3)))) by A3, Th2

      .= ((((( sin x1) * ( sin x2)) * ( sin x3)) * ((( cot x2) * ( cot x3)) - 1)) + ((((( sin x1) * ( cot x1)) * ( sin x2)) * ( cos x3)) + ((( cos x1) * ( cos x2)) * ( sin x3)))) by A1, Th2

      .= ((((( sin x1) * ( sin x2)) * ( sin x3)) * ((( cot x2) * ( cot x3)) - 1)) + ((((( sin x1) * ( cot x1)) * ( sin x2)) * (( sin x3) * ( cot x3))) + ((( cos x1) * ( cos x2)) * ( sin x3)))) by A3, Th2

      .= (((((( sin x1) * ( sin x2)) * ( sin x3)) * ((( cot x2) * ( cot x3)) - 1)) + ((((( sin x1) * ( sin x2)) * ( sin x3)) * ( cot x1)) * ( cot x3))) + ((( cos x1) * ( cos x2)) * ( sin x3)))

      .= ((((( sin x1) * ( sin x2)) * ( sin x3)) * (((( cot x2) * ( cot x3)) - 1) + (( cot x1) * ( cot x3)))) + (((( sin x1) * ( cot x1)) * ( cos x2)) * ( sin x3))) by A1, Th2

      .= ((((( sin x1) * ( sin x2)) * ( sin x3)) * (((( cot x2) * ( cot x3)) - 1) + (( cot x1) * ( cot x3)))) + (((( sin x1) * ( cot x1)) * (( sin x2) * ( cot x2))) * ( sin x3))) by A2, Th2

      .= (((( sin x1) * ( sin x2)) * ( sin x3)) * ((((( cot x2) * ( cot x3)) + (( cot x1) * ( cot x3))) + (( cot x1) * ( cot x2))) - 1));

      hence thesis;

    end;

    theorem :: SIN_COS5:4

    ( sin x1) <> 0 & ( sin x2) <> 0 & ( sin x3) <> 0 implies ( cos ((x1 + x2) + x3)) = ( - (((( sin x1) * ( sin x2)) * ( sin x3)) * (((( cot x1) + ( cot x2)) + ( cot x3)) - ((( cot x1) * ( cot x2)) * ( cot x3)))))

    proof

      assume that

       A1: ( sin x1) <> 0 and

       A2: ( sin x2) <> 0 and

       A3: ( sin x3) <> 0 ;

      ( cos ((x1 + x2) + x3)) = ( cos (x1 + (x2 + x3)))

      .= ((( cos x1) * ( cos (x2 + x3))) - (( sin x1) * ( sin (x2 + x3)))) by SIN_COS: 75

      .= ((( cos x1) * ((( cos x2) * ( cos x3)) - (( sin x2) * ( sin x3)))) - (( sin x1) * ( sin (x2 + x3)))) by SIN_COS: 75

      .= (((( cos x1) * (( cos x2) * ( cos x3))) - (( cos x1) * (( sin x2) * ( sin x3)))) - (( sin x1) * ((( sin x2) * ( cos x3)) + (( cos x2) * ( sin x3))))) by SIN_COS: 75

      .= ((((( cos x1) * ( cos x2)) * ( cos x3)) - ((( cos x1) * ( sin x2)) * ( sin x3))) - (((( sin x1) * ( sin x2)) * ( cos x3)) + ((( sin x1) * ( sin x3)) * ( cos x2))))

      .= ((((( cos x1) * ( cos x2)) * ( cos x3)) - ((( cos x1) * ( sin x2)) * ( sin x3))) - (((( sin x1) * ( sin x2)) * (( sin x3) * ( cot x3))) + ((( sin x1) * ( sin x3)) * ( cos x2)))) by A3, Th2

      .= ((((( cos x1) * ( cos x2)) * ( cos x3)) - ((( cos x1) * ( sin x2)) * ( sin x3))) - (((( sin x1) * ( sin x2)) * (( sin x3) * ( cot x3))) + ((( sin x1) * ( sin x3)) * (( sin x2) * ( cot x2))))) by A2, Th2

      .= (((((( sin x1) * ( cot x1)) * ( cos x2)) * ( cos x3)) - ((( cos x1) * ( sin x2)) * ( sin x3))) - (((( sin x1) * ( sin x2)) * ( sin x3)) * (( cot x3) + ( cot x2)))) by A1, Th2

      .= (((((( sin x1) * ( cot x1)) * (( sin x2) * ( cot x2))) * ( cos x3)) - ((( cos x1) * ( sin x2)) * ( sin x3))) - (((( sin x1) * ( sin x2)) * ( sin x3)) * (( cot x3) + ( cot x2)))) by A2, Th2

      .= (((((( sin x1) * ( cot x1)) * (( sin x2) * ( cot x2))) * (( sin x3) * ( cot x3))) - ((( cos x1) * ( sin x2)) * ( sin x3))) - (((( sin x1) * ( sin x2)) * ( sin x3)) * (( cot x3) + ( cot x2)))) by A3, Th2

      .= (((((( sin x1) * ( sin x2)) * ( sin x3)) * ((( cot x1) * ( cot x2)) * ( cot x3))) - (((( sin x1) * ( cot x1)) * ( sin x2)) * ( sin x3))) - (((( sin x1) * ( sin x2)) * ( sin x3)) * (( cot x3) + ( cot x2)))) by A1, Th2

      .= ( - (((( sin x1) * ( sin x2)) * ( sin x3)) * (((( cot x1) + ( cot x2)) + ( cot x3)) - ((( cot x1) * ( cot x2)) * ( cot x3)))));

      hence thesis;

    end;

    theorem :: SIN_COS5:5

    

     Th5: ( sin (2 * x)) = ((2 * ( sin x)) * ( cos x))

    proof

      ( sin (2 * x)) = ( sin (x + x))

      .= ((( sin x) * ( cos x)) + (( cos x) * ( sin x))) by SIN_COS: 75

      .= ((2 * ( sin x)) * ( cos x));

      hence thesis;

    end;

    theorem :: SIN_COS5:6

    

     Th6: ( cos x) <> 0 implies ( sin (2 * x)) = ((2 * ( tan x)) / (1 + (( tan x) ^2 )))

    proof

      assume

       A1: ( cos x) <> 0 ;

      then

       A2: (( cos x) ^2 ) <> 0 by SQUARE_1: 12;

      ( sin (2 * x)) = (((2 * ( sin x)) * ( cos x)) * 1) by Th5

      .= (((2 * ( sin x)) * ( cos x)) * (( cos x) / ( cos x))) by A1, XCMPLX_1: 60

      .= ((((2 * ( sin x)) * ( cos x)) * ( cos x)) / ( cos x)) by XCMPLX_1: 74

      .= (((2 * (( cos x) ^2 )) * ( sin x)) / ( cos x))

      .= (((2 * (( cos x) ^2 )) * ( tan x)) / 1) by XCMPLX_1: 74

      .= (((2 * ( tan x)) * (( cos x) ^2 )) / ((( sin x) ^2 ) + (( cos x) ^2 ))) by SIN_COS: 29

      .= ((2 * ( tan x)) / (((( sin x) ^2 ) + (( cos x) ^2 )) / (( cos x) ^2 ))) by XCMPLX_1: 77

      .= ((2 * ( tan x)) / (((( sin x) ^2 ) / (( cos x) ^2 )) + ((( cos x) ^2 ) / (( cos x) ^2 )))) by XCMPLX_1: 62

      .= ((2 * ( tan x)) / (((( sin x) ^2 ) / (( cos x) ^2 )) + 1)) by A2, XCMPLX_1: 60

      .= ((2 * ( tan x)) / ((( tan x) ^2 ) + 1)) by XCMPLX_1: 76;

      hence thesis;

    end;

    theorem :: SIN_COS5:7

    

     Th7: ( cos (2 * x)) = ((( cos x) ^2 ) - (( sin x) ^2 )) & ( cos (2 * x)) = ((2 * (( cos x) ^2 )) - 1) & ( cos (2 * x)) = (1 - (2 * (( sin x) ^2 )))

    proof

      

       A1: ( cos (2 * x)) = ( cos (x + x))

      .= ((( cos x) ^2 ) - (( sin x) ^2 )) by SIN_COS: 75;

      

      then ( cos (2 * x)) = ((((( cos x) ^2 ) - (( sin x) ^2 )) - 1) + 1)

      .= ((((( cos x) ^2 ) - (( sin x) ^2 )) - ((( cos x) ^2 ) + (( sin x) ^2 ))) + 1) by SIN_COS: 29

      .= ( - (( - 1) + (2 * (( sin x) ^2 ))));

      hence thesis by A1;

    end;

    theorem :: SIN_COS5:8

    

     Th8: ( cos x) <> 0 implies ( cos (2 * x)) = ((1 - (( tan x) ^2 )) / (1 + (( tan x) ^2 )))

    proof

      assume ( cos x) <> 0 ;

      then

       A1: (( cos x) ^2 ) <> 0 by SQUARE_1: 12;

      ( cos (2 * x)) = (((( cos x) ^2 ) - (( sin x) ^2 )) * 1) by Th7

      .= (((( cos x) ^2 ) - (( sin x) ^2 )) * ((( cos x) ^2 ) / (( cos x) ^2 ))) by A1, XCMPLX_1: 60

      .= ((((( cos x) ^2 ) - (( sin x) ^2 )) / (( cos x) ^2 )) * (( cos x) ^2 )) by XCMPLX_1: 75

      .= ((((( cos x) ^2 ) / (( cos x) ^2 )) - ((( sin x) ^2 ) / (( cos x) ^2 ))) * (( cos x) ^2 )) by XCMPLX_1: 120

      .= ((1 - ((( sin x) ^2 ) / (( cos x) ^2 ))) * (( cos x) ^2 )) by A1, XCMPLX_1: 60

      .= (((1 - (( tan x) ^2 )) * (( cos x) ^2 )) / 1) by XCMPLX_1: 76

      .= (((1 - (( tan x) ^2 )) * (( cos x) ^2 )) / ((( cos x) ^2 ) + (( sin x) ^2 ))) by SIN_COS: 29

      .= ((1 - (( tan x) ^2 )) / (((( cos x) ^2 ) + (( sin x) ^2 )) / (( cos x) ^2 ))) by XCMPLX_1: 77

      .= ((1 - (( tan x) ^2 )) / (((( cos x) ^2 ) / (( cos x) ^2 )) + ((( sin x) ^2 ) / (( cos x) ^2 )))) by XCMPLX_1: 62

      .= ((1 - (( tan x) ^2 )) / (1 + ((( sin x) ^2 ) / (( cos x) ^2 )))) by A1, XCMPLX_1: 60

      .= ((1 - (( tan x) ^2 )) / (1 + (( tan x) ^2 ))) by XCMPLX_1: 76;

      hence thesis;

    end;

    theorem :: SIN_COS5:9

    ( cos x) <> 0 implies ( tan (2 * x)) = ((2 * ( tan x)) / (1 - (( tan x) ^2 )))

    proof

      assume

       A1: ( cos x) <> 0 ;

      ( tan (2 * x)) = ( tan (x + x))

      .= ((( tan x) + ( tan x)) / (1 - (( tan x) * ( tan x)))) by A1, SIN_COS4: 7

      .= ((2 * ( tan x)) / (1 - (( tan x) * ( tan x))));

      hence thesis;

    end;

    theorem :: SIN_COS5:10

    ( sin x) <> 0 implies ( cot (2 * x)) = (((( cot x) ^2 ) - 1) / (2 * ( cot x)))

    proof

      assume

       A1: ( sin x) <> 0 ;

      ( cot (2 * x)) = ( cot (x + x))

      .= (((( cot x) * ( cot x)) - 1) / (( cot x) + ( cot x))) by A1, SIN_COS4: 9

      .= (((( cot x) * ( cot x)) - 1) / (2 * ( cot x)));

      hence thesis;

    end;

    theorem :: SIN_COS5:11

    

     Th11: ( cos x) <> 0 implies (( sec x) ^2 ) = (1 + (( tan x) ^2 ))

    proof

      assume ( cos x) <> 0 ;

      then

       A1: (( cos x) ^2 ) <> 0 by SQUARE_1: 12;

      (( sec x) ^2 ) = ((1 ^2 ) / (( cos x) ^2 )) by XCMPLX_1: 76

      .= (((( sin x) ^2 ) + (( cos x) ^2 )) / (( cos x) ^2 )) by SIN_COS: 29

      .= (((( sin x) ^2 ) / (( cos x) ^2 )) + ((( cos x) ^2 ) / (( cos x) ^2 ))) by XCMPLX_1: 62

      .= (((( sin x) ^2 ) / (( cos x) ^2 )) + 1) by A1, XCMPLX_1: 60

      .= (((( sin x) / ( cos x)) ^2 ) + 1) by XCMPLX_1: 76;

      hence thesis;

    end;

    theorem :: SIN_COS5:12

    ( cot x) = (1 / ( tan x)) by XCMPLX_1: 57;

    theorem :: SIN_COS5:13

    

     Th13: ( cos x) <> 0 & ( sin x) <> 0 implies ( sec (2 * x)) = ((( sec x) ^2 ) / (1 - (( tan x) ^2 ))) & ( sec (2 * x)) = ((( cot x) + ( tan x)) / (( cot x) - ( tan x)))

    proof

      assume that

       A1: ( cos x) <> 0 and

       A2: ( sin x) <> 0 ;

      

       A3: ( sec (2 * x)) = (1 / ((1 - (( tan x) ^2 )) / (1 + (( tan x) ^2 )))) by A1, Th8

      .= ((1 + (( tan x) ^2 )) / (1 - (( tan x) ^2 ))) by XCMPLX_1: 57

      .= ((( sec x) ^2 ) / (1 - (( tan x) ^2 ))) by A1, Th11;

      

      then ( sec (2 * x)) = ((1 + (( tan x) ^2 )) / (1 - (( tan x) ^2 ))) by A1, Th11

      .= (((1 + (( tan x) ^2 )) / ( tan x)) / ((1 - (( tan x) ^2 )) / ( tan x))) by A1, A2, XCMPLX_1: 50, XCMPLX_1: 55

      .= (((1 / ( tan x)) + ((( tan x) ^2 ) / ( tan x))) / ((1 - (( tan x) ^2 )) / ( tan x))) by XCMPLX_1: 62

      .= ((( cot x) + ((( tan x) ^2 ) / ( tan x))) / ((1 - (( tan x) ^2 )) / ( tan x))) by XCMPLX_1: 57

      .= ((( cot x) + ((( tan x) ^2 ) / ( tan x))) / ((1 / ( tan x)) - ((( tan x) ^2 ) / ( tan x)))) by XCMPLX_1: 120

      .= ((( cot x) + ((( tan x) * ( tan x)) / ( tan x))) / (( cot x) - ((( tan x) ^2 ) / ( tan x)))) by XCMPLX_1: 57

      .= ((( cot x) + ( tan x)) / (( cot x) - ((( tan x) * ( tan x)) / ( tan x)))) by A1, A2, XCMPLX_1: 50, XCMPLX_1: 89;

      hence thesis by A1, A2, A3, XCMPLX_1: 50, XCMPLX_1: 89;

    end;

    theorem :: SIN_COS5:14

    ( sin x) <> 0 implies (( cosec x) ^2 ) = (1 + (( cot x) ^2 ))

    proof

      assume ( sin x) <> 0 ;

      then

       A1: (( sin x) ^2 ) <> 0 by SQUARE_1: 12;

      (( cosec x) ^2 ) = ((1 ^2 ) / (( sin x) ^2 )) by XCMPLX_1: 76

      .= (((( sin x) ^2 ) + (( cos x) ^2 )) / (( sin x) ^2 )) by SIN_COS: 29

      .= (((( sin x) ^2 ) / (( sin x) ^2 )) + ((( cos x) ^2 ) / (( sin x) ^2 ))) by XCMPLX_1: 62

      .= (1 + ((( cos x) ^2 ) / (( sin x) ^2 ))) by A1, XCMPLX_1: 60

      .= (1 + ((( cos x) / ( sin x)) ^2 )) by XCMPLX_1: 76;

      hence thesis;

    end;

    theorem :: SIN_COS5:15

    ( cos x) <> 0 & ( sin x) <> 0 implies ( cosec (2 * x)) = ((( sec x) * ( cosec x)) / 2) & ( cosec (2 * x)) = ((( tan x) + ( cot x)) / 2)

    proof

      assume that

       A1: ( cos x) <> 0 and

       A2: ( sin x) <> 0 ;

      

       A3: ( cosec (2 * x)) = (1 / ((2 * ( tan x)) / (1 + (( tan x) ^2 )))) by A1, Th6

      .= ((1 + (( tan x) ^2 )) / (2 * ( tan x))) by XCMPLX_1: 57

      .= (((1 + (( tan x) ^2 )) / ( tan x)) / 2) by XCMPLX_1: 78

      .= (((1 / (( sin x) / ( cos x))) + ((( tan x) ^2 ) / ( tan x))) / 2) by XCMPLX_1: 62

      .= ((( cot x) + ((( tan x) * ( tan x)) / ( tan x))) / 2) by XCMPLX_1: 57

      .= ((( cot x) + ( tan x)) / 2) by A1, A2, XCMPLX_1: 50, XCMPLX_1: 89;

      ( cosec (2 * x)) = (1 / ((2 * ( tan x)) / (1 + (( tan x) ^2 )))) by A1, Th6

      .= ((1 + (( tan x) ^2 )) / (2 * ( tan x))) by XCMPLX_1: 57

      .= ((( sec x) ^2 ) / (2 * ( tan x))) by A1, Th11

      .= (((( sec x) * ( sec x)) / ( tan x)) / 2) by XCMPLX_1: 78

      .= ((( sec x) * (( sec x) / (( sin x) / ( cos x)))) / 2) by XCMPLX_1: 74

      .= ((( sec x) * ((( sec x) * ( cos x)) / ( sin x))) / 2) by XCMPLX_1: 77

      .= ((( sec x) * ( cosec x)) / 2) by A1, XCMPLX_1: 106;

      hence thesis by A3;

    end;

    theorem :: SIN_COS5:16

    

     Th16: ( sin (3 * x)) = (( - (4 * (( sin x) |^ 3))) + (3 * ( sin x)))

    proof

      ( sin (3 * x)) = ( sin ((x + x) + x))

      .= ((( sin (2 * x)) * ( cos x)) + (( cos (x + x)) * ( sin x))) by SIN_COS: 75

      .= ((((2 * ( sin x)) * ( cos x)) * ( cos x)) + (( cos (2 * x)) * ( sin x))) by Th5

      .= (((2 * ( sin x)) * (( cos x) * ( cos x))) + ((1 - (2 * (( sin x) ^2 ))) * ( sin x))) by Th7

      .= (((2 * ( sin x)) * (1 - (( sin x) ^2 ))) + ((1 - (2 * (( sin x) ^2 ))) * ( sin x))) by SIN_COS4: 5

      .= ((((2 * ( sin x)) * 1) - ((2 * ( sin x)) * (( sin x) * ( sin x)))) + ((1 * ( sin x)) - ((2 * (( sin x) ^2 )) * ( sin x))))

      .= ((((2 * ( sin x)) * 1) - ((2 * ((( sin x) |^ 1) * ( sin x))) * ( sin x))) + ((1 * ( sin x)) - ((2 * (( sin x) ^2 )) * ( sin x))))

      .= ((((2 * ( sin x)) * 1) - ((2 * (( sin x) |^ (1 + 1))) * ( sin x))) + ((1 * ( sin x)) - ((2 * (( sin x) ^2 )) * ( sin x)))) by NEWTON: 6

      .= ((((2 * ( sin x)) * 1) - (2 * ((( sin x) |^ 2) * ( sin x)))) + ((1 * ( sin x)) - ((2 * (( sin x) ^2 )) * ( sin x))))

      .= ((((2 * ( sin x)) * 1) - (2 * (( sin x) |^ (2 + 1)))) + ((1 * ( sin x)) - ((2 * (( sin x) ^2 )) * ( sin x)))) by NEWTON: 6

      .= (((2 * ( sin x)) - (2 * (( sin x) |^ 3))) + (( sin x) - ((2 * ((( sin x) |^ 1) * ( sin x))) * ( sin x))))

      .= (((2 * ( sin x)) - (2 * (( sin x) |^ 3))) + (( sin x) - ((2 * (( sin x) |^ (1 + 1))) * ( sin x)))) by NEWTON: 6

      .= (((2 * ( sin x)) - (2 * (( sin x) |^ 3))) + (( sin x) - (2 * ((( sin x) |^ (1 + 1)) * ( sin x)))))

      .= (((2 * ( sin x)) - (2 * (( sin x) |^ 3))) + (( sin x) - (2 * (( sin x) |^ (2 + 1))))) by NEWTON: 6

      .= ( - (( - (3 * ( sin x))) + (4 * (( sin x) |^ 3))));

      hence thesis;

    end;

    theorem :: SIN_COS5:17

    

     Th17: ( cos (3 * x)) = ((4 * (( cos x) |^ 3)) - (3 * ( cos x)))

    proof

      ( cos (3 * x)) = ( cos ((x + x) + x))

      .= ((( cos (2 * x)) * ( cos x)) - (( sin (x + x)) * ( sin x))) by SIN_COS: 75

      .= ((((2 * (( cos x) ^2 )) - 1) * ( cos x)) - (( sin (2 * x)) * ( sin x))) by Th7

      .= (((2 * ((( cos x) * ( cos x)) * ( cos x))) - (1 * ( cos x))) - (( sin (2 * x)) * ( sin x)))

      .= (((2 * (((( cos x) |^ 1) * ( cos x)) * ( cos x))) - (1 * ( cos x))) - (( sin (2 * x)) * ( sin x)))

      .= (((2 * ((( cos x) |^ (1 + 1)) * ( cos x))) - (1 * ( cos x))) - (( sin (2 * x)) * ( sin x))) by NEWTON: 6

      .= (((2 * (( cos x) |^ (2 + 1))) - ( cos x)) - (( sin (2 * x)) * ( sin x))) by NEWTON: 6

      .= (((2 * (( cos x) |^ 3)) - ( cos x)) - (((2 * ( sin x)) * ( cos x)) * ( sin x))) by Th5

      .= (((2 * (( cos x) |^ 3)) - ( cos x)) - ((2 * ( cos x)) * (( sin x) * ( sin x))))

      .= (((2 * (( cos x) |^ 3)) - ( cos x)) - ((2 * ( cos x)) * (1 - (( cos x) * ( cos x))))) by SIN_COS4: 4

      .= (((2 * (( cos x) |^ 3)) - ( cos x)) - ((2 * ( cos x)) - (2 * ((( cos x) * ( cos x)) * ( cos x)))))

      .= (((2 * (( cos x) |^ 3)) - ( cos x)) - ((2 * ( cos x)) - (2 * (((( cos x) |^ 1) * ( cos x)) * ( cos x)))))

      .= (((2 * (( cos x) |^ 3)) - ( cos x)) - ((2 * ( cos x)) - (2 * ((( cos x) |^ (1 + 1)) * ( cos x))))) by NEWTON: 6

      .= (((2 * (( cos x) |^ 3)) - ( cos x)) - ((2 * ( cos x)) - (2 * (( cos x) |^ (2 + 1))))) by NEWTON: 6

      .= (((2 * (( cos x) |^ 3)) + (2 * (( cos x) |^ 3))) - (3 * ( cos x)));

      hence thesis;

    end;

    theorem :: SIN_COS5:18

    ( cos x) <> 0 implies ( tan (3 * x)) = (((3 * ( tan x)) - (( tan x) |^ 3)) / (1 - (3 * (( tan x) ^2 ))))

    proof

      assume

       A1: ( cos x) <> 0 ;

      ( tan (3 * x)) = ( tan ((x + x) + x))

      .= ((((( tan x) + ( tan x)) + ( tan x)) - ((( tan x) * ( tan x)) * ( tan x))) / (((1 - (( tan x) * ( tan x))) - (( tan x) * ( tan x))) - (( tan x) * ( tan x)))) by A1, SIN_COS4: 13

      .= (((3 * ( tan x)) - (((( tan x) |^ 1) * ( tan x)) * ( tan x))) / (1 - ((3 * ( tan x)) * ( tan x))))

      .= (((3 * ( tan x)) - ((( tan x) |^ (1 + 1)) * ( tan x))) / (1 - ((3 * ( tan x)) * ( tan x)))) by NEWTON: 6

      .= (((3 * ( tan x)) - (( tan x) |^ (2 + 1))) / (1 - (3 * (( tan x) * ( tan x))))) by NEWTON: 6;

      hence thesis;

    end;

    theorem :: SIN_COS5:19

    ( sin x) <> 0 implies ( cot (3 * x)) = (((( cot x) |^ 3) - (3 * ( cot x))) / ((3 * (( cot x) ^2 )) - 1))

    proof

      assume

       A1: ( sin x) <> 0 ;

      ( cot (3 * x)) = ( cot ((x + x) + x))

      .= ((((((( cot x) * ( cot x)) * ( cot x)) - ( cot x)) - ( cot x)) - ( cot x)) / ((((( cot x) * ( cot x)) + (( cot x) * ( cot x))) + (( cot x) * ( cot x))) - 1)) by A1, SIN_COS4: 14

      .= ((((( cot x) * ( cot x)) * ( cot x)) - (3 * ( cot x))) / ((3 * (( cot x) ^2 )) - 1))

      .= (((((( cot x) |^ 1) * ( cot x)) * ( cot x)) - (3 * ( cot x))) / ((3 * (( cot x) ^2 )) - 1))

      .= ((((( cot x) |^ (1 + 1)) * ( cot x)) - (3 * ( cot x))) / ((3 * (( cot x) ^2 )) - 1)) by NEWTON: 6

      .= (((( cot x) |^ (2 + 1)) - (3 * ( cot x))) / ((3 * (( cot x) ^2 )) - 1)) by NEWTON: 6;

      hence thesis;

    end;

    theorem :: SIN_COS5:20

    (( sin x) ^2 ) = ((1 - ( cos (2 * x))) / 2)

    proof

      ((1 - ( cos (2 * x))) / 2) = ((1 - (1 - (2 * (( sin x) ^2 )))) / 2) by Th7

      .= (((( sin x) ^2 ) * 2) / 2);

      hence thesis;

    end;

    theorem :: SIN_COS5:21

    (( cos x) ^2 ) = ((1 + ( cos (2 * x))) / 2)

    proof

      ((1 + ( cos (2 * x))) / 2) = ((1 + ((2 * (( cos x) ^2 )) - 1)) / 2) by Th7

      .= (((( cos x) ^2 ) * 2) / 2);

      hence thesis;

    end;

    theorem :: SIN_COS5:22

    (( sin x) |^ 3) = (((3 * ( sin x)) - ( sin (3 * x))) / 4)

    proof

      (((3 * ( sin x)) - ( sin (3 * x))) / 4) = (((3 * ( sin x)) - (( - (4 * (( sin x) |^ 3))) + (3 * ( sin x)))) / 4) by Th16

      .= ((4 * (( sin x) |^ 3)) / 4);

      hence thesis;

    end;

    theorem :: SIN_COS5:23

    (( cos x) |^ 3) = (((3 * ( cos x)) + ( cos (3 * x))) / 4)

    proof

      (((3 * ( cos x)) + ( cos (3 * x))) / 4) = (((3 * ( cos x)) + ((4 * (( cos x) |^ 3)) - (3 * ( cos x)))) / 4) by Th17

      .= ((4 * (( cos x) |^ 3)) / 4);

      hence thesis;

    end;

    theorem :: SIN_COS5:24

    (( sin x) |^ 4) = (((3 - (4 * ( cos (2 * x)))) + ( cos (4 * x))) / 8)

    proof

      (((3 - (4 * ( cos (2 * x)))) + ( cos ((2 * 2) * x))) / 8) = (((3 - (4 * ( cos (2 * x)))) + ( cos (2 * (2 * x)))) / 8)

      .= (((3 - (4 * ( cos (2 * x)))) + (1 - (2 * (( sin (2 * x)) ^2 )))) / 8) by Th7

      .= (((3 - (4 * ( cos (2 * x)))) + (1 - (2 * (((2 * ( sin x)) * ( cos x)) ^2 )))) / 8) by Th5

      .= (((3 - (4 * (1 - (2 * (( sin x) ^2 ))))) + (1 - ((8 * (( sin x) ^2 )) * (( cos x) ^2 )))) / 8) by Th7

      .= ((( sin x) ^2 ) * (1 - (( cos x) * ( cos x))))

      .= ((( sin x) * ( sin x)) * (( sin x) * ( sin x))) by SIN_COS4: 4

      .= (((( sin x) |^ 1) * ( sin x)) * (( sin x) * ( sin x)))

      .= ((( sin x) |^ (1 + 1)) * (( sin x) * ( sin x))) by NEWTON: 6

      .= (((( sin x) |^ (1 + 1)) * ( sin x)) * ( sin x))

      .= ((( sin x) |^ (2 + 1)) * ( sin x)) by NEWTON: 6

      .= (( sin x) |^ (3 + 1)) by NEWTON: 6;

      hence thesis;

    end;

    theorem :: SIN_COS5:25

    (( cos x) |^ 4) = (((3 + (4 * ( cos (2 * x)))) + ( cos (4 * x))) / 8)

    proof

      (((3 + (4 * ( cos (2 * x)))) + ( cos (4 * x))) / 8) = (((3 + (4 * ( cos (2 * x)))) + ( cos (2 * (2 * x)))) / 8)

      .= (((3 + (4 * ( cos (2 * x)))) + (1 - (2 * (( sin (2 * x)) ^2 )))) / 8) by Th7

      .= (((3 + (4 * ( cos (2 * x)))) + (1 - (2 * (((2 * ( sin x)) * ( cos x)) ^2 )))) / 8) by Th5

      .= (((3 + (4 * (1 - (2 * (( sin x) ^2 ))))) + (1 - ((8 * (( sin x) ^2 )) * (( cos x) ^2 )))) / 8) by Th7

      .= (1 - ((( sin x) * ( sin x)) * (1 + (( cos x) ^2 ))))

      .= (1 - (((1 ^2 ) - (( cos x) ^2 )) * ((1 ^2 ) + (( cos x) ^2 )))) by SIN_COS4: 4

      .= (((( cos x) * ( cos x)) * ( cos x)) * ( cos x))

      .= ((((( cos x) |^ 1) * ( cos x)) * ( cos x)) * ( cos x))

      .= (((( cos x) |^ (1 + 1)) * ( cos x)) * ( cos x)) by NEWTON: 6

      .= ((( cos x) |^ (2 + 1)) * ( cos x)) by NEWTON: 6

      .= (( cos x) |^ (3 + 1)) by NEWTON: 6;

      hence thesis;

    end;

    theorem :: SIN_COS5:26

    ( sin (x / 2)) = ( sqrt ((1 - ( cos x)) / 2)) or ( sin (x / 2)) = ( - ( sqrt ((1 - ( cos x)) / 2)))

    proof

      

       A1: ( sqrt ((1 - ( cos x)) / 2)) = ( sqrt ((1 - ( cos (2 * (x / 2)))) / 2))

      .= ( sqrt ((1 - (1 - (2 * (( sin (x / 2)) ^2 )))) / 2)) by Th7

      .= |.( sin (x / 2)).| by COMPLEX1: 72;

      per cases ;

        suppose ( sin (x / 2)) >= 0 ;

        hence thesis by A1, ABSVALUE:def 1;

      end;

        suppose ( sin (x / 2)) < 0 ;

        then (( sqrt ((1 - ( cos x)) / 2)) * ( - 1)) = (( - ( sin (x / 2))) * ( - 1)) by A1, ABSVALUE:def 1;

        hence thesis;

      end;

    end;

    theorem :: SIN_COS5:27

    ( cos (x / 2)) = ( sqrt ((1 + ( cos x)) / 2)) or ( cos (x / 2)) = ( - ( sqrt ((1 + ( cos x)) / 2)))

    proof

      

       A1: ( sqrt ((1 + ( cos x)) / 2)) = ( sqrt ((1 + ( cos (2 * (x / 2)))) / 2))

      .= ( sqrt ((1 + ((2 * (( cos (x / 2)) ^2 )) - 1)) / 2)) by Th7

      .= |.( cos (x / 2)).| by COMPLEX1: 72;

      per cases ;

        suppose ( cos (x / 2)) >= 0 ;

        hence thesis by A1, ABSVALUE:def 1;

      end;

        suppose ( cos (x / 2)) < 0 ;

        then (( sqrt ((1 + ( cos x)) / 2)) * ( - 1)) = (( - ( cos (x / 2))) * ( - 1)) by A1, ABSVALUE:def 1;

        hence thesis;

      end;

    end;

    theorem :: SIN_COS5:28

    ( sin (x / 2)) <> 0 implies ( tan (x / 2)) = ((1 - ( cos x)) / ( sin x))

    proof

      assume ( sin (x / 2)) <> 0 ;

      then

       A1: (2 * ( sin (x / 2))) <> 0 ;

      ((1 - ( cos x)) / ( sin x)) = ((1 - (1 - (2 * (( sin (x / 2)) ^2 )))) / ( sin (2 * (x / 2)))) by Th7

      .= (((2 * ( sin (x / 2))) * ( sin (x / 2))) / ((2 * ( sin (x / 2))) * ( cos (x / 2)))) by Th5

      .= ( tan (x / 2)) by A1, XCMPLX_1: 91;

      hence thesis;

    end;

    theorem :: SIN_COS5:29

    ( cos (x / 2)) <> 0 implies ( tan (x / 2)) = (( sin x) / (1 + ( cos x)))

    proof

      assume ( cos (x / 2)) <> 0 ;

      then

       A1: (2 * ( cos (x / 2))) <> 0 ;

      (( sin x) / (1 + ( cos x))) = (((2 * ( sin (x / 2))) * ( cos (x / 2))) / (1 + ( cos (2 * (x / 2))))) by Th5

      .= (((2 * ( sin (x / 2))) * ( cos (x / 2))) / (1 + ((2 * (( cos (x / 2)) ^2 )) - 1))) by Th7

      .= (((2 * ( cos (x / 2))) * ( sin (x / 2))) / ((2 * ( cos (x / 2))) * ( cos (x / 2))))

      .= (( sin (x / 2)) / ( cos (x / 2))) by A1, XCMPLX_1: 91;

      hence thesis;

    end;

    theorem :: SIN_COS5:30

    ( tan (x / 2)) = ( sqrt ((1 - ( cos x)) / (1 + ( cos x)))) or ( tan (x / 2)) = ( - ( sqrt ((1 - ( cos x)) / (1 + ( cos x)))))

    proof

      

       A1: ( sqrt ((1 - ( cos x)) / (1 + ( cos x)))) = ( sqrt ((1 - (1 - (2 * (( sin (x / 2)) ^2 )))) / (1 + ( cos (2 * (x / 2)))))) by Th7

      .= ( sqrt (((1 - 1) + (2 * (( sin (x / 2)) ^2 ))) / (1 + ((2 * (( cos (x / 2)) ^2 )) - 1)))) by Th7

      .= ( sqrt ((( sin (x / 2)) ^2 ) / (( cos (x / 2)) ^2 ))) by XCMPLX_1: 91

      .= ( sqrt (( tan (x / 2)) ^2 )) by XCMPLX_1: 76

      .= |.( tan (x / 2)).| by COMPLEX1: 72;

      per cases ;

        suppose ( tan (x / 2)) >= 0 ;

        hence thesis by A1, ABSVALUE:def 1;

      end;

        suppose ( tan (x / 2)) < 0 ;

        then (( sqrt ((1 - ( cos x)) / (1 + ( cos x)))) * ( - 1)) = (( - ( tan (x / 2))) * ( - 1)) by A1, ABSVALUE:def 1;

        hence thesis;

      end;

    end;

    theorem :: SIN_COS5:31

    ( cos (x / 2)) <> 0 implies ( cot (x / 2)) = ((1 + ( cos x)) / ( sin x))

    proof

      assume ( cos (x / 2)) <> 0 ;

      then

       A1: (2 * ( cos (x / 2))) <> 0 ;

      ((1 + ( cos x)) / ( sin x)) = ((1 + ((2 * (( cos (x / 2)) ^2 )) - 1)) / ( sin (2 * (x / 2)))) by Th7

      .= ((2 * (( cos (x / 2)) * ( cos (x / 2)))) / ((2 * ( sin (x / 2))) * ( cos (x / 2)))) by Th5

      .= (((2 * ( cos (x / 2))) * ( cos (x / 2))) / ((2 * ( cos (x / 2))) * ( sin (x / 2))))

      .= ( cot (x / 2)) by A1, XCMPLX_1: 91;

      hence thesis;

    end;

    theorem :: SIN_COS5:32

    ( sin (x / 2)) <> 0 implies ( cot (x / 2)) = (( sin x) / (1 - ( cos x)))

    proof

      assume ( sin (x / 2)) <> 0 ;

      then

       A1: (2 * ( sin (x / 2))) <> 0 ;

      (( sin x) / (1 - ( cos x))) = (((2 * ( sin (x / 2))) * ( cos (x / 2))) / (1 - ( cos (2 * (x / 2))))) by Th5

      .= (((2 * ( sin (x / 2))) * ( cos (x / 2))) / (1 - (1 - (2 * (( sin (x / 2)) ^2 ))))) by Th7

      .= (((2 * ( sin (x / 2))) * ( cos (x / 2))) / ((2 * ( sin (x / 2))) * ( sin (x / 2))))

      .= (( cos (x / 2)) / ( sin (x / 2))) by A1, XCMPLX_1: 91;

      hence thesis;

    end;

    theorem :: SIN_COS5:33

    ( cot (x / 2)) = ( sqrt ((1 + ( cos x)) / (1 - ( cos x)))) or ( cot (x / 2)) = ( - ( sqrt ((1 + ( cos x)) / (1 - ( cos x)))))

    proof

      

       A1: ( sqrt ((1 + ( cos x)) / (1 - ( cos x)))) = ( sqrt ((1 + ((2 * (( cos (x / 2)) ^2 )) - 1)) / (1 - ( cos (2 * (x / 2)))))) by Th7

      .= ( sqrt ((1 - (1 - (2 * (( cos (x / 2)) ^2 )))) / (1 - (1 - (2 * (( sin (x / 2)) ^2 )))))) by Th7

      .= ( sqrt ((( cos (x / 2)) ^2 ) / (( sin (x / 2)) ^2 ))) by XCMPLX_1: 91

      .= ( sqrt (( cot (x / 2)) ^2 )) by XCMPLX_1: 76

      .= |.( cot (x / 2)).| by COMPLEX1: 72;

      per cases ;

        suppose ( cot (x / 2)) >= 0 ;

        hence thesis by A1, ABSVALUE:def 1;

      end;

        suppose ( cot (x / 2)) < 0 ;

        then (( sqrt ((1 + ( cos x)) / (1 - ( cos x)))) * ( - 1)) = (( - ( cot (x / 2))) * ( - 1)) by A1, ABSVALUE:def 1;

        hence thesis;

      end;

    end;

    theorem :: SIN_COS5:34

    ( sin (x / 2)) <> 0 & ( cos (x / 2)) <> 0 & (1 - (( tan (x / 2)) ^2 )) <> 0 implies ( sec (x / 2)) = ( sqrt ((2 * ( sec x)) / (( sec x) + 1))) or ( sec (x / 2)) = ( - ( sqrt ((2 * ( sec x)) / (( sec x) + 1))))

    proof

      assume that

       A1: ( sin (x / 2)) <> 0 and

       A2: ( cos (x / 2)) <> 0 and

       A3: (1 - (( tan (x / 2)) ^2 )) <> 0 ;

      set b = (( sec (x / 2)) ^2 );

      set a = (1 - (( tan (x / 2)) ^2 ));

      

       A4: (a + b) = ((1 + (( tan (x / 2)) ^2 )) + (1 - (( tan (x / 2)) ^2 ))) by A2, Th11

      .= (1 + 1);

      ( sqrt ((2 * ( sec x)) / (( sec x) + 1))) = ( sqrt ((2 * ((( sec (x / 2)) ^2 ) / (1 - (( tan (x / 2)) ^2 )))) / (( sec (2 * (x / 2))) + 1))) by A1, A2, Th13

      .= ( sqrt ((2 * ((( sec (x / 2)) ^2 ) / (1 - (( tan (x / 2)) ^2 )))) / (((( sec (x / 2)) ^2 ) / (1 - (( tan (x / 2)) ^2 ))) + 1))) by A1, A2, Th13;

      

      then

       A5: ( sqrt ((2 * ( sec x)) / (( sec x) + 1))) = ( sqrt (((2 * (b / a)) * a) / (((b / a) + 1) * a))) by A3, XCMPLX_1: 91

      .= ( sqrt ((2 * ((b / a) * a)) / (((b / a) * a) + (1 * a))))

      .= ( sqrt ((2 * ((b / a) * a)) / (b + a))) by A3, XCMPLX_1: 87

      .= ( sqrt ((2 * b) / 2)) by A3, A4, XCMPLX_1: 87

      .= |.( sec (x / 2)).| by COMPLEX1: 72;

      per cases ;

        suppose ( sec (x / 2)) >= 0 ;

        hence thesis by A5, ABSVALUE:def 1;

      end;

        suppose ( sec (x / 2)) < 0 ;

        then (( sqrt ((2 * ( sec x)) / (( sec x) + 1))) * ( - 1)) = (( - ( sec (x / 2))) * ( - 1)) by A5, ABSVALUE:def 1;

        hence thesis;

      end;

    end;

    theorem :: SIN_COS5:35

    ( sin (x / 2)) <> 0 & ( cos (x / 2)) <> 0 & (1 - (( tan (x / 2)) ^2 )) <> 0 implies ( cosec (x / 2)) = ( sqrt ((2 * ( sec x)) / (( sec x) - 1))) or ( cosec (x / 2)) = ( - ( sqrt ((2 * ( sec x)) / (( sec x) - 1))))

    proof

      assume that

       A1: ( sin (x / 2)) <> 0 and

       A2: ( cos (x / 2)) <> 0 and

       A3: (1 - (( tan (x / 2)) ^2 )) <> 0 ;

      set b = (( sec (x / 2)) ^2 );

      set a = (1 - (( tan (x / 2)) ^2 ));

      

       A4: (b - a) = ((1 + (( tan (x / 2)) ^2 )) - (1 - (( tan (x / 2)) ^2 ))) by A2, Th11

      .= (2 * (( tan (x / 2)) ^2 ));

      ( sqrt ((2 * ( sec x)) / (( sec x) - 1))) = ( sqrt ((2 * ((( sec (x / 2)) ^2 ) / (1 - (( tan (x / 2)) ^2 )))) / (( sec (2 * (x / 2))) - 1))) by A1, A2, Th13

      .= ( sqrt ((2 * ((( sec (x / 2)) ^2 ) / (1 - (( tan (x / 2)) ^2 )))) / (((( sec (x / 2)) ^2 ) / (1 - (( tan (x / 2)) ^2 ))) - 1))) by A1, A2, Th13;

      

      then

       A5: ( sqrt ((2 * ( sec x)) / (( sec x) - 1))) = ( sqrt (((2 * (b / a)) * a) / (((b / a) - 1) * a))) by A3, XCMPLX_1: 91

      .= ( sqrt ((2 * ((b / a) * a)) / (((b / a) * a) - (1 * a))))

      .= ( sqrt ((2 * ((b / a) * a)) / (b - a))) by A3, XCMPLX_1: 87

      .= ( sqrt ((2 * b) / (2 * (( tan (x / 2)) ^2 )))) by A3, A4, XCMPLX_1: 87

      .= ( sqrt ((( sec (x / 2)) ^2 ) / (( tan (x / 2)) ^2 ))) by XCMPLX_1: 91

      .= ( sqrt ((( sec (x / 2)) / ( tan (x / 2))) ^2 )) by XCMPLX_1: 76

      .= ( sqrt (( cosec (x / 2)) ^2 )) by A2, Th1

      .= |.( cosec (x / 2)).| by COMPLEX1: 72;

      per cases ;

        suppose ( cosec (x / 2)) >= 0 ;

        hence thesis by A5, ABSVALUE:def 1;

      end;

        suppose ( cosec (x / 2)) < 0 ;

        then (( sqrt ((2 * ( sec x)) / (( sec x) - 1))) * ( - 1)) = (( - ( cosec (x / 2))) * ( - 1)) by A5, ABSVALUE:def 1;

        hence thesis;

      end;

    end;

    definition

      let x be Real;

      :: SIN_COS5:def1

      func coth (x) -> Real equals (( cosh x) / ( sinh x));

      coherence ;

      :: SIN_COS5:def2

      func sech (x) -> Real equals (1 / ( cosh x));

      coherence ;

      :: SIN_COS5:def3

      func cosech (x) -> Real equals (1 / ( sinh x));

      coherence ;

    end

    theorem :: SIN_COS5:36

    

     Th36: ( coth x) = ((( exp_R x) + ( exp_R ( - x))) / (( exp_R x) - ( exp_R ( - x)))) & ( sech x) = (2 / (( exp_R x) + ( exp_R ( - x)))) & ( cosech x) = (2 / (( exp_R x) - ( exp_R ( - x))))

    proof

      

       A1: ( sech x) = (1 / ( cosh . x)) by SIN_COS2:def 4

      .= (1 / ((( exp_R . x) + ( exp_R . ( - x))) / 2)) by SIN_COS2:def 3

      .= ((1 * 2) / (((( exp_R . x) + ( exp_R . ( - x))) / 2) * 2)) by XCMPLX_1: 91

      .= (2 / (( exp_R . x) + ( exp_R ( - x)))) by SIN_COS:def 23

      .= (2 / (( exp_R x) + ( exp_R ( - x)))) by SIN_COS:def 23;

      

       A2: ( cosech x) = (1 / ( sinh . x)) by SIN_COS2:def 2

      .= (1 / ((( exp_R . x) - ( exp_R . ( - x))) / 2)) by SIN_COS2:def 1

      .= ((1 * 2) / (((( exp_R . x) - ( exp_R . ( - x))) / 2) * 2)) by XCMPLX_1: 91

      .= (2 / (( exp_R . x) - ( exp_R ( - x)))) by SIN_COS:def 23;

      ( coth x) = (( cosh . x) / ( sinh x)) by SIN_COS2:def 4

      .= (( cosh . x) / ( sinh . x)) by SIN_COS2:def 2

      .= (((( exp_R . x) + ( exp_R . ( - x))) / 2) / ( sinh . x)) by SIN_COS2:def 3

      .= (((( exp_R . x) + ( exp_R . ( - x))) / 2) / ((( exp_R . x) - ( exp_R . ( - x))) / 2)) by SIN_COS2:def 1

      .= ((((( exp_R . x) + ( exp_R . ( - x))) / 2) * 2) / (((( exp_R . x) - ( exp_R . ( - x))) / 2) * 2)) by XCMPLX_1: 91

      .= ((( exp_R . x) + ( exp_R . ( - x))) / (( exp_R . x) - ( exp_R ( - x)))) by SIN_COS:def 23

      .= ((( exp_R . x) + ( exp_R . ( - x))) / (( exp_R x) - ( exp_R ( - x)))) by SIN_COS:def 23

      .= ((( exp_R . x) + ( exp_R ( - x))) / (( exp_R x) - ( exp_R ( - x)))) by SIN_COS:def 23

      .= ((( exp_R x) + ( exp_R ( - x))) / (( exp_R x) - ( exp_R ( - x)))) by SIN_COS:def 23;

      hence thesis by A1, A2, SIN_COS:def 23;

    end;

    theorem :: SIN_COS5:37

    (( exp_R x) - ( exp_R ( - x))) <> 0 implies (( tanh x) * ( coth x)) = 1

    proof

      assume

       A1: (( exp_R x) - ( exp_R ( - x))) <> 0 ;

      ( exp_R x) > 0 by SIN_COS: 55;

      then

       A2: (( exp_R x) + ( exp_R ( - x))) > ( 0 + 0 ) by SIN_COS: 55, XREAL_1: 8;

      (( tanh x) * ( coth x)) = (( tanh . x) * ( coth x)) by SIN_COS2:def 6

      .= (((( exp_R . x) - ( exp_R . ( - x))) / (( exp_R . x) + ( exp_R . ( - x)))) * ( coth x)) by SIN_COS2:def 5

      .= (((( exp_R . x) - ( exp_R . ( - x))) / (( exp_R . x) + ( exp_R . ( - x)))) * ((( exp_R x) + ( exp_R ( - x))) / (( exp_R x) - ( exp_R ( - x))))) by Th36

      .= (((( exp_R . x) - ( exp_R . ( - x))) / (( exp_R . x) + ( exp_R ( - x)))) * ((( exp_R x) + ( exp_R ( - x))) / (( exp_R x) - ( exp_R ( - x))))) by SIN_COS:def 23

      .= (((( exp_R x) - ( exp_R . ( - x))) / (( exp_R . x) + ( exp_R ( - x)))) * ((( exp_R x) + ( exp_R ( - x))) / (( exp_R x) - ( exp_R ( - x))))) by SIN_COS:def 23

      .= (((( exp_R x) - ( exp_R ( - x))) / (( exp_R . x) + ( exp_R ( - x)))) * ((( exp_R x) + ( exp_R ( - x))) / (( exp_R x) - ( exp_R ( - x))))) by SIN_COS:def 23

      .= (((( exp_R x) - ( exp_R ( - x))) / (( exp_R x) + ( exp_R ( - x)))) * ((( exp_R x) + ( exp_R ( - x))) / (( exp_R x) - ( exp_R ( - x))))) by SIN_COS:def 23

      .= ((((( exp_R x) - ( exp_R ( - x))) / (( exp_R x) + ( exp_R ( - x)))) * (( exp_R x) + ( exp_R ( - x)))) / (( exp_R x) - ( exp_R ( - x)))) by XCMPLX_1: 74;

      

      then (( tanh x) * ( coth x)) = ((( exp_R x) - ( exp_R ( - x))) / (( exp_R x) - ( exp_R ( - x)))) by A2, XCMPLX_1: 87

      .= 1 by A1, XCMPLX_1: 60;

      hence thesis;

    end;

    theorem :: SIN_COS5:38

    ((( sech x) ^2 ) + (( tanh x) ^2 )) = 1

    proof

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

      then

       A1: (( cosh . x) ^2 ) <> 0 by SQUARE_1: 12;

      ((( sech x) ^2 ) + (( tanh x) ^2 )) = (((1 / ( cosh x)) ^2 ) + (( tanh . x) ^2 )) by SIN_COS2:def 6

      .= (((1 / ( cosh . x)) ^2 ) + (( tanh . x) ^2 )) by SIN_COS2:def 4

      .= (((1 ^2 ) / (( cosh . x) ^2 )) + (( tanh . x) ^2 )) by XCMPLX_1: 76

      .= (((1 ^2 ) / (( cosh . x) ^2 )) + ((( sinh . x) / ( cosh . x)) ^2 )) by SIN_COS2: 17

      .= ((1 / (( cosh . x) ^2 )) + ((( sinh . x) ^2 ) / (( cosh . x) ^2 ))) by XCMPLX_1: 76

      .= ((1 + (( sinh . x) ^2 )) / (( cosh . x) ^2 )) by XCMPLX_1: 62

      .= ((((( cosh . x) ^2 ) - (( sinh . x) ^2 )) + (( sinh . x) ^2 )) / (( cosh . x) ^2 )) by SIN_COS2: 14

      .= ((( cosh . x) ^2 ) / (( cosh . x) ^2 ));

      hence thesis by A1, XCMPLX_1: 60;

    end;

    theorem :: SIN_COS5:39

    ( sinh x) <> 0 implies ((( coth x) ^2 ) - (( cosech x) ^2 )) = 1

    proof

      assume ( sinh x) <> 0 ;

      then

       A1: (( sinh x) ^2 ) <> 0 by SQUARE_1: 12;

      ((( coth x) ^2 ) - (( cosech x) ^2 )) = (((( cosh x) ^2 ) / (( sinh x) ^2 )) - ((1 / ( sinh x)) ^2 )) by XCMPLX_1: 76

      .= (((( cosh x) ^2 ) / (( sinh x) ^2 )) - ((1 ^2 ) / (( sinh x) ^2 ))) by XCMPLX_1: 76

      .= (((( cosh x) ^2 ) - 1) / (( sinh x) ^2 )) by XCMPLX_1: 120

      .= (((( cosh x) ^2 ) - ((( cosh . x) ^2 ) - (( sinh . x) ^2 ))) / (( sinh x) ^2 )) by SIN_COS2: 14

      .= ((((( cosh x) ^2 ) - (( cosh . x) ^2 )) + (( sinh . x) ^2 )) / (( sinh x) ^2 ))

      .= ((((( cosh x) ^2 ) - (( cosh x) ^2 )) + (( sinh . x) ^2 )) / (( sinh x) ^2 )) by SIN_COS2:def 4

      .= (( 0 + (( sinh x) ^2 )) / (( sinh x) ^2 )) by SIN_COS2:def 2;

      hence thesis by A1, XCMPLX_1: 60;

    end;

    

     Lm1: ( coth ( - x)) = ( - ( coth x))

    proof

      ( coth ( - x)) = (( cosh . ( - x)) / ( sinh ( - x))) by SIN_COS2:def 4

      .= (( cosh . ( - x)) / ( sinh . ( - x))) by SIN_COS2:def 2

      .= (( cosh . x) / ( sinh . ( - x))) by SIN_COS2: 19

      .= (( cosh . x) / ( - ( sinh . x))) by SIN_COS2: 19

      .= ( - (( cosh . x) / ( sinh . x))) by XCMPLX_1: 188

      .= ( - (( cosh x) / ( sinh . x))) by SIN_COS2:def 4

      .= ( - ( coth x)) by SIN_COS2:def 2;

      hence thesis;

    end;

    theorem :: SIN_COS5:40

    

     Th40: ( sinh x1) <> 0 & ( sinh x2) <> 0 implies ( coth (x1 + x2)) = ((1 + (( coth x1) * ( coth x2))) / (( coth x1) + ( coth x2)))

    proof

      assume that

       A1: ( sinh x1) <> 0 and

       A2: ( sinh x2) <> 0 ;

      

       A3: ( sinh . x1) <> 0 by A1, SIN_COS2:def 2;

      

       A4: ( sinh . x2) <> 0 by A2, SIN_COS2:def 2;

      ( coth (x1 + x2)) = (( cosh . (x1 + x2)) / ( sinh (x1 + x2))) by SIN_COS2:def 4

      .= (( cosh . (x1 + x2)) / ( sinh . (x1 + x2))) by SIN_COS2:def 2

      .= (((( cosh . x1) * ( cosh . x2)) + (( sinh . x1) * ( sinh . x2))) / ( sinh . (x1 + x2))) by SIN_COS2: 20

      .= (((( cosh . x1) * ( cosh . x2)) + (( sinh . x1) * ( sinh . x2))) / ((( sinh . x1) * ( cosh . x2)) + (( cosh . x1) * ( sinh . x2)))) by SIN_COS2: 21

      .= ((((( cosh . x1) * ( cosh . x2)) + (( sinh . x1) * ( sinh . x2))) / (( sinh . x1) * ( sinh . x2))) / (((( sinh . x1) * ( cosh . x2)) + (( cosh . x1) * ( sinh . x2))) / (( sinh . x1) * ( sinh . x2)))) by A3, A4, XCMPLX_1: 6, XCMPLX_1: 55

      .= ((((( cosh . x1) * ( cosh . x2)) / (( sinh . x1) * ( sinh . x2))) + ((( sinh . x1) * ( sinh . x2)) / (( sinh . x1) * ( sinh . x2)))) / (((( sinh . x1) * ( cosh . x2)) + (( cosh . x1) * ( sinh . x2))) / (( sinh . x1) * ( sinh . x2)))) by XCMPLX_1: 62

      .= ((((( cosh . x1) * ( cosh . x2)) / (( sinh . x1) * ( sinh . x2))) + 1) / (((( sinh . x1) * ( cosh . x2)) + (( cosh . x1) * ( sinh . x2))) / (( sinh . x1) * ( sinh . x2)))) by A3, A4, XCMPLX_1: 6, XCMPLX_1: 60

      .= (((((( cosh . x1) / ( sinh . x1)) * ( cosh . x2)) / ( sinh . x2)) + 1) / (((( sinh . x1) * ( cosh . x2)) + (( cosh . x1) * ( sinh . x2))) / (( sinh . x1) * ( sinh . x2)))) by XCMPLX_1: 83

      .= ((((( cosh . x1) / ( sinh . x1)) * (( cosh . x2) / ( sinh . x2))) + 1) / (((( sinh . x1) * ( cosh . x2)) + (( cosh . x1) * ( sinh . x2))) / (( sinh . x1) * ( sinh . x2)))) by XCMPLX_1: 74

      .= ((((( cosh . x1) / ( sinh . x1)) * (( cosh . x2) / ( sinh . x2))) + 1) / (((( sinh . x1) * ( cosh . x2)) / (( sinh . x1) * ( sinh . x2))) + ((( cosh . x1) * ( sinh . x2)) / (( sinh . x1) * ( sinh . x2))))) by XCMPLX_1: 62

      .= ((((( cosh . x1) / ( sinh . x1)) * (( cosh . x2) / ( sinh . x2))) + 1) / ((((( sinh . x1) / ( sinh . x1)) * ( cosh . x2)) / ( sinh . x2)) + ((( cosh . x1) * ( sinh . x2)) / (( sinh . x1) * ( sinh . x2))))) by XCMPLX_1: 83

      .= ((((( cosh . x1) / ( sinh . x1)) * (( cosh . x2) / ( sinh . x2))) + 1) / ((((( sinh . x1) / ( sinh . x1)) * ( cosh . x2)) / ( sinh . x2)) + (((( cosh . x1) / ( sinh . x1)) * ( sinh . x2)) / ( sinh . x2)))) by XCMPLX_1: 83

      .= ((((( cosh . x1) / ( sinh . x1)) * (( cosh . x2) / ( sinh . x2))) + 1) / (((1 * ( cosh . x2)) / ( sinh . x2)) + (((( cosh . x1) / ( sinh . x1)) * ( sinh . x2)) / ( sinh . x2)))) by A3, XCMPLX_1: 60

      .= ((((( cosh . x1) / ( sinh . x1)) * (( cosh . x2) / ( sinh . x2))) + 1) / ((( cosh . x2) / ( sinh . x2)) + (( cosh . x1) / ( sinh . x1)))) by A4, XCMPLX_1: 89

      .= ((((( cosh x1) / ( sinh . x1)) * (( cosh . x2) / ( sinh . x2))) + 1) / ((( cosh . x2) / ( sinh . x2)) + (( cosh . x1) / ( sinh . x1)))) by SIN_COS2:def 4

      .= ((((( cosh x1) / ( sinh . x1)) * (( cosh x2) / ( sinh . x2))) + 1) / ((( cosh . x2) / ( sinh . x2)) + (( cosh . x1) / ( sinh . x1)))) by SIN_COS2:def 4

      .= ((((( cosh x1) / ( sinh . x1)) * (( cosh x2) / ( sinh . x2))) + 1) / ((( cosh x2) / ( sinh . x2)) + (( cosh . x1) / ( sinh . x1)))) by SIN_COS2:def 4

      .= ((((( cosh x1) / ( sinh . x1)) * (( cosh x2) / ( sinh . x2))) + 1) / ((( cosh x2) / ( sinh . x2)) + (( cosh x1) / ( sinh . x1)))) by SIN_COS2:def 4

      .= ((((( cosh x1) / ( sinh x1)) * (( cosh x2) / ( sinh . x2))) + 1) / ((( cosh x2) / ( sinh . x2)) + (( cosh x1) / ( sinh . x1)))) by SIN_COS2:def 2

      .= ((((( cosh x1) / ( sinh x1)) * (( cosh x2) / ( sinh . x2))) + 1) / ((( cosh x2) / ( sinh x2)) + (( cosh x1) / ( sinh . x1)))) by SIN_COS2:def 2

      .= ((((( cosh x1) / ( sinh x1)) * (( cosh x2) / ( sinh . x2))) + 1) / ((( cosh x2) / ( sinh x2)) + (( cosh x1) / ( sinh x1)))) by SIN_COS2:def 2

      .= (((( coth x1) * ( coth x2)) + 1) / (( coth x2) + ( coth x1))) by SIN_COS2:def 2;

      hence thesis;

    end;

    theorem :: SIN_COS5:41

    ( sinh x1) <> 0 & ( sinh x2) <> 0 implies ( coth (x1 - x2)) = ((1 - (( coth x1) * ( coth x2))) / (( coth x1) - ( coth x2)))

    proof

      assume that

       A1: ( sinh x1) <> 0 and

       A2: ( sinh x2) <> 0 ;

      ( - ( sinh . x2)) <> 0 by A2, SIN_COS2:def 2;

      then ( sinh . ( - x2)) <> 0 by SIN_COS2: 19;

      then

       A3: ( sinh ( - x2)) <> 0 by SIN_COS2:def 2;

      ( coth (x1 - x2)) = ( coth (x1 + ( - x2)))

      .= ((1 + (( coth x1) * ( coth ( - x2)))) / (( coth x1) + ( coth ( - x2)))) by A1, A3, Th40

      .= ((1 + (( coth x1) * ( - ( coth x2)))) / (( coth x1) + ( coth ( - x2)))) by Lm1

      .= ((1 - (( coth x1) * ( coth x2))) / (( coth x1) + ( - ( coth x2)))) by Lm1

      .= ((1 - (( coth x1) * ( coth x2))) / (( coth x1) - ( coth x2)));

      hence thesis;

    end;

    theorem :: SIN_COS5:42

    ( sinh x1) <> 0 & ( sinh x2) <> 0 implies (( coth x1) + ( coth x2)) = (( sinh (x1 + x2)) / (( sinh x1) * ( sinh x2))) & (( coth x1) - ( coth x2)) = ( - (( sinh (x1 - x2)) / (( sinh x1) * ( sinh x2))))

    proof

      assume that

       A1: ( sinh x1) <> 0 and

       A2: ( sinh x2) <> 0 ;

      

       A3: ( sinh . x1) <> 0 by A1, SIN_COS2:def 2;

      

       A4: ( sinh . x2) <> 0 by A2, SIN_COS2:def 2;

      

       A5: ( - (( sinh (x1 - x2)) / (( sinh x1) * ( sinh x2)))) = ( - (( sinh . (x1 - x2)) / (( sinh x1) * ( sinh x2)))) by SIN_COS2:def 2

      .= ( - (( sinh . (x1 - x2)) / (( sinh . x1) * ( sinh x2)))) by SIN_COS2:def 2

      .= ( - (( sinh . (x1 - x2)) / (( sinh . x1) * ( sinh . x2)))) by SIN_COS2:def 2

      .= ( - (((( sinh . x1) * ( cosh . x2)) - (( cosh . x1) * ( sinh . x2))) / (( sinh . x1) * ( sinh . x2)))) by SIN_COS2: 21

      .= ( - (((( sinh . x1) * ( cosh . x2)) / (( sinh . x1) * ( sinh . x2))) - ((( cosh . x1) * ( sinh . x2)) / (( sinh . x1) * ( sinh . x2))))) by XCMPLX_1: 120

      .= ( - ((((( sinh . x1) / ( sinh . x1)) * ( cosh . x2)) / ( sinh . x2)) - ((( cosh . x1) * ( sinh . x2)) / (( sinh . x1) * ( sinh . x2))))) by XCMPLX_1: 83

      .= ( - ((((( sinh . x1) / ( sinh . x1)) * ( cosh . x2)) / ( sinh . x2)) - (((( sinh . x2) / ( sinh . x2)) * ( cosh . x1)) / ( sinh . x1)))) by XCMPLX_1: 83

      .= ( - (((1 * ( cosh . x2)) / ( sinh . x2)) - (((( sinh . x2) / ( sinh . x2)) * ( cosh . x1)) / ( sinh . x1)))) by A3, XCMPLX_1: 60

      .= ( - ((( cosh . x2) / ( sinh . x2)) - ((1 * ( cosh . x1)) / ( sinh . x1)))) by A4, XCMPLX_1: 60

      .= ( - ((( cosh x2) / ( sinh . x2)) - (( cosh . x1) / ( sinh . x1)))) by SIN_COS2:def 4

      .= ( - ((( cosh x2) / ( sinh . x2)) - (( cosh x1) / ( sinh . x1)))) by SIN_COS2:def 4

      .= ( - ((( cosh x2) / ( sinh x2)) - (( cosh x1) / ( sinh . x1)))) by SIN_COS2:def 2

      .= ( - (( coth x2) - (( cosh x1) / ( sinh x1)))) by SIN_COS2:def 2

      .= (( coth x1) - ( coth x2));

      (( sinh (x1 + x2)) / (( sinh x1) * ( sinh x2))) = (( sinh . (x1 + x2)) / (( sinh x1) * ( sinh x2))) by SIN_COS2:def 2

      .= (((( sinh . x1) * ( cosh . x2)) + (( cosh . x1) * ( sinh . x2))) / (( sinh x1) * ( sinh x2))) by SIN_COS2: 21

      .= (((( sinh . x1) * ( cosh . x2)) + (( cosh . x1) * ( sinh . x2))) / (( sinh . x1) * ( sinh x2))) by SIN_COS2:def 2

      .= (((( sinh . x1) * ( cosh . x2)) + (( cosh . x1) * ( sinh . x2))) / (( sinh . x1) * ( sinh . x2))) by SIN_COS2:def 2

      .= (((( sinh . x1) * ( cosh . x2)) / (( sinh . x1) * ( sinh . x2))) + ((( cosh . x1) * ( sinh . x2)) / (( sinh . x1) * ( sinh . x2)))) by XCMPLX_1: 62

      .= ((((( sinh . x1) / ( sinh . x1)) * ( cosh . x2)) / ( sinh . x2)) + ((( cosh . x1) * ( sinh . x2)) / (( sinh . x1) * ( sinh . x2)))) by XCMPLX_1: 83

      .= (((1 * ( cosh . x2)) / ( sinh . x2)) + ((( cosh . x1) * ( sinh . x2)) / (( sinh . x1) * ( sinh . x2)))) by A3, XCMPLX_1: 60

      .= ((( cosh . x2) / ( sinh . x2)) + (((( cosh . x1) / ( sinh . x1)) * ( sinh . x2)) / ( sinh . x2))) by XCMPLX_1: 83

      .= ((( cosh . x2) / ( sinh . x2)) + ((( cosh . x1) / ( sinh . x1)) * (( sinh . x2) / ( sinh . x2)))) by XCMPLX_1: 74

      .= ((( cosh . x2) / ( sinh . x2)) + ((( cosh . x1) / ( sinh . x1)) * 1)) by A4, XCMPLX_1: 60

      .= ((( cosh . x2) / ( sinh . x2)) + (( cosh . x1) / ( sinh x1))) by SIN_COS2:def 2

      .= ((( cosh . x2) / ( sinh x2)) + (( cosh . x1) / ( sinh x1))) by SIN_COS2:def 2

      .= ((( cosh x2) / ( sinh x2)) + (( cosh . x1) / ( sinh x1))) by SIN_COS2:def 4

      .= (( coth x2) + ( coth x1)) by SIN_COS2:def 4;

      hence thesis by A5;

    end;

    

     Lm2: (( cosh . x) ^2 ) = (1 + (( sinh . x) ^2 ))

    proof

      (((( cosh . x) ^2 ) - (( sinh . x) ^2 )) + (( sinh . x) ^2 )) = (1 + (( sinh . x) ^2 )) by SIN_COS2: 14;

      hence thesis;

    end;

    

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

    proof

      (((( cosh . x) ^2 ) - (( sinh . x) ^2 )) + (( sinh . x) ^2 )) = (1 + (( sinh . x) ^2 )) by SIN_COS2: 14;

      hence thesis;

    end;

    theorem :: SIN_COS5:43

    ( sinh (3 * x)) = ((3 * ( sinh x)) + (4 * (( sinh x) |^ 3)))

    proof

      ( sinh (3 * x)) = ( sinh . ((x + x) + x)) by SIN_COS2:def 2

      .= ((( sinh . (2 * x)) * ( cosh . x)) + (( cosh . (2 * x)) * ( sinh . x))) by SIN_COS2: 21

      .= ((((2 * ( sinh . x)) * ( cosh . x)) * ( cosh . x)) + (( cosh . (2 * x)) * ( sinh . x))) by SIN_COS2: 23

      .= (((2 * ( sinh . x)) * (( cosh . x) ^2 )) + (((2 * (( cosh . x) ^2 )) - 1) * ( sinh . x))) by SIN_COS2: 23

      .= (((2 * ( sinh . x)) * (1 + (( sinh . x) ^2 ))) + (((2 * (( cosh . x) ^2 )) - 1) * ( sinh . x))) by Lm2

      .= (((2 * ( sinh . x)) * (1 + (( sinh . x) ^2 ))) + (((2 * (1 + (( sinh . x) ^2 ))) - 1) * ( sinh . x))) by Lm2

      .= (((2 * ( sinh . x)) + (((2 + 2) * ( sinh . x)) * (( sinh . x) ^2 ))) + ( sinh . x))

      .= (((2 * ( sinh . x)) + ((4 * (( sinh . x) |^ 1)) * (( sinh . x) ^2 ))) + ( sinh . x))

      .= ((3 * ( sinh . x)) + (4 * (((( sinh . x) |^ 1) * ( sinh . x)) * ( sinh . x))))

      .= ((3 * ( sinh . x)) + (4 * ((( sinh . x) |^ (1 + 1)) * ( sinh . x)))) by NEWTON: 6

      .= ((3 * ( sinh . x)) + (4 * (( sinh . x) |^ (2 + 1)))) by NEWTON: 6

      .= ((3 * ( sinh x)) + (4 * (( sinh . x) |^ 3))) by SIN_COS2:def 2;

      hence thesis by SIN_COS2:def 2;

    end;

    theorem :: SIN_COS5:44

    ( cosh (3 * x)) = ((4 * (( cosh x) |^ 3)) - (3 * ( cosh x)))

    proof

      ( cosh (3 * x)) = ( cosh . ((x + x) + x)) by SIN_COS2:def 4

      .= ((( cosh . (2 * x)) * ( cosh . x)) + (( sinh . (2 * x)) * ( sinh . x))) by SIN_COS2: 20

      .= ((((2 * (( cosh . x) ^2 )) - 1) * ( cosh . x)) + (( sinh . (2 * x)) * ( sinh . x))) by SIN_COS2: 23

      .= ((((2 * (( cosh . x) ^2 )) - 1) * ( cosh . x)) + (((2 * ( sinh . x)) * ( cosh . x)) * ( sinh . x))) by SIN_COS2: 23

      .= ((((2 * (( cosh . x) ^2 )) - 1) * ( cosh . x)) + ((2 * (( sinh . x) ^2 )) * ( cosh . x)))

      .= ((((2 * (( cosh . x) ^2 )) - 1) * ( cosh . x)) + ((2 * ((( cosh . x) ^2 ) - 1)) * ( cosh . x))) by Lm3

      .= ((4 * ((( cosh . x) * ( cosh . x)) * ( cosh . x))) - (3 * ( cosh . x)))

      .= ((4 * (((( cosh . x) |^ 1) * ( cosh . x)) * ( cosh . x))) - (3 * ( cosh . x)))

      .= ((4 * ((( cosh . x) |^ (1 + 1)) * ( cosh . x))) - (3 * ( cosh . x))) by NEWTON: 6

      .= ((4 * (( cosh . x) |^ (2 + 1))) - (3 * ( cosh . x))) by NEWTON: 6

      .= ((4 * (( cosh . x) |^ 3)) - (3 * ( cosh x))) by SIN_COS2:def 4;

      hence thesis by SIN_COS2:def 4;

    end;

    theorem :: SIN_COS5:45

    ( sinh x) <> 0 implies ( coth (2 * x)) = ((1 + (( coth x) ^2 )) / (2 * ( coth x)))

    proof

      assume ( sinh x) <> 0 ;

      then

       A1: ( sinh . x) <> 0 by SIN_COS2:def 2;

      then

       A2: (( sinh . x) ^2 ) <> 0 by SQUARE_1: 12;

      ( coth (2 * x)) = (( cosh . (2 * x)) / ( sinh (2 * x))) by SIN_COS2:def 4

      .= (( cosh . (2 * x)) / ( sinh . (2 * x))) by SIN_COS2:def 2

      .= (((2 * (( cosh . x) ^2 )) - 1) / ( sinh . (2 * x))) by SIN_COS2: 23

      .= (((2 * (( cosh . x) ^2 )) - 1) / ((2 * ( sinh . x)) * ( cosh . x))) by SIN_COS2: 23

      .= ((((2 * (( cosh . x) ^2 )) - 1) / (( sinh . x) ^2 )) / (((2 * ( sinh . x)) * ( cosh . x)) / (( sinh . x) ^2 ))) by A2, XCMPLX_1: 55

      .= ((((2 * (( cosh . x) ^2 )) - ((( cosh . x) ^2 ) - (( sinh . x) ^2 ))) / (( sinh . x) ^2 )) / (((2 * ( sinh . x)) * ( cosh . x)) / (( sinh . x) ^2 ))) by SIN_COS2: 14

      .= (((((2 - 1) * (( cosh . x) ^2 )) + (( sinh . x) ^2 )) / (( sinh . x) ^2 )) / (((2 * ( sinh . x)) * ( cosh . x)) / (( sinh . x) ^2 )))

      .= ((((( cosh . x) ^2 ) / (( sinh . x) ^2 )) + ((( sinh . x) ^2 ) / (( sinh . x) ^2 ))) / (((2 * ( sinh . x)) * ( cosh . x)) / (( sinh . x) ^2 ))) by XCMPLX_1: 62

      .= ((((( cosh . x) / ( sinh . x)) ^2 ) + ((( sinh . x) ^2 ) / (( sinh . x) ^2 ))) / (((2 * ( sinh . x)) * ( cosh . x)) / (( sinh . x) ^2 ))) by XCMPLX_1: 76

      .= ((((( cosh . x) / ( sinh . x)) ^2 ) + ((( sinh . x) / ( sinh . x)) ^2 )) / (((2 * ( sinh . x)) * ( cosh . x)) / (( sinh . x) ^2 ))) by XCMPLX_1: 76

      .= ((((( cosh . x) / ( sinh . x)) ^2 ) + (1 ^2 )) / (((2 * ( cosh . x)) * ( sinh . x)) / (( sinh . x) * ( sinh . x)))) by A1, XCMPLX_1: 60

      .= ((((( cosh . x) / ( sinh . x)) ^2 ) + 1) / ((((2 * ( cosh . x)) * ( sinh . x)) / ( sinh . x)) / ( sinh . x))) by XCMPLX_1: 78

      .= ((((( cosh . x) / ( sinh . x)) ^2 ) + 1) / ((2 * ( cosh . x)) / ( sinh . x))) by A1, XCMPLX_1: 89

      .= ((((( cosh . x) / ( sinh . x)) ^2 ) + 1) / (2 * (( cosh . x) / ( sinh . x)))) by XCMPLX_1: 74

      .= ((((( cosh x) / ( sinh . x)) ^2 ) + 1) / (2 * (( cosh . x) / ( sinh . x)))) by SIN_COS2:def 4

      .= ((((( cosh x) / ( sinh . x)) ^2 ) + 1) / (2 * (( cosh x) / ( sinh . x)))) by SIN_COS2:def 4

      .= ((((( cosh x) / ( sinh x)) ^2 ) + 1) / (2 * (( cosh x) / ( sinh . x)))) by SIN_COS2:def 2

      .= (((( coth x) ^2 ) + 1) / (2 * (( cosh x) / ( sinh x)))) by SIN_COS2:def 2;

      hence thesis;

    end;

    

     Lm4: x > 0 implies ( sinh x) >= 0

    proof

      assume

       A1: x > 0 ;

      then (x + ( - x)) > ( 0 + ( - x)) by XREAL_1: 8;

      then

       A2: ( exp_R . ( - x)) <= 1 by SIN_COS: 53;

      ( exp_R . x) >= 1 by A1, SIN_COS: 52;

      then (( exp_R . x) - ( exp_R . ( - x))) >= (1 - 1) by A2, XREAL_1: 13;

      then ((( exp_R . x) - ( exp_R . ( - x))) / 2) >= 0 by XREAL_1: 136;

      then ( sinh . x) >= 0 by SIN_COS2:def 1;

      hence thesis by SIN_COS2:def 2;

    end;

    theorem :: SIN_COS5:46

    x >= 0 implies ( sinh x) >= 0

    proof

      assume

       A1: x >= 0 ;

      per cases by A1, XXREAL_0: 1;

        suppose x > 0 ;

        hence thesis by Lm4;

      end;

        suppose x = 0 ;

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

      end;

    end;

    theorem :: SIN_COS5:47

    x <= 0 implies ( sinh x) <= 0

    proof

      assume

       A1: x <= 0 ;

      per cases by A1, XXREAL_0: 1;

        suppose

         A2: x < 0 ;

        then ( - x) > 0 by XREAL_1: 58;

        then

         A3: ( exp_R . ( - x)) >= 1 by SIN_COS: 52;

        ( exp_R . x) <= 1 by A2, SIN_COS: 53;

        then (( exp_R . x) - ( exp_R . ( - x))) <= (1 - 1) by A3, XREAL_1: 13;

        then ((( exp_R . x) - ( exp_R . ( - x))) / 2) <= 0 by XREAL_1: 138;

        then ( sinh . x) <= 0 by SIN_COS2:def 1;

        hence thesis by SIN_COS2:def 2;

      end;

        suppose x = 0 ;

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

      end;

    end;

    theorem :: SIN_COS5:48

    ( cosh (x / 2)) = ( sqrt ((( cosh x) + 1) / 2))

    proof

      

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

      ( sqrt ((( cosh x) + 1) / 2)) = ( sqrt ((( cosh . (2 * (x / 2))) + 1) / 2)) by SIN_COS2:def 4

      .= ( sqrt ((((2 * (( cosh . (x / 2)) ^2 )) - 1) + 1) / 2)) by SIN_COS2: 23

      .= ( cosh . (x / 2)) by A1, SQUARE_1: 22;

      hence thesis by SIN_COS2:def 4;

    end;

    theorem :: SIN_COS5:49

    ( sinh (x / 2)) <> 0 implies ( tanh (x / 2)) = ((( cosh x) - 1) / ( sinh x))

    proof

      assume ( sinh (x / 2)) <> 0 ;

      then

       A1: (2 * ( sinh . (x / 2))) <> 0 by SIN_COS2:def 2;

      ((( cosh x) - 1) / ( sinh x)) = ((( cosh . (2 * (x / 2))) - 1) / ( sinh (2 * (x / 2)))) by SIN_COS2:def 4

      .= ((((2 * (( cosh . (x / 2)) ^2 )) - 1) - 1) / ( sinh (2 * (x / 2)))) by SIN_COS2: 23

      .= ((2 * ((( cosh . (x / 2)) ^2 ) - 1)) / ( sinh (2 * (x / 2))))

      .= ((2 * (( sinh . (x / 2)) ^2 )) / ( sinh (2 * (x / 2)))) by Lm3

      .= ((2 * (( sinh . (x / 2)) ^2 )) / ( sinh . (2 * (x / 2)))) by SIN_COS2:def 2

      .= (((2 * ( sinh . (x / 2))) * ( sinh . (x / 2))) / ((2 * ( sinh . (x / 2))) * ( cosh . (x / 2)))) by SIN_COS2: 23

      .= (( sinh . (x / 2)) / ( cosh . (x / 2))) by A1, XCMPLX_1: 91

      .= ( tanh . (x / 2)) by SIN_COS2: 17

      .= ( tanh (x / 2)) by SIN_COS2:def 6;

      hence thesis;

    end;

    theorem :: SIN_COS5:50

    ( cosh (x / 2)) <> 0 implies ( tanh (x / 2)) = (( sinh x) / (( cosh x) + 1))

    proof

      assume ( cosh (x / 2)) <> 0 ;

      then

       A1: (2 * ( cosh . (x / 2))) <> 0 by SIN_COS2:def 4;

      (( sinh x) / (( cosh x) + 1)) = (( sinh . (2 * (x / 2))) / (( cosh (2 * (x / 2))) + 1)) by SIN_COS2:def 2

      .= (( sinh . (2 * (x / 2))) / (( cosh . (2 * (x / 2))) + 1)) by SIN_COS2:def 4

      .= (((2 * ( sinh . (x / 2))) * ( cosh . (x / 2))) / (( cosh . (2 * (x / 2))) + 1)) by SIN_COS2: 23

      .= (((2 * ( sinh . (x / 2))) * ( cosh . (x / 2))) / (((2 * (( cosh . (x / 2)) ^2 )) - 1) + 1)) by SIN_COS2: 23

      .= (((2 * ( cosh . (x / 2))) * ( sinh . (x / 2))) / ((2 * ( cosh . (x / 2))) * ( cosh . (x / 2))))

      .= (( sinh . (x / 2)) / ( cosh . (x / 2))) by A1, XCMPLX_1: 91

      .= ( tanh . (x / 2)) by SIN_COS2: 17;

      hence thesis by SIN_COS2:def 6;

    end;

    theorem :: SIN_COS5:51

    ( sinh (x / 2)) <> 0 implies ( coth (x / 2)) = (( sinh x) / (( cosh x) - 1))

    proof

      assume ( sinh (x / 2)) <> 0 ;

      then

       A1: (2 * ( sinh . (x / 2))) <> 0 by SIN_COS2:def 2;

      (( sinh x) / (( cosh x) - 1)) = (( sinh . (2 * (x / 2))) / (( cosh (2 * (x / 2))) - 1)) by SIN_COS2:def 2

      .= (( sinh . (2 * (x / 2))) / (( cosh . (2 * (x / 2))) - 1)) by SIN_COS2:def 4

      .= (((2 * ( sinh . (x / 2))) * ( cosh . (x / 2))) / (( cosh . (2 * (x / 2))) - 1)) by SIN_COS2: 23

      .= (((2 * ( sinh . (x / 2))) * ( cosh . (x / 2))) / (((2 * (( cosh . (x / 2)) ^2 )) - 1) - 1)) by SIN_COS2: 23

      .= (((2 * ( sinh . (x / 2))) * ( cosh . (x / 2))) / (2 * ((( cosh . (x / 2)) ^2 ) - 1)))

      .= (((2 * ( sinh . (x / 2))) * ( cosh . (x / 2))) / (2 * (( sinh . (x / 2)) ^2 ))) by Lm3

      .= (((2 * ( sinh . (x / 2))) * ( cosh . (x / 2))) / ((2 * ( sinh . (x / 2))) * ( sinh . (x / 2))))

      .= (( cosh . (x / 2)) / ( sinh . (x / 2))) by A1, XCMPLX_1: 91

      .= (( cosh (x / 2)) / ( sinh . (x / 2))) by SIN_COS2:def 4

      .= (( cosh (x / 2)) / ( sinh (x / 2))) by SIN_COS2:def 2;

      hence thesis;

    end;

    theorem :: SIN_COS5:52

    ( cosh (x / 2)) <> 0 implies ( coth (x / 2)) = ((( cosh x) + 1) / ( sinh x))

    proof

      assume ( cosh (x / 2)) <> 0 ;

      then

       A1: (2 * ( cosh . (x / 2))) <> 0 by SIN_COS2:def 4;

      ((( cosh x) + 1) / ( sinh x)) = ((( cosh . (2 * (x / 2))) + 1) / ( sinh (2 * (x / 2)))) by SIN_COS2:def 4

      .= ((((2 * (( cosh . (x / 2)) ^2 )) - 1) + 1) / ( sinh (2 * (x / 2)))) by SIN_COS2: 23

      .= ((2 * (( cosh . (x / 2)) ^2 )) / ( sinh . (2 * (x / 2)))) by SIN_COS2:def 2

      .= ((2 * (( cosh . (x / 2)) * ( cosh . (x / 2)))) / ((2 * ( sinh . (x / 2))) * ( cosh . (x / 2)))) by SIN_COS2: 23

      .= (((2 * ( cosh . (x / 2))) * ( cosh . (x / 2))) / ((2 * ( cosh . (x / 2))) * ( sinh . (x / 2))))

      .= (( cosh . (x / 2)) / ( sinh . (x / 2))) by A1, XCMPLX_1: 91

      .= (( cosh (x / 2)) / ( sinh . (x / 2))) by SIN_COS2:def 4

      .= (( cosh (x / 2)) / ( sinh (x / 2))) by SIN_COS2:def 2;

      hence thesis;

    end;