:: by Takashi Mitsuishi and Yuguang Yang

::

:: Received March 13, 1999

:: Copyright (c) 1999-2016 Association of Mizar Users

Lm1: for th being Real st th in ].0,(PI / 2).[ holds

0 < sin . th

proof end;

definition

ex b_{1} being Function of REAL,REAL st

for d being Real holds b_{1} . d = ((exp_R . d) - (exp_R . (- d))) / 2

for b_{1}, b_{2} being Function of REAL,REAL st ( for d being Real holds b_{1} . d = ((exp_R . d) - (exp_R . (- d))) / 2 ) & ( for d being Real holds b_{2} . d = ((exp_R . d) - (exp_R . (- d))) / 2 ) holds

b_{1} = b_{2}
end;

func sinh -> Function of REAL,REAL means :Def1: :: SIN_COS2:def 1

for d being Real holds it . d = ((exp_R . d) - (exp_R . (- d))) / 2;

existence for d being Real holds it . d = ((exp_R . d) - (exp_R . (- d))) / 2;

ex b

for d being Real holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines sinh SIN_COS2:def 1 :

for b_{1} being Function of REAL,REAL holds

( b_{1} = sinh iff for d being Real holds b_{1} . d = ((exp_R . d) - (exp_R . (- d))) / 2 );

for b

( b

definition
end;

definition

ex b_{1} being Function of REAL,REAL st

for d being Real holds b_{1} . d = ((exp_R . d) + (exp_R . (- d))) / 2

for b_{1}, b_{2} being Function of REAL,REAL st ( for d being Real holds b_{1} . d = ((exp_R . d) + (exp_R . (- d))) / 2 ) & ( for d being Real holds b_{2} . d = ((exp_R . d) + (exp_R . (- d))) / 2 ) holds

b_{1} = b_{2}
end;

func cosh -> Function of REAL,REAL means :Def3: :: SIN_COS2:def 3

for d being Real holds it . d = ((exp_R . d) + (exp_R . (- d))) / 2;

existence for d being Real holds it . d = ((exp_R . d) + (exp_R . (- d))) / 2;

ex b

for d being Real holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def3 defines cosh SIN_COS2:def 3 :

for b_{1} being Function of REAL,REAL holds

( b_{1} = cosh iff for d being Real holds b_{1} . d = ((exp_R . d) + (exp_R . (- d))) / 2 );

for b

( b

definition
end;

definition

ex b_{1} being Function of REAL,REAL st

for d being Real holds b_{1} . d = ((exp_R . d) - (exp_R . (- d))) / ((exp_R . d) + (exp_R . (- d)))

for b_{1}, b_{2} being Function of REAL,REAL st ( for d being Real holds b_{1} . d = ((exp_R . d) - (exp_R . (- d))) / ((exp_R . d) + (exp_R . (- d))) ) & ( for d being Real holds b_{2} . d = ((exp_R . d) - (exp_R . (- d))) / ((exp_R . d) + (exp_R . (- d))) ) holds

b_{1} = b_{2}
end;

func tanh -> Function of REAL,REAL means :Def5: :: SIN_COS2:def 5

for d being Real holds it . d = ((exp_R . d) - (exp_R . (- d))) / ((exp_R . d) + (exp_R . (- d)));

existence for d being Real holds it . d = ((exp_R . d) - (exp_R . (- d))) / ((exp_R . d) + (exp_R . (- d)));

ex b

for d being Real holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def5 defines tanh SIN_COS2:def 5 :

for b_{1} being Function of REAL,REAL holds

( b_{1} = tanh iff for d being Real holds b_{1} . d = ((exp_R . d) - (exp_R . (- d))) / ((exp_R . d) + (exp_R . (- d))) );

for b

( b

definition
end;

theorem Th14: :: SIN_COS2:14

for p being Real holds

( ((cosh . p) ^2) - ((sinh . p) ^2) = 1 & ((cosh . p) * (cosh . p)) - ((sinh . p) * (sinh . p)) = 1 )

( ((cosh . p) ^2) - ((sinh . p) ^2) = 1 & ((cosh . p) * (cosh . p)) - ((sinh . p) * (sinh . p)) = 1 )

proof end;

Lm2: for p, r being Real holds cosh . (p + r) = ((cosh . p) * (cosh . r)) + ((sinh . p) * (sinh . r))

proof end;

Lm3: for p, r being Real holds sinh . (p + r) = ((sinh . p) * (cosh . r)) + ((cosh . p) * (sinh . r))

proof end;

Lm4: for p, q, r, a1 being Real st r <> 0 & q <> 0 holds

((p * q) + (r * a1)) / ((r * q) + (p * a1)) = ((p / r) + (a1 / q)) / (1 + ((p / r) * (a1 / q)))

proof end;

Lm5: for p, r being Real holds tanh . (p + r) = ((tanh . p) + (tanh . r)) / (1 + ((tanh . p) * (tanh . r)))

proof end;

theorem Th18: :: SIN_COS2:18

for p being Real holds

( (sinh . p) ^2 = (1 / 2) * ((cosh . (2 * p)) - 1) & (cosh . p) ^2 = (1 / 2) * ((cosh . (2 * p)) + 1) )

( (sinh . p) ^2 = (1 / 2) * ((cosh . (2 * p)) - 1) & (cosh . p) ^2 = (1 / 2) * ((cosh . (2 * p)) + 1) )

proof end;

Lm6: for p being Real holds

( sinh . (2 * p) = (2 * (sinh . p)) * (cosh . p) & cosh . (2 * p) = (2 * ((cosh . p) ^2)) - 1 )

proof end;

theorem Th19: :: SIN_COS2:19

for p being Real holds

( cosh . (- p) = cosh . p & sinh . (- p) = - (sinh . p) & tanh . (- p) = - (tanh . p) )

( cosh . (- p) = cosh . p & sinh . (- p) = - (sinh . p) & tanh . (- p) = - (tanh . p) )

proof end;

Lm7: for p, r being Real holds cosh . (p - r) = ((cosh . p) * (cosh . r)) - ((sinh . p) * (sinh . r))

proof end;

theorem :: SIN_COS2:20

Lm8: for p, r being Real holds sinh . (p - r) = ((sinh . p) * (cosh . r)) - ((cosh . p) * (sinh . r))

proof end;

theorem :: SIN_COS2:21

Lm9: for p, r being Real holds tanh . (p - r) = ((tanh . p) - (tanh . r)) / (1 - ((tanh . p) * (tanh . r)))

proof end;

theorem :: SIN_COS2:22

theorem :: SIN_COS2:23

for p being Real 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)) )

( 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 end;

theorem Th24: :: SIN_COS2:24

for p, q being Real 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) )

