:: Formulas And Identities of Trigonometric Functions
:: by Yuzhong Ding and Xiquan Liang
::
:: Received March 18, 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 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;
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;