begin
theorem Th1:
theorem Th2:
theorem
theorem
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem
theorem
theorem Th11:
theorem
theorem Th13:
theorem
theorem
theorem Th16:
theorem Th17:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
:: deftheorem defines coth SIN_COS5:def 1 :
for x being real number holds coth x = (cosh x) / (sinh x);
:: deftheorem defines sech SIN_COS5:def 2 :
for x being real number holds sech x = 1 / (cosh x);
:: deftheorem defines cosech SIN_COS5:def 3 :
for x being real number holds cosech x = 1 / (sinh x);
theorem Th36:
theorem
theorem
theorem
Lm1:
for x being real number holds coth (- x) = - (coth x)
theorem Th40:
theorem
theorem
Lm2:
for x being real number holds (cosh . x) ^2 = 1 + ((sinh . x) ^2)
Lm3:
for x being real number holds ((cosh . x) ^2) - 1 = (sinh . x) ^2
theorem
theorem
theorem
Lm4:
for x being real number st x > 0 holds
sinh x >= 0
theorem
theorem
theorem
theorem
theorem
theorem
theorem