SIN_COS7

:: Formulas And Identities of Inverse Hyperbolic Functions
::  by Fuguo Ge , Xiquan Liang and Yuzhong Ding
::
:: Received May 24, 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, 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, ARITHM;
 equalities SQUARE_1, XCMPLX_0;
 theorems SQUARE_1, ABSVALUE, SIN_COS, NEWTON, XCMPLX_1, QUIN_1, SIN_COS2,
      TAYLOR_1, POWER, POLYEQ_1, XREAL_1, COMPLEX1, ASYMPT_1, XXREAL_0;

begin

reserve x,y,t for Real;

Lm1: number_e<>1 by TAYLOR_1:11;

Lm2: x^2<1 & y<1 implies x^2*y<1
proof
  assume that
A1: x^2<1 and
A2: y<1;
  per cases by XREAL_1:63;
  suppose
    0=x^2;
    hence thesis;
  end;
  suppose
    0<x^2;
    then y*x^2<1*x^2 by A2,XREAL_1:68;
    hence thesis by A1,XXREAL_0:2;
  end;
end;

theorem Th1:
  x>0 implies 1/x=x to_power (-1)
proof
  assume x>0;
  then x to_power (-1) =(1/x) to_power 1 by POWER:32
    .=1/x by POWER:25;
  hence thesis;
end;

theorem
  x>1 implies ((sqrt(x^2-1))/x)^2<1
proof
A1: -1+x^2<0+x^2 by XREAL_1:6;
  assume x>1;
  then x^2>1^2+0 by SQUARE_1:16;
  then
A2: x^2-1>0 by XREAL_1:20;
  ((sqrt(x^2-1))/x)^2=(sqrt(x^2-1))^2/x^2 by XCMPLX_1:76
    .=(x^2-1)/x^2 by A2,SQUARE_1:def 2;
  hence thesis by A2,A1,XREAL_1:189;
end;

theorem
  (x/sqrt(x^2+1))^2<1
proof
A1: x^2<x^2+1 by XREAL_1:29;
A2: x^2>=0 by XREAL_1:63;
  then (sqrt(x^2+1))^2=sqrt(x^2+1)^2 by SQUARE_1:29
    .=x^2+1 by A2,SQUARE_1:22;
  then
A3: (x/sqrt(x^2+1))^2=(x^2)/(x^2+1) by XCMPLX_1:76;
  per cases by XREAL_1:63;
  suppose
    x^2>0;
    hence thesis by A1,A3,XREAL_1:189;
  end;
  suppose
    x^2=0;
    hence thesis;
  end;
end;

theorem Th4:
  sqrt(x^2+1)>0
proof
  x^2>=0 by XREAL_1:63;
  hence thesis by SQUARE_1:25;
end;

theorem Th5:
  sqrt(x^2+1)+x>0
proof
  per cases;
  suppose
    x>0;
    hence thesis by Th4,XREAL_1:29;
  end;
  suppose
A1: x<=0;
    x^2<x^2+1 by XREAL_1:29;
    then sqrt(x^2)<sqrt(x^2+1) by SQUARE_1:27,XREAL_1:63;
    then -x<sqrt(x^2+1) by A1,SQUARE_1:23;
    hence thesis by XREAL_1:62;
  end;
end;

Lm3: 1<=x implies x^2-1>=0
proof
  assume 1<=x;
  then x^2>=1^2 by SQUARE_1:15;
  then 1+(-1)<=x^2+(-1) by XREAL_1:6;
  hence thesis;
end;

theorem
  y>=0 & x>=1 implies (x+1)/y>=0;

theorem Th7:
  y>=0 & x>=1 implies (x-1)/y>=0
proof
  assume that
A1: y>=0 and
A2: x>=1;
  x+(-1)>=1+(-1) by A2,XREAL_1:6;
  hence thesis by A1;
end;

theorem Th8:
  x>=1 implies sqrt((x+1)/2)>=1
proof
  assume x>=1;
  then x+1>=1+1 by XREAL_1:6;
  then (x+1)/2>=1 by XREAL_1:181;
  hence thesis by SQUARE_1:18,26;
end;

theorem Th9:
  y>=0 & x>=1 implies (x^2-1)/y>=0
proof
  assume that
A1: y>=0 and
A2: x>=1;
  x^2-1>=0 by A2,Lm3;
  hence thesis by A1;
end;

theorem Th10:
  x>=1 implies sqrt((x+1)/2)+sqrt((x-1)/2)>0
proof
  assume
A1: x>=1;
  then (x-1)/2>=0 by Th7;
  then
A2: sqrt((x-1)/2)>=0 by SQUARE_1:17,26;
  sqrt((x+1)/2)>=1 by A1,Th8;
  hence thesis by A2;
end;

theorem Th11:
  x^2<1 implies x+1>0 & 1-x>0
proof
  assume x^2<1;
  then -1<x & x<1 by SQUARE_1:52;
  hence thesis by XREAL_1:148,149;
end;

Lm4: x^2<1 implies (x+1)/(1-x)>0
proof
  assume x^2<1;
  then x+1>0 & 1-x>0 by Th11;
  hence thesis;
end;

theorem Th12:
  x<>1 implies (1-x)^2>0
proof
  assume x<>1;
  then 0<>1-x;
  hence thesis by SQUARE_1:12;
end;

theorem Th13:
  x^2<1 implies (x^2+1)/(1-x^2)>=0
proof
  assume x^2<1;
  then
A1: 0<1-x^2 by XREAL_1:50;
  x^2>=0 by XREAL_1:63;
  hence thesis by A1;
end;

theorem
  x^2<1 implies ((2*x)/(1+x^2))^2<1
proof
  assume x^2<1;
  then x^2+(-1)<1+(-1) by XREAL_1:8;
  then (x^2-1)*(x^2-1)>0*(x^2-1);
  then
A1: x^2>=0 & (x^2)^2-2*(x^2)+1+4*x^2>0+4*x^2 by XREAL_1:8,63;
  ((2*x)/(1+x^2))^2 = (2*x)^2/(1+x^2)^2 by XCMPLX_1:76
    .=4*x^2/((x^2)^2+2*(x^2)+1);
  hence thesis by A1,XREAL_1:189;
end;

theorem Th15:
  0<x & x<1 implies (1+x)/(1-x)>0
proof
  assume that
A1: 0<x and
A2: x<1;
  x^2<x by A1,A2,SQUARE_1:13;
  then x^2<1 by A2,XXREAL_0:2;
  hence thesis by Lm4;
end;

theorem
  0<x & x<1 implies x^2<1
proof
  assume that
A1: 0<x and
A2: x<1;
  x^2<x by A1,A2,SQUARE_1:13;
  hence thesis by A2,XXREAL_0:2;
end;

Lm5: 0<x & x<1 implies 0<1-x^2
proof
  assume that
A1: 0<x and
A2: x<1;
  x^2<x by A1,A2,SQUARE_1:13;
  then x^2<1 by A2,XXREAL_0:2;
  then x^2-x^2<1-x^2 by XREAL_1:9;
  hence thesis;
end;

theorem
  0<x & x<1 implies 1/(sqrt(1-x^2))>1
proof
  assume that
A1: 0<x and
A2: x<1;
A3: 0<1-x^2 by A1,A2,Lm5;
  then
A4: 0<sqrt(1-x^2) by SQUARE_1:25;
  x*x>0*x by A1;
  then x^2*(-1)<0*(-1);
  then -x^2+1<0+1 by XREAL_1:8;
  then sqrt(1-x^2)<1 by A3,SQUARE_1:18,27;
  hence thesis by A4,XREAL_1:187;
end;

theorem Th18:
  0<x & x<1 implies (2*x)/(1-x^2)>0
proof
  assume that
A1: 0<x and
A2: x<1;
  x^2<x by A1,A2,SQUARE_1:13;
  then x^2<1 by A2,XXREAL_0:2;
  then
A3: x^2+(-x^2)<1+(-x^2) by XREAL_1:8;
  0*2<x*2 by A1;
  hence thesis by A3;
end;

theorem Th19:
  0<x & x<1 implies 0<(1-x^2)^2
proof
  assume that
A1: 0<x and
A2: x<1;
  x^2<x by A1,A2,SQUARE_1:13;
  then x^2<1 by A2,XXREAL_0:2;
  then x^2+(-x^2)<1+(-x^2) by XREAL_1:8;
  hence thesis;
end;

theorem
  0<x & x<1 implies ((1+x^2)/(1-x^2))>1
proof
  assume that
A1: 0<x and
A2: x<1;
  x^2<x by A1,A2,SQUARE_1:13;
  then x^2<1 by A2,XXREAL_0:2;
  then
A3: x^2+(-x^2)<1+(-x^2) by XREAL_1:8;
  0*x<x*x by A1;
  then -x^2+1<x^2+1 by XREAL_1:8;
  hence thesis by A3,XREAL_1:187;
end;

theorem
  1<x^2 implies (1/x)^2<1
proof
  assume
A1: 1<x^2;
  then (1/x^2)<((x^2)/(x^2)) by XREAL_1:74;
  then (1^2/x^2)<1 by A1,XCMPLX_1:60;
  hence thesis by XCMPLX_1:76;
end;

theorem Th22:
  0<x & x<=1 implies 1-x^2>=0
proof
  assume that
A1: 0<x and
A2: x<=1;
A3: x-1<=1-1 by A2,XREAL_1:9;
  per cases by A3;
  suppose
    x-1<0;
    then x-1+1<0+1 by XREAL_1:8;
    hence thesis by A1,Lm5;
  end;
  suppose
    x-1=0;
    hence thesis;
  end;
end;

theorem Th23:
  1<=x implies 0<x+sqrt(x^2-1)
proof
  assume
A1: 1<=x;
  then x^2-1>=0 by Lm3;
  then 0<=sqrt(x^2-1) by SQUARE_1:def 2;
  hence thesis by A1;
end;

theorem Th24:
  1<=x & 1<=y implies 0<=x*sqrt(y^2-1)+y*sqrt(x^2-1)
proof
  assume that
A1: 1<=x and
A2: 1<=y;
  0<=y^2-1 by A2,Lm3;
  then
A3: 0<=sqrt(y^2-1) by SQUARE_1:def 2;
  0<=x^2-1 by A1,Lm3;
  then 0<=sqrt(x^2-1) by SQUARE_1:def 2;
  hence thesis by A1,A2,A3;
end;

theorem Th25:
  1<=y implies 0<y-sqrt(y^2-1)
proof
  assume
A1: 1<=y;
  then 1*y<=y*y by XREAL_1:64;
  then 1<=y^2 by A1,XXREAL_0:2;
  then
A2: 1-1<=y^2-1 by XREAL_1:13;
  -1+y^2<0+y^2 by XREAL_1:8;
  then sqrt(y^2-1)<sqrt(y^2) by A2,SQUARE_1:27;
  then sqrt(y^2-1)<y by A1,SQUARE_1:22;
  then sqrt(y^2-1)-sqrt(y^2-1)<y-sqrt(y^2-1) by XREAL_1:14;
  hence thesis;
end;

theorem Th26:
  1<=x & 1<=y & |.y.|<=|.x.| implies 0<=y*sqrt(x^2-1)-x*sqrt(y^2 -1)
proof
  assume that
A1: 1<=x and
A2: 1<=y and
A3: |.y.|<=|.x.|;
A4: 0<=y^2-1 by A2,Lm3;
A5: |.x.|^2=x^2 & |.y.|^2=y^2 by COMPLEX1:75;
  1<=|.y.| by A2,ABSVALUE:def 1;
  then y^2<=x^2 by A3,A5,SQUARE_1:15;
  then (-1)*x^2<=(-1)*y^2 by XREAL_1:65;
  then -x^2+x^2*y^2<=-y^2+x^2*y^2 by XREAL_1:6;
  then 0<=x^2 & sqrt(x^2*(y^2-1))<=sqrt(y^2*(x^2-1)) by A1,A4,SQUARE_1:26;
  then sqrt(x^2)*sqrt(y^2-1)<=sqrt(y^2*(x^2-1)) by A4,SQUARE_1:29;
  then
A6: x*sqrt(y^2-1)<=sqrt(y^2*(x^2-1)) by A1,SQUARE_1:22;
  0<=y^2 & 0<=x^2-1 by A1,Lm3,XREAL_1:63;
  then x*sqrt(y^2-1)<=sqrt(y^2)*sqrt(x^2-1) by A6,SQUARE_1:29;
  then x*sqrt(y^2-1)<=y*sqrt(x^2-1) by A2,SQUARE_1:22;
  then x*sqrt(y^2-1)-x*sqrt(y^2-1)<=y*sqrt(x^2-1)-x*sqrt(y^2-1) by XREAL_1:13;
  hence thesis;
end;

theorem Th27:
  x^2<1 & y^2<1 implies x*y<>-1
proof
  assume
A1: x^2<1 & y^2<1;
  assume x*y=-1;
  then x*y*(x*y)=1;
  then (x*x)*(y*y)=1;
  hence contradiction by A1,Lm2;
end;

theorem Th28:
  x^2<1 & y^2<1 implies x*y<>1
proof
  assume
A1: x^2<1 & y^2<1;
  assume x*y=1;
  then x*y*(x*y)=1;
  then (x*x)*(y*y)=1;
  hence contradiction by A1,Lm2;
