:: SIN_COS2 semantic presentation

begin


theorem Th1: :: SIN_COS2:1
for p, r being real number st p >= 0 & r >= 0 holds
p + r >= 2 * (sqrt (p * r))
proof
let p, r be real number ; ::_thesis: ( p >= 0 & r >= 0 implies p + r >= 2 * (sqrt (p * r)) )
assume that
A1: p >= 0 and
A2: r >= 0 ; ::_thesis: p + r >= 2 * (sqrt (p * r))
A3: ((sqrt p) - (sqrt r)) ^2 >= 0 by XREAL_1:63;
((sqrt p) - (sqrt r)) ^2 = (((sqrt p) ^2) - ((2 * (sqrt p)) * (sqrt r))) + ((sqrt r) ^2)
.= (p - ((2 * (sqrt p)) * (sqrt r))) + ((sqrt r) ^2) by A1, SQUARE_1:def_2
.= (p - ((2 * (sqrt p)) * (sqrt r))) + r by A2, SQUARE_1:def_2
.= (p + r) - ((2 * (sqrt p)) * (sqrt r)) ;
then  0 + ((2 * (sqrt p)) * (sqrt r)) <= p + r by A3, XREAL_1:19;
then  2 * ((sqrt p) * (sqrt r)) <= p + r ;
hence  p + r >= 2 * (sqrt (p * r)) by A1, A2, SQUARE_1:29; ::_thesis: verum
end;

