sin_cos4.miz

    begin

    reserve th,th1,th2,th3 for Real;

    definition

      let th be Real;

      :: SIN_COS4:def1

      func tan (th) -> Real equals (( sin th) / ( cos th));

      correctness ;

    end

    definition

      let th be Real;

      :: SIN_COS4:def2

      func cot (th) -> Real equals (( cos th) / ( sin th));

      correctness ;

    end

    definition

      let th be Real;

      :: SIN_COS4:def3

      func cosec (th) -> Real equals (1 / ( sin th));

      correctness ;

    end

    definition

      let th be Real;

      :: SIN_COS4:def4

      func sec (th) -> Real equals (1 / ( cos th));

      correctness ;

    end

    theorem :: SIN_COS4:1

    ( tan ( - th)) = ( - ( tan th))

    proof

      ( tan ( - th)) = (( sin ( - th)) / ( cos th)) by SIN_COS: 31

      .= (( - ( sin th)) / ( cos th)) by SIN_COS: 31

      .= ( - ( tan th)) by XCMPLX_1: 187;

      hence thesis;

    end;

    theorem :: SIN_COS4:2

    ( cosec ( - th)) = ( - (1 / ( sin th)))

    proof

      ( cosec ( - th)) = (1 / ( - ( sin th))) by SIN_COS: 31

      .= ( - (1 / ( sin th))) by XCMPLX_1: 188;

      hence thesis;

    end;

    theorem :: SIN_COS4:3

    ( cot ( - th)) = ( - ( cot th))

    proof

      ( cot ( - th)) = (( cos th) / ( sin ( - th))) by SIN_COS: 31

      .= (( cos th) / ( - ( sin th))) by SIN_COS: 31

      .= ( - ( cot th)) by XCMPLX_1: 188;

      hence thesis;

    end;

    theorem :: SIN_COS4:4



     Th4: (( sin th) * ( sin th)) = (1 - (( cos th) * ( cos th)))

    proof

      (( sin th) * ( sin th)) = ((( sin th) * ( sin th)) + (1 - 1))

      .= ((( sin th) * ( sin th)) + (1 - ( - ( - ((( sin th) * ( sin th)) + (( cos th) * ( cos th))))))) by SIN_COS: 29

      .= (1 - (( cos th) * ( cos th)));

      hence thesis;

    end;

    theorem :: SIN_COS4:5



     Th5: (( cos th) * ( cos th)) = (1 - (( sin th) * ( sin th)))

    proof

      (( cos th) * ( cos th)) = ((( cos th) * ( cos th)) + (1 - 1))

      .= ((( cos th) * ( cos th)) + (1 - ( - ( - ((( sin th) * ( sin th)) + (( cos th) * ( cos th))))))) by SIN_COS: 29

      .= (1 - (( sin th) * ( sin th)));

      hence thesis;

    end;

    theorem :: SIN_COS4:6



     Th6: ( cos th) <> 0 implies ( sin th) = (( cos th) * ( tan th))

    proof

      assume ( cos th) <> 0 ;



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

      .= (( cos th) * ( tan th)) by XCMPLX_1: 75;

      hence thesis;

    end;

    theorem :: SIN_COS4:7

    ( cos th1) <> 0 & ( cos th2) <> 0 implies ( tan (th1 + th2)) = ((( tan th1) + ( tan th2)) / (1 - (( tan th1) * ( tan th2))))

    proof

      assume that

       A1: ( cos th1) <> 0 and

       A2: ( cos th2) <> 0 ;

      ( tan (th1 + th2)) = ((( sin (th1 + th2)) / (( cos th1) * ( cos th2))) / (( cos (th1 + th2)) / (( cos th1) * ( cos th2)))) by A1, A2, XCMPLX_1: 55

      .= ((((( sin th1) * ( cos th2)) + (( cos th1) * ( sin th2))) / (( cos th1) * ( cos th2))) / (( cos (th1 + th2)) / (( cos th1) * ( cos th2)))) by SIN_COS: 75

      .= ((((( sin th1) * ( cos th2)) + (( cos th1) * ( sin th2))) / (( cos th1) * ( cos th2))) / (((( cos th1) * ( cos th2)) - (( sin th1) * ( sin th2))) / (( cos th1) * ( cos th2)))) by SIN_COS: 75

      .= ((((( sin th1) * ( cos th2)) / (( cos th1) * ( cos th2))) + ((( cos th1) * ( sin th2)) / (( cos th1) * ( cos th2)))) / (((( cos th1) * ( cos th2)) - (( sin th1) * ( sin th2))) / (( cos th1) * ( cos th2)))) by XCMPLX_1: 62

      .= ((((( sin th1) * ( cos th2)) / (( cos th1) * ( cos th2))) + ((( cos th1) * ( sin th2)) / (( cos th1) * ( cos th2)))) / (((( cos th1) * ( cos th2)) / (( cos th1) * ( cos th2))) - ((( sin th1) * ( sin th2)) / (( cos th1) * ( cos th2))))) by XCMPLX_1: 120

      .= ((((( sin th1) / ( cos th1)) * (( cos th2) / ( cos th2))) + ((( cos th1) * ( sin th2)) / (( cos th1) * ( cos th2)))) / (((( cos th1) * ( cos th2)) / (( cos th1) * ( cos th2))) - ((( sin th1) * ( sin th2)) / (( cos th1) * ( cos th2))))) by XCMPLX_1: 76

      .= ((((( sin th1) / ( cos th1)) * (( cos th2) / ( cos th2))) + ((( sin th2) / ( cos th2)) * (( cos th1) / ( cos th1)))) / (((( cos th1) * ( cos th2)) / (( cos th1) * ( cos th2))) - ((( sin th1) * ( sin th2)) / (( cos th1) * ( cos th2))))) by XCMPLX_1: 76

      .= ((((( sin th1) / ( cos th1)) * (( cos th2) / ( cos th2))) + ((( sin th2) / ( cos th2)) * (( cos th1) / ( cos th1)))) / (((( cos th1) / ( cos th1)) * (( cos th2) / ( cos th2))) - ((( sin th1) * ( sin th2)) / (( cos th1) * ( cos th2))))) by XCMPLX_1: 76

      .= ((((( sin th1) / ( cos th1)) * (( cos th2) / ( cos th2))) + ((( sin th2) / ( cos th2)) * (( cos th1) / ( cos th1)))) / (((( cos th1) / ( cos th1)) * (( cos th2) / ( cos th2))) - ((( sin th1) / ( cos th1)) * (( sin th2) / ( cos th2))))) by XCMPLX_1: 76

      .= (((( sin th1) / ( cos th1)) + ((( sin th2) / ( cos th2)) * (( cos th1) / ( cos th1)))) / (((( cos th1) / ( cos th1)) * (( cos th2) / ( cos th2))) - ((( sin th1) / ( cos th1)) * (( sin th2) / ( cos th2))))) by A2, XCMPLX_1: 88

      .= (((( sin th1) / ( cos th1)) + (( sin th2) / ( cos th2))) / (((( cos th1) / ( cos th1)) * (( cos th2) / ( cos th2))) - ((( sin th1) / ( cos th1)) * (( sin th2) / ( cos th2))))) by A1, XCMPLX_1: 88

      .= (((( sin th1) / ( cos th1)) + (( sin th2) / ( cos th2))) / ((( cos th1) / ( cos th1)) - ((( sin th1) / ( cos th1)) * (( sin th2) / ( cos th2))))) by A2, XCMPLX_1: 88

      .= ((( tan th1) + ( tan th2)) / (1 - (( tan th1) * ( tan th2)))) by A1, XCMPLX_1: 60;

      hence thesis;

    end;

    theorem :: SIN_COS4:8

    ( cos th1) <> 0 & ( cos th2) <> 0 implies ( tan (th1 - th2)) = ((( tan th1) - ( tan th2)) / (1 + (( tan th1) * ( tan th2))))

    proof

      assume that

       A1: ( cos th1) <> 0 and

       A2: ( cos th2) <> 0 ;

      ( tan (th1 - th2)) = ((( sin (th1 + ( - th2))) / (( cos th1) * ( cos th2))) / (( cos (th1 + ( - th2))) / (( cos th1) * ( cos th2)))) by A1, A2, XCMPLX_1: 55

      .= ((((( sin th1) * ( cos ( - th2))) + (( cos th1) * ( sin ( - th2)))) / (( cos th1) * ( cos th2))) / (( cos (th1 + ( - th2))) / (( cos th1) * ( cos th2)))) by SIN_COS: 75

      .= ((((( sin th1) * ( cos th2)) + (( cos th1) * ( sin ( - th2)))) / (( cos th1) * ( cos th2))) / (( cos (th1 + ( - th2))) / (( cos th1) * ( cos th2)))) by SIN_COS: 31

      .= ((((( sin th1) * ( cos th2)) + (( cos th1) * ( - ( sin th2)))) / (( cos th1) * ( cos th2))) / (( cos (th1 + ( - th2))) / (( cos th1) * ( cos th2)))) by SIN_COS: 31

      .= ((((( sin th1) * ( cos th2)) - (( cos th1) * ( sin th2))) / (( cos th1) * ( cos th2))) / (((( cos th1) * ( cos ( - th2))) - (( sin th1) * ( sin ( - th2)))) / (( cos th1) * ( cos th2)))) by SIN_COS: 75

      .= ((((( sin th1) * ( cos th2)) - (( cos th1) * ( sin th2))) / (( cos th1) * ( cos th2))) / (((( cos th1) * ( cos th2)) - (( sin th1) * ( sin ( - th2)))) / (( cos th1) * ( cos th2)))) by SIN_COS: 31

      .= ((((( sin th1) * ( cos th2)) - (( cos th1) * ( sin th2))) / (( cos th1) * ( cos th2))) / (((( cos th1) * ( cos th2)) - (( sin th1) * ( - ( sin th2)))) / (( cos th1) * ( cos th2)))) by SIN_COS: 31

      .= ((((( sin th1) * ( cos th2)) / (( cos th1) * ( cos th2))) - ((( cos th1) * ( sin th2)) / (( cos th1) * ( cos th2)))) / (((( cos th1) * ( cos th2)) + (( sin th1) * ( sin th2))) / (( cos th1) * ( cos th2)))) by XCMPLX_1: 120

      .= ((((( sin th1) * ( cos th2)) / (( cos th1) * ( cos th2))) - ((( cos th1) * ( sin th2)) / (( cos th1) * ( cos th2)))) / (((( cos th1) * ( cos th2)) / (( cos th1) * ( cos th2))) + ((( sin th1) * ( sin th2)) / (( cos th1) * ( cos th2))))) by XCMPLX_1: 62

      .= ((((( sin th1) / ( cos th1)) * (( cos th2) / ( cos th2))) - ((( cos th1) * ( sin th2)) / (( cos th1) * ( cos th2)))) / (((( cos th1) * ( cos th2)) / (( cos th1) * ( cos th2))) + ((( sin th1) * ( sin th2)) / (( cos th1) * ( cos th2))))) by XCMPLX_1: 76

      .= ((((( sin th1) / ( cos th1)) * (( cos th2) / ( cos th2))) - ((( sin th2) / ( cos th2)) * (( cos th1) / ( cos th1)))) / (((( cos th1) * ( cos th2)) / (( cos th1) * ( cos th2))) + ((( sin th1) * ( sin th2)) / (( cos th1) * ( cos th2))))) by XCMPLX_1: 76

      .= ((((( sin th1) / ( cos th1)) * (( cos th2) / ( cos th2))) - ((( sin th2) / ( cos th2)) * (( cos th1) / ( cos th1)))) / (((( cos th1) / ( cos th1)) * (( cos th2) / ( cos th2))) + ((( sin th1) * ( sin th2)) / (( cos th1) * ( cos th2))))) by XCMPLX_1: 76

      .= ((((( sin th1) / ( cos th1)) * (( cos th2) / ( cos th2))) - ((( sin th2) / ( cos th2)) * (( cos th1) / ( cos th1)))) / (((( cos th1) / ( cos th1)) * (( cos th2) / ( cos th2))) + ((( sin th1) / ( cos th1)) * (( sin th2) / ( cos th2))))) by XCMPLX_1: 76

      .= (((( sin th1) / ( cos th1)) - ((( sin th2) / ( cos th2)) * (( cos th1) / ( cos th1)))) / (((( cos th1) / ( cos th1)) * (( cos th2) / ( cos th2))) + ((( sin th1) / ( cos th1)) * (( sin th2) / ( cos th2))))) by A2, XCMPLX_1: 88

      .= (((( sin th1) / ( cos th1)) - (( sin th2) / ( cos th2))) / (((( cos th1) / ( cos th1)) * (( cos th2) / ( cos th2))) + ((( sin th1) / ( cos th1)) * (( sin th2) / ( cos th2))))) by A1, XCMPLX_1: 88

      .= (((( sin th1) / ( cos th1)) - (( sin th2) / ( cos th2))) / ((( cos th1) / ( cos th1)) + ((( sin th1) / ( cos th1)) * (( sin th2) / ( cos th2))))) by A2, XCMPLX_1: 88

      .= ((( tan th1) - ( tan th2)) / (1 + (( tan th1) * ( tan th2)))) by A1, XCMPLX_1: 60;

      hence thesis;

    end;

    theorem :: SIN_COS4:9

    ( sin th1) <> 0 & ( sin th2) <> 0 implies ( cot (th1 + th2)) = (((( cot th1) * ( cot th2)) - 1) / (( cot th2) + ( cot th1)))

    proof

      assume that

       A1: ( sin th1) <> 0 and

       A2: ( sin th2) <> 0 ;

      ( cot (th1 + th2)) = ((( cos (th1 + th2)) / (( sin th1) * ( sin th2))) / (( sin (th1 + th2)) / (( sin th1) * ( sin th2)))) by A1, A2, XCMPLX_1: 55

      .= ((((( cos th1) * ( cos th2)) - (( sin th1) * ( sin th2))) / (( sin th1) * ( sin th2))) / (( sin (th1 + th2)) / (( sin th1) * ( sin th2)))) by SIN_COS: 75

      .= ((((( cos th1) * ( cos th2)) - (( sin th1) * ( sin th2))) / (( sin th1) * ( sin th2))) / (((( sin th1) * ( cos th2)) + (( cos th1) * ( sin th2))) / (( sin th1) * ( sin th2)))) by SIN_COS: 75

      .= ((((( cos th1) * ( cos th2)) / (( sin th1) * ( sin th2))) - ((( sin th1) * ( sin th2)) / (( sin th1) * ( sin th2)))) / (((( sin th1) * ( cos th2)) + (( cos th1) * ( sin th2))) / (( sin th1) * ( sin th2)))) by XCMPLX_1: 120

      .= ((((( cos th1) * ( cos th2)) / (( sin th1) * ( sin th2))) - ((( sin th1) * ( sin th2)) / (( sin th1) * ( sin th2)))) / (((( sin th1) * ( cos th2)) / (( sin th1) * ( sin th2))) + ((( cos th1) * ( sin th2)) / (( sin th1) * ( sin th2))))) by XCMPLX_1: 62

      .= ((((( cos th1) / ( sin th1)) * (( cos th2) / ( sin th2))) - ((( sin th1) * ( sin th2)) / (( sin th1) * ( sin th2)))) / (((( sin th1) * ( cos th2)) / (( sin th1) * ( sin th2))) + ((( cos th1) * ( sin th2)) / (( sin th1) * ( sin th2))))) by XCMPLX_1: 76

      .= ((((( cos th1) / ( sin th1)) * (( cos th2) / ( sin th2))) - ((( sin th1) / ( sin th1)) * (( sin th2) / ( sin th2)))) / (((( sin th1) * ( cos th2)) / (( sin th1) * ( sin th2))) + ((( cos th1) * ( sin th2)) / (( sin th1) * ( sin th2))))) by XCMPLX_1: 76

      .= ((((( cos th1) / ( sin th1)) * (( cos th2) / ( sin th2))) - ((( sin th1) / ( sin th1)) * (( sin th2) / ( sin th2)))) / (((( sin th1) / ( sin th1)) * (( cos th2) / ( sin th2))) + ((( cos th1) * ( sin th2)) / (( sin th1) * ( sin th2))))) by XCMPLX_1: 76

      .= ((((( cos th1) / ( sin th1)) * (( cos th2) / ( sin th2))) - ((( sin th1) / ( sin th1)) * (( sin th2) / ( sin th2)))) / (((( sin th1) / ( sin th1)) * (( cos th2) / ( sin th2))) + ((( cos th1) / ( sin th1)) * (( sin th2) / ( sin th2))))) by XCMPLX_1: 76

      .= ((((( cos th1) / ( sin th1)) * (( cos th2) / ( sin th2))) - (( sin th1) / ( sin th1))) / (((( sin th1) / ( sin th1)) * (( cos th2) / ( sin th2))) + ((( cos th1) / ( sin th1)) * (( sin th2) / ( sin th2))))) by A2, XCMPLX_1: 88

      .= ((((( cos th1) / ( sin th1)) * (( cos th2) / ( sin th2))) - 1) / (((( sin th1) / ( sin th1)) * (( cos th2) / ( sin th2))) + ((( cos th1) / ( sin th1)) * (( sin th2) / ( sin th2))))) by A1, XCMPLX_1: 60

      .= ((((( cos th1) / ( sin th1)) * (( cos th2) / ( sin th2))) - 1) / ((( cos th2) / ( sin th2)) + ((( cos th1) / ( sin th1)) * (( sin th2) / ( sin th2))))) by A1, XCMPLX_1: 88

      .= (((( cot th1) * ( cot th2)) - 1) / (( cot th2) + ( cot th1))) by A2, XCMPLX_1: 88;

      hence thesis;

    end;

    theorem :: SIN_COS4:10

    ( sin th1) <> 0 & ( sin th2) <> 0 implies ( cot (th1 - th2)) = (((( cot th1) * ( cot th2)) + 1) / (( cot th2) - ( cot th1)))

    proof

      assume that

       A1: ( sin th1) <> 0 and

       A2: ( sin th2) <> 0 ;

      ( cot (th1 - th2)) = ((( cos (th1 - th2)) / (( sin th1) * ( sin th2))) / (( sin (th1 - th2)) / (( sin th1) * ( sin th2)))) by A1, A2, XCMPLX_1: 55

      .= ((((( cos th1) * ( cos th2)) + (( sin th1) * ( sin th2))) / (( sin th1) * ( sin th2))) / (( sin (th1 - th2)) / (( sin th1) * ( sin th2)))) by SIN_COS: 83

      .= ((((( cos th1) * ( cos th2)) + (( sin th1) * ( sin th2))) / (( sin th1) * ( sin th2))) / (((( sin th1) * ( cos th2)) - (( cos th1) * ( sin th2))) / (( sin th1) * ( sin th2)))) by SIN_COS: 82

      .= ((((( cos th1) * ( cos th2)) / (( sin th1) * ( sin th2))) + ((( sin th1) * ( sin th2)) / (( sin th1) * ( sin th2)))) / (((( sin th1) * ( cos th2)) - (( cos th1) * ( sin th2))) / (( sin th1) * ( sin th2)))) by XCMPLX_1: 62

      .= ((((( cos th1) * ( cos th2)) / (( sin th1) * ( sin th2))) + ((( sin th1) * ( sin th2)) / (( sin th1) * ( sin th2)))) / (((( sin th1) * ( cos th2)) / (( sin th1) * ( sin th2))) - ((( cos th1) * ( sin th2)) / (( sin th1) * ( sin th2))))) by XCMPLX_1: 120

      .= ((((( cos th1) / ( sin th1)) * (( cos th2) / ( sin th2))) + ((( sin th1) * ( sin th2)) / (( sin th1) * ( sin th2)))) / (((( sin th1) * ( cos th2)) / (( sin th1) * ( sin th2))) - ((( cos th1) * ( sin th2)) / (( sin th1) * ( sin th2))))) by XCMPLX_1: 76

      .= ((((( cos th1) / ( sin th1)) * (( cos th2) / ( sin th2))) + ((( sin th1) / ( sin th1)) * (( sin th2) / ( sin th2)))) / (((( sin th1) * ( cos th2)) / (( sin th1) * ( sin th2))) - ((( cos th1) * ( sin th2)) / (( sin th1) * ( sin th2))))) by XCMPLX_1: 76

      .= ((((( cos th1) / ( sin th1)) * (( cos th2) / ( sin th2))) + ((( sin th1) / ( sin th1)) * (( sin th2) / ( sin th2)))) / (((( sin th1) / ( sin th1)) * (( cos th2) / ( sin th2))) - ((( cos th1) * ( sin th2)) / (( sin th1) * ( sin th2))))) by XCMPLX_1: 76

      .= ((((( cos th1) / ( sin th1)) * (( cos th2) / ( sin th2))) + ((( sin th1) / ( sin th1)) * (( sin th2) / ( sin th2)))) / (((( sin th1) / ( sin th1)) * (( cos th2) / ( sin th2))) - ((( cos th1) / ( sin th1)) * (( sin th2) / ( sin th2))))) by XCMPLX_1: 76

      .= ((((( cos th1) / ( sin th1)) * (( cos th2) / ( sin th2))) + (( sin th1) / ( sin th1))) / (((( sin th1) / ( sin th1)) * (( cos th2) / ( sin th2))) - ((( cos th1) / ( sin th1)) * (( sin th2) / ( sin th2))))) by A2, XCMPLX_1: 88

      .= ((((( cos th1) / ( sin th1)) * (( cos th2) / ( sin th2))) + 1) / (((( sin th1) / ( sin th1)) * (( cos th2) / ( sin th2))) - ((( cos th1) / ( sin th1)) * (( sin th2) / ( sin th2))))) by A1, XCMPLX_1: 60

      .= ((((( cos th1) / ( sin th1)) * (( cos th2) / ( sin th2))) + 1) / ((( cos th2) / ( sin th2)) - ((( cos th1) / ( sin th1)) * (( sin th2) / ( sin th2))))) by A1, XCMPLX_1: 88

      .= (((( cot th1) * ( cot th2)) + 1) / (( cot th2) - ( cot th1))) by A2, XCMPLX_1: 88;

      hence thesis;

    end;

    theorem :: SIN_COS4:11



     Th11: ( cos th1) <> 0 & ( cos th2) <> 0 & ( cos th3) <> 0 implies ( sin ((th1 + th2) + th3)) = (((( cos th1) * ( cos th2)) * ( cos th3)) * (((( tan th1) + ( tan th2)) + ( tan th3)) - ((( tan th1) * ( tan th2)) * ( tan th3))))

    proof

      assume that

       A1: ( cos th1) <> 0 and

       A2: ( cos th2) <> 0 and

       A3: ( cos th3) <> 0 ;

      ( sin ((th1 + th2) + th3)) = ( sin (th1 + (th2 + th3)))

      .= ((( sin th1) * ( cos (th2 + th3))) + (( cos th1) * ( sin (th2 + th3)))) by SIN_COS: 75

      .= ((( sin th1) * ((( cos th2) * ( cos th3)) - (( sin th2) * ( sin th3)))) + (( cos th1) * ( sin (th2 + th3)))) by SIN_COS: 75

      .= (((( sin th1) * (( cos th2) * ( cos th3))) - (( sin th1) * (( sin th2) * ( sin th3)))) + (( cos th1) * ((( sin th2) * ( cos th3)) + (( cos th2) * ( sin th3))))) by SIN_COS: 75

      .= ((((( cos th1) * ( tan th1)) * (( cos th2) * ( cos th3))) - (( sin th1) * (( sin th2) * ( sin th3)))) + ((( cos th1) * (( sin th2) * ( cos th3))) + (( cos th1) * (( cos th2) * ( sin th3))))) by A1, Th6

      .= ((((( cos th1) * ( tan th1)) * (( cos th2) * ( cos th3))) - ((( cos th1) * ( tan th1)) * (( sin th2) * ( sin th3)))) + ((( cos th1) * (( sin th2) * ( cos th3))) + (( cos th1) * (( cos th2) * ( sin th3))))) by A1, Th6

      .= ((((( cos th1) * ( tan th1)) * (( cos th2) * ( cos th3))) - ((( cos th1) * ( tan th1)) * ((( cos th2) * ( tan th2)) * ( sin th3)))) + ((( cos th1) * (( sin th2) * ( cos th3))) + (( cos th1) * (( cos th2) * ( sin th3))))) by A2, Th6

      .= ((((( cos th1) * ( tan th1)) * (( cos th2) * ( cos th3))) - ((( cos th1) * ( tan th1)) * ((( cos th2) * ( tan th2)) * (( cos th3) * ( tan th3))))) + ((( cos th1) * (( sin th2) * ( cos th3))) + (( cos th1) * (( cos th2) * ( sin th3))))) by A3, Th6

      .= ((((( cos th1) * ( tan th1)) * (( cos th2) * ( cos th3))) - ((( cos th1) * ( tan th1)) * ((( cos th2) * ( tan th2)) * (( cos th3) * ( tan th3))))) + ((( cos th1) * ((( cos th2) * ( tan th2)) * ( cos th3))) + (( cos th1) * (( cos th2) * ( sin th3))))) by A2, Th6

      .= ((((( cos th1) * ( cos th2)) * (( cos th3) * ( tan th1))) - (((( cos th1) * ( cos th2)) * (( tan th1) * ( tan th2))) * (( cos th3) * ( tan th3)))) + ((( cos th1) * ((( cos th2) * ( tan th2)) * ( cos th3))) + (( cos th1) * (( cos th2) * (( cos th3) * ( tan th3)))))) by A3, Th6

      .= (((( cos th1) * ( cos th2)) * ( cos th3)) * (((( tan th1) + ( tan th2)) + ( tan th3)) - ((( tan th1) * ( tan th2)) * ( tan th3))));

      hence thesis;

    end;

    theorem :: SIN_COS4:12



     Th12: ( cos th1) <> 0 & ( cos th2) <> 0 & ( cos th3) <> 0 implies ( cos ((th1 + th2) + th3)) = (((( cos th1) * ( cos th2)) * ( cos th3)) * (((1 - (( tan th2) * ( tan th3))) - (( tan th3) * ( tan th1))) - (( tan th1) * ( tan th2))))

    proof

      assume that

       A1: ( cos th1) <> 0 and

       A2: ( cos th2) <> 0 and

       A3: ( cos th3) <> 0 ;

      ( cos ((th1 + th2) + th3)) = ( cos (th1 + (th2 + th3)))

      .= ((( cos th1) * ( cos (th2 + th3))) - (( sin th1) * ( sin (th2 + th3)))) by SIN_COS: 75

      .= ((( cos th1) * ((( cos th2) * ( cos th3)) - (( sin th2) * ( sin th3)))) - (( sin th1) * ( sin (th2 + th3)))) by SIN_COS: 75

      .= (((( cos th1) * (( cos th2) * ( cos th3))) - (( cos th1) * (( sin th2) * ( sin th3)))) - (( sin th1) * ((( sin th2) * ( cos th3)) + (( cos th2) * ( sin th3))))) by SIN_COS: 75

      .= (((( cos th1) * (( cos th2) * ( cos th3))) - (( cos th1) * ((( cos th2) * ( tan th2)) * ( sin th3)))) - (( sin th1) * ((( sin th2) * ( cos th3)) + (( cos th2) * ( sin th3))))) by A2, Th6

      .= (((( cos th1) * (( cos th2) * ( cos th3))) - (( cos th1) * ((( cos th2) * ( tan th2)) * (( cos th3) * ( tan th3))))) - (( sin th1) * ((( sin th2) * ( cos th3)) + (( cos th2) * ( sin th3))))) by A3, Th6

      .= (((( cos th1) * (( cos th2) * ( cos th3))) - (( cos th1) * ((( cos th2) * ( tan th2)) * (( cos th3) * ( tan th3))))) - ((( cos th1) * ( tan th1)) * ((( sin th2) * ( cos th3)) + (( cos th2) * ( sin th3))))) by A1, Th6

      .= (((( cos th1) * (( cos th2) * ( cos th3))) - (( cos th1) * ((( cos th2) * ( tan th2)) * (( cos th3) * ( tan th3))))) - ((( cos th1) * ( tan th1)) * (((( cos th2) * ( tan th2)) * ( cos th3)) + (( cos th2) * ( sin th3))))) by A2, Th6

      .= ((((( cos th1) * ( cos th2)) * ( cos th3)) - (((( cos th1) * ( cos th2)) * ( cos th3)) * (( tan th2) * ( tan th3)))) - ((( cos th1) * ( tan th1)) * (((( cos th2) * ( cos th3)) * ( tan th2)) + (( cos th2) * (( cos th3) * ( tan th3)))))) by A3, Th6

      .= (((( cos th1) * ( cos th2)) * ( cos th3)) * (((1 - (( tan th2) * ( tan th3))) - (( tan th3) * ( tan th1))) - (( tan th1) * ( tan th2))));

      hence thesis;

    end;

    theorem :: SIN_COS4:13

    ( cos th1) <> 0 & ( cos th2) <> 0 & ( cos th3) <> 0 implies ( tan ((th1 + th2) + th3)) = ((((( tan th1) + ( tan th2)) + ( tan th3)) - ((( tan th1) * ( tan th2)) * ( tan th3))) / (((1 - (( tan th2) * ( tan th3))) - (( tan th3) * ( tan th1))) - (( tan th1) * ( tan th2))))

    proof

      assume that

       A1: ( cos th1) <> 0 & ( cos th2) <> 0 and

       A2: ( cos th3) <> 0 ;



       A3: (( cos th1) * ( cos th2)) <> 0 by A1;

      ( tan ((th1 + th2) + th3)) = ((((( cos th1) * ( cos th2)) * ( cos th3)) * (((( tan th1) + ( tan th2)) + ( tan th3)) - ((( tan th1) * ( tan th2)) * ( tan th3)))) / ( cos ((th1 + th2) + th3))) by A1, A2, Th11

      .= ((((( cos th1) * ( cos th2)) * ( cos th3)) * (((( tan th1) + ( tan th2)) + ( tan th3)) - ((( tan th1) * ( tan th2)) * ( tan th3)))) / (((( cos th1) * ( cos th2)) * ( cos th3)) * (((1 - (( tan th2) * ( tan th3))) - (( tan th3) * ( tan th1))) - (( tan th1) * ( tan th2))))) by A1, A2, Th12

      .= ((((( cos th1) * ( cos th2)) * ( cos th3)) / ((( cos th1) * ( cos th2)) * ( cos th3))) / ((((1 - (( tan th2) * ( tan th3))) - (( tan th3) * ( tan th1))) - (( tan th1) * ( tan th2))) / (((( tan th1) + ( tan th2)) + ( tan th3)) - ((( tan th1) * ( tan th2)) * ( tan th3))))) by XCMPLX_1: 84

      .= (1 / ((((1 - (( tan th2) * ( tan th3))) - (( tan th3) * ( tan th1))) - (( tan th1) * ( tan th2))) / (((( tan th1) + ( tan th2)) + ( tan th3)) - ((( tan th1) * ( tan th2)) * ( tan th3))))) by A2, A3, XCMPLX_1: 60

      .= ((((( tan th1) + ( tan th2)) + ( tan th3)) - ((( tan th1) * ( tan th2)) * ( tan th3))) / (((1 - (( tan th2) * ( tan th3))) - (( tan th3) * ( tan th1))) - (( tan th1) * ( tan th2)))) by XCMPLX_1: 57;

      hence thesis;

    end;

    theorem :: SIN_COS4:14

    ( sin th1) <> 0 & ( sin th2) <> 0 & ( sin th3) <> 0 implies ( cot ((th1 + th2) + th3)) = ((((((( cot th1) * ( cot th2)) * ( cot th3)) - ( cot th1)) - ( cot th2)) - ( cot th3)) / ((((( cot th2) * ( cot th3)) + (( cot th3) * ( cot th1))) + (( cot th1) * ( cot th2))) - 1))

    proof

      assume that

       A1: ( sin th1) <> 0 and

       A2: ( sin th2) <> 0 and

       A3: ( sin th3) <> 0 ;



       A4: (( sin th1) * ( sin th2)) <> 0 by A1, A2;

      ( cot ((th1 + th2) + th3)) = (((( cos (th1 + th2)) * ( cos th3)) - (( sin (th1 + th2)) * ( sin th3))) / ( sin ((th1 + th2) + th3))) by SIN_COS: 75

      .= (((((( cos th1) * ( cos th2)) - (( sin th1) * ( sin th2))) * ( cos th3)) - (( sin (th1 + th2)) * ( sin th3))) / ( sin ((th1 + th2) + th3))) by SIN_COS: 75

      .= (((( cos th3) * ((( cos th1) * ( cos th2)) - (( sin th1) * ( sin th2)))) - (( sin th3) * ((( sin th1) * ( cos th2)) + (( cos th1) * ( sin th2))))) / ( sin ((th1 + th2) + th3))) by SIN_COS: 75

      .= ((((( cos th3) * ((( cos th1) * ( cos th2)) - (( sin th1) * ( sin th2)))) - (( sin th3) * ((( sin th1) * ( cos th2)) + (( cos th1) * ( sin th2))))) / ((( sin th1) * ( sin th2)) * ( sin th3))) / (( sin ((th1 + th2) + th3)) / ((( sin th1) * ( sin th2)) * ( sin th3)))) by A3, A4, XCMPLX_1: 55

      .= ((((( cos th3) * ((( cos th1) * ( cos th2)) - (( sin th1) * ( sin th2)))) / (( sin th3) * (( sin th1) * ( sin th2)))) - ((( sin th3) * ((( sin th1) * ( cos th2)) + (( cos th1) * ( sin th2)))) / (( sin th3) * (( sin th1) * ( sin th2))))) / (( sin ((th1 + th2) + th3)) / ((( sin th1) * ( sin th2)) * ( sin th3)))) by XCMPLX_1: 120

      .= (((( cot th3) * (((( cos th1) * ( cos th2)) - (( sin th1) * ( sin th2))) / (( sin th1) * ( sin th2)))) - ((( sin th3) * ((( sin th1) * ( cos th2)) + (( cos th1) * ( sin th2)))) / (( sin th3) * (( sin th1) * ( sin th2))))) / (( sin ((th1 + th2) + th3)) / ((( sin th1) * ( sin th2)) * ( sin th3)))) by XCMPLX_1: 76

      .= (((( cot th3) * (((( cos th1) * ( cos th2)) / (( sin th1) * ( sin th2))) - ((( sin th1) * ( sin th2)) / (( sin th1) * ( sin th2))))) - ((( sin th3) * ((( sin th1) * ( cos th2)) + (( cos th1) * ( sin th2)))) / (( sin th3) * (( sin th1) * ( sin th2))))) / (( sin ((th1 + th2) + th3)) / ((( sin th1) * ( sin th2)) * ( sin th3)))) by XCMPLX_1: 120

      .= (((( cot th3) * ((( cot th1) * (( cos th2) / ( sin th2))) - ((( sin th1) * ( sin th2)) / (( sin th1) * ( sin th2))))) - ((( sin th3) * ((( sin th1) * ( cos th2)) + (( cos th1) * ( sin th2)))) / (( sin th3) * (( sin th1) * ( sin th2))))) / (( sin ((th1 + th2) + th3)) / ((( sin th1) * ( sin th2)) * ( sin th3)))) by XCMPLX_1: 76

      .= (((( cot th3) * ((( cot th1) * ( cot th2)) - 1)) - ((((( sin th1) * ( cos th2)) + (( cos th1) * ( sin th2))) * ( sin th3)) / ((( sin th1) * ( sin th2)) * ( sin th3)))) / (( sin ((th1 + th2) + th3)) / ((( sin th1) * ( sin th2)) * ( sin th3)))) by A1, A2, XCMPLX_1: 60

      .= (((( cot th3) * ((( cot th1) * ( cot th2)) - 1)) - (((( sin th1) * ( cos th2)) + (( cos th1) * ( sin th2))) / (( sin th1) * ( sin th2)))) / (( sin ((th1 + th2) + th3)) / ((( sin th1) * ( sin th2)) * ( sin th3)))) by A3, XCMPLX_1: 91

      .= (((( cot th3) * ((( cot th1) * ( cot th2)) - 1)) - (((( sin th1) * ( cos th2)) / (( sin th1) * ( sin th2))) + ((( cos th1) * ( sin th2)) / (( sin th1) * ( sin th2))))) / (( sin ((th1 + th2) + th3)) / ((( sin th1) * ( sin th2)) * ( sin th3)))) by XCMPLX_1: 62

      .= (((( cot th3) * ((( cot th1) * ( cot th2)) - 1)) - ((( cos th2) / ( sin th2)) + ((( cos th1) * ( sin th2)) / (( sin th1) * ( sin th2))))) / (( sin ((th1 + th2) + th3)) / ((( sin th1) * ( sin th2)) * ( sin th3)))) by A1, XCMPLX_1: 91

      .= (((( cot th3) * ((( cot th1) * ( cot th2)) - 1)) - (( cot th2) + (( cos th1) / ( sin th1)))) / (( sin ((th1 + th2) + th3)) / ((( sin th1) * ( sin th2)) * ( sin th3)))) by A2, XCMPLX_1: 91

      .= ((((((( cot th1) * ( cot th2)) * ( cot th3)) - ( cot th1)) - ( cot th2)) - ( cot th3)) / (((( sin (th1 + th2)) * ( cos th3)) + (( cos (th1 + th2)) * ( sin th3))) / ((( sin th1) * ( sin th2)) * ( sin th3)))) by SIN_COS: 75

      .= ((((((( cot th1) * ( cot th2)) * ( cot th3)) - ( cot th1)) - ( cot th2)) - ( cot th3)) / (((( sin (th1 + th2)) * ( cos th3)) / ((( sin th1) * ( sin th2)) * ( sin th3))) + ((( cos (th1 + th2)) * ( sin th3)) / ((( sin th1) * ( sin th2)) * ( sin th3))))) by XCMPLX_1: 62

      .= ((((((( cot th1) * ( cot th2)) * ( cot th3)) - ( cot th1)) - ( cot th2)) - ( cot th3)) / (((( sin (th1 + th2)) * ( cos th3)) / ((( sin th1) * ( sin th2)) * ( sin th3))) + (( cos (th1 + th2)) / (( sin th1) * ( sin th2))))) by A3, XCMPLX_1: 91

      .= ((((((( cot th1) * ( cot th2)) * ( cot th3)) - ( cot th1)) - ( cot th2)) - ( cot th3)) / ((( cot th3) * (( sin (th1 + th2)) / (( sin th1) * ( sin th2)))) + (( cos (th1 + th2)) / (( sin th1) * ( sin th2))))) by XCMPLX_1: 76

      .= ((((((( cot th1) * ( cot th2)) * ( cot th3)) - ( cot th1)) - ( cot th2)) - ( cot th3)) / ((( cot th3) * (((( sin th1) * ( cos th2)) + (( cos th1) * ( sin th2))) / (( sin th1) * ( sin th2)))) + (( cos (th1 + th2)) / (( sin th1) * ( sin th2))))) by SIN_COS: 75

      .= ((((((( cot th1) * ( cot th2)) * ( cot th3)) - ( cot th1)) - ( cot th2)) - ( cot th3)) / ((( cot th3) * (((( sin th1) * ( cos th2)) / (( sin th1) * ( sin th2))) + ((( cos th1) * ( sin th2)) / (( sin th1) * ( sin th2))))) + (( cos (th1 + th2)) / (( sin th1) * ( sin th2))))) by XCMPLX_1: 62

      .= ((((((( cot th1) * ( cot th2)) * ( cot th3)) - ( cot th1)) - ( cot th2)) - ( cot th3)) / ((( cot th3) * ((( cos th2) / ( sin th2)) + ((( cos th1) * ( sin th2)) / (( sin th1) * ( sin th2))))) + (( cos (th1 + th2)) / (( sin th1) * ( sin th2))))) by A1, XCMPLX_1: 91

      .= ((((((( cot th1) * ( cot th2)) * ( cot th3)) - ( cot th1)) - ( cot th2)) - ( cot th3)) / ((( cot th3) * (( cot th2) + (( cos th1) / ( sin th1)))) + (( cos (th1 + th2)) / (( sin th1) * ( sin th2))))) by A2, XCMPLX_1: 91

      .= ((((((( cot th1) * ( cot th2)) * ( cot th3)) - ( cot th1)) - ( cot th2)) - ( cot th3)) / ((( cot th3) * (( cot th2) + ( cot th1))) + (((( cos th1) * ( cos th2)) - (( sin th1) * ( sin th2))) / (( sin th1) * ( sin th2))))) by SIN_COS: 75

      .= ((((((( cot th1) * ( cot th2)) * ( cot th3)) - ( cot th1)) - ( cot th2)) - ( cot th3)) / ((( cot th3) * (( cot th2) + ( cot th1))) + (((( cos th1) * ( cos th2)) / (( sin th1) * ( sin th2))) - ((( sin th1) * ( sin th2)) / (( sin th1) * ( sin th2)))))) by XCMPLX_1: 120

      .= ((((((( cot th1) * ( cot th2)) * ( cot th3)) - ( cot th1)) - ( cot th2)) - ( cot th3)) / ((( cot th3) * (( cot th2) + ( cot th1))) + (((( cos th1) * ( cos th2)) / (( sin th1) * ( sin th2))) - 1))) by A1, A2, XCMPLX_1: 60

      .= ((((((( cot th1) * ( cot th2)) * ( cot th3)) - ( cot th1)) - ( cot th2)) - ( cot th3)) / ((( cot th3) * (( cot th2) + ( cot th1))) + ((( cot th1) * (( cos th2) / ( sin th2))) - 1))) by XCMPLX_1: 76

      .= ((((((( cot th1) * ( cot th2)) * ( cot th3)) - ( cot th1)) - ( cot th2)) - ( cot th3)) / ((((( cot th2) * ( cot th3)) + (( cot th3) * ( cot th1))) + (( cot th1) * ( cot th2))) - 1));

      hence thesis;

    end;

    theorem :: SIN_COS4:15



     Th15: (( sin th1) + ( sin th2)) = (2 * (( cos ((th1 - th2) / 2)) * ( sin ((th1 + th2) / 2))))

    proof

      (( sin th1) + ( sin th2)) = (( sin ((th1 / 2) + (th1 / 2))) + ( sin ((th2 / 2) + (th2 / 2))))

      .= (((( sin (th1 / 2)) * ( cos (th1 / 2))) + (( cos (th1 / 2)) * ( sin (th1 / 2)))) + ( sin ((th2 / 2) + (th2 / 2)))) by SIN_COS: 75

      .= ((2 * (( sin (th1 / 2)) * ( cos (th1 / 2)))) + ((( sin (th2 / 2)) * ( cos (th2 / 2))) + (( sin (th2 / 2)) * ( cos (th2 / 2))))) by SIN_COS: 75

      .= (2 * (((( sin (th1 / 2)) * ( cos (th1 / 2))) * 1) + (( sin (th2 / 2)) * ( cos (th2 / 2)))))

      .= (2 * (((( sin (th1 / 2)) * ( cos (th1 / 2))) * ((( cos (th2 / 2)) * ( cos (th2 / 2))) + (( sin (th2 / 2)) * ( sin (th2 / 2))))) + ((( sin (th2 / 2)) * ( cos (th2 / 2))) * 1))) by SIN_COS: 29

      .= (2 * ((((( sin (th1 / 2)) * ( cos (th1 / 2))) * (( cos (th2 / 2)) * ( cos (th2 / 2)))) + ((( sin (th1 / 2)) * ( cos (th1 / 2))) * (( sin (th2 / 2)) * ( sin (th2 / 2))))) + ((( sin (th2 / 2)) * ( cos (th2 / 2))) * ((( cos (th1 / 2)) * ( cos (th1 / 2))) + (( sin (th1 / 2)) * ( sin (th1 / 2))))))) by SIN_COS: 29

      .= (2 * (((( sin (th1 / 2)) * ( cos (th2 / 2))) + (( cos (th1 / 2)) * ( sin (th2 / 2)))) * ((( cos (th1 / 2)) * ( cos (th2 / 2))) + (( sin (th1 / 2)) * ( sin (th2 / 2))))))

      .= (2 * (( sin ((th1 / 2) + (th2 / 2))) * ((( cos (th1 / 2)) * ( cos (th2 / 2))) + (( sin (th1 / 2)) * ( sin (th2 / 2)))))) by SIN_COS: 75

      .= (2 * (( cos ((th1 / 2) - (th2 / 2))) * ( sin ((th1 + th2) / 2)))) by SIN_COS: 83

      .= (2 * (( cos ((th1 - th2) / 2)) * ( sin ((th1 + th2) / 2))));

      hence thesis;

    end;

    theorem :: SIN_COS4:16



     Th16: (( sin th1) - ( sin th2)) = (2 * (( cos ((th1 + th2) / 2)) * ( sin ((th1 - th2) / 2))))

    proof

      (( sin th1) - ( sin th2)) = (( sin ((th1 / 2) + (th1 / 2))) - ( sin ((th2 / 2) + (th2 / 2))))

      .= (((( sin (th1 / 2)) * ( cos (th1 / 2))) + (( cos (th1 / 2)) * ( sin (th1 / 2)))) - ( sin ((th2 / 2) + (th2 / 2)))) by SIN_COS: 75

      .= ((2 * (( sin (th1 / 2)) * ( cos (th1 / 2)))) - ((( sin (th2 / 2)) * ( cos (th2 / 2))) + (( sin (th2 / 2)) * ( cos (th2 / 2))))) by SIN_COS: 75

      .= (2 * (((( sin (th1 / 2)) * ( cos (th1 / 2))) * 1) - (( sin (th2 / 2)) * ( cos (th2 / 2)))))

      .= (2 * (((( sin (th1 / 2)) * ( cos (th1 / 2))) * ((( cos (th2 / 2)) * ( cos (th2 / 2))) + (( sin (th2 / 2)) * ( sin (th2 / 2))))) - ((( sin (th2 / 2)) * ( cos (th2 / 2))) * 1))) by SIN_COS: 29

      .= (2 * ((((( sin (th1 / 2)) * ( cos (th1 / 2))) * (( cos (th2 / 2)) * ( cos (th2 / 2)))) + ((( sin (th1 / 2)) * ( cos (th1 / 2))) * (( sin (th2 / 2)) * ( sin (th2 / 2))))) - ((( sin (th2 / 2)) * ( cos (th2 / 2))) * ((( cos (th1 / 2)) * ( cos (th1 / 2))) + (( sin (th1 / 2)) * ( sin (th1 / 2))))))) by SIN_COS: 29

      .= (2 * (((( sin (th1 / 2)) * ( cos (th2 / 2))) - (( cos (th1 / 2)) * ( sin (th2 / 2)))) * ((( cos (th1 / 2)) * ( cos (th2 / 2))) + ( - (( sin (th1 / 2)) * ( sin (th2 / 2)))))))

      .= (2 * (( sin ((th1 / 2) - (th2 / 2))) * ((( cos (th1 / 2)) * ( cos (th2 / 2))) - (( sin (th1 / 2)) * ( sin (th2 / 2)))))) by SIN_COS: 82

      .= (2 * (( sin ((th1 - th2) / 2)) * ( cos ((th1 / 2) + (th2 / 2))))) by SIN_COS: 75

      .= (2 * (( cos ((th1 + th2) / 2)) * ( sin ((th1 - th2) / 2))));

      hence thesis;

    end;

    theorem :: SIN_COS4:17



     Th17: (( cos th1) + ( cos th2)) = (2 * (( cos ((th1 + th2) / 2)) * ( cos ((th1 - th2) / 2))))

    proof

      (( cos th1) + ( cos th2)) = (( cos ((th1 / 2) + (th1 / 2))) + ( cos ((th2 / 2) + (th2 / 2))))

      .= (((( cos (th1 / 2)) * ( cos (th1 / 2))) - (( sin (th1 / 2)) * ( sin (th1 / 2)))) + ( cos ((th2 / 2) + (th2 / 2)))) by SIN_COS: 75

      .= ((((( cos (th1 / 2)) * ( cos (th1 / 2))) + ( - (( sin (th1 / 2)) * ( sin (th1 / 2))))) + (1 + ( - 1))) + ((( cos (th2 / 2)) * ( cos (th2 / 2))) - (( sin (th2 / 2)) * ( sin (th2 / 2))))) by SIN_COS: 75

      .= ((((( cos (th1 / 2)) * ( cos (th1 / 2))) + ( - (( sin (th1 / 2)) * ( sin (th1 / 2))))) + 1) + (( - 1) + ((( cos (th2 / 2)) * ( cos (th2 / 2))) - (( sin (th2 / 2)) * ( sin (th2 / 2))))))

      .= ((((( cos (th1 / 2)) * ( cos (th1 / 2))) + ( - (( sin (th1 / 2)) * ( sin (th1 / 2))))) + ((( sin (th1 / 2)) * ( sin (th1 / 2))) + (( cos (th1 / 2)) * ( cos (th1 / 2))))) + (( - 1) + ((( cos (th2 / 2)) * ( cos (th2 / 2))) - (( sin (th2 / 2)) * ( sin (th2 / 2)))))) by SIN_COS: 29

      .= (((( cos (th1 / 2)) * ( cos (th1 / 2))) + (((( sin (th1 / 2)) * ( sin (th1 / 2))) - ( - ( - (( sin (th1 / 2)) * ( sin (th1 / 2)))))) + (( cos (th1 / 2)) * ( cos (th1 / 2))))) + (( - ((( sin (th2 / 2)) * ( sin (th2 / 2))) + (( cos (th2 / 2)) * ( cos (th2 / 2))))) + ((( cos (th2 / 2)) * ( cos (th2 / 2))) - (( sin (th2 / 2)) * ( sin (th2 / 2)))))) by SIN_COS: 29

      .= (2 * ((( cos (th1 / 2)) * ( cos (th1 / 2))) - ((( sin (th2 / 2)) * ( sin (th2 / 2))) * 1)))

      .= (2 * ((( cos (th1 / 2)) * ( cos (th1 / 2))) - ((( sin (th2 / 2)) * ( sin (th2 / 2))) * ((( cos (th1 / 2)) * ( cos (th1 / 2))) + (( sin (th1 / 2)) * ( sin (th1 / 2))))))) by SIN_COS: 29

      .= (2 * (((( cos (th1 / 2)) * ( cos (th1 / 2))) * (1 - ( - ( - (( sin (th2 / 2)) * ( sin (th2 / 2))))))) + ( - ((( sin (th2 / 2)) * ( sin (th2 / 2))) * (( sin (th1 / 2)) * ( sin (th1 / 2)))))))

      .= (2 * (((( cos (th1 / 2)) * ( cos (th1 / 2))) * (((( cos (th2 / 2)) * ( cos (th2 / 2))) + (( sin (th2 / 2)) * ( sin (th2 / 2)))) - ( - ( - (( sin (th2 / 2)) * ( sin (th2 / 2))))))) + ( - ((( sin (th2 / 2)) * ( sin (th2 / 2))) * (( sin (th1 / 2)) * ( sin (th1 / 2))))))) by SIN_COS: 29

      .= (2 * (((( cos (th1 / 2)) * ( cos (th2 / 2))) + (( sin (th1 / 2)) * ( sin (th2 / 2)))) * ((( cos (th1 / 2)) * ( cos (th2 / 2))) + ( - (( sin (th1 / 2)) * ( sin (th2 / 2)))))))

      .= (2 * (( cos ((th1 / 2) - (th2 / 2))) * ((( cos (th1 / 2)) * ( cos (th2 / 2))) - (( sin (th1 / 2)) * ( sin (th2 / 2)))))) by SIN_COS: 83

      .= (2 * (( cos ((th1 - th2) / 2)) * ( cos ((th1 / 2) + (th2 / 2))))) by SIN_COS: 75

      .= (2 * (( cos ((th1 + th2) / 2)) * ( cos ((th1 - th2) / 2))));

      hence thesis;

    end;

    theorem :: SIN_COS4:18



     Th18: (( cos th1) - ( cos th2)) = ( - (2 * (( sin ((th1 + th2) / 2)) * ( sin ((th1 - th2) / 2)))))

    proof

      (( cos th1) - ( cos th2)) = (( cos ((th1 / 2) + (th1 / 2))) - ( cos ((th2 / 2) + (th2 / 2))))

      .= (((( cos (th1 / 2)) * ( cos (th1 / 2))) - (( sin (th1 / 2)) * ( sin (th1 / 2)))) - ( cos ((th2 / 2) + (th2 / 2)))) by SIN_COS: 75

      .= ((((( cos (th1 / 2)) * ( cos (th1 / 2))) + ( - (( sin (th1 / 2)) * ( sin (th1 / 2))))) + (1 + ( - 1))) - ((( cos (th2 / 2)) * ( cos (th2 / 2))) - (( sin (th2 / 2)) * ( sin (th2 / 2))))) by SIN_COS: 75

      .= ((((( cos (th1 / 2)) * ( cos (th1 / 2))) + ( - (( sin (th1 / 2)) * ( sin (th1 / 2))))) + 1) + (( - 1) + (( - (( cos (th2 / 2)) * ( cos (th2 / 2)))) + (( sin (th2 / 2)) * ( sin (th2 / 2))))))

      .= ((((( cos (th1 / 2)) * ( cos (th1 / 2))) + ( - (( sin (th1 / 2)) * ( sin (th1 / 2))))) + ((( sin (th1 / 2)) * ( sin (th1 / 2))) + (( cos (th1 / 2)) * ( cos (th1 / 2))))) + (( - 1) + (( - (( cos (th2 / 2)) * ( cos (th2 / 2)))) + (( sin (th2 / 2)) * ( sin (th2 / 2)))))) by SIN_COS: 29

      .= (((( cos (th1 / 2)) * ( cos (th1 / 2))) + (((( sin (th1 / 2)) * ( sin (th1 / 2))) - ( - ( - (( sin (th1 / 2)) * ( sin (th1 / 2)))))) + (( cos (th1 / 2)) * ( cos (th1 / 2))))) + (( - ((( sin (th2 / 2)) * ( sin (th2 / 2))) + (( cos (th2 / 2)) * ( cos (th2 / 2))))) + (( - (( cos (th2 / 2)) * ( cos (th2 / 2)))) + (( sin (th2 / 2)) * ( sin (th2 / 2)))))) by SIN_COS: 29

      .= (2 * (((( cos (th1 / 2)) * ( cos (th1 / 2))) * 1) - (( cos (th2 / 2)) * ( cos (th2 / 2)))))

      .= (2 * (((( cos (th1 / 2)) * ( cos (th1 / 2))) * ((( sin (th2 / 2)) * ( sin (th2 / 2))) + (( cos (th2 / 2)) * ( cos (th2 / 2))))) - (( cos (th2 / 2)) * ( cos (th2 / 2))))) by SIN_COS: 29

      .= (2 * (((( cos (th1 / 2)) * ( cos (th1 / 2))) * (( sin (th2 / 2)) * ( sin (th2 / 2)))) + ((( cos (th2 / 2)) * ( cos (th2 / 2))) * ((( cos (th1 / 2)) * ( cos (th1 / 2))) - ( - ( - 1))))))

      .= (2 * (((( cos (th1 / 2)) * ( cos (th1 / 2))) * (( sin (th2 / 2)) * ( sin (th2 / 2)))) + ((( cos (th2 / 2)) * ( cos (th2 / 2))) * ((( cos (th1 / 2)) * ( cos (th1 / 2))) - ( - ( - ((( cos (th1 / 2)) * ( cos (th1 / 2))) + (( sin (th1 / 2)) * ( sin (th1 / 2)))))))))) by SIN_COS: 29

      .= ( - (2 * (((( sin (th1 / 2)) * ( cos (th2 / 2))) - ( - ( - (( cos (th1 / 2)) * ( sin (th2 / 2)))))) * ((( sin (th1 / 2)) * ( cos (th2 / 2))) + (( cos (th1 / 2)) * ( sin (th2 / 2)))))))

      .= ( - (2 * (( sin ((th1 / 2) + (th2 / 2))) * ((( sin (th1 / 2)) * ( cos (th2 / 2))) - (( cos (th1 / 2)) * ( sin (th2 / 2))))))) by SIN_COS: 75

      .= ( - (2 * (( sin ((th1 + th2) / 2)) * ( sin ((th1 / 2) - (th2 / 2)))))) by SIN_COS: 82

      .= ( - (2 * (( sin ((th1 + th2) / 2)) * ( sin ((th1 - th2) / 2)))));

      hence thesis;

    end;

    theorem :: SIN_COS4:19

    ( cos th1) <> 0 & ( cos th2) <> 0 implies (( tan th1) + ( tan th2)) = (( sin (th1 + th2)) / (( cos th1) * ( cos th2)))

    proof

      assume ( cos th1) <> 0 & ( cos th2) <> 0 ;



      then (( tan th1) + ( tan th2)) = (((( sin th1) * ( cos th2)) + (( sin th2) * ( cos th1))) / (( cos th1) * ( cos th2))) by XCMPLX_1: 116

      .= (( sin (th1 + th2)) / (( cos th1) * ( cos th2))) by SIN_COS: 75;

      hence thesis;

    end;

    theorem :: SIN_COS4:20

    ( cos th1) <> 0 & ( cos th2) <> 0 implies (( tan th1) - ( tan th2)) = (( sin (th1 - th2)) / (( cos th1) * ( cos th2)))

    proof

      assume ( cos th1) <> 0 & ( cos th2) <> 0 ;



      then (( tan th1) - ( tan th2)) = (((( sin th1) * ( cos th2)) - (( sin th2) * ( cos th1))) / (( cos th1) * ( cos th2))) by XCMPLX_1: 130

      .= (( sin (th1 - th2)) / (( cos th1) * ( cos th2))) by SIN_COS: 82;

      hence thesis;

    end;

    theorem :: SIN_COS4:21

    ( cos th1) <> 0 & ( sin th2) <> 0 implies (( tan th1) + ( cot th2)) = (( cos (th1 - th2)) / (( cos th1) * ( sin th2)))

    proof

      assume ( cos th1) <> 0 & ( sin th2) <> 0 ;



      then (( tan th1) + ( cot th2)) = (((( cos th1) * ( cos th2)) + (( sin th1) * ( sin th2))) / (( cos th1) * ( sin th2))) by XCMPLX_1: 116

      .= (( cos (th1 - th2)) / (( cos th1) * ( sin th2))) by SIN_COS: 83;

      hence thesis;

    end;

    theorem :: SIN_COS4:22

    ( cos th1) <> 0 & ( sin th2) <> 0 implies (( tan th1) - ( cot th2)) = ( - (( cos (th1 + th2)) / (( cos th1) * ( sin th2))))

    proof

      assume ( cos th1) <> 0 & ( sin th2) <> 0 ;



      then (( tan th1) - ( cot th2)) = (((( sin th1) * ( sin th2)) - ( - ( - (( cos th1) * ( cos th2))))) / (( cos th1) * ( sin th2))) by XCMPLX_1: 130

      .= (( - ((( cos th1) * ( cos th2)) - (( sin th1) * ( sin th2)))) / (( cos th1) * ( sin th2)))

      .= ( - (((( cos th1) * ( cos th2)) - (( sin th1) * ( sin th2))) / (( cos th1) * ( sin th2)))) by XCMPLX_1: 187

      .= ( - (( cos (th1 + th2)) / (( cos th1) * ( sin th2)))) by SIN_COS: 75;

      hence thesis;

    end;

    theorem :: SIN_COS4:23

    ( sin th1) <> 0 & ( sin th2) <> 0 implies (( cot th1) + ( cot th2)) = (( sin (th1 + th2)) / (( sin th1) * ( sin th2)))

    proof

      assume ( sin th1) <> 0 & ( sin th2) <> 0 ;



      then (( cot th1) + ( cot th2)) = (((( cos th1) * ( sin th2)) + (( cos th2) * ( sin th1))) / (( sin th1) * ( sin th2))) by XCMPLX_1: 116

      .= (( sin (th1 + th2)) / (( sin th1) * ( sin th2))) by SIN_COS: 75;

      hence thesis;

    end;

    theorem :: SIN_COS4:24

    ( sin th1) <> 0 & ( sin th2) <> 0 implies (( cot th1) - ( cot th2)) = ( - (( sin (th1 - th2)) / (( sin th1) * ( sin th2))))

    proof

      assume ( sin th1) <> 0 & ( sin th2) <> 0 ;



      then (( cot th1) - ( cot th2)) = (((( cos th1) * ( sin th2)) - ( - ( - (( cos th2) * ( sin th1))))) / (( sin th1) * ( sin th2))) by XCMPLX_1: 130

      .= (( - ((( sin th1) * ( cos th2)) - (( cos th1) * ( sin th2)))) / (( sin th1) * ( sin th2)))

      .= (( - ( sin (th1 - th2))) / (( sin th1) * ( sin th2))) by SIN_COS: 82

      .= ( - (( sin (th1 - th2)) / (( sin th1) * ( sin th2)))) by XCMPLX_1: 187;

      hence thesis;

    end;

    theorem :: SIN_COS4:25

    (( sin (th1 + th2)) + ( sin (th1 - th2))) = (2 * (( sin th1) * ( cos th2)))

    proof

      (( sin (th1 + th2)) + ( sin (th1 - th2))) = (((( sin th1) * ( cos th2)) + (( cos th1) * ( sin th2))) + ( sin (th1 - th2))) by SIN_COS: 75

      .= (((( sin th1) * ( cos th2)) + (( cos th1) * ( sin th2))) + ((( sin th1) * ( cos th2)) - ( - ( - (( cos th1) * ( sin th2)))))) by SIN_COS: 82

      .= (2 * (( sin th1) * ( cos th2)));

      hence thesis;

    end;

    theorem :: SIN_COS4:26

    (( sin (th1 + th2)) - ( sin (th1 - th2))) = (2 * (( cos th1) * ( sin th2)))

    proof

      (( sin (th1 + th2)) - ( sin (th1 - th2))) = (((( sin th1) * ( cos th2)) + (( cos th1) * ( sin th2))) - ( sin (th1 - th2))) by SIN_COS: 75

      .= (((( sin th1) * ( cos th2)) + (( cos th1) * ( sin th2))) - ( - ( - ((( sin th1) * ( cos th2)) - (( cos th1) * ( sin th2)))))) by SIN_COS: 82

      .= (2 * (( cos th1) * ( sin th2)));

      hence thesis;

    end;

    theorem :: SIN_COS4:27

    (( cos (th1 + th2)) + ( cos (th1 - th2))) = (2 * (( cos th1) * ( cos th2)))

    proof

      (( cos (th1 + th2)) + ( cos (th1 - th2))) = (((( cos th1) * ( cos th2)) - (( sin th1) * ( sin th2))) + ( cos (th1 - th2))) by SIN_COS: 75

      .= (((( cos th1) * ( cos th2)) + ( - (( sin th1) * ( sin th2)))) + ((( sin th1) * ( sin th2)) + (( cos th1) * ( cos th2)))) by SIN_COS: 83

      .= (2 * (( cos th1) * ( cos th2)));

      hence thesis;

    end;

    theorem :: SIN_COS4:28

    (( cos (th1 + th2)) - ( cos (th1 - th2))) = ( - (2 * (( sin th1) * ( sin th2))))

    proof

      (( cos (th1 + th2)) - ( cos (th1 - th2))) = (((( cos th1) * ( cos th2)) - (( sin th1) * ( sin th2))) - ( cos (th1 - th2))) by SIN_COS: 75

      .= (((( cos th1) * ( cos th2)) + ( - (( sin th1) * ( sin th2)))) - ((( cos th1) * ( cos th2)) + (( sin th1) * ( sin th2)))) by SIN_COS: 83

      .= ( - (2 * (( sin th1) * ( sin th2))));

      hence thesis;

    end;

    theorem :: SIN_COS4:29



     Th29: (( sin th1) * ( sin th2)) = ( - ((1 / 2) * (( cos (th1 + th2)) - ( cos (th1 - th2)))))

    proof

      (( sin th1) * ( sin th2)) = (((((( cos th1) * ( cos th2)) + (( sin th1) * ( sin th2))) - (( cos th1) * ( cos th2))) + (( sin th1) * ( sin th2))) / 2)

      .= (((((( cos th1) * ( cos ( - th2))) + (( sin th1) * ( sin th2))) - (( cos th1) * ( cos th2))) + (( sin th1) * ( sin th2))) / 2) by SIN_COS: 31

      .= (((((( cos th1) * ( cos ( - th2))) - (( sin th1) * ( - ( sin th2)))) - (( cos th1) * ( cos th2))) + (( sin th1) * ( sin th2))) / 2)

      .= (((((( cos th1) * ( cos ( - th2))) - (( sin th1) * ( sin ( - th2)))) - (( cos th1) * ( cos th2))) + (( sin th1) * ( sin th2))) / 2) by SIN_COS: 31

      .= (((( cos (th1 + ( - th2))) - (( cos th1) * ( cos th2))) + (( sin th1) * ( sin th2))) / 2) by SIN_COS: 75

      .= ((( cos (th1 - th2)) - ((( cos th1) * ( cos th2)) - (( sin th1) * ( sin th2)))) / 2)

      .= ((( cos (th1 - th2)) - ( cos (th1 + th2))) / (2 / 1)) by SIN_COS: 75

      .= ( - ((1 / 2) * (( cos (th1 + th2)) - ( cos (th1 - th2)))));

      hence thesis;

    end;

    theorem :: SIN_COS4:30



     Th30: (( sin th1) * ( cos th2)) = ((1 / 2) * (( sin (th1 + th2)) + ( sin (th1 - th2))))

    proof

      (( sin th1) * ( cos th2)) = ((1 / 2) * (((( sin th1) * ( cos th2)) + (( cos th1) * ( sin th2))) + ((( sin th1) * ( cos th2)) - (( cos th1) * ( sin th2)))))

      .= ((1 / 2) * (( sin (th1 + th2)) + ((( sin th1) * ( cos th2)) + (( cos th1) * ( - ( sin th2)))))) by SIN_COS: 75

      .= ((1 / 2) * (( sin (th1 + th2)) + ((( sin th1) * ( cos th2)) + (( cos th1) * ( sin ( - th2)))))) by SIN_COS: 31

      .= ((1 / 2) * (( sin (th1 + th2)) + ((( sin th1) * ( cos ( - th2))) + (( cos th1) * ( sin ( - th2)))))) by SIN_COS: 31

      .= ((1 / 2) * (( sin (th1 + th2)) + ( sin (th1 + ( - th2))))) by SIN_COS: 75

      .= ((1 / 2) * (( sin (th1 + th2)) + ( sin (th1 - th2))));

      hence thesis;

    end;

    theorem :: SIN_COS4:31



     Th31: (( cos th1) * ( sin th2)) = ((1 / 2) * (( sin (th1 + th2)) - ( sin (th1 - th2))))

    proof

      (( cos th1) * ( sin th2)) = ((1 / 2) * (((( sin th1) * ( cos th2)) + (( cos th1) * ( sin th2))) - ((( sin th1) * ( cos th2)) - (( cos th1) * ( sin th2)))))

      .= ((1 / 2) * (( sin (th1 + th2)) - ((( sin th1) * ( cos th2)) + (( cos th1) * ( - ( sin th2)))))) by SIN_COS: 75

      .= ((1 / 2) * (( sin (th1 + th2)) - ((( sin th1) * ( cos th2)) + (( cos th1) * ( sin ( - th2)))))) by SIN_COS: 31

      .= ((1 / 2) * (( sin (th1 + th2)) - ((( sin th1) * ( cos ( - th2))) + (( cos th1) * ( sin ( - th2)))))) by SIN_COS: 31

      .= ((1 / 2) * (( sin (th1 + th2)) - ( sin (th1 + ( - th2))))) by SIN_COS: 75

      .= ((1 / 2) * (( sin (th1 + th2)) - ( sin (th1 - th2))));

      hence thesis;

    end;

    theorem :: SIN_COS4:32



     Th32: (( cos th1) * ( cos th2)) = ((1 / 2) * (( cos (th1 + th2)) + ( cos (th1 - th2))))

    proof

      (( cos th1) * ( cos th2)) = ((1 / 2) * (((( cos th1) * ( cos th2)) - (( sin th1) * ( sin th2))) + ((( cos th1) * ( cos th2)) - ( - (( sin th1) * ( sin th2))))))

      .= ((1 / 2) * (( cos (th1 + th2)) + ((( cos th1) * ( cos th2)) - (( sin th1) * ( - ( sin th2)))))) by SIN_COS: 75

      .= ((1 / 2) * (( cos (th1 + th2)) + ((( cos th1) * ( cos th2)) - (( sin th1) * ( sin ( - th2)))))) by SIN_COS: 31

      .= ((1 / 2) * (( cos (th1 + th2)) + ((( cos th1) * ( cos ( - th2))) - (( sin th1) * ( sin ( - th2)))))) by SIN_COS: 31

      .= ((1 / 2) * (( cos (th1 + th2)) + ( cos (th1 + ( - th2))))) by SIN_COS: 75

      .= ((1 / 2) * (( cos (th1 + th2)) + ( cos (th1 - th2))));

      hence thesis;

    end;

    theorem :: SIN_COS4:33

    ((( sin th1) * ( sin th2)) * ( sin th3)) = ((1 / 4) * (((( sin ((th1 + th2) - th3)) + ( sin ((th2 + th3) - th1))) + ( sin ((th3 + th1) - th2))) - ( sin ((th1 + th2) + th3))))

    proof

      ((( sin th1) * ( sin th2)) * ( sin th3)) = (( - ((1 / 2) * (( cos (th1 + th2)) - ( cos (th1 - th2))))) * ( sin th3)) by Th29

      .= ((1 / 2) * ((( cos (th1 - th2)) * ( sin th3)) - (( cos (th1 + th2)) * ( sin th3))))

      .= ((1 / 2) * (((1 / 2) * (( sin ((th1 - th2) + th3)) - ( sin ((th1 - th2) - th3)))) - (( cos (th1 + th2)) * ( sin th3)))) by Th31

      .= ((1 / 2) * (((1 / 2) * (( sin ((th1 - th2) + th3)) - ( sin ((th1 - th2) - th3)))) - ((1 / 2) * (( sin ((th1 + th2) + th3)) - ( sin ((th1 + th2) - th3)))))) by Th31

      .= ((1 / (2 * 2)) * ((( sin ((th1 - th2) + th3)) + ( - ( sin ((th1 - th2) - th3)))) + (( sin ((th1 + th2) - th3)) - ( sin ((th1 + th2) + th3)))))

      .= ((1 / (2 * 2)) * ((( sin ((th1 - th2) + th3)) + ( sin ( - ((th1 - th2) - th3)))) + (( sin ((th1 + th2) - th3)) - ( sin ((th1 + th2) + th3))))) by SIN_COS: 31

      .= ((1 / (2 * 2)) * (((( sin ((th1 + th2) - th3)) + ( sin ((th2 + th3) - th1))) + ( sin ((th3 + th1) - th2))) - ( sin ((th1 + th2) + th3))));

      hence thesis;

    end;

    theorem :: SIN_COS4:34

    ((( sin th1) * ( sin th2)) * ( cos th3)) = ((1 / 4) * (((( - ( cos ((th1 + th2) - th3))) + ( cos ((th2 + th3) - th1))) + ( cos ((th3 + th1) - th2))) - ( cos ((th1 + th2) + th3))))

    proof

      ((( sin th1) * ( sin th2)) * ( cos th3)) = (( - ((1 / 2) * (( cos (th1 + th2)) - ( cos (th1 - th2))))) * ( cos th3)) by Th29

      .= ((1 / 2) * ((( cos (th1 - th2)) * ( cos th3)) - (( cos (th1 + th2)) * ( cos th3))))

      .= ((1 / 2) * (((1 / 2) * (( cos ((th1 - th2) + th3)) + ( cos ((th1 - th2) - th3)))) - (( cos (th1 + th2)) * ( cos th3)))) by Th32

      .= ((1 / 2) * (((1 / 2) * (( cos ((th1 - th2) + th3)) + ( cos ((th1 - th2) - th3)))) - ((1 / 2) * (( cos ((th1 + th2) + th3)) + ( cos ((th1 + th2) - th3)))))) by Th32

      .= ((1 / (2 * 2)) * ((( - ( cos ((th1 + th2) - th3))) + ( cos ( - ((th2 - th1) + th3)))) + (( cos ((th3 + th1) + ( - th2))) + ( - ( cos ((th1 + th2) + th3))))))

      .= ((1 / (2 * 2)) * ((( - ( cos ((th1 + th2) - th3))) + ( cos ((th2 - th1) + th3))) + (( cos ((th3 + th1) + ( - th2))) + ( - ( cos ((th1 + th2) + th3)))))) by SIN_COS: 31

      .= ((1 / (2 * 2)) * (((( - ( cos ((th1 + th2) - th3))) + ( cos ((th2 + th3) - th1))) + ( cos ((th3 + th1) - th2))) - ( cos ((th1 + th2) + th3))));

      hence thesis;

    end;

    theorem :: SIN_COS4:35

    ((( sin th1) * ( cos th2)) * ( cos th3)) = ((1 / 4) * (((( sin ((th1 + th2) - th3)) - ( sin ((th2 + th3) - th1))) + ( sin ((th3 + th1) - th2))) + ( sin ((th1 + th2) + th3))))

    proof

      ((( sin th1) * ( cos th2)) * ( cos th3)) = (((1 / 2) * (( sin (th1 + th2)) + ( sin (th1 - th2)))) * ( cos th3)) by Th30

      .= ((1 / 2) * ((( sin (th1 + th2)) * ( cos th3)) + (( sin (th1 - th2)) * ( cos th3))))

      .= ((1 / 2) * (((1 / 2) * (( sin ((th1 + th2) + th3)) + ( sin ((th1 + th2) - th3)))) + (( sin (th1 - th2)) * ( cos th3)))) by Th30

      .= ((1 / 2) * (((1 / 2) * (( sin ((th1 + th2) + th3)) + ( sin ((th1 + th2) - th3)))) + ((1 / 2) * (( sin ((th1 - th2) + th3)) + ( sin ((th1 - th2) - th3)))))) by Th30

      .= ((1 / (2 * 2)) * ((( sin ((th1 + th2) + th3)) + ( sin ((th1 + th2) - th3))) + (( sin ((th1 + ( - th2)) + th3)) + ( sin ( - ((th2 - th1) + th3))))))

      .= ((1 / (2 * 2)) * ((( sin ((th1 + th2) + th3)) + ( sin ((th1 + th2) - th3))) + (( - ( sin ((th2 - th1) + th3))) + ( sin ((th3 + th1) + ( - th2)))))) by SIN_COS: 31

      .= ((1 / (2 * 2)) * (((( sin ((th1 + th2) - th3)) - ( sin ((th2 + th3) - th1))) + ( sin ((th3 + th1) - th2))) + ( sin ((th1 + th2) + th3))));

      hence thesis;

    end;

    theorem :: SIN_COS4:36

    ((( cos th1) * ( cos th2)) * ( cos th3)) = ((1 / 4) * (((( cos ((th1 + th2) - th3)) + ( cos ((th2 + th3) - th1))) + ( cos ((th3 + th1) - th2))) + ( cos ((th1 + th2) + th3))))

    proof

      ((( cos th1) * ( cos th2)) * ( cos th3)) = (((1 / 2) * (( cos (th1 + th2)) + ( cos (th1 - th2)))) * ( cos th3)) by Th32

      .= ((1 / 2) * ((( cos (th1 + th2)) * ( cos th3)) + (( cos (th1 - th2)) * ( cos th3))))

      .= ((1 / 2) * (((1 / 2) * (( cos ((th1 + th2) + th3)) + ( cos ((th1 + th2) - th3)))) + (( cos (th1 - th2)) * ( cos th3)))) by Th32

      .= ((1 / 2) * (((1 / 2) * (( cos ((th1 + th2) + th3)) + ( cos ((th1 + th2) - th3)))) + ((1 / 2) * (( cos ((th1 - th2) + th3)) + ( cos ((th1 - th2) - th3)))))) by Th32

      .= ((1 / (2 * 2)) * ((( cos ((th1 + th2) + th3)) + ( cos ((th1 + th2) - th3))) + (( cos ((th3 + th1) + ( - th2))) + ( cos ( - ((th2 - th1) + th3))))))

      .= ((1 / (2 * 2)) * ((( cos ((th1 + th2) + th3)) + ( cos ((th1 + th2) - th3))) + (( cos ((th3 + th1) - th2)) + ( cos ((th2 + th3) + ( - th1)))))) by SIN_COS: 31

      .= ((1 / (2 * 2)) * (((( cos ((th1 + th2) - th3)) + ( cos ((th2 + th3) - th1))) + ( cos ((th3 + th1) - th2))) + ( cos ((th1 + th2) + th3))));

      hence thesis;

    end;

    theorem :: SIN_COS4:37



     Th37: (( sin (th1 + th2)) * ( sin (th1 - th2))) = ((( sin th1) * ( sin th1)) - (( sin th2) * ( sin th2)))

    proof

      (( sin (th1 + th2)) * ( sin (th1 - th2))) = (((( sin th1) * ( cos th2)) + (( cos th1) * ( sin th2))) * ( sin (th1 - th2))) by SIN_COS: 75

      .= (((( sin th1) * ( cos th2)) + (( cos th1) * ( sin th2))) * ((( sin th1) * ( cos th2)) - ( - ( - (( cos th1) * ( sin th2)))))) by SIN_COS: 82

      .= (((( sin th1) * ( sin th1)) * (( cos th2) * ( cos th2))) - (((( cos th1) * ( sin th2)) * ( cos th1)) * ( sin th2)))

      .= (((( sin th1) * ( sin th1)) * (1 - (( sin th2) * ( sin th2)))) - (((( cos th1) * ( cos th1)) * ( sin th2)) * ( sin th2))) by Th5

      .= (((( sin th1) * ( sin th1)) * (1 + ( - (( sin th2) * ( sin th2))))) - (((1 - ( - ( - (( sin th1) * ( sin th1))))) * ( sin th2)) * ( sin th2))) by Th5

      .= ((( sin th1) * ( sin th1)) - (( sin th2) * ( sin th2)));

      hence thesis;

    end;

    theorem :: SIN_COS4:38

    (( sin (th1 + th2)) * ( sin (th1 - th2))) = ((( cos th2) * ( cos th2)) - (( cos th1) * ( cos th1)))

    proof

      (( sin (th1 + th2)) * ( sin (th1 - th2))) = ((( sin th1) * ( sin th1)) - (( sin th2) * ( sin th2))) by Th37

      .= ((1 - (( cos th1) * ( cos th1))) - (( sin th2) * ( sin th2))) by Th4

      .= ((1 - ( - ( - (( cos th1) * ( cos th1))))) - ( - ( - (1 - (( cos th2) * ( cos th2)))))) by Th4

      .= ((( cos th2) * ( cos th2)) - (( cos th1) * ( cos th1)));

      hence thesis;

    end;

    theorem :: SIN_COS4:39



     Th39: (( sin (th1 + th2)) * ( cos (th1 - th2))) = ((( sin th1) * ( cos th1)) + (( sin th2) * ( cos th2)))

    proof

      (( sin (th1 + th2)) * ( cos (th1 - th2))) = (((( sin th1) * ( cos th2)) + (( cos th1) * ( sin th2))) * ( cos (th1 - th2))) by SIN_COS: 75

      .= (((( sin th1) * ( cos th2)) + (( cos th1) * ( sin th2))) * ((( cos th1) * ( cos th2)) + (( sin th1) * ( sin th2)))) by SIN_COS: 83

      .= (((( sin th1) * ( cos th1)) * ((( sin th2) * ( sin th2)) + (( cos th2) * ( cos th2)))) + (((( sin th2) * ( cos th2)) * (( sin th1) * ( sin th1))) + ((( sin th2) * ( cos th2)) * (( cos th1) * ( cos th1)))))

      .= (((( sin th1) * ( cos th1)) * 1) + ((( sin th2) * ( cos th2)) * ((( sin th1) * ( sin th1)) + (( cos th1) * ( cos th1))))) by SIN_COS: 29

      .= ((( sin th1) * ( cos th1)) + ((( sin th2) * ( cos th2)) * (1 / 1))) by SIN_COS: 29

      .= ((( sin th1) * ( cos th1)) + (( sin th2) * ( cos th2)));

      hence thesis;

    end;

    theorem :: SIN_COS4:40

    (( cos (th1 + th2)) * ( sin (th1 - th2))) = ((( sin th1) * ( cos th1)) - (( sin th2) * ( cos th2)))

    proof

      (( cos (th1 + th2)) * ( sin (th1 - th2))) = (( sin (th1 + ( - th2))) * ( cos (th1 - ( - th2))))

      .= ((( sin th1) * ( cos th1)) + (( sin ( - th2)) * ( cos ( - th2)))) by Th39

      .= ((( sin th1) * ( cos th1)) + (( sin ( - th2)) * ( cos th2))) by SIN_COS: 31

      .= ((( sin th1) * ( cos th1)) + (( - ( sin th2)) * ( cos th2))) by SIN_COS: 31

      .= ((( sin th1) * ( cos th1)) - (( sin th2) * ( cos th2)));

      hence thesis;

    end;

    theorem :: SIN_COS4:41



     Th41: (( cos (th1 + th2)) * ( cos (th1 - th2))) = ((( cos th1) * ( cos th1)) - (( sin th2) * ( sin th2)))

    proof

      (( cos (th1 + th2)) * ( cos (th1 - th2))) = (((( cos th1) * ( cos th2)) - (( sin th1) * ( sin th2))) * ( cos (th1 - th2))) by SIN_COS: 75

      .= (((( cos th1) * ( cos th2)) + ( - (( sin th1) * ( sin th2)))) * ((( cos th1) * ( cos th2)) + (( sin th1) * ( sin th2)))) by SIN_COS: 83

      .= (((((( cos th1) * ( cos th1)) * (( cos th2) * ( cos th2))) + ((( cos th1) * ( cos th2)) * (( sin th1) * ( sin th2)))) + ( - ((( sin th1) * ( sin th2)) * (( cos th1) * ( cos th2))))) + ( - (((( sin th1) * ( sin th1)) * ( sin th2)) * ( sin th2))))

      .= (((( cos th1) * ( cos th1)) * (1 - ( - ( - (( sin th2) * ( sin th2)))))) + ( - ((( sin th1) * ( sin th1)) * (( sin th2) * ( sin th2))))) by Th5

      .= (((( cos th1) * ( cos th1)) * 1) + ((( sin th2) * ( sin th2)) * ( - ((( cos th1) * ( cos th1)) + (( sin th1) * ( sin th1))))))

      .= (((( cos th1) * ( cos th1)) * 1) + ((( sin th2) * ( sin th2)) * ( - 1))) by SIN_COS: 29

      .= ((( cos th1) * ( cos th1)) - (( sin th2) * ( sin th2)));

      hence thesis;

    end;

    theorem :: SIN_COS4:42

    (( cos (th1 + th2)) * ( cos (th1 - th2))) = ((( cos th2) * ( cos th2)) - (( sin th1) * ( sin th1)))

    proof

      (( cos (th1 + th2)) * ( cos (th1 - th2))) = ((( cos th1) * ( cos th1)) - (( sin th2) * ( sin th2))) by Th41

      .= ((1 - (( sin th1) * ( sin th1))) - (( sin th2) * ( sin th2))) by Th5

      .= ((1 - (( sin th1) * ( sin th1))) - (1 - (( cos th2) * ( cos th2)))) by Th4

      .= ((( cos th2) * ( cos th2)) - (( sin th1) * ( sin th1)));

      hence thesis;

    end;

    theorem :: SIN_COS4:43

    ( cos th1) <> 0 & ( cos th2) <> 0 implies (( sin (th1 + th2)) / ( sin (th1 - th2))) = ((( tan th1) + ( tan th2)) / (( tan th1) - ( tan th2)))

    proof

      assume that

       A1: ( cos th1) <> 0 and

       A2: ( cos th2) <> 0 ;

      (( sin (th1 + th2)) / ( sin (th1 - th2))) = (((( sin th1) * ( cos th2)) + (( cos th1) * ( sin th2))) / ( sin (th1 - th2))) by SIN_COS: 75

      .= (((( sin th1) * ( cos th2)) + (( cos th1) * ( sin th2))) / ((( sin th1) * ( cos th2)) - (( cos th1) * ( sin th2)))) by SIN_COS: 82

      .= ((((( sin th1) * ( cos th2)) + (( cos th1) * ( sin th2))) / (( cos th1) * ( cos th2))) / (((( sin th1) * ( cos th2)) - (( cos th1) * ( sin th2))) / (( cos th1) * ( cos th2)))) by A1, A2, XCMPLX_1: 55

      .= ((((( sin th1) * ( cos th2)) / (( cos th1) * ( cos th2))) + ((( cos th1) * ( sin th2)) / (( cos th1) * ( cos th2)))) / (((( sin th1) * ( cos th2)) + ( - (( cos th1) * ( sin th2)))) / (( cos th1) * ( cos th2)))) by XCMPLX_1: 62

      .= ((((( sin th1) * ( cos th2)) / (( cos th1) * ( cos th2))) + ((( cos th1) * ( sin th2)) / (( cos th1) * ( cos th2)))) / (((( sin th1) * ( cos th2)) / (( cos th1) * ( cos th2))) + (( - (( cos th1) * ( sin th2))) / (( cos th1) * ( cos th2))))) by XCMPLX_1: 62

      .= ((((( sin th1) / ( cos th1)) * (( cos th2) / ( cos th2))) + ((( cos th1) * ( sin th2)) / (( cos th1) * ( cos th2)))) / (((( sin th1) * ( cos th2)) / (( cos th1) * ( cos th2))) + (( - (( cos th1) * ( sin th2))) / (( cos th1) * ( cos th2))))) by XCMPLX_1: 76

      .= ((((( sin th1) / ( cos th1)) * (( cos th2) / ( cos th2))) + ((( cos th1) / ( cos th1)) * (( sin th2) / ( cos th2)))) / (((( sin th1) * ( cos th2)) / (( cos th1) * ( cos th2))) + (( - (( cos th1) * ( sin th2))) / (( cos th1) * ( cos th2))))) by XCMPLX_1: 76

      .= ((((( sin th1) / ( cos th1)) * (( cos th2) / ( cos th2))) + ((( cos th1) / ( cos th1)) * (( sin th2) / ( cos th2)))) / (((( sin th1) / ( cos th1)) * (( cos th2) / ( cos th2))) + ((( cos th1) * ( - ( sin th2))) / (( cos th1) * ( cos th2))))) by XCMPLX_1: 76

      .= ((((( sin th1) / ( cos th1)) * (( cos th2) / ( cos th2))) + ((( cos th1) / ( cos th1)) * (( sin th2) / ( cos th2)))) / (((( sin th1) / ( cos th1)) * (( cos th2) / ( cos th2))) + ((( cos th1) / ( cos th1)) * (( - ( sin th2)) / ( cos th2))))) by XCMPLX_1: 76

      .= (((( sin th1) / ( cos th1)) + ((( cos th1) / ( cos th1)) * (( sin th2) / ( cos th2)))) / (((( sin th1) / ( cos th1)) * (( cos th2) / ( cos th2))) + ((( cos th1) / ( cos th1)) * (( - ( sin th2)) / ( cos th2))))) by A2, XCMPLX_1: 88

      .= (((( sin th1) / ( cos th1)) + (( sin th2) / ( cos th2))) / (((( sin th1) / ( cos th1)) * (( cos th2) / ( cos th2))) + ((( cos th1) / ( cos th1)) * (( - ( sin th2)) / ( cos th2))))) by A1, XCMPLX_1: 88

      .= (((( sin th1) / ( cos th1)) + (( sin th2) / ( cos th2))) / ((( sin th1) / ( cos th1)) + ((( cos th1) / ( cos th1)) * (( - ( sin th2)) / ( cos th2))))) by A2, XCMPLX_1: 88

      .= (((( sin th1) / ( cos th1)) + (( sin th2) / ( cos th2))) / ((( sin th1) / ( cos th1)) + (( - ( sin th2)) / ( cos th2)))) by A1, XCMPLX_1: 88

      .= ((( tan th1) + ( tan th2)) / (( tan th1) + ( - (( sin th2) / ( cos th2))))) by XCMPLX_1: 187

      .= ((( tan th1) + ( tan th2)) / (( tan th1) - ( tan th2)));

      hence thesis;

    end;

    theorem :: SIN_COS4:44

    ( cos th1) <> 0 & ( cos th2) <> 0 implies (( cos (th1 + th2)) / ( cos (th1 - th2))) = ((1 - (( tan th1) * ( tan th2))) / (1 + (( tan th1) * ( tan th2))))

    proof

      assume

       A1: ( cos th1) <> 0 & ( cos th2) <> 0 ;

      (( cos (th1 + th2)) / ( cos (th1 - th2))) = (((( cos th1) * ( cos th2)) - (( sin th1) * ( sin th2))) / ( cos (th1 - th2))) by SIN_COS: 75

      .= ((((( cos th1) * ( cos th2)) - (( sin th1) * ( sin th2))) / (( cos th1) * ( cos th2))) / (( cos (th1 - th2)) / (( cos th1) * ( cos th2)))) by A1, XCMPLX_1: 55

      .= ((((( cos th1) * ( cos th2)) / (( cos th1) * ( cos th2))) - ((( sin th1) * ( sin th2)) / (( cos th1) * ( cos th2)))) / (( cos (th1 - th2)) / (( cos th1) * ( cos th2)))) by XCMPLX_1: 120

      .= ((1 - ((( sin th1) * ( sin th2)) / (( cos th1) * ( cos th2)))) / (( cos (th1 - th2)) / (( cos th1) * ( cos th2)))) by A1, XCMPLX_1: 60

      .= ((1 - (( tan th1) * (( sin th2) / ( cos th2)))) / (( cos (th1 - th2)) / (( cos th1) * ( cos th2)))) by XCMPLX_1: 76

      .= ((1 - (( tan th1) * ( tan th2))) / (((( cos th1) * ( cos th2)) + (( sin th1) * ( sin th2))) / (( cos th1) * ( cos th2)))) by SIN_COS: 83

      .= ((1 - (( tan th1) * ( tan th2))) / (((( cos th1) * ( cos th2)) / (( cos th1) * ( cos th2))) + ((( sin th1) * ( sin th2)) / (( cos th1) * ( cos th2))))) by XCMPLX_1: 62

      .= ((1 - (( tan th1) * ( tan th2))) / (1 + ((( sin th1) * ( sin th2)) / (( cos th1) * ( cos th2))))) by A1, XCMPLX_1: 60

      .= ((1 - (( tan th1) * ( tan th2))) / (1 + (( tan th1) * ( tan th2)))) by XCMPLX_1: 76;

      hence thesis;

    end;

    theorem :: SIN_COS4:45

    ((( sin th1) + ( sin th2)) / (( sin th1) - ( sin th2))) = (( tan ((th1 + th2) / 2)) * ( cot ((th1 - th2) / 2)))

    proof

      ((( sin th1) + ( sin th2)) / (( sin th1) - ( sin th2))) = ((2 * (( cos ((th1 - th2) / 2)) * ( sin ((th1 + th2) / 2)))) / (( sin th1) - ( sin th2))) by Th15

      .= ((2 * (( cos ((th1 - th2) / 2)) * ( sin ((th1 + th2) / 2)))) / (2 * (( cos ((th1 + th2) / 2)) * ( sin ((th1 - th2) / 2))))) by Th16

      .= ((2 / 2) * ((( cos ((th1 - th2) / 2)) * ( sin ((th1 + th2) / 2))) / (( cos ((th1 + th2) / 2)) * ( sin ((th1 - th2) / 2))))) by XCMPLX_1: 76

      .= (( tan ((th1 + th2) / 2)) * ( cot ((th1 - th2) / 2))) by XCMPLX_1: 76;

      hence thesis;

    end;

    theorem :: SIN_COS4:46

    ( cos ((th1 - th2) / 2)) <> 0 implies ((( sin th1) + ( sin th2)) / (( cos th1) + ( cos th2))) = ( tan ((th1 + th2) / 2))

    proof

      assume

       A1: ( cos ((th1 - th2) / 2)) <> 0 ;

      ((( sin th1) + ( sin th2)) / (( cos th1) + ( cos th2))) = ((2 * (( cos ((th1 - th2) / 2)) * ( sin ((th1 + th2) / 2)))) / (( cos th1) + ( cos th2))) by Th15

      .= ((2 * (( cos ((th1 - th2) / 2)) * ( sin ((th1 + th2) / 2)))) / (2 * (( cos ((th1 + th2) / 2)) * ( cos ((th1 - th2) / 2))))) by Th17

      .= ((2 / 2) * ((( cos ((th1 - th2) / 2)) * ( sin ((th1 + th2) / 2))) / (( cos ((th1 - th2) / 2)) * ( cos ((th1 + th2) / 2))))) by XCMPLX_1: 76

      .= ((( cos ((th1 - th2) / 2)) / ( cos ((th1 - th2) / 2))) * (( sin ((th1 + th2) / 2)) / ( cos ((th1 + th2) / 2)))) by XCMPLX_1: 76

      .= ( tan ((th1 + th2) / 2)) by A1, XCMPLX_1: 88;

      hence thesis;

    end;

    theorem :: SIN_COS4:47

    ( cos ((th1 + th2) / 2)) <> 0 implies ((( sin th1) - ( sin th2)) / (( cos th1) + ( cos th2))) = ( tan ((th1 - th2) / 2))

    proof

      assume

       A1: ( cos ((th1 + th2) / 2)) <> 0 ;

      ((( sin th1) - ( sin th2)) / (( cos th1) + ( cos th2))) = ((2 * (( cos ((th1 + th2) / 2)) * ( sin ((th1 - th2) / 2)))) / (( cos th1) + ( cos th2))) by Th16

      .= ((2 * (( cos ((th1 + th2) / 2)) * ( sin ((th1 - th2) / 2)))) / (2 * (( cos ((th1 + th2) / 2)) * ( cos ((th1 - th2) / 2))))) by Th17

      .= ((2 / 2) * ((( cos ((th1 + th2) / 2)) * ( sin ((th1 - th2) / 2))) / (( cos ((th1 + th2) / 2)) * ( cos ((th1 - th2) / 2))))) by XCMPLX_1: 76

      .= ((( cos ((th1 + th2) / 2)) / ( cos ((th1 + th2) / 2))) * (( sin ((th1 - th2) / 2)) / ( cos ((th1 - th2) / 2)))) by XCMPLX_1: 76

      .= ( tan ((th1 - th2) / 2)) by A1, XCMPLX_1: 88;

      hence thesis;

    end;

    theorem :: SIN_COS4:48

    ( sin ((th1 + th2) / 2)) <> 0 implies ((( sin th1) + ( sin th2)) / (( cos th2) - ( cos th1))) = ( cot ((th1 - th2) / 2))

    proof

      assume

       A1: ( sin ((th1 + th2) / 2)) <> 0 ;

      ((( sin th1) + ( sin th2)) / (( cos th2) - ( cos th1))) = ((2 * (( cos ((th1 - th2) / 2)) * ( sin ((th1 + th2) / 2)))) / (( cos th2) - ( cos th1))) by Th15

      .= ((2 * (( cos ((th1 - th2) / 2)) * ( sin ((th1 + th2) / 2)))) / ( - (2 * (( sin ((th2 + th1) / 2)) * ( sin ((th2 - th1) / 2)))))) by Th18

      .= ((2 * (( cos ((th1 - th2) / 2)) * ( sin ((th1 + th2) / 2)))) / (2 * (( sin ((th2 + th1) / 2)) * ( - ( sin ((th2 - th1) / 2))))))

      .= ((2 * (( cos ((th1 - th2) / 2)) * ( sin ((th1 + th2) / 2)))) / (2 * (( sin ((th2 + th1) / 2)) * ( sin ( - ((th2 - th1) / 2)))))) by SIN_COS: 31

      .= ((2 / 2) * ((( cos ((th1 - th2) / 2)) * ( sin ((th1 + th2) / 2))) / (( sin ((th2 + th1) / 2)) * ( sin ((th1 - th2) / 2))))) by XCMPLX_1: 76

      .= ((( cos ((th1 - th2) / 2)) / ( sin ((th1 - th2) / 2))) * (( sin ((th1 + th2) / 2)) / ( sin ((th2 + th1) / 2)))) by XCMPLX_1: 76

      .= ( cot ((th1 - th2) / 2)) by A1, XCMPLX_1: 88;

      hence thesis;

    end;

    theorem :: SIN_COS4:49

    ( sin ((th1 - th2) / 2)) <> 0 implies ((( sin th1) - ( sin th2)) / (( cos th2) - ( cos th1))) = ( cot ((th1 + th2) / 2))

    proof

      assume

       A1: ( sin ((th1 - th2) / 2)) <> 0 ;

      ((( sin th1) - ( sin th2)) / (( cos th2) - ( cos th1))) = ((2 * (( cos ((th1 + th2) / 2)) * ( sin ((th1 - th2) / 2)))) / (( cos th2) - ( cos th1))) by Th16

      .= ((2 * (( cos ((th1 + th2) / 2)) * ( sin ((th1 - th2) / 2)))) / ( - (2 * (( sin ((th2 + th1) / 2)) * ( sin ((th2 - th1) / 2)))))) by Th18

      .= ((2 * (( cos ((th1 + th2) / 2)) * ( sin ((th1 - th2) / 2)))) / (2 * (( sin ((th2 + th1) / 2)) * ( - ( sin ((th2 - th1) / 2))))))

      .= ((2 * (( cos ((th1 + th2) / 2)) * ( sin ((th1 - th2) / 2)))) / (2 * (( sin ((th2 + th1) / 2)) * ( sin ( - ((th2 - th1) / 2)))))) by SIN_COS: 31

      .= ((2 / 2) * ((( cos ((th1 + th2) / 2)) * ( sin ((th1 - th2) / 2))) / (( sin ((th2 + th1) / 2)) * ( sin ((th1 - th2) / 2))))) by XCMPLX_1: 76

      .= ((( cos ((th1 + th2) / 2)) / ( sin ((th2 + th1) / 2))) * (( sin ((th1 - th2) / 2)) / ( sin ((th1 - th2) / 2)))) by XCMPLX_1: 76

      .= ( cot ((th1 + th2) / 2)) by A1, XCMPLX_1: 88;

      hence thesis;

    end;

    theorem :: SIN_COS4:50

    ((( cos th1) + ( cos th2)) / (( cos th1) - ( cos th2))) = (( cot ((th1 + th2) / 2)) * ( cot ((th2 - th1) / 2)))

    proof

      ((( cos th1) + ( cos th2)) / (( cos th1) - ( cos th2))) = ((2 * (( cos ((th1 + th2) / 2)) * ( cos ((th1 - th2) / 2)))) / (( cos th1) - ( cos th2))) by Th17

      .= ((2 * (( cos ((th1 + th2) / 2)) * ( cos ((th1 - th2) / 2)))) / ( - (2 * (( sin ((th1 + th2) / 2)) * ( sin ((th1 - th2) / 2)))))) by Th18

      .= ((2 * (( cos ((th1 + th2) / 2)) * ( cos ((th1 - th2) / 2)))) / (2 * (( sin ((th1 + th2) / 2)) * ( - ( sin ((th1 - th2) / 2))))))

      .= ((2 * (( cos ((th1 + th2) / 2)) * ( cos ((th1 - th2) / 2)))) / (2 * (( sin ((th1 + th2) / 2)) * ( sin ( - ((th1 - th2) / 2)))))) by SIN_COS: 31

      .= ((2 / 2) * ((( cos ((th1 + th2) / 2)) * ( cos ((th1 - th2) / 2))) / (( sin ((th1 + th2) / 2)) * ( sin ((th2 - th1) / 2))))) by XCMPLX_1: 76

      .= ((( cos ((th1 + th2) / 2)) / ( sin ((th1 + th2) / 2))) * (( cos ( - ((th2 - th1) / 2))) / ( sin ((th2 - th1) / 2)))) by XCMPLX_1: 76

      .= (( cot ((th1 + th2) / 2)) * ( cot ((th2 - th1) / 2))) by SIN_COS: 31;

      hence thesis;

    end;