end;

theorem Th29:
  x<>0 implies exp_R(x)<>1
proof
  assume
A1: x<>0;
  assume
A2: exp_R(x)=1;
  x=log(number_e,exp_R(x)) by TAYLOR_1:12
    .=0 by A2,Lm1,POWER:51,TAYLOR_1:11;
  hence contradiction by A1;
end;

theorem Th30:
  0<>x implies (exp_R x)^2-1<>0
proof
  assume
A1: 0<>x;
  assume (exp_R x)^2-1=0;
  then exp_R x=1 or exp_R x= -1 by XCMPLX_1:182;
  hence contradiction by A1,Th29,SIN_COS:55;
end;

Lm6: x^2+1>0
proof
  x^2>=0 by XREAL_1:63;
  hence thesis;
end;

theorem Th31:
  (t^2-1)/(t^2+1)<1
proof
A1: 0<t^2+1 by Lm6;
  -1+t^2<1+t^2 by XREAL_1:8;
  then (-1+t^2)/((1+t^2))<(1+t^2)/((1+t^2)) by A1,XREAL_1:74;
  hence thesis by A1,XCMPLX_1:60;
end;

theorem Th32:
  -1<t & t<1 implies 0<(t+1)/(1-t)
proof
  assume -1<t & t<1;
  then -1+1<t+1 & t-t<1-t by XREAL_1:8;
  then 0/(1-t)<(t+1)/(1-t);
  hence thesis;
end;

Lm7: 1<t or t< -1 implies 0<(t+1)/(t-1)
proof
  assume
A1: 1<t or t < -1;
  per cases by A1;
  suppose
A2: 1<t;
    then 1-1<t-1 by XREAL_1:14;
    then 0/(t-1)<(t+1)/(t-1) by A2;
    hence thesis;
  end;
  suppose
A3: t< -1;
    then t+1< -1+1 by XREAL_1:8;
    then 0/(t-1)<(t+1)/(t-1) by A3;
    hence thesis;
  end;
end;

Lm8: sqrt(x^2+1)>x
proof
  per cases;
  suppose
A1: x>=0;
    x^2+1>x^2+0 by XREAL_1:8;
    then sqrt(x^2+1)>sqrt(x^2) by SQUARE_1:27,XREAL_1:63;
    hence thesis by A1,SQUARE_1:22;
  end;
  suppose
    x<0;
    hence thesis by Th4;
  end;
end;

Lm9: sqrt(x^2+1)*sqrt(y^2+1)-x*y>0
proof
A1: y^2+1>0 by Lm6;
  assume (sqrt(x^2+1)*sqrt(y^2+1))-x*y<=0;
  then
A2: sqrt(x^2+1)*sqrt(y^2+1)<=x*y by XREAL_1:50;
  sqrt(x^2+1)>0 & sqrt(y^2+1)>0 by Th4;
  then (sqrt(x^2+1)*sqrt(y^2+1))^2<=(x*y)^2 by A2,SQUARE_1:15;
  then
A3: (sqrt(x^2+1))^2*(sqrt(y^2+1))^2<=(x*y)^2;
  x^2+1>0 by Lm6;
  then (x^2+1)*(sqrt(y^2+1))^2<=(x*y)^2 by A3,SQUARE_1:def 2;
  then (x^2+1)*(y^2+1)<=(x*y)^2 by A1,SQUARE_1:def 2;
  then
A4: (x*y)^2+x^2+y^2+1-(x*y)^2<=(x*y)^2-(x*y)^2 by XREAL_1:13;
  0<=x^2 & 0<=y^2 by XREAL_1:63;
  then 0+1<=x^2+y^2+1 by XREAL_1:6;
  hence contradiction by A4;
end;

Lm10: 1<=y implies y+sqrt(y^2-1)>0
proof
  assume
A1: 1<=y;
  then 0<=y^2-1 by Lm3;
  then 0<=sqrt(y^2-1) by SQUARE_1:def 2;
  hence thesis by A1;
end;

Lm11: 0<t implies -1<(t^2-1)/(t^2+1)
proof
A1: 0<t^2+1 by Lm6;
  assume 0<t;
  then 0<t^2;
  then 0*2<2*t^2;
  then 0-(t^2+1)<2*t^2-(t^2+1) by XREAL_1:14;
  then (-(t^2+1))/(t^2+1)<(t^2-1)/(t^2+1) by A1,XREAL_1:74;
  then -(t^2+1)/(t^2+1)<(t^2-1)/(t^2+1);
  hence thesis by A1,XCMPLX_1:60;
end;

Lm12: 0<t & t<>1 implies 1<(t^2+1)/(t^2-1) or (t^2+1)/(t^2-1)< -1
proof
  assume that
A1: 0<t and
A2: t<>1;
  1<t or t<1 by A2,XXREAL_0:1;
  then
A3: 1-1<t-1 or t-1<1-1 by XREAL_1:14;
  per cases by A3;
  suppose
    0<t-1;
    then
A4: 0+1<t-1+1 by XREAL_1:8;
    then t<t^2 by SQUARE_1:14;
    then 1<t^2 by A4,XXREAL_0:2;
    then
A5: 1-1<t^2-1 by XREAL_1:14;
    -1+t^2<1+t^2 by XREAL_1:8;
    hence thesis by A5,XREAL_1:187;
  end;
  suppose
    t-1<0;
    then
A6: t-1+1<0+1 by XREAL_1:8;
    then t^2<t by A1,SQUARE_1:13;
    then t^2<1 by A6,XXREAL_0:2;
    then
A7: t^2-t^2<1-t^2 by XREAL_1:14;
    0<t^2 by A1;
    then -t^2+1<t^2+1 by XREAL_1:8;
    then 1<(t^2+1)/(1-t^2) by A7,XREAL_1:187;
    then (-1)*((t^2+1)/(1-t^2))<1*(-1) by XREAL_1:69;
    then (-(t^2+1))/(1-t^2)<1*(-1);
    then (t^2+1)/(-(1-t^2))<1*(-1) by XCMPLX_1:192;
    hence thesis;
  end;
end;

Lm13: 0<t implies 0<2*t/(1+t^2);

Lm14: 0<t implies 2*t/(1+t^2)<=1
proof
  0<=(t-1)^2 by XREAL_1:63;
  then
A1: 0+2*t<=t^2-2*t+1+2*t by XREAL_1:6;
  assume 0<t;
  hence thesis by A1,XREAL_1:183;
end;

Lm15: 0<t implies (1-sqrt(1+t^2))/t<0
proof
  assume
A1: 0<t;
  then 0+1<t^2+1 by XREAL_1:8;
  then 1<sqrt(t^2+1) by SQUARE_1:18,27;
  then -sqrt(t^2+1)< -1 by XREAL_1:24;
  then -sqrt(t^2+1)+1< -1+1 by XREAL_1:8;
  then (1-sqrt(t^2+1))/t<0/t by A1;
  hence thesis;
end;

Lm16: 0<t & t<=1 implies 0<=1-t^2
proof
  assume 0<t & t<=1;
  then t^2<=1^2 by SQUARE_1:15;
  then t^2-t^2<=1-t^2 by XREAL_1:13;
  hence thesis;
end;

Lm17: 0<t & t<=1 implies 0<=4-4*t^2
proof
  assume 0<t & t<=1;
  then 0<=1-t^2 by Lm16;
  then 0*4<=4*(1-t^2);
  hence thesis;
end;

Lm18: 0<t & t<=1 implies 0<1+sqrt(1-t^2)
proof
  assume 0<t & t<=1;
  then 0<=1-t^2 by Lm16;
  then 0<=sqrt(1-t^2) by SQUARE_1:17,26;
  hence thesis;
end;

Lm19: 0<t & t<=1 implies 0<(1+sqrt(1-t^2))/t
proof
  assume that
A1: 0<t and
A2: t<=1;
  0<1+sqrt(1-t^2) by A1,A2,Lm18;
  then 0/t<(1+sqrt(1-t^2))/t by A1;
  hence thesis;
end;

Lm20: 0<t & t<>1 implies 2*t/(t^2-1)<>0
proof
  assume that
A1: 0<t and
A2: t<>1;
  per cases by A2,XXREAL_0:1;
  suppose
A3: 1<t;
    then t<t^2 by SQUARE_1:14;
    then 1<t^2 by A3,XXREAL_0:2;
    then
A4: 1-1<t^2-1 by XREAL_1:14;
    2*1<2*t by A3,XREAL_1:68;
    then 0/(t^2-1)<2*t/(t^2-1) by A4;
    hence thesis;
  end;
  suppose
A5: t<1;
    then t^2<t by A1,SQUARE_1:13;
    then t^2<1 by A5,XXREAL_0:2;
    then
A6: t^2-1<1-1 by XREAL_1:14;
    0*2<2*t by A1;
    then 2*t/(t^2-1)<0/(t^2-1) by A6;
    hence thesis;
  end;
end;

Lm21: t<0 implies (1+sqrt(1+t^2))/t<0
proof
  assume
A1: t<0;
  0+1<(sqrt(1+t^2))+1 by Th4,XREAL_1:8;
  then (1+sqrt(1+t^2))/t<0/t by A1;
  hence thesis;
end;

begin :: Main Part

definition
  let x be Real;
  func sinh"(x) -> Real equals
  log(number_e,(x+sqrt(x^2+1)));
  coherence;
end;

definition
  let x be Real;
  func cosh1"(x) -> Real equals
  log(number_e,x+sqrt(x^2-1));
  coherence;
end;

definition
  let x be Real;
  func cosh2"(x) -> Real equals
  -(log(number_e,x+sqrt(x^2-1)));
  coherence;
end;

definition
  let x be Real;
  func tanh"(x) -> Real equals
  (1/2)*log(number_e,(1+x)/(1-x));
  coherence;
end;

definition
  let x be Real;
  func coth"(x) -> Real equals
  (1/2)*log(number_e,(x+1)/(x-1));
  coherence;
end;

definition
  let x be Real;
  func sech1"(x) -> Real equals
  log(number_e,(1+sqrt(1-x^2))/x);
  coherence;
end;

definition
  let x be Real;
  func sech2"(x) -> Real equals
  -(log(number_e,(1+sqrt(1-x^2))/x));
  coherence;
end;

definition
  let x be Real;
  func csch"(x) -> Real equals
  :Def8:
  log(number_e,(1+sqrt(1+x^2))/x)
  if 0<x, log(number_e,(1-sqrt(1+x^2))/x) if x<0;
  correctness;
end;

theorem
  0<=x implies sinh"(x)=cosh1"(sqrt(x^2+1))
proof
  assume
A1: 0<=x;
  x^2>=0 by XREAL_1:63;
  then cosh1"(sqrt(x^2+1)) =log(number_e,sqrt(x^2+1)+sqrt(x^2+1-1)) by
SQUARE_1:def 2
    .=log(number_e,(sqrt(x^2+1)+x)) by A1,SQUARE_1:22;
  hence thesis;
end;

theorem
  x<0 implies sinh"(x)=cosh2"(sqrt(x^2+1))
proof
  assume
A1: x<0;
A2: sqrt(x^2+1)+x>0 by Th5;
A3: 1/(sqrt(x^2+1)+x)=(sqrt(x^2+1)+x) to_power (-1) by Th1,Th5;
A4: x^2>=0 by XREAL_1:63;
  then cosh2"(sqrt(x^2+1)) =-log(number_e,sqrt(x^2+1)+sqrt(x^2+1-1)) by
SQUARE_1:def 2
    .=-log(number_e,(sqrt(x^2+1)+(-x))) by A1,SQUARE_1:23
    .=-log(number_e,(sqrt(x^2+1)-x)*(sqrt(x^2+1)+x)/(sqrt(x^2+1)+x)) by A2,
XCMPLX_1:89
    .=-log(number_e,((sqrt(x^2+1))^2-x^2)/(sqrt(x^2+1)+x))
    .=-log(number_e,((x^2+1)-x^2)/(sqrt(x^2+1)+x)) by A4,SQUARE_1:def 2
    .=-((-1)*log(number_e,(sqrt(x^2+1)+x))) by A2,A3,Lm1,POWER:55,TAYLOR_1:11
    .=log(number_e,(sqrt(x^2+1)+x));
  hence thesis;
end;

theorem
  sinh"(x)=tanh"(x/sqrt(x^2+1))
proof
  set t = sqrt(x^2+1)+x;
A1: sqrt(x^2+1)+x>0 by Th5;
A2: x^2+1>0 by Lm6;
A3: sqrt(x^2+1)>0 by Th4;
  then
  tanh"(x/sqrt(x^2+1)) =(1/2)*log(number_e,((sqrt(x^2+1)*1+x)/sqrt(x^2+1))
  /(1-x/sqrt(x^2+1))) by XCMPLX_1:113
    .=(1/2)*log(number_e,((sqrt(x^2+1)*1+x)/sqrt(x^2+1))/((1*sqrt(x^2+1)-x)
  /sqrt(x^2+1))) by A3,XCMPLX_1:127
    .=(1/2)*log(number_e,t/(sqrt(x^2+1)-x)) by A3,XCMPLX_1:55
    .=(1/2)*log(number_e,t*t/((sqrt(x^2+1)-x)*t)) by A1,XCMPLX_1:91
    .=(1/2)*log(number_e,(t*t)/((sqrt(x^2+1))*(sqrt(x^2+1))-x^2))
    .=(1/2)*log(number_e,(t*t)/((sqrt((x^2+1)^2))-x^2)) by A2,SQUARE_1:29
    .=(1/2)*log(number_e,(t*t)/((x^2+1)-x^2)) by A2,SQUARE_1:22
    .=(1/2)*log(number_e,t^2)
    .=(1/2)*log(number_e,t to_power 2) by POWER:46
    .=(1/2)*(2*log(number_e,t)) by A1,Lm1,POWER:55,TAYLOR_1:11
    .=log(number_e,t);
  hence thesis;