theorem :: SIN_COS2:2
sin | ].0,(PI / 2).[ is increasing
proof
 for th being Real st th in ].0,(PI / 2).[ holds
0 < diff (sin,th)
proof
let th be Real; ::_thesis: ( th in ].0,(PI / 2).[ implies 0 < diff (sin,th) )
assume  th in ].0,(PI / 2).[ ; ::_thesis: 0 < diff (sin,th)
then  cos . th > 0 by SIN_COS:80;
hence  0 < diff (sin,th) by SIN_COS:68; ::_thesis: verum
end;
hence  sin | ].0,(PI / 2).[ is increasing by FDIFF_1:26, ROLLE:9, SIN_COS:24, SIN_COS:68; ::_thesis: verum
end;

Lm1:  for th being real number st th in ].0,(PI / 2).[ holds
0 < sin . th
proof
let th be real number ; ::_thesis: ( th in ].0,(PI / 2).[ implies 0 < sin . th )
assume A1: th in ].0,(PI / 2).[ ; ::_thesis: 0 < sin . th
then  th < PI / 2 by XXREAL_1:4;
then  - th > - (PI / 2) by XREAL_1:24;
then A2: (- th) + (PI / 2) > (- (PI / 2)) + (PI / 2) by XREAL_1:6;
 0 < th by A1, XXREAL_1:4;
then  0 - th < 0 ;
then  (- th) + (PI / 2) < 0 + (PI / 2) by XREAL_1:6;
then  (PI / 2) - th in ].0,(PI / 2).[ by A2, XXREAL_1:4;
then  cos . ((PI / 2) - th) > 0 by SIN_COS:80;
hence  0 < sin . th by SIN_COS:78; ::_thesis: verum
end;

theorem :: SIN_COS2:3
sin | ].(PI / 2),PI.[ is decreasing
proof
 for th1 being Real st th1 in ].(PI / 2),PI.[ holds
0 > diff (sin,th1)
proof
let th1 be Real; ::_thesis: ( th1 in ].(PI / 2),PI.[ implies 0 > diff (sin,th1) )
assume A1: th1 in ].(PI / 2),PI.[ ; ::_thesis: 0 > diff (sin,th1)
then  th1 < PI by XXREAL_1:4;
then A2: th1 - (PI / 2) < PI - (PI / 2) by XREAL_1:9;
 PI / 2 < th1 by A1, XXREAL_1:4;
then  (PI / 2) - (PI / 2) < th1 - (PI / 2) by XREAL_1:9;
then  th1 - (PI / 2) in ].0,(PI / 2).[ by A2, XXREAL_1:4;
then  sin . (th1 - (PI / 2)) > 0 by Lm1;
then A3: 0 - (sin . (th1 - (PI / 2))) < 0 ;
diff (sin,th1) = cos . ((PI / 2) + (th1 - (PI / 2))) by SIN_COS:68
.= - (sin . (th1 - (PI / 2))) by SIN_COS:78 ;
hence  0 > diff (sin,th1) by A3; ::_thesis: verum
end;
hence  sin | ].(PI / 2),PI.[ is decreasing by FDIFF_1:26, ROLLE:10, SIN_COS:24, SIN_COS:68; ::_thesis: verum
end;

theorem :: SIN_COS2:4
cos | ].0,(PI / 2).[ is decreasing
proof
 for th being Real st th in ].0,(PI / 2).[ holds
diff (cos,th) < 0
proof
let th be Real; ::_thesis: ( th in ].0,(PI / 2).[ implies diff (cos,th) < 0 )
assume  th in ].0,(PI / 2).[ ; ::_thesis: diff (cos,th) < 0
then  0 < sin . th by Lm1;
then  ( diff (cos,th) = - (sin . th) & 0 - (sin . th) < 0 ) by SIN_COS:67;
hence  diff (cos,th) < 0 ; ::_thesis: verum
end;
hence  cos | ].0,(PI / 2).[ is decreasing by FDIFF_1:26, ROLLE:10, SIN_COS:24, SIN_COS:67; ::_thesis: verum
end;

theorem :: SIN_COS2:5
cos | ].(PI / 2),PI.[ is decreasing
proof
 for th being Real st th in ].(PI / 2),PI.[ holds
diff (cos,th) < 0
proof
let th be Real; ::_thesis: ( th in ].(PI / 2),PI.[ implies diff (cos,th) < 0 )
assume A1: th in ].(PI / 2),PI.[ ; ::_thesis: diff (cos,th) < 0
then  th < PI by XXREAL_1:4;
then A2: th - (PI / 2) < PI - (PI / 2) by XREAL_1:9;
 PI / 2 < th by A1, XXREAL_1:4;
then  (PI / 2) - (PI / 2) < th - (PI / 2) by XREAL_1:9;
then  th - (PI / 2) in ].0,(PI / 2).[ by A2, XXREAL_1:4;
then  cos . (th - (PI / 2)) > 0 by SIN_COS:80;
then A3: 0 - (cos . (th - (PI / 2))) < 0 ;
diff (cos,th) = - (sin . ((PI / 2) + (th - (PI / 2)))) by SIN_COS:67
.= - (cos . (th - (PI / 2))) by SIN_COS:78 ;
hence  diff (cos,th) < 0 by A3; ::_thesis: verum
end;
hence  cos | ].(PI / 2),PI.[ is decreasing by FDIFF_1:26, ROLLE:10, SIN_COS:24, SIN_COS:67; ::_thesis: verum
end;

theorem :: SIN_COS2:6
sin | ].PI,((3 / 2) * PI).[ is decreasing
proof
 for th being Real st th in ].PI,((3 / 2) * PI).[ holds
diff (sin,th) < 0
proof
let th be Real; ::_thesis: ( th in ].PI,((3 / 2) * PI).[ implies diff (sin,th) < 0 )
assume A1: th in ].PI,((3 / 2) * PI).[ ; ::_thesis: diff (sin,th) < 0
 th < (3 / 2) * PI by A1, XXREAL_1:4;
then A2: th - PI < ((3 / 2) * PI) - PI by XREAL_1:9;
 PI < th by A1, XXREAL_1:4;
then  PI - PI < th - PI by XREAL_1:9;
then  th - PI in ].0,(PI / 2).[ by A2, XXREAL_1:4;
then  cos . (th - PI) > 0 by SIN_COS:80;
then A3: 0 - (cos . (th - PI)) < 0 ;
diff (sin,th) = cos . (PI + (th - PI)) by SIN_COS:68
.= - (cos . (th - PI)) by SIN_COS:78 ;
hence  diff (sin,th) < 0 by A3; ::_thesis: verum
end;
hence  sin | ].PI,((3 / 2) * PI).[ is decreasing by FDIFF_1:26, ROLLE:10, SIN_COS:24, SIN_COS:68; ::_thesis: verum
end;

theorem :: SIN_COS2:7
sin | ].((3 / 2) * PI),(2 * PI).[ is increasing
proof
 for th being Real st th in ].((3 / 2) * PI),(2 * PI).[ holds
diff (sin,th) > 0
proof
let th be Real; ::_thesis: ( th in ].((3 / 2) * PI),(2 * PI).[ implies diff (sin,th) > 0 )
assume A1: th in ].((3 / 2) * PI),(2 * PI).[ ; ::_thesis: diff (sin,th) > 0
 th < 2 * PI by A1, XXREAL_1:4;
then A2: th - ((3 / 2) * PI) < (2 * PI) - ((3 / 2) * PI) by XREAL_1:9;
A3: diff (sin,th) = cos . (PI + ((PI / 2) + (th - ((3 / 2) * PI)))) by SIN_COS:68
.= - (cos . ((PI / 2) + (th - ((3 / 2) * PI)))) by SIN_COS:78
.= - (- (sin . (th - ((3 / 2) * PI)))) by SIN_COS:78
.= sin . (th - ((3 / 2) * PI)) ;
 (3 / 2) * PI < th by A1, XXREAL_1:4;
then  ((3 / 2) * PI) - ((3 / 2) * PI) < th - ((3 / 2) * PI) by XREAL_1:9;
then  th - ((3 / 2) * PI) in ].0,(PI / 2).[ by A2, XXREAL_1:4;
hence  diff (sin,th) > 0 by A3, Lm1; ::_thesis: verum
end;
hence  sin | ].((3 / 2) * PI),(2 * PI).[ is increasing by FDIFF_1:26, ROLLE:9, SIN_COS:24, SIN_COS:68; ::_thesis: verum
end;

theorem :: SIN_COS2:8
cos | ].PI,((3 / 2) * PI).[ is increasing
proof
 for th being Real st th in ].PI,((3 / 2) * PI).[ holds
diff (cos,th) > 0
proof
let th be Real; ::_thesis: ( th in ].PI,((3 / 2) * PI).[ implies diff (cos,th) > 0 )
assume A1: th in ].PI,((3 / 2) * PI).[ ; ::_thesis: diff (cos,th) > 0
 th < (3 / 2) * PI by A1, XXREAL_1:4;
then A2: th - PI < ((3 / 2) * PI) - PI by XREAL_1:9;
A3: diff (cos,th) = - (sin . (PI + (th - PI))) by SIN_COS:67
.= - (- (sin . (th - PI))) by SIN_COS:78
.= sin . (th - PI) ;
 PI < th by A1, XXREAL_1:4;
then  PI - PI < th - PI by XREAL_1:9;
then  th - PI in ].0,(PI / 2).[ by A2, XXREAL_1:4;
hence  diff (cos,th) > 0 by A3, Lm1; ::_thesis: verum
end;
hence  cos | ].PI,((3 / 2) * PI).[ is increasing by FDIFF_1:26, ROLLE:9, SIN_COS:24, SIN_COS:67; ::_thesis: verum
end;

theorem :: SIN_COS2:9
cos | ].((3 / 2) * PI),(2 * PI).[ is increasing
proof
 for th being Real st th in ].((3 / 2) * PI),(2 * PI).[ holds
diff (cos,th) > 0
proof
let th be Real; ::_thesis: ( th in ].((3 / 2) * PI),(2 * PI).[ implies diff (cos,th) > 0 )
assume A1: th in ].((3 / 2) * PI),(2 * PI).[ ; ::_thesis: diff (cos,th) > 0
 th < 2 * PI by A1, XXREAL_1:4;
then A2: th - ((3 / 2) * PI) < (2 * PI) - ((3 / 2) * PI) by XREAL_1:9;
A3: diff (cos,th) = - (sin . (PI + ((PI / 2) + (th - ((3 / 2) * PI))))) by SIN_COS:67
.= - (- (sin . ((PI / 2) + (th - ((3 / 2) * PI))))) by SIN_COS:78
.= cos . (th - ((3 / 2) * PI)) by SIN_COS:78 ;
 (3 / 2) * PI < th by A1, XXREAL_1:4;
then  ((3 / 2) * PI) - ((3 / 2) * PI) < th - ((3 / 2) * PI) by XREAL_1:9;
then  th - ((3 / 2) * PI) in ].0,(PI / 2).[ by A2, XXREAL_1:4;
hence  diff (cos,th) > 0 by A3, SIN_COS:80; ::_thesis: verum
end;
hence  cos | ].((3 / 2) * PI),(2 * PI).[ is increasing by FDIFF_1:26, ROLLE:9, SIN_COS:24, SIN_COS:67; ::_thesis: verum
end;

theorem :: SIN_COS2:10
for th being real number
for n being Nat holds sin . th = sin . (((2 * PI) * n) + th)
proof
let th be real number ; ::_thesis: for n being Nat holds sin . th = sin . (((2 * PI) * n) + th)
defpred S1[ Nat] means  for th being real number holds sin . th = sin . (((2 * PI) * $1) + th);
let n be Nat; ::_thesis: sin . th = sin . (((2 * PI) * n) + th)
A1: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: for th being real number holds sin . th = sin . (((2 * PI) * n) + th) ; ::_thesis: S1[n + 1]
 for th being real number holds sin . th = sin . (((2 * PI) * (n + 1)) + th)
proof
let th be real number ; ::_thesis: sin . th = sin . (((2 * PI) * (n + 1)) + th)
sin . (((2 * PI) * (n + 1)) + th) = sin . ((((2 * PI) * n) + th) + (2 * PI))
.= sin . (((2 * PI) * n) + th) by SIN_COS:78
.= sin . th by A2 ;
hence  sin . th = sin . (((2 * PI) * (n + 1)) + th) ; ::_thesis: verum
end;
hence  S1[n + 1] ; ::_thesis: verum
end;
A3: S1[ 0 ] ;
 for n being Nat holds S1[n] from NAT_1:sch_2(A3, A1);
hence  sin . th = sin . (((2 * PI) * n) + th) ; ::_thesis: verum
end;

theorem :: SIN_COS2:11
for th being real number
for n being Nat holds cos . th = cos . (((2 * PI) * n) + th)
proof
let th be real number ; ::_thesis: for n being Nat holds cos . th = cos . (((2 * PI) * n) + th)
defpred S1[ Nat] means  for th being real number holds cos . th = cos . (((2 * PI) * $1) + th);
let n be Nat; ::_thesis: cos . th = cos . (((2 * PI) * n) + th)
A1: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: for th being real number holds cos . th = cos . (((2 * PI) * n) + th) ; ::_thesis: S1[n + 1]
 for th being real number holds cos . th = cos . (((2 * PI) * (n + 1)) + th)
proof
let th be real number ; ::_thesis: cos . th = cos . (((2 * PI) * (n + 1)) + th)
cos . (((2 * PI) * (n + 1)) + th) = cos . ((((2 * PI) * n) + th) + (2 * PI))
.= cos . (((2 * PI) * n) + th) by SIN_COS:78
.= cos . th by A2 ;
hence  cos . th = cos . (((2 * PI) * (n + 1)) + th) ; ::_thesis: verum
end;
hence  S1[n + 1] ; ::_thesis: verum
end;
A3: S1[ 0 ] ;
 for n being Nat holds S1[n] from NAT_1:sch_2(A3, A1);
hence  cos . th = cos . (((2 * PI) * n) + th) ; ::_thesis: verum
end;

begin

definition
func sinh  ->  Function of REAL,REAL means :Def1: :: SIN_COS2:def 1
 for d being real number holds it . d = ((exp_R . d) - (exp_R . (- d))) / 2;
existence
 ex b1 being Function of REAL,REAL st
for d being real number holds b1 . d = ((exp_R . d) - (exp_R . (- d))) / 2
proof
deffunc H1( Real) ->  Element of REAL = ((exp_R . $1) - (exp_R . (- $1))) / 2;
consider f being Function of REAL,REAL such that
A1: for d being Element of REAL holds f . d = H1(d) from FUNCT_2:sch_4();
take  f ; ::_thesis: for d being real number holds f . d = ((exp_R . d) - (exp_R . (- d))) / 2
let d be real number ; ::_thesis: f . d = ((exp_R . d) - (exp_R . (- d))) / 2
 d is Real by XREAL_0:def_1;
hence  f . d = ((exp_R . d) - (exp_R . (- d))) / 2 by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of REAL,REAL st ( for d being real number holds b1 . d = ((exp_R . d) - (exp_R . (- d))) / 2 ) & ( for d being real number holds b2 . d = ((exp_R . d) - (exp_R . (- d))) / 2 ) holds
b1 = b2
proof
let f1, f2 be Function of REAL,REAL; ::_thesis: ( ( for d being real number holds f1 . d = ((exp_R . d) - (exp_R . (- d))) / 2 ) & ( for d being real number holds f2 . d = ((exp_R . d) - (exp_R . (- d))) / 2 ) implies f1 = f2 )
assume A2: for d being real number holds f1 . d = ((exp_R . d) - (exp_R . (- d))) / 2 ; ::_thesis: ( ex d being real number st not f2 . d = ((exp_R . d) - (exp_R . (- d))) / 2 or f1 = f2 )
assume A3: for d being real number holds f2 . d = ((exp_R . d) - (exp_R . (- d))) / 2 ; ::_thesis: f1 = f2
 for d being Element of REAL holds f1 . d = f2 . d
proof
let d be Element of REAL ; ::_thesis: f1 . d = f2 . d
thus f1 . d = ((exp_R . d) - (exp_R . (- d))) / 2 by A2
.= f2 . d by A3 ; ::_thesis: verum
end;
hence  f1 = f2 by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines sinh SIN_COS2:def_1_:_
 for b1 being Function of REAL,REAL holds
( b1 = sinh iff for d being real number holds b1 . d = ((exp_R . d) - (exp_R . (- d))) / 2 );

definition
let d be number ;
func sinh d ->  set  equals :: SIN_COS2:def 2
sinh . d;
coherence
 sinh . d is set ;
end;

:: deftheorem  defines sinh SIN_COS2:def_2_:_
 for d being number holds sinh d = sinh . d;

registration
let d be number ;
cluster sinh d ->  real ;
coherence
 sinh d is real ;
end;

definition
let d be number ;
:: original: sinh
redefine func sinh d ->  Real;
coherence
 sinh d is Real ;
end;

definition
func cosh  ->  Function of REAL,REAL means :Def3: :: SIN_COS2:def 3
 for d being real number holds it . d = ((exp_R . d) + (exp_R . (- d))) / 2;
existence
 ex b1 being Function of REAL,REAL st
for d being real number holds b1 . d = ((exp_R . d) + (exp_R . (- d))) / 2
proof
deffunc H1( Real) ->  Element of REAL = ((exp_R . $1) + (exp_R . (- $1))) / 2;
consider f being Function of REAL,REAL such that
A1: for d being Element of REAL holds f . d = H1(d) from FUNCT_2:sch_4();
take  f ; ::_thesis: for d being real number holds f . d = ((exp_R . d) + (exp_R . (- d))) / 2
let d be real number ; ::_thesis: f . d = ((exp_R . d) + (exp_R . (- d))) / 2
 d is Real by XREAL_0:def_1;
hence  f . d = ((exp_R . d) + (exp_R . (- d))) / 2 by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of REAL,REAL st ( for d being real number holds b1 . d = ((exp_R . d) + (exp_R . (- d))) / 2 ) & ( for d being real number holds b2 . d = ((exp_R . d) + (exp_R . (- d))) / 2 ) holds
b1 = b2
proof
let f1, f2 be Function of REAL,REAL; ::_thesis: ( ( for d being real number holds f1 . d = ((exp_R . d) + (exp_R . (- d))) / 2 ) & ( for d being real number holds f2 . d = ((exp_R . d) + (exp_R . (- d))) / 2 ) implies f1 = f2 )
assume A2: for d being real number holds f1 . d = ((exp_R . d) + (exp_R . (- d))) / 2 ; ::_thesis: ( ex d being real number st not f2 . d = ((exp_R . d) + (exp_R . (- d))) / 2 or f1 = f2 )
assume A3: for d being real number holds f2 . d = ((exp_R . d) + (exp_R . (- d))) / 2 ; ::_thesis: f1 = f2
 for d being Element of REAL holds f1 . d = f2 . d
proof
let d be Element of REAL ; ::_thesis: f1 . d = f2 . d
thus f1 . d = ((exp_R . d) + (exp_R . (- d))) / 2 by A2
.= f2 . d by A3 ; ::_thesis: verum
end;
hence  f1 = f2 by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines cosh SIN_COS2:def_3_:_
 for b1 being Function of REAL,REAL holds
( b1 = cosh iff for d being real number holds b1 . d = ((exp_R . d) + (exp_R . (- d))) / 2 );

definition
let d be number ;
func cosh d ->  set  equals :: SIN_COS2:def 4
cosh . d;
coherence
 cosh . d is set ;
end;

:: deftheorem  defines cosh SIN_COS2:def_4_:_
 for d being number holds cosh d = cosh . d;

registration
let d be number ;
cluster cosh d ->  real ;
coherence
 cosh d is real ;
end;

definition
let d be number ;
:: original: cosh
redefine func cosh d ->  Real;
coherence
 cosh d is Real ;
end;

definition
func tanh  ->  Function of REAL,REAL means :Def5: :: SIN_COS2:def 5
 for d being real number holds it . d = ((exp_R . d) - (exp_R . (- d))) / ((exp_R . d) + (exp_R . (- d)));
existence
 ex b1 being Function of REAL,REAL st
for d being real number holds b1 . d = ((exp_R . d) - (exp_R . (- d))) / ((exp_R . d) + (exp_R . (- d)))
proof
deffunc H1( Real) ->  Element of REAL = ((exp_R . $1) - (exp_R . (- $1))) / ((exp_R . $1) + (exp_R . (- $1)));
consider f being Function of REAL,REAL such that
A1: for d being Element of REAL holds f . d = H1(d) from FUNCT_2:sch_4();
take  f ; ::_thesis: for d being real number holds f . d = ((exp_R . d) - (exp_R . (- d))) / ((exp_R . d) + (exp_R . (- d)))
let d be real number ; ::_thesis: f . d = ((exp_R . d) - (exp_R . (- d))) / ((exp_R . d) + (exp_R . (- d)))
 d is Real by XREAL_0:def_1;
hence  f . d = ((exp_R . d) - (exp_R . (- d))) / ((exp_R . d) + (exp_R . (- d))) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of REAL,REAL st ( for d being real number holds b1 . d = ((exp_R . d) - (exp_R . (- d))) / ((exp_R . d) + (exp_R . (- d))) ) & ( for d being real number holds b2 . d = ((exp_R . d) - (exp_R . (- d))) / ((exp_R . d) + (exp_R . (- d))) ) holds
b1 = b2
proof
let f1, f2 be Function of REAL,REAL; ::_thesis: ( ( for d being real number holds f1 . d = ((exp_R . d) - (exp_R . (- d))) / ((exp_R . d) + (exp_R . (- d))) ) & ( for d being real number holds f2 . d = ((exp_R . d) - (exp_R . (- d))) / ((exp_R . d) + (exp_R . (- d))) ) implies f1 = f2 )
assume A2: for d being real number holds f1 . d = ((exp_R . d) - (exp_R . (- d))) / ((exp_R . d) + (exp_R . (- d))) ; ::_thesis: ( ex d being real number st not f2 . d = ((exp_R . d) - (exp_R . (- d))) / ((exp_R . d) + (exp_R . (- d))) or f1 = f2 )
assume A3: for d being real number holds f2 . d = ((exp_R . d) - (exp_R . (- d))) / ((exp_R . d) + (exp_R . (- d))) ; ::_thesis: f1 = f2
 for d being Element of REAL holds f1 . d = f2 . d
proof
let d be Element of REAL ; ::_thesis: f1 . d = f2 . d
thus f1 . d = ((exp_R . d) - (exp_R . (- d))) / ((exp_R . d) + (exp_R . (- d))) by A2
.= f2 . d by A3 ; ::_thesis: verum
end;
hence  f1 = f2 by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines tanh SIN_COS2:def_5_:_
 for b1 being Function of REAL,REAL holds
( b1 = tanh iff for d being real number holds b1 . d = ((exp_R . d) - (exp_R . (- d))) / ((exp_R . d) + (exp_R . (- d))) );

definition
let d be number ;
func tanh d ->  set  equals :: SIN_COS2:def 6
tanh . d;
coherence
 tanh . d is set ;
end;

:: deftheorem  defines tanh SIN_COS2:def_6_:_
 for d being number holds tanh d = tanh . d;

registration
let d be number ;
cluster tanh d ->  real ;
coherence
 tanh d is real ;
end;

definition
let d be number ;
:: original: tanh
redefine func tanh d ->  Real;
coherence
 tanh d is Real ;
end;

theorem Th12: :: SIN_COS2:12
for p, q being real number holds exp_R . (p + q) = (exp_R . p) * (exp_R . q)
proof
let p, q be real number ; ::_thesis: exp_R . (p + q) = (exp_R . p) * (exp_R . q)
exp_R . (p + q) = exp_R (p + q) by SIN_COS:def_23
.= (exp_R p) * (exp_R q) by SIN_COS:50
.= (exp_R . p) * (exp_R q) by SIN_COS:def_23
.= (exp_R . p) * (exp_R . q) by SIN_COS:def_23 ;
hence  exp_R . (p + q) = (exp_R . p) * (exp_R . q) ; ::_thesis: verum
end;

theorem Th13: :: SIN_COS2:13
exp_R . 0 = 1 by SIN_COS:51, SIN_COS:def_23;

theorem Th14: :: SIN_COS2:14
for p being real number holds
( ((cosh . p) ^2) - ((sinh . p) ^2) = 1 & ((cosh . p) * (cosh . p)) - ((sinh . p) * (sinh . p)) = 1 )
proof
let p be real number ; ::_thesis: ( ((cosh . p) ^2) - ((sinh . p) ^2) = 1 & ((cosh . p) * (cosh . p)) - ((sinh . p) * (sinh . p)) = 1 )
A1: (sinh . p) * (sinh . p) = (((exp_R . p) - (exp_R . (- p))) / 2) * (sinh . p) by Def1
.= (((exp_R . p) - (exp_R . (- p))) / 2) * (((exp_R . p) - (exp_R . (- p))) / 2) by Def1
.= (((((exp_R . p) * (exp_R . p)) - ((exp_R . p) * (exp_R . (- p)))) - ((exp_R . (- p)) * (exp_R . p))) + ((exp_R . (- p)) * (exp_R . (- p)))) / (2 * 2)
.= ((((exp_R . (p + p)) - ((exp_R . p) * (exp_R . (- p)))) - ((exp_R . (- p)) * (exp_R . p))) + ((exp_R . (- p)) * (exp_R . (- p)))) / 4 by Th12
.= ((((exp_R . (p + p)) - (exp_R . (p + (- p)))) - ((exp_R . (- p)) * (exp_R . p))) + ((exp_R . (- p)) * (exp_R . (- p)))) / 4 by Th12
.= ((((exp_R . (p + p)) - (exp_R . (p + (- p)))) - ((exp_R . (- p)) * (exp_R . p))) + (exp_R . ((- p) + (- p)))) / 4 by Th12
.= ((((exp_R . (p + p)) - 1) - 1) + (exp_R . ((- p) + (- p)))) / 4 by Th12, Th13 ;
(cosh . p) * (cosh . p) = (((exp_R . p) + (exp_R . (- p))) / 2) * (cosh . p) by Def3
.= (((exp_R . p) + (exp_R . (- p))) / 2) * (((exp_R . p) + (exp_R . (- p))) / 2) by Def3
.= (((((exp_R . p) * (exp_R . p)) + ((exp_R . p) * (exp_R . (- p)))) + ((exp_R . (- p)) * (exp_R . p))) + ((exp_R . (- p)) * (exp_R . (- p)))) / (2 * 2)
.= ((((exp_R . (p + p)) + ((exp_R . p) * (exp_R . (- p)))) + ((exp_R . (- p)) * (exp_R . p))) + ((exp_R . (- p)) * (exp_R . (- p)))) / 4 by Th12
.= ((((exp_R . (p + p)) + (exp_R . (p + (- p)))) + ((exp_R . (- p)) * (exp_R . p))) + ((exp_R . (- p)) * (exp_R . (- p)))) / 4 by Th12
.= ((((exp_R . (p + p)) + (exp_R . (p + (- p)))) + ((exp_R . (- p)) * (exp_R . p))) + (exp_R . ((- p) + (- p)))) / 4 by Th12
.= ((((exp_R . (p + p)) + 1) + 1) + (exp_R . ((- p) + (- p)))) / 4 by Th12, Th13
.= (((exp_R . (p + p)) + 2) + (exp_R . ((- p) + (- p)))) / 4 ;
hence  ( ((cosh . p) ^2) - ((sinh . p) ^2) = 1 & ((cosh . p) * (cosh . p)) - ((sinh . p) * (sinh . p)) = 1 ) by A1; ::_thesis: verum
end;

Lm2:  for p, r being real number holds cosh . (p + r) = ((cosh . p) * (cosh . r)) + ((sinh . p) * (sinh . r))
proof
let p, r be real number ; ::_thesis: cosh . (p + r) = ((cosh . p) * (cosh . r)) + ((sinh . p) * (sinh . r))
((cosh . p) * (cosh . r)) + ((sinh . p) * (sinh . r)) = ((((exp_R . p) + (exp_R . (- p))) / 2) * (cosh . r)) + ((sinh . p) * (sinh . r)) by Def3
.= ((((exp_R . p) + (exp_R . (- p))) / 2) * (((exp_R . r) + (exp_R . (- r))) / 2)) + ((sinh . p) * (sinh . r)) by Def3
.= ((((exp_R . p) + (exp_R . (- p))) / 2) * (((exp_R . r) + (exp_R . (- r))) / 2)) + ((((exp_R . p) - (exp_R . (- p))) / 2) * (sinh . r)) by Def1
.= ((((exp_R . p) + (exp_R . (- p))) / 2) * (((exp_R . r) + (exp_R . (- r))) / 2)) + ((((exp_R . p) - (exp_R . (- p))) / 2) * (((exp_R . r) - (exp_R . (- r))) / 2)) by Def1
.= ((2 * ((exp_R . p) * (exp_R . r))) + (2 * ((exp_R . (- p)) * (exp_R . (- r))))) / 4
.= ((2 * (exp_R . (p + r))) + (2 * ((exp_R . (- p)) * (exp_R . (- r))))) / 4 by Th12
.= ((2 * (exp_R . (p + r))) + (2 * (exp_R . ((- p) + (- r))))) / 4 by Th12
.= ((exp_R . (p + r)) + (exp_R . (- (p + r)))) / 2
.= cosh . (p + r) by Def3 ;
hence  cosh . (p + r) = ((cosh . p) * (cosh . r)) + ((sinh . p) * (sinh . r)) ; ::_thesis: verum
end;

Lm3:  for p, r being real number holds sinh . (p + r) = ((sinh . p) * (cosh . r)) + ((cosh . p) * (sinh . r))
proof
let p, r be real number ; ::_thesis: sinh . (p + r) = ((sinh . p) * (cosh . r)) + ((cosh . p) * (sinh . r))
((sinh . p) * (cosh . r)) + ((cosh . p) * (sinh . r)) = ((((exp_R . p) - (exp_R . (- p))) / 2) * (cosh . r)) + ((cosh . p) * (sinh . r)) by Def1
.= ((((exp_R . p) - (exp_R . (- p))) / 2) * (((exp_R . r) + (exp_R . (- r))) / 2)) + ((cosh . p) * (sinh . r)) by Def3
.= ((((exp_R . p) - (exp_R . (- p))) / 2) * (((exp_R . r) + (exp_R . (- r))) / 2)) + ((((exp_R . p) + (exp_R . (- p))) / 2) * (sinh . r)) by Def3
.= ((((exp_R . p) - (exp_R . (- p))) / 2) * (((exp_R . r) + (exp_R . (- r))) / 2)) + ((((exp_R . p) + (exp_R . (- p))) / 2) * (((exp_R . r) - (exp_R . (- r))) / 2)) by Def1
.= ((2 * ((exp_R . p) * (exp_R . r))) + (2 * (- ((exp_R . (- p)) * (exp_R . (- r)))))) / 4
.= ((2 * (exp_R . (p + r))) + (2 * (- ((exp_R . (- p)) * (exp_R . (- r)))))) / 4 by Th12
.= ((2 * (exp_R . (p + r))) + (2 * (- (exp_R . ((- p) + (- r)))))) / 4 by Th12
.= ((exp_R . (p + r)) - (exp_R . (- (p + r)))) / 2
.= sinh . (p + r) by Def1 ;
hence  sinh . (p + r) = ((sinh . p) * (cosh . r)) + ((cosh . p) * (sinh . r)) ; ::_thesis: verum
end;

theorem Th15: :: SIN_COS2:15
for p being real number holds
( cosh . p <> 0 & cosh . p > 0 & cosh . 0 = 1 )
proof
let p be real number ; ::_thesis: ( cosh . p <> 0 & cosh . p > 0 & cosh . 0 = 1 )
 ( exp_R . p > 0 & exp_R . (- p) > 0 ) by SIN_COS:54;
then A1: ((exp_R . p) + (exp_R . (- p))) / 2 > 0 by XREAL_1:139;
cosh . 0 = ((exp_R . 0) + (exp_R . (- 0))) / 2 by Def3
.= 1 by SIN_COS:51, SIN_COS:def_23 ;
hence  ( cosh . p <> 0 & cosh . p > 0 & cosh . 0 = 1 ) by A1, Def3; ::_thesis: verum
end;

theorem Th16: :: SIN_COS2:16
sinh . 0 = 0
proof
sinh . 0 = ((exp_R . 0) - (exp_R . (- 0))) / 2 by Def1
.= 0 ;
hence  sinh . 0 = 0 ; ::_thesis: verum
end;

theorem Th17: :: SIN_COS2:17
for p being real number holds tanh . p = (sinh . p) / (cosh . p)
proof
let p be real number ; ::_thesis: tanh . p = (sinh . p) / (cosh . p)
(sinh . p) / (cosh . p) = (((exp_R . p) - (exp_R . (- p))) / 2) / (cosh . p) by Def1
.= (((exp_R . p) - (exp_R . (- p))) / 2) / (((exp_R . p) + (exp_R . (- p))) / 2) by Def3
.= ((exp_R . p) - (exp_R . (- p))) / ((exp_R . p) + (exp_R . (- p))) by XCMPLX_1:55
.= tanh . p by Def5 ;
hence  tanh . p = (sinh . p) / (cosh . p) ; ::_thesis: verum
end;

Lm4:  for r, q, p, a1 being real number st r <> 0 & q <> 0 holds
((p * q) + (r * a1)) / ((r * q) + (p * a1)) = ((p / r) + (a1 / q)) / (1 + ((p / r) * (a1 / q)))
proof
let r, q, p, a1 be real number ; ::_thesis: ( r <> 0 & q <> 0 implies ((p * q) + (r * a1)) / ((r * q) + (p * a1)) = ((p / r) + (a1 / q)) / (1 + ((p / r) * (a1 / q))) )
assume that
A1: r <> 0 and
A2: q <> 0 ; ::_thesis: ((p * q) + (r * a1)) / ((r * q) + (p * a1)) = ((p / r) + (a1 / q)) / (1 + ((p / r) * (a1 / q)))
((p * q) + (r * a1)) / ((r * q) + (p * a1)) = (((p * q) + (r * a1)) / (r * q)) / (((r * q) + (p * a1)) / (r * q)) by A1, A2, XCMPLX_1:6, XCMPLX_1:55
.= (((p * q) / (r * q)) + ((r * a1) / (r * q))) / (((r * q) + (p * a1)) / (r * q)) by XCMPLX_1:62
.= (((p * q) / (r * q)) + ((r * a1) / (r * q))) / (((r * q) / (r * q)) + ((p * a1) / (r * q))) by XCMPLX_1:62
.= ((p / r) + ((a1 * r) / (q * r))) / (((r * q) / (r * q)) + ((p * a1) / (r * q))) by A2, XCMPLX_1:91
.= ((p / r) + (a1 / q)) / (((r * q) / (r * q)) + ((p * a1) / (r * q))) by A1, XCMPLX_1:91
.= ((p / r) + (a1 / q)) / (1 + ((p * a1) / (r * q))) by A1, A2, XCMPLX_1:6, XCMPLX_1:60
.= ((p / r) + (a1 / q)) / (1 + ((p / r) * (a1 / q))) by XCMPLX_1:76 ;
hence  ((p * q) + (r * a1)) / ((r * q) + (p * a1)) = ((p / r) + (a1 / q)) / (1 + ((p / r) * (a1 / q))) ; ::_thesis: verum
end;

Lm5:  for p, r being real number holds tanh . (p + r) = ((tanh . p) + (tanh . r)) / (1 + ((tanh . p) * (tanh . r)))
proof
let p, r be real number ; ::_thesis: tanh . (p + r) = ((tanh . p) + (tanh . r)) / (1 + ((tanh . p) * (tanh . r)))
A1: ( cosh . r <> 0 & cosh . p <> 0 ) by Th15;
tanh . (p + r) = (sinh . (p + r)) / (cosh . (p + r)) by Th17
.= (((sinh . p) * (cosh . r)) + ((cosh . p) * (sinh . r))) / (cosh . (p + r)) by Lm3
.= (((sinh . p) * (cosh . r)) + ((cosh . p) * (sinh . r))) / (((cosh . p) * (cosh . r)) + ((sinh . p) * (sinh . r))) by Lm2
.= (((sinh . p) / (cosh . p)) + ((sinh . r) / (cosh . r))) / (1 + (((sinh . p) / (cosh . p)) * ((sinh . r) / (cosh . r)))) by A1, Lm4
.= ((tanh . p) + ((sinh . r) / (cosh . r))) / (1 + (((sinh . p) / (cosh . p)) * ((sinh . r) / (cosh . r)))) by Th17
.= ((tanh . p) + (tanh . r)) / (1 + (((sinh . p) / (cosh . p)) * ((sinh . r) / (cosh . r)))) by Th17
.= ((tanh . p) + (tanh . r)) / (1 + ((tanh . p) * ((sinh . r) / (cosh . r)))) by Th17
.= ((tanh . p) + (tanh . r)) / (1 + ((tanh . p) * (tanh . r))) by Th17 ;
hence  tanh . (p + r) = ((tanh . p) + (tanh . r)) / (1 + ((tanh . p) * (tanh . r))) ; ::_thesis: verum
end;

theorem Th18: :: SIN_COS2:18
for p being real number holds
( (sinh . p) ^2 = (1 / 2) * ((cosh . (2 * p)) - 1) & (cosh . p) ^2 = (1 / 2) * ((cosh . (2 * p)) + 1) )
proof
let p be real number ; ::_thesis: ( (sinh . p) ^2 = (1 / 2) * ((cosh . (2 * p)) - 1) & (cosh . p) ^2 = (1 / 2) * ((cosh . (2 * p)) + 1) )
A1: (cosh . p) ^2 = (((exp_R . p) + (exp_R . (- p))) / 2) * (cosh . p) by Def3
.= (((exp_R . p) + (exp_R . (- p))) / 2) * (((exp_R . p) + (exp_R . (- p))) / 2) by Def3
.= (((((exp_R . p) * (exp_R . p)) + ((exp_R . p) * (exp_R . (- p)))) + ((exp_R . (- p)) * (exp_R . p))) + ((exp_R . (- p)) * (exp_R . (- p)))) / 4
.= ((((exp_R . (p + p)) + ((exp_R . p) * (exp_R . (- p)))) + ((exp_R . p) * (exp_R . (- p)))) + ((exp_R . (- p)) * (exp_R . (- p)))) / 4 by Th12
.= ((((exp_R . (p + p)) + ((exp_R . p) * (exp_R . (- p)))) + ((exp_R . p) * (exp_R . (- p)))) + (exp_R . ((- p) + (- p)))) / 4 by Th12
.= ((((exp_R . (p + p)) + (exp_R . (p + (- p)))) + ((exp_R . p) * (exp_R . (- p)))) + (exp_R . ((- p) + (- p)))) / 4 by Th12
.= ((((exp_R . (p + p)) + (exp_R . (p + (- p)))) + (exp_R . (p + (- p)))) + (exp_R . ((- p) + (- p)))) / 4 by Th12
.= (((exp_R . (2 * p)) + (2 * (exp_R . 0))) + (exp_R . ((- p) + (- p)))) / 4
.= (((exp_R . (2 * p)) + (2 * 1)) + (exp_R . (- (2 * p)))) / 4 by SIN_COS:51, SIN_COS:def_23
.= ((1 / 2) * (((exp_R . (2 * p)) + (exp_R . (- (2 * p)))) / 2)) + ((1 * 2) / (2 * 2))
.= ((1 / 2) * (cosh . (2 * p))) + ((1 / 2) * ((2 * 1) / 2)) by Def3
.= (1 / 2) * ((cosh . (2 * p)) + 1) ;
(sinh . p) ^2 = (((exp_R . p) - (exp_R . (- p))) / 2) * (sinh . p) by Def1
.= (((exp_R . p) - (exp_R . (- p))) / 2) * (((exp_R . p) - (exp_R . (- p))) / 2) by Def1
.= (((((exp_R . p) * (exp_R . p)) - ((exp_R . p) * (exp_R . (- p)))) - ((exp_R . (- p)) * (exp_R . p))) + ((exp_R . (- p)) * (exp_R . (- p)))) / 4
.= ((((exp_R . (p + p)) - ((exp_R . p) * (exp_R . (- p)))) - ((exp_R . p) * (exp_R . (- p)))) + ((exp_R . (- p)) * (exp_R . (- p)))) / 4 by Th12
.= ((((exp_R . (p + p)) - ((exp_R . p) * (exp_R . (- p)))) - ((exp_R . p) * (exp_R . (- p)))) + (exp_R . ((- p) + (- p)))) / 4 by Th12
.= ((((exp_R . (p + p)) - (exp_R . (p + (- p)))) - ((exp_R . p) * (exp_R . (- p)))) + (exp_R . ((- p) + (- p)))) / 4 by Th12
.= ((((exp_R . (p + p)) + (- (exp_R . (p + (- p))))) - (exp_R . (p + (- p)))) + (exp_R . ((- p) + (- p)))) / 4 by Th12
.= (((exp_R . (2 * p)) + (2 * (- (exp_R . 0)))) + (exp_R . ((- p) + (- p)))) / 4
.= (((exp_R . (2 * p)) + (2 * (- 1))) + (exp_R . (- (2 * p)))) / 4 by SIN_COS:51, SIN_COS:def_23
.= ((1 / 2) * (((exp_R . (2 * p)) + (exp_R . (- (2 * p)))) / 2)) + (((- 1) * 2) / (2 * 2))
.= ((1 / 2) * (cosh . (2 * p))) + ((1 / 2) * ((2 * (- 1)) / 2)) by Def3
.= (1 / 2) * ((cosh . (2 * p)) - 1) ;
hence  ( (sinh . p) ^2 = (1 / 2) * ((cosh . (2 * p)) - 1) & (cosh . p) ^2 = (1 / 2) * ((cosh . (2 * p)) + 1) ) by A1; ::_thesis: verum
end;

Lm6:  for p being real number holds
( sinh . (2 * p) = (2 * (sinh . p)) * (cosh . p) & cosh . (2 * p) = (2 * ((cosh . p) ^2)) - 1 )
proof
let p be real number ; ::_thesis: ( sinh . (2 * p) = (2 * (sinh . p)) * (cosh . p) & cosh . (2 * p) = (2 * ((cosh . p) ^2)) - 1 )
A1: 2 * ((cosh . p) ^2) = 2 * ((1 / 2) * ((cosh . (2 * p)) + 1)) by Th18
.= (cosh . (2 * p)) + 1 ;
(2 * (sinh . p)) * (cosh . p) = (2 * (((exp_R . p) - (exp_R . (- p))) / 2)) * (cosh . p) by Def1
.= (2 * (((exp_R . p) - (exp_R . (- p))) / 2)) * (((exp_R . p) + (exp_R . (- p))) / 2) by Def3
.= (2 / 4) * (((exp_R . p) ^2) - ((exp_R . (- p)) ^2))
.= (2 / 4) * ((exp_R . (p + p)) - ((exp_R . (- p)) * (exp_R . (- p)))) by Th12
.= (2 / 4) * ((exp_R . (2 * p)) - (exp_R . ((- p) + (- p)))) by Th12
.= (((exp_R . (2 * p)) - (exp_R . (- (2 * p)))) / 2) * 1
.= sinh . (2 * p) by Def1 ;
hence  ( sinh . (2 * p) = (2 * (sinh . p)) * (cosh . p) & cosh . (2 * p) = (2 * ((cosh . p) ^2)) - 1 ) by A1; ::_thesis: verum
end;

theorem Th19: :: SIN_COS2:19
for p being real number holds
( cosh . (- p) = cosh . p & sinh . (- p) = - (sinh . p) & tanh . (- p) = - (tanh . p) )
proof
let p be real number ; ::_thesis: ( cosh . (- p) = cosh . p & sinh . (- p) = - (sinh . p) & tanh . (- p) = - (tanh . p) )
A1: cosh . (- p) = ((exp_R . (- p)) + (exp_R . (- (- p)))) / 2 by Def3
.= cosh . p by Def3 ;
A2: sinh . (- p) = ((exp_R . (- p)) - (exp_R . (- (- p)))) / 2 by Def1
.= - (((exp_R . p) - (exp_R . (- p))) / 2)
.= - (sinh . p) by Def1 ;
then tanh . (- p) = (- (sinh . p)) / (cosh . (- p)) by Th17
.= - ((sinh . p) / (cosh . p)) by A1, XCMPLX_1:187
.= - (tanh . p) by Th17 ;
hence  ( cosh . (- p) = cosh . p & sinh . (- p) = - (sinh . p) & tanh . (- p) = - (tanh . p) ) by A1, A2; ::_thesis: verum
end;

Lm7:  for p, r being real number holds cosh . (p - r) = ((cosh . p) * (cosh . r)) - ((sinh . p) * (sinh . r))
proof
let p, r be real number ; ::_thesis: cosh . (p - r) = ((cosh . p) * (cosh . r)) - ((sinh . p) * (sinh . r))
cosh . (p - r) = cosh . (p + (- r))
.= ((cosh . p) * (cosh . (- r))) + ((sinh . p) * (sinh . (- r))) by Lm2
.= ((cosh . p) * (cosh . r)) + ((sinh . p) * (sinh . (- r))) by Th19
.= ((cosh . p) * (cosh . r)) + ((sinh . p) * (- (sinh . r))) by Th19
.= ((cosh . p) * (cosh . r)) - ((sinh . p) * (sinh . r)) ;
hence  cosh . (p - r) = ((cosh . p) * (cosh . r)) - ((sinh . p) * (sinh . r)) ; ::_thesis: verum
end;

theorem :: SIN_COS2:20
for p, r being real number holds
( cosh . (p + r) = ((cosh . p) * (cosh . r)) + ((sinh . p) * (sinh . r)) & cosh . (p - r) = ((cosh . p) * (cosh . r)) - ((sinh . p) * (sinh . r)) ) by Lm2, Lm7;

Lm8:  for p, r being real number holds sinh . (p - r) = ((sinh . p) * (cosh . r)) - ((cosh . p) * (sinh . r))
proof
let p, r be real number ; ::_thesis: sinh . (p - r) = ((sinh . p) * (cosh . r)) - ((cosh . p) * (sinh . r))
sinh . (p - r) = sinh . (p + (- r))
.= ((sinh . p) * (cosh . (- r))) + ((cosh . p) * (sinh . (- r))) by Lm3
.= ((sinh . p) * (cosh . r)) + ((cosh . p) * (sinh . (- r))) by Th19
.= ((sinh . p) * (cosh . r)) + ((cosh . p) * (- (sinh . r))) by Th19
.= ((sinh . p) * (cosh . r)) - ((cosh . p) * (sinh . r)) ;
hence  sinh . (p - r) = ((sinh . p) * (cosh . r)) - ((cosh . p) * (sinh . r)) ; ::_thesis: verum
end;

theorem :: SIN_COS2:21
for p, r being real number holds
( sinh . (p + r) = ((sinh . p) * (cosh . r)) + ((cosh . p) * (sinh . r)) & sinh . (p - r) = ((sinh . p) * (cosh . r)) - ((cosh . p) * (sinh . r)) ) by Lm3, Lm8;

Lm9:  for p, r being real number holds tanh . (p - r) = ((tanh . p) - (tanh . r)) / (1 - ((tanh . p) * (tanh . r)))
proof
let p, r be real number ; ::_thesis: tanh . (p - r) = ((tanh . p) - (tanh . r)) / (1 - ((tanh . p) * (tanh . r)))
tanh . (p - r) = tanh . (p + (- r))
.= ((tanh . p) + (tanh . (- r))) / (1 + ((tanh . p) * (tanh . (- r)))) by Lm5
.= ((tanh . p) + (- (tanh . r))) / (1 + ((tanh . p) * (tanh . (- r)))) by Th19
.= ((tanh . p) - (tanh . r)) / (1 + ((tanh . p) * (- (tanh . r)))) by Th19
.= ((tanh . p) - (tanh . r)) / (1 - ((tanh . p) * (tanh . r))) ;
hence  tanh . (p - r) = ((tanh . p) - (tanh . r)) / (1 - ((tanh . p) * (tanh . r))) ; ::_thesis: verum
end;

theorem :: SIN_COS2:22
for p, r being real number holds
( tanh . (p + r) = ((tanh . p) + (tanh . r)) / (1 + ((tanh . p) * (tanh . r))) & tanh . (p - r) = ((tanh . p) - (tanh . r)) / (1 - ((tanh . p) * (tanh . r))) ) by Lm5, Lm9;

theorem :: SIN_COS2:23
for p being real number holds
( sinh . (2 * p) = (2 * (sinh . p)) * (cosh . p) & cosh . (2 * p) = (2 * ((cosh . p) ^2)) - 1 & tanh . (2 * p) = (2 * (tanh . p)) / (1 + ((tanh . p) ^2)) )
proof
let p be real number ; ::_thesis: ( sinh . (2 * p) = (2 * (sinh . p)) * (cosh . p) & cosh . (2 * p) = (2 * ((cosh . p) ^2)) - 1 & tanh . (2 * p) = (2 * (tanh . p)) / (1 + ((tanh . p) ^2)) )
tanh . (2 * p) = tanh . (p + p)
.= ((tanh . p) + (tanh . p)) / (1 + ((tanh . p) * (tanh . p))) by Lm5
.= (2 * (tanh . p)) / (1 + ((tanh . p) ^2)) ;
hence  ( sinh . (2 * p) = (2 * (sinh . p)) * (cosh . p) & cosh . (2 * p) = (2 * ((cosh . p) ^2)) - 1 & tanh . (2 * p) = (2 * (tanh . p)) / (1 + ((tanh . p) ^2)) ) by Lm6; ::_thesis: verum
end;

theorem Th24: :: SIN_COS2:24
for p, q being real number holds
( ((sinh . p) ^2) - ((sinh . q) ^2) = (sinh . (p + q)) * (sinh . (p - q)) & (sinh . (p + q)) * (sinh . (p - q)) = ((cosh . p) ^2) - ((cosh . q) ^2) & ((sinh . p) ^2) - ((sinh . q) ^2) = ((cosh . p) ^2) - ((cosh . q) ^2) )
proof
let p, q be real number ; ::_thesis: ( ((sinh . p) ^2) - ((sinh . q) ^2) = (sinh . (p + q)) * (sinh . (p - q)) & (sinh . (p + q)) * (sinh . (p - q)) = ((cosh . p) ^2) - ((cosh . q) ^2) & ((sinh . p) ^2) - ((sinh . q) ^2) = ((cosh . p) ^2) - ((cosh . q) ^2) )
A1: (sinh . (p + q)) * (sinh . (p - q)) = (((sinh . p) * (cosh . q)) + ((cosh . p) * (sinh . q))) * (sinh . (p + (- q))) by Lm3
.= (((sinh . p) * (cosh . q)) + ((cosh . p) * (sinh . q))) * (((sinh . p) * (cosh . (- q))) + ((cosh . p) * (sinh . (- q)))) by Lm3
.= (((sinh . p) * (cosh . q)) + ((cosh . p) * (sinh . q))) * (((sinh . p) * (cosh . q)) + ((cosh . p) * (sinh . (- q)))) by Th19
.= (((sinh . p) * (cosh . q)) + ((cosh . p) * (sinh . q))) * (((sinh . p) * (cosh . q)) + ((cosh . p) * (- (sinh . q)))) by Th19
.= (((sinh . p) ^2) * ((cosh . q) ^2)) - (((sinh . q) ^2) * ((cosh . p) ^2)) ;
then A2: (sinh . (p + q)) * (sinh . (p - q)) = (((cosh . q) ^2) * (- (((cosh . p) ^2) - ((sinh . p) ^2)))) + ((((cosh . p) ^2) * ((cosh . q) ^2)) + (- (((sinh . q) ^2) * ((cosh . p) ^2))))
.= (((cosh . q) ^2) * (- 1)) + (((cosh . p) ^2) * (((cosh . q) ^2) - ((sinh . q) ^2))) by Th14
.= (((cosh . q) ^2) * (- 1)) + (((cosh . p) ^2) * 1) by Th14
.= ((cosh . p) ^2) - ((cosh . q) ^2) ;
(sinh . (p + q)) * (sinh . (p - q)) = ((((sinh . p) ^2) * (((cosh . q) ^2) - ((sinh . q) ^2))) + (((sinh . q) ^2) * ((sinh . p) ^2))) - (((sinh . q) ^2) * ((cosh . p) ^2)) by A1
.= ((((sinh . p) ^2) * 1) + (((sinh . p) ^2) * ((sinh . q) ^2))) - (((sinh . q) ^2) * ((cosh . p) ^2)) by Th14
.= ((sinh . p) ^2) + (((sinh . q) ^2) * (- (((cosh . p) ^2) - ((sinh . p) ^2))))
.= ((sinh . p) ^2) + (((sinh . q) ^2) * (- 1)) by Th14
.= ((sinh . p) ^2) - ((sinh . q) ^2) ;
hence  ( ((sinh . p) ^2) - ((sinh . q) ^2) = (sinh . (p + q)) * (sinh . (p - q)) & (sinh . (p + q)) * (sinh . (p - q)) = ((cosh . p) ^2) - ((cosh . q) ^2) & ((sinh . p) ^2) - ((sinh . q) ^2) = ((cosh . p) ^2) - ((cosh . q) ^2) ) by A2; ::_thesis: verum
end;

theorem Th25: :: SIN_COS2:25
for p, q being real number holds
( ((sinh . p) ^2) + ((cosh . q) ^2) = (cosh . (p + q)) * (cosh . (p - q)) & (cosh . (p + q)) * (cosh . (p - q)) = ((cosh . p) ^2) + ((sinh . q) ^2) & ((sinh . p) ^2) + ((cosh . q) ^2) = ((cosh . p) ^2) + ((sinh . q) ^2) )
proof
let p, q be real number ; ::_thesis: ( ((sinh . p) ^2) + ((cosh . q) ^2) = (cosh . (p + q)) * (cosh . (p - q)) & (cosh . (p + q)) * (cosh . (p - q)) = ((cosh . p) ^2) + ((sinh . q) ^2) & ((sinh . p) ^2) + ((cosh . q) ^2) = ((cosh . p) ^2) + ((sinh . q) ^2) )
A1: (cosh . (p + q)) * (cosh . (p - q)) = (((cosh . p) * (cosh . q)) + ((sinh . p) * (sinh . q))) * (cosh . (p + (- q))) by Lm2
.= (((cosh . p) * (cosh . q)) + ((sinh . p) * (sinh . q))) * (((cosh . p) * (cosh . (- q))) + ((sinh . p) * (sinh . (- q)))) by Lm2
.= (((((cosh . p) * (cosh . q)) * ((cosh . p) * (cosh . (- q)))) + (((cosh . p) * (cosh . q)) * ((sinh . p) * (sinh . (- q))))) + (((sinh . p) * (sinh . q)) * ((cosh . p) * (cosh . (- q))))) + (((sinh . p) * (sinh . q)) * ((sinh . p) * (sinh . (- q))))
.= (((((cosh . p) * (cosh . q)) * ((cosh . p) * (cosh . q))) + (((cosh . p) * (cosh . q)) * ((sinh . (- q)) * (sinh . p)))) + (((sinh . p) * (sinh . q)) * ((cosh . p) * (cosh . (- q))))) + (((sinh . p) * (sinh . q)) * ((sinh . (- q)) * (sinh . p))) by Th19
.= (((((cosh . p) * (cosh . q)) ^2) + (((sinh . (- q)) * (sinh . p)) * ((cosh . p) * (cosh . q)))) + (((sinh . p) * (sinh . q)) * ((cosh . p) * (cosh . q)))) + (((sinh . (- q)) * (sinh . p)) * ((sinh . p) * (sinh . q))) by Th19
.= (((((cosh . p) * (cosh . q)) ^2) + (((- (sinh . q)) * (sinh . p)) * ((cosh . p) * (cosh . q)))) + (((sinh . p) * (sinh . q)) * ((cosh . p) * (cosh . q)))) + (((sinh . (- q)) * (sinh . p)) * ((sinh . p) * (sinh . q))) by Th19
.= ((((cosh . p) * (cosh . q)) ^2) + 0) + ((((- 1) * (sinh . q)) * (sinh . p)) * ((sinh . p) * (sinh . q))) by Th19
.= (((cosh . p) ^2) * ((cosh . q) ^2)) - (((sinh . q) ^2) * ((sinh . p) ^2)) ;
then A2: (cosh . (p + q)) * (cosh . (p - q)) = ((((cosh . p) ^2) * (((cosh . q) ^2) - ((sinh . q) ^2))) + (((cosh . p) ^2) * ((sinh . q) ^2))) + (- (((sinh . q) ^2) * ((sinh . p) ^2)))
.= ((((cosh . p) ^2) * 1) + (((cosh . p) ^2) * ((sinh . q) ^2))) + (- (((sinh . q) ^2) * ((sinh . p) ^2))) by Th14
.= ((cosh . p) ^2) + (((sinh . q) ^2) * (((cosh . p) ^2) - ((sinh . p) ^2)))
.= ((cosh . p) ^2) + (((sinh . q) ^2) * 1) by Th14
.= ((cosh . p) ^2) + ((sinh . q) ^2) ;
(cosh . (p + q)) * (cosh . (p - q)) = (((cosh . q) ^2) * (((cosh . p) ^2) - ((sinh . p) ^2))) + ((((cosh . q) ^2) * ((sinh . p) ^2)) + (- (((sinh . p) ^2) * ((sinh . q) ^2)))) by A1
.= (((cosh . q) ^2) * 1) + ((((cosh . q) ^2) * ((sinh . p) ^2)) - (((sinh . p) ^2) * ((sinh . q) ^2))) by Th14
.= ((cosh . q) ^2) + (((sinh . p) ^2) * (((cosh . q) ^2) - ((sinh . q) ^2)))
.= ((cosh . q) ^2) + (((sinh . p) ^2) * 1) by Th14
.= ((cosh . q) ^2) + ((sinh . p) ^2) ;
hence  ( ((sinh . p) ^2) + ((cosh . q) ^2) = (cosh . (p + q)) * (cosh . (p - q)) & (cosh . (p + q)) * (cosh . (p - q)) = ((cosh . p) ^2) + ((sinh . q) ^2) & ((sinh . p) ^2) + ((cosh . q) ^2) = ((cosh . p) ^2) + ((sinh . q) ^2) ) by A2; ::_thesis: verum
end;

theorem :: SIN_COS2:26
for p, r being real number holds
( (sinh . p) + (sinh . r) = (2 * (sinh . ((p / 2) + (r / 2)))) * (cosh . ((p / 2) - (r / 2))) & (sinh . p) - (sinh . r) = (2 * (sinh . ((p / 2) - (r / 2)))) * (cosh . ((p / 2) + (r / 2))) )
proof
let p, r be real number ; ::_thesis: ( (sinh . p) + (sinh . r) = (2 * (sinh . ((p / 2) + (r / 2)))) * (cosh . ((p / 2) - (r / 2))) & (sinh . p) - (sinh . r) = (2 * (sinh . ((p / 2) - (r / 2)))) * (cosh . ((p / 2) + (r / 2))) )
A1: (2 * (sinh . ((p / 2) - (r / 2)))) * (cosh . ((p / 2) + (r / 2))) = (2 * (((sinh . (p / 2)) * (cosh . (r / 2))) - ((cosh . (p / 2)) * (sinh . (r / 2))))) * (cosh . ((p / 2) + (r / 2))) by Lm8
.= (2 * (((sinh . (p / 2)) * (cosh . (r / 2))) - ((cosh . (p / 2)) * (sinh . (r / 2))))) * (((cosh . (p / 2)) * (cosh . (r / 2))) + ((sinh . (p / 2)) * (sinh . (r / 2)))) by Lm2
.= 2 * (((((cosh . (r / 2)) * (sinh . (r / 2))) * (- (((cosh . (p / 2)) ^2) - ((sinh . (p / 2)) ^2)))) + ((sinh . (p / 2)) * ((cosh . (p / 2)) * ((cosh . (r / 2)) ^2)))) - ((cosh . (p / 2)) * ((sinh . (p / 2)) * ((sinh . (r / 2)) ^2))))
.= 2 * (((((cosh . (r / 2)) * (sinh . (r / 2))) * (- 1)) + ((sinh . (p / 2)) * ((cosh . (p / 2)) * ((cosh . (r / 2)) ^2)))) - ((cosh . (p / 2)) * ((sinh . (p / 2)) * ((sinh . (r / 2)) ^2)))) by Th14
.= 2 * ((((sinh . (p / 2)) * (cosh . (p / 2))) * (((cosh . (r / 2)) ^2) - ((sinh . (r / 2)) ^2))) + ((- 1) * ((cosh . (r / 2)) * (sinh . (r / 2)))))
.= 2 * ((((sinh . (p / 2)) * (cosh . (p / 2))) * 1) + ((- 1) * ((cosh . (r / 2)) * (sinh . (r / 2))))) by Th14
.= ((2 * (sinh . (p / 2))) * (cosh . (p / 2))) - (2 * ((sinh . (r / 2)) * (cosh . (r / 2))))
.= (sinh . (2 * (p / 2))) - ((2 * (sinh . (r / 2))) * (cosh . (r / 2))) by Lm6
.= (sinh . p) - (sinh . (2 * (r / 2))) by Lm6
.= (sinh . p) - (sinh . r) ;
(2 * (sinh . ((p / 2) + (r / 2)))) * (cosh . ((p / 2) - (r / 2))) = (2 * (((sinh . (p / 2)) * (cosh . (r / 2))) + ((cosh . (p / 2)) * (sinh . (r / 2))))) * (cosh . ((p / 2) - (r / 2))) by Lm3
.= (2 * (((sinh . (p / 2)) * (cosh . (r / 2))) + ((cosh . (p / 2)) * (sinh . (r / 2))))) * (((cosh . (p / 2)) * (cosh . (r / 2))) - ((sinh . (p / 2)) * (sinh . (r / 2)))) by Lm7
.= 2 * (((((sinh . (r / 2)) * (cosh . (r / 2))) * (((cosh . (p / 2)) ^2) - ((sinh . (p / 2)) ^2))) + ((sinh . (p / 2)) * ((cosh . (p / 2)) * ((cosh . (r / 2)) ^2)))) - ((cosh . (p / 2)) * ((sinh . (p / 2)) * ((sinh . (r / 2)) ^2))))
.= 2 * (((((sinh . (r / 2)) * (cosh . (r / 2))) * 1) + ((sinh . (p / 2)) * ((cosh . (p / 2)) * ((cosh . (r / 2)) ^2)))) - ((cosh . (p / 2)) * ((sinh . (p / 2)) * ((sinh . (r / 2)) ^2)))) by Th14
.= 2 * ((((sinh . (p / 2)) * (cosh . (p / 2))) * (((cosh . (r / 2)) ^2) - ((sinh . (r / 2)) ^2))) + ((sinh . (r / 2)) * (cosh . (r / 2))))
.= 2 * ((((sinh . (p / 2)) * (cosh . (p / 2))) * 1) + ((sinh . (r / 2)) * (cosh . (r / 2)))) by Th14
.= ((2 * (sinh . (p / 2))) * (cosh . (p / 2))) + (2 * ((sinh . (r / 2)) * (cosh . (r / 2))))
.= (sinh . (2 * (p / 2))) + ((2 * (sinh . (r / 2))) * (cosh . (r / 2))) by Lm6
.= (sinh . p) + (sinh . (2 * (r / 2))) by Lm6
.= (sinh . p) + (sinh . r) ;
hence  ( (sinh . p) + (sinh . r) = (2 * (sinh . ((p / 2) + (r / 2)))) * (cosh . ((p / 2) - (r / 2))) & (sinh . p) - (sinh . r) = (2 * (sinh . ((p / 2) - (r / 2)))) * (cosh . ((p / 2) + (r / 2))) ) by A1; ::_thesis: verum
end;

theorem :: SIN_COS2:27
for p, r being real number holds
( (cosh . p) + (cosh . r) = (2 * (cosh . ((p / 2) + (r / 2)))) * (cosh . ((p / 2) - (r / 2))) & (cosh . p) - (cosh . r) = (2 * (sinh . ((p / 2) - (r / 2)))) * (sinh . ((p / 2) + (r / 2))) )
proof
let p, r be real number ; ::_thesis: ( (cosh . p) + (cosh . r) = (2 * (cosh . ((p / 2) + (r / 2)))) * (cosh . ((p / 2) - (r / 2))) & (cosh . p) - (cosh . r) = (2 * (sinh . ((p / 2) - (r / 2)))) * (sinh . ((p / 2) + (r / 2))) )
A1: (2 * (sinh . ((p / 2) - (r / 2)))) * (sinh . ((p / 2) + (r / 2))) = 2 * ((sinh . ((p / 2) - (r / 2))) * (sinh . ((p / 2) + (r / 2))))
.= 2 * (((cosh . (p / 2)) ^2) - ((cosh . (r / 2)) ^2)) by Th24
.= 2 * (((1 / 2) * ((cosh . (2 * (p / 2))) + 1)) - ((cosh . (r / 2)) ^2)) by Th18
.= 2 * (((1 / 2) * ((cosh . p) + 1)) - ((1 / 2) * ((cosh . (2 * (r / 2))) + 1))) by Th18
.= (cosh . p) - (cosh . r) ;
(2 * (cosh . ((p / 2) + (r / 2)))) * (cosh . ((p / 2) - (r / 2))) = 2 * ((cosh . ((p / 2) + (r / 2))) * (cosh . ((p / 2) - (r / 2))))
.= 2 * (((sinh . (p / 2)) ^2) + ((cosh . (r / 2)) ^2)) by Th25
.= 2 * (((1 / 2) * ((cosh . (2 * (p / 2))) - 1)) + ((cosh . (r / 2)) ^2)) by Th18
.= 2 * (((1 / 2) * ((cosh . p) - 1)) + ((1 / 2) * ((cosh . (2 * (r / 2))) + 1))) by Th18
.= (cosh . r) + (cosh . p) ;
hence  ( (cosh . p) + (cosh . r) = (2 * (cosh . ((p / 2) + (r / 2)))) * (cosh . ((p / 2) - (r / 2))) & (cosh . p) - (cosh . r) = (2 * (sinh . ((p / 2) - (r / 2)))) * (sinh . ((p / 2) + (r / 2))) ) by A1; ::_thesis: verum
end;

theorem :: SIN_COS2:28
for p, r being real number holds
( (tanh . p) + (tanh . r) = (sinh . (p + r)) / ((cosh . p) * (cosh . r)) & (tanh . p) - (tanh . r) = (sinh . (p - r)) / ((cosh . p) * (cosh . r)) )
proof
let p, r be real number ; ::_thesis: ( (tanh . p) + (tanh . r) = (sinh . (p + r)) / ((cosh . p) * (cosh . r)) & (tanh . p) - (tanh . r) = (sinh . (p - r)) / ((cosh . p) * (cosh . r)) )
A1: (sinh . (p - r)) / ((cosh . p) * (cosh . r)) = (((sinh . p) * (cosh . r)) - ((cosh . p) * (sinh . r))) / ((cosh . p) * (cosh . r)) by Lm8
.= (((sinh . p) * (cosh . r)) / ((cosh . p) * (cosh . r))) - (((cosh . p) * (sinh . r)) / ((cosh . p) * (cosh . r))) by XCMPLX_1:120
.= ((sinh . p) / (cosh . p)) - (((cosh . p) * (sinh . r)) / ((cosh . p) * (cosh . r))) by Th15, XCMPLX_1:91
.= ((sinh . p) / (cosh . p)) - ((sinh . r) / (cosh . r)) by Th15, XCMPLX_1:91
.= (tanh . p) - ((sinh . r) / (cosh . r)) by Th17
.= (tanh . p) - (tanh . r) by Th17 ;
(sinh . (p + r)) / ((cosh . p) * (cosh . r)) = (((sinh . p) * (cosh . r)) + ((cosh . p) * (sinh . r))) / ((cosh . p) * (cosh . r)) by Lm3
.= (((sinh . p) * (cosh . r)) / ((cosh . p) * (cosh . r))) + (((cosh . p) * (sinh . r)) / ((cosh . p) * (cosh . r))) by XCMPLX_1:62
.= ((sinh . p) / (cosh . p)) + (((cosh . p) * (sinh . r)) / ((cosh . p) * (cosh . r))) by Th15, XCMPLX_1:91
.= ((sinh . p) / (cosh . p)) + ((sinh . r) / (cosh . r)) by Th15, XCMPLX_1:91
.= (tanh . p) + ((sinh . r) / (cosh . r)) by Th17
.= (tanh . p) + (tanh . r) by Th17 ;
hence  ( (tanh . p) + (tanh . r) = (sinh . (p + r)) / ((cosh . p) * (cosh . r)) & (tanh . p) - (tanh . r) = (sinh . (p - r)) / ((cosh . p) * (cosh . r)) ) by A1; ::_thesis: verum
end;

theorem :: SIN_COS2:29
for p being real number
for n being Element of NAT holds ((cosh . p) + (sinh . p)) |^ n = (cosh . (n * p)) + (sinh . (n * p))
proof
let p be real number ; ::_thesis: for n being Element of NAT holds ((cosh . p) + (sinh . p)) |^ n = (cosh . (n * p)) + (sinh . (n * p))
let n be Element of NAT ; ::_thesis: ((cosh . p) + (sinh . p)) |^ n = (cosh . (n * p)) + (sinh . (n * p))
defpred S1[ Nat] means  for p being real number holds ((cosh . p) + (sinh . p)) |^ $1 = (cosh . ($1 * p)) + (sinh . ($1 * p));
A1: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: for p being real number holds ((cosh . p) + (sinh . p)) |^ n = (cosh . (n * p)) + (sinh . (n * p)) ; ::_thesis: S1[n + 1]
 for p being real number holds ((cosh . p) + (sinh . p)) |^ (n + 1) = (cosh . ((n + 1) * p)) + (sinh . ((n + 1) * p))
proof
let p be real number ; ::_thesis: ((cosh . p) + (sinh . p)) |^ (n + 1) = (cosh . ((n + 1) * p)) + (sinh . ((n + 1) * p))
A3: ((cosh . (n * p)) * (cosh . p)) + ((sinh . (n * p)) * (sinh . p)) = ((((exp_R . (n * p)) + (exp_R . (- (n * p)))) / 2) * (cosh . p)) + ((sinh . (n * p)) * (sinh . p)) by Def3
.= ((((exp_R . (n * p)) + (exp_R . (- (n * p)))) / 2) * (((exp_R . p) + (exp_R . (- p))) / 2)) + ((sinh . (n * p)) * (sinh . p)) by Def3
.= ((((exp_R . (n * p)) + (exp_R . (- (n * p)))) / 2) * (((exp_R . p) + (exp_R . (- p))) / 2)) + ((((exp_R . (n * p)) - (exp_R . (- (n * p)))) / 2) * (sinh . p)) by Def1
.= ((((exp_R . (n * p)) / 2) + ((exp_R . (- (n * p))) / 2)) * (((exp_R . p) / 2) + ((exp_R . (- p)) / 2))) + ((((exp_R . (n * p)) / 2) - ((exp_R . (- (n * p))) / 2)) * (((exp_R . p) - (exp_R . (- p))) / 2)) by Def1
.= (2 * (((exp_R . (n * p)) * (exp_R . p)) / (2 * 2))) + (2 * (((exp_R . (- (n * p))) / 2) * ((exp_R . (- p)) / 2)))
.= (2 * ((exp_R . ((p * n) + (p * 1))) / (2 * 2))) + (2 * (((exp_R . (- (n * p))) * (exp_R . (- p))) / (2 * 2))) by Th12
.= (2 * ((exp_R . (p * (n + 1))) / (2 * 2))) + (2 * ((exp_R . ((- (n * p)) + (- p))) / (2 * 2))) by Th12
.= ((exp_R . (p * (n + 1))) + (exp_R . (- (p * (n + 1))))) / 2
.= cosh . (p * (n + 1)) by Def3 ;
A4: ((cosh . (n * p)) * (sinh . p)) + ((sinh . (n * p)) * (cosh . p)) = ((((exp_R . (n * p)) + (exp_R . (- (n * p)))) / 2) * (sinh . p)) + ((sinh . (n * p)) * (cosh . p)) by Def3
.= ((((exp_R . (n * p)) + (exp_R . (- (n * p)))) / 2) * (((exp_R . p) - (exp_R . (- p))) / 2)) + ((sinh . (n * p)) * (cosh . p)) by Def1
.= ((((exp_R . (n * p)) + (exp_R . (- (n * p)))) / 2) * (((exp_R . p) - (exp_R . (- p))) / 2)) + ((((exp_R . (n * p)) - (exp_R . (- (n * p)))) / 2) * (cosh . p)) by Def1
.= ((((((exp_R . (n * p)) / 2) * ((exp_R . p) / 2)) - (((exp_R . (n * p)) / 2) * ((exp_R . (- p)) / 2))) + (((exp_R . (- (n * p))) / 2) * ((exp_R . p) / 2))) - (((exp_R . (- (n * p))) / 2) * ((exp_R . (- p)) / 2))) + ((((exp_R . (n * p)) - (exp_R . (- (n * p)))) / 2) * (((exp_R . p) + (exp_R . (- p))) / 2)) by Def3
.= (2 * (((exp_R . (n * p)) * (exp_R . p)) / 4)) + (2 * (- (((exp_R . (- (n * p))) * (exp_R . (- p))) / (2 * 2))))
.= (2 * ((exp_R . ((n * p) + p)) / 4)) + (2 * (- (((exp_R . (- (n * p))) * (exp_R . (- p))) / 4))) by Th12
.= (2 * ((exp_R . ((n * p) + p)) / 4)) + (2 * (- ((exp_R . ((- (n * p)) + (- p))) / 4))) by Th12
.= ((exp_R . (p * (n + 1))) - (exp_R . (- (p * (n + 1))))) / 2
.= sinh . (p * (n + 1)) by Def1 ;
((cosh . p) + (sinh . p)) |^ (n + 1) = (((cosh . p) + (sinh . p)) |^ n) * ((cosh . p) + (sinh . p)) by NEWTON:6
.= ((cosh . (n * p)) + (sinh . (n * p))) * ((cosh . p) + (sinh . p)) by A2
.= (sinh . ((n + 1) * p)) + (cosh . ((n + 1) * p)) by A3, A4 ;
hence  ((cosh . p) + (sinh . p)) |^ (n + 1) = (cosh . ((n + 1) * p)) + (sinh . ((n + 1) * p)) ; ::_thesis: verum
end;
hence  S1[n + 1] ; ::_thesis: verum
end;
A5: S1[ 0 ] by Th15, Th16, NEWTON:4;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A5, A1);
hence  ((cosh . p) + (sinh . p)) |^ n = (cosh . (n * p)) + (sinh . (n * p)) ; ::_thesis: verum
end;

