:: Formulas And Identities of Trigonometric Functions :: by Pacharapokin Chanapat, Kanchun and Hiroshi Yamazaki :: :: Received February 3, 2004 :: Copyright (c) 2004-2021 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; begin reserve th, th1, th2, th3 for Real; definition let th be Real; func tan(th) -> Real equals :: SIN_COS4:def 1 sin(th)/cos(th); end; definition let th be Real; func cot(th) -> Real equals :: SIN_COS4:def 2 cos(th)/sin(th); end; definition let th be Real; func cosec(th) -> Real equals :: SIN_COS4:def 3 1/sin(th); end; definition let th be Real; func sec(th) -> Real equals :: SIN_COS4:def 4 1/cos(th); end; theorem :: SIN_COS4:1 tan(-th) = -tan(th); theorem :: SIN_COS4:2 cosec(-th) = -1/sin(th); theorem :: SIN_COS4:3 cot(-th) = -cot(th); theorem :: SIN_COS4:4 sin(th)*sin(th) = 1-cos(th)*cos(th); theorem :: SIN_COS4:5 cos(th)*cos(th) = 1-sin(th)*sin(th); theorem :: SIN_COS4:6 cos(th)<>0 implies sin(th) = cos(th)*tan(th); theorem :: SIN_COS4:7 cos(th1)<>0 & cos(th2)<>0 implies tan(th1+th2)=(tan(th1)+tan(th2))/(1- tan(th1)*tan(th2)); theorem :: SIN_COS4:8 cos(th1)<>0 & cos(th2)<>0 implies tan(th1-th2)=(tan(th1)-tan(th2))/(1+ tan(th1)*tan(th2)); theorem :: SIN_COS4:9 sin(th1)<>0 & sin(th2)<>0 implies cot(th1+th2) = (cot(th1)*cot(th2)-1) /(cot(th2)+cot(th1)); theorem :: SIN_COS4:10 sin(th1)<>0 & sin(th2)<>0 implies cot(th1-th2)=(cot(th1)*cot(th2)+1)/( cot(th2)-cot(th1)); theorem :: SIN_COS4:11 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)); theorem :: SIN_COS4:12 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)); 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)); 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); theorem :: SIN_COS4:15 sin(th1)+sin(th2)= 2*(cos((th1-th2)/2)*sin((th1+th2)/2)); theorem :: SIN_COS4:16 sin(th1)-sin(th2)= 2*(cos((th1+th2)/2)*sin((th1-th2)/2)); theorem :: SIN_COS4:17 cos(th1)+cos(th2)= 2*(cos((th1+th2)/2)*cos((th1-th2)/2)); theorem :: SIN_COS4:18 cos(th1)-cos(th2)= -2*(sin((th1+th2)/2)*sin((th1-th2)/2)); theorem :: SIN_COS4:19 cos(th1)<>0 & cos(th2)<>0 implies tan(th1)+tan(th2)= sin(th1+th2)/(cos (th1)*cos(th2)); theorem :: SIN_COS4:20 cos(th1)<>0 & cos(th2)<>0 implies tan(th1)-tan(th2)= sin(th1-th2)/(cos (th1)*cos(th2)); theorem :: SIN_COS4:21 cos(th1)<>0 & sin(th2)<>0 implies tan(th1)+cot(th2)= cos(th1-th2)/(cos (th1)*sin(th2)); theorem :: SIN_COS4:22 cos(th1)<>0 & sin(th2)<>0 implies tan(th1)-cot(th2)= -cos(th1+th2)/( cos(th1)*sin(th2)); theorem :: SIN_COS4:23 sin(th1)<>0 & sin(th2)<>0 implies cot(th1)+cot(th2) = sin(th1+th2)/( sin(th1)*sin(th2)); theorem :: SIN_COS4:24 sin(th1)<>0 & sin(th2)<>0 implies cot(th1)-cot(th2)= -sin(th1-th2)/( sin(th1)*sin(th2)); theorem :: SIN_COS4:25 sin(th1+th2)+sin(th1-th2) = 2*(sin(th1)*cos(th2)); theorem :: SIN_COS4:26 sin(th1+th2)-sin(th1-th2) = 2*(cos(th1)*sin(th2)); theorem :: SIN_COS4:27 cos(th1+th2)+cos(th1-th2) = 2*(cos(th1)*cos(th2)); theorem :: SIN_COS4:28 cos(th1+th2)-cos(th1-th2) = -2*(sin(th1)*sin(th2)); theorem :: SIN_COS4:29 sin(th1)*sin(th2) = -(1/2)*(cos(th1+th2)-cos(th1-th2)); theorem :: SIN_COS4:30 sin(th1)*cos(th2)= (1/2)*(sin(th1+th2)+sin(th1-th2)); theorem :: SIN_COS4:31 cos(th1)*sin(th2)= (1/2)*(sin(th1+th2)-sin(th1-th2)); theorem :: SIN_COS4:32 cos(th1)*cos(th2)= (1/2)*(cos(th1+th2)+cos(th1-th2)); 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)); 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)); 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)); 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)); theorem :: SIN_COS4:37 sin(th1+th2)*sin(th1-th2) = sin(th1)*sin(th1)-sin(th2)*sin(th2); theorem :: SIN_COS4:38 sin(th1+th2)*sin(th1-th2)= cos(th2)*cos(th2)-cos(th1)*cos(th1); theorem :: SIN_COS4:39 sin(th1+th2)*cos(th1-th2) = sin(th1)*cos(th1)+sin(th2)*cos(th2); theorem :: SIN_COS4:40 cos(th1+th2)*sin(th1-th2) = sin(th1)*cos(th1)-sin(th2)*cos(th2); theorem :: SIN_COS4:41 cos(th1+th2)*cos(th1-th2)= cos(th1)*cos(th1)-sin(th2)*sin(th2); theorem :: SIN_COS4:42 cos(th1+th2)*cos(th1-th2) = cos(th2)*cos(th2)-sin(th1)*sin(th1); 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)); 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)); theorem :: SIN_COS4:45 (sin(th1)+sin(th2))/(sin(th1)-sin(th2)) = tan((th1+th2)/2)*cot((th1- th2)/2 ) ; theorem :: SIN_COS4:46 cos((th1-th2)/2)<>0 implies (sin(th1)+sin(th2))/(cos(th1)+cos(th2)) = tan((th1+th2)/2); theorem :: SIN_COS4:47 cos((th1+th2)/2)<>0 implies (sin(th1)-sin(th2))/(cos(th1)+cos(th2)) = tan((th1-th2)/2); theorem :: SIN_COS4:48 sin((th1+th2)/2)<>0 implies (sin(th1)+sin(th2))/(cos(th2)-cos(th1)) = cot((th1-th2)/2); theorem :: SIN_COS4:49 sin((th1-th2)/2)<>0 implies (sin(th1)-sin(th2))/(cos(th2)-cos(th1)) = cot((th1+th2)/2); theorem :: SIN_COS4:50 (cos(th1)+cos(th2))/(cos(th1)-cos(th2)) = cot((th1+th2)/2)*cot((th2- th1)/2);