func sinh -> PartFunc of REAL , REAL means :Def1: :: SIN_COS2:def 1
( dom a₁ = REAL & ( for b₁ being real number holds a₁ . b₁ = ((exp . b₁) - (exp . (- b₁))) / 2 ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines sinh SIN_COS2:def 1 :

definition

let c₁ be number ;
func sinh c₁ -> set equals :: SIN_COS2:def 2
sinh . a₁;
coherence ;

end;

:: deftheorem Def2 defines sinh SIN_COS2:def 2 :

registration

let c₁ be number ;
cluster sinh a₁ -> real ;
coherence ;

end;

definition

let c₁ be number ;
redefine func sinh as sinh c₁ -> Real;
coherence ;

end;

definition

func cosh -> PartFunc of REAL , REAL means :Def3: :: SIN_COS2:def 3
( dom a₁ = REAL & ( for b₁ being real number holds a₁ . b₁ = ((exp . b₁) + (exp . (- b₁))) / 2 ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines cosh SIN_COS2:def 3 :

definition

let c₁ be number ;
func cosh c₁ -> set equals :: SIN_COS2:def 4
cosh . a₁;
coherence ;

end;

:: deftheorem Def4 defines cosh SIN_COS2:def 4 :

registration

let c₁ be number ;
cluster cosh a₁ -> real ;
coherence ;

end;

definition

let c₁ be number ;
redefine func cosh as cosh c₁ -> Real;
coherence ;

end;

definition

func tanh -> PartFunc of REAL , REAL means :Def5: :: SIN_COS2:def 5
( dom a₁ = REAL & ( for b₁ being real number holds a₁ . b₁ = ((exp . b₁) - (exp . (- b₁))) / ((exp . b₁) + (exp . (- b₁))) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines tanh SIN_COS2:def 5 :

definition

let c₁ be number ;
func tanh c₁ -> set equals :: SIN_COS2:def 6
tanh . a₁;
coherence ;

end;

:: deftheorem Def6 defines tanh SIN_COS2:def 6 :

registration

let c₁ be number ;
cluster tanh a₁ -> real ;
coherence ;

end;

definition

let c₁ be number ;
redefine func tanh as tanh c₁ -> Real;
coherence ;

end;

theorem Th12: :: SIN_COS2:12

for b₁, b₂ being real number holds exp . (b₁ + b₂) = (exp . b₁) * (exp . b₂)

proof end;

theorem Th13: :: SIN_COS2:13

exp . 0 = 1 by SIN_COS:56, SIN_COS:def 27;

theorem Th14: :: SIN_COS2:14

for b₁ being real number holds
( ((cosh . b₁) ^2 ) - ((sinh . b₁) ^2 ) = 1 & ((cosh . b₁) * (cosh . b₁)) - ((sinh . b₁) * (sinh . b₁)) = 1 )

proof end;

Lemma10: for b₁, b₂ being real number holds cosh . (b₁ + b₂) = ((cosh . b₁) * (cosh . b₂)) + ((sinh . b₁) * (sinh . b₂))

proof end;

Lemma11: for b₁, b₂ being real number holds sinh . (b₁ + b₂) = ((sinh . b₁) * (cosh . b₂)) + ((cosh . b₁) * (sinh . b₂))

proof end;

theorem Th15: :: SIN_COS2:15

for b₁ being real number holds
( cosh . b₁ <> 0 & cosh . b₁ > 0 & cosh . 0 = 1 )

proof end;

theorem Th16: :: SIN_COS2:16

sinh . 0 = 0

proof end;

theorem Th17: :: SIN_COS2:17

for b₁ being real number holds tanh . b₁ = (sinh . b₁) / (cosh . b₁)

proof end;

Lemma15: for b₁, b₂, b₃, b₄ being real number st b₁ <> 0 & b₂ <> 0 & (b₁ * b₂) + (b₃ * b₄) <> 0 holds
((b₃ * b₂) + (b₁ * b₄)) / ((b₁ * b₂) + (b₃ * b₄)) = ((b₃ / b₁) + (b₄ / b₂)) / (1 + ((b₃ / b₁) * (b₄ / b₂)))

proof end;

Lemma16: for b₁, b₂ being real number holds tanh . (b₁ + b₂) = ((tanh . b₁) + (tanh . b₂)) / (1 + ((tanh . b₁) * (tanh . b₂)))

proof end;

theorem Th18: :: SIN_COS2:18

for b₁ being real number holds
( (sinh . b₁) ^2 = (1 / 2) * ((cosh . (2 * b₁)) - 1) & (cosh . b₁) ^2 = (1 / 2) * ((cosh . (2 * b₁)) + 1) )

proof end;

Lemma18: for b₁ being real number holds
( sinh . (2 * b₁) = (2 * (sinh . b₁)) * (cosh . b₁) & cosh . (2 * b₁) = (2 * ((cosh . b₁) ^2 )) - 1 )

proof end;

theorem Th19: :: SIN_COS2:19

for b₁ being real number holds
( cosh . (- b₁) = cosh . b₁ & sinh . (- b₁) = - (sinh . b₁) & tanh . (- b₁) = - (tanh . b₁) )

proof end;

Lemma20: for b₁, b₂ being real number holds cosh . (b₁ - b₂) = ((cosh . b₁) * (cosh . b₂)) - ((sinh . b₁) * (sinh . b₂))

proof end;

theorem Th20: :: SIN_COS2:20

for b₁, b₂ being real number holds
( cosh . (b₁ + b₂) = ((cosh . b₁) * (cosh . b₂)) + ((sinh . b₁) * (sinh . b₂)) & cosh . (b₁ - b₂) = ((cosh . b₁) * (cosh . b₂)) - ((sinh . b₁) * (sinh . b₂)) ) by Lemma10, Lemma20;

Lemma21: for b₁, b₂ being real number holds sinh . (b₁ - b₂) = ((sinh . b₁) * (cosh . b₂)) - ((cosh . b₁) * (sinh . b₂))

proof end;

theorem Th21: :: SIN_COS2:21

for b₁, b₂ being real number holds
( sinh . (b₁ + b₂) = ((sinh . b₁) * (cosh . b₂)) + ((cosh . b₁) * (sinh . b₂)) & sinh . (b₁ - b₂) = ((sinh . b₁) * (cosh . b₂)) - ((cosh . b₁) * (sinh . b₂)) ) by Lemma11, Lemma21;

Lemma22: for b₁, b₂ being real number holds tanh . (b₁ - b₂) = ((tanh . b₁) - (tanh . b₂)) / (1 - ((tanh . b₁) * (tanh . b₂)))

proof end;

theorem Th22: :: SIN_COS2:22

for b₁, b₂ being real number holds
( tanh . (b₁ + b₂) = ((tanh . b₁) + (tanh . b₂)) / (1 + ((tanh . b₁) * (tanh . b₂))) & tanh . (b₁ - b₂) = ((tanh . b₁) - (tanh . b₂)) / (1 - ((tanh . b₁) * (tanh . b₂))) ) by Lemma16, Lemma22;

theorem Th23: :: SIN_COS2:23

for b₁ being real number holds
( sinh . (2 * b₁) = (2 * (sinh . b₁)) * (cosh . b₁) & cosh . (2 * b₁) = (2 * ((cosh . b₁) ^2 )) - 1 & tanh . (2 * b₁) = (2 * (tanh . b₁)) / (1 + ((tanh . b₁) ^2 )) )

proof end;

theorem Th24: :: SIN_COS2:24

for b₁, b₂ being real number holds
( ((sinh . b₁) ^2 ) - ((sinh . b₂) ^2 ) = (sinh . (b₁ + b₂)) * (sinh . (b₁ - b₂)) & (sinh . (b₁ + b₂)) * (sinh . (b₁ - b₂)) = ((cosh . b₁) ^2 ) - ((cosh . b₂) ^2 ) & ((sinh . b₁) ^2 ) - ((sinh . b₂) ^2 ) = ((cosh . b₁) ^2 ) - ((cosh . b₂) ^2 ) )

proof end;

theorem Th25: :: SIN_COS2:25

for b₁, b₂ being real number holds
( ((sinh . b₁) ^2 ) + ((cosh . b₂) ^2 ) = (cosh . (b₁ + b₂)) * (cosh . (b₁ - b₂)) & (cosh . (b₁ + b₂)) * (cosh . (b₁ - b₂)) = ((cosh . b₁) ^2 ) + ((sinh . b₂) ^2 ) & ((sinh . b₁) ^2 ) + ((cosh . b₂) ^2 ) = ((cosh . b₁) ^2 ) + ((sinh . b₂) ^2 ) )

proof end;

theorem Th26: :: SIN_COS2:26

for b₁, b₂ being real number holds
( (sinh . b₁) + (sinh . b₂) = (2 * (sinh . ((b₁ / 2) + (b₂ / 2)))) * (cosh . ((b₁ / 2) - (b₂ / 2))) & (sinh . b₁) - (sinh . b₂) = (2 * (sinh . ((b₁ / 2) - (b₂ / 2)))) * (cosh . ((b₁ / 2) + (b₂ / 2))) )

proof end;

theorem Th27: :: SIN_COS2:27

for b₁, b₂ being real number holds
( (cosh . b₁) + (cosh . b₂) = (2 * (cosh . ((b₁ / 2) + (b₂ / 2)))) * (cosh . ((b₁ / 2) - (b₂ / 2))) & (cosh . b₁) - (cosh . b₂) = (2 * (sinh . ((b₁ / 2) - (b₂ / 2)))) * (sinh . ((b₁ / 2) + (b₂ / 2))) )

proof end;

theorem Th28: :: SIN_COS2:28

for b₁, b₂ being real number holds
( (tanh . b₁) + (tanh . b₂) = (sinh . (b₁ + b₂)) / ((cosh . b₁) * (cosh . b₂)) & (tanh . b₁) - (tanh . b₂) = (sinh . (b₁ - b₂)) / ((cosh . b₁) * (cosh . b₂)) )

proof end;

theorem Th29: :: SIN_COS2:29

for b₁ being real number
for b₂ being Nat holds ((cosh . b₁) + (sinh . b₁)) |^ b₂ = (cosh . (b₂ * b₁)) + (sinh . (b₂ * b₁))

proof end;

registration

cluster sinh -> total ;
coherence

proof end;

cluster cosh -> total ;
coherence

proof end;

cluster tanh -> total ;
coherence

proof end;

end;

theorem Th30: :: SIN_COS2:30

( dom sinh = REAL & dom cosh = REAL & dom tanh = REAL ) by Def1, Def3, Def5;

Lemma26: for b₁ being real number holds compreal . b₁ = (- 1) * b₁

proof end;

Lemma27: ( dom compreal = REAL & rng compreal c= REAL )
by FUNCT_2:def 1, RELSET_1:12;

Lemma28: for b₁ being PartFunc of REAL , REAL st b₁ = compreal holds
for b₂ being real number holds
( b₁ is_differentiable_in b₂ & diff b₁,b₂ = - 1 )

proof end;

Lemma29: for b₁ being real number
for b₂ being PartFunc of REAL , REAL st b₂ = compreal holds
( exp * b₂ is_differentiable_in b₁ & diff (exp * b₂),b₁ = (- 1) * (exp . (b₂ . b₁)) )

proof end;

Lemma30: for b₁ being real number
for b₂ being PartFunc of REAL , REAL st b₂ = compreal holds
exp . ((- 1) * b₁) = (exp * b₂) . b₁

proof end;

Lemma31: for b₁ being real number
for b₂ being PartFunc of REAL , REAL st b₂ = compreal holds
( exp - (exp * b₂) is_differentiable_in b₁ & exp + (exp * b₂) is_differentiable_in b₁ & diff (exp - (exp * b₂)),b₁ = (exp . b₁) + (exp . (- b₁)) & diff (exp + (exp * b₂)),b₁ = (exp . b₁) - (exp . (- b₁)) )

proof end;

Lemma32: for b₁ being real number
for b₂ being PartFunc of REAL , REAL st b₂ = compreal holds
( (1 / 2) (#) (exp - (exp * b₂)) is_differentiable_in b₁ & diff ((1 / 2) (#) (exp - (exp * b₂))),b₁ = (1 / 2) * (diff (exp - (exp * b₂)),b₁) )

proof end;

Lemma33: for b₁ being real number
for b₂ being PartFunc of REAL , REAL st b₂ = compreal holds
sinh . b₁ = ((1 / 2) (#) (exp - (exp * b₂))) . b₁

proof end;

Lemma34: for b₁ being PartFunc of REAL , REAL st b₁ = compreal holds
sinh = (1 / 2) (#) (exp - (exp * b₁))

proof end;

theorem Th31: :: SIN_COS2:31

for b₁ being real number holds
( sinh is_differentiable_in b₁ & diff sinh ,b₁ = cosh . b₁ )

proof end;

Lemma36: for b₁ being real number
for b₂ being PartFunc of REAL , REAL st b₂ = compreal holds
( (1 / 2) (#) (exp + (exp * b₂)) is_differentiable_in b₁ & diff ((1 / 2) (#) (exp + (exp * b₂))),b₁ = (1 / 2) * (diff (exp + (exp * b₂)),b₁) )

proof end;

Lemma37: for b₁ being real number
for b₂ being PartFunc of REAL , REAL st b₂ = compreal holds
cosh . b₁ = ((1 / 2) (#) (exp + (exp * b₂))) . b₁

proof end;

Lemma38: for b₁ being PartFunc of REAL , REAL st b₁ = compreal holds
cosh = (1 / 2) (#) (exp + (exp * b₁))

proof end;

theorem Th32: :: SIN_COS2:32

for b₁ being real number holds
( cosh is_differentiable_in b₁ & diff cosh ,b₁ = sinh . b₁ )

proof end;

Lemma40: for b₁ being real number holds
( sinh / cosh is_differentiable_in b₁ & diff (sinh / cosh ),b₁ = 1 / ((cosh . b₁) ^2 ) )

proof end;

Lemma41: tanh = sinh / cosh

proof end;

theorem Th33: :: SIN_COS2:33

for b₁ being real number holds
( tanh is_differentiable_in b₁ & diff tanh ,b₁ = 1 / ((cosh . b₁) ^2 ) ) by Lemma40, Lemma41;

theorem Th34: :: SIN_COS2:34

for b₁ being real number holds
( sinh is_differentiable_on REAL & diff sinh ,b₁ = cosh . b₁ )

proof end;

theorem Th35: :: SIN_COS2:35

for b₁ being real number holds
( cosh is_differentiable_on REAL & diff cosh ,b₁ = sinh . b₁ )

proof end;

theorem Th36: :: SIN_COS2:36

for b₁ being real number holds
( tanh is_differentiable_on REAL & diff tanh ,b₁ = 1 / ((cosh . b₁) ^2 ) )

proof end;

Lemma45: for b₁ being real number holds (exp . b₁) + (exp . (- b₁)) >= 2

proof end;

theorem Th37: :: SIN_COS2:37

for b₁ being real number holds cosh . b₁ >= 1

proof end;

theorem Th38: :: SIN_COS2:38

for b₁ being real number holds sinh is_continuous_in b₁

proof end;

theorem Th39: :: SIN_COS2:39

for b₁ being real number holds cosh is_continuous_in b₁

proof end;

theorem Th40: :: SIN_COS2:40

for b₁ being real number holds tanh is_continuous_in b₁

proof end;

theorem Th41: :: SIN_COS2:41

sinh is_continuous_on REAL by Th34, FDIFF_1:33;

theorem Th42: :: SIN_COS2:42

cosh is_continuous_on REAL by Th35, FDIFF_1:33;

theorem Th43: :: SIN_COS2:43

tanh is_continuous_on REAL by Th36, FDIFF_1:33;

theorem Th44: :: SIN_COS2:44

for b₁ being real number holds
( tanh . b₁ < 1 & tanh . b₁ > - 1 )

proof end;