begin
Lm1:
for th being real number st th in ].0,(PI / 2).[ holds
0 < sin . th
begin
Lm2:
for p, r being real number holds cosh . (p + r) = ((cosh . p) * (cosh . r)) + ((sinh . p) * (sinh . r))
Lm3:
for p, r being real number holds sinh . (p + r) = ((sinh . p) * (cosh . r)) + ((cosh . p) * (sinh . r))
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)))
Lm5:
for p, r being real number holds tanh . (p + r) = ((tanh . p) + (tanh . r)) / (1 + ((tanh . p) * (tanh . r)))
Lm6:
for p being real number holds
( sinh . (2 * p) = (2 * (sinh . p)) * (cosh . p) & cosh . (2 * p) = (2 * ((cosh . p) ^2)) - 1 )
Lm7:
for p, r being real number holds cosh . (p - r) = ((cosh . p) * (cosh . r)) - ((sinh . p) * (sinh . r))
Lm8:
for p, r being real number holds sinh . (p - r) = ((sinh . p) * (cosh . r)) - ((cosh . p) * (sinh . r))
Lm9:
for p, r being real number holds tanh . (p - r) = ((tanh . p) - (tanh . r)) / (1 - ((tanh . p) * (tanh . r)))
Lm10:
for d being real number holds compreal . d = (- 1) * d
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 )
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)) )
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
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)) )
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)) )
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
Lm18:
for ff being PartFunc of REAL,REAL st ff = compreal holds
sinh = (1 / 2) (#) (exp_R - (exp_R * ff))
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)) )
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
Lm21:
for ff being PartFunc of REAL,REAL st ff = compreal holds
cosh = (1 / 2) (#) (exp_R + (exp_R * ff))
Lm22:
for p being real number holds
( sinh / cosh is_differentiable_in p & diff ((sinh / cosh),p) = 1 / ((cosh . p) ^2) )
Lm23:
tanh = sinh / cosh
Lm24:
for p being real number holds (exp_R . p) + (exp_R . (- p)) >= 2