end;

theorem
  x>=1 implies cosh1"(x)=sinh"(sqrt(x^2-1))
proof
  assume
A1: x>=1;
  then x^2-1>=0 by Lm3;
  then sinh"(sqrt(x^2-1)) =log(number_e,((sqrt(x^2-1))+sqrt((x^2-1)+1))) by
SQUARE_1:def 2
    .=log(number_e,((sqrt(x^2-1))+x)) by A1,SQUARE_1:22;
  hence thesis;
end;

theorem
  x>1 implies cosh1"(x)=tanh"((sqrt(x^2-1))/x)
proof
  assume
A1: x>1;
  then
A2: sqrt(x^2-1)+x>0 by Th23;
  x^2>1^2+0 by A1,SQUARE_1:16;
  then
A3: x^2-1>0 by XREAL_1:20;
  tanh"((sqrt(x^2-1))/x) =(1/2)*log(number_e,((sqrt(x^2-1)+x*1)/x)/(1-(
  sqrt(x^2-1))/x)) by A1,XCMPLX_1:113
    .=(1/2)*log(number_e,((sqrt(x^2-1)+x)/x)/((1*x-(sqrt(x^2-1)))/x)) by A1,
XCMPLX_1:127
    .=(1/2)*log(number_e,(sqrt(x^2-1)+x)/(x-sqrt(x^2-1))) by A1,XCMPLX_1:55
    .=(1/2)*log(number_e,((sqrt(x^2-1)+x)*(sqrt(x^2-1)+x))/ ((x-sqrt(x^2-1))
  *(sqrt(x^2-1)+x))) by A2,XCMPLX_1:91
    .=(1/2)*log(number_e,((sqrt(x^2-1)+x)*(sqrt(x^2-1)+x))/ (x^2-(sqrt(x^2-1
  ))^2))
    .=(1/2)*log(number_e,((sqrt(x^2-1)+x)*(sqrt(x^2-1)+x))/ (x^2-(x^2-1)))
  by A3,SQUARE_1:def 2
    .=(1/2)*log(number_e,((sqrt(x^2-1)+x)^2))
    .=(1/2)*log(number_e,((sqrt(x^2-1)+x) to_power 2)) by POWER:46
    .=(1/2)*(2*log(number_e,(sqrt(x^2-1)+x))) by A2,Lm1,POWER:55,TAYLOR_1:11
    .=log(number_e,(sqrt(x^2-1)+x));
  hence thesis;
end;

theorem
  x>=1 implies cosh1"(x)=2*cosh1"(sqrt((x+1)/2))
proof
  assume
A1: x>=1;
  then
A2: (x-1)/2>=0 by Th7;
A3: (x^2-1)/4>=0 by A1,Th9;
A4: sqrt((x+1)/2)+sqrt((x-1)/2)>0 by A1,Th10;
  2*cosh1"(sqrt((x+1)/2)) =2*(log(number_e,(sqrt((x+1)/2))+sqrt(((x+1)/2)-
  1))) by A1,SQUARE_1:def 2
    .=log(number_e,((sqrt((x+1)/2))+sqrt((x-1)/2)) to_power 2) by A4,Lm1,
POWER:55,TAYLOR_1:11
    .=log(number_e,((sqrt((x+1)/2))+sqrt((x-1)/2))^2) by POWER:46
    .=log(number_e,(sqrt((x+1)/2))^2+2*(sqrt((x+1)/2))* (sqrt((x-1)/2))+(
  sqrt((x-1)/2))^2)
    .=log(number_e,((x+1)/2)+2*(sqrt((x+1)/2))* (sqrt((x-1)/2))+(sqrt((x-1)/
  2))^2) by A1,SQUARE_1:def 2
    .=log(number_e,(x+1)/2+2*sqrt((x+1)/2)* sqrt((x-1)/2)+(x-1)/2) by A2,
SQUARE_1:def 2
    .=log(number_e,x+2*(sqrt((x+1)/2)*sqrt((x-1)/2)))
    .=log(number_e,x+2*(sqrt(((x+1)/2)*((x-1)/2)))) by A1,A2,SQUARE_1:29
    .=log(number_e,x+sqrt(2^2)*(sqrt((x^2-1)/4))) by SQUARE_1:22
    .=log(number_e,x+sqrt(4*((x^2-1)/4))) by A3,SQUARE_1:29
    .=log(number_e,x+sqrt(x^2-1));
  hence thesis;
end;

theorem
  x>=1 implies cosh2"(x)=2*cosh2"(sqrt((x+1)/2))
proof
  assume
A1: x>=1;
  then
A2: (x-1)/2>=0 by Th7;
A3: (x^2-1)/4>=0 by A1,Th9;
A4: sqrt((x+1)/2)+sqrt((x-1)/2)>0 by A1,Th10;
  2*cosh2"(sqrt((x+1)/2)) =2*(-(log(number_e,(sqrt((x+1)/2))+sqrt(((x+1)/2
  )-1)))) by A1,SQUARE_1:def 2
    .=-(2*(log(number_e,(sqrt((x+1)/2))+sqrt((x-1)/2))))
    .=-(log(number_e,((sqrt((x+1)/2))+sqrt((x-1)/2)) to_power 2)) by A4,Lm1,
POWER:55,TAYLOR_1:11
    .=-log(number_e,((sqrt((x+1)/2))+sqrt((x-1)/2))^2) by POWER:46
    .=-log(number_e,(sqrt((x+1)/2))^2+2*(sqrt((x+1)/2))* (sqrt((x-1)/2))+(
  sqrt((x-1)/2))^2)
    .=-log(number_e,((x+1)/2)+2*(sqrt((x+1)/2))* (sqrt((x-1)/2))+(sqrt((x-1)
  /2))^2) by A1,SQUARE_1:def 2
    .=-log(number_e,(x+1)/2+2*sqrt((x+1)/2)* sqrt((x-1)/2)+(x-1)/2) by A2,
SQUARE_1:def 2
    .=-log(number_e,(x+2*(sqrt((x+1)/2)*sqrt((x-1)/2))))
    .=-log(number_e,(x+2*(sqrt(((x+1)/2)*((x-1)/2))))) by A1,A2,SQUARE_1:29
    .=-log(number_e,(x+sqrt(2^2)*(sqrt((x^2-1)/4)))) by SQUARE_1:22
    .=-log(number_e,(x+sqrt(4*((x^2-1)/4)))) by A3,SQUARE_1:29
    .=-log(number_e,(x+sqrt(x^2-1)));
  hence thesis;
end;

theorem
  x>=1 implies cosh1"(x)=2*sinh"(sqrt((x-1)/2))
proof
  assume
A1: x>=1;
  then
A2: sqrt((x+1)/2)+sqrt((x-1)/2)>0 by Th10;
A3: (x^2-1)/4>=0 by A1,Th9;
A4: (x-1)/2>=0 by A1,Th7;
  then
  2*sinh"(sqrt((x-1)/2)) =2*log(number_e,((sqrt((x-1)/2))+sqrt(((x-1)/2)+1
  ))) by SQUARE_1:def 2
    .=log(number_e,(sqrt((x-1)/2)+sqrt((x+1)/2)) to_power 2) by A2,Lm1,POWER:55
,TAYLOR_1:11
    .=log(number_e,(sqrt((x-1)/2)+sqrt((x+1)/2))^2) by POWER:46
    .=log(number_e,(sqrt((x-1)/2))^2+2*(sqrt((x-1)/2)) *(sqrt((x+1)/2))+(
  sqrt((x+1)/2))^2)
    .=log(number_e,((x-1)/2)+2*(sqrt((x-1)/2)) *(sqrt((x+1)/2))+(sqrt((x+1)/
  2))^2) by A4,SQUARE_1:def 2
    .=log(number_e,(x-1)/2+2*(sqrt((x-1)/2)) *(sqrt((x+1)/2))+(x+1)/2) by A1,
SQUARE_1:def 2
    .=log(number_e,x+2*((sqrt((x-1)/2))*(sqrt((x+1)/2))))
    .=log(number_e,x+2*(sqrt(((x-1)/2)*((x+1)/2)))) by A1,A4,SQUARE_1:29
    .=log(number_e,x+sqrt(2^2)*(sqrt((x^2-1)/4))) by SQUARE_1:22
    .=log(number_e,x+sqrt(4*((x^2-1)/4))) by A3,SQUARE_1:29
    .=log(number_e,x+sqrt(x^2-1));
  hence thesis;
end;

theorem
  x^2<1 implies tanh"(x)=sinh"(x/sqrt(1-x^2))
proof
  assume
A1: x^2<1;
  then
A2: x+1>0 by Th11;
A3: sqrt(x+1)>0 by A1,Th11,SQUARE_1:25;
A4: (x+1)/(1-x)>0 by A1,Lm4;
A5: 1-x^2>0 by A1,XREAL_1:50;
A6: 1-x>0 by A1,Th11;
  then
A7: sqrt((x+1)/(1-x))=((x+1)/(1-x)) to_power (1/2) by A2,ASYMPT_1:83;
  sinh"(x/sqrt(1-x^2)) =log(number_e,((x/sqrt(1-x^2))+sqrt((x^2/(sqrt(1-x
  ^2))^2)+1))) by XCMPLX_1:76
    .=log(number_e,((x/sqrt(1-x^2))+sqrt((x^2/(1-x^2))+1))) by A5,
SQUARE_1:def 2
    .=log(number_e,((x/sqrt(1-x^2))+sqrt((x^2+(1-x^2)*1)/(1-x^2)))) by A5,
XCMPLX_1:113
    .=log(number_e,((x/sqrt(1-x^2))+sqrt(1)/sqrt(1-x^2))) by A5,SQUARE_1:30
    .=log(number_e,((x+1)/sqrt((1-x)*(1+x))))
    .=log(number_e,(sqrt((x+1)^2)/sqrt((1-x)*(1+x)))) by A2,SQUARE_1:22
    .=log(number_e,((sqrt(x+1)*sqrt(x+1))/sqrt((1-x)*(1+x)))) by A2,SQUARE_1:29
    .=log(number_e,((sqrt(x+1)*sqrt(x+1))/(sqrt(1-x)*sqrt(1+x)))) by A2,A6,
SQUARE_1:29
    .=log(number_e,(sqrt(x+1)/sqrt(1-x))) by A3,XCMPLX_1:91
    .=log(number_e,(sqrt((x+1)/(1-x)))) by A2,A6,SQUARE_1:30
    .=(1/2)*log(number_e,((1+x)/(1-x))) by A4,A7,Lm1,POWER:55,TAYLOR_1:11;
  hence thesis;
end;

theorem
  0<x & x<1 implies tanh"(x)=cosh1"(1/(sqrt(1-x^2)))
proof
  assume that
A1: 0<x and
A2: x<1;
A3: 1-x^2>0 by A1,A2,Lm5;
A4: (1+x)/(1-x)>0 by A1,A2,Th15;
A5: 1-x>0 by A2,XREAL_1:50;
A6: sqrt(1+x)>0 by A1,SQUARE_1:25;
  (1+x)/(1-x)>0 by A1,A2,Th15;
  then
A7: sqrt((1+x)/(1-x))=((1+x)/(1-x)) to_power (1/2) by ASYMPT_1:83;
A8: x^2>=0 by XREAL_1:63;
  cosh1"(1/(sqrt(1-x^2))) =log(number_e,(1/(sqrt(1-x^2)))+sqrt((1/((sqrt(
  1-x^2))^2))-1^2)) by XCMPLX_1:76
    .=log(number_e,(1/(sqrt(1-x^2)))+sqrt(1/(1-x^2)-1)) by A3,SQUARE_1:def 2
    .=log(number_e,(1/(sqrt(1-x^2)))+sqrt((1-1*(1-x^2))/(1-x^2))) by A3,
XCMPLX_1:126
    .=log(number_e,(1/(sqrt(1-x^2)))+sqrt(x^2)/sqrt(1-x^2)) by A3,A8,
SQUARE_1:30
    .=log(number_e,1/(sqrt(1-x^2))+x/sqrt(1-x^2)) by A1,SQUARE_1:22
    .=log(number_e,(1+x)/sqrt((1-x)*(1+x)))
    .=log(number_e,(1+x)/(sqrt(1-x)*sqrt(1+x))) by A1,A5,SQUARE_1:29
    .=log(number_e,(sqrt((1+x)^2))/(sqrt(1-x)*sqrt(1+x))) by A1,SQUARE_1:22
    .=log(number_e,(sqrt(1+x)*sqrt(1+x))/(sqrt(1-x)*sqrt(1+x))) by A1,