( ((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 end;

theorem Th25: :: SIN_COS2:25

for p, q being Real 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) )

( ((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 end;

theorem :: SIN_COS2:26

for p, r being Real 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))) )

( (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 end;

theorem :: SIN_COS2:27

for p, r being Real 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))) )

( (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 end;

theorem :: SIN_COS2:28

for p, r being Real holds

( (tanh . p) + (tanh . r) = (sinh . (p + r)) / ((cosh . p) * (cosh . r)) & (tanh . p) - (tanh . r) = (sinh . (p - r)) / ((cosh . p) * (cosh . r)) )

( (tanh . p) + (tanh . r) = (sinh . (p + r)) / ((cosh . p) * (cosh . r)) & (tanh . p) - (tanh . r) = (sinh . (p - r)) / ((cosh . p) * (cosh . r)) )

proof end;

theorem :: SIN_COS2:29

for p being Real

for n being Nat holds ((cosh . p) + (sinh . p)) |^ n = (cosh . (n * p)) + (sinh . (n * p))

for n being Nat holds ((cosh . p) + (sinh . p)) |^ n = (cosh . (n * p)) + (sinh . (n * p))

proof end;

Lm10: for d being Real holds compreal . d = (- 1) * d

proof 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 holds

( f is_differentiable_in p & diff (f,p) = - 1 )

proof end;

Lm13: for p being Real

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 end;

Lm14: for p being Real

for f being PartFunc of REAL,REAL st f = compreal holds

exp_R . ((- 1) * p) = (exp_R * f) . p

proof end;

Lm15: for p being Real

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 end;

Lm16: for p being Real

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 end;

Lm17: for p being Real

for ff being PartFunc of REAL,REAL st ff = compreal holds

sinh . p = ((1 / 2) (#) (exp_R - (exp_R * ff))) . p

proof end;

Lm18: for ff being PartFunc of REAL,REAL st ff = compreal holds

sinh = (1 / 2) (#) (exp_R - (exp_R * ff))

proof end;

Lm19: for p being Real

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 end;

Lm20: for p being Real

for ff being PartFunc of REAL,REAL st ff = compreal holds

cosh . p = ((1 / 2) (#) (exp_R + (exp_R * ff))) . p

proof end;

Lm21: for ff being PartFunc of REAL,REAL st ff = compreal holds

cosh = (1 / 2) (#) (exp_R + (exp_R * ff))

proof end;

Lm22: for p being Real holds

( sinh / cosh is_differentiable_in p & diff ((sinh / cosh),p) = 1 / ((cosh . p) ^2) )

proof end;

Lm23: tanh = sinh / cosh

proof end;

theorem :: SIN_COS2:33

Lm24: for p being Real holds (exp_R . p) + (exp_R . (- p)) >= 2

proof end;