theorem Th30: :: SIN_COS2:30
( dom sinh = REAL & dom cosh = REAL & dom tanh = REAL ) by FUNCT_2:def_1;

Lm10:  for d being real number holds compreal . d = (- 1) * d
proof
let d be real number ; ::_thesis: compreal . d = (- 1) * d
thus compreal . d = - d by BINOP_2:def_7
.= (- 1) * d ; ::_thesis: verum
end;

Lm11:  dom compreal = REAL
by FUNCT_2:def_1;

Lm12:  for f being PartFunc of REAL,REAL st f = compreal holds
for p being real number holds
( f is_differentiable_in p & diff (f,p) = - 1 )
proof
reconsider f2 = REAL --> 0 as Function of REAL,REAL ;
deffunc H1( Real) ->  Element of REAL = - $1;
let f be PartFunc of REAL,REAL; ::_thesis: ( f = compreal implies for p being real number holds
( f is_differentiable_in p & diff (f,p) = - 1 ) )
assume A1: f = compreal ; ::_thesis: for p being real number holds
( f is_differentiable_in p & diff (f,p) = - 1 )
let p be real number ; ::_thesis: ( f is_differentiable_in p & diff (f,p) = - 1 )
consider f1 being Function of REAL,REAL such that
A2: for p being Element of REAL holds f1 . p = H1(p) from FUNCT_2:sch_4();
A3: dom f2 = REAL by FUNCOP_1:13;
 for hy1 being non-zero 0 -convergent Real_Sequence holds
