:: Formulas and Identities of Hyperbolic Functions :: by Pacharapokin Chanapat and Hiroshi Yamazaki :: :: Received November 7, 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, 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, BOOLE, 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;