SQUARE_1:29
    .=log(number_e,(sqrt(1+x))/(sqrt(1-x))) by A6,XCMPLX_1:91
    .=log(number_e,sqrt((1+x)/(1-x))) by A1,A5,SQUARE_1:30
    .=(1/2)*log(number_e,((1+x)/(1-x))) by A7,A4,Lm1,POWER:55,TAYLOR_1:11;
  hence thesis;
end;

theorem
  x^2<1 implies tanh"(x)=(1/2)*sinh"((2*x)/(1-x^2))
proof
  assume
A1: x^2<1;
  then
A2: (1-x^2)^2>0 by Th12;
A3: x+1>0 by A1,Th11;
  (1/2)*sinh"((2*x)/(1-x^2)) =(1/2)*log(number_e,(((2*x)/(1-x^2))+sqrt(((2
  *x)^2/(1-x^2)^2)+1))) by XCMPLX_1:76
    .=(1/2)*log(number_e,(((2*x)/(1-x^2))+sqrt(((4*x^2)+((1-x^2)^2)*1)/ ((1-
  x^2)^2)))) by A2,XCMPLX_1:113
    .=(1/2)*log(number_e,(((2*x)/(1-x^2))+sqrt((((x^2)+1)^2)/ ((1-x^2)^2))))
    .=(1/2)*log(number_e,(((2*x)/(1-x^2))+sqrt((((x^2)+1)/(1-x^2))^2))) by
XCMPLX_1:76
    .=(1/2)*log(number_e,((2*x)/(1-x^2)+((x^2)+1)/(1-x^2))) by A1,Th13,
SQUARE_1:22
    .=(1/2)*log(number_e,(((2*x)+((x^2)+1))/(1-x^2)))
    .=(1/2)*log(number_e,((x+1)*(x+1)/((1-x)*(1+x))))
    .=(1/2)*log(number_e,((x+1)/(1-x))) by A3,XCMPLX_1:91;
  hence thesis;
end;

theorem
  x>0 & x<1 implies tanh"(x)=(1/2)*cosh1"((1+x^2)/(1-x^2))
proof
  assume that
A1: x>0 and
A2: x<1;
A3: 0<(1-x^2)^2 by A1,A2,Th19;
A4: (2*x)/(1-x^2)>0 by A1,A2,Th18;
  (1/2)*cosh1"((1+x^2)/(1-x^2)) =(1/2)*log(number_e,((1+x^2)/(1-x^2))+sqrt
  ((1+x^2)^2/(1-x^2)^2-1)) by XCMPLX_1:76
    .=(1/2)*log(number_e,((1+x^2)/(1-x^2))+sqrt((((1+x^2)^2)-1* ((1-x^2)^2))
  /((1-x^2)^2))) by A3,XCMPLX_1:126
    .=(1/2)*log(number_e,((1+x^2)/(1-x^2))+sqrt(((2*x)^2)/((1-x^2)^2)))
    .=(1/2)*log(number_e,((1+x^2)/(1-x^2))+sqrt(((2*x)/(1-x^2))^2)) by
XCMPLX_1:76
    .=(1/2)*log(number_e,(1+x^2)/(1-x^2)+(2*x)/(1-x^2)) by A4,SQUARE_1:22
    .=(1/2)*log(number_e,((1+x^2)+(2*x))/(1-x^2))
    .=(1/2)*log(number_e,(x+1)*(x+1)/((1-x)*(1+x)))
    .=(1/2)*log(number_e,(x+1)/((1-x))) by A1,XCMPLX_1:91;
  hence thesis;
end;

theorem
  x^2<1 implies tanh"(x)=(1/2)*tanh"((2*x)/(1+x^2))
proof
  assume x^2<1;
  then
A1: (x+1)/(1-x)>0 by Lm4;
A2: 1+x^2>0 by Lm6;
  then
  (1/2)*tanh"((2*x)/(1+x^2)) =(1/2)*((1/2)*log(number_e,(((2*x)+(1+x^2)*1)
  /(1+x^2))/(1-(2*x)/(1+x^2)))) by XCMPLX_1:113
    .=(1/2)*((1/2)*log(number_e,((2*x+1+x^2)/(1+x^2))/((1*(1+x^2)-(2*x)) /(1
  +x^2)))) by A2,XCMPLX_1:127
    .=(1/2)*((1/2)*log(number_e,(x+1)^2/(1-x)^2)) by A2,XCMPLX_1:55
    .=(1/2)*((1/2)*log(number_e,((x+1)/(1-x))^2)) by XCMPLX_1:76
    .=(1/2)*((1/2)*log(number_e,((x+1)/(1-x)) to_power 2)) by POWER:46
    .=(1/2)*((1/2)*(2*log(number_e,((x+1)/(1-x))))) by A1,Lm1,POWER:55
,TAYLOR_1:11
    .=(1/2)*log(number_e,(1+x)/(1-x));
  hence thesis;
end;

theorem
  x^2>1 implies coth"(x)=tanh"(1/x)
proof
  assume x^2>1;
  then
A1: x<>0;
  then tanh"(1/x) =(1/2)*log(number_e,((1+x*1)/x)/(1-(1/x))) by XCMPLX_1:113
    .=(1/2)*log(number_e,((1+x*1)/x)/((1*x-1)/x)) by A1,XCMPLX_1:127
    .=(1/2)*log(number_e,(1+x)/(x-1)) by A1,XCMPLX_1:55;
  hence thesis;
end;

theorem
  x>0 & x<=1 implies sech1"(x)=cosh1"(1/x)
proof
  assume that
A1: x>0 and
A2: x<=1;
A3: 1-x^2>=0 by A1,A2,Th22;
A4: x^2>0 by A1;
  cosh1"(1/x)=log(number_e,(1/x)+sqrt(1/x^2-1^2)) by XCMPLX_1:76
    .=log(number_e,(1/x)+sqrt((1-1*(x^2))/x^2)) by A4,XCMPLX_1:126
    .=log(number_e,(1/x)+sqrt(1-(x^2))/sqrt(x^2)) by A1,A3,SQUARE_1:30
    .=log(number_e,(1/x)+sqrt(1-(x^2))/x) by A1,SQUARE_1:22
    .=log(number_e,(1+sqrt(1-x^2))/x);
  hence thesis;
end;

theorem
  x>0 & x<=1 implies sech2"(x)=cosh2"(1/x)
proof
  assume that
A1: x>0 and
A2: x<=1;
A3: 1-x^2>=0 by A1,A2,Th22;
A4: x^2>0 by A1;
  cosh2"(1/x) =-log(number_e,(1/x)+sqrt(1/x^2-1^2)) by XCMPLX_1:76
    .=-log(number_e,(1/x)+sqrt((1-1*(x^2))/x^2)) by A4,XCMPLX_1:126
    .=-log(number_e,(1/x)+sqrt(1-(x^2))/sqrt(x^2)) by A1,A3,SQUARE_1:30
    .=-log(number_e,(1/x)+sqrt(1-(x^2))/x) by A1,SQUARE_1:22
    .=-log(number_e,(1+sqrt(1-x^2))/x);
  hence thesis;
end;

theorem
  x>0 implies csch"(x)=sinh"(1/x)
proof
  assume
A1: x>0;
  then
A2: x^2>0;
  sinh"(1/x)=log(number_e,(1/x+sqrt(1/x^2+1^2))) by XCMPLX_1:76
    .=log(number_e,(1/x+sqrt((1+x^2*1)/(x^2)))) by A2,XCMPLX_1:113
    .=log(number_e,(1/x+sqrt(1+x^2)/sqrt(x^2))) by A1,SQUARE_1:30
    .=log(number_e,(1/x+sqrt(1+x^2)/x)) by A1,SQUARE_1:22
    .=log(number_e,(1+sqrt(1+x^2))/x);
  hence thesis by A1,Def8;
end;

theorem
  (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))
proof
  assume
A1: (x*y+sqrt(x^2+1)*sqrt(y^2+1))>=0;
  sqrt(x^2+1)+x>0 & sqrt(y^2+1)+y>0 by Th5;
  then
A2: sinh"(x)+sinh"(y) =log(number_e,(x+sqrt(x^2+1))*(y+sqrt(y^2+1))) by Lm1,
POWER:53,TAYLOR_1:11
    .=log(number_e,(x*sqrt(y^2+1)+sqrt(x^2+1)*y+(x*y+sqrt(x^2+1)*sqrt(y^2+1)
  )))
    .=log(number_e,(x*sqrt(y^2+1)+sqrt(x^2+1)*y+ sqrt((x*y+sqrt(x^2+1)*sqrt(
  y^2+1))^2))) by A1,SQUARE_1:22;
A3: y^2+1>=0 by Lm6;
  set p=sqrt(((x*sqrt(1+y^2))+(y*sqrt(1+x^2)))^2+1);
  set t=sqrt((x*y+sqrt(x^2+1)*sqrt(y^2+1))^2);
A4: x^2+1>=0 by Lm6;
A5: p=sqrt((x^2*(sqrt(1+y^2))^2+2*(x*sqrt(1+y^2))*(y*sqrt(1+x^2)) +(y*sqrt(1
  +x^2))^2)+1)
    .=sqrt((x^2*(1+y^2)+2*(x*sqrt(1+y^2))*(y*sqrt(1+x^2)) +(y*sqrt(1+x^2))^2
  )+1) by A3,SQUARE_1:def 2
    .=sqrt((x^2+(x*y)^2+2*(x*sqrt(1+y^2))*(y*sqrt(1+x^2)) +y^2*(sqrt(1+x^2))
  ^2)+1)
    .=sqrt((x^2+(x*y)^2+2*(x*sqrt(1+y^2))*(y*sqrt(1+x^2)) +y^2*(1+x^2))+1)
  by A4,SQUARE_1:def 2
    .=sqrt(x^2+2*(x*y)^2+y^2+1+2*x*y*(sqrt(1+y^2)*sqrt(1+x^2)))
    .=sqrt(x^2+2*(x*y)^2+y^2+1+2*x*y*sqrt((1+y^2)*(1+x^2))) by A4,A3,
SQUARE_1:29;
  t=sqrt((x*y+sqrt((x^2+1)*(y^2+1)))^2) by A4,A3,SQUARE_1:29
    .=sqrt((x*y)^2+2*(x*y)*(sqrt((x^2+1)*(y^2+1)))+(sqrt((x^2+1)*(y^2+1)))^2
  )
    .=sqrt((x*y)^2+2*(x*y)*(sqrt((x^2+1)*(y^2+1)))+((x*y)^2+x^2+y^2+1)) by A4
,A3,SQUARE_1:def 2
    .=sqrt(2*(x*y)^2+x^2+y^2+1+2*(x*y)*(sqrt((x^2+1)*(y^2+1))));
  hence thesis by A2,A5;
end;

theorem
  sinh"(x)-sinh"(y)=sinh"(x*sqrt(1+y^2)-y*sqrt(1+x^2))
proof
  set t=(sqrt(x^2+1))*(sqrt(y^2+1))-x*y;
  set q=sqrt((x*sqrt(1+y^2)-y*sqrt(1+x^2))^2+1);
A1: x^2+1>=0 by Lm6;
  y+0<sqrt(y^2+1) by Lm8;
  then
A2: sqrt(y^2+1)-y>0 by XREAL_1:20;
A3: y^2+1>=0 by Lm6;
  (sqrt(x^2+1)*sqrt(y^2+1)-x*y)>=0 by Lm9;
  then
A4: t=sqrt(((sqrt(x^2+1))*(sqrt(y^2+1))-x*y)^2) by SQUARE_1:22
    .=sqrt(((sqrt(x^2+1))^2*(sqrt(y^2+1))^2)-2*((sqrt(x^2+1))* (sqrt(y^2+1))
  )*(x*y)+(x*y)^2)
    .=sqrt(((x^2+1)*(sqrt(y^2+1))^2)-2*((sqrt(x^2+1))* (sqrt(y^2+1)))*(x*y)+
  (x*y)^2) by A1,SQUARE_1:def 2
    .=sqrt(((x^2+1)*(y^2+1))-2*((sqrt(x^2+1))* (sqrt(y^2+1)))*(x*y)+(x*y)^2)
  by A3,SQUARE_1:def 2
    .=sqrt(2*((x*y)^2)+x^2+y^2+1-2*(x*y)*((sqrt(x^2+1))* (sqrt(y^2+1))));
A5: q=sqrt((x^2*(sqrt(1+y^2))^2)-2*(x*sqrt(1+y^2))*(y*sqrt(1+x^2)) +((y*
  sqrt(1+x^2)))^2+1)
    .=sqrt((x^2*(1+y^2))-2*(x*sqrt(1+y^2))*(y*sqrt(1+x^2)) +((y*sqrt(1+x^2))
  )^2+1) by A3,SQUARE_1:def 2
    .=sqrt((x^2+x^2*y^2)-2*(x*sqrt(1+y^2))*(y*sqrt(1+x^2)) +(y^2*(sqrt(1+x^2
  ))^2)+1)
    .=sqrt((x^2+x^2*y^2)-2*(x*sqrt(1+y^2))*(y*sqrt(1+x^2)) +(y^2*(1+x^2))+1)
  by A1,SQUARE_1:def 2
    .=sqrt(x^2+y^2+2*(x*y)^2+1-2*x*y*sqrt(1+y^2)*sqrt(1+x^2));
  sqrt(x^2+1)+x>0 & sqrt(y^2+1)+y>0 by Th5;
  then sinh"(x)-sinh"(y) =log(number_e,(x+sqrt(x^2+1))/(y+sqrt(y^2+1))) by Lm1,