( (hy1 ") (#) (f2 /* hy1) is convergent & lim ((hy1 ") (#) (f2 /* hy1)) = 0 )
proof
let hy1 be non-zero 0 -convergent Real_Sequence; ::_thesis: ( (hy1 ") (#) (f2 /* hy1) is convergent & lim ((hy1 ") (#) (f2 /* hy1)) = 0 )
A4: for n being Nat holds ((hy1 ") (#) (f2 /* hy1)) . n = 0
proof
let n be Nat; ::_thesis: ((hy1 ") (#) (f2 /* hy1)) . n = 0
A5: rng hy1 c= dom f2 by A3;
A6: n in NAT by ORDINAL1:def_12;
then ((hy1 ") (#) (f2 /* hy1)) . n = ((hy1 ") . n) * ((f2 /* hy1) . n) by SEQ_1:8
.= ((hy1 . n) ") * ((f2 /* hy1) . n) by VALUED_1:10 ;
then ((hy1 ") (#) (f2 /* hy1)) . n = ((hy1 . n) ") * (f2 . (hy1 . n)) by A6, A5, FUNCT_2:108
.= ((hy1 . n) ") * 0 by FUNCOP_1:7
.= 0 ;
hence  ((hy1 ") (#) (f2 /* hy1)) . n = 0 ; ::_thesis: verum
end;
then A7: (hy1 ") (#) (f2 /* hy1) is constant by VALUED_0:def_18;
 for n being Element of NAT holds lim ((hy1 ") (#) (f2 /* hy1)) = 0
proof
let n be Element of NAT ; ::_thesis: lim ((hy1 ") (#) (f2 /* hy1)) = 0
lim ((hy1 ") (#) (f2 /* hy1)) = ((hy1 ") (#) (f2 /* hy1)) . n by A7, SEQ_4:26
.= 0 by A4 ;
hence  lim ((hy1 ") (#) (f2 /* hy1)) = 0 ; ::_thesis: verum
end;
hence  ( (hy1 ") (#) (f2 /* hy1) is convergent & lim ((hy1 ") (#) (f2 /* hy1)) = 0 ) by A7; ::_thesis: verum
end;
then A8: f2 is RestFunc by FDIFF_1:def_2;
A9: ex N being Neighbourhood of p st
( N c= dom compreal & ( for r being Real st r in N holds
(compreal . r) - (compreal . p) = (f1 . (r - p)) + (f2 . (r - p)) ) )
proof
take  ].(p - 1),(p + 1).[ ; ::_thesis: ( ].(p - 1),(p + 1).[ is Neighbourhood of p & ].(p - 1),(p + 1).[ c= dom compreal & ( for r being Real st r in ].(p - 1),(p + 1).[ holds
(compreal . r) - (compreal . p) = (f1 . (r - p)) + (f2 . (r - p)) ) )
 for r being real number st r in ].(p - 1),(p + 1).[ holds
(compreal . r) - (compreal . p) = (f1 . (r - p)) + (f2 . (r - p))
proof
let r be real number ; ::_thesis: ( r in ].(p - 1),(p + 1).[ implies (compreal . r) - (compreal . p) = (f1 . (r - p)) + (f2 . (r - p)) )
A10: for d being real number holds f2 . d = 0
proof
let d be real number ; ::_thesis: f2 . d = 0
 d is Real by XREAL_0:def_1;
hence  f2 . d = 0 by FUNCOP_1:7; ::_thesis: verum
end;
A11: for p being real number holds f1 . p = - p
proof
let p be real number ; ::_thesis: f1 . p = - p
 p is Real by XREAL_0:def_1;
hence  f1 . p = - p by A2; ::_thesis: verum
end;
(compreal . r) - (compreal . p) = ((- 1) * r) - (compreal . p) by Lm10
.= (((- 1) * r) - ((- 1) * p)) + 0 by Lm10
.= (- (r - p)) + (f2 . (r - p)) by A10
.= (f1 . (r - p)) + (f2 . (r - p)) by A11 ;
hence  ( r in ].(p - 1),(p + 1).[ implies (compreal . r) - (compreal . p) = (f1 . (r - p)) + (f2 . (r - p)) ) ; ::_thesis: verum
end;
hence  ( ].(p - 1),(p + 1).[ is Neighbourhood of p & ].(p - 1),(p + 1).[ c= dom compreal & ( for r being Real st r in ].(p - 1),(p + 1).[ holds
(compreal . r) - (compreal . p) = (f1 . (r - p)) + (f2 . (r - p)) ) ) by Lm11, RCOMP_1:def_6; ::_thesis: verum
end;
 for p being Real holds f1 . p = (- 1) * p
proof
let p be Real; ::_thesis: f1 . p = (- 1) * p
 f1 . p = - p by A2;
hence  f1 . p = (- 1) * p ; ::_thesis: verum
end;
then A12: f1 is LinearFunc by FDIFF_1:def_3;
then  f is_differentiable_in p by A1, A8, A9, FDIFF_1:def_4;
then  diff (f,p) = f1 . 1 by A1, A12, A8, A9, FDIFF_1:def_5
.= - 1 by A2 ;
hence  ( f is_differentiable_in p & diff (f,p) = - 1 ) by A1, A12, A8, A9, FDIFF_1:def_4; ::_thesis: verum
end;

Lm13:  for p being real number
for f being PartFunc of REAL,REAL st f = compreal holds
( exp_R * f is_differentiable_in p & diff ((exp_R * f),p) = (- 1) * (exp_R . (f . p)) )
proof
let p be real number ; ::_thesis: for f being PartFunc of REAL,REAL st f = compreal holds
( exp_R * f is_differentiable_in p & diff ((exp_R * f),p) = (- 1) * (exp_R . (f . p)) )
let f be PartFunc of REAL,REAL; ::_thesis: ( f = compreal implies ( exp_R * f is_differentiable_in p & diff ((exp_R * f),p) = (- 1) * (exp_R . (f . p)) ) )
assume A1: f = compreal ; ::_thesis: ( exp_R * f is_differentiable_in p & diff ((exp_R * f),p) = (- 1) * (exp_R . (f . p)) )
A2: ( p is Real & exp_R is_differentiable_in f . p ) by SIN_COS:65, XREAL_0:def_1;
A3: f is_differentiable_in p by A1, Lm12;
then  diff ((exp_R * f),p) = (diff (exp_R,(f . p))) * (diff (f,p)) by A2, FDIFF_2:13
.= (diff (exp_R,(f . p))) * (- 1) by A1, Lm12
.= (exp_R . (f . p)) * (- 1) by SIN_COS:65 ;
hence  ( exp_R * f is_differentiable_in p & diff ((exp_R * f),p) = (- 1) * (exp_R . (f . p)) ) by A2, A3, FDIFF_2:13; ::_thesis: verum
end;

Lm14:  for p being real number
for f being PartFunc of REAL,REAL st f = compreal holds
exp_R . ((- 1) * p) = (exp_R * f) . p
proof
let p be real number ; ::_thesis: for f being PartFunc of REAL,REAL st f = compreal holds
exp_R . ((- 1) * p) = (exp_R * f) . p
let f be PartFunc of REAL,REAL; ::_thesis: ( f = compreal implies exp_R . ((- 1) * p) = (exp_R * f) . p )
A1: p is Real by XREAL_0:def_1;
assume A2: f = compreal ; ::_thesis: exp_R . ((- 1) * p) = (exp_R * f) . p
then exp_R . ((- 1) * p) = exp_R . (f . p) by Lm10
.= (exp_R * f) . p by A2, A1, FUNCT_2:15 ;
hence  exp_R . ((- 1) * p) = (exp_R * f) . p ; ::_thesis: verum
end;

Lm15:  for p being real number
for f being PartFunc of REAL,REAL st f = compreal holds
( exp_R - (exp_R * f) is_differentiable_in p & exp_R + (exp_R * f) is_differentiable_in p & diff ((exp_R - (exp_R * f)),p) = (exp_R . p) + (exp_R . (- p)) & diff ((exp_R + (exp_R * f)),p) = (exp_R . p) - (exp_R . (- p)) )
proof
let p be real number ; ::_thesis: for f being PartFunc of REAL,REAL st f = compreal holds
( exp_R - (exp_R * f) is_differentiable_in p & exp_R + (exp_R * f) is_differentiable_in p & diff ((exp_R - (exp_R * f)),p) = (exp_R . p) + (exp_R . (- p)) & diff ((exp_R + (exp_R * f)),p) = (exp_R . p) - (exp_R . (- p)) )
let f be PartFunc of REAL,REAL; ::_thesis: ( f = compreal implies ( exp_R - (exp_R * f) is_differentiable_in p & exp_R + (exp_R * f) is_differentiable_in p & diff ((exp_R - (exp_R * f)),p) = (exp_R . p) + (exp_R . (- p)) & diff ((exp_R + (exp_R * f)),p) = (exp_R . p) - (exp_R . (- p)) ) )
A1: ( p is Real & exp_R is_differentiable_in p ) by SIN_COS:65, XREAL_0:def_1;
assume A2: f = compreal ; ::_thesis: ( exp_R - (exp_R * f) is_differentiable_in p & exp_R + (exp_R * f) is_differentiable_in p & diff ((exp_R - (exp_R * f)),p) = (exp_R . p) + (exp_R . (- p)) & diff ((exp_R + (exp_R * f)),p) = (exp_R . p) - (exp_R . (- p)) )
then A3: exp_R * f is_differentiable_in p by Lm13;
then A4: diff ((exp_R + (exp_R * f)),p) = (diff (exp_R,p)) + (diff ((exp_R * f),p)) by A1, FDIFF_1:13
.= (exp_R . p) + (diff ((exp_R * f),p)) by SIN_COS:65
.= (exp_R . p) + ((- 1) * (exp_R . (f . p))) by A2, Lm13
.= (exp_R . p) + ((- 1) * (exp_R . ((- 1) * p))) by A2, Lm10
.= (exp_R . p) - (exp_R . (- p)) ;
diff ((exp_R - (exp_R * f)),p) = (diff (exp_R,p)) - (diff ((exp_R * f),p)) by A1, A3, FDIFF_1:14
.= (exp_R . p) - (diff ((exp_R * f),p)) by SIN_COS:65
.= (exp_R . p) - ((- 1) * (exp_R . (f . p))) by A2, Lm13
.= (exp_R . p) - ((- 1) * (exp_R . ((- 1) * p))) by A2, Lm10
.= (exp_R . p) + (exp_R . (- p)) ;
hence  ( exp_R - (exp_R * f) is_differentiable_in p & exp_R + (exp_R * f) is_differentiable_in p & diff ((exp_R - (exp_R * f)),p) = (exp_R . p) + (exp_R . (- p)) & diff ((exp_R + (exp_R * f)),p) = (exp_R . p) - (exp_R . (- p)) ) by A1, A3, A4, FDIFF_1:13, FDIFF_1:14; ::_thesis: verum
end;

Lm16:  for p being real number
for f being PartFunc of REAL,REAL st f = compreal holds
( (1 / 2) (#) (exp_R - (exp_R * f)) is_differentiable_in p & diff (((1 / 2) (#) (exp_R - (exp_R * f))),p) = (1 / 2) * (diff ((exp_R - (exp_R * f)),p)) )
proof
let p be real number ; ::_thesis: for f being PartFunc of REAL,REAL st f = compreal holds
( (1 / 2) (#) (exp_R - (exp_R * f)) is_differentiable_in p & diff (((1 / 2) (#) (exp_R - (exp_R * f))),p) = (1 / 2) * (diff ((exp_R - (exp_R * f)),p)) )
let f be PartFunc of REAL,REAL; ::_thesis: ( f = compreal implies ( (1 / 2) (#) (exp_R - (exp_R * f)) is_differentiable_in p & diff (((1 / 2) (#) (exp_R - (exp_R * f))),p) = (1 / 2) * (diff ((exp_R - (exp_R * f)),p)) ) )
assume  f = compreal ; ::_thesis: ( (1 / 2) (#) (exp_R - (exp_R * f)) is_differentiable_in p & diff (((1 / 2) (#) (exp_R - (exp_R * f))),p) = (1 / 2) * (diff ((exp_R - (exp_R * f)),p)) )
then  ( p is Real & exp_R - (exp_R * f) is_differentiable_in p ) by Lm15, XREAL_0:def_1;
hence  ( (1 / 2) (#) (exp_R - (exp_R * f)) is_differentiable_in p & diff (((1 / 2) (#) (exp_R - (exp_R * f))),p) = (1 / 2) * (diff ((exp_R - (exp_R * f)),p)) ) by FDIFF_1:15; ::_thesis: verum
end;

Lm17:  for p being real number
for ff being PartFunc of REAL,REAL st ff = compreal holds
sinh . p = ((1 / 2) (#) (exp_R - (exp_R * ff))) . p
proof
let p be real number ; ::_thesis: for ff being PartFunc of REAL,REAL st ff = compreal holds
sinh . p = ((1 / 2) (#) (exp_R - (exp_R * ff))) . p
A1: p is Real by XREAL_0:def_1;
let ff be PartFunc of REAL,REAL; ::_thesis: ( ff = compreal implies sinh . p = ((1 / 2) (#) (exp_R - (exp_R * ff))) . p )
assume A2: ff = compreal ; ::_thesis: sinh . p = ((1 / 2) (#) (exp_R - (exp_R * ff))) . p
A3: ( dom (exp_R - (exp_R * ff)) = (dom exp_R) /\ (dom (exp_R * ff)) & dom (exp_R * ff) = REAL ) by A2, FUNCT_2:def_1, VALUED_1:12;
A4: dom ((1 / 2) (#) (exp_R - (exp_R * ff))) = REAL by A2, FUNCT_2:def_1;
sinh . p = ((exp_R . p) - (exp_R . (- p))) / 2 by Def1
.= (1 / 2) * ((exp_R . p) - (exp_R . ((- 1) * p)))
.= (1 / 2) * ((exp_R . p) - ((exp_R * ff) . p)) by A2, Lm14
.= (1 / 2) * ((exp_R - (exp_R * ff)) . p) by A1, A3, SIN_COS:47, VALUED_1:13
.= ((1 / 2) (#) (exp_R - (exp_R * ff))) . p by A1, A4, VALUED_1:def_5 ;
hence  sinh . p = ((1 / 2) (#) (exp_R - (exp_R * ff))) . p ; ::_thesis: verum
end;

Lm18:  for ff being PartFunc of REAL,REAL st ff = compreal holds
sinh = (1 / 2) (#) (exp_R - (exp_R * ff))
proof
let ff be PartFunc of REAL,REAL; ::_thesis: ( ff = compreal implies sinh = (1 / 2) (#) (exp_R - (exp_R * ff)) )
assume  ff = compreal ; ::_thesis: sinh = (1 / 2) (#) (exp_R - (exp_R * ff))
then A1: ( REAL = dom ((1 / 2) (#) (exp_R - (exp_R * ff))) & ( for p being Element of REAL st p in REAL holds
sinh . p = ((1 / 2) (#) (exp_R - (exp_R * ff))) . p ) ) by Lm17, FUNCT_2:def_1;
 REAL = dom sinh by FUNCT_2:def_1;
hence  sinh = (1 / 2) (#) (exp_R - (exp_R * ff)) by A1, PARTFUN1:5; ::_thesis: verum
end;

theorem Th31: :: SIN_COS2:31
for p being real number holds
( sinh is_differentiable_in p & diff (sinh,p) = cosh . p )
proof
let p be real number ; ::_thesis: ( sinh is_differentiable_in p & diff (sinh,p) = cosh . p )
set ff = compreal ;
A1: sinh = (1 / 2) (#) (exp_R - (exp_R * compreal)) by Lm18;
diff (sinh,p) = diff (((1 / 2) (#) (exp_R - (exp_R * compreal))),p) by Lm18
.= (1 / 2) * (diff ((exp_R - (exp_R * compreal)),p)) by Lm16
.= (1 / 2) * ((exp_R . p) + (exp_R . (- p))) by Lm15
.= ((exp_R . p) + (exp_R . (- p))) / 2
.= cosh . p by Def3 ;
hence  ( sinh is_differentiable_in p & diff (sinh,p) = cosh . p ) by A1, Lm16; ::_thesis: verum
end;

Lm19:  for p being real number
for ff being PartFunc of REAL,REAL st ff = compreal holds
( (1 / 2) (#) (exp_R + (exp_R * ff)) is_differentiable_in p & diff (((1 / 2) (#) (exp_R + (exp_R * ff))),p) = (1 / 2) * (diff ((exp_R + (exp_R * ff)),p)) )
proof
let p be real number ; ::_thesis: for ff being PartFunc of REAL,REAL st ff = compreal holds
( (1 / 2) (#) (exp_R + (exp_R * ff)) is_differentiable_in p & diff (((1 / 2) (#) (exp_R + (exp_R * ff))),p) = (1 / 2) * (diff ((exp_R + (exp_R * ff)),p)) )
let ff be PartFunc of REAL,REAL; ::_thesis: ( ff = compreal implies ( (1 / 2) (#) (exp_R + (exp_R * ff)) is_differentiable_in p & diff (((1 / 2) (#) (exp_R + (exp_R * ff))),p) = (1 / 2) * (diff ((exp_R + (exp_R * ff)),p)) ) )
assume  ff = compreal ; ::_thesis: ( (1 / 2) (#) (exp_R + (exp_R * ff)) is_differentiable_in p & diff (((1 / 2) (#) (exp_R + (exp_R * ff))),p) = (1 / 2) * (diff ((exp_R + (exp_R * ff)),p)) )
then  ( p is Real & exp_R + (exp_R * ff) is_differentiable_in p ) by Lm15, XREAL_0:def_1;
hence  ( (1 / 2) (#) (exp_R + (exp_R * ff)) is_differentiable_in p & diff (((1 / 2) (#) (exp_R + (exp_R * ff))),p) = (1 / 2) * (diff ((exp_R + (exp_R * ff)),p)) ) by FDIFF_1:15; ::_thesis: verum
end;

Lm20:  for p being real number
for ff being PartFunc of REAL,REAL st ff = compreal holds
cosh . p = ((1 / 2) (#) (exp_R + (exp_R * ff))) . p
proof
let p be real number ; ::_thesis: for ff being PartFunc of REAL,REAL st ff = compreal holds
cosh . p = ((1 / 2) (#) (exp_R + (exp_R * ff))) . p
A1: p is Real by XREAL_0:def_1;
let ff be PartFunc of REAL,REAL; ::_thesis: ( ff = compreal implies cosh . p = ((1 / 2) (#) (exp_R + (exp_R * ff))) . p )
assume A2: ff = compreal ; ::_thesis: cosh . p = ((1 / 2) (#) (exp_R + (exp_R * ff))) . p
A3: ( dom (exp_R + (exp_R * ff)) = (dom exp_R) /\ (dom (exp_R * ff)) & dom (exp_R * ff) = REAL ) by A2, FUNCT_2:def_1, VALUED_1:def_1;
A4: dom ((1 / 2) (#) (exp_R + (exp_R * ff))) = REAL by A2, FUNCT_2:def_1;
cosh . p = ((exp_R . p) + (exp_R . (- p))) / 2 by Def3
.= (1 / 2) * ((exp_R . p) + (exp_R . ((- 1) * p)))
.= (1 / 2) * ((exp_R . p) + ((exp_R * ff) . p)) by A2, Lm14
.= (1 / 2) * ((exp_R + (exp_R * ff)) . p) by A1, A3, SIN_COS:47, VALUED_1:def_1
.= ((1 / 2) (#) (exp_R + (exp_R * ff))) . p by A1, A4, VALUED_1:def_5 ;
hence  cosh . p = ((1 / 2) (#) (exp_R + (exp_R * ff))) . p ; ::_thesis: verum
end;

Lm21:  for ff being PartFunc of REAL,REAL st ff = compreal holds
cosh = (1 / 2) (#) (exp_R + (exp_R * ff))
proof
let ff be PartFunc of REAL,REAL; ::_thesis: ( ff = compreal implies cosh = (1 / 2) (#) (exp_R + (exp_R * ff)) )
assume  ff = compreal ; ::_thesis: cosh = (1 / 2) (#) (exp_R + (exp_R * ff))
then A1: ( REAL = dom ((1 / 2) (#) (exp_R + (exp_R * ff))) & ( for p being Element of REAL st p in REAL holds
cosh . p = ((1 / 2) (#) (exp_R + (exp_R * ff))) . p ) ) by Lm20, FUNCT_2:def_1;
 REAL = dom cosh by FUNCT_2:def_1;
hence  cosh = (1 / 2) (#) (exp_R + (exp_R * ff)) by A1, PARTFUN1:5; ::_thesis: verum
end;

theorem Th32: :: SIN_COS2:32
for p being real number holds
( cosh is_differentiable_in p & diff (cosh,p) = sinh . p )
proof
let p be real number ; ::_thesis: ( cosh is_differentiable_in p & diff (cosh,p) = sinh . p )
reconsider ff = compreal as PartFunc of REAL,REAL ;
A1: cosh = (1 / 2) (#) (exp_R + (exp_R * ff)) by Lm21;
diff (cosh,p) = diff (((1 / 2) (#) (exp_R + (exp_R * ff))),p) by Lm21
.= (1 / 2) * (diff ((exp_R + (exp_R * ff)),p)) by Lm19
.= (1 / 2) * ((exp_R . p) - (exp_R . (- p))) by Lm15
.= ((exp_R . p) - (exp_R . (- p))) / 2
.= sinh . p by Def1 ;
hence  ( cosh is_differentiable_in p & diff (cosh,p) = sinh . p ) by A1, Lm19; ::_thesis: verum
end;

Lm22:  for p being real number holds
( sinh / cosh is_differentiable_in p & diff ((sinh / cosh),p) = 1 / ((cosh . p) ^2) )
proof
let p be real number ; ::_thesis: ( sinh / cosh is_differentiable_in p & diff ((sinh / cosh),p) = 1 / ((cosh . p) ^2) )
A1: ( p is Real & cosh . p <> 0 ) by Th15, XREAL_0:def_1;
A2: ( sinh is_differentiable_in p & cosh is_differentiable_in p ) by Th31, Th32;
then  diff ((sinh / cosh),p) = (((diff (sinh,p)) * (cosh . p)) - ((diff (cosh,p)) * (sinh . p))) / ((cosh . p) ^2) by A1, FDIFF_2:14
.= (((cosh . p) * (cosh . p)) - ((diff (cosh,p)) * (sinh . p))) / ((cosh . p) ^2) by Th31
.= (((cosh . p) ^2) - ((sinh . p) * (sinh . p))) / ((cosh . p) ^2) by Th32
.= 1 / ((cosh . p) ^2) by Th14 ;
hence  ( sinh / cosh is_differentiable_in p & diff ((sinh / cosh),p) = 1 / ((cosh . p) ^2) ) by A1, A2, FDIFF_2:14; ::_thesis: verum
end;

Lm23:  tanh = sinh / cosh
proof
 not 0 in rng cosh
proof
assume  0 in rng cosh ; ::_thesis: contradiction
then  ex p being Real st
( p in dom cosh & 0 = cosh . p ) by PARTFUN1:3;
hence  contradiction by Th15; ::_thesis: verum
end;
then A1: ( dom (sinh / cosh) = (dom sinh) /\ ((dom cosh) \ (cosh " {0})) & cosh " {0} = {} ) by FUNCT_1:72, RFUNCT_1:def_1;
 for p being Element of REAL st p in REAL holds
tanh . p = (sinh / cosh) . p
proof
let p be real number ; ::_thesis: ( p is Element of REAL & p in REAL implies tanh . p = (sinh / cosh) . p )
 p is Real by XREAL_0:def_1;
then (sinh / cosh) . p = (sinh . p) * ((cosh . p) ") by A1, Th30, RFUNCT_1:def_1
.= (sinh . p) / (cosh . p) by XCMPLX_0:def_9
.= tanh . p by Th17 ;
hence  ( p is Element of REAL & p in REAL implies tanh . p = (sinh / cosh) . p ) ; ::_thesis: verum
end;
hence  tanh = sinh / cosh by A1, Th30, PARTFUN1:5; ::_thesis: verum
end;

theorem :: SIN_COS2:33
for p being real number holds
( tanh is_differentiable_in p & diff (tanh,p) = 1 / ((cosh . p) ^2) ) by Lm22, Lm23;

theorem Th34: :: SIN_COS2:34
for p being real number holds
( sinh is_differentiable_on REAL & diff (sinh,p) = cosh . p )
proof
let p be real number ; ::_thesis: ( sinh is_differentiable_on REAL & diff (sinh,p) = cosh . p )
A1: ( [#] REAL is open Subset of REAL & REAL c= dom sinh ) by FUNCT_2:def_1;
 for p being Real st p in REAL holds
sinh is_differentiable_in p by Th31;
hence  ( sinh is_differentiable_on REAL & diff (sinh,p) = cosh . p ) by A1, Th31, FDIFF_1:9; ::_thesis: verum
end;

theorem Th35: :: SIN_COS2:35
for p being real number holds
( cosh is_differentiable_on REAL & diff (cosh,p) = sinh . p )
proof
let p be real number ; ::_thesis: ( cosh is_differentiable_on REAL & diff (cosh,p) = sinh . p )
A1: ( [#] REAL is open Subset of REAL & REAL c= dom cosh ) by FUNCT_2:def_1;
 for r being Real st r in REAL holds
cosh is_differentiable_in r by Th32;
hence  ( cosh is_differentiable_on REAL & diff (cosh,p) = sinh . p ) by A1, Th32, FDIFF_1:9; ::_thesis: verum
end;

theorem Th36: :: SIN_COS2:36
for p being real number holds
( tanh is_differentiable_on REAL & diff (tanh,p) = 1 / ((cosh . p) ^2) )
proof
let p be real number ; ::_thesis: ( tanh is_differentiable_on REAL & diff (tanh,p) = 1 / ((cosh . p) ^2) )
 ( [#] REAL is open Subset of REAL & ( for p being Real st p in REAL holds
tanh is_differentiable_in p ) ) by Lm22, Lm23;
hence  ( tanh is_differentiable_on REAL & diff (tanh,p) = 1 / ((cosh . p) ^2) ) by Lm22, Lm23, Th30, FDIFF_1:9; ::_thesis: verum
end;

Lm24:  for p being real number holds (exp_R . p) + (exp_R . (- p)) >= 2
proof
let p be real number ; ::_thesis: (exp_R . p) + (exp_R . (- p)) >= 2
A1: ( exp_R . p >= 0 & exp_R . (- p) >= 0 ) by SIN_COS:54;
2 * (sqrt ((exp_R . p) * (exp_R . (- p)))) = 2 * (sqrt (exp_R . (p + (- p)))) by Th12
.= 2 * 1 by SIN_COS:51, SIN_COS:def_23, SQUARE_1:18 ;
hence  (exp_R . p) + (exp_R . (- p)) >= 2 by A1, Th1; ::_thesis: verum
end;

theorem :: SIN_COS2:37
for p being real number holds cosh . p >= 1
proof
let p be real number ; ::_thesis: cosh . p >= 1
 ((exp_R . p) + (exp_R . (- p))) / 2 >= 2 / 2 by Lm24, XREAL_1:72;
hence  cosh . p >= 1 by Def3; ::_thesis: verum
end;

theorem :: SIN_COS2:38
for p being real number holds sinh is_continuous_in p by Th31, FDIFF_1:24;

theorem :: SIN_COS2:39
for p being real number holds cosh is_continuous_in p by Th32, FDIFF_1:24;

theorem :: SIN_COS2:40
for p being real number holds tanh is_continuous_in p by Lm22, Lm23, FDIFF_1:24;

theorem :: SIN_COS2:41
sinh | REAL is continuous by Th34, FDIFF_1:25;

theorem :: SIN_COS2:42
cosh | REAL is continuous by Th35, FDIFF_1:25;

theorem :: SIN_COS2:43
tanh | REAL is continuous by Th36, FDIFF_1:25;

theorem :: SIN_COS2:44
for p being real number holds
( tanh . p < 1 & tanh . p > - 1 )
proof
let p be real number ; ::_thesis: ( tanh . p < 1 & tanh . p > - 1 )
A1: ( exp_R . p > 0 & exp_R . (- p) > 0 ) by SIN_COS:54;
thus  tanh . p < 1 ::_thesis: tanh . p > - 1
proof
assume  tanh . p >= 1 ; ::_thesis: contradiction
then A2: ((exp_R . p) - (exp_R . (- p))) / ((exp_R . p) + (exp_R . (- p))) >= 1 by Def5;
 ( exp_R . p > 0 & exp_R . (- p) > 0 ) by SIN_COS:54;
then A3: (((exp_R . p) - (exp_R . (- p))) / ((exp_R . p) + (exp_R . (- p)))) * ((exp_R . p) + (exp_R . (- p))) = (exp_R . p) - (exp_R . (- p)) by XCMPLX_1:87;
 (exp_R . p) + (exp_R . (- p)) >= 2 by Lm24;
then  (((exp_R . p) - (exp_R . (- p))) / ((exp_R . p) + (exp_R . (- p)))) * ((exp_R . p) + (exp_R . (- p))) >= 1 * ((exp_R . p) + (exp_R . (- p))) by A2, XREAL_1:64;
then  ((exp_R . p) - (exp_R . (- p))) - (exp_R . p) >= ((exp_R . p) + (exp_R . (- p))) - (exp_R . p) by A3, XREAL_1:9;
then A4: (- (exp_R . (- p))) + (exp_R . (- p)) >= (exp_R . (- p)) + (exp_R . (- p)) by XREAL_1:6;
 exp_R . (- p) > 0 by SIN_COS:54;
hence  contradiction by A4; ::_thesis: verum
end;
assume  tanh . p <= - 1 ; ::_thesis: contradiction
then A5: ((exp_R . p) - (exp_R . (- p))) / ((exp_R . p) + (exp_R . (- p))) <= - 1 by Def5;
 (exp_R . p) + (exp_R . (- p)) >= 2 by Lm24;
then  (((exp_R . p) - (exp_R . (- p))) / ((exp_R . p) + (exp_R . (- p)))) * ((exp_R . p) + (exp_R . (- p))) <= (- 1) * ((exp_R . p) + (exp_R . (- p))) by A5, XREAL_1:64;
then  (exp_R . p) - (exp_R . (- p)) <= - ((exp_R . p) + (exp_R . (- p))) by A1, XCMPLX_1:87;
then A6: ((exp_R . p) - (exp_R . (- p))) + (exp_R . (- p)) <= ((- (exp_R . p)) + (- (exp_R . (- p)))) + (exp_R . (- p)) by XREAL_1:6;
 exp_R . p > 0 by SIN_COS:54;
hence  contradiction by A6; ::_thesis: verum
end;