:: Formulas and Identities of Hyperbolic Functions :: by Pacharapokin Chanapat and Hiroshi Yamazaki :: :: Received November 7, 2005 :: Copyright (c) 2005-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies 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; begin :: Hyperbolic sine, hyperbolic cosine and hyperbolic tangent reserve x, y, z, w for Real; reserve n for Element of NAT; theorem :: SIN_COS8:1 tanh x = sinh(x)/cosh(x) & tanh 0 = 0; theorem :: SIN_COS8:2 sinh x = 1/cosech x & cosh x = 1/sech x & tanh x = 1/coth x; theorem :: SIN_COS8:3 sech x <= 1 & 0 < sech x & sech 0 = 1; theorem :: SIN_COS8:4 x >= 0 implies tanh x >= 0; theorem :: SIN_COS8:5 cosh x = 1/sqrt (1-(tanh x)^2) & sinh x = tanh(x)/sqrt (1-(tanh x)^2); theorem :: SIN_COS8:6 (cosh(x)+sinh(x)) |^ n = cosh(n*x)+sinh(n*x) & (cosh(x)-sinh(x)) |^ n = cosh(n*x)-sinh(n*x); theorem :: SIN_COS8:7 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)); theorem :: SIN_COS8:8 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); theorem :: SIN_COS8:9 (cosh(x)+sinh x)/(cosh(x)-sinh(x)) = (1+tanh(x))/(1-tanh x); theorem :: SIN_COS8:10 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)); theorem :: SIN_COS8:11 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)); theorem :: SIN_COS8:12 (sinh y)^2-(cosh z)^2 = sinh(y+z)*sinh(y-z)-1; theorem :: SIN_COS8:13 (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; theorem :: SIN_COS8:14 (sinh(y)+sinh(z))/(sinh(y)-sinh(z)) = tanh((y+z)/2)*coth((y-z)/2); theorem :: SIN_COS8:15 (cosh(y)+cosh(z))/(cosh(y)-cosh(z)) = coth((y+z)/2)*coth((y-z)/2); theorem :: SIN_COS8:16 y-z <> 0 implies (sinh(y)+sinh(z))/(cosh(y)+cosh(z)) = (cosh(y)-cosh(z ))/(sinh(y)-sinh(z)); theorem :: SIN_COS8:17 y+z <> 0 implies (sinh(y)-sinh(z))/(cosh(y)+cosh(z)) = (cosh(y)-cosh(z ))/(sinh(y)+sinh(z)); theorem :: SIN_COS8:18 (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); theorem :: SIN_COS8:19 (tanh(y)+tanh(z))/(tanh(y)-tanh(z)) = sinh(y+z)/sinh(y-z); theorem :: SIN_COS8:20 (sinh(y-z)+sinh(y)+sinh(y+z))/(cosh(y-z)+cosh(y)+cosh(y+z)) = tanh(y); theorem :: SIN_COS8:21 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); theorem :: SIN_COS8:22 cosh(2*y)+cosh(2*z)+cosh(2*w)+cosh(2*(y+z+w)) = 4*cosh(z+w)*cosh(w+y)* cosh(y+z); theorem :: SIN_COS8:23 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; theorem :: SIN_COS8:24 x >= 0 implies sinh(x/2) = sqrt ((cosh(x)-1)/2); theorem :: SIN_COS8:25 x < 0 implies sinh(x/2) = - sqrt ((cosh(x)-1)/2); theorem :: SIN_COS8:26 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); theorem :: SIN_COS8:27 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); theorem :: SIN_COS8:28 (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); theorem :: SIN_COS8:29 x >= 0 implies tanh(x/2) = sqrt((cosh(x)-1)/(cosh(x)+1)); theorem :: SIN_COS8:30 x < 0 implies tanh(x/2) = -sqrt((cosh(x)-1)/(cosh(x)+1)); theorem :: SIN_COS8:31 (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; theorem :: SIN_COS8:32 (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; theorem :: SIN_COS8:33 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);