POWER:54,TAYLOR_1:11
    .=log(number_e,((x+sqrt(x^2+1))*(sqrt(y^2+1)-y))/ ((y+sqrt(y^2+1))*(sqrt
  (y^2+1)-y))) by A2,XCMPLX_1:91
    .=log(number_e,((x+sqrt(x^2+1))*(sqrt(y^2+1)-y))/ ((sqrt(y^2+1))^2-y^2))
    .=log(number_e,((x+sqrt(x^2+1))*(sqrt(y^2+1)-y))/ ((y^2+1)-y^2)) by A3,
SQUARE_1:def 2
    .=log(number_e,x*(sqrt(y^2+1))-y*(sqrt(x^2+1))+(sqrt(x^2+1)) *(sqrt(y^2+
  1))-x*y);
  hence thesis by A4,A5;
end;

theorem
  1<=x & 1<=y implies cosh1"(x)+cosh1"(y)=cosh1"(x*y+sqrt((x^2-1)*(y^2-1 )))
proof
  assume that
A1: 1<=x and
A2: 1<=y;
A3: y^2-1>=0 by A2,Lm3;
  set t=x*sqrt(y^2-1)+y*sqrt(x^2-1);
A4: x^2-1>=0 by A1,Lm3;
  t=sqrt((x*sqrt(y^2-1)+y*sqrt(x^2-1))^2) by A1,A2,Th24,SQUARE_1:22
    .=sqrt(x^2*(sqrt(y^2-1))^2+2*(x*sqrt(y^2-1))*(y*sqrt(x^2-1))+ (y*sqrt(x
  ^2-1))^2)
    .=sqrt(x^2*(y^2-1)+2*(x*sqrt(y^2-1))*(y*sqrt(x^2-1))+ (y*sqrt(x^2-1))^2)
  by A3,SQUARE_1:def 2
    .=sqrt(x^2*y^2-x^2+2*(x*sqrt(y^2-1))*(y*sqrt(x^2-1))+ y^2*(sqrt(x^2-1))
  ^2)
    .=sqrt(x^2*y^2-x^2+2*(x*sqrt(y^2-1))*(y*sqrt(x^2-1))+ y^2*(x^2-1)) by A4,
SQUARE_1:def 2
    .=sqrt(2*(x*y)^2-x^2-y^2+2*(x*sqrt(y^2-1))*(y*sqrt(x^2-1)));
  then
A5: log(number_e,x*sqrt(y^2-1)+y*sqrt(x^2-1)+sqrt((x^2-1)*(y^2-1))+x*y) =log
(number_e,(sqrt(2*(x*y)^2-x^2-y^2+2*x*y*(sqrt(y^2-1) *sqrt(x^2-1))))+sqrt((x^2-
  1)*(y^2-1))+x*y)
    .=log(number_e,(sqrt(2*(x*y)^2-x^2-y^2+2*x*y*sqrt((y^2-1)*(x^2-1)))) +
  sqrt((x^2-1)*(y^2-1))+x*y) by A4,A3,SQUARE_1:29;
A6: cosh1"(x*y+sqrt((x^2-1)*(y^2-1))) =log(number_e,(x*y+sqrt((x^2-1)*(y^2-
1)))+sqrt((x*y)^2+ 2*(x*y)*(sqrt((x^2-1)*(y^2-1)))+((sqrt((x^2-1)*(y^2-1)))^2)-
  1))
    .=log(number_e,(x*y+sqrt((x^2-1)*(y^2-1)))+sqrt((x*y)^2+ 2*(x*y)*(sqrt((
  x^2-1)*(y^2-1)))+(x^2-1)*(y^2-1)-1)) by A4,A3,SQUARE_1:def 2
    .=log(number_e,((sqrt(2*(x*y)^2-x^2-y^2+2*x*y*sqrt((y^2-1)*(x^2-1))))) +
  (sqrt((x^2-1)*(y^2-1))+x*y));
  0<x+sqrt(x^2-1) & 0<y+sqrt(y^2-1) by A1,A2,Th23;
  then cosh1"(x)+cosh1"(y) =log(number_e,(x+sqrt(x^2-1))*(y+sqrt(y^2-1))) by
Lm1,POWER:53,TAYLOR_1:11
    .=log(number_e,x*sqrt(y^2-1)+y*sqrt(x^2-1)+(sqrt(x^2-1))*(sqrt(y^2-1))+x
  *y)
    .=log(number_e,x*sqrt(y^2-1)+y*sqrt(x^2-1)+sqrt((x^2-1)*(y^2-1))+x*y) by A4
,A3,SQUARE_1:29;
  hence thesis by A5,A6;
end;

theorem
  1<=x & 1<=y implies cosh2"(x)+cosh2"(y)=cosh2"(x*y+sqrt((x^2-1)*(y^2-1 )))
proof
  assume that
A1: 1<=x and
A2: 1<=y;
A3: y^2-1>=0 by A2,Lm3;
A4: 0<x+sqrt(x^2-1) & 0<y+sqrt(y^2-1) by A1,A2,Th23;
  set t=x*sqrt(y^2-1)+y*sqrt(x^2-1);
A5: x^2-1>=0 by A1,Lm3;
  t=sqrt((x*sqrt(y^2-1)+y*sqrt(x^2-1))^2) by A1,A2,Th24,SQUARE_1:22
    .=sqrt(x^2*(sqrt(y^2-1))^2+2*(x*sqrt(y^2-1))*(y*sqrt(x^2-1))+ (y*sqrt(x
  ^2-1))^2)
    .=sqrt(x^2*(y^2-1)+2*(x*sqrt(y^2-1))*(y*sqrt(x^2-1))+ (y*sqrt(x^2-1))^2)
  by A3,SQUARE_1:def 2
    .=sqrt(x^2*y^2-x^2+2*(x*sqrt(y^2-1))*(y*sqrt(x^2-1))+ y^2*(sqrt(x^2-1))
  ^2)
    .=sqrt(x^2*y^2-x^2+2*(x*sqrt(y^2-1))*(y*sqrt(x^2-1))+ y^2*(x^2-1)) by A5,
SQUARE_1:def 2
    .=sqrt(2*(x*y)^2-x^2-y^2+2*(x*sqrt(y^2-1))*(y*sqrt(x^2-1)));
  then
A6: -log(number_e,x*sqrt(y^2-1)+y*sqrt(x^2-1)+sqrt((x^2-1)*(y^2-1))+x*y) =-
log(number_e,(sqrt(2*(x*y)^2-x^2-y^2+2*x*y*(sqrt(y^2-1) *sqrt(x^2-1))))+sqrt((x
  ^2-1)*(y^2-1))+x*y)
    .=-log(number_e,(sqrt(2*(x*y)^2-x^2-y^2+2*x*y*sqrt((y^2-1)*(x^2-1)))) +
  sqrt((x^2-1)*(y^2-1))+x*y) by A5,A3,SQUARE_1:29;
A7: cosh2"(x*y+sqrt((x^2-1)*(y^2-1))) =-log(number_e,(x*y+sqrt((x^2-1)*(y^2
-1)))+sqrt((x*y)^2+ 2*(x*y)*(sqrt((x^2-1)*(y^2-1)))+((sqrt((x^2-1)*(y^2-1)))^2)
  -1))
    .=-log(number_e,(x*y+sqrt((x^2-1)*(y^2-1)))+sqrt((x*y)^2+ 2*(x*y)*(sqrt(
  (x^2-1)*(y^2-1)))+(x^2-1)*(y^2-1)-1)) by A5,A3,SQUARE_1:def 2
    .=-log(number_e,((sqrt(2*(x*y)^2-x^2-y^2+2*x*y*sqrt((y^2-1)*(x^2-1)))))
  +(sqrt((x^2-1)*(y^2-1))+x*y));
  cosh2"(x)+cosh2"(y) =(-1)*(log(number_e,x+sqrt(x^2-1))+log(number_e,y+
  sqrt(y^2-1)))
    .=(-1)*log(number_e,(x+sqrt(x^2-1))*(y+sqrt(y^2-1))) by A4,Lm1,POWER:53
,TAYLOR_1:11
    .=-log(number_e,x*sqrt(y^2-1)+y*sqrt(x^2-1)+(sqrt(x^2-1))*(sqrt(y^2-1))+
  x*y)
    .=-log(number_e,x*sqrt(y^2-1)+y*sqrt(x^2-1)+sqrt((x^2-1)*(y^2-1))+x*y)
  by A5,A3,SQUARE_1:29;
  hence thesis by A6,A7;
end;

theorem
  1<=x & 1<=y & |.y.|<=|.x.| implies cosh1"(x)-cosh1"(y)=cosh1"(x*y-
  sqrt((x^2-1)*(y^2-1)))
proof
  assume that
A1: 1<=x and
A2: 1<=y and
A3: |.y.|<=|.x.|;
A4: 0<=x^2-1 by A1,Lm3;
  set t=y*sqrt(x^2-1)-x*sqrt(y^2-1);
A5: (y-sqrt(y^2-1))>0 by A2,Th25;
A6: 0<=y^2-1 by A2,Lm3;
  0<x+sqrt(x^2-1) & 0<y+sqrt(y^2-1) by A1,A2,Th23;
  then
A7: cosh1"(x)-cosh1"(y) =log(number_e,((x+sqrt(x^2-1))/(y+sqrt(y^2-1)))) by Lm1
,POWER:54,TAYLOR_1:11
    .=log(number_e,(((x+sqrt(x^2-1))*(y-sqrt(y^2-1)))/ ((y+sqrt(y^2-1))*(y-
  sqrt(y^2-1))))) by A5,XCMPLX_1:91
    .=log(number_e,(((x+sqrt(x^2-1))*(y-sqrt(y^2-1)))/ (y^2-(sqrt(y^2-1))^2)
  ))
    .=log(number_e,(((x+sqrt(x^2-1))*(y-sqrt(y^2-1)))/ (y^2-(y^2-1)))) by A6,
SQUARE_1:def 2
    .=log(number_e,(x*y-x*sqrt(y^2-1)+y*sqrt(x^2-1)-sqrt(x^2-1)* (sqrt(y^2-1
  ))))
    .=log(number_e,(x*y-x*sqrt(y^2-1)+y*sqrt(x^2-1)-sqrt((x^2-1)*(y^2-1))))
  by A4,A6,SQUARE_1:29
    .=log(number_e,(x*y-sqrt((x^2-1)*(y^2-1))+y*sqrt(x^2-1)-x*sqrt(y^2-1)));
A8: cosh1"(x*y-sqrt((x^2-1)*(y^2-1))) =log(number_e,(x*y-sqrt((x^2-1)*(y^2-
1)))+sqrt((x*y)^2-2*(x*y)* (sqrt((x^2-1)*(y^2-1)))+(sqrt((x^2-1)*(y^2-1)))^2-1)
  )
    .=log(number_e,(x*y-sqrt((x^2-1)*(y^2-1)))+sqrt((x*y)^2-2*(x*y)* (sqrt((
  x^2-1)*(y^2-1)))+((x^2-1)*(y^2-1))-1)) by A4,A6,SQUARE_1:def 2
    .=log(number_e,(x*y-sqrt((x^2-1)*(y^2-1)))+sqrt(2*(x*y)^2-x^2-y^2 -2*x*y
  *(sqrt((x^2-1)*(y^2-1)))));
  t=sqrt((y*sqrt(x^2-1)-x*sqrt(y^2-1))^2) by A1,A2,A3,Th26,SQUARE_1:22
    .=sqrt(y^2*(sqrt(x^2-1))^2-2*(y*sqrt(x^2-1))* (x*sqrt(y^2-1))+(x*sqrt(y
  ^2-1))^2)
    .=sqrt(y^2*(x^2-1)-2*(y*sqrt(x^2-1))* (x*sqrt(y^2-1))+(x*sqrt(y^2-1))^2)
  by A4,SQUARE_1:def 2
    .=sqrt((x*y)^2-y^2-2*(y*sqrt(x^2-1))* (x*sqrt(y^2-1))+x^2*(sqrt(y^2-1))
  ^2)
    .=sqrt((x*y)^2-y^2-2*(y*sqrt(x^2-1))* (x*sqrt(y^2-1))+x^2*(y^2-1)) by A6,
SQUARE_1:def 2
    .=sqrt(2*(x*y)^2-x^2-y^2-2*x*y*(sqrt(x^2-1)*sqrt(y^2-1)))
    .=sqrt(2*(x*y)^2-x^2-y^2-2*x*y*(sqrt((x^2-1)*(y^2-1)))) by A4,A6,
SQUARE_1:29;
  hence thesis by A7,A8;
end;

theorem
  1<=x & 1<=y & |.y.|<=|.x.| implies cosh2"(x)-cosh2"(y)=cosh2"(x*y-
  sqrt((x^2-1)*(y^2-1)))
proof
  assume that
A1: 1<=x and
A2: 1<=y and
A3: |.y.|<=|.x.|;
A4: 0<x+sqrt(x^2-1) & 0<y+sqrt(y^2-1) by A1,A2,Th23;
A5: 0<=y^2-1 by A2,Lm3;
  set t=y*sqrt(x^2-1)-x*sqrt(y^2-1);
