:: Formulas And Identities of Trigonometric Functions :: by Yuzhong Ding and Xiquan Liang :: :: Received March 18, 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 NUMBERS, SIN_COS, CARD_1, SIN_COS4, ARYTM_3, RELAT_1, ARYTM_1, SQUARE_1, NEWTON, COMPLEX1, XXREAL_0, REAL_1, SIN_COS2, FUNCT_1, SIN_COS5; notations FUNCT_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, SQUARE_1, SIN_COS4, SIN_COS, NEWTON, NAT_1, SIN_COS2, XXREAL_0; constructors REAL_1, SQUARE_1, NAT_1, BINOP_2, SIN_COS, SIN_COS2, SIN_COS4, VALUED_1, NEWTON; registrations XREAL_0, SQUARE_1, MEMBERED, NEWTON, SIN_COS, VALUED_0, RELSET_1, SIN_COS2; requirements REAL, NUMERALS, SUBSET, ARITHM, BOOLE; begin reserve x,x1,x2,x3 for Real; theorem :: SIN_COS5:1 cos(x)<>0 implies cosec(x)=sec(x)/tan(x); theorem :: SIN_COS5:2 sin(x)<>0 implies cos(x) = sin(x)*cot(x); theorem :: SIN_COS5:3 sin(x1)<>0 & sin(x2)<>0 & sin(x3)<>0 implies sin(x1+x2+x3)=sin(x1)*sin (x2)*sin(x3)*(cot(x2)*cot(x3)+ cot(x1)*cot(x3)+cot(x1)*cot(x2)-1); theorem :: SIN_COS5:4 sin(x1)<>0 & sin(x2)<>0 & sin(x3)<>0 implies cos(x1+x2+x3)=-sin(x1)* sin(x2)*sin(x3)*(cot(x1)+cot(x2)+cot(x3)- cot(x1)*cot(x2)*cot(x3)); theorem :: SIN_COS5:5 sin(2*x) = 2*sin(x)*cos(x); theorem :: SIN_COS5:6 cos(x)<>0 implies sin(2*x)=(2*tan(x))/(1+(tan(x))^2); theorem :: SIN_COS5:7 cos(2*x)=(cos(x))^2-(sin(x))^2 & cos(2*x)=2*(cos(x))^2-1 & cos(2* x)=1-2*(sin(x))^2; theorem :: SIN_COS5:8 cos(x)<>0 implies cos(2*x)=(1-(tan(x))^2)/(1+(tan(x))^2); theorem :: SIN_COS5:9 cos(x)<>0 implies tan(2*x)=(2*tan(x))/(1-(tan(x))^2); theorem :: SIN_COS5:10 sin(x)<>0 implies cot(2*x)=((cot(x))^2-1)/(2*cot(x)); theorem :: SIN_COS5:11 cos(x)<>0 implies (sec x)^2 = 1 + (tan x)^2; theorem :: SIN_COS5:12 cot(x) = 1/tan(x); theorem :: SIN_COS5:13 cos(x)<>0 & sin(x)<>0 implies sec(2*x) = (sec(x))^2/(1-(tan(x)) ^2) & sec(2*x)=(cot(x)+tan(x))/(cot(x)-tan(x)); theorem :: SIN_COS5:14 sin(x)<>0 implies (cosec(x))^2 = 1 +(cot(x))^2; theorem :: SIN_COS5:15 cos(x)<>0 & sin(x)<>0 implies cosec(2*x)=sec(x)*cosec(x)/2 & cosec(2*x )=(tan(x)+cot(x))/2; theorem :: SIN_COS5:16 sin(3*x)=-4*(sin(x))|^3+3*sin(x); theorem :: SIN_COS5:17 cos(3*x)=4*(cos(x))|^3-3*cos(x); theorem :: SIN_COS5:18 cos(x)<>0 implies tan(3*x)=(3*tan(x)-(tan(x))|^3)/(1-3*(tan(x))^2); theorem :: SIN_COS5:19 sin(x)<>0 implies cot(3*x)=((cot(x))|^3-3*cot(x))/(3*(cot(x))^2-1); theorem :: SIN_COS5:20 (sin(x))^2=(1-cos(2*x))/2; theorem :: SIN_COS5:21 (cos(x))^2=(1+cos(2*x))/2; theorem :: SIN_COS5:22 (sin(x))|^3=(3*sin(x)-sin(3*x))/4; theorem :: SIN_COS5:23 (cos(x))|^3=(3*cos(x)+cos(3*x))/4; theorem :: SIN_COS5:24 (sin(x))|^4=(3-4*cos(2*x)+cos(4*x))/8; theorem :: SIN_COS5:25 (cos(x))|^4 = (3+4*cos(2*x)+cos(4*x))/8; :: Half Angle theorem :: SIN_COS5:26 sin(x/2)=sqrt((1-cos(x))/2) or sin(x/2)=-sqrt((1-cos(x))/2); theorem :: SIN_COS5:27 cos(x/2)=sqrt((1+cos(x))/2) or cos(x/2)=-sqrt((1+cos(x))/2); theorem :: SIN_COS5:28 sin(x/2)<>0 implies tan(x/2)=(1-cos(x))/sin(x); theorem :: SIN_COS5:29 cos(x/2)<>0 implies tan(x/2)=sin(x)/(1+cos(x)); theorem :: SIN_COS5:30 tan(x/2)=sqrt((1-cos(x))/(1+cos(x))) or tan(x/2)=-sqrt((1-cos(x))/(1+ cos(x))); theorem :: SIN_COS5:31 cos(x/2)<>0 implies cot(x/2)=(1+cos(x))/sin(x); theorem :: SIN_COS5:32 sin(x/2)<>0 implies cot(x/2)=sin(x)/(1-cos(x)); theorem :: SIN_COS5:33 cot(x/2) = sqrt((1+cos(x))/(1-cos(x))) or cot(x/2) =-sqrt((1+cos(x))/( 1-cos(x))); theorem :: SIN_COS5:34 sin(x/2)<>0 & cos(x/2)<>0 & 1-(tan(x/2))^2<>0 implies sec(x/2)= sqrt(( 2*sec(x))/(sec(x)+1)) or sec(x/2)=-sqrt((2*sec(x))/(sec(x)+1)); theorem :: SIN_COS5:35 sin(x/2)<>0 & cos(x/2)<>0 & 1-(tan(x/2))^2<>0 implies cosec(x/2)= sqrt ((2*sec(x))/(sec(x)-1)) or cosec(x/2)=-sqrt((2*sec(x))/(sec(x)-1)); definition let x be Real; func coth(x) -> Real equals :: SIN_COS5:def 1 cosh(x)/sinh(x); func sech(x) -> Real equals :: SIN_COS5:def 2 1/cosh(x); func cosech(x) -> Real equals :: SIN_COS5:def 3 1/sinh(x); end; theorem :: SIN_COS5:36 coth(x)=(exp_R(x)+exp_R(-x))/(exp_R(x)-exp_R(-x)) & sech(x)=2/( exp_R(x)+exp_R(-x)) & cosech(x)=2/(exp_R(x)-exp_R(-x)); theorem :: SIN_COS5:37 exp_R(x)-exp_R(-x)<>0 implies tanh(x)*coth(x)=1; theorem :: SIN_COS5:38 (sech(x))^2+(tanh(x))^2=1; theorem :: SIN_COS5:39 sinh x <> 0 implies (coth x)^2-(cosech x)^2=1; theorem :: SIN_COS5:40 sinh(x1)<>0 & sinh(x2)<>0 implies coth(x1+x2)=(1+coth(x1)*coth( x2))/(coth(x1)+coth(x2)); theorem :: SIN_COS5:41 sinh(x1)<>0 & sinh(x2)<>0 implies coth(x1-x2)=(1-coth(x1)*coth(x2))/( coth(x1)-coth(x2)); theorem :: SIN_COS5:42 sinh(x1)<>0 & sinh(x2)<>0 implies coth(x1)+coth(x2)=sinh(x1+x2)/(sinh( x1)*sinh(x2)) & coth(x1)-coth(x2)=-(sinh(x1-x2))/(sinh(x1)*sinh(x2)); theorem :: SIN_COS5:43 sinh(3*x)=3*sinh(x)+4*(sinh(x))|^3; theorem :: SIN_COS5:44 cosh(3*x)=4*(cosh(x))|^3-3*cosh(x); theorem :: SIN_COS5:45 sinh(x)<>0 implies coth(2*x)=(1+(coth(x))^2)/(2*coth(x)); theorem :: SIN_COS5:46 x >= 0 implies sinh x >= 0; theorem :: SIN_COS5:47 x<=0 implies sinh x<=0; theorem :: SIN_COS5:48 cosh(x/2)=sqrt((cosh(x)+1)/2); theorem :: SIN_COS5:49 sinh(x/2)<>0 implies tanh(x/2)=(cosh(x)-1)/(sinh(x)); theorem :: SIN_COS5:50 cosh(x/2)<>0 implies tanh(x/2)=(sinh(x))/(cosh(x)+1); theorem :: SIN_COS5:51 sinh(x/2)<>0 implies coth(x/2)=(sinh(x))/(cosh(x)-1); theorem :: SIN_COS5:52 cosh(x/2)<>0 implies coth(x/2)=(cosh(x)+1)/(sinh(x));