:: Formulas And Identities of Inverse Hyperbolic Functions
:: by Fuguo Ge , Xiquan Liang and Yuzhong Ding
::
:: Received May 24, 2005
:: Copyright (c) 2005 Association of Mizar Users
Lm1:
1 / 1 = 1
;
Lm2:
( number_e > 0 & number_e <> 1 )
by TAYLOR_1:11;
Lm3:
for x, y being real number st x ^2 < 1 & y < 1 holds
(x ^2 ) * y < 1
theorem Th1: :: SIN_COS7:1
theorem Th2: :: SIN_COS7:2
theorem Th3: :: SIN_COS7:3
theorem Th4: :: SIN_COS7:4
theorem Th5: :: SIN_COS7:5
Lm4:
for x being real number st 1 <= x holds
(x ^2 ) - 1 >= 0
theorem :: SIN_COS7:6
theorem Th7: :: SIN_COS7:7
theorem Th8: :: SIN_COS7:8
theorem Th9: :: SIN_COS7:9
theorem Th10: :: SIN_COS7:10
theorem Th11: :: SIN_COS7:11
Lm5:
for x being real number st x ^2 < 1 holds
(x + 1) / (1 - x) > 0
theorem Th12: :: SIN_COS7:12
theorem Th13: :: SIN_COS7:13
theorem Th14: :: SIN_COS7:14
theorem Th15: :: SIN_COS7:15
theorem Th16: :: SIN_COS7:16
Lm7:
for x being real number st 0 < x & x < 1 holds
0 < 1 - (x ^2 )
theorem Th17: :: SIN_COS7:17
theorem Th18: :: SIN_COS7:18
theorem Th19: :: SIN_COS7:19
theorem Th20: :: SIN_COS7:20
theorem Th21: :: SIN_COS7:21
theorem Th22: :: SIN_COS7:22
theorem Th23: :: SIN_COS7:23
theorem Th24: :: SIN_COS7:24
theorem Th25: :: SIN_COS7:25
theorem Th26: :: SIN_COS7:26
theorem Th27: :: SIN_COS7:27
theorem Th28: :: SIN_COS7:28
theorem Th29: :: SIN_COS7:29
theorem Th30: :: SIN_COS7:30
Lm8:
for x being real number holds (x ^2 ) + 1 > 0
theorem Th31: :: SIN_COS7:31
theorem Th32: :: SIN_COS7:32
Lm9:
for t being real number st ( 1 < t or t < - 1 ) holds
0 < (t + 1) / (t - 1)
Lm10:
for x being real number holds sqrt ((x ^2 ) + 1) > x
Lm11:
for x, y being real number holds ((sqrt ((x ^2 ) + 1)) * (sqrt ((y ^2 ) + 1))) - (x * y) > 0
Lm12:
for y being real number st 1 <= y holds
y + (sqrt ((y ^2 ) - 1)) > 0
Lm13:
for t being real number st 0 < t holds
- 1 < ((t ^2 ) - 1) / ((t ^2 ) + 1)
Lm14:
for t being real number st 0 < t & t <> 1 & not 1 < ((t ^2 ) + 1) / ((t ^2 ) - 1) holds
((t ^2 ) + 1) / ((t ^2 ) - 1) < - 1
Lm15:
for t being real number st 0 < t holds
0 < (2 * t) / (1 + (t ^2 ))
Lm16:
for t being real number st 0 < t holds
(2 * t) / (1 + (t ^2 )) <= 1
Lm17:
for t being real number st 0 < t holds
0 < (1 + (sqrt (1 + (t ^2 )))) / t
Lm18:
for t being real number st 0 < t holds
(1 - (sqrt (1 + (t ^2 )))) / t < 0
Lm19:
for t being real number st 0 < t & t <= 1 holds
0 <= 1 - (t ^2 )
Lm20:
for t being real number st 0 < t & t <= 1 holds
0 <= 4 - (4 * (t ^2 ))
Lm21:
for t being real number st 0 < t & t <= 1 holds
0 < 1 + (sqrt (1 - (t ^2 )))
Lm22:
for t being real number st 0 < t & t <= 1 holds
0 < (1 + (sqrt (1 - (t ^2 )))) / t
Lm23:
for t being real number st 0 < t & t <> 1 holds
(2 * t) / ((t ^2 ) - 1) <> 0
Lm24:
for t being real number st t < 0 holds
(1 + (sqrt (1 + (t ^2 )))) / t < 0
Lm25:
for t being real number st t < 0 holds
0 < (1 - (sqrt (1 + (t ^2 )))) / t
:: deftheorem defines sinh" SIN_COS7:def 1 :
:: deftheorem defines cosh1" SIN_COS7:def 2 :
:: deftheorem defines cosh2" SIN_COS7:def 3 :
:: deftheorem defines tanh" SIN_COS7:def 4 :
:: deftheorem defines coth" SIN_COS7:def 5 :
:: deftheorem defines sech1" SIN_COS7:def 6 :
:: deftheorem defines sech2" SIN_COS7:def 7 :
:: deftheorem Def8 defines csch" SIN_COS7:def 8 :
theorem :: SIN_COS7:33
theorem :: SIN_COS7:34
theorem :: SIN_COS7:35
theorem :: SIN_COS7:36
theorem :: SIN_COS7:37
theorem :: SIN_COS7:38
theorem :: SIN_COS7:39
theorem :: SIN_COS7:40
theorem :: SIN_COS7:41
theorem :: SIN_COS7:42
theorem :: SIN_COS7:43
theorem :: SIN_COS7:44
theorem :: SIN_COS7:45
theorem :: SIN_COS7:46
theorem :: SIN_COS7:47
theorem :: SIN_COS7:48
theorem :: SIN_COS7:49
theorem :: SIN_COS7:50
theorem :: SIN_COS7:51
theorem :: SIN_COS7:52
theorem :: SIN_COS7:53
theorem :: SIN_COS7:54
theorem :: SIN_COS7:55
theorem :: SIN_COS7:56
theorem :: SIN_COS7:57
theorem :: SIN_COS7:58
theorem :: SIN_COS7:59
theorem :: SIN_COS7:60
theorem :: SIN_COS7:61
theorem :: SIN_COS7:62
theorem :: SIN_COS7:63
theorem :: SIN_COS7:64
theorem :: SIN_COS7:65
theorem :: SIN_COS7:66
theorem :: SIN_COS7:67
theorem :: SIN_COS7:68
theorem Th69: :: SIN_COS7:69
theorem Th70: :: SIN_COS7:70
theorem Th71: :: SIN_COS7:71
theorem :: SIN_COS7:72
theorem :: SIN_COS7:73