A6: (y-sqrt(y^2-1))>0 by A2,Th25;
A7: 0<=x^2-1 by A1,Lm3;
A8: cosh2"(x*y-sqrt((x^2-1)*(y^2-1))) =-log(number_e,(x*y-sqrt((x^2-1)*(y^2
-1)))+sqrt((x*y)^2-2*(x*y)* (sqrt((x^2-1)*(y^2-1)))+(sqrt((x^2-1)*(y^2-1)))^2-1
  ))
    .=-log(number_e,(x*y-sqrt((x^2-1)*(y^2-1)))+sqrt((x*y)^2-2*(x*y)* (sqrt(
  (x^2-1)*(y^2-1)))+((x^2-1)*(y^2-1))-1)) by A7,A5,SQUARE_1:def 2
    .=-log(number_e,(x*y-sqrt((x^2-1)*(y^2-1)))+sqrt(2*(x*y)^2-x^2-y^2 -2*x*
  y*(sqrt((x^2-1)*(y^2-1)))));
A9: cosh2"(x)-cosh2"(y) =-(log(number_e,x+sqrt(x^2-1))-log(number_e,y+sqrt(y
  ^2-1)))
    .=-log(number_e,((x+sqrt(x^2-1))/(y+sqrt(y^2-1)))) by A4,Lm1,POWER:54
,TAYLOR_1:11
    .=-log(number_e,(((x+sqrt(x^2-1))*(y-sqrt(y^2-1)))/ ((y+sqrt(y^2-1))*(y-
  sqrt(y^2-1))))) by A6,XCMPLX_1:91
    .=-log(number_e,(((x+sqrt(x^2-1))*(y-sqrt(y^2-1)))/ (y^2-(sqrt(y^2-1))^2
  )))
    .=-log(number_e,(((x+sqrt(x^2-1))*(y-sqrt(y^2-1)))/ (y^2-(y^2-1)))) by A5,
SQUARE_1:def 2
    .=-log(number_e,(x*y-x*sqrt(y^2-1)+y*sqrt(x^2-1)-sqrt(x^2-1)* (sqrt(y^2-
  1))))
    .=-log(number_e,(x*y-x*sqrt(y^2-1)+y*sqrt(x^2-1)-sqrt((x^2-1)*(y^2-1))))
  by A7,A5,SQUARE_1:29
    .=-log(number_e,(x*y-sqrt((x^2-1)*(y^2-1))+y*sqrt(x^2-1)-x*sqrt(y^2-1)));
  t=sqrt((y*sqrt(x^2-1)-x*sqrt(y^2-1))^2) by A1,A2,A3,Th26,SQUARE_1:22
    .=sqrt(y^2*(sqrt(x^2-1))^2-2*(y*sqrt(x^2-1))* (x*sqrt(y^2-1))+(x*sqrt(y
  ^2-1))^2)
    .=sqrt(y^2*(x^2-1)-2*(y*sqrt(x^2-1))* (x*sqrt(y^2-1))+(x*sqrt(y^2-1))^2)
  by A7,SQUARE_1:def 2
    .=sqrt((x*y)^2-y^2-2*(y*sqrt(x^2-1))* (x*sqrt(y^2-1))+x^2*(sqrt(y^2-1))
  ^2)
    .=sqrt((x*y)^2-y^2-2*(y*sqrt(x^2-1))* (x*sqrt(y^2-1))+x^2*(y^2-1)) by A5,
SQUARE_1:def 2
    .=sqrt(2*(x*y)^2-x^2-y^2-2*x*y*(sqrt(x^2-1)*sqrt(y^2-1)))
    .=sqrt(2*(x*y)^2-x^2-y^2-2*x*y*(sqrt((x^2-1)*(y^2-1)))) by A7,A5,
SQUARE_1:29;
  hence thesis by A9,A8;
end;

theorem
  x^2<1 & y^2<1 implies tanh"(x)+tanh"(y)=tanh"((x+y)/(1+x*y))
proof
  assume
A1: x^2<1 & y^2<1;
  then
A2: 0<(1+x)/(1-x) & 0<(1+y)/(1-y) by Lm4;
A3: tanh"(x)+tanh"(y) =(1/2)*(log(number_e,(1+x)/(1-x))+log(number_e,(1+y)/(
  1-y)))
    .=(1/2)*(log(number_e,((1+x)/(1-x))*((1+y)/(1-y)))) by A2,Lm1,POWER:53
,TAYLOR_1:11
    .=(1/2)*(log(number_e,(((1+x)*(1+y))/((1-x)*(1-y))))) by XCMPLX_1:76
    .=(1/2)*(log(number_e,((1+x+y+x*y)/(1+x*y-x-y))));
A4: x*y+1<>0 by A1,Th27;
  then
  tanh"((x+y)/(1+x*y)) =(1/2)*log(number_e,(((x+y)+(1+x*y)*1)/(1+x*y))/(1-
  ((x+y)/(1+x*y)))) by XCMPLX_1:113
    .=(1/2)*log(number_e,((x+y+1+x*y)/(1+x*y))/(((1*(1+x*y)-(x+y))/(1+x*y)))
  ) by A4,XCMPLX_1:127
    .=(1/2)*log(number_e,(1+x+y+x*y)/(1+x*y-x-y)) by A4,XCMPLX_1:55;
  hence thesis by A3;
end;

theorem
  x^2<1 & y^2<1 implies tanh"(x)-tanh"(y)=tanh"((x-y)/(1-x*y))
proof
  assume
A1: x^2<1 & y^2<1;
  then
A2: 0<(1+x)/(1-x) & 0<(1+y)/(1-y) by Lm4;
A3: tanh"(x)-tanh"(y) =(1/2)*(log(number_e,(1+x)/(1-x))-log(number_e,(1+y)/(
  1-y)))
    .=(1/2)*(log(number_e,((1+x)/(1-x))/((1+y)/(1-y)))) by A2,Lm1,POWER:54
,TAYLOR_1:11
    .=(1/2)*(log(number_e,((1+x)*(1-y))/((1-x)*(1+y)))) by XCMPLX_1:84
    .=(1/2)*(log(number_e,(1-y+x-x*y)/(1+y-x-x*y)));
A4: 1-x*y<>0 by A1,Th28;
  then
  tanh"((x-y)/(1-x*y)) =(1/2)*log(number_e,(((x-y)+(1-x*y)*1)/(1-x*y))/(1-
  ((x-y)/(1-x*y)))) by XCMPLX_1:113
    .=(1/2)*log(number_e,((x-y+1-x*y)/(1-x*y))/((1*(1-x*y)-(x-y))/(1-x*y)))
  by A4,XCMPLX_1:127
    .=(1/2)*(log(number_e,(1-y+x-x*y)/(1+y-x-x*y))) by A4,XCMPLX_1:55;
  hence thesis by A3;
end;

theorem
  0<x implies log(number_e,x)=2*tanh"((x-1)/(x+1))
proof
  assume
A1: 0<x;
  then
  2*tanh"((x-1)/(x+1)) =log(number_e,(((x-1)+(x+1)*1)/(x+1))/(1-(x-1)/(x+1
  ))) by XCMPLX_1:113
    .=log(number_e,((2*x)/(x+1))/((1*(x+1)-(x-1))/(x+1))) by A1,XCMPLX_1:127
    .=log(number_e,(2*x)/2) by A1,XCMPLX_1:55
    .=log(number_e,x);
  hence thesis;
end;

theorem
  0<x implies log(number_e,x)=tanh"((x^2-1)/(x^2+1))
proof
  assume
A1: 0<x;
A2: x^2+1>0 by Lm6;
  then
  tanh"((x^2-1)/(x^2+1)) =(1/2)*log(number_e,(((x^2-1)+(x^2+1)*1)/(x^2+1))
  /(1-(x^2-1)/(x^2+1))) by XCMPLX_1:113
    .=(1/2)*log(number_e,((2*x^2)/(x^2+1))/((1*(x^2+1)-(x^2-1))/(x^2+1))) by A2
,XCMPLX_1:127
    .=(1/2)*log(number_e,2*x^2/2) by A2,XCMPLX_1:55
    .=(1/2)*log(number_e,x to_power 2) by POWER:46
    .=(1/2)*(2*log(number_e,x)) by A1,Lm1,POWER:55,TAYLOR_1:11
    .=log(number_e,x);
  hence thesis;
end;

theorem
  1<x implies log(number_e,x)=cosh1"((x^2+1)/(2*x))
proof
  assume
A1: 1<x;
  then x<x^2 by SQUARE_1:14;
  then 1<x^2 by A1,XXREAL_0:2;
  then
A2: 1-1<x^2-1 by XREAL_1:14;
  1*2<2*x by A1,XREAL_1:68;
  then 1<2*x by XXREAL_0:2;
  then
A3: 1^2<(2*x)^2 by SQUARE_1:16;
  cosh1"((x^2+1)/(2*x)) =log(number_e,((x^2+1)/(2*x))+sqrt(((x^2+1))^2/(2*
  x)^2-1)) by XCMPLX_1:76
    .=log(number_e,((x^2+1)/(2*x))+sqrt((((x^2)^2+2*x^2+1)-1*(2*x)^2)/(2*x)
  ^2)) by A3,XCMPLX_1:126
    .=log(number_e,((x^2+1)/(2*x))+sqrt(((x^2)-1)^2)/sqrt((2*x)^2)) by A1,A2,
SQUARE_1:30
    .=log(number_e,((x^2+1)/(2*x))+(x^2-1)/sqrt((2*x)^2)) by A2,SQUARE_1:22
    .=log(number_e,((x^2+1)/(2*x))+(x^2-1)/(2*x)) by A1,SQUARE_1:22
    .=log(number_e,((x^2+1)+(x^2-1))/(2*x))
    .=log(number_e,(2*x^2)/(2*x))
    .=log(number_e,(x*x)/x) by XCMPLX_1:91
    .=log(number_e,x/(x/x)) by XCMPLX_1:77
    .=log(number_e,x/1) by A1,XCMPLX_1:60
    .=log(number_e,x);
  hence thesis;
end;

theorem
  0<x & x<1 & 1<=(x^2+1)/(2*x) implies log(number_e,x)=cosh2"((x^2+1)/(2 *x))
proof
  assume that
A1: 0<x and
A2: x<1 and
 1<=(x^2+1)/(2*x);
A3: (1/x)=x to_power (-1) by A1,Th1;
  x^2<x by A1,A2,SQUARE_1:13;
  then x^2<1 by A2,XXREAL_0:2;
  then
A4: x^2-x^2<1-x^2 by XREAL_1:14;
  0*2<x*2 by A1;
  then
A5: 0<(2*x)^2;
  cosh2"((x^2+1)/(2*x)) =-log(number_e,((x^2+1)/(2*x))+sqrt(((x^2+1))^2/(
  2*x)^2-1)) by XCMPLX_1:76
    .=-log(number_e,((x^2+1)/(2*x))+sqrt((((x^2)^2+2*x^2+1)-1*(2*x)^2)/(2*x)
  ^2)) by A5,XCMPLX_1:126
    .=-log(number_e,((x^2+1)/(2*x))+sqrt((1-(x^2))^2)/sqrt(2*x)^2) by A1,A4,
SQUARE_1:30
    .=-log(number_e,((x^2+1)/(2*x))+(1-(x^2))/sqrt(2*x)^2) by A4,SQUARE_1:22
    .=-log(number_e,((x^2+1)/(2*x))+(1-x^2)/(2*x)) by A1,SQUARE_1:22
    .=-log(number_e,((x^2+1)+(1-x^2))/(2*x))
    .=-log(number_e,(2*1)/(2*x))
    .=-log(number_e,1/x) by XCMPLX_1:91
    .=-((-1)*log(number_e,x)) by A1,A3,Lm1,POWER:55,TAYLOR_1:11
    .=log(number_e,x);
  hence thesis;
end;

theorem
  0<x implies log(number_e,x)=sinh"((x^2-1)/(2*x))
proof
A1: x^2>=0 by XREAL_1:63;
  assume
A2: 0<x;
  then 0*2<x*2;
  then
A3: 0<(2*x)^2;
  sinh"((x^2-1)/(2*x)) =log(number_e,(((x^2-1)/(2*x))+sqrt((x^2-1)^2/(2*x)
  ^2+1))) by XCMPLX_1:76
    .=log(number_e,(((x^2-1)/(2*x))+sqrt((((x^2)^2-2*x^2+1)+ (2*x)^2*1)/(2*x
  )^2))) by A3,XCMPLX_1:113
    .=log(number_e,(((x^2-1)/(2*x))+sqrt((x^2+1)^2)/sqrt((2*x)^2))) by A2,
SQUARE_1:30
    .=log(number_e,(((x^2-1)/(2*x))+(x^2+1)/sqrt((2*x)^2))) by A1,SQUARE_1:22
    .=log(number_e,((x^2-1)/(2*x)+(x^2+1)/(2*x))) by A2,SQUARE_1:22
    .=log(number_e,(((x^2-1)+(x^2+1))/(2*x)))
    .=log(number_e,((2*x^2)/(2*x)))
    .=log(number_e,(x*x)/x) by XCMPLX_1:91
    .=log(number_e,x/(x/x)) by XCMPLX_1:77
    .=log(number_e,x/1) by A2,XCMPLX_1:60
    .=log(number_e,x);
  hence thesis;
