:: Formulas And Identities of Inverse Hyperbolic Functions :: by Fuguo Ge , Xiquan Liang and Yuzhong Ding :: :: Received May 24, 2005 :: Copyright (c) 2005-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, POWER, SQUARE_1, ARYTM_3, RELAT_1, CARD_1, XXREAL_0, ARYTM_1, COMPLEX1, SIN_COS, FUNCT_3, POLYEQ_1, SIN_COS2, FUNCT_1, NEWTON, SIN_COS7, REAL_1; notations ORDINAL1, FUNCT_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, SQUARE_1, NEWTON, QUIN_1, COMPLEX1, SIN_COS, SIN_COS2, POWER, POLYEQ_1; constructors REAL_1, SQUARE_1, NAT_1, BINOP_2, QUIN_1, POWER, POLYEQ_1, SIN_COS, SIN_COS2, VALUED_1, NEWTON; registrations XXREAL_0, XREAL_0, SQUARE_1, QUIN_1, SIN_COS, VALUED_0, RELSET_1, SIN_COS2, NEWTON, XCMPLX_0, NAT_1, ORDINAL1; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin reserve x,y,t for Real; theorem :: SIN_COS7:1 x>0 implies 1/x=x to_power (-1); theorem :: SIN_COS7:2 x>1 implies ((sqrt(x^2-1))/x)^2<1; theorem :: SIN_COS7:3 (x/sqrt(x^2+1))^2<1; theorem :: SIN_COS7:4 sqrt(x^2+1)>0; theorem :: SIN_COS7:5 sqrt(x^2+1)+x>0; theorem :: SIN_COS7:6 y>=0 & x>=1 implies (x+1)/y>=0; theorem :: SIN_COS7:7 y>=0 & x>=1 implies (x-1)/y>=0; theorem :: SIN_COS7:8 x>=1 implies sqrt((x+1)/2)>=1; theorem :: SIN_COS7:9 y>=0 & x>=1 implies (x^2-1)/y>=0; theorem :: SIN_COS7:10 x>=1 implies sqrt((x+1)/2)+sqrt((x-1)/2)>0; theorem :: SIN_COS7:11 x^2<1 implies x+1>0 & 1-x>0; theorem :: SIN_COS7:12 x<>1 implies (1-x)^2>0; theorem :: SIN_COS7:13 x^2<1 implies (x^2+1)/(1-x^2)>=0; theorem :: SIN_COS7:14 x^2<1 implies ((2*x)/(1+x^2))^2<1; theorem :: SIN_COS7:15 00; theorem :: SIN_COS7:16 01; theorem :: SIN_COS7:18 00; theorem :: SIN_COS7:19 01; theorem :: SIN_COS7:21 1=0; theorem :: SIN_COS7:23 1<=x implies 0-1; theorem :: SIN_COS7:28 x^2<1 & y^2<1 implies x*y<>1; theorem :: SIN_COS7:29 x<>0 implies exp_R(x)<>1; theorem :: SIN_COS7:30 0<>x implies (exp_R x)^2-1<>0; theorem :: SIN_COS7:31 (t^2-1)/(t^2+1)<1; theorem :: SIN_COS7:32 -1 Real equals :: SIN_COS7:def 1 log(number_e,(x+sqrt(x^2+1))); end; definition let x be Real; func cosh1"(x) -> Real equals :: SIN_COS7:def 2 log(number_e,x+sqrt(x^2-1)); end; definition let x be Real; func cosh2"(x) -> Real equals :: SIN_COS7:def 3 -(log(number_e,x+sqrt(x^2-1))); end; definition let x be Real; func tanh"(x) -> Real equals :: SIN_COS7:def 4 (1/2)*log(number_e,(1+x)/(1-x)); end; definition let x be Real; func coth"(x) -> Real equals :: SIN_COS7:def 5 (1/2)*log(number_e,(x+1)/(x-1)); end; definition let x be Real; func sech1"(x) -> Real equals :: SIN_COS7:def 6 log(number_e,(1+sqrt(1-x^2))/x); end; definition let x be Real; func sech2"(x) -> Real equals :: SIN_COS7:def 7 -(log(number_e,(1+sqrt(1-x^2))/x)); end; definition let x be Real; func csch"(x) -> Real equals :: SIN_COS7:def 8 log(number_e,(1+sqrt(1+x^2))/x) if 0=1 implies cosh1"(x)=sinh"(sqrt(x^2-1)); theorem :: SIN_COS7:37 x>1 implies cosh1"(x)=tanh"((sqrt(x^2-1))/x); theorem :: SIN_COS7:38 x>=1 implies cosh1"(x)=2*cosh1"(sqrt((x+1)/2)); theorem :: SIN_COS7:39 x>=1 implies cosh2"(x)=2*cosh2"(sqrt((x+1)/2)); theorem :: SIN_COS7:40 x>=1 implies cosh1"(x)=2*sinh"(sqrt((x-1)/2)); theorem :: SIN_COS7:41 x^2<1 implies tanh"(x)=sinh"(x/sqrt(1-x^2)); theorem :: SIN_COS7:42 00 & x<1 implies tanh"(x)=(1/2)*cosh1"((1+x^2)/(1-x^2)); theorem :: SIN_COS7:45 x^2<1 implies tanh"(x)=(1/2)*tanh"((2*x)/(1+x^2)); theorem :: SIN_COS7:46 x^2>1 implies coth"(x)=tanh"(1/x); theorem :: SIN_COS7:47 x>0 & x<=1 implies sech1"(x)=cosh1"(1/x); theorem :: SIN_COS7:48 x>0 & x<=1 implies sech2"(x)=cosh2"(1/x); theorem :: SIN_COS7:49 x>0 implies csch"(x)=sinh"(1/x); theorem :: SIN_COS7:50 (x*y+sqrt(x^2+1)*sqrt(y^2+1))>=0 implies sinh"(x)+sinh"(y)=sinh"(x* sqrt(1+y^2)+y*sqrt(1+x^2)); theorem :: SIN_COS7:51 sinh"(x)-sinh"(y)=sinh"(x*sqrt(1+y^2)-y*sqrt(1+x^2)); theorem :: SIN_COS7:52 1<=x & 1<=y implies cosh1"(x)+cosh1"(y)=cosh1"(x*y+sqrt((x^2-1)*(y^2-1 ))); theorem :: SIN_COS7:53 1<=x & 1<=y implies cosh2"(x)+cosh2"(y)=cosh2"(x*y+sqrt((x^2-1)*(y^2-1 ))); theorem :: SIN_COS7:54 1<=x & 1<=y & |.y.|<=|.x.| implies cosh1"(x)-cosh1"(y)=cosh1"(x*y- sqrt((x^2-1)*(y^2-1))); theorem :: SIN_COS7:55 1<=x & 1<=y & |.y.|<=|.x.| implies cosh2"(x)-cosh2"(y)=cosh2"(x*y- sqrt((x^2-1)*(y^2-1))); theorem :: SIN_COS7:56 x^2<1 & y^2<1 implies tanh"(x)+tanh"(y)=tanh"((x+y)/(1+x*y)); theorem :: SIN_COS7:57 x^2<1 & y^2<1 implies tanh"(x)-tanh"(y)=tanh"((x-y)/(1-x*y)); theorem :: SIN_COS7:58 00 implies x=(1/2)*log (number_e,(y+1)/(y-1)); theorem :: SIN_COS7:67 y=1/((exp_R(x)+exp_R(-x))/2) implies x=log(number_e,(1+sqrt(1-y^2))/y) or x=-log(number_e,(1+sqrt(1-y^2))/y); theorem :: SIN_COS7:68 y=1/((exp_R(x)-exp_R(-x))/2) & x<>0 implies x=log(number_e,(1+sqrt(1+y ^2))/y) or x=log(number_e,(1-sqrt(1+y^2))/y); theorem :: SIN_COS7:69 cosh.(2*x)=1+2*(sinh.x)^2; theorem :: SIN_COS7:70 (cosh.x)^2=1+(sinh.x)^2; theorem :: SIN_COS7:71 (sinh.x)^2=(cosh.x)^2-1; theorem :: SIN_COS7:72 sinh(5*x)=5*sinh(x)+20*(sinh(x))|^3+16*(sinh(x))|^5; theorem :: SIN_COS7:73 cosh(5*x)=5*cosh(x)-20*(cosh(x))|^3+16*(cosh(x))|^5;