:: Formulas And Identities of Trigonometric Functions
:: by Pacharapokin Chanapat, Kanchun and Hiroshi Yamazaki
::
:: Received February 3, 2004
:: Copyright (c) 2004-2026 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;