end;

theorem
  y=(1/2)*(exp_R(x)-exp_R(-x)) implies x=log(number_e,(y+sqrt(y^2+1)))
proof
A1: exp_R(x)>0 by SIN_COS:55;
  set t=exp_R(x);
A2: delta(1,-2*y,-1)=((-2)*y)^2-4*1*(-1) by QUIN_1:def 1
    .=4*(y^2)+4;
A3: 0<=y^2 by XREAL_1:63;
  assume y=(1/2)*(exp_R(x)-exp_R(-x));
  then 2*y*exp_R(x)=(exp_R(x)-1/exp_R(x))*exp_R(x) by TAYLOR_1:4;
  then 2*y*t=t^2-(t*1)/t;
  then 2*y*t-2*y*t=t^2-1-2*y*t by A1,XCMPLX_1:60;
  then 1*t^2+(-2*y)*t+(-1)=0;
  then
  t = (-(-2*y)+sqrt delta(1,-2*y,-1))/(2*1) or t = (-(-2*y)-sqrt delta(1,-
  2*y,-1))/(2*1) by A2,A3,QUIN_1:15;
  then t=(2*y+sqrt(4)*sqrt(y^2+1))/2 or t=(2*y-sqrt(4*(y^2+1)))/2 by A2,A3,
SQUARE_1:29;
  then t=(2*y+2*sqrt(y^2+1))/2 or t=(2*y-2*sqrt(y^2+1))/2 by A3,SQUARE_1:20,29;
  then
A4: exp_R(x)=y+sqrt(y^2+1) or exp_R(x)=y-sqrt(y^2+1);
  y<sqrt(y^2+1)+0 by Lm8;
  hence thesis by A1,A4,TAYLOR_1:12,XREAL_1:19;
end;

theorem
  y=(1/2)*(exp_R(x)+exp_R(-x)) & 1<=y implies x=log(number_e,(y+sqrt(y^2
  -1))) or x=-log(number_e,(y+sqrt(y^2-1)))
proof
  assume that
A1: y=(1/2)*(exp_R(x)+exp_R(-x)) and
A2: 1<=y;
A3: y+sqrt(y^2-1)>0 by A2,Lm10;
  set t=exp_R(x);
  2*y*exp_R(x)=(exp_R(x)+1/exp_R(x))*exp_R(x) by A1,TAYLOR_1:4;
  then 0<exp_R(x) & 2*y*t=t^2+(t*1)/t by SIN_COS:55;
  then 2*y*t-2*y*t=t^2+1-2*y*t by XCMPLX_1:60;
  then
A4: 0=1*t^2+(-2*y)*t+1;
A5: delta(1,-2*y,1)=((-2)*y)^2-4*1*1 by QUIN_1:def 1
    .=4*(y^2)-4;
A6: 0<=(y^2)-1 by A2,Lm3;
  then 0*4<=((y^2)-1)*4;
  then
  t = (-(-2*y)+sqrt delta(1,-2*y,1))/(2*1) or t = (-(-2*y)-sqrt delta(1,-
  2*y,1))/(2*1) by A4,A5,QUIN_1:15;
  then t=(2*y+sqrt(4)*sqrt(y^2-1))/2 or t=(2*y-sqrt(4*(y^2-1)))/2 by A6,A5,
SQUARE_1:29;
  then t=(2*y+2*sqrt(y^2-1))/2 or t=(2*y-2*sqrt(y^2-1))/2 by A6,SQUARE_1:20,29;
  then log(number_e,y+sqrt(y^2-1))=x or log(number_e,y-sqrt(y^2-1))=x by
TAYLOR_1:12;
  then
  log(number_e,y+sqrt(y^2-1))=x or log(number_e,(y-sqrt(y^2-1))*(y+sqrt(y
  ^2-1))/ (y+sqrt(y^2-1)))=x by A3,XCMPLX_1:89;
  then log(number_e,y+sqrt(y^2-1)) = x or log(number_e,(y^2-(sqrt(y^2-1))^2)/
  (y+sqrt(y^2-1)))=x;
  then
A7: log(number_e,y+sqrt(y^2-1))=x or log(number_e,(y^2-(y^2-1))/(y+sqrt(y^2
  -1)))=x by A6,SQUARE_1:def 2;
  1/(y+sqrt(y^2-1))=(y+sqrt(y^2-1)) to_power (-1) by A3,Th1;
  then log(number_e,y+sqrt(y^2-1))=x or (-1)*log(number_e,(y+sqrt(y^2-1)))=x
  by A3,A7,Lm1,POWER:55,TAYLOR_1:11;
  hence thesis;
end;

theorem
  y=(exp_R(x)-exp_R(-x))/(exp_R(x)+exp_R(-x)) implies x=(1/2)*log(
  number_e,(1+y)/(1-y))
proof
A1: 0<exp_R(x) by SIN_COS:55;
  set t=exp_R(x);
  assume y=(exp_R(x)-exp_R(-x))/(exp_R(x)+exp_R(-x));
  then y=(exp_R(x)-1/exp_R(x))/(exp_R(x)+exp_R(-x)) by TAYLOR_1:4;
  then y=(exp_R(x)-1/exp_R(x))/(exp_R(x)+1/exp_R(x)) by TAYLOR_1:4;
  then y=((exp_R(x)*exp_R(x)-1)/exp_R(x))/(exp_R(x)+1/exp_R(x)) by A1,
XCMPLX_1:127;
  then y=(((exp_R x)^2-1)/exp_R(x))/((1+exp_R(x)*exp_R(x))/exp_R(x)) by A1,
XCMPLX_1:113;
  then
A2: y=((exp_R x)^2-1)/(1+(exp_R(x))^2) by A1,XCMPLX_1:55;
  then 1*y+t^2*y=(t^2-1)/(1+t^2)*(1+t^2);
  then y+t^2*y-(t^2-1)=t^2-1-(t^2-1) by A1,XCMPLX_1:87;
  then t^2*(y-1)/(y-1)=(-(y+1))/(y-1);
  then
A3: t^2*(y-1)/(y-1)=(y+1)/(-(y-1)) by XCMPLX_1:192;
  y-1<>0 by A2,Th31;
  then sqrt(t^2)=sqrt((y+1)/(1-y)) by A3,XCMPLX_1:89;
  then
A4: exp_R(x)=sqrt((y+1)/(1-y)) by A1,SQUARE_1:22;
  -1<y by A2,Lm11,SIN_COS:55;
  then
A5: 0<(y+1)/(1-y) by A2,Th31,Th32;
  then sqrt((y+1)/(1-y))=((y+1)/(1-y)) to_power (1/2) by ASYMPT_1:83;
  then log(number_e,((y+1)/(1-y)) to_power (1/2))=x by A4,TAYLOR_1:12;
  hence thesis by A5,Lm1,POWER:55,TAYLOR_1:11;
end;

theorem
  y=(exp_R(x)+exp_R(-x))/(exp_R(x)-exp_R(-x)) & x<>0 implies x=(1/2)*log
  (number_e,(y+1)/(y-1))
proof
A1: 0<exp_R(x) by SIN_COS:55;
  set t=exp_R x;
  assume that
A2: y=(exp_R(x)+exp_R(-x))/(exp_R(x)-exp_R(-x)) and
A3: x<>0;
  y=(exp_R(x)+1/exp_R(x))/(exp_R(x)-exp_R(-x)) by A2,TAYLOR_1:4;
  then y=(exp_R(x)+1/exp_R(x))/(exp_R(x)-1/exp_R(x)) by TAYLOR_1:4;
  then y=(exp_R(x)+1/exp_R(x))/((exp_R(x)*exp_R(x)-1)/exp_R(x)) by A1,
XCMPLX_1:127;
  then y=((1+exp_R(x)*exp_R(x))/exp_R(x))/(((exp_R(x))^2-1)/exp_R(x)) by A1,
XCMPLX_1:113;
  then
A4: y=(1+(exp_R x)^2)/((exp_R x)^2-1) by A1,XCMPLX_1:55;
  then y*(t^2-1)=1+t^2 by A3,Th30,XCMPLX_1:87;
  then
A5: t^2*(y-1)/(y-1)=(y+1)/(y-1);
  exp_R(x)<>1 by A3,Th29;
  then
A6: 1<y or y< -1 by A4,Lm12,SIN_COS:55;
  then 1-1<y-1 or y-1< -1-1 by XREAL_1:14;
  then sqrt(t^2)=sqrt((y+1)/(y-1)) by A5,XCMPLX_1:89;
  then
A7: exp_R(x)=sqrt((y+1)/(y-1)) by A1,SQUARE_1:22;
A8: 0<(y+1)/(y-1) by A6,Lm7;
  then sqrt((y+1)/(y-1))=((y+1)/(y-1)) to_power (1/2) by ASYMPT_1:83;
  then log(number_e,((y+1)/(y-1)) to_power (1/2))=x by A7,TAYLOR_1:12;
  hence thesis by A8,Lm1,POWER:55,TAYLOR_1:11;
end;

theorem
  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)
proof
  set t=exp_R(x);
A1: delta(y,-2,y) =(-2)^2-4*y*y by QUIN_1:def 1
    .=4-4*y^2;
  assume y=1/((exp_R(x)+exp_R(-x))/2);
  then y=(1*2)/(2*((exp_R(x)+exp_R(-x))/2)) by XCMPLX_1:91;
  then 0<exp_R(x) & y=2/(exp_R(x)+1/exp_R(x)) by SIN_COS:55,TAYLOR_1:4;
  then y=2/((1+exp_R(x)*exp_R(x))/exp_R(x)) by XCMPLX_1:113;
  then y=2*(exp_R(x)/(1+(exp_R(x))^2)) by XCMPLX_1:79;
  then
A2: y=2*t/(1+t^2);
  then
A3: 0<y by Lm13,SIN_COS:55;
  1+t^2>0 by Lm6;
  then
A4: y*(1+t^2)=(2*t) by A2,XCMPLX_1:87;
A5: y<=1 by A2,Lm14,SIN_COS:55;
  then
A6: 0<=1-y^2 by A3,Lm16;
  Polynom(y,-2,y,t)=y*t^2+(-2)*t+y by POLYEQ_1:def 2;
  then
  t=(-(-2)+sqrt delta(y,-2,y))/(2*y) or t=(-(-2)-sqrt delta(y,-2,y))/(2*y
  ) by A3,A5,A4,A1,Lm17,QUIN_1:15;
  then t=(2+sqrt(4*(1-y^2)))/(2*y) or t=(2-sqrt(4*(1-y^2)))/(2*y) by A1;
  then t=(2+2*sqrt(1-y^2))/(2*y) or t=(2-2*sqrt(1-y^2))/(2*y) by A6,SQUARE_1:20
,29;
  then t=(2*(1+sqrt(1-y^2)))/(2*y) or t=(2*(1-sqrt(1-y^2)))/(2*y);
  then
A7: t=(1+sqrt(1-y^2))/y or t=(1-sqrt(1-y^2))/y by XCMPLX_1:91;
  0<1+sqrt(1-y^2) by A3,A5,Lm18;
  then
  t=(1+sqrt(1-y^2))/y or t=((1-sqrt(1-y^2))*(1+sqrt(1-y^2)))/(y*(1+sqrt(1
  -y^2))) by A7,XCMPLX_1:91;
  then t=(1+sqrt(1-y^2))/y or t=(1-(sqrt(1-y^2))^2)/(y*(1+sqrt(1-y^2)));
  then t=(1+sqrt(1-y^2))/y or t=(1-(1-y^2))/(y*(1+sqrt(1-y^2))) by A6,
SQUARE_1:def 2;
  then
A8: t=(1+sqrt(1-y^2))/y or t=y/(1+sqrt(1-y^2)) by A3,XCMPLX_1:91;
  log(number_e,exp_R(x))=x & 1/((1+sqrt(1-y^2))/y)=((1+sqrt(1-y^2))/y)
  to_power (-1) by A3,A5,Lm19,Th1,TAYLOR_1:12;
  then
A9: log(number_e,(1+sqrt(1-y^2))/y)=x or log(number_e,((1+sqrt(1-y^2))/y)
  to_power (-1))=x by A8,XCMPLX_1:57;
  0<(1+sqrt(1-y^2))/y by A3,A5,Lm19;
  then
  log(number_e,(1+sqrt(1-y^2))/y)=x or (-1)*log(number_e,((1+sqrt(1-y^2))
  /y))=x by A9,Lm1,POWER:55,TAYLOR_1:11;
  hence thesis;
end;

theorem
  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)
proof
A1: 0<exp_R(x) by SIN_COS:55;
  set t=exp_R x;
  assume that
A2: y=1/((exp_R(x)-exp_R(-x))/2) and
A3: x<>0;
A4: delta(y,-2,-y)=(-2)^2-4*y*(-y) by QUIN_1:def 1
    .=4+4*y^2;
  y=(1*2)/(2*((exp_R(x)-exp_R(-x))/2)) by A2,XCMPLX_1:91;
  then y=2/(exp_R(x)-1/exp_R(x)) by TAYLOR_1:4;
  then y=2/((exp_R(x)*exp_R(x)-1)/exp_R(x)) by A1,XCMPLX_1:127;
  then
A5: y=2*(exp_R(x)/((exp_R(x))^2-1)) by XCMPLX_1:79;
  then
