:: 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; equalities SQUARE_1, SIN_COS4; theorems XCMPLX_1, SIN_COS, SIN_COS4, SQUARE_1, NEWTON, ABSVALUE, SIN_COS2, COMPLEX1, XREAL_1, XXREAL_0; begin reserve x,x1,x2,x3 for Real; theorem Th1: cos(x)<>0 implies cosec(x)=sec(x)/tan(x) proof assume A1: cos(x)<>0; then sec(x)/tan(x)=((1/cos(x))*cos(x))/((sin(x)/cos(x))*cos(x)) by XCMPLX_1:91 .=1/((sin(x)/cos(x))*cos(x)) by A1,XCMPLX_1:87 .=1/sin(x) by A1,XCMPLX_1:87; hence thesis; end; theorem Th2: sin(x)<>0 implies cos(x) = sin(x)*cot(x) proof assume sin(x)<>0; then cos(x)= (sin(x)/sin(x))*cos(x) by XCMPLX_1:88 .= sin(x)*cot(x) by XCMPLX_1:75; hence thesis; end; theorem 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) proof assume that A1: sin(x1)<>0 and A2: sin(x2)<>0 and A3: sin(x3)<>0; sin(x1+x2+x3) = sin(x1+(x2+x3)) .=sin(x1)*cos(x2+x3)+cos(x1)*sin(x2+x3) by SIN_COS:75 .=sin(x1)*(cos(x2)*cos(x3)-sin(x2)*sin(x3)) + cos(x1)*sin(x2+x3) by SIN_COS:75 .=sin(x1)*(cos(x2)*cos(x3))-sin(x1)*(sin(x2)*sin(x3)) +cos(x1)*(sin(x2)* cos(x3)+cos(x2)*sin(x3)) by SIN_COS:75 .=sin(x1)*cos(x2)*cos(x3)-sin(x1)*sin(x2)*sin(x3) +(cos(x1)*sin(x2)*cos( x3)+cos(x1)*cos(x2)*sin(x3)) .=sin(x1)*(sin(x2)*cot(x2))*cos(x3)-sin(x1)*sin(x2)*sin(x3) +(cos(x1)* sin(x2)*cos(x3)+cos(x1)*cos(x2)*sin(x3)) by A2,Th2 .=sin(x1)*(sin(x2)*cot(x2))*(sin(x3)*cot(x3))-sin(x1)*sin(x2) *sin(x3)+( cos(x1)*sin(x2)*cos(x3)+cos(x1)*cos(x2)*sin(x3)) by A3,Th2 .=(sin(x1)*sin(x2)*sin(x3))*(cot(x2)*cot(x3)-1)+((sin(x1)*cot(x1) )*sin( x2)*cos(x3)+cos(x1)*cos(x2)*sin(x3)) by A1,Th2 .=(sin(x1)*sin(x2)*sin(x3))*(cot(x2)*cot(x3)-1)+((sin(x1)*cot(x1) )*sin( x2)*(sin(x3)*cot(x3))+cos(x1)*cos(x2)*sin(x3)) by A3,Th2 .=(sin(x1)*sin(x2)*sin(x3))*(cot(x2)*cot(x3)-1)+sin(x1)*sin(x2 )*sin(x3) *cot(x1)*cot(x3)+cos(x1)*cos(x2)*sin(x3) .=(sin(x1)*sin(x2)*sin(x3))*((cot(x2)*cot(x3)-1)+cot(x1)*cot(x3)) +(sin( x1)*cot(x1))*cos(x2)*sin(x3) by A1,Th2 .=(sin(x1)*sin(x2)*sin(x3))*((cot(x2)*cot(x3)-1)+cot(x1)*cot(x3)) +(sin( x1)*cot(x1))*(sin(x2)*cot(x2))*sin(x3) by A2,Th2 .=(sin(x1)*sin(x2)*sin(x3))*(cot(x2)*cot(x3)+cot(x1)*cot(x3) +cot(x1)* cot(x2)-1); hence thesis; end; theorem 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)) proof assume that A1: sin(x1)<>0 and A2: sin(x2)<>0 and A3: sin(x3)<>0; cos(x1+x2+x3)=cos(x1+(x2+x3)) .=cos(x1)*cos(x2+x3)-sin(x1)*sin(x2+x3) by SIN_COS:75 .=cos(x1)*(cos(x2)*cos(x3)-sin(x2)*sin(x3))-sin(x1)*sin(x2+x3) by SIN_COS:75 .=cos(x1)*(cos(x2)*cos(x3))-cos(x1)*(sin(x2)*sin(x3)) -(sin(x1))*(sin(x2 )*cos(x3)+cos(x2)*sin(x3)) by SIN_COS:75 .=cos(x1)*cos(x2)*cos(x3)-cos(x1)*sin(x2)*sin(x3)-(sin(x1) *sin(x2)*cos( x3)+sin(x1)*sin(x3)*cos(x2)) .=cos(x1)*cos(x2)*cos(x3)-cos(x1)*sin(x2)*sin(x3)-(sin(x1) *sin(x2)*(sin (x3)*cot(x3))+sin(x1)*sin(x3)*cos(x2)) by A3,Th2 .=cos(x1)*cos(x2)*cos(x3)-cos(x1)*sin(x2)*sin(x3)-(sin(x1) *sin(x2)*(sin (x3)*cot(x3))+sin(x1)*sin(x3)*(sin(x2)*cot(x2))) by A2,Th2 .=sin(x1)*cot(x1)*cos(x2)*cos(x3)-cos(x1)*sin(x2)*sin(x3)-(sin(x1) *sin( x2)*sin(x3))*(cot(x3)+cot(x2)) by A1,Th2 .=sin(x1)*cot(x1)*(sin(x2)*cot(x2))*cos(x3)-cos(x1)*sin(x2) *sin(x3)-( sin(x1)*sin(x2)*sin(x3))*(cot(x3)+cot(x2)) by A2,Th2 .=sin(x1)*cot(x1)*(sin(x2)*cot(x2))*(sin(x3)*cot(x3))-cos(x1) *sin(x2)* sin(x3)-(sin(x1)*sin(x2)*sin(x3))*(cot(x3)+cot(x2)) by A3,Th2 .=sin(x1)*sin(x2)*sin(x3)*(cot(x1)*cot(x2)*cot(x3))-sin(x1)*cot(x1) *sin (x2)*sin(x3)-(sin(x1)*sin(x2)*sin(x3))*(cot(x3)+cot(x2)) by A1,Th2 .=-sin(x1)*sin(x2)*sin(x3)*(cot(x1)+cot(x2)+cot(x3)-cot(x1) *cot(x2)*cot (x3)); hence thesis; end; theorem Th5: sin(2*x) = 2*sin(x)*cos(x) proof sin(2*x)=sin(x+x) .=sin(x)*cos(x)+cos(x)*sin(x) by SIN_COS:75 .=2*sin(x)*cos(x); hence thesis; end; theorem Th6: cos(x)<>0 implies sin(2*x)=(2*tan(x))/(1+(tan(x))^2) proof assume A1: cos(x)<>0; then A2: (cos(x))^2<>0 by SQUARE_1:12; sin(2*x)=2*sin(x)*cos(x)*1 by Th5 .=2*sin(x)*cos(x)*(cos(x)/cos(x)) by A1,XCMPLX_1:60 .=2*sin(x)*cos(x)*cos(x)/cos(x) by XCMPLX_1:74 .=2*(cos(x))^2*sin(x)/cos(x) .=2*(cos(x))^2*tan(x)/1 by XCMPLX_1:74 .=2*tan(x)*(cos(x))^2/((sin(x))^2+(cos(x))^2) by SIN_COS:29 .=2*tan(x)/(((sin(x))^2+(cos(x))^2)/(cos(x))^2) by XCMPLX_1:77 .=2*tan(x)/((sin(x))^2/(cos(x))^2+(cos(x))^2/(cos(x))^2) by XCMPLX_1:62 .=2*tan(x)/((sin(x))^2/(cos(x))^2+1) by A2,XCMPLX_1:60 .=2*tan(x)/((tan x)^2+1) by XCMPLX_1:76; hence thesis; end; theorem Th7: 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 proof A1: cos(2*x) = cos(x+x) .=(cos(x))^2 -(sin(x))^2 by SIN_COS:75; then cos(2*x)=(cos(x))^2 -(sin(x))^2-1+1 .=(cos(x))^2 -(sin(x))^2-((cos(x))^2+(sin(x))^2)+1 by SIN_COS:29 .=-(-1+ 2*(sin(x))^2); hence thesis by A1; end; theorem Th8: cos(x)<>0 implies cos(2*x)=(1-(tan(x))^2)/(1+(tan(x))^2) proof assume cos(x)<>0; then A1: (cos(x))^2<>0 by SQUARE_1:12; cos(2*x) = ((cos(x))^2-(sin(x))^2)*1 by Th7 .=((cos(x))^2-(sin(x))^2)*((cos(x))^2/(cos(x))^2) by A1,XCMPLX_1:60 .=((cos(x))^2-(sin(x))^2)/(cos(x))^2*(cos(x))^2 by XCMPLX_1:75 .=((cos(x))^2/(cos(x))^2-(sin(x))^2/(cos(x))^2)*(cos(x))^2 by XCMPLX_1:120 .=(1-(sin(x))^2/(cos(x))^2)*(cos(x))^2 by A1,XCMPLX_1:60 .=(1-(tan(x))^2)*(cos(x))^2/1 by XCMPLX_1:76 .=(1-(tan(x))^2)*(cos(x))^2/((cos(x))^2+(sin(x))^2) by SIN_COS:29 .=(1-(tan(x))^2)/(((cos(x))^2+(sin(x))^2)/(cos(x))^2) by XCMPLX_1:77 .=(1-(tan(x))^2)/(((cos(x))^2/(cos(x))^2+(sin(x))^2/(cos(x))^2)) by XCMPLX_1:62 .=(1-(tan(x))^2)/((1+(sin(x))^2/(cos(x))^2)) by A1,XCMPLX_1:60 .=(1-(tan(x))^2)/((1+(tan(x))^2)) by XCMPLX_1:76; hence thesis; end; theorem cos(x)<>0 implies tan(2*x)=(2*tan(x))/(1-(tan(x))^2) proof assume A1: cos(x)<>0; tan(2*x) = tan(x+x) .=(tan(x)+tan(x))/(1-tan(x)*tan(x)) by A1,SIN_COS4:7 .=(2*tan(x))/(1-tan(x)*tan(x)); hence thesis; end; theorem sin(x)<>0 implies cot(2*x)=((cot(x))^2-1)/(2*cot(x)) proof assume A1: sin(x)<>0; cot(2*x)=cot(x+x) .=(cot(x)*cot(x)-1)/(cot(x)+cot(x)) by A1,SIN_COS4:9 .=(cot(x)*cot(x)-1)/(2*cot(x)); hence thesis; end; theorem Th11: cos(x)<>0 implies (sec x)^2 = 1 + (tan x)^2 proof assume cos(x)<>0; then A1: (cos(x))^2 <>0 by SQUARE_1:12; (sec(x))^2=1^2/(cos(x))^2 by XCMPLX_1:76 .=((sin(x))^2+(cos(x))^2)/(cos(x))^2 by SIN_COS:29 .=(sin(x))^2/(cos(x))^2+(cos(x))^2/(cos(x))^2 by XCMPLX_1:62 .=(sin(x))^2/(cos(x))^2+1 by A1,XCMPLX_1:60 .=(sin(x)/cos(x))^2+1 by XCMPLX_1:76; hence thesis; end; theorem cot(x) = 1/tan(x) by XCMPLX_1:57; theorem Th13: 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)) proof assume that A1: cos(x)<>0 and A2: sin(x)<>0; A3: sec(2*x)=1/((1-(tan(x))^2)/(1+(tan(x))^2)) by A1,Th8 .=(1+(tan(x))^2)/(1-(tan(x))^2) by XCMPLX_1:57 .=((sec(x))^2)/(1-(tan(x))^2) by A1,Th11; then sec(2*x)=(1+(tan(x))^2)/(1-(tan(x))^2) by A1,Th11 .=((1+(tan(x))^2)/tan(x))/((1-(tan(x))^2)/tan(x)) by A1,A2,XCMPLX_1:50,55 .=(1/tan(x)+(tan(x))^2/tan(x))/((1-(tan(x))^2)/tan(x)) by XCMPLX_1:62 .=(cot(x)+(tan(x))^2/tan(x))/((1-(tan(x))^2)/tan(x)) by XCMPLX_1:57 .=(cot(x)+(tan(x))^2/tan(x))/(1/tan(x)-(tan(x))^2/tan(x)) by XCMPLX_1:120 .=(cot(x)+tan(x)*tan(x)/tan(x))/(cot(x)-(tan(x))^2/tan(x)) by XCMPLX_1:57 .=(cot(x)+tan(x))/(cot(x)-tan(x)*tan(x)/tan(x)) by A1,A2,XCMPLX_1:50,89; hence thesis by A1,A2,A3,XCMPLX_1:50,89; end; theorem sin(x)<>0 implies (cosec(x))^2 = 1 +(cot(x))^2 proof assume sin(x)<>0; then A1: (sin(x))^2 <>0 by SQUARE_1:12; (cosec(x))^2=1^2/(sin(x))^2 by XCMPLX_1:76 .=((sin(x))^2+(cos(x))^2)/(sin(x))^2 by SIN_COS:29 .=(sin(x))^2/(sin(x))^2+(cos(x))^2/(sin(x))^2 by XCMPLX_1:62 .=1+(cos(x))^2/(sin(x))^2by A1,XCMPLX_1:60 .=1+(cos(x)/sin(x))^2 by XCMPLX_1:76; hence thesis; end; theorem cos(x)<>0 & sin(x)<>0 implies cosec(2*x)=sec(x)*cosec(x)/2 & cosec(2*x )=(tan(x)+cot(x))/2 proof assume that A1: cos(x)<>0 and A2: sin(x)<>0; A3: cosec(2*x)=1/((2*tan(x))/(1+(tan(x))^2)) by A1,Th6 .=(1+(tan(x))^2)/(2*tan(x)) by XCMPLX_1:57 .=(1+(tan(x))^2)/tan(x)/2 by XCMPLX_1:78 .=(1/(sin(x)/cos(x))+(tan(x))^2/tan(x))/2 by XCMPLX_1:62 .=(cot(x)+tan(x)*tan(x)/tan(x))/2 by XCMPLX_1:57 .=(cot(x)+tan(x))/2 by A1,A2,XCMPLX_1:50,89; cosec(2*x)=1/((2*tan(x))/(1+(tan(x))^2)) by A1,Th6 .=(1+(tan(x))^2)/(2*tan(x)) by XCMPLX_1:57 .=(sec(x))^2/(2*tan(x)) by A1,Th11 .=sec(x)*sec(x)/tan(x)/2 by XCMPLX_1:78 .=sec(x)*(sec(x)/(sin(x)/cos(x)))/2 by XCMPLX_1:74 .=sec(x)*(sec(x)*cos(x)/sin(x))/2 by XCMPLX_1:77 .=sec(x)*cosec(x)/2 by A1,XCMPLX_1:106; hence thesis by A3; end; theorem Th16: sin(3*x)=-4*(sin(x))|^3+3*sin(x) proof sin(3*x)=sin((x+x)+x) .=sin(2*x)*cos(x)+cos(x+x)*sin(x) by SIN_COS:75 .=(2*sin(x)*cos(x))*cos(x)+cos(2*x)*sin(x) by Th5 .=2*sin(x)*(cos(x)*cos(x))+(1-2*(sin(x))^2)*sin(x) by Th7 .=2*sin(x)*(1-(sin(x))^2)+(1-2*(sin(x))^2)*sin(x) by SIN_COS4:5 .=2*sin(x)*1-2*sin(x)*(sin(x)*sin(x))+(1*sin(x)-2*(sin(x))^2*sin(x)) .=2*sin(x)*1-2*((sin(x))|^1*(sin(x)))*sin(x) +(1*sin(x)-2*(sin(x))^2*sin (x)) .=2*sin(x)*1-2*((sin(x))|^(1+1))*sin(x) +(1*sin(x)-2*(sin(x))^2*sin(x)) by NEWTON:6 .=2*sin(x)*1-2*((sin(x))|^2*sin(x)) +(1*sin(x)-2*(sin(x))^2*sin(x)) .=2*sin(x)*1-2*(sin(x))|^(2+1) +(1*sin(x)-2*(sin(x))^2*sin(x)) by NEWTON:6 .=2*sin(x)-2*(sin(x))|^3+(sin(x)-2* ((sin(x))|^1*sin(x))*sin(x)) .=2*sin(x)-2*(sin(x))|^3+(sin(x)-2*((sin(x))|^(1+1))*sin(x)) by NEWTON:6 .=2*sin(x)-2*(sin(x))|^3+(sin(x)-2*((sin(x))|^(1+1)*sin(x))) .=2*sin(x)-2*(sin(x))|^3+(sin(x)-2*((sin(x))|^(2+1))) by NEWTON:6 .=-(-3*sin(x)+4*(sin(x))|^3); hence thesis; end; theorem Th17: cos(3*x)=4*(cos(x))|^3-3*cos(x) proof cos(3*x)=cos((x+x)+x) .=cos(2*x)*cos(x)-sin(x+x)*sin(x) by SIN_COS:75 .=(2*(cos(x))^2-1)*cos(x)-sin(2*x)*sin(x) by Th7 .=2*(cos(x)*cos(x)*cos(x))-1*cos(x)-sin(2*x)*sin(x) .=2*((cos(x))|^1*cos(x)*cos(x))-1*cos(x)-sin(2*x)*sin(x) .=2*((cos(x))|^(1+1)*cos(x))-1*cos(x)-sin(2*x)*sin(x) by NEWTON:6 .=2*((cos(x))|^(2+1))-cos(x)-sin(2*x)*sin(x) by NEWTON:6 .=2*(cos(x))|^3-cos(x)-(2*sin(x)*cos(x))*sin(x) by Th5 .=2*(cos(x))|^3-cos(x)-2*cos(x)*(sin(x)*sin(x)) .=2*(cos(x))|^3-cos(x)-2*cos(x)*(1-cos(x)*cos(x)) by SIN_COS4:4 .=2*(cos(x))|^3-cos(x)-(2*cos(x)-2*(cos(x)*cos(x)*cos(x))) .=2*(cos(x))|^3-cos(x)-(2*cos(x)-2*((cos(x))|^1*cos(x)*cos(x))) .=2*(cos(x))|^3-cos(x)-(2*cos(x)-2*((cos(x))|^(1+1)*cos(x))) by NEWTON:6 .=2*(cos(x))|^3-cos(x)-(2*cos(x)-2*((cos(x))|^(2+1))) by NEWTON:6 .=2*(cos(x))|^3+2*(cos(x))|^3-3*cos(x); hence thesis; end; theorem cos(x)<>0 implies tan(3*x)=(3*tan(x)-(tan(x))|^3)/(1-3*(tan(x))^2) proof assume A1: cos(x)<>0; tan(3*x)=tan(x+x+x) .=(tan(x)+tan(x)+tan(x)-tan(x)*tan(x)*tan(x)) /(1-tan(x)*tan(x)-tan(x)* tan(x)-tan(x)*tan(x)) by A1,SIN_COS4:13 .=(3*tan(x)-(tan(x))|^1*tan(x)*tan(x))/(1-3*tan(x)*tan(x)) .=(3*tan(x)-(tan(x))|^(1+1)*tan(x))/(1-3*tan(x)*tan(x)) by NEWTON:6 .=(3*tan(x)-(tan(x))|^(2+1))/(1-3*(tan(x)*tan(x))) by NEWTON:6; hence thesis; end; theorem sin(x)<>0 implies cot(3*x)=((cot(x))|^3-3*cot(x))/(3*(cot(x))^2-1) proof assume A1: sin(x)<>0; cot(3*x)=cot(x+x+x) .=(cot(x)*cot(x)*cot(x)-cot(x)-cot(x)-cot(x)) /(cot(x)*cot(x)+cot(x)*cot (x)+cot(x)*cot(x)-1) by A1,SIN_COS4:14 .=(cot(x)*cot(x)*cot(x)-3*cot(x))/(3*(cot(x))^2-1) .=((cot(x))|^1*cot(x)*cot(x)-3*cot(x))/(3*(cot(x))^2-1) .=((cot(x))|^(1+1)*cot(x)-3*cot(x))/(3*(cot(x))^2-1) by NEWTON:6 .=((cot(x))|^(2+1)-3*cot(x))/(3*(cot(x))^2-1) by NEWTON:6; hence thesis; end; theorem (sin(x))^2=(1-cos(2*x))/2 proof (1-cos(2*x))/2=(1-(1-2*(sin(x))^2))/2 by Th7 .=(sin(x))^2*2/2; hence thesis; end; theorem (cos(x))^2=(1+cos(2*x))/2 proof (1+cos(2*x))/2=(1+(2*(cos(x))^2-1))/2 by Th7 .=(cos(x))^2*2/2; hence thesis; end; theorem (sin(x))|^3=(3*sin(x)-sin(3*x))/4 proof (3*sin(x)-sin(3*x))/4=(3*sin(x)-(-4*(sin(x))|^3+3*sin(x)))/4 by Th16 .=(4*(sin(x))|^3)/4; hence thesis; end; theorem (cos(x))|^3=(3*cos(x)+cos(3*x))/4 proof (3*cos(x)+cos(3*x))/4 =(3*cos(x)+(4*(cos(x))|^3 - 3*cos(x)))/4 by Th17 .=(4*(cos(x))|^3)/4; hence thesis; end; theorem (sin(x))|^4=(3-4*cos(2*x)+cos(4*x))/8 proof (3-4*cos(2*x)+cos(2*2*x))/8 =(3-4*cos(2*x)+cos(2*(2*x)))/8 .=(3-4*cos(2*x)+(1-2*(sin(2*x))^2))/8 by Th7 .=(3-4*cos(2*x)+(1-2*(2*sin(x)*cos(x))^2))/8 by Th5 .=(3-4*(1-2*(sin(x))^2)+(1-8*(sin(x))^2*(cos(x))^2))/8 by Th7 .=(sin(x))^2*(1-cos(x)*cos(x)) .=sin(x)*sin(x)*(sin(x)*sin(x)) by SIN_COS4:4 .=(sin(x))|^1*sin(x)*(sin(x)*sin(x)) .=(sin(x))|^(1+1)*(sin(x)*sin(x)) by NEWTON:6 .=(sin(x))|^(1+1)*sin(x)*sin(x) .=(sin(x))|^(2+1)*sin(x) by NEWTON:6 .=(sin(x))|^(3+1) by NEWTON:6; hence thesis; end; theorem (cos(x))|^4 = (3+4*cos(2*x)+cos(4*x))/8 proof (3+4*cos(2*x)+cos(4*x))/8 =(3+4*cos(2*x)+cos(2*(2*x)))/8 .=(3+4*cos(2*x)+(1-2*(sin(2*x))^2))/8 by Th7 .=(3+4*cos(2*x)+(1-2*(2*sin(x)*cos(x))^2))/8 by Th5 .=(3+4*(1-2*(sin(x))^2)+(1-8*(sin(x))^2*(cos(x))^2))/8 by Th7 .=1-(sin(x)*sin(x))*(1+(cos(x))^2) .=1-(1^2-(cos(x))^2)*(1^2+(cos(x))^2) by SIN_COS4:4 .=cos(x)*cos(x)*cos(x)*cos(x) .=(cos(x))|^1*cos(x)*cos(x)*cos(x) .=(cos(x))|^(1+1)*cos(x)*cos(x) by NEWTON:6 .=(cos(x))|^(2+1)*cos(x) by NEWTON:6 .=(cos(x))|^(3+1) by NEWTON:6; hence thesis; end; :: Half Angle theorem sin(x/2)=sqrt((1-cos(x))/2) or sin(x/2)=-sqrt((1-cos(x))/2) proof A1: sqrt((1-cos(x))/2)=sqrt((1-cos(2*(x/2)))/2) .=sqrt((1-(1-2*(sin(x/2))^2))/2) by Th7 .=|.sin(x/2).| by COMPLEX1:72; per cases; suppose sin(x/2)>=0; hence thesis by A1,ABSVALUE:def 1; end; suppose sin(x/2)<0; then sqrt((1-cos(x))/2)*(-1)=(-sin(x/2))*(-1) by A1,ABSVALUE:def 1; hence thesis; end; end; theorem cos(x/2)=sqrt((1+cos(x))/2) or cos(x/2)=-sqrt((1+cos(x))/2) proof A1: sqrt((1+cos(x))/2)=sqrt((1+cos(2*(x/2)))/2) .=sqrt((1+(2*(cos(x/2))^2-1))/2) by Th7 .=|.cos(x/2).| by COMPLEX1:72; per cases; suppose cos(x/2)>=0; hence thesis by A1,ABSVALUE:def 1; end; suppose cos(x/2)<0; then sqrt((1+cos(x))/2)*(-1)=(-cos(x/2))*(-1) by A1,ABSVALUE:def 1; hence thesis; end; end; theorem sin(x/2)<>0 implies tan(x/2)=(1-cos(x))/sin(x) proof assume sin(x/2)<>0; then A1: 2*sin(x/2)<>0; (1-cos(x))/sin(x)=(1-(1-2*(sin(x/2))^2))/sin(2*(x/2)) by Th7 .=(2*sin(x/2)*sin(x/2))/(2*sin(x/2)*cos(x/2)) by Th5 .=tan(x/2) by A1,XCMPLX_1:91; hence thesis; end; theorem cos(x/2)<>0 implies tan(x/2)=sin(x)/(1+cos(x)) proof assume cos(x/2)<>0; then A1: 2*cos(x/2)<>0; sin(x)/(1+cos(x))=(2*sin(x/2)*cos(x/2))/(1+cos(2*(x/2))) by Th5 .=(2*sin(x/2)*cos(x/2))/(1+(2*(cos(x/2))^2-1)) by Th7 .=(2*cos(x/2)*sin(x/2))/(2*cos(x/2)*cos(x/2)) .=(sin(x/2))/(cos(x/2)) by A1,XCMPLX_1:91; hence thesis; end; theorem tan(x/2)=sqrt((1-cos(x))/(1+cos(x))) or tan(x/2)=-sqrt((1-cos(x))/(1+ cos(x))) proof A1: sqrt((1-cos(x))/(1+cos(x))) =sqrt((1-(1-2*(sin(x/2))^2))/(1+cos(2*(x/2)) )) by Th7 .=sqrt((1-1+2*(sin(x/2))^2)/(1+(2*(cos(x/2))^2-1))) by Th7 .=sqrt((sin(x/2))^2/(cos(x/2))^2) by XCMPLX_1:91 .=sqrt((tan(x/2))^2) by XCMPLX_1:76 .=|.tan(x/2).| by COMPLEX1:72; per cases; suppose tan(x/2)>=0; hence thesis by A1,ABSVALUE:def 1; end; suppose tan(x/2)<0; then sqrt((1-cos(x))/(1+cos(x)))*(-1) =(-tan(x/2))*(-1) by A1, ABSVALUE:def 1; hence thesis; end; end; theorem cos(x/2)<>0 implies cot(x/2)=(1+cos(x))/sin(x) proof assume cos(x/2)<>0; then A1: 2*cos(x/2)<>0; (1+cos(x))/sin(x)=(1+(2*(cos(x/2))^2-1))/sin(2*(x/2)) by Th7 .=(2*(cos(x/2)*cos(x/2)))/(2*sin(x/2)*cos(x/2)) by Th5 .=(2*cos(x/2)*cos(x/2))/(2*cos(x/2)*sin(x/2)) .=cot(x/2) by A1,XCMPLX_1:91; hence thesis; end; theorem sin(x/2)<>0 implies cot(x/2)=sin(x)/(1-cos(x)) proof assume sin(x/2)<>0; then A1: 2*sin(x/2)<>0; sin(x)/(1-cos(x))=(2*sin(x/2)*cos(x/2))/(1-cos(2*(x/2))) by Th5 .=(2*sin(x/2)*cos(x/2))/(1-(1-2*(sin(x/2))^2)) by Th7 .=(2*sin(x/2)*cos(x/2))/(2*sin(x/2)*sin(x/2)) .=(cos(x/2))/(sin(x/2)) by A1,XCMPLX_1:91; hence thesis; end; theorem cot(x/2) = sqrt((1+cos(x))/(1-cos(x))) or cot(x/2) =-sqrt((1+cos(x))/( 1-cos(x))) proof A1: sqrt((1+cos(x))/(1-cos(x))) =sqrt((1+(2*(cos(x/2))^2-1))/(1-cos(2*(x/2)) )) by Th7 .=sqrt((1-(1-2*(cos(x/2))^2))/(1-(1-2*(sin(x/2))^2))) by Th7 .=sqrt((cos(x/2))^2/(sin(x/2))^2) by XCMPLX_1:91 .=sqrt((cot(x/2))^2) by XCMPLX_1:76 .=|.cot(x/2).| by COMPLEX1:72; per cases; suppose cot(x/2)>=0; hence thesis by A1,ABSVALUE:def 1; end; suppose cot(x/2)<0; then sqrt((1+cos(x))/(1-cos(x)))*(-1) =(-cot(x/2))*(-1) by A1, ABSVALUE:def 1; hence thesis; end; end; theorem 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)) proof assume that A1: sin(x/2)<>0 and A2: cos(x/2)<>0 and A3: 1-(tan(x/2))^2<>0; set b=(sec(x/2))^2; set a=1-(tan(x/2))^2; A4: a+b=(1+(tan(x/2))^2)+(1-(tan(x/2))^2) by A2,Th11 .=1+1; sqrt((2*sec(x))/(sec(x)+1)) =sqrt((2*((sec(x/2))^2/(1-(tan(x/2))^2)))/( sec(2*(x/2))+1)) by A1,A2,Th13 .=sqrt((2*((sec(x/2))^2/(1-(tan(x/2))^2))) /(((sec(x/2))^2/(1-(tan(x/2)) ^2))+1)) by A1,A2,Th13; then A5: sqrt((2*sec(x))/(sec(x)+1))=sqrt(((2*(b/a))*a)/((b/a+1)*a)) by A3, XCMPLX_1:91 .=sqrt((2*((b/a)*a))/(b/a*a+1*a)) .=sqrt((2*((b/a)*a))/(b+a)) by A3,XCMPLX_1:87 .=sqrt(2*b/2) by A3,A4,XCMPLX_1:87 .=|.sec(x/2).| by COMPLEX1:72; per cases; suppose sec(x/2)>=0; hence thesis by A5,ABSVALUE:def 1; end; suppose sec(x/2)<0; then sqrt((2*sec(x))/(sec(x)+1))*(-1) =(-sec(x/2))*(-1) by A5, ABSVALUE:def 1; hence thesis; end; end; theorem 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)) proof assume that A1: sin(x/2)<>0 and A2: cos(x/2)<>0 and A3: 1-(tan(x/2))^2<>0; set b=(sec(x/2))^2; set a=1-(tan(x/2))^2; A4: b-a=(1+(tan(x/2))^2)-(1-(tan(x/2))^2) by A2,Th11 .=2*(tan(x/2))^2; sqrt((2*sec(x))/(sec(x)-1)) =sqrt((2*((sec(x/2))^2/(1-(tan(x/2))^2)))/( sec(2*(x/2))-1)) by A1,A2,Th13 .=sqrt((2*((sec(x/2))^2/(1-(tan(x/2))^2))) /(((sec(x/2))^2/(1-(tan(x/2)) ^2))-1)) by A1,A2,Th13; then A5: sqrt((2*sec(x))/(sec(x)-1))=sqrt(((2*(b/a))*a)/((b/a-1)*a)) by A3, XCMPLX_1:91 .=sqrt((2*((b/a)*a))/(b/a*a-1*a)) .=sqrt((2*((b/a)*a))/(b-a)) by A3,XCMPLX_1:87 .=sqrt(2*b/(2*(tan(x/2))^2)) by A3,A4,XCMPLX_1:87 .=sqrt((sec(x/2))^2/(tan(x/2))^2) by XCMPLX_1:91 .=sqrt((sec(x/2)/(tan(x/2)))^2) by XCMPLX_1:76 .=sqrt((cosec(x/2))^2) by A2,Th1 .=|.cosec(x/2).| by COMPLEX1:72; per cases; suppose cosec(x/2)>=0; hence thesis by A5,ABSVALUE:def 1; end; suppose cosec(x/2)<0; then sqrt((2*sec(x))/(sec(x)-1))*(-1) =(-cosec(x/2))*(-1) by A5, ABSVALUE:def 1; hence thesis; end; end; definition let x be Real; func coth(x) -> Real equals cosh(x)/sinh(x); coherence; func sech(x) -> Real equals 1/cosh(x); coherence; func cosech(x) -> Real equals 1/sinh(x); coherence; end; theorem Th36: 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)) proof A1: sech(x)=1/cosh.x by SIN_COS2:def 4 .=1/((exp_R.(x)+exp_R.(-x))/2) by SIN_COS2:def 3 .=1*2/((exp_R.(x)+exp_R.(-x))/2*2) by XCMPLX_1:91 .=2/(exp_R.(x)+exp_R(-x)) by SIN_COS:def 23 .=2/(exp_R(x)+exp_R(-x)) by SIN_COS:def 23; A2: cosech(x)=1/sinh.x by SIN_COS2:def 2 .=1/((exp_R.(x)-exp_R.(-x))/2) by SIN_COS2:def 1 .=1*2/((exp_R.(x)-exp_R.(-x))/2*2) by XCMPLX_1:91 .=2/(exp_R.(x)-exp_R(-x)) by SIN_COS:def 23; coth(x)=cosh.x/sinh(x) by SIN_COS2:def 4 .=cosh.x/sinh.x by SIN_COS2:def 2 .=((exp_R.(x)+exp_R.(-x))/2)/sinh.x by SIN_COS2:def 3 .=((exp_R.(x)+exp_R.(-x))/2)/((exp_R.(x)-exp_R.(-x))/2) by SIN_COS2:def 1 .=((exp_R.(x)+exp_R.(-x))/2*2)/((exp_R.(x)-exp_R.(-x))/2*2) by XCMPLX_1:91 .=(exp_R.(x)+exp_R.(-x))/(exp_R.(x)-exp_R(-x)) by SIN_COS:def 23 .=(exp_R.(x)+exp_R.(-x))/(exp_R(x)-exp_R(-x)) by SIN_COS:def 23 .=(exp_R.(x)+exp_R(-x))/(exp_R(x)-exp_R(-x)) by SIN_COS:def 23 .=(exp_R(x)+exp_R(-x))/(exp_R(x)-exp_R(-x)) by SIN_COS:def 23; hence thesis by A1,A2,SIN_COS:def 23; end; theorem exp_R(x)-exp_R(-x)<>0 implies tanh(x)*coth(x)=1 proof assume A1: exp_R(x)-exp_R(-x)<>0; exp_R(x)>0 by SIN_COS:55; then A2: exp_R(x) + exp_R(-x)>0+0 by SIN_COS:55,XREAL_1:8; tanh(x)*coth(x)=tanh.x*coth(x) by SIN_COS2:def 6 .=(exp_R.x-exp_R.(-x))/(exp_R.x+exp_R.(-x))*coth(x) by SIN_COS2:def 5 .=(exp_R.x-exp_R.(-x))/(exp_R.x+exp_R.(-x))* ((exp_R(x)+exp_R(-x))/( exp_R(x)-exp_R(-x))) by Th36 .=(exp_R.x-exp_R.(-x))/(exp_R.x+exp_R(-x))* ((exp_R(x)+exp_R(-x))/(exp_R (x)-exp_R(-x))) by SIN_COS:def 23 .=(exp_R(x)-exp_R.(-x))/(exp_R.x+exp_R(-x))* ((exp_R(x)+exp_R(-x))/( exp_R(x)-exp_R(-x))) by SIN_COS:def 23 .=(exp_R(x)-exp_R(-x))/(exp_R.x+exp_R(-x))* ((exp_R(x)+exp_R(-x))/(exp_R (x)-exp_R(-x))) by SIN_COS:def 23 .=(exp_R(x)-exp_R(-x))/(exp_R(x)+exp_R(-x))* ((exp_R(x)+exp_R(-x))/( exp_R(x)-exp_R(-x))) by SIN_COS:def 23 .=(exp_R(x)-exp_R(-x))/(exp_R(x)+exp_R(-x))* (exp_R(x)+exp_R(-x))/(exp_R (x)-exp_R(-x)) by XCMPLX_1:74; then tanh(x)*coth(x) =(exp_R(x)-exp_R(-x))/(exp_R(x)-exp_R(-x)) by A2, XCMPLX_1:87 .=1 by A1,XCMPLX_1:60; hence thesis; end; theorem (sech(x))^2+(tanh(x))^2=1 proof cosh.x <>0 by SIN_COS2:15; then A1: (cosh.x)^2<>0 by SQUARE_1:12; (sech(x))^2+(tanh(x))^2 =(1/cosh(x))^2 + (tanh.x)^2 by SIN_COS2:def 6 .=(1/cosh.(x))^2+(tanh.(x))^2 by SIN_COS2:def 4 .=(1^2/(cosh.(x))^2)+(tanh.(x))^2 by XCMPLX_1:76 .=(1^2/(cosh.(x))^2)+(sinh.(x)/cosh.(x))^2 by SIN_COS2:17 .=(1/(cosh.(x))^2)+((sinh.(x))^2/(cosh.(x))^2) by XCMPLX_1:76 .=(1+(sinh.(x))^2)/(cosh.(x))^2 by XCMPLX_1:62 .=((cosh.x)^2-(sinh.x)^2+(sinh.(x))^2)/(cosh.(x))^2 by SIN_COS2:14 .=(cosh.x)^2/(cosh.(x))^2; hence thesis by A1,XCMPLX_1:60; end; theorem sinh x <> 0 implies (coth x)^2-(cosech x)^2=1 proof assume sinh(x)<>0; then A1: (sinh x)^2<>0 by SQUARE_1:12; (coth x)^2-(cosech x)^2 =(cosh(x))^2/(sinh(x))^2-(1/sinh(x))^2 by XCMPLX_1:76 .=(cosh(x))^2/(sinh(x))^2-1^2/(sinh(x))^2 by XCMPLX_1:76 .=((cosh(x))^2-1)/(sinh(x))^2 by XCMPLX_1:120 .=((cosh(x))^2-((cosh.x)^2-(sinh.x)^2))/(sinh(x))^2 by SIN_COS2:14 .=((cosh(x))^2-(cosh.x)^2+(sinh.x)^2)/(sinh(x))^2 .=((cosh(x))^2-(cosh(x))^2+(sinh.x)^2)/(sinh(x))^2 by SIN_COS2:def 4 .=(0+(sinh(x))^2)/(sinh(x))^2 by SIN_COS2:def 2; hence thesis by A1,XCMPLX_1:60; end; Lm1: coth(-x)=-coth(x) proof coth(-x)=cosh.(-x)/sinh(-x) by SIN_COS2:def 4 .=cosh.(-x)/sinh.(-x) by SIN_COS2:def 2 .=cosh.(x)/sinh.(-x) by SIN_COS2:19 .=cosh.(x)/(-sinh.(x)) by SIN_COS2:19 .=-cosh.(x)/sinh.(x) by XCMPLX_1:188 .= - cosh(x)/sinh.(x) by SIN_COS2:def 4 .=-coth(x) by SIN_COS2:def 2; hence thesis; end; theorem Th40: sinh(x1)<>0 & sinh(x2)<>0 implies coth(x1+x2)=(1+coth(x1)*coth( x2))/(coth(x1)+coth(x2)) proof assume that A1: sinh(x1)<>0 and A2: sinh(x2)<>0; A3: sinh.(x1)<>0 by A1,SIN_COS2:def 2; A4: sinh.(x2)<>0 by A2,SIN_COS2:def 2; coth(x1+x2)=cosh.(x1+x2)/sinh(x1+x2) by SIN_COS2:def 4 .=cosh.(x1+x2)/sinh.(x1+x2) by SIN_COS2:def 2 .=((cosh.x1)*(cosh.x2) + (sinh.x1)*(sinh.x2)) /sinh.(x1+x2) by SIN_COS2:20 .=((cosh.x1)*(cosh.x2) + (sinh.x1)*(sinh.x2)) /((sinh.x1)*(cosh.x2) + ( cosh.x1)*(sinh.x2)) by SIN_COS2:21 .=(((cosh.x1)*(cosh.x2) + (sinh.x1)*(sinh.x2))/((sinh.x1)*(sinh.x2))) /( ((sinh.x1)*(cosh.x2) + (cosh.x1)*(sinh.x2))/((sinh.x1)*(sinh.x2))) by A3,A4, XCMPLX_1:6,55 .=(((cosh.x1)*(cosh.x2)/((sinh.x1)*(sinh.x2))) + (sinh.x1)*(sinh.x2)/(( sinh.x1)*(sinh.x2))) /(((sinh.x1)*(cosh.x2) + (cosh.x1)*(sinh.x2))/((sinh.x1)*( sinh.x2))) by XCMPLX_1:62 .=(((cosh.x1)*(cosh.x2)/((sinh.x1)*(sinh.x2)))+ 1) /(((sinh.x1)*(cosh.x2 )+(cosh.x1)*(sinh.x2))/((sinh.x1)*(sinh.x2))) by A3,A4,XCMPLX_1:6,60 .=(((cosh.x1)/(sinh.x1)*(cosh.x2)/(sinh.x2))+ 1) /(((sinh.x1)*(cosh.x2)+ (cosh.x1)*(sinh.x2))/((sinh.x1)*(sinh.x2))) by XCMPLX_1:83 .=(((cosh.x1)/(sinh.x1)*((cosh.x2)/(sinh.x2)))+ 1) /(((sinh.x1)*(cosh.x2 )+(cosh.x1)*(sinh.x2))/((sinh.x1)*(sinh.x2))) by XCMPLX_1:74 .=(((cosh.x1)/(sinh.x1))*((cosh.x2)/(sinh.x2))+ 1)/(((sinh.x1) *(cosh.x2 ))/((sinh.x1)*(sinh.x2))+((cosh.x1)*(sinh.x2))/((sinh.x1) *(sinh.x2))) by XCMPLX_1:62 .=(((cosh.x1)/(sinh.x1))*((cosh.x2)/(sinh.x2))+ 1)/(((sinh.x1)/(sinh.x1) *(cosh.x2))/(sinh.x2)+((cosh.x1)*(sinh.x2))/((sinh.x1) *(sinh.x2))) by XCMPLX_1:83 .=(((cosh.x1)/(sinh.x1))*((cosh.x2)/(sinh.x2))+ 1)/(((sinh.x1)/(sinh.x1) *(cosh.x2))/(sinh.x2)+((cosh.x1)/(sinh.x1)*(sinh.x2))/( (sinh.x2))) by XCMPLX_1:83 .=(((cosh.x1)/(sinh.x1))*((cosh.x2)/(sinh.x2))+ 1)/(1* cosh.x2/sinh.x2+( (cosh.x1)/(sinh.x1)*(sinh.x2))/( (sinh.x2))) by A3,XCMPLX_1:60 .=(((cosh.x1)/(sinh.x1))*((cosh.x2)/(sinh.x2))+ 1)/( cosh.x2/sinh.x2+ cosh.x1/sinh.x1) by A4,XCMPLX_1:89 .=(((cosh(x1))/(sinh.x1))*((cosh.x2)/(sinh.x2))+ 1)/( cosh.x2/sinh.x2+ cosh.x1/sinh.x1) by SIN_COS2:def 4 .=(((cosh(x1))/(sinh.x1))*((cosh(x2))/(sinh.x2))+ 1)/( cosh.x2/sinh.x2+ cosh.x1/sinh.x1) by SIN_COS2:def 4 .=(((cosh(x1))/(sinh.x1))*((cosh(x2))/(sinh.x2))+ 1)/( cosh(x2)/sinh.x2+ cosh.x1/sinh.x1) by SIN_COS2:def 4 .=(((cosh(x1))/(sinh.x1))*((cosh(x2))/(sinh.x2))+ 1)/( cosh(x2)/sinh.x2+ cosh(x1)/sinh.x1) by SIN_COS2:def 4 .=(((cosh(x1))/(sinh(x1)))*((cosh(x2))/(sinh.x2))+ 1)/( cosh(x2)/sinh.x2 +cosh(x1)/sinh.x1) by SIN_COS2:def 2 .=(((cosh(x1))/(sinh(x1)))*((cosh(x2))/(sinh.x2))+ 1)/( cosh(x2)/sinh(x2 )+cosh(x1)/sinh.x1) by SIN_COS2:def 2 .=(((cosh(x1))/(sinh(x1)))*((cosh(x2))/(sinh.x2))+ 1)/( cosh(x2)/sinh(x2 )+cosh(x1)/sinh(x1)) by SIN_COS2:def 2 .=(coth(x1)*coth(x2)+ 1)/(coth(x2)+coth(x1)) by SIN_COS2:def 2; hence thesis; end; theorem sinh(x1)<>0 & sinh(x2)<>0 implies coth(x1-x2)=(1-coth(x1)*coth(x2))/( coth(x1)-coth(x2)) proof assume that A1: sinh(x1)<>0 and A2: sinh(x2)<>0; -sinh.(x2)<>0 by A2,SIN_COS2:def 2; then sinh.(-x2)<>0 by SIN_COS2:19; then A3: sinh(-x2)<>0 by SIN_COS2:def 2; coth(x1-x2)=coth(x1+(-x2)) .=(1+coth(x1)*coth(-x2))/(coth(x1)+coth(-x2)) by A1,A3,Th40 .=(1+coth(x1)*(-coth(x2)))/(coth(x1)+coth(-x2)) by Lm1 .=(1-coth(x1)*(coth(x2)))/(coth(x1)+-coth(x2)) by Lm1 .=(1-coth(x1)*(coth(x2)))/(coth(x1)-coth(x2)); hence thesis; end; theorem 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)) proof assume that A1: sinh(x1)<>0 and A2: sinh(x2)<>0; A3: sinh.(x1)<>0 by A1,SIN_COS2:def 2; A4: sinh.(x2)<>0 by A2,SIN_COS2:def 2; A5: -(sinh(x1-x2))/(sinh(x1)*sinh(x2)) =-(sinh.(x1-x2))/(sinh(x1)*sinh(x2)) by SIN_COS2:def 2 .=-(sinh.(x1-x2))/(sinh.(x1)*sinh(x2)) by SIN_COS2:def 2 .=-(sinh.(x1-x2))/(sinh.(x1)*sinh.(x2)) by SIN_COS2:def 2 .=-((sinh.x1)*(cosh.x2)-(cosh.x1)*(sinh.x2))/(sinh.(x1)*sinh.(x2)) by SIN_COS2:21 .=-((sinh.x1)*(cosh.x2)/(sinh.(x1)*sinh.(x2)) -(cosh.x1)*(sinh.x2)/(sinh .(x1)*sinh.(x2))) by XCMPLX_1:120 .=-((sinh.x1)/sinh.(x1)*(cosh.x2)/(sinh.(x2)) -(cosh.x1)*(sinh.x2)/(sinh .(x1)*sinh.(x2))) by XCMPLX_1:83 .=-((sinh.x1)/sinh.(x1)*(cosh.x2)/(sinh.(x2)) -((sinh.x2)/sinh.(x2)*cosh .x1)/(sinh.(x1))) by XCMPLX_1:83 .=-(1*(cosh.x2)/(sinh.(x2)) -((sinh.x2)/sinh.(x2)*cosh.x1)/(sinh.(x1))) by A3,XCMPLX_1:60 .=-(cosh.x2/(sinh.(x2))-(1*cosh.x1)/(sinh.(x1))) by A4,XCMPLX_1:60 .=-(cosh(x2)/(sinh.(x2))-(cosh.x1)/(sinh.(x1))) by SIN_COS2:def 4 .=-(cosh(x2)/(sinh.(x2))-(cosh(x1))/(sinh.(x1))) by SIN_COS2:def 4 .=-(cosh(x2)/(sinh(x2))-(cosh(x1))/(sinh.(x1))) by SIN_COS2:def 2 .=-(coth(x2)-(cosh(x1))/(sinh(x1))) by SIN_COS2:def 2 .=coth(x1)-coth(x2); sinh(x1+x2)/(sinh(x1)*sinh(x2)) =sinh.(x1+x2)/(sinh(x1)*sinh(x2)) by SIN_COS2:def 2 .=((sinh.x1)*(cosh.x2)+(cosh.x1)*(sinh.x2))/(sinh(x1)*sinh(x2)) by SIN_COS2:21 .=((sinh.x1)*(cosh.x2)+(cosh.x1)*(sinh.x2))/(sinh.(x1)*sinh(x2)) by SIN_COS2:def 2 .=((sinh.x1)*(cosh.x2)+(cosh.x1)*(sinh.x2))/(sinh.(x1)*sinh.(x2)) by SIN_COS2:def 2 .=(sinh.x1)*(cosh.x2)/(sinh.(x1)*sinh.(x2)) +(cosh.x1)*(sinh.x2)/(sinh.( x1)*sinh.(x2)) by XCMPLX_1:62 .=(sinh.x1)/sinh.(x1)*(cosh.x2)/(sinh.(x2)) +(cosh.x1)*(sinh.x2)/(sinh.( x1)*sinh.(x2)) by XCMPLX_1:83 .=1*(cosh.x2)/(sinh.(x2)) +(cosh.x1)*(sinh.x2)/(sinh.(x1)*sinh.(x2)) by A3, XCMPLX_1:60 .=(cosh.x2)/(sinh.(x2)) +(cosh.x1)/sinh.(x1)*(sinh.x2)/(sinh.(x2)) by XCMPLX_1:83 .=(cosh.x2)/(sinh.(x2)) +(cosh.x1)/sinh.(x1)*((sinh.x2)/(sinh.(x2))) by XCMPLX_1:74 .=(cosh.x2)/(sinh.(x2)) +(cosh.x1)/sinh.(x1)*1 by A4,XCMPLX_1:60 .=(cosh.x2)/(sinh.(x2)) +(cosh.x1)/sinh(x1) by SIN_COS2:def 2 .=(cosh.x2)/(sinh(x2)) +(cosh.x1)/sinh(x1) by SIN_COS2:def 2 .=cosh(x2)/(sinh(x2)) +(cosh.x1)/sinh(x1) by SIN_COS2:def 4 .=coth(x2)+coth(x1) by SIN_COS2:def 4; hence thesis by A5; end; Lm2: (cosh.x)^2=1+(sinh.x)^2 proof (cosh.x)^2-(sinh.x)^2+(sinh.x)^2=1+(sinh.x)^2 by SIN_COS2:14; hence thesis; end; Lm3: (cosh.x)^2-1=(sinh.x)^2 proof (cosh.x)^2-(sinh.x)^2+(sinh.x)^2=1+(sinh.x)^2 by SIN_COS2:14; hence thesis; end; theorem sinh(3*x)=3*sinh(x)+4*(sinh(x))|^3 proof sinh(3*x)=sinh.(x+x+x) by SIN_COS2:def 2 .=(sinh.(2*x))*(cosh.x) + (cosh.(2*x))*(sinh.x) by SIN_COS2:21 .=2*sinh.x*cosh.x*(cosh.x) + (cosh.(2*x))*(sinh.x) by SIN_COS2:23 .=2*sinh.x*(cosh.x)^2+(2*(cosh.x)^2-1)*(sinh.x) by SIN_COS2:23 .=2*sinh.x*(1+(sinh.x)^2)+(2*(cosh.x)^2-1)*(sinh.x) by Lm2 .=2*sinh.x*(1+(sinh.x)^2)+(2*(1+(sinh.x)^2)-1)*(sinh.x) by Lm2 .=2*sinh.x+(2+2)*sinh.x*(sinh.x)^2+sinh.x .=2*sinh.x+4*(sinh.x)|^1*(sinh.x)^2+sinh.x .=3*sinh.x+4*((sinh.x)|^1*sinh.x*sinh.x) .=3*sinh.x+4*((sinh.x)|^(1+1)*sinh.x) by NEWTON:6 .=3*sinh.x+4*(sinh.x)|^(2+1) by NEWTON:6 .=3*sinh(x)+4*(sinh.x)|^3 by SIN_COS2:def 2; hence thesis by SIN_COS2:def 2; end; theorem cosh(3*x)=4*(cosh(x))|^3-3*cosh(x) proof cosh(3*x)=cosh.(x+x+x) by SIN_COS2:def 4 .=(cosh.(2*x))*(cosh.x) + (sinh.(2*x))*(sinh.x) by SIN_COS2:20 .=(2*(cosh.x)^2-1)*(cosh.x)+(sinh.(2*x))*(sinh.x) by SIN_COS2:23 .=(2*(cosh.x)^2-1)*(cosh.x)+(2*(sinh.x)*(cosh.x))*(sinh.x) by SIN_COS2:23 .=(2*(cosh.x)^2-1)*cosh.x+2*(sinh.x)^2*cosh.x .=(2*(cosh.x)^2-1)*cosh.x+2*((cosh.x)^2-1)*cosh.x by Lm3 .=4*(cosh.x*cosh.x*cosh.x)-3*cosh.x .=4*((cosh.x)|^1*cosh.x*cosh.x)-3*cosh.x .=4*((cosh.x)|^(1+1)*cosh.x)-3*cosh.x by NEWTON:6 .=4*((cosh.x)|^(2+1))-3*cosh.x by NEWTON:6 .=4*(cosh.x)|^3-3*cosh(x) by SIN_COS2:def 4; hence thesis by SIN_COS2:def 4; end; theorem sinh(x)<>0 implies coth(2*x)=(1+(coth(x))^2)/(2*coth(x)) proof assume sinh(x)<>0; then A1: sinh.x<>0 by SIN_COS2:def 2; then A2: (sinh.(x))^2 <>0 by SQUARE_1:12; coth(2*x)=cosh.(2*x)/sinh(2*x) by SIN_COS2:def 4 .=cosh.(2*x)/sinh.(2*x) by SIN_COS2:def 2 .=(2*(cosh.x)^2 - 1)/sinh.(2*x) by SIN_COS2:23 .=(2*(cosh.x)^2 - 1)/(2*(sinh.x)*(cosh.x)) by SIN_COS2:23 .=((2*(cosh.x)^2 - 1)/(sinh.(x))^2)/((2*(sinh.x)*(cosh.x))/ (sinh.(x))^2 ) by A2,XCMPLX_1:55 .=((2*(cosh.x)^2-((cosh.x)^2-(sinh.x)^2))/(sinh.(x))^2)/((2* (sinh.x)*( cosh.x))/(sinh.(x))^2) by SIN_COS2:14 .=(((2-1)*(cosh.x)^2+(sinh.x)^2)/(sinh.(x))^2)/((2* (sinh.x)*(cosh.x))/( sinh.(x))^2) .=((cosh.x)^2/(sinh.(x))^2+(sinh.x)^2/(sinh.(x))^2)/((2* (sinh.x)*(cosh. x))/(sinh.(x))^2) by XCMPLX_1:62 .=((cosh.x/sinh.x)^2+(sinh.x)^2/(sinh.(x))^2)/((2* (sinh.x)*(cosh.x))/( sinh.(x))^2) by XCMPLX_1:76 .=((cosh.x/sinh.x)^2+(sinh.x/sinh.x)^2)/((2* (sinh.x)*(cosh.x))/(sinh.(x ))^2) by XCMPLX_1:76 .=((cosh.x/sinh.x)^2+1^2)/(2*cosh.x*sinh.x/(sinh.x*sinh.x)) by A1, XCMPLX_1:60 .=((cosh.x/sinh.x)^2+1)/(2*cosh.x*sinh.x/sinh.x/sinh.x) by XCMPLX_1:78 .=((cosh.x/sinh.x)^2+1)/(2*cosh.x/sinh.x) by A1,XCMPLX_1:89 .=((cosh.x/sinh.x)^2+1)/(2*(cosh.x/sinh.x)) by XCMPLX_1:74 .=((cosh(x)/sinh.x)^2+1)/(2*(cosh.(x)/sinh.x)) by SIN_COS2:def 4 .=((cosh(x)/sinh.x)^2+1)/(2*(cosh(x)/sinh.x)) by SIN_COS2:def 4 .=((cosh(x)/sinh(x))^2+1)/(2*(cosh(x)/sinh.x)) by SIN_COS2:def 2 .=((coth(x))^2+1)/(2*(cosh(x)/sinh(x))) by SIN_COS2:def 2; hence thesis; end; Lm4: x>0 implies sinh x>=0 proof assume A1: x>0; then x+(-x)>0+(-x) by XREAL_1:8; then A2: exp_R.(-x)<=1 by SIN_COS:53; exp_R.x>=1 by A1,SIN_COS:52; then exp_R.(x)-exp_R.(-x)>=1-1 by A2,XREAL_1:13; then (exp_R.(x)-exp_R.(-x))/2>=0 by XREAL_1:136; then sinh.(x)>=0 by SIN_COS2:def 1; hence thesis by SIN_COS2:def 2; end; theorem x >= 0 implies sinh x >= 0 proof assume A1: x >= 0; per cases by A1,XXREAL_0:1; suppose x > 0; hence thesis by Lm4; end; suppose x = 0; hence thesis by SIN_COS2:16,def 2; end; end; theorem x<=0 implies sinh x<=0 proof assume A1: x<=0; per cases by A1,XXREAL_0:1; suppose A2: x < 0; then -x>0 by XREAL_1:58; then A3: exp_R.(-x)>=1 by SIN_COS:52; exp_R.x<=1 by A2,SIN_COS:53; then exp_R.x-exp_R.(-x)<=1-1 by A3,XREAL_1:13; then (exp_R.x-exp_R.(-x))/2<=0 by XREAL_1:138; then sinh.x<=0 by SIN_COS2:def 1; hence thesis by SIN_COS2:def 2; end; suppose x = 0; hence thesis by SIN_COS2:16,def 2; end; end; theorem cosh(x/2)=sqrt((cosh(x)+1)/2) proof A1: cosh.(x/2)>0 by SIN_COS2:15; sqrt((cosh(x)+1)/2) = sqrt((cosh.(2*(x/2))+1)/2) by SIN_COS2:def 4 .= sqrt((2*(cosh.(x/2))^2 - 1 +1)/2) by SIN_COS2:23 .= cosh.(x/2) by A1,SQUARE_1:22; hence thesis by SIN_COS2:def 4; end; theorem sinh(x/2)<>0 implies tanh(x/2)=(cosh(x)-1)/(sinh(x)) proof assume sinh(x/2)<>0; then A1: 2*sinh.(x/2)<>0 by SIN_COS2:def 2; (cosh(x)-1)/(sinh(x))=(cosh.(2*(x/2))-1)/(sinh(2*(x/2))) by SIN_COS2:def 4 .=(2*(cosh.(x/2))^2-1-1)/(sinh(2*(x/2))) by SIN_COS2:23 .=(2*((cosh.(x/2))^2-1))/(sinh(2*(x/2))) .=(2*(sinh.(x/2))^2)/(sinh(2*(x/2))) by Lm3 .=(2*(sinh.(x/2))^2)/(sinh.(2*(x/2))) by SIN_COS2:def 2 .=(2*sinh.(x/2)*sinh.(x/2))/(2*sinh.(x/2)*cosh.(x/2)) by SIN_COS2:23 .=sinh.(x/2)/cosh.(x/2) by A1,XCMPLX_1:91 .=tanh.(x/2) by SIN_COS2:17 .=tanh(x/2) by SIN_COS2:def 6; hence thesis; end; theorem cosh(x/2)<>0 implies tanh(x/2)=(sinh(x))/(cosh(x)+1) proof assume cosh(x/2)<>0; then A1: 2*cosh.(x/2)<>0 by SIN_COS2:def 4; (sinh(x))/(cosh(x)+1)=(sinh.(2*(x/2)))/(cosh(2*(x/2))+1) by SIN_COS2:def 2 .=(sinh.(2*(x/2)))/(cosh.(2*(x/2))+1) by SIN_COS2:def 4 .=(2*sinh.(x/2)*cosh.(x/2))/(cosh.(2*(x/2))+1) by SIN_COS2:23 .=(2*sinh.(x/2)*cosh.(x/2))/(2*(cosh.(x/2))^2-1+1) by SIN_COS2:23 .=(2*cosh.(x/2)*sinh.(x/2))/(2*cosh.(x/2)*cosh.(x/2)) .=sinh.(x/2)/cosh.(x/2) by A1,XCMPLX_1:91 .=tanh.(x/2) by SIN_COS2:17; hence thesis by SIN_COS2:def 6; end; theorem sinh(x/2)<>0 implies coth(x/2)=(sinh(x))/(cosh(x)-1) proof assume sinh(x/2)<>0; then A1: 2*sinh.(x/2)<>0 by SIN_COS2:def 2; (sinh(x))/(cosh(x)-1)=(sinh.(2*(x/2)))/(cosh(2*(x/2))-1) by SIN_COS2:def 2 .=(sinh.(2*(x/2)))/(cosh.(2*(x/2))-1) by SIN_COS2:def 4 .=(2*sinh.(x/2)*cosh.(x/2))/(cosh.(2*(x/2))-1) by SIN_COS2:23 .=(2*sinh.(x/2)*cosh.(x/2))/(2*(cosh.(x/2))^2-1-1) by SIN_COS2:23 .=(2*sinh.(x/2)*cosh.(x/2))/(2*((cosh.(x/2))^2-1)) .=(2*sinh.(x/2)*cosh.(x/2))/(2*(sinh.(x/2))^2) by Lm3 .=(2*sinh.(x/2)*cosh.(x/2))/(2*sinh.(x/2)*sinh.(x/2)) .=cosh.(x/2)/sinh.(x/2) by A1,XCMPLX_1:91 .=cosh(x/2)/sinh.(x/2) by SIN_COS2:def 4 .=cosh(x/2)/sinh(x/2) by SIN_COS2:def 2; hence thesis; end; theorem cosh(x/2)<>0 implies coth(x/2)=(cosh(x)+1)/(sinh(x)) proof assume cosh(x/2)<>0; then A1: 2*cosh.(x/2)<>0 by SIN_COS2:def 4; (cosh(x)+1)/(sinh(x))=(cosh.(2*(x/2))+1)/(sinh(2*(x/2))) by SIN_COS2:def 4 .=(2*(cosh.(x/2))^2-1+1)/(sinh(2*(x/2))) by SIN_COS2:23 .=(2*(cosh.(x/2))^2)/(sinh.(2*(x/2))) by SIN_COS2:def 2 .=(2*(cosh.(x/2)*cosh.(x/2)))/(2*sinh.(x/2)*cosh.(x/2)) by SIN_COS2:23 .=(2*cosh.(x/2)*cosh.(x/2))/(2*cosh.(x/2)*sinh.(x/2)) .=cosh.(x/2)/sinh.(x/2) by A1,XCMPLX_1:91 .=cosh(x/2)/sinh.(x/2) by SIN_COS2:def 4 .=cosh(x/2)/sinh(x/2) by SIN_COS2:def 2; hence thesis; end;