:: Formulas and Identities of Hyperbolic Functions
:: by Pacharapokin Chanapat and Hiroshi Yamazaki
::
:: Received November 7, 2005
:: Copyright (c) 2005-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, SUBSET_1, SIN_COS2, XXREAL_0, CARD_1, FUNCT_1, SIN_COS,
ARYTM_1, ARYTM_3, SQUARE_1, RELAT_1, SIN_COS5, NEWTON, REAL_1;
notations ORDINAL1, SUBSET_1, FUNCT_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0,
SQUARE_1, NEWTON, SIN_COS, SIN_COS2, SIN_COS5;
constructors REAL_1, SQUARE_1, NAT_1, BINOP_2, SIN_COS, SIN_COS2, SIN_COS5,
VALUED_1, NEWTON;
registrations XREAL_0, SQUARE_1, NAT_1, SIN_COS, VALUED_0, RELSET_1, SIN_COS2,
NEWTON, ORDINAL1;
requirements REAL, NUMERALS, SUBSET, ARITHM;
equalities SQUARE_1;
theorems XREAL_1, SQUARE_1, SIN_COS, NEWTON, XCMPLX_1, SIN_COS2, SIN_COS5,
POLYEQ_2, SIN_COS7, TAYLOR_1;
begin :: Hyperbolic sine, hyperbolic cosine and hyperbolic tangent
reserve x, y, z, w for Real;
reserve n for Element of NAT;
Lm1: cosh x >= 1 & cosh 0 = 1 & sinh 0 = 0
proof
cosh.x >= 1 by SIN_COS2:37;
hence thesis by SIN_COS2:15,16,def 2,def 4;
end;
Lm2: sinh x = (exp_R(x)-exp_R(-x))/2 & cosh x = (exp_R(x)+exp_R(-x))/2 & tanh
x = (exp_R(x)-exp_R(-x))/(exp_R(x)+exp_R(-x))
proof
A1: sinh x = sinh.x by SIN_COS2:def 2
.=(exp_R.x-exp_R.-x)/2 by SIN_COS2:def 1
.=(exp_R(x)-exp_R.-x)/2 by SIN_COS:def 23
.=(exp_R(x)-exp_R(-x))/2 by SIN_COS:def 23;
A2: cosh x = cosh.x by SIN_COS2:def 4
.=(exp_R.x+exp_R.-x)/2 by SIN_COS2:def 3
.=(exp_R(x)+exp_R.-x)/2 by SIN_COS:def 23
.=(exp_R(x)+exp_R(-x))/2 by SIN_COS:def 23;
tanh x = tanh.x by SIN_COS2:def 6
.= sinh.x/cosh.x by SIN_COS2:17
.= sinh(x)/cosh.x by SIN_COS2:def 2
.= (exp_R(x)-exp_R(-x))/2/((exp_R(x)+exp_R(-x))/2) by A1,A2,SIN_COS2:def 4;
hence thesis by A1,A2,XCMPLX_1:55;
end;
Lm3: (cosh x)^2-(sinh x)^2 = 1 & cosh(x)*cosh(x)-sinh(x)*sinh(x) = 1
proof
(cosh x)^2-(sinh x)^2 = (cosh x)^2-(sinh.x)^2 by SIN_COS2:def 2
.= (cosh.x)^2-(sinh.x)^2 by SIN_COS2:def 4
.= 1 by SIN_COS2:14;
hence thesis;
end;
theorem Th1:
tanh x = sinh(x)/cosh(x) & tanh 0 = 0
proof
A1: tanh 0 = tanh.0 by SIN_COS2:def 6
.= sinh.0/cosh.0 by SIN_COS2:17
.= 0 by SIN_COS2:16;
tanh(x) = tanh.x by SIN_COS2:def 6
.= sinh.x/cosh.x by SIN_COS2:17
.= sinh(x)/cosh.x by SIN_COS2:def 2
.= sinh(x)/cosh(x) by SIN_COS2:def 4;
hence thesis by A1;
end;
Lm4: x <> 0 implies sinh x <> 0 & tanh x <> 0
proof
A1: exp_R(x) > 0 by SIN_COS:55;
assume x <> 0;
then 1/exp_R(x) <> exp_R(x) by A1,SIN_COS7:29,XCMPLX_1:199;
then (exp_R(x) - exp_R(-x))/2 <> 0 by TAYLOR_1:4;
then
A2: sinh(x) <> 0 by Lm2;
cosh(x) <> 0 by Lm1;
then sinh(x)/cosh(x) <> 0 by A2,XCMPLX_1:50;
hence thesis by Th1;
end;
Lm5: y-z <> 0 implies sinh(y/2-z/2) <> 0
proof
assume y-z <> 0;
then (y-z)/2 <> 0;
hence thesis by Lm4;
end;
Lm6: y+z <> 0 implies sinh(y/2+z/2) <> 0
proof
assume y+z <> 0;
then (y+z)/2 <> 0;
hence thesis by Lm4;
end;
Lm7: (sinh x)^2 = 1/2*(cosh(2*x) - 1) & (cosh x)^2 = 1/2*(cosh(2*x) + 1)
proof
A1: (cosh x)^2 = (cosh.x)^2 by SIN_COS2:def 4
.=1/2*(cosh.(2*x)+1) by SIN_COS2:18;
(sinh x)^2 = (sinh.x)^2 by SIN_COS2:def 2
.=1/2*(cosh.(2*x)-1) by SIN_COS2:18
.=1/2*(cosh(2*x)-1) by SIN_COS2:def 4;
hence thesis by A1,SIN_COS2:def 4;
end;
Lm8: sinh(-x) = -sinh x & cosh(-x) = cosh(x) & tanh(-x) = -tanh x & coth(-x) =
-coth(x) & sech(-x) = sech x & cosech(-x) = -cosech(x)
proof
A1: tanh(-x) = tanh.-x by SIN_COS2:def 6
.= -tanh.x by SIN_COS2:19
.= -tanh x by SIN_COS2:def 6;
A2: sinh(-x) = sinh.-x by SIN_COS2:def 2
.= -sinh.x by SIN_COS2:19
.= -sinh x by SIN_COS2:def 2;
then
A3: cosech(-x) = 1/(-sinh(x)) by SIN_COS5:def 3
.= -(1/sinh x) by XCMPLX_1:188
.= -cosech x by SIN_COS5:def 3;
A4: cosh(-x) = cosh.-x by SIN_COS2:def 4
.= cosh.x by SIN_COS2:19
.= cosh x by SIN_COS2:def 4;
then
A5: sech(-x) = 1/cosh(x) by SIN_COS5:def 2
.= sech x by SIN_COS5:def 2;
coth(-x) = cosh(x)/-sinh(x) by A2,A4,SIN_COS5:def 1
.= -(cosh(x)/sinh(x)) by XCMPLX_1:188
.= -coth x by SIN_COS5:def 1;
hence thesis by A2,A4,A1,A5,A3;
end;
theorem Th2:
sinh x = 1/cosech x & cosh x = 1/sech x & tanh x = 1/coth x
proof
A1: sinh x = 1/(1/sinh x) by XCMPLX_1:56
.= 1/cosech x by SIN_COS5:def 3;
A2: cosh x = 1/(1/cosh x) by XCMPLX_1:56
.= 1/sech(x) by SIN_COS5:def 2;
tanh x = sinh(x)/cosh(x) by Th1
.= 1/(cosh(x)/sinh(x)) by XCMPLX_1:57
.= 1/coth x by SIN_COS5:def 1;
hence thesis by A1,A2;
end;
Lm9: exp_R(x)+exp_R(-x) >= 2
proof
exp_R.x >= 0 by SIN_COS:54;
then
A1: exp_R(x) >= 0 by SIN_COS:def 23;
exp_R.-x >= 0 by SIN_COS:54;
then
A2: exp_R(-x) >= 0 by SIN_COS:def 23;
2*sqrt(exp_R(x)*exp_R(-x)) =2*sqrt(exp_R(x)*exp_R.-x) by SIN_COS:def 23
.=2*sqrt(exp_R.x*exp_R.-x) by SIN_COS:def 23
.=2*sqrt(exp_R.(x+-x)) by SIN_COS2:12
.=2*1 by SIN_COS:51,def 23,SQUARE_1:18;
hence thesis by A1,A2,SIN_COS2:1;
end;
theorem Th3:
sech x <= 1 & 0 < sech x & sech 0 = 1
proof
A1: 2/2 >= 2/(exp_R(x)+exp_R(-x)) by Lm9,XREAL_1:183;
0 < cosh.x by SIN_COS2:15;
then 0 < cosh x by SIN_COS2:def 4;
then
A2: 0 < 1/cosh(x) by XREAL_1:139;
sech 0 = 1/1 by Lm1,SIN_COS5:def 2
.= 1;
hence thesis by A2,A1,SIN_COS5:36,def 2;
end;
theorem
x >= 0 implies tanh x >= 0
proof
A1: cosh(x) >= 1 by Lm1;
assume
A2: x >= 0;
per cases by A2;
suppose
x > 0;
then sinh(x) >= 0 by SIN_COS5:46;
then sinh(x)/cosh(x) >= 0 by A1;
hence thesis by Th1;
end;
suppose
x = 0;
hence thesis by Th1;
end;
end;
theorem
cosh x = 1/sqrt (1-(tanh x)^2) & sinh x = tanh(x)/sqrt (1-(tanh x)^2)
proof
A1: (sech x)^2 = (sech x)^2+(tanh x)^2-(tanh x)^2
.= 1-(tanh x)^2 by SIN_COS5:38;
A2: sech x > 0 by Th3;
A3: cosh x = 1/(1/cosh x) by XCMPLX_1:56
.= 1/sech(x) by SIN_COS5:def 2
.= 1/sqrt (1-(tanh x)^2) by A1,A2,SQUARE_1:22;
cosh x <> 0 by Lm1;
then sinh x = sinh(x)/cosh(x)*cosh(x) by XCMPLX_1:87
.= tanh(x)*(1/sqrt (1-(tanh x)^2)) by A3,Th1
.= tanh(x)/sqrt (1-(tanh x)^2) by XCMPLX_1:99;
hence thesis by A3;
end;
theorem
(cosh(x)+sinh(x)) |^ n = cosh(n*x)+sinh(n*x) & (cosh(x)-sinh(x)) |^ n
= cosh(n*x)-sinh(n*x)
proof
A1: (cosh(x) + sinh(x)) |^ n = (cosh.x+sinh(x)) |^ n by SIN_COS2:def 4
.= (cosh.x+sinh.x) |^ n by SIN_COS2:def 2
.= cosh.(n*x)+sinh.(n*x) by SIN_COS2:29
.= cosh(n*x)+sinh.(n*x) by SIN_COS2:def 4
.= cosh(n*x)+sinh(n*x) by SIN_COS2:def 2;
(cosh(x) - sinh(x)) |^ n = (cosh(x)+-sinh(x)) |^ n
.= (cosh(x)+sinh(-x)) |^ n by Lm8
.= (cosh.x+sinh(-x)) |^ n by SIN_COS2:def 4
.= (cosh.x+sinh.-x) |^ n by SIN_COS2:def 2
.= (cosh.-x+sinh.-x) |^ n by SIN_COS2:19
.= cosh.(n*-x)+sinh.(-n*x) by SIN_COS2:29
.= cosh.(n*x)+sinh.(-n*x) by SIN_COS2:19
.= cosh.(n*x)+-sinh.(n*x) by SIN_COS2:19
.= cosh.(n*x)-sinh.(n*x)
.= cosh(n*x)-sinh.(n*x) by SIN_COS2:def 4
.= cosh(n*x)-sinh(n*x) by SIN_COS2:def 2;
hence thesis by A1;
end;
theorem Th7:
exp_R(x) = cosh(x)+sinh(x) & exp_R(-x) = cosh(x)-sinh(x) & exp_R(
x) = (cosh(x/2)+sinh(x/2))/(cosh(x/2)-sinh(x/2)) & exp_R(-x) = (cosh(x/2)-sinh(
x/2))/(cosh(x/2)+sinh(x/2)) & exp_R(x) = (1+tanh(x/2))/(1-tanh(x/2)) & exp_R(-x
) = (1-tanh(x/2))/(1+tanh(x/2))
proof
A1: exp_R(x/2)>0 by SIN_COS:55;
A2: cosh(x/2) <> 0 by Lm1;
A3: exp_R(-x) = exp_R(-x/2+-x/2) .= exp_R(-x/2)*exp_R(-x/2) by SIN_COS:50
.= exp_R(-x/2)*exp_R(x/2)*(exp_R(-x/2)/exp_R(x/2)) by A1,XCMPLX_1:90
.= exp_R(-x/2+x/2)*(exp_R(-x/2)/exp_R(x/2)) by SIN_COS:50
.= ((exp_R(x/2)+exp_R(-x/2))/2-(exp_R(x/2)-exp_R(-x/2))/2)/exp_R(x/2) by
SIN_COS:51
.= ((exp_R(x/2)+exp_R(-x/2))/2-sinh(x/2))/exp_R(x/2) by Lm2
.= (cosh(x/2)-sinh(x/2))/((exp_R(x/2)+exp_R(-x/2))/2 +(exp_R(x/2)/2-
exp_R(-x/2)/2)) by Lm2
.= (cosh(x/2)-sinh(x/2))/(cosh(x/2)+(exp_R(x/2)-exp_R(-x/2))/2) by Lm2
.= (cosh(x/2)-sinh(x/2))/(cosh(x/2)+sinh(x/2)) by Lm2;
then
A4: exp_R(-x) = (cosh(x/2)-sinh(x/2))/cosh(x/2) /((cosh(x/2)+sinh(x/2))/cosh
(x/2)) by A2,XCMPLX_1:55
.= (cosh(x/2)/cosh(x/2)-sinh(x/2)/cosh(x/2)) /((cosh(x/2)+sinh(x/2))/
cosh(x/2)) by XCMPLX_1:120
.= (1-sinh(x/2)/cosh(x/2))/((cosh(x/2)+sinh(x/2))/cosh(x/2)) by A2,
XCMPLX_1:60
.= (1-tanh(x/2))/((cosh(x/2)+sinh(x/2))/cosh(x/2)) by Th1
.= (1-tanh(x/2))/(cosh(x/2)/cosh(x/2)+sinh(x/2)/cosh(x/2)) by XCMPLX_1:62
.= (1-tanh(x/2))/(1+sinh(x/2)/cosh(x/2)) by A2,XCMPLX_1:60
.= (1-tanh(x/2))/(1+tanh(x/2)) by Th1;
A5: exp_R(-x) = (exp_R(x)+exp_R(-x))/2-(exp_R(x)-exp_R(-x))/2
.= cosh(x)-(exp_R(x)-exp_R(-x))/2 by Lm2
.= cosh(x)-sinh(x) by Lm2;
A6: exp_R(x) = (exp_R(x)+exp_R(-x))/2+(exp_R(x)-exp_R(-x))/2
.= cosh(x)+(exp_R(x)-exp_R(-x))/2 by Lm2
.= cosh(x)+sinh(x) by Lm2;
A7: exp_R(-x/2)>0 by SIN_COS:55;
A8: exp_R(x) = exp_R(x/2+x/2) .= exp_R(x/2)*exp_R(x/2) by SIN_COS:50
.= exp_R(x/2)*exp_R(-x/2)*(exp_R(x/2)/exp_R(-x/2)) by A7,XCMPLX_1:90
.= exp_R(x/2+-x/2)*(exp_R(x/2)/exp_R(-x/2)) by SIN_COS:50
.= ((exp_R(x/2)+exp_R(-x/2))/2+ (exp_R(x/2)-exp_R(-x/2))/2)/exp_R(-x/2)
by SIN_COS:51
.= (cosh(x/2)+(exp_R(x/2)-exp_R(-x/2))/2)/exp_R(-x/2) by Lm2
.= (cosh(x/2)+sinh(x/2))/((exp_R(-x/2)+exp_R(x/2))/2 -(exp_R(x/2)-exp_R(
-x/2))/2) by Lm2
.= (cosh(x/2)+sinh(x/2))/((exp_R(x/2)+exp_R(-x/2))/2-sinh(x/2)) by Lm2
.= (cosh(x/2)+sinh(x/2))/(cosh(x/2)-sinh(x/2)) by Lm2;
then
exp_R(x) = (cosh(x/2)+sinh(x/2))/cosh(x/2) /((cosh(x/2)-sinh(x/2))/cosh(
x/2)) by A2,XCMPLX_1:55
.= (cosh(x/2)/cosh(x/2)+sinh(x/2)/cosh(x/2)) /((cosh(x/2)-sinh(x/2))/
cosh(x/2)) by XCMPLX_1:62
.= (1+sinh(x/2)/cosh(x/2))/((cosh(x/2)-sinh(x/2))/cosh(x/2)) by A2,
XCMPLX_1:60
.= (1+tanh(x/2))/((cosh(x/2)-sinh(x/2))/cosh(x/2)) by Th1
.= (1+tanh(x/2))/(cosh(x/2)/cosh(x/2)-sinh(x/2)/cosh(x/2)) by XCMPLX_1:120
.= (1+tanh(x/2))/(1-sinh(x/2)/cosh(x/2)) by A2,XCMPLX_1:60
.= (1+tanh(x/2))/(1-tanh(x/2)) by Th1;
hence thesis by A6,A5,A8,A3,A4;
end;
theorem
x <> 0 implies exp_R(x) = (coth(x/2)+1)/(coth(x/2)-1) & exp_R(-x) = (
coth(x/2)-1)/(coth(x/2)+1)
proof
assume x <> 0;
then
A1: x/2 <> 0;
A2: coth(x/2)-1 = 1/(1/coth(x/2))-1 by XCMPLX_1:56
.= 1/tanh(x/2)-1 by Th2
.= 1/tanh(x/2)-tanh(x/2)/tanh(x/2) by A1,Lm4,XCMPLX_1:60
.= (1-tanh(x/2))/tanh(x/2) by XCMPLX_1:120;
A3: coth(x/2)+1 = 1/(1/coth(x/2))+1 by XCMPLX_1:56
.= 1/tanh(x/2)+1 by Th2
.= 1/tanh(x/2)+tanh(x/2)/tanh(x/2) by A1,Lm4,XCMPLX_1:60
.= (1+tanh(x/2))/tanh(x/2) by XCMPLX_1:62;
A4: exp_R(-x) = (1-tanh(x/2))/(1+tanh(x/2)) by Th7
.= (coth(x/2)-1)/(coth(x/2)+1)by A1,A3,A2,Lm4,XCMPLX_1:55;
exp_R(x) = (1+tanh(x/2))/(1-tanh(x/2)) by Th7
.= (coth(x/2)+1)/(coth(x/2)-1)by A1,A3,A2,Lm4,XCMPLX_1:55;
hence thesis by A4;
end;
theorem
(cosh(x)+sinh x)/(cosh(x)-sinh(x)) = (1+tanh(x))/(1-tanh x)
proof
A1: exp_R(2*x) = (1+tanh(x))/(1-tanh((2*x)/2)) by Th7
.= (1+tanh(x))/(1-tanh(x));
exp_R(2*x) = (cosh((2*x)/2)+sinh((2*x)/2))/(cosh((2*x)/2)-sinh((2*x)/2))
by Th7
.= (cosh(x)+sinh(x))/(cosh(x)-sinh(x));
hence thesis by A1;
end;
Lm10: cosh(y+z) = cosh(y)*cosh(z)+sinh(y)*sinh(z) & cosh(y-z) = cosh(y)*cosh(z
)-sinh(y)*sinh(z) & sinh(y+z) = sinh(y)*cosh(z)+cosh(y)*sinh(z) & sinh(y-z) =
sinh(y)*cosh(z)-cosh(y)*sinh(z) & tanh(y+z) = (tanh(y)+tanh(z))/(1+tanh(y)*tanh
(z)) & tanh(y-z) = (tanh(y)-tanh(z))/(1-tanh(y)*tanh(z))
proof
A1: cosh(y)*cosh(z)-sinh(y)*sinh(z) = cosh.y*cosh(z)-sinh(y)*sinh(z) by
SIN_COS2:def 4
.= cosh.y*cosh.z-sinh(y)*sinh(z) by SIN_COS2:def 4
.= cosh.y*cosh.z-sinh.y*sinh(z) by SIN_COS2:def 2
.= cosh.y*cosh.z-sinh.y*sinh.z by SIN_COS2:def 2
.= cosh.(y-z) by SIN_COS2:20
.= cosh(y-z) by SIN_COS2:def 4;
A2: sinh(y)*cosh(z)+cosh(y)*sinh(z) = sinh.y*cosh(z)+cosh(y)*sinh(z) by
SIN_COS2:def 2
.= sinh.y*cosh(z)+cosh(y)*sinh.z by SIN_COS2:def 2
.= sinh.y*cosh.z+cosh(y)*sinh.z by SIN_COS2:def 4
.= sinh.y*cosh.z+cosh.y*sinh.z by SIN_COS2:def 4
.= sinh.(y+z) by SIN_COS2:21
.= sinh(y+z) by SIN_COS2:def 2;
A3: tanh(y-z) = tanh.(y-z) by SIN_COS2:def 6
.= (tanh.y-tanh.z)/(1-tanh.y*tanh.z) by SIN_COS2:22
.= (tanh(y)-tanh.z)/(1-tanh.y*tanh.z) by SIN_COS2:def 6
.= (tanh(y)-tanh(z))/(1-tanh.y*tanh.z) by SIN_COS2:def 6
.= (tanh(y)-tanh(z))/(1-tanh(y)*tanh.z) by SIN_COS2:def 6
.= (tanh(y)-tanh(z))/(1-tanh(y)*tanh(z)) by SIN_COS2:def 6;
A4: tanh(y+z) = tanh.(y+z) by SIN_COS2:def 6
.= (tanh.y+tanh.z)/(1+tanh.y*tanh.z) by SIN_COS2:22
.= (tanh(y)+tanh.z)/(1+tanh.y*tanh.z) by SIN_COS2:def 6
.= (tanh(y)+tanh(z))/(1+tanh.y*tanh.z) by SIN_COS2:def 6
.= (tanh(y)+tanh(z))/(1+tanh(y)*tanh.z) by SIN_COS2:def 6
.= (tanh(y)+tanh(z))/(1+tanh(y)*tanh(z)) by SIN_COS2:def 6;
A5: sinh(y)*cosh(z)-cosh(y)*sinh(z) = sinh.y*cosh(z)-cosh(y)*sinh(z) by
SIN_COS2:def 2
.= sinh.y*cosh(z)-cosh(y)*sinh.z by SIN_COS2:def 2
.= sinh.y*cosh.z-cosh(y)*sinh.z by SIN_COS2:def 4
.= sinh.y*cosh.z-cosh.y*sinh.z by SIN_COS2:def 4
.= sinh.(y-z) by SIN_COS2:21
.= sinh(y-z) by SIN_COS2:def 2;
cosh(y)*cosh(z)+sinh(y)*sinh(z) = cosh.y*cosh(z)+sinh(y)*sinh(z) by
SIN_COS2:def 4
.= cosh.y*cosh.z+sinh(y)*sinh(z) by SIN_COS2:def 4
.= cosh.y*cosh.z+sinh.y*sinh(z) by SIN_COS2:def 2
.= cosh.y*cosh.z+sinh.y*sinh.z by SIN_COS2:def 2
.= cosh.(y+z) by SIN_COS2:20
.= cosh(y+z) by SIN_COS2:def 4;
hence thesis by A1,A2,A5,A4,A3;
end;
theorem
y <> 0 implies coth(y)+tanh(z) = cosh(y+z)/(sinh(y)*cosh(z)) & coth(y)
-tanh(z) = cosh(y-z)/(sinh(y)*cosh(z))
proof
assume
A1: y <> 0;
A2: cosh(z) <> 0 by Lm1;
A3: coth(y)-tanh(z) = cosh(y)/sinh(y)-tanh(z) by SIN_COS5:def 1
.= cosh(y)*cosh(z)/(sinh(y)*cosh(z))-tanh(z) by A2,XCMPLX_1:91
.= cosh(y)*cosh(z)/(sinh(y)*cosh(z))-sinh(z)/cosh(z) by Th1
.= cosh(y)*cosh(z)/(sinh(y)*cosh(z)) -sinh(y)*sinh(z)/(sinh(y)*cosh(z))
by A1,Lm4,XCMPLX_1:91
.= (cosh(y)*cosh(z)-sinh(y)*sinh(z))/(sinh(y)*cosh(z)) by XCMPLX_1:120
.= cosh(y-z)/(sinh(y)*cosh(z)) by Lm10;
coth(y)+tanh(z) = cosh(y)/sinh(y)+tanh(z) by SIN_COS5:def 1
.= cosh(y)*cosh(z)/(sinh(y)*cosh z)+tanh z by A2,XCMPLX_1:91
.= cosh(y)*cosh(z)/(sinh(y)*cosh z)+sinh(z)/cosh(z) by Th1
.= cosh(y)*cosh(z)/(sinh(y)*cosh z) +sinh(y)*sinh(z)/(sinh(y)*cosh z) by A1
,Lm4,XCMPLX_1:91
.= (cosh(y)*cosh(z)+sinh(y)*sinh(z))/(sinh(y)*cosh(z)) by XCMPLX_1:62
.= cosh(y+z)/(sinh(y)*cosh(z)) by Lm10;
hence thesis by A3;
end;
theorem Th11:
sinh(y)*sinh(z) = 1/2*(cosh(y+z)-cosh(y-z)) & sinh(y)*cosh(z) =
1/2*(sinh(y+z)+sinh(y-z)) & cosh(y)*sinh(z) = 1/2*(sinh(y+z)-sinh(y-z)) & cosh(
y)*cosh(z) = 1/2*(cosh(y+z)+cosh(y-z))
proof
A1: sinh(y)*cosh(z) = 1/2*(sinh(y)*cosh(z)+cosh(y)*sinh(z)+(sinh(y)*cosh(z)-
cosh(y)*sinh(z)))
.= 1/2*(sinh(y+z)+(sinh(y)*cosh(z)-cosh(y)*sinh(z))) by Lm10
.= 1/2*(sinh(y+z)+sinh(y-z)) by Lm10;
A2: cosh(y)*sinh(z) = 1/2*(sinh(y)*cosh(z)+cosh(y)*sinh(z)-(sinh(y)*cosh(z)-
cosh(y)*sinh(z)))
.= 1/2*(sinh(y+z)-(sinh(y)*cosh(z)-cosh(y)*sinh(z))) by Lm10
.= 1/2*(sinh(y+z)-sinh(y-z)) by Lm10;
A3: cosh(y)*cosh(z) = 1/2*(cosh(y)*cosh(z)+sinh(y)*sinh(z)+(cosh(y)*cosh(z)-
sinh(y)*sinh(z)))
.= 1/2*(cosh(y+z)+(cosh(y)*cosh(z)-sinh(y)*sinh(z))) by Lm10
.= 1/2*(cosh(y+z)+cosh(y-z)) by Lm10;
sinh(y)*sinh(z) = 1/2*(cosh(y)*cosh(z)+sinh(y)*sinh(z)-(cosh(y)*cosh(z)-
sinh(y)*sinh(z)))
.= 1/2 * (cosh(y+z)-(cosh(y)*cosh(z)-sinh(y)*sinh(z))) by Lm10
.= 1/2 * (cosh(y+z)-cosh(y-z)) by Lm10;
hence thesis by A1,A2,A3;
end;
theorem
(sinh y)^2-(cosh z)^2 = sinh(y+z)*sinh(y-z)-1
proof
(sinh y)^2-(cosh z)^2 = (sinh y)^2-(cosh z)^2*1
.= (sinh y)^2-(cosh z)^2*((cosh y)^2-(sinh y)^2) by Lm3
.= (sinh y)^2+((cosh z)^2*(sinh y)^2 -(cosh y)^2*((cosh z)^2-(sinh z)^2+
(sinh z)^2))
.= (sinh y)^2+((cosh z)^2*(sinh y)^2 -(cosh y)^2*(1+(sinh z)^2)) by Lm3
.= (sinh y)^2+((sinh(y)*cosh(z)+cosh(y)*sinh(z)) *(sinh(y)*cosh(z)-cosh(
y)*sinh z)-(cosh y)^2)
.= (sinh y)^2+(sinh(y+z) *(sinh(y)*cosh(z)-cosh(y)*sinh(z))-(cosh y)^2)
by Lm10
.= sinh(y+z)*sinh(y-z)-(cosh y)^2+(sinh y)^2 by Lm10
.= sinh(y+z)*sinh(y-z)-((cosh y)^2-(sinh y)^2)
.= sinh(y+z)*sinh(y-z)-1 by Lm3;
hence thesis;
end;
Lm11: sinh(y)+sinh(z) = 2*sinh(y/2+z/2)*cosh(y/2-z/2) & sinh(y)-sinh(z) = 2*
sinh(y/2-z/2)*cosh(y/2+z/2) & cosh(y)+cosh(z) = 2*cosh(y/2+z/2)*cosh(y/2-z/2) &
cosh(y)-cosh(z) = 2*sinh(y/2-z/2)*sinh(y/2+z/2) & tanh(y)+tanh(z) = sinh(y+z)/(
cosh(y)*cosh(z)) & tanh(y)-tanh(z) = sinh(y-z)/(cosh(y)*cosh(z))
proof
A1: 2*sinh(y/2-z/2)*cosh(y/2+z/2) = 2*sinh.(y/2-z/2)*cosh(y/2+z/2) by
SIN_COS2:def 2
.= 2*sinh.(y/2-z/2)*cosh.(y/2+z/2) by SIN_COS2:def 4
.= sinh.y-sinh.z by SIN_COS2:26
.= sinh(y)-sinh.z by SIN_COS2:def 2
.= sinh(y)-sinh(z) by SIN_COS2:def 2;
A2: 2*cosh(y/2+z/2)*cosh(y/2-z/2) = 2*cosh.(y/2+z/2)*cosh(y/2-z/2) by
SIN_COS2:def 4
.= 2*cosh.(y/2+z/2)*cosh.(y/2-z/2) by SIN_COS2:def 4
.= cosh.y+cosh.z by SIN_COS2:27
.= cosh(y)+cosh.z by SIN_COS2:def 4
.= cosh(y)+cosh(z) by SIN_COS2:def 4;
A3: sinh(y-z)/(cosh(y)*cosh(z)) = sinh.(y-z)/(cosh(y)*cosh(z)) by
SIN_COS2:def 2
.= sinh.(y-z)/(cosh.y*cosh(z)) by SIN_COS2:def 4
.= sinh.(y-z)/(cosh.y*cosh.z) by SIN_COS2:def 4
.= tanh.y-tanh.z by SIN_COS2:28
.= tanh(y)-tanh.z by SIN_COS2:def 6
.= tanh(y)-tanh(z) by SIN_COS2:def 6;
A4: sinh(y+z)/(cosh(y)*cosh(z)) = sinh.(y+z)/(cosh(y)*cosh(z)) by
SIN_COS2:def 2
.= sinh.(y+z)/(cosh.y*cosh(z)) by SIN_COS2:def 4
.= sinh.(y+z)/(cosh.y*cosh.z) by SIN_COS2:def 4
.= tanh.y+tanh.z by SIN_COS2:28
.= tanh(y)+tanh.z by SIN_COS2:def 6
.= tanh(y)+tanh(z) by SIN_COS2:def 6;
A5: 2*sinh(y/2-z/2)*sinh(y/2+z/2) = 2*sinh.(y/2-z/2)*sinh(y/2+z/2) by
SIN_COS2:def 2
.= 2*sinh.(y/2-z/2)*sinh.(y/2+z/2) by SIN_COS2:def 2
.= cosh.y-cosh.z by SIN_COS2:27
.= cosh(y)-cosh.z by SIN_COS2:def 4
.= cosh(y)-cosh(z) by SIN_COS2:def 4;
2*sinh(y/2+z/2)*cosh(y/2-z/2) = 2*sinh.(y/2+z/2)*cosh(y/2-z/2) by
SIN_COS2:def 2
.= 2*sinh.(y/2+z/2)*cosh.(y/2-z/2) by SIN_COS2:def 4
.= sinh.y+sinh.z by SIN_COS2:26
.= sinh(y)+sinh.z by SIN_COS2:def 2
.= sinh(y)+sinh(z) by SIN_COS2:def 2;
hence thesis by A1,A2,A5,A4,A3;
end;
theorem
(sinh(y)-sinh z)^2-(cosh(y)-cosh z)^2 = 4*(sinh((y-z)/2))^2 & (cosh(y)
+cosh z)^2-(sinh(y)+sinh z)^2 = 4*(cosh((y-z)/2))^2
proof
A1: (cosh(y)+cosh(z))^2-(sinh(y)+sinh(z))^2 = (2*cosh(y/2+z/2)*cosh(y/2-z/2)
)^2-(sinh(y)+sinh(z))^2 by Lm11
.= (2*(cosh(y/2+z/2)*cosh(y/2-z/2)))^2 - (2*sinh(y/2+z/2)*cosh(y/2-z/2))
^2 by Lm11
.= 4*((cosh(y/2-z/2))^2 * ((cosh(y/2+z/2))^2 - (sinh(y/2+z/2))^2))
.= 4*((cosh(y/2-z/2))^2*1) by Lm3
.= 4*(cosh((y-z)/2))^2;
(sinh(y)-sinh z)^2-(cosh(y)-cosh z)^2 = (2*sinh(y/2-z/2)*cosh(y/2+z/2))
^2-(cosh(y)-cosh z)^2 by Lm11
.= (2*cosh(y/2+z/2)*sinh(y/2-z/2))^2 -(2*sinh(y/2-z/2)*sinh((y+z)/2))^2
by Lm11
.= 4*((sinh(y/2-z/2))^2*((cosh(y/2+z/2))^2 - (sinh(y/2+z/2))^2))
.= 4*((sinh(y/2-z/2))^2*1) by Lm3
.= 4*(sinh((y-z)/2))^2;
hence thesis by A1;
end;
theorem
(sinh(y)+sinh(z))/(sinh(y)-sinh(z)) = tanh((y+z)/2)*coth((y-z)/2)
proof
(sinh(y)+sinh(z))/(sinh(y)-sinh(z)) = 2*sinh(y/2+z/2)*cosh(y/2-z/2)/(
sinh(y)-sinh(z)) by Lm11
.= 2*sinh(y/2+z/2)*cosh(y/2-z/2) / (2*sinh(y/2-z/2)*cosh(y/2+z/2)) by Lm11
.= 2*sinh(y/2+z/2)*cosh(y/2-z/2) / (2*cosh(y/2+z/2)*sinh(y/2-z/2))
.= 2*sinh(y/2+z/2)/(2*cosh(y/2+z/2)) * (cosh(y/2-z/2)/sinh(y/2-z/2)) by
XCMPLX_1:76
.= 2*sinh(y/2+z/2)/(2*cosh(y/2+z/2)) * coth(y/2-z/2) by SIN_COS5:def 1
.= 2/2*(sinh(y/2+z/2)/cosh(y/2+z/2)) * coth(y/2-z/2) by XCMPLX_1:76
.= tanh((y+z)/2) * coth((y-z)/2) by Th1;
hence thesis;
end;
theorem
(cosh(y)+cosh(z))/(cosh(y)-cosh(z)) = coth((y+z)/2)*coth((y-z)/2)
proof
(cosh(y)+cosh(z))/(cosh(y)-cosh(z)) = 2*cosh(y/2+z/2)*cosh(y/2-z/2)/(
cosh(y)-cosh(z)) by Lm11
.= 2*cosh(y/2+z/2)*cosh(y/2-z/2)/(2*sinh(y/2-z/2)*sinh((y+z)/2)) by Lm11
.= 2*cosh(y/2+z/2)*cosh(y/2-z/2)/(2*sinh(y/2+z/2)*sinh((y-z)/2))
.= 2*cosh(y/2+z/2)/(2*sinh(y/2+z/2)) * (cosh(y/2-z/2)/sinh(y/2-z/2)) by
XCMPLX_1:76
.= 2*cosh(y/2+z/2)/(2*sinh(y/2+z/2))*coth(y/2-z/2) by SIN_COS5:def 1
.= 2/2*(cosh(y/2+z/2)/sinh(y/2+z/2))*coth(y/2-z/2) by XCMPLX_1:76
.= coth((y+z)/2)*coth((y-z)/2) by SIN_COS5:def 1;
hence thesis;
end;
theorem
y-z <> 0 implies (sinh(y)+sinh(z))/(cosh(y)+cosh(z)) = (cosh(y)-cosh(z
))/(sinh(y)-sinh(z))
proof
assume
A1: y-z <> 0;
A2: cosh(y/2-z/2) <> 0 by Lm1;
(sinh(y)+sinh(z))/(cosh(y)+cosh(z)) = 2*sinh(y/2+z/2)*cosh(y/2-z/2)/(
cosh(y)+cosh(z)) by Lm11
.= 2*sinh(y/2+z/2)*cosh(y/2-z/2)/(2*cosh(y/2+z/2)*cosh(y/2-z/2)) by Lm11
.= 2*sinh(y/2+z/2)/(2*cosh(y/2+z/2)) * (cosh(y/2-z/2)/cosh(y/2-z/2)) by
XCMPLX_1:76
.= 2*sinh(y/2+z/2)/(2*cosh(y/2+z/2))*1 by A2,XCMPLX_1:60
.= 2*sinh((y+z)/2)*sinh((y-z)/2) / (2*cosh(y/2+z/2)*sinh(y/2-z/2)) by A1
,Lm5,XCMPLX_1:91
.= 2*sinh((y-z)/2)*sinh((y+z)/2)/(2*cosh(y/2+z/2)*sinh(y/2-z/2))
.= (cosh(y)-cosh(z))/(2*sinh(y/2-z/2)*cosh(y/2+z/2)) by Lm11
.= (cosh(y)-cosh(z))/(sinh(y)-sinh(z)) by Lm11;
hence thesis;
end;
theorem
y+z <> 0 implies (sinh(y)-sinh(z))/(cosh(y)+cosh(z)) = (cosh(y)-cosh(z
))/(sinh(y)+sinh(z))
proof
assume
A1: y+z <> 0;
A2: cosh(y/2+z/2) <> 0 by Lm1;
(sinh(y)-sinh(z))/(cosh(y)+cosh(z)) = 2*sinh(y/2-z/2)*cosh(y/2+z/2)/(
cosh(y)+cosh(z)) by Lm11
.= 2*cosh(y/2+z/2)*sinh(y/2-z/2)/(2*cosh(y/2+z/2)*cosh(y/2-z/2)) by Lm11
.= 2*cosh(y/2+z/2)/(2*cosh(y/2+z/2)) * (sinh(y/2-z/2)/cosh(y/2-z/2)) by
XCMPLX_1:76
.= cosh(y/2+z/2)/cosh(y/2+z/2) *(sinh(y/2-z/2)/cosh(y/2-z/2)) by
XCMPLX_1:91
.= 1*(sinh(y/2-z/2)/cosh(y/2-z/2)) by A2,XCMPLX_1:60
.= sinh(y/2+z/2)*sinh(y/2-z/2) / (sinh(y/2+z/2)*cosh(y/2-z/2)) by A1,Lm6,
XCMPLX_1:91
.= 2*(sinh(y/2+z/2)*sinh(y/2-z/2)) /(2*(sinh(y/2+z/2)*cosh(y/2-z/2))) by
XCMPLX_1:91
.= 2*sinh((y-z)/2)*sinh((y+z)/2) / (2*sinh(y/2+z/2)*cosh(y/2-z/2))
.= (cosh(y)-cosh(z))/(2*sinh(y/2+z/2)*cosh(y/2-z/2)) by Lm11
.= (cosh(y)-cosh(z))/(sinh(y)+sinh(z)) by Lm11;
hence thesis;
end;
theorem
(sinh(y)+sinh(z))/(cosh(y)+cosh(z)) = tanh(y/2+z/2) & (sinh(y)-sinh(z)
)/(cosh(y)+cosh(z)) = tanh(y/2-z/2)
proof
A1: cosh(y/2-z/2) <> 0 by Lm1;
A2: cosh(y/2+z/2) <> 0 by Lm1;
A3: (sinh(y)-sinh(z))/(cosh(y)+cosh(z)) = 2*sinh(y/2-z/2)*cosh(y/2+z/2)/(
cosh(y)+cosh(z)) by Lm11
.= 2*(sinh(y/2-z/2)*cosh(y/2+z/2))/(2*cosh(y/2+z/2)*cosh(y/2-z/2)) by Lm11
.= 2*(sinh(y/2-z/2)*cosh(y/2+z/2))/(2*(cosh(y/2+z/2)*cosh(y/2-z/2)))
.= cosh(y/2+z/2)*sinh(y/2-z/2)/(cosh(y/2+z/2)*cosh(y/2-z/2)) by XCMPLX_1:91
.= cosh(y/2+z/2)/cosh(y/2+z/2)*(sinh(y/2-z/2)/cosh(y/2-z/2)) by XCMPLX_1:76
.= 1*(sinh(y/2-z/2)/cosh(y/2-z/2)) by A2,XCMPLX_1:60
.= tanh(y/2-z/2) by Th1;
(sinh(y)+sinh(z))/(cosh(y)+cosh(z)) = 2*sinh(y/2+z/2)*cosh(y/2-z/2)/(
cosh(y)+cosh(z)) by Lm11
.= 2*sinh(y/2+z/2)*cosh(y/2-z/2)/(2*cosh(y/2+z/2)*cosh(y/2-z/2)) by Lm11
.= 2*sinh(y/2+z/2)/(2*cosh(y/2+z/2))*(cosh(y/2-z/2)/cosh(y/2-z/2)) by
XCMPLX_1:76
.= 2*sinh(y/2+z/2)/(2*cosh(y/2+z/2))*1 by A1,XCMPLX_1:60
.= 2/2*(sinh(y/2+z/2)/cosh(y/2+z/2)) by XCMPLX_1:76
.= tanh(y/2+z/2) by Th1;
hence thesis by A3;
end;
theorem
(tanh(y)+tanh(z))/(tanh(y)-tanh(z)) = sinh(y+z)/sinh(y-z)
proof
A1: cosh(y) <> 0 & cosh(z) <> 0 by Lm1;
(tanh(y)+tanh(z))/(tanh(y)-tanh(z)) = sinh(y+z)/(cosh(y)*cosh(z))/(tanh(
y)-tanh(z)) by Lm11
.= sinh(y+z)/(cosh(y)*cosh(z))/(sinh(y-z)/(cosh(y)*cosh(z))) by Lm11
.= sinh(y+z)/sinh(y-z) by A1,XCMPLX_1:6,55;
hence thesis;
end;
Lm12: 1+(cosh(x)+cosh(x)) <> 0
proof
cosh.x > 0 by SIN_COS2:15;
then cosh x > 0 by SIN_COS2:def 4;
hence thesis;
end;
Lm13: cosh(x)+1 > 0 & cosh(x)-1 >= 0 & cosh(x)+2+cosh(x) <> 0
proof
cosh.x > 0 by SIN_COS2:15;
then
A1: cosh x > 0 by SIN_COS2:def 4;
cosh(x) >= 1 by Lm1;
then cosh(x)-1 >= 1-1 by XREAL_1:13;
hence thesis by A1;
end;
theorem
(sinh(y-z)+sinh(y)+sinh(y+z))/(cosh(y-z)+cosh(y)+cosh(y+z)) = tanh(y)
proof
(sinh(y-z)+sinh(y)+sinh(y+z))/(cosh(y-z)+cosh(y)+cosh(y+z)) = (sinh(y)*
cosh(z)-cosh(y)*sinh(z)+sinh(y)+sinh(y+z)) /(cosh(y-z)+cosh(y)+cosh(y+z)) by
Lm10
.= (sinh(y)+(sinh(y)*cosh(z)-cosh(y)*sinh(z)) +(sinh(y)*cosh(z)+cosh(y)*
sinh(z)))/(cosh(y)+cosh(y-z)+cosh(y+z)) by Lm10
.= sinh(y)*(1+(cosh(z)+cosh(z))) / (cosh(y)+(cosh(y)*cosh(z)-sinh(y)*
sinh(z))+cosh(y+z)) by Lm10
.= sinh(y)*(1+(cosh(z)+cosh(z))) /(cosh(y)+(cosh(y)*cosh(z)-sinh(y)*sinh
(z)) +(cosh(y)*cosh(z)+sinh(y)*sinh(z))) by Lm10
.= sinh(y)*(1+(cosh(z)+cosh(z)))/(cosh(y)*(1+(cosh(z)+cosh(z))))
.= sinh(y)/cosh(y) * ((1+(cosh(z)+cosh(z)))/(1+(cosh(z)+cosh(z)))) by
XCMPLX_1:76
.= sinh(y)/cosh(y)*1 by Lm12,XCMPLX_1:60
.= tanh(y) by Th1;
hence thesis;
end;
Lm14: sinh(y)*cosh(z)/(cosh(y)*cosh(z)) = tanh(y) & sinh(y)*cosh(z) = tanh(y)*
(cosh(y)*cosh(z)) & sinh(y) = tanh(y)*cosh(y) & sinh(y)*sinh(z) = tanh(y)*tanh(
z)*(cosh(y)*cosh(z))
proof
A1: cosh y <> 0 by Lm1;
then
A2: sinh(y) = sinh(y)/cosh(y)*cosh(y) by XCMPLX_1:87
.= tanh(y)*cosh(y) by Th1;
A3: cosh z <> 0 by Lm1;
then
A4: sinh(y)*cosh(z)/(cosh(y)*cosh(z)) = sinh(y)/cosh(y) by XCMPLX_1:91
.= tanh(y) by Th1;
sinh(y)*sinh(z) = sinh(y)*sinh(z)/(cosh(y)*cosh(z))*(cosh(y)*cosh(z)) by A1
,A3,XCMPLX_1:6,87
.= sinh(y)/cosh(y)*(sinh(z)/cosh(z))*(cosh(y)*cosh(z)) by XCMPLX_1:76
.= tanh(y)*(sinh(z)/cosh(z))*(cosh(y)*cosh(z)) by Th1
.= tanh(y)*tanh(z)*(cosh(y)*cosh(z)) by Th1;
hence thesis by A4,A2;
end;
theorem Th21:
sinh(y+z+w) = (tanh(y)+tanh(z)+tanh(w)+tanh(y)*tanh(z)*tanh w) *
cosh(y)*cosh(z)*cosh(w) & cosh(y+z+w) = (1+tanh(y)*tanh(z)+tanh(z)*tanh(w)+tanh
(w)*tanh y) * cosh(y)*cosh(z)*cosh(w) & tanh(y+z+w) = (tanh(y)+tanh(z)+tanh(w)+
tanh(y)*tanh(z)*tanh w) / (1+tanh(z)*tanh(w)+tanh(w)*tanh(y)+tanh(y)*tanh z)
proof
A1: cosh(w) <> 0 by Lm1;
cosh(y) <> 0 & cosh(z) <> 0 by Lm1;
then
A2: cosh(y)*cosh(z) <> 0 by XCMPLX_1:6;
A3: cosh(y+z+w) = cosh(y+z)*cosh(w)+sinh(y+z)*sinh(w) by Lm10
.= (cosh(y)*cosh(z)+sinh(y)*sinh(z))*cosh(w)+sinh(y+z)*sinh(w) by Lm10
.= cosh(y)*cosh(z)*cosh(w)+sinh(y)*sinh(z)*cosh(w) + (sinh(y)*cosh(z)+
cosh(y)*sinh(z))*sinh(w) by Lm10
.= cosh(y)*cosh(z)*cosh(w)+tanh(y)*tanh(z)*(cosh(y)*cosh(z))*cosh(w) + (
sinh(y)*sinh(w)*cosh(z)+sinh(z)*sinh(w)*cosh(y)) by Lm14
.= cosh(y)*cosh(z)*cosh(w) + tanh(y)*tanh(z)*(cosh(y)*cosh(z))*cosh(w) +
(tanh(w)*tanh(y)*(cosh(w)*cosh(y))*cosh(z)+sinh(z)*sinh(w)*cosh(y)) by Lm14
.= (1+tanh(y)*tanh(z))*(cosh(y)*cosh(z)*cosh(w)) + (tanh(z)*tanh(w)*(
cosh(z)*cosh(w))*cosh(y) + tanh(w)*tanh(y)*(cosh(y)*cosh(z)*cosh(w))) by Lm14
.= (1+tanh(y)*tanh(z)+tanh(z)*tanh(w)+tanh(w)*tanh(y)) *cosh(y)*cosh(z)*
cosh(w);
A4: sinh(y+z+w) = sinh(y+z)*cosh(w)+cosh(y+z)*sinh(w) by Lm10
.= (sinh(y)*cosh(z)+cosh(y)*sinh(z))*cosh(w)+cosh(y+z)*sinh(w) by Lm10
.= (sinh(y)*cosh(z)+cosh(y)*sinh(z))*cosh(w) +(cosh(y)*cosh(z)+sinh(y)*
sinh(z))*sinh(w) by Lm10
.= (tanh(y)*(cosh(y)*cosh(z))+cosh(y)*sinh(z))*cosh(w) + (cosh(y)*cosh(z
)+sinh(y)*sinh(z))*sinh(w) by Lm14
.= (tanh(y)*(cosh(y)*cosh(z))+tanh(z)*(cosh(y)*cosh(z)))*cosh(w) + (cosh
(y)*cosh(z)+sinh(y)*sinh(z))*sinh(w) by Lm14
.= (tanh(y)+tanh(z))*(cosh(y)*cosh(z)*cosh(w)) + (cosh(y)*(cosh(z)*sinh(
w))+sinh(y)*sinh(z)*sinh(w))
.= (tanh(y)+tanh(z))*(cosh(y)*cosh(z)*cosh(w)) + (cosh(y)*(tanh(w)*(cosh
(z)*cosh(w)))+sinh(y)*sinh(z)*sinh(w)) by Lm14
.= (tanh(y)+tanh(z))*(cosh(y)*cosh(z)*cosh(w)) + (tanh(w)*(cosh(y)*cosh(
z))*cosh(w) + tanh(y)*cosh(y)*sinh(z)*sinh(w)) by Lm14
.= (tanh(y)+tanh(z))*(cosh(y)*cosh(z)*cosh(w)) + (tanh(w)*(cosh(y)*cosh(
z))*cosh(w) + tanh(y)*cosh(y)*(tanh(z)*cosh(z))*sinh(w)) by Lm14
.= (tanh(y)+tanh(z))*(cosh(y)*cosh(z)*cosh(w)) +(tanh(w)*(cosh(y)*cosh(z
))*cosh(w) +tanh(y)*tanh(z)*(cosh(y)*cosh(z))*(tanh(w)*cosh(w))) by Lm14
.= (tanh(y)+tanh(z)+tanh(w)+tanh(y)*tanh(z)*tanh(w)) *cosh(y)*cosh(z)*
cosh(w);
then
tanh(y+z+w) = ((tanh(y)+tanh(z)+tanh(w)+tanh(y)*tanh(z)*tanh(w)) *(cosh(
y)*cosh(z)*cosh(w))) /((1+tanh(y)*tanh(z)+tanh(z)*tanh(w)+tanh(w)*tanh(y)) *(
cosh(y)*cosh(z)*cosh(w))) by A3,Th1
.= (tanh(y)+tanh(z)+tanh(w)+tanh(y)*tanh(z)*tanh(w)) /(1+tanh(y)*tanh(z)
+tanh(z)*tanh(w)+tanh(w)*tanh(y)) by A1,A2,XCMPLX_1:6,91;
hence thesis by A4,A3;
end;
theorem
cosh(2*y)+cosh(2*z)+cosh(2*w)+cosh(2*(y+z+w)) = 4*cosh(z+w)*cosh(w+y)*
cosh(y+z)
proof
cosh(2*y)+cosh(2*z)+cosh(2*w)+cosh(2*(y+z+w)) = 2*(1/2*(cosh(2*(y+z+w))+
cosh(2*y))+1/2*(cosh(2*w)+cosh(2*z)))
.= 2*(1/2*(2*cosh(2*(y+z+w)/2+2*y/2)*cosh(2*(y+z+w)/2-2*y/2)) + 1/2*(
cosh(2*w)+cosh(2*z))) by Lm11
.= 2*((cosh(z+w)*cosh((y+z+w)+y)) + 1/2*(2*cosh((2*w)/2+2*z/2)*cosh(2*w/
2-2*z/2))) by Lm11
.= 2*(cosh(z+w)*(cosh(2*y+(z+w))+cosh(w-z)))
.= 2*(cosh(z+w) *(2*cosh((2*y+(z+w))/2+(w-z)/2)*cosh((2*y+(z+w))/2-(w-z)
/2))) by Lm11
.= 4*cosh(z+w)*cosh(w+y)*cosh(y+z);
hence thesis;
end;
theorem
sinh(y)*sinh(z)*sinh(z-y) + sinh(z)*sinh(w)*sinh(w-z) + sinh(w)*sinh(y
)*sinh(y-w) + (sinh(z-y)*sinh(w-z)*sinh(y-w)) = 0
proof
sinh(y)*sinh(z)*sinh(z-y) + sinh(z)*sinh(w)*sinh(w-z) + sinh(w)*sinh(y)*
sinh(y-w) + (sinh(z-y)*sinh(w-z)*sinh(y-w)) = (1/2*(cosh(y+z)-cosh(y-z)))*sinh(
z-y) + sinh(z)*sinh(w)*sinh(w-z) + sinh(w)*sinh(y)*sinh(y-w) + sinh(z-y)*sinh(w
-z)*sinh(y-w) by Th11
.= 1/2*(cosh(y+z)*sinh(z-y)-cosh(y-z)*sinh(z-y)) + sinh(z)*sinh(w)*sinh(
w-z) + sinh(w)*sinh(y)*sinh(y-w) + sinh(z-y)*sinh(w-z)*sinh(y-w)
.= 1/2*(1/2*(sinh(y+z+(z-y))-sinh(y+z-(z-y)))-cosh(y-z)*sinh(z-y)) +
sinh(z)*sinh(w)*sinh(w-z) + sinh(w)*sinh(y)*sinh(y-w) + sinh(z-y)*sinh(w-z)*
sinh(y-w) by Th11
.= 1/2*(1/2*(sinh(2*z)-sinh(y+y))-1/2*(sinh(y-z+-(y-z))-sinh(y-z-(z-y)))
) +sinh(z)*sinh(w)*sinh(w-z) +sinh(w)*sinh(y)*sinh(y-w) +sinh(z-y)*sinh(w-z)*
sinh(y-w) by Th11
.= 1/2*(1/2*(sinh(2*z)-sinh(2*y))-1/2*(sinh.0-sinh(2*(y-z)))) + sinh(z)*
sinh(w)*sinh(w-z) + sinh(w)*sinh(y)*sinh(y-w) + sinh(z-y)*sinh(w-z)*sinh(y-w)
by SIN_COS2:def 2
.= 1/2*(1/2*(sinh(2*z)-sinh(2*y)--sinh(2*(y-z)))) + 1/2*(cosh(z+w)-cosh(
z-w))*sinh(w-z) + sinh(w)*sinh(y)*sinh(y-w) + sinh(z-y)*sinh(w-z)*sinh(y-w) by
Th11,SIN_COS2:16
.= 1/2*(1/2*(sinh(2*z)-sinh(2*y)--sinh(2*(y-z))) + (cosh(z+w)*sinh(w-z)-
cosh(z-w)*sinh(w-z))) + sinh(w)*sinh(y)*sinh(y-w) + sinh(z-y)*sinh(w-z)*sinh(y-
w)
.= 1/2*(1/2*(sinh(2*z)-sinh(2*y)--sinh(2*(y-z))) + (1/2*(sinh(z+w+(w-z))
-sinh(z+w-(w-z))) - cosh(z-w)*sinh(w-z))) + sinh(w)*sinh(y)*sinh(y-w) + sinh(z-
y)*sinh(w-z)*sinh(y-w) by Th11
.= 1/2*(1/2*(sinh(2*z)-sinh(2*y)--sinh(2*(y-z))) + (1/2*(sinh(2*w)-sinh(
2*z)) - 1/2*(sinh(z-w+(w-z))-sinh(z-w-(w-z))))) + sinh(w)*sinh(y)*sinh(y-w) +
sinh(z-y)*sinh(w-z)*sinh(y-w) by Th11
.= 1/2*(1/2*(sinh(2*z)-sinh(2*y)--sinh(2*(y-z))) + (1/2*(sinh(2*w)-sinh(
2*z)) - 1/2*(0-sinh(z-w-(w-z))))) + sinh(w)*sinh(y)*sinh(y-w) + sinh(z-y)*sinh(
w-z)*sinh(y-w) by SIN_COS2:16,def 2
.= 1/2*(1/2*(sinh(2*z)-sinh(2*y)--sinh(2*(y-z)) + (sinh(2*w)-sinh(2*z)--
sinh(2*(z-w))))) + 1/2*(cosh(w+y)-cosh(w-y))*sinh(y-w) + sinh(z-y)*sinh(w-z)*
sinh(y-w) by Th11
.= 1/2*(1/2*(sinh(2*z)-sinh(2*y)--sinh(2*(y-z)) + (sinh(2*w)-sinh(2*z)--
sinh(2*(z-w)))) + (cosh(w+y)*sinh(y-w)-cosh(w-y)*sinh(y-w))) + sinh(z-y)*sinh(w
-z)*sinh(y-w)
.= 1/2*(1/2*(sinh(2*z)-sinh(2*y)--sinh(2*(y-z)) + (sinh(2*w)-sinh(2*z)--
sinh(2*(z-w)))) + (1/2*(sinh(w+y+(y-w))-sinh(w+y-(y-w)))-cosh(w-y)*sinh(y-w)))
+ sinh(z-y)*sinh(w-z)*sinh(y-w) by Th11
.= 1/2*(1/2*(sinh(2*z)-sinh(2*y)--sinh(2*(y-z)) + (sinh(2*w)-sinh(2*z)--
sinh(2*(z-w)))) + (1/2*(sinh(2*y)-sinh(2*w))-1/2*(sinh(w-y +-(w-y))-sinh(w-y--(
w-y))))) + sinh(z-y)*sinh(w-z)*sinh(y-w) by Th11
.= 1/2*(1/2*(sinh(2*z)-sinh(2*y)--sinh(2*(y-z)) + (sinh(2*w)-sinh(2*z)--
sinh(2*(z-w)))) + (1/2*(sinh(2*y)-sinh(2*w))-1/2*(0-sinh(2*(w-y))))) + sinh(z-y
)*sinh(w-z)*sinh(y-w) by SIN_COS2:16,def 2
.= 1/2*(1/2*(sinh(2*(y-z))+sinh(2*(z-w))+sinh(2*(w-y)))) + 1/2*(cosh(z-y
+-(z-w)) - cosh(z-y-(w-z)))*sinh(y-w) by Th11
.= 1/2*(1/2*(sinh(2*(y-z))+sinh(2*(z-w))+sinh(2*(w-y))) + (cosh(w-y)*
sinh(y-w)-cosh(z-y-(w-z))*sinh(y-w)))
.= 1/2*(1/2*(sinh(2*(y-z))+sinh(2*(z-w))+sinh(2*(w-y))) + (1/2*(sinh(w-y
+-(w-y))-sinh(w-y-(y-w)))-cosh(z-y-(w-z))*sinh(y-w))) by Th11
.= 1/2*(1/2*(sinh(2*(y-z))+sinh(2*(z-w))+sinh(2*(w-y))) + (1/2*(0-sinh(w
-y-(y-w)))-cosh(z-y-(w-z))*sinh(y-w))) by SIN_COS2:16,def 2
.= 1/2*(1/2*(sinh(2*(y-z))+sinh(2*(z-w))+sinh(2*(w-y))) + (1/2*-sinh(2*(
w-y))-1/2*(sinh(z-y+(z-w)+(y-w))-sinh(z-y+(z-w)-(y-w))))) by Th11
.= 1/2*(1/2*(sinh(2*(y-z))+sinh(2*(z-w))+sinh(2*(w-y))) + 1/2*((sinh(-(2
*(y-z)))-sinh(2*(z-w)))+-sinh(2*(w-y))))
.= 1/2*(1/2*(sinh(2*(y-z))+sinh(2*(z-w))+sinh(2*(w-y))) + 1/2*(-sinh(2*(
y-z))-sinh(2*(z-w))+-sinh(2*(w-y)))) by Lm8;
hence thesis;
end;
theorem Th24:
x >= 0 implies sinh(x/2) = sqrt ((cosh(x)-1)/2)
proof
assume x >= 0;
then sinh(x/2) = sqrt (sinh(x/2))^2 by SIN_COS5:46,SQUARE_1:22
.= sqrt (sinh.(x/2))^2 by SIN_COS2:def 2
.= sqrt (1/2*(cosh.(2*(x/2))-1)) by SIN_COS2:18
.= sqrt ((cosh.x-1)/2)
.= sqrt ((cosh(x)-1)/2) by SIN_COS2:def 4;
hence thesis;
end;
theorem Th25:
x < 0 implies sinh(x/2) = - sqrt ((cosh(x)-1)/2)
proof
assume x < 0;
then
A1: x/2 < 0 by XREAL_1:141;
sinh(x/2) = --sinh(x/2) .= - sqrt (sinh(x/2))^2 by A1,SIN_COS5:47,SQUARE_1:23
.= - sqrt (sinh.(x/2))^2 by SIN_COS2:def 2
.= - sqrt (1/2*(cosh.(2*(x/2))-1)) by SIN_COS2:18
.= - sqrt ((cosh.x-1)/2)
.= - sqrt ((cosh(x)-1)/2) by SIN_COS2:def 4;
hence thesis;
end;
theorem Th26:
sinh(2*x) = 2*sinh(x)*cosh(x) & cosh(2*x) = 2*(cosh x)^2-1 &
tanh(2*x) = (2*tanh x)/(1+(tanh x)^2)
proof
A1: cosh(2*x) = cosh.(2*x) by SIN_COS2:def 4
.= 2*(cosh.x)^2-1 by SIN_COS2:23
.= 2*(cosh x)^2-1 by SIN_COS2:def 4;
A2: tanh(2*x) = tanh.(2*x) by SIN_COS2:def 6
.= (2*tanh.x)/(1+(tanh.x)^2) by SIN_COS2:23
.= (2*tanh x)/(1+(tanh.x)^2) by SIN_COS2:def 6
.= (2*tanh x)/(1+(tanh x)^2) by SIN_COS2:def 6;
sinh(2*x) = sinh.(2*x) by SIN_COS2:def 2
.= 2*sinh.x*cosh.x by SIN_COS2:23
.= 2*sinh(x)*cosh.x by SIN_COS2:def 2
.= 2*sinh(x)*cosh(x) by SIN_COS2:def 4;
hence thesis by A1,A2;
end;
theorem Th27:
sinh(2*x) = 2*tanh(x)/(1-(tanh x)^2) & sinh(3*x) = sinh(x)*(4*(
cosh x)^2-1) & sinh(3*x) = 3*sinh(x)-2*sinh(x)*(1-cosh(2*x)) & cosh(2*x) = 1+2*
(sinh x)^2 & cosh(2*x) = (cosh x)^2+(sinh x)^2 & cosh(2*x) = (1+(tanh x)^2)/(1-
(tanh x)^2) & cosh(3*x) = cosh(x)*(4*(sinh x)^2+1) & tanh(3*x) = (3*tanh x+(
tanh x)|^3)/(1+3*(tanh x)^2)
proof
A1: cosh x <> 0 by Lm1;
A2: sinh(2*x) = 2*sinh(x)*cosh(x) by Th26
.= 2*sinh(x)*cosh(x)*(cosh(x)/cosh(x)) by A1,XCMPLX_1:88
.= 2*sinh(x)*cosh(x)*cosh(x)/cosh(x) by XCMPLX_1:74
.= 2*sinh(x)*(cosh(x)*cosh(x))/cosh(x)
.= 2*sinh(x)/cosh(x)*(cosh(x)*cosh(x)) by XCMPLX_1:74
.= 2*(sinh(x)/cosh(x))*(cosh(x)*cosh(x)) by XCMPLX_1:74
.= 2*tanh(x)*(cosh(x)*cosh(x)) by Th1
.= 2*tanh(x)/(1/(cosh(x)*cosh x)) by XCMPLX_1:100
.= 2*tanh(x)/((cosh(x)*cosh(x)-(sinh x)^2)/(cosh(x)*cosh x)) by Lm3
.= 2*tanh(x) / (cosh(x)*cosh(x)/(cosh(x)*cosh(x)) - sinh(x)*sinh(x)/(
cosh(x)*cosh x)) by XCMPLX_1:120
.= 2*tanh(x) / (cosh(x)/cosh(x)*(cosh(x)/cosh(x)) - sinh(x)*sinh(x)/(
cosh(x)*cosh x)) by XCMPLX_1:76
.= 2*tanh(x) / (1*(cosh(x)/cosh(x)) - sinh(x)*sinh(x)/(cosh(x)*cosh x))
by A1,XCMPLX_1:60
.= 2*tanh(x) / (1-sinh(x)*sinh(x)/(cosh(x)*cosh x)) by A1,XCMPLX_1:60
.= 2*tanh(x) / (1-sinh(x)/cosh(x)*(sinh(x)/cosh x)) by XCMPLX_1:76
.= 2*tanh(x) / (1-tanh(x)*(sinh(x)/cosh x)) by Th1
.= 2*tanh(x) / (1-(tanh x)^2) by Th1;
A3: cosh(3*x) = 4*(cosh x)|^(2+1)-3*cosh x by SIN_COS5:44
.= 4*((cosh x)|^2*cosh x)-3*cosh x by NEWTON:6
.= (4*(cosh x)|^(1+1)-3)*cosh x
.= (4*((cosh x)|^1*cosh x)-3)*cosh x by NEWTON:6
.= (4*((cosh x)^2-(sinh x)^2+(sinh x)^2)-3)*cosh x
.= (4*(1+(sinh x)^2)-3)*cosh x by Lm3
.= cosh(x)*(4*(sinh x)^2+1);
A4: cosh(2*x) = 2*((cosh x)^2-(sinh x)^2+(sinh x)^2)-1 by Th26
.= 2*(1+(sinh x)^2)-1 by Lm3
.= 1+2*(sinh x)^2;
A5: tanh(3*x) = tanh(x+x+x)
.= (tanh(x)+tanh(x)+tanh(x)+tanh(x)*tanh(x)*tanh x) /(1+tanh(x)*tanh(x)+
tanh(x)*tanh(x)+tanh(x)*tanh x) by Th21
.= (3*tanh(x)+(tanh(x))|^1*tanh(x)*tanh x)/(1+tanh(x)*tanh(x) +tanh(x)*
tanh(x)+tanh(x)*tanh x)
.= (3*tanh(x)+(tanh(x))|^(1+1)*tanh x)/(1+tanh(x)*tanh x +tanh(x)*tanh(x
)+tanh(x)*tanh x) by NEWTON:6
.= (3*tanh(x)+(tanh x)|^(1+1+1))/(1+tanh(x)*tanh x +tanh(x)*tanh(x)+tanh
(x)*tanh(x)) by NEWTON:6
.= (3*tanh(x)+(tanh x)|^3)/(1+3*(tanh x)^2);
A6: cosh x <> 0 by Lm1;
A7: cosh(2*x) = 2*(cosh x)^2-1 by Th26
.= 2*(cosh x)^2-((cosh x)^2-(sinh x)^2) by Lm3
.= (cosh x)^2+(sinh x)^2;
then
A8: cosh(2*x) = (1/sech x)^2+(sinh x)^2 by Th2
.= 1/(sech x)^2+(sinh x)^2*1^2 by XCMPLX_1:76
.= 1/(sech x)^2+((sinh x)^2/(cosh x)^2)*(cosh x)^2 by A6,XCMPLX_1:6,87
.= 1/(sech x)^2+(sinh x/cosh x)^2*(cosh x)^2 by XCMPLX_1:76
.= 1/(sech x)^2+(tanh x)^2*(cosh x)^2 by Th1
.= 1/(sech x)^2+(tanh x)^2/(1^2/(cosh x)^2) by XCMPLX_1:100
.= 1/(sech x)^2+(tanh x)^2/(1/cosh x)^2 by XCMPLX_1:76
.= 1/(sech x)^2+(tanh x)^2/(sech x)^2 by SIN_COS5:def 2
.= (1+(tanh x)^2)/((sech x)^2+(tanh x)^2-(tanh x)^2) by XCMPLX_1:62
.= (1+(tanh x)^2)/(1-(tanh x)^2) by SIN_COS5:38;
A9: sinh(3*x) = 4*(sinh(x))|^(2+1)+3*sinh x by SIN_COS5:43
.= 4*((sinh x)|^2*sinh x)+3*sinh x by NEWTON:6
.= sinh(x)*(4*(sinh x)|^(1+1)+3)
.= sinh(x)*(4*((sinh x)|^1*sinh x)+3) by NEWTON:6
.= sinh(x)*(4*((cosh x)^2-((cosh x)^2-(sinh x)^2))+3)
.= sinh(x)*(4*((cosh x)^2-1)+3) by Lm3
.= sinh(x)*(4*(cosh x)^2-1);
then sinh(3*x) = sinh(x)*(4*((cosh x)^2-(sinh x)^2+(sinh x)^2))-sinh x
.= sinh(x)*(4*(1+(sinh x)^2))-sinh x by Lm3
.= (4*sinh(x)+sinh(x)*(2*((cosh x)^2-((cosh x)^2-(sinh x)^2)) +2*(sinh x
)^2))-sinh x
.= (4*sinh(x)+sinh(x)*(2*((cosh x)^2-1)+2*(sinh x)^2))-sinh x by Lm3
.= (4*sinh(x)+sinh(x)*(2*((cosh(x)*cosh x) +(sinh x)^2-1)))-sinh x
.= (4*sinh(x)+sinh(x)*(2*(cosh(x+x)-1)))-sinh(x) by Lm10
.= 3*sinh(x)-2*sinh(x)*(1-cosh(2*x));
hence thesis by A2,A9,A4,A7,A8,A3,A5;
end;
theorem
(sinh(5*x)+2*sinh(3*x)+sinh x)/(sinh(7*x)+2*sinh(5*x)+sinh(3*x)) =
sinh(3*x)/sinh(5*x)
proof
(sinh(5*x)+2*sinh(3*x)+sinh(x))/(sinh(7*x)+2*sinh(5*x)+sinh(3*x)) = (
sinh(3*x+2*x)+2*sinh(3*x)+sinh(x)) /(sinh((5+2)*x)+2*sinh(5*x)+sinh(3*x))
.= ((sinh(3*x)*cosh(2*x)+cosh(3*x)*sinh(2*x))+2*sinh(3*x) +sinh(x))/(
sinh((5+2)*x)+2*sinh(5*x)+sinh(3*x)) by Lm10
.= (sinh(3*x)*(cosh(2*x)+2)+(cosh(2*x+1*x)*sinh(2*x)+sinh(x))) /(sinh(5*
x+2*x)+2*sinh(5*x)+sinh(3*x))
.= (sinh(3*x)*(cosh(2*x)+2)+((cosh(2*x)*cosh(x) +sinh(2*x)*sinh(x))*sinh
(2*x)+sinh(x))) /(sinh(5*x+2*x)+2*sinh(5*x)+sinh(3*x)) by Lm10
.= (sinh(3*x)*(cosh(2*x)+2)+(cosh(2*x)*cosh(x)*sinh(2*x) +((sinh(2*x))^2
+1)*sinh(x))) /(sinh(5*x+2*x)+2*sinh(5*x)+sinh(3*x))
.= (sinh(3*x)*(cosh(2*x)+2)+(cosh(2*x)*cosh(x)*sinh(2*x) +(((cosh(2*x))
^2-(sinh(2*x))^2)+(sinh(2*x))^2)*sinh(x))) /(sinh(5*x+2*x)+2*sinh(5*x)+sinh(3*x
)) by Lm3
.= (sinh(3*x)*(cosh(2*x)+2)+(cosh(2*x)*(sinh(2*x)*cosh(x) +cosh(2*x)*
sinh(x))))/(sinh(5*x+2*x)+2*sinh(5*x)+sinh(3*x))
.= (sinh(3*x)*(cosh(2*x)+2)+(cosh(2*x)*sinh(2*x+1*x))) /(sinh(5*x+2*x)+2
*sinh(5*x)+sinh(3*x)) by Lm10
.= sinh(3*x)*((cosh(2*x)+2)+cosh(2*x))/((sinh(5*x)*cosh(2*x) +cosh(5*x)*
sinh(2*x))+sinh(5*x)*2+sinh(3*x)) by Lm10
.= sinh(3*x)*((cosh(2*x)+2)+cosh(2*x))/(sinh(5*x)*(cosh(2*x)+2) +(cosh(3
*x+2*x)*sinh(2*x)+sinh(3*x)))
.= sinh(3*x)*((cosh(2*x)+2)+cosh(2*x))/(sinh(5*x)*(cosh(2*x)+2) +((cosh(
3*x)*cosh(2*x)+sinh(3*x)*sinh(2*x)) *sinh(2*x)+sinh(3*x))) by Lm10
.= sinh(3*x)*((cosh(2*x)+2)+cosh(2*x))/(sinh(5*x)*(cosh(2*x)+2) +(cosh(3
*x)*cosh(2*x)*sinh(2*x)+sinh(3*x)*((sinh(2*x))^2+1)))
.= sinh(3*x)*((cosh(2*x)+2)+cosh(2*x))/(sinh(5*x)*(cosh(2*x)+2) +(cosh(3
*x)*cosh(2*x)*sinh(2*x)+sinh(3*x)*(((cosh(2*x))^2 -(sinh(2*x))^2)+(sinh(2*x))^2
))) by Lm3
.= sinh(3*x)*((cosh(2*x)+2)+cosh(2*x))/(sinh(5*x)*(cosh(2*x)+2) +cosh(2*
x)*(sinh(2*x)*cosh(3*x)+cosh(2*x)*sinh(3*x)))
.= sinh(3*x)*((cosh(2*x)+2)+cosh(2*x))/(sinh(5*x)*(cosh(2*x)+2) +cosh(2*
x)*sinh(2*x+3*x)) by Lm10
.= sinh(3*x)*((cosh(2*x)+2)+cosh(2*x)) /(sinh(5*x)*((cosh(2*x)+2)+cosh(2
*x)))
.= sinh(3*x)/sinh(5*x) by Lm13,XCMPLX_1:91;
hence thesis;
end;
theorem
x >= 0 implies tanh(x/2) = sqrt((cosh(x)-1)/(cosh(x)+1))
proof
assume
A1: x >= 0;
A2: cosh(x)+1 > 0 & cosh(x)-1 >= 0 by Lm13;
tanh(x/2) = sinh(x/2)/cosh(x/2) by Th1
.= sqrt ((cosh(x)-1)/2)/cosh(x/2) by A1,Th24
.= sqrt ((cosh(x)-1)/2)/sqrt((cosh(x)+1)/2) by SIN_COS5:48
.= sqrt (((cosh(x)-1)/2)/((cosh(x)+1)/2)) by A2,SQUARE_1:30
.= sqrt ((cosh(x)-1)/(cosh(x)+1)) by XCMPLX_1:55;
hence thesis;
end;
theorem
x < 0 implies tanh(x/2) = -sqrt((cosh(x)-1)/(cosh(x)+1))
proof
assume
A1: x < 0;
A2: cosh(x)+1 > 0 & cosh(x)-1 >= 0 by Lm13;
tanh(x/2) = sinh(x/2)/cosh(x/2) by Th1
.= (-sqrt ((cosh(x)-1)/2))/cosh(x/2) by A1,Th25
.= -sqrt ((cosh(x)-1)/2)/cosh(x/2) by XCMPLX_1:187
.= -sqrt ((cosh(x)-1)/2)/sqrt((cosh(x)+1)/2) by SIN_COS5:48
.= -sqrt (((cosh(x)-1)/2)/((cosh(x)+1)/2)) by A2,SQUARE_1:30
.= -sqrt ((cosh(x)-1)/(cosh(x)+1)) by XCMPLX_1:55;
hence thesis;
end;
theorem
(sinh x)|^3 = (sinh(3*x)-3*sinh x)/4 & (sinh x)|^4 = (cosh(4*x)-4*cosh
(2*x)+3)/8 & (sinh x)|^5 = (sinh(5*x)-5*sinh(3*x)+10*sinh(x))/16 & (sinh x)|^6
= (cosh(6*x)-6*cosh(4*x)+15*cosh(2*x)-10)/32 & (sinh x)|^7 = (sinh(7*x)-7*sinh(
5*x)+21*sinh(3*x)-35*sinh(x))/64 & (sinh x)|^8 = (cosh(8*x)-8*cosh(6*x)+28*cosh
(4*x)-56*cosh(2*x)+35)/128
proof
A1: (sinh x)|^3 = (4*(sinh(x))|^3+3*sinh(x)-3*sinh(x))/4
.= (sinh(3*x)-3*sinh(x))/4 by SIN_COS5:43;
then
A2: (sinh x)|^4 = (sinh(3*x)-3*sinh(x))/4*sinh(x) by POLYEQ_2:4
.= (sinh(3*x)*sinh(x)-3*(sinh(x)*sinh(x)))/4
.= (1/2*(cosh(3*x+1*x)-cosh(3*x-1*x))-3*(sinh(x)*sinh(x)))/4 by Th11
.= (1/2*(cosh(4*x)-cosh(2*x))-(sinh x)^2*3)/4
.= (1/2*(cosh(4*x)-cosh(2*x))-1/2*(cosh(2*x)-1)*3)/4 by Lm7
.= (cosh(4*x)-4*cosh(2*x)+3)/8;
A3: (sinh x)|^5 = (sinh(x))|^(4+1)
.= (cosh(4*x)-4*cosh(2*x)+3)/8*sinh(x) by A2,NEWTON:6
.= (cosh(4*x)*sinh(x)-4*(cosh(2*x)*sinh(x))+3*sinh(x))/8
.= (1/2*(sinh(4*x+1*x)-sinh(4*x-1*x))-4*(cosh(2*x)*sinh(x)) +3*sinh(x))/
8 by Th11
.= (1/2*(sinh(5*x)-sinh(3*x))-4*(1/2*(sinh(2*x+1*x) -sinh(2*x-1*x)))+3*
sinh(x))/8 by Th11
.= (sinh(5*x)-5*sinh(3*x)+10*sinh(x))/16;
A4: (sinh x)|^6 = (sinh x)|^(5+1)
.= (sinh(5*x)-5*sinh(3*x)+10*sinh(x))/16*sinh(x) by A3,NEWTON:6
.= (sinh(5*x)*sinh(x)-5*(sinh(3*x)*sinh(x)) +10*(sinh(x)*sinh(x)))/16
.= (1/2*(cosh(5*x+1*x)-cosh(5*x-1*x))-5*(sinh(3*x)*sinh(x)) +10*(sinh(x)
*sinh(x)))/16 by Th11
.= (1/2*(cosh(6*x)-cosh(4*x))-1/2*(cosh(3*x+1*x) -cosh(3*x-1*x))*5+10*(
sinh(x)*sinh(x)))/16 by Th11
.= (1/2*(cosh(6*x)-6*cosh(4*x)+cosh(2*x)*5)+10*(sinh x)^2)/16
.= (1/2*(cosh(6*x)-6*cosh(4*x)+cosh(2*x)*5)+1/2*(cosh(2*x)-1)*10)/16 by Lm7
.= (cosh(6*x)-6*cosh(4*x)+15*cosh(2*x)-10)/32;
A5: (sinh x)|^7 = (sinh x)|^(6+1)
.= (cosh(6*x)-6*cosh(4*x)+15*cosh(2*x)-10)/32*sinh(x) by A4,NEWTON:6
.= ((cosh(6*x)*sinh(x)-6*cosh(4*x)*sinh(x) +15*cosh(2*x)*sinh(x)-10*sinh
(x)))/32
.= (1/2*(sinh(6*x+1*x)-sinh(6*x-1*x))-6*cosh(4*x)*sinh(x) +15*cosh(2*x)*
sinh(x)-10*sinh(x))/32 by Th11
.= (1/2*(sinh(7*x)-sinh(5*x))-6*(cosh(4*x)*sinh(x)) +15*cosh(2*x)*sinh(x
)-10*sinh(x))/32
.= (1/2*(sinh(7*x)-sinh(5*x))-6*(1/2*(sinh(4*x+1*x)-sinh(4*x-1*x))) +15*
cosh(2*x)*sinh(x)-10*sinh(x))/32 by Th11
.= (1/2*(sinh(7*x)-7*sinh(5*x)+sinh(3*x)*6) +15*(cosh(2*x)*sinh(x))-10*
sinh(x))/32
.= (1/2*(sinh(7*x)-7*sinh(5*x)+sinh(3*x)*6)+15 *(1/2*(sinh(2*x+1*x)-sinh
(2*x-1*x)))-10*sinh(x))/32 by Th11
.= (sinh(7*x)-7*sinh(5*x)+21*sinh(3*x)-35*sinh(x))/64;
(sinh x)|^8 = (sinh x)|^(7+1)
.= (sinh(7*x)-7*sinh(5*x)+21*sinh(3*x)-35*sinh(x))/64*sinh(x) by A5,
NEWTON:6
.= (sinh(7*x)*sinh(x)-7*(sinh(5*x)*sinh x) +21*(sinh(3*x)*sinh(x))-35*(
sinh(x)*sinh x))/64
.= (1/2*(cosh(7*x+1*x)-cosh(7*x-1*x))-7*(sinh(5*x)*sinh(x)) +21*(sinh(3*
x)*sinh(x))-35*(sinh(x)*sinh x))/64 by Th11
.= (1/2*(cosh(8*x)-cosh(6*x))-(1/2*(cosh(5*x+1*x) -cosh(5*x-1*x))*7)+21*
(sinh(3*x)*sinh x) -35*(sinh(x)*sinh(x)))/64 by Th11
.= (1/2*(cosh(8*x)-8*cosh(6*x)+cosh(4*x)*7)+1/2*(cosh(3*x+1*x) -cosh(3*x
-1*x))*21-35*(sinh(x)*sinh x))/64 by Th11
.= (1/2*(cosh(8*x)-8*cosh(6*x)+28*cosh(4*x)+-cosh(2*x)*21) -35*(sinh x)
^2)/64
.= (1/2*(cosh(8*x)-8*cosh(6*x)+28*cosh(4*x)+-cosh(2*x)*21) -1/2*(cosh(2*
x)-1)*35)/64 by Lm7
.= (cosh(8*x)-8*cosh(6*x)+28*cosh(4*x)-56*cosh(2*x)+35)/128;
hence thesis by A1,A2,A3,A4,A5;
end;
theorem
(cosh x)|^3 = (cosh(3*x)+3*cosh x)/4 & (cosh x)|^4 = (cosh(4*x)+4*cosh
(2*x)+3)/8 & (cosh x)|^5 = (cosh(5*x)+5*cosh(3*x)+10*cosh x)/16 & (cosh x)|^6 =
(cosh(6*x)+6*cosh(4*x)+15*cosh(2*x)+10)/32 & (cosh x)|^7 = (cosh(7*x)+7*cosh(5*
x)+21*cosh(3*x)+35*cosh x)/64 & (cosh x)|^8 = (cosh(8*x)+8*cosh(6*x)+28*cosh(4*
x)+56*cosh(2*x)+35)/128
proof
A1: (cosh x)|^3 = (cosh x)|^(1+1+1) .= (cosh x)|^(1+1)*cosh(x) by NEWTON:6
.= (cosh x)|^1*cosh(x)*cosh(x) by NEWTON:6
.= ((cosh x)^2*cosh(x) + 3*(cosh(x)*((cosh x)^2-(sinh x)^2 +(sinh x)^2))
)/4
.= ((cosh x)^2*cosh(x)+3*(cosh(x)*(1+(sinh x)^2)))/4 by Lm3
.= (cosh(x)*(cosh(x)*cosh(x)+(sinh x)^2)+2*(cosh(x)*(sinh x)^2) + 3*cosh
x)/4
.= (cosh(x)*cosh(x+x)+2*(cosh(x)*(sinh x)^2) + 3*cosh x)/4 by Lm10
.= (cosh(x)*cosh(2*x)+2*sinh(x)*cosh(x)*sinh(x)+3*cosh(x))/4
.= (cosh(2*x)*cosh(x)+sinh(2*x)*sinh(x)+3*cosh(x))/4 by Th26
.= (cosh(x+x+x)+3*cosh x)/4 by Lm10
.= (cosh(3*x)+3*cosh x)/4;
then
A2: (cosh x)|^4 = (cosh(3*x)+3*cosh x)/4*cosh(x) by POLYEQ_2:4
.= (cosh(3*x)*cosh(x)+3*(cosh(x)*cosh x))/4
.= (1/2*(cosh(3*x+1*x)+cosh(3*x-x))+3*(cosh(x)*cosh x))/4 by Th11
.= (1/2*(cosh(4*x)+cosh(2*x))+3*(1/2*(cosh(x+x)+cosh(x-x))))/4 by Th11
.= (1/2*(cosh(4*x)+cosh(2*x))+1/2*(cosh(2*x)+1)*3)/4 by SIN_COS2:15,def 4
.= (cosh(4*x)+4*cosh(2*x)+3)/8;
A3: (cosh x)|^5 = (cosh x)|^(4+1)
.= (cosh(4*x)+4*cosh(2*x)+3)/8*cosh(x) by A2,NEWTON:6
.= (cosh(4*x)*cosh(x)+4*(cosh(2*x)*cosh(x))+3*cosh(x))/8
.= (1/2*(cosh(4*x+1*x)+cosh(4*x-x)) + 4*(cosh(2*x)*cosh(x)) + 3*cosh(x))
/8 by Th11
.= (1/2*(cosh(5*x)+cosh(3*x)) + 4*(1/2*(cosh(2*x+1*x)+cosh(2*x-x))) + 3*
cosh(x))/8 by Th11
.= (cosh(5*x)+5*cosh(3*x)+10*cosh(x))/16;
A4: (cosh x)|^6 = (cosh x)|^(5+1)
.= (cosh(5*x)+5*cosh(3*x)+10*cosh(x))/16*cosh(x) by A3,NEWTON:6
.= (cosh(5*x)*cosh(x)+5*(cosh(3*x)*cosh(x))+10*(cosh(x)*cosh(x)))/16
.= (1/2*(cosh(5*x+x)+cosh(5*x-x))+5*(cosh(3*x)*cosh(x)) + 10*(cosh(x)*
cosh x))/16 by Th11
.= (1/2*(cosh(5*x+x)+cosh(5*x-x)) + 1/2*(cosh(3*x+x)+cosh(3*x-x))*5 + 10
*(cosh(x)*cosh x))/16 by Th11
.= (1/2*(cosh(6*x)+6*cosh(4*x)+cosh(2*x)*5) + 10*(cosh x)^2)/16
.= (1/2*(cosh(6*x)+6*cosh(4*x)+cosh(2*x)*5) + 1/2*(cosh(2*x)+1)*10)/16
by Lm7
.= (cosh(6*x)+6*cosh(4*x)+15*cosh(2*x)+10)/32;
A5: (cosh x)|^7 = (cosh(x))|^(6+1)
.= (cosh(6*x)+6*cosh(4*x)+15*cosh(2*x)+10)/32*cosh(x) by A4,NEWTON:6
.= (cosh(6*x)*cosh(x) + 6*(cosh(4*x)*cosh(x)) + 15*(cosh(2*x)*cosh(x)) +
10*cosh(x))/32
.= (1/2*(cosh(6*x+1*x)+cosh(6*x-1*x)) + 6*(cosh(4*x)*cosh(x)) + 15*(cosh
(2*x)*cosh(x)) + 10*cosh(x))/32 by Th11
.= (1/2*(cosh(7*x)+cosh(5*x)) + 1/2*(cosh(4*x+x)+cosh(4*x-x))*6 + 15*(
cosh(2*x)*cosh(x)) + 10*cosh(x))/32 by Th11
.= (1/2*(cosh(7*x)+7*cosh(5*x)+cosh(3*x)*6) + 1/2*(cosh(2*x+x)+cosh(2*x-
x))*15 + 10*cosh(x))/32 by Th11
.= (cosh(7*x)+7*cosh(5*x)+21*cosh(3*x)+35*cosh(x))/64;
(cosh x)|^8 = (cosh x)|^(7+1)
.= (cosh(7*x)+7*cosh(5*x)+21*cosh(3*x)+35*cosh(x))/64*cosh(x) by A5,
NEWTON:6
.= (cosh(7*x)*cosh(x) + 7*cosh(5*x)*cosh(x) + 21*cosh(3*x)*cosh(x) + 35*
(cosh x)^2)/64
.= (1/2*(cosh(7*x+1*x)+cosh(7*x-x)) + 7*cosh(5*x)*cosh(x) + 21*cosh(3*x)
*cosh(x) + 35*(cosh x)^2)/64 by Th11
.= (1/2*(cosh(8*x)+cosh(6*x)) + 7*(cosh(5*x)*cosh(x)) + 21*cosh(3*x)*
cosh(x) + 35*(cosh x)^2)/64
.= (1/2*(cosh(8*x)+cosh(6*x)) + 7*(1/2*(cosh(5*x+1*x)+cosh(5*x-1*x))) +
21*cosh(3*x)*cosh(x) + 35*(cosh x)^2)/64 by Th11
.= (1/2*(cosh(8*x)+8*cosh(6*x)+cosh(4*x)*7) + 21*(cosh(3*x)*cosh x) + 35
*(cosh x)^2)/64
.= (1/2*(cosh(8*x)+8*cosh(6*x)+cosh(4*x)*7) + 21*(1/2*(cosh(3*x+1*x)+
cosh(3*x-x))) + 35*(cosh x)^2)/64 by Th11
.= (1/2*(cosh(8*x)+8*cosh(6*x)+28*cosh(4*x)+cosh(2*x)*21) + 1/2*(cosh(2*
x)+1)*35)/64 by Lm7
.= (cosh(8*x)+8*cosh(6*x)+28*cosh(4*x)+56*cosh(2*x)+35)/128;
hence thesis by A1,A2,A3,A4,A5;
end;
theorem
cosh(2*y)+cos(2*z) = 2+2*((sinh y)^2-(sin z)^2) & cosh(2*y)-cos(2*z) =
2*((sinh y)^2+(sin z)^2)
proof
A1: cosh(2*y)-cos(2*z) = 1+2*(sinh y)^2-cos(2*z) by Th27
.= 1+2*(sinh y)^2-(1-2*(sin z)^2) by SIN_COS5:7
.= 2*((sinh y)^2+(sin z)^2);
cosh(2*y)+cos(2*z) = 1+2*(sinh y)^2+cos(2*z) by Th27
.= 1+2*(sinh y)^2+(1-2*(sin z)^2) by SIN_COS5:7
.= 2+2*((sinh y)^2-(sin z)^2);
hence thesis by A1;
end;