A6: y=2*exp_R(x)/((exp_R(x))^2-1);
  then y*(t^2-1)=2*t by A3,Th30,XCMPLX_1:87;
  then
A7: y*t^2+(-2)*t+(-y)=0;
A8: exp_R(x)<>1 by A3,Th29;
  then
A9: 2*exp_R(x)/((exp_R(x))^2-1)<>0 by Lm20,SIN_COS:55;
  per cases by A9,A5;
  suppose
A10: 0<y;
A11: 0<1+y^2 by Lm6;
    then 0*4<4*(1+y^2);
    then
    t=(2+sqrt delta(y,-2,-y))/(2*y) or t=(-(-2)-sqrt delta(y,-2,-y))/(2*y
    ) by A1,A8,A6,A7,A4,Lm20,QUIN_1:15;
    then
    t=(2+sqrt(4)*sqrt(1+y^2))/(2*y) or t=(2-sqrt(4*(1+y^2)))/(2*y) by A4,A11,
SQUARE_1:29;
    then t=(2*(1+sqrt(1+y^2)))/(2*y) or t=(2-2*sqrt(1+y^2))/(2*y) by A11,
SQUARE_1:20,29;
    then
A12: t=(1+sqrt(1+y^2))/y or t=(2*(1-sqrt(1+y^2)))/(2*y) by XCMPLX_1:91;
    (1-sqrt(1+y^2))/y<0 by A10,Lm15;
    hence thesis by A1,A12,TAYLOR_1:12,XCMPLX_1:91;
  end;
  suppose
A13: y<0;
A14: 0<1+y^2 by Lm6;
    then 0*4<4*(1+y^2);
    then
    t=(2+sqrt delta(y,-2,-y))/(2*y) or t=(-(-2)-sqrt delta(y,-2,-y))/(2*y
    ) by A1,A8,A6,A7,A4,Lm20,QUIN_1:15;
    then
    t=(2+sqrt(4)*sqrt(1+y^2))/(2*y) or t=(2-sqrt(4*(1+y^2)))/(2*y) by A4,A14,
SQUARE_1:29;
    then t=(2*(1+sqrt(1+y^2)))/(2*y) or t=(2-2*sqrt(1+y^2))/(2*y) by A14,
SQUARE_1:20,29;
    then
A15: t=(1+sqrt(1+y^2))/y or t=(2*(1-sqrt(1+y^2)))/(2*y) by XCMPLX_1:91;
    (1+sqrt(1+y^2))/y<0 by A13,Lm21;
    then exp_R(x)=(1-sqrt(1+y^2))/y by A15,SIN_COS:55,XCMPLX_1:91;
    hence thesis by TAYLOR_1:12;
  end;
end;

theorem Th69:
  cosh.(2*x)=1+2*(sinh.x)^2
proof
  2*(sinh.x)^2=2*(1/2*(cosh.(2*x)-1)) by SIN_COS2:18;
  hence thesis;
end;

theorem Th70:
  (cosh.x)^2=1+(sinh.x)^2
proof
  cosh.(2*x)=cosh.(x+x) .=(cosh.x)^2+(sinh.x)^2 by SIN_COS2:20;
  then 1+2*(sinh.x)^2-(sinh.x)^2=(cosh.x)^2+(sinh.x)^2-(sinh.x)^2 by Th69;
  hence thesis;
end;

theorem Th71:
  (sinh.x)^2=(cosh.x)^2-1
proof
  (cosh.x)^2-(sinh.x)^2-1=1-1 by SIN_COS2:14;
  hence thesis;
end;

theorem
  sinh(5*x)=5*sinh(x)+20*(sinh(x))|^3+16*(sinh(x))|^5
proof
  set t = sinh.x;
  sinh(5*x) =sinh.(4*x+x) by SIN_COS2:def 2
    .=sinh.(2*(2*x))*(cosh.x)+(cosh.(4*x))*t by SIN_COS2:21
    .=2*(sinh.(2*x))*(cosh.(2*x))*(cosh.x)+(cosh.(4*x))*t by SIN_COS2:23
    .=2*(2*t*(cosh.x))*(cosh.(2*x))*(cosh.x)+(cosh.(4*x))*t by SIN_COS2:23
    .=4*t*((cosh.x)^2)*(cosh.(2*x))+(cosh.(4*x))*t
    .=4*t*((cosh.x)^2)*(1+2*t^2)+(cosh.(2*(2*x)))*t by Th69
    .=4*t*((cosh.x)^2)*(1+2*t^2)+(1+2*(sinh.(2*x))^2)*t by Th69
    .=4*t*((cosh.x)^2)*(1+2*t^2)+(1+2*(2*t* (cosh.x))^2)*t by SIN_COS2:23
    .=4*t*((cosh.x)^2)*(1+2*t^2)+t+8*t^2*t*(cosh.x)^2
    .=4*t*((cosh.x)^2)*(1+2*t^2)+t+8*(t|^1*t)*t*(cosh.x)^2
    .=4*t*((cosh.x)^2)*(1+2*t^2)+t+8*t|^(1+1)*t*(cosh.x)^2 by NEWTON:6
    .=4*t*((cosh.x)^2)*(1+2*t^2)+t+8*(t|^2*t)*(cosh.x)^2
    .=4*t*((cosh.x)^2)*(1+2*t^2)+t+8*(t|^(2+1))*(cosh.x)^2 by NEWTON:6
    .=4*t*((cosh.x)^2)*1+4*t*((cosh.x)^2)*2*t^2+t+8*t|^3*(cosh.x)^2
    .=4*t*(1+t^2)*1+8*t*((cosh.x)^2)*t^2+t+8*t|^3*(cosh.x)^2 by Th70
    .=4*t+4*t*t*t+8*t*((cosh.x)^2)*t^2+sinh.x+8*t|^3*(cosh.x)^2
    .=4*t+4*t|^1*t*t+8*t*((cosh.x)^2)*t^2+t+8*t|^3*(cosh.x)^2
    .=4*t+4*(t|^1*t)*t+8*t*((cosh.x)^2)*t^2+t+8*t|^3*(cosh.x)^2
    .=4*t+4*t|^(1+1)*t+8*t*((cosh.x)^2)* t^2+t+8*t|^3*(cosh.x)^2 by NEWTON:6
    .=4*t+4*(t|^2*t)+8*t*((cosh.x)^2)*t^2+t+8*t|^3*(cosh.x)^2
    .=4*t+4*(t|^(2+1))+8*t*((cosh.x)^2)*t^2+t+8*t|^3*(cosh.x)^2 by NEWTON:6
    .=4*t+4*t|^3+8*t*t*t*((cosh.x)^2)+t+8*t|^3*(cosh.x)^2
    .=4*t+4*t|^3+8*t|^1*t*t* ((cosh.x)^2)+t+8*t|^3*(cosh.x)^2
    .=4*t+4*t|^3+8*(t|^1*t)*t*((cosh.x)^2)+t+8*t|^3*(cosh.x)^2
    .=4*t+4*t|^3+8*(t|^(1+1))*t* ((cosh.x)^2)+t+8*t|^3*(cosh.x)^2 by NEWTON:6
    .=4*t+4*t|^3+8*(t|^2*t)*((cosh.x)^2)+t+8*t|^3*(cosh.x)^2
    .=4*t+4*t|^3+8*(t|^(2+1))* ((cosh.x)^2)+t+8*t|^3*(cosh.x)^2 by NEWTON:6
    .=4*t+4*t|^3+8*t|^3*(1+t^2)+t+8*t|^3*(cosh.x)^2 by Th70
    .=4*t+4*t|^3+8*t|^3+8*(t|^3*t)*t+t+8*t|^3*(cosh.x)^2
    .=4*t+4*t|^3+8*t|^3+8*(t|^(3+1))*t+t+8*t|^3*(cosh.x)^2 by NEWTON:6
    .=4*t+4*t|^3+8*t|^3+8*(t|^4*t)+t+8*t|^3*(cosh.x)^2
    .=4*t+4*t|^3+8*t|^3+8*(t|^(4+1))+t+8*t|^3*(cosh.x)^2 by NEWTON:6
    .=4*t+4*t|^3+8*t|^3+8*t|^5+t+8*t|^3*(1+t^2) by Th70
    .=4*t+4*t|^3+8*t|^3+8*t|^5+t+8*t|^3+8*(t|^3*t)*t
    .=4*t+4*t|^3+8*t|^3+8*t|^5+t+8*t|^3+8*(t|^(3+1))*t by NEWTON:6
    .=4*t+4*t|^3+8*t|^3+8*t|^5+t+8*t|^3+8*(t|^4*t)
    .=4*t+4*t|^3+8*t|^3+8*t|^5+t+8*t|^3+8*(t|^(4+1)) by NEWTON:6
    .=5*t+20*t|^3+(8*t|^5+8*t|^5)
    .=5*sinh(x)+20*t|^3+16*t|^5 by SIN_COS2:def 2
    .=5*sinh(x)+20*(sinh x)|^3+16*t|^5 by SIN_COS2:def 2
    .=5*sinh(x)+20*(sinh x)|^3+16*(sinh x)|^5 by SIN_COS2:def 2;
  hence thesis;
end;

theorem
  cosh(5*x)=5*cosh(x)-20*(cosh(x))|^3+16*(cosh(x))|^5
proof
  set t = cosh.x, u = sinh.x;
  cosh(5*x) = cosh.(4*x+x) by SIN_COS2:def 4
    .=(cosh.(2*(2*x)))*t+(sinh.(4*x))*u by SIN_COS2:20
    .=(1+2*(sinh.(2*x))^2)*t+(sinh.(4*x))*u by Th69
    .=(1+2*((2*u)*t)^2)*t+(sinh.(2*(2*x)))*u by SIN_COS2:23
    .=t+8*u^2*(t^2*t)+(sinh.(2*(2*x)))*u
    .=t+8*u^2*(t|^1*t*t)+(sinh.(2*(2*x)))*u
    .=t+8*u^2*(t|^(1+1)*t)+(sinh.(2*(2*x)))*u by NEWTON:6
    .=t+8*(sinh.x)^2*(t|^(2+1))+(sinh.(2*(2*x)))*u by NEWTON:6
    .=t+8*(t^2-1)*(t|^3)+(sinh.(2*(2*x)))*u by Th71
    .=t+8*(t|^3*t*t)-8*t|^3+(sinh.(2*(2*x)))*u
    .=t+8*(t|^(3+1)*t)-8*t|^3+(sinh.(2*(2*x)))*u by NEWTON:6
    .=t+8*(t|^(4+1))-8*t|^3+(sinh.(2*(2*x)))*u by NEWTON:6
    .=t+8*(t|^5)-8*t|^3+(2*(sinh.(2*x))*(cosh.(2*x)))*u by SIN_COS2:23
    .=t+8*(t|^5)-8*t|^3+(2*(2*u*t)*(cosh.(2*x)))*u by SIN_COS2:23
    .=t+8*(t|^5)-8*t|^3+4*u^2*t*(cosh.(2*x))
    .=t+8*(t|^5)-8*t|^3+4*(t^2-1)*t*(cosh.(2*x)) by Th71
    .=t+8*(t|^5)-8*t|^3+4*(t*t*t)*(cosh.(2*x))-4*t*(cosh.(2*x))
    .=t+8*(t|^5)-8*t|^3+4*(t|^1*t*t)*(cosh.(2*x))-4*t*(cosh.(2*x))
    .=t+8*(t|^5)-8*t|^3+4*(t|^(1+1)*t)*(cosh.(2*x))-4*t*(cosh.(2*x)) by
NEWTON:6
    .=t+8*(t|^5)-8*t|^3+4*(t|^(2+1)) *(cosh.(2*x))-4*t*(cosh.(2*x)) by NEWTON:6
    .=t+8*(t|^5)-8*t|^3+4*t|^3*(2*t^2-1)-4*t*(cosh.(2*x)) by SIN_COS2:23
    .=t+8*(t|^5)-8*t|^3+8*(t|^3*t*t)-4*t|^3-4*t*(cosh.(2*x))
    .=t+8*(t|^5)-8*t|^3+8*(t|^(3+1)*t)-4*t|^3-4*t*(cosh.(2*x)) by NEWTON:6
    .=t+8*(t|^5)-8*t|^3+8*(t|^(4+1))-4*t|^3-4*t*(cosh.(2*x)) by NEWTON:6
    .=t+16*(t|^5)-12*t|^3-4*t*(2*t^2-1) by SIN_COS2:23
    .=5*t+16*(t|^5)-12*t|^3-8*(t*t*t)
    .=5*t+16*(t|^5)-12*t|^3-8*(t|^1*t*t)
    .=5*t+16*(t|^5)-12*t|^3-8*(t|^(1+1)*t) by NEWTON:6
    .=5*t+16*(t|^5)-12*t|^3-8*(t|^(2+1)) by NEWTON:6
    .=5*t-20*t|^3+16*(t|^5)
    .=5*(cosh x)-20*t|^3+16*(t|^5) by SIN_COS2:def 4
    .=5*(cosh x)-20*(cosh x)|^3+16*(t|^5) by SIN_COS2:def 4
    .=5*cosh(x)-20*(cosh x)|^3+16*(cosh x)|^5 by SIN_COS2:def 4;
  hence thesis;
end;