begin
theorem Th1:
theorem
Lm1:
for th being real number st th in ].0 ,(PI / 2).[ holds
0 < sin . th
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
begin
:: 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 );
:: deftheorem defines sinh SIN_COS2:def 2 :
for d being number holds sinh d = sinh . d;
:: 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 );
:: deftheorem defines cosh SIN_COS2:def 4 :
for d being number holds cosh d = cosh . d;
:: 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))) );
:: deftheorem defines tanh SIN_COS2:def 6 :
for d being number holds tanh d = tanh . d;
theorem Th12:
theorem Th13:
theorem Th14:
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))
theorem Th15:
theorem Th16:
theorem Th17:
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)))
theorem Th18:
Lm6:
for p being real number holds
( sinh . (2 * p) = (2 * (sinh . p)) * (cosh . p) & cosh . (2 * p) = (2 * ((cosh . p) ^2 )) - 1 )
theorem Th19:
Lm7:
for p, r being real number holds cosh . (p - r) = ((cosh . p) * (cosh . r)) - ((sinh . p) * (sinh . r))
theorem
Lm8:
for p, r being real number holds sinh . (p - r) = ((sinh . p) * (cosh . r)) - ((cosh . p) * (sinh . r))
theorem
Lm9:
for p, r being real number holds tanh . (p - r) = ((tanh . p) - (tanh . r)) / (1 - ((tanh . p) * (tanh . r)))
theorem
theorem
theorem Th24:
theorem Th25:
theorem
theorem
theorem
theorem
theorem Th30:
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))
theorem Th31:
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))
theorem Th32:
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
theorem
theorem Th34:
theorem Th35:
theorem Th36:
Lm24:
for p being real number holds (exp_R . p) + (exp_R . (- p)) >= 2
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem