:: Formulas And Identities of Trigonometric Functions :: by Pacharapokin Chanapat, Kanchun and Hiroshi Yamazaki :: :: Received February 3, 2004 :: Copyright (c) 2004-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies SIN_COS, REAL_1, ARYTM_3, ARYTM_1, RELAT_1, CARD_1, SIN_COS4; notations ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, SIN_COS; constructors SQUARE_1, NEWTON, SIN_COS; registrations XCMPLX_0, XREAL_0, SIN_COS, ORDINAL1; requirements NUMERALS, SUBSET, ARITHM; theorems XCMPLX_1, SIN_COS; begin reserve th, th1, th2, th3 for Real; definition let th be Real; func tan(th) -> Real equals sin(th)/cos(th); correctness; end; definition let th be Real; func cot(th) -> Real equals cos(th)/sin(th); correctness; end; definition let th be Real; func cosec(th) -> Real equals 1/sin(th); correctness; end; definition let th be Real; func sec(th) -> Real equals 1/cos(th); correctness; end; theorem 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 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 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 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 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 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 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 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(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(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 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 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 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(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 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 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 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 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 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 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 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 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(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(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(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(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 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 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 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 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 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 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(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(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(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 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 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(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 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 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 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 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 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 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(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 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 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((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((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 (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;