:: 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

proof end;

theorem Th1: :: SIN_COS7:1

for x being real number st x > 0 holds
1 / x = x to_power (- 1)

proof end;

theorem Th2: :: SIN_COS7:2

for x being real number st x > 1 holds
((sqrt ((x ^2 ) - 1)) / x) ^2 < 1

proof end;

theorem Th3: :: SIN_COS7:3

for x being real number holds (x / (sqrt ((x ^2 ) + 1))) ^2 < 1

proof end;

theorem Th4: :: SIN_COS7:4

for x being real number holds sqrt ((x ^2 ) + 1) > 0

proof end;

theorem Th5: :: SIN_COS7:5

for x being real number holds (sqrt ((x ^2 ) + 1)) + x > 0

proof end;

Lm4: for x being real number st 1 <= x holds
(x ^2 ) - 1 >= 0

proof end;

theorem :: SIN_COS7:6

for y, x being real number st y >= 0 & x >= 1 holds
(x + 1) / y >= 0 ;

theorem Th7: :: SIN_COS7:7

for y, x being real number st y >= 0 & x >= 1 holds
(x - 1) / y >= 0

proof end;

theorem Th8: :: SIN_COS7:8

for x being real number st x >= 1 holds
sqrt ((x + 1) / 2) >= 1

proof end;

theorem Th9: :: SIN_COS7:9

for y, x being real number st y >= 0 & x >= 1 holds
((x ^2 ) - 1) / y >= 0

proof end;

theorem Th10: :: SIN_COS7:10

for x being real number st x >= 1 holds
(sqrt ((x + 1) / 2)) + (sqrt ((x - 1) / 2)) > 0

proof end;

theorem Th11: :: SIN_COS7:11

for x being real number st x ^2 < 1 holds
( x + 1 > 0 & 1 - x > 0 )

proof end;

Lm5: for x being real number st x ^2 < 1 holds
(x + 1) / (1 - x) > 0

proof end;

theorem Th12: :: SIN_COS7:12

for x being real number st x <> 1 holds
(1 - x) ^2 > 0

proof end;

theorem Th13: :: SIN_COS7:13

for x being real number st x ^2 < 1 holds
((x ^2 ) + 1) / (1 - (x ^2 )) >= 0

proof end;

theorem Th14: :: SIN_COS7:14

for x being real number st x ^2 < 1 holds
((2 * x) / (1 + (x ^2 ))) ^2 < 1

proof end;

theorem Th15: :: SIN_COS7:15

for x being real number st 0 < x & x < 1 holds
(1 + x) / (1 - x) > 0

proof end;

theorem Th16: :: SIN_COS7:16

for x being real number st 0 < x & x < 1 holds
x ^2 < 1

proof end;

Lm7: for x being real number st 0 < x & x < 1 holds
0 < 1 - (x ^2 )

proof end;

theorem Th17: :: SIN_COS7:17

for x being real number st 0 < x & x < 1 holds
1 / (sqrt (1 - (x ^2 ))) > 1

proof end;

theorem Th18: :: SIN_COS7:18

for x being real number st 0 < x & x < 1 holds
(2 * x) / (1 - (x ^2 )) > 0

proof end;

theorem Th19: :: SIN_COS7:19

for x being real number st 0 < x & x < 1 holds
0 < (1 - (x ^2 )) ^2

proof end;

theorem Th20: :: SIN_COS7:20

for x being real number st 0 < x & x < 1 holds
(1 + (x ^2 )) / (1 - (x ^2 )) > 1

proof end;

theorem Th21: :: SIN_COS7:21

for x being real number st 1 < x ^2 holds
(1 / x) ^2 < 1

proof end;

theorem Th22: :: SIN_COS7:22

for x being real number st 0 < x & x <= 1 holds
1 - (x ^2 ) >= 0

proof end;

theorem Th23: :: SIN_COS7:23

for x being real number st 1 <= x holds
0 < x + (sqrt ((x ^2 ) - 1))

proof end;

theorem Th24: :: SIN_COS7:24

for x, y being real number st 1 <= x & 1 <= y holds
0 <= (x * (sqrt ((y ^2 ) - 1))) + (y * (sqrt ((x ^2 ) - 1)))

proof end;

theorem Th25: :: SIN_COS7:25

for x, y being real number st 1 <= x & 1 <= y & abs y <= abs x holds
0 < y - (sqrt ((y ^2 ) - 1))

proof end;

theorem Th26: :: SIN_COS7:26

for x, y being real number st 1 <= x & 1 <= y & abs y <= abs x holds
0 <= (y * (sqrt ((x ^2 ) - 1))) - (x * (sqrt ((y ^2 ) - 1)))

proof end;

theorem Th27: :: SIN_COS7:27

for x, y being real number st x ^2 < 1 & y ^2 < 1 holds
x * y <> - 1

proof end;

theorem Th28: :: SIN_COS7:28

for x, y being real number st x ^2 < 1 & y ^2 < 1 holds
x * y <> 1

proof end;

theorem Th29: :: SIN_COS7:29

for x being real number st x <> 0 holds
exp_R x <> 1

proof end;

theorem Th30: :: SIN_COS7:30

for x being real number st 0 <> x holds
((exp_R x) ^2 ) - 1 <> 0

proof end;

Lm8: for x being real number holds (x ^2 ) + 1 > 0

proof end;

theorem Th31: :: SIN_COS7:31

for t being real number st 0 < t holds
((t ^2 ) - 1) / ((t ^2 ) + 1) < 1

proof end;

theorem Th32: :: SIN_COS7:32

for t being real number st - 1 < t & t < 1 holds
0 < (t + 1) / (1 - t)

proof end;

Lm9: for t being real number st ( 1 < t or t < - 1 ) holds
0 < (t + 1) / (t - 1)

proof end;

Lm10: for x being real number holds sqrt ((x ^2 ) + 1) > x

proof end;

Lm11: for x, y being real number holds ((sqrt ((x ^2 ) + 1)) * (sqrt ((y ^2 ) + 1))) - (x * y) > 0

proof end;

Lm12: for y being real number st 1 <= y holds
y + (sqrt ((y ^2 ) - 1)) > 0

proof end;

Lm13: for t being real number st 0 < t holds
- 1 < ((t ^2 ) - 1) / ((t ^2 ) + 1)

proof end;

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

proof end;

Lm15: for t being real number st 0 < t holds
0 < (2 * t) / (1 + (t ^2 ))

proof end;

Lm16: for t being real number st 0 < t holds
(2 * t) / (1 + (t ^2 )) <= 1

proof end;

Lm17: for t being real number st 0 < t holds
0 < (1 + (sqrt (1 + (t ^2 )))) / t

proof end;

Lm18: for t being real number st 0 < t holds
(1 - (sqrt (1 + (t ^2 )))) / t < 0

proof end;

Lm19: for t being real number st 0 < t & t <= 1 holds
0 <= 1 - (t ^2 )

proof end;

Lm20: for t being real number st 0 < t & t <= 1 holds
0 <= 4 - (4 * (t ^2 ))

proof end;

Lm21: for t being real number st 0 < t & t <= 1 holds
0 < 1 + (sqrt (1 - (t ^2 )))

proof end;

Lm22: for t being real number st 0 < t & t <= 1 holds
0 < (1 + (sqrt (1 - (t ^2 )))) / t

proof end;

Lm23: for t being real number st 0 < t & t <> 1 holds
(2 * t) / ((t ^2 ) - 1) <> 0

proof end;

Lm24: for t being real number st t < 0 holds
(1 + (sqrt (1 + (t ^2 )))) / t < 0

proof end;

Lm25: for t being real number st t < 0 holds
0 < (1 - (sqrt (1 + (t ^2 )))) / t

proof end;

definition

let x be real number ;
func sinh" x -> real number equals :: SIN_COS7:def 1
log number_e ,(x + (sqrt ((x ^2 ) + 1)));
coherence
log number_e ,(x + (sqrt ((x ^2 ) + 1))) is real number ;

end;

:: deftheorem defines sinh" SIN_COS7:def 1 :

for x being real number holds sinh" x = log number_e ,(x + (sqrt ((x ^2 ) + 1)));

definition

let x be real number ;
func cosh1" x -> real number equals :: SIN_COS7:def 2
log number_e ,(x + (sqrt ((x ^2 ) - 1)));
coherence
log number_e ,(x + (sqrt ((x ^2 ) - 1))) is real number ;

end;

:: deftheorem defines cosh1" SIN_COS7:def 2 :

for x being real number holds cosh1" x = log number_e ,(x + (sqrt ((x ^2 ) - 1)));

definition

let x be real number ;
func cosh2" x -> real number equals :: SIN_COS7:def 3
- (log number_e ,(x + (sqrt ((x ^2 ) - 1))));
coherence
- (log number_e ,(x + (sqrt ((x ^2 ) - 1)))) is real number ;

end;

:: deftheorem defines cosh2" SIN_COS7:def 3 :

for x being real number holds cosh2" x = - (log number_e ,(x + (sqrt ((x ^2 ) - 1))));

definition

let x be real number ;
func tanh" x -> real number equals :: SIN_COS7:def 4
(1 / 2) * (log number_e ,((1 + x) / (1 - x)));
coherence
(1 / 2) * (log number_e ,((1 + x) / (1 - x))) is real number ;

end;

:: deftheorem defines tanh" SIN_COS7:def 4 :

for x being real number holds tanh" x = (1 / 2) * (log number_e ,((1 + x) / (1 - x)));

definition

let x be real number ;
func coth" x -> real number equals :: SIN_COS7:def 5
(1 / 2) * (log number_e ,((x + 1) / (x - 1)));
coherence
(1 / 2) * (log number_e ,((x + 1) / (x - 1))) is real number ;

end;

:: deftheorem defines coth" SIN_COS7:def 5 :

for x being real number holds coth" x = (1 / 2) * (log number_e ,((x + 1) / (x - 1)));

definition

let x be real number ;
func sech1" x -> real number equals :: SIN_COS7:def 6
log number_e ,((1 + (sqrt (1 - (x ^2 )))) / x);
coherence
log number_e ,((1 + (sqrt (1 - (x ^2 )))) / x) is real number ;

end;

:: deftheorem defines sech1" SIN_COS7:def 6 :

for x being real number holds sech1" x = log number_e ,((1 + (sqrt (1 - (x ^2 )))) / x);

definition

let x be real number ;
func sech2" x -> real number equals :: SIN_COS7:def 7
- (log number_e ,((1 + (sqrt (1 - (x ^2 )))) / x));
coherence
- (log number_e ,((1 + (sqrt (1 - (x ^2 )))) / x)) is real number ;

end;

:: deftheorem defines sech2" SIN_COS7:def 7 :

for x being real number holds sech2" x = - (log number_e ,((1 + (sqrt (1 - (x ^2 )))) / x));

definition

let x be real number ;
func csch" x -> real number equals :Def8: :: SIN_COS7:def 8
log number_e ,((1 + (sqrt (1 + (x ^2 )))) / x) if 0 < x
log number_e ,((1 - (sqrt (1 + (x ^2 )))) / x) if x < 0
;
correctness
coherence
( ( 0 < x implies log number_e ,((1 + (sqrt (1 + (x ^2 )))) / x) is real number ) & ( x < 0 implies log number_e ,((1 - (sqrt (1 + (x ^2 )))) / x) is real number ) );
consistency
for b₁ being real number st 0 < x & x < 0 holds
( b₁ = log number_e ,((1 + (sqrt (1 + (x ^2 )))) / x) iff b₁ = log number_e ,((1 - (sqrt (1 + (x ^2 )))) / x) );
;

end;

:: deftheorem Def8 defines csch" SIN_COS7:def 8 :

for x being real number holds
( ( 0 < x implies csch" x = log number_e ,((1 + (sqrt (1 + (x ^2 )))) / x) ) & ( x < 0 implies csch" x = log number_e ,((1 - (sqrt (1 + (x ^2 )))) / x) ) );

theorem :: SIN_COS7:33

for x being real number st 0 <= x holds
sinh" x = cosh1" (sqrt ((x ^2 ) + 1))

proof end;

theorem :: SIN_COS7:34

for x being real number st x < 0 holds
sinh" x = cosh2" (sqrt ((x ^2 ) + 1))

proof end;

theorem :: SIN_COS7:35

for x being real number holds sinh" x = tanh" (x / (sqrt ((x ^2 ) + 1)))

proof end;

theorem :: SIN_COS7:36

for x being real number st x >= 1 holds
cosh1" x = sinh" (sqrt ((x ^2 ) - 1))

proof end;

theorem :: SIN_COS7:37

for x being real number st x > 1 holds
cosh1" x = tanh" ((sqrt ((x ^2 ) - 1)) / x)

proof end;

theorem :: SIN_COS7:38

for x being real number st x >= 1 holds
cosh1" x = 2 * (cosh1" (sqrt ((x + 1) / 2)))

proof end;

theorem :: SIN_COS7:39

for x being real number st x >= 1 holds
cosh2" x = 2 * (cosh2" (sqrt ((x + 1) / 2)))

proof end;

theorem :: SIN_COS7:40

for x being real number st x >= 1 holds
cosh1" x = 2 * (sinh" (sqrt ((x - 1) / 2)))

proof end;

theorem :: SIN_COS7:41

for x being real number st x ^2 < 1 holds
tanh" x = sinh" (x / (sqrt (1 - (x ^2 ))))

proof end;

theorem :: SIN_COS7:42

for x being real number st 0 < x & x < 1 holds
tanh" x = cosh1" (1 / (sqrt (1 - (x ^2 ))))

proof end;

theorem :: SIN_COS7:43

for x being real number st x ^2 < 1 holds
tanh" x = (1 / 2) * (sinh" ((2 * x) / (1 - (x ^2 ))))

proof end;

theorem :: SIN_COS7:44

for x being real number st x > 0 & x < 1 holds
tanh" x = (1 / 2) * (cosh1" ((1 + (x ^2 )) / (1 - (x ^2 ))))

proof end;

theorem :: SIN_COS7:45

for x being real number st x ^2 < 1 holds
tanh" x = (1 / 2) * (tanh" ((2 * x) / (1 + (x ^2 ))))

proof end;

theorem :: SIN_COS7:46

for x being real number st x ^2 > 1 holds
coth" x = tanh" (1 / x)

proof end;

theorem :: SIN_COS7:47

for x being real number st x > 0 & x <= 1 holds
sech1" x = cosh1" (1 / x)

proof end;

theorem :: SIN_COS7:48

for x being real number st x > 0 & x <= 1 holds
sech2" x = cosh2" (1 / x)

proof end;

theorem :: SIN_COS7:49

for x being real number st x > 0 holds
csch" x = sinh" (1 / x)

proof end;

theorem :: SIN_COS7:50

for x, y being real number st (x * y) + ((sqrt ((x ^2 ) + 1)) * (sqrt ((y ^2 ) + 1))) >= 0 holds
(sinh" x) + (sinh" y) = sinh" ((x * (sqrt (1 + (y ^2 )))) + (y * (sqrt (1 + (x ^2 )))))

proof end;

theorem :: SIN_COS7:51

for x, y being real number holds (sinh" x) - (sinh" y) = sinh" ((x * (sqrt (1 + (y ^2 )))) - (y * (sqrt (1 + (x ^2 )))))

proof end;

theorem :: SIN_COS7:52

for x, y being real number st 1 <= x & 1 <= y holds
(cosh1" x) + (cosh1" y) = cosh1" ((x * y) + (sqrt (((x ^2 ) - 1) * ((y ^2 ) - 1))))

proof end;

theorem :: SIN_COS7:53

for x, y being real number st 1 <= x & 1 <= y holds
(cosh2" x) + (cosh2" y) = cosh2" ((x * y) + (sqrt (((x ^2 ) - 1) * ((y ^2 ) - 1))))

proof end;

theorem :: SIN_COS7:54

for x, y being real number st 1 <= x & 1 <= y & abs y <= abs x holds
(cosh1" x) - (cosh1" y) = cosh1" ((x * y) - (sqrt (((x ^2 ) - 1) * ((y ^2 ) - 1))))

proof end;

theorem :: SIN_COS7:55

for x, y being real number st 1 <= x & 1 <= y & abs y <= abs x holds
(cosh2" x) - (cosh2" y) = cosh2" ((x * y) - (sqrt (((x ^2 ) - 1) * ((y ^2 ) - 1))))

proof end;

theorem :: SIN_COS7:56

for x, y being real number st x ^2 < 1 & y ^2 < 1 holds
(tanh" x) + (tanh" y) = tanh" ((x + y) / (1 + (x * y)))

proof end;

theorem :: SIN_COS7:57

for x, y being real number st x ^2 < 1 & y ^2 < 1 holds
(tanh" x) - (tanh" y) = tanh" ((x - y) / (1 - (x * y)))

proof end;

theorem :: SIN_COS7:58

for x being real number st 0 < x & ((x - 1) / (x + 1)) ^2 < 1 holds
log number_e ,x = 2 * (tanh" ((x - 1) / (x + 1)))

proof end;

theorem :: SIN_COS7:59

for x being real number st 0 < x & (((x ^2 ) - 1) / ((x ^2 ) + 1)) ^2 < 1 holds
log number_e ,x = tanh" (((x ^2 ) - 1) / ((x ^2 ) + 1))

proof end;

theorem :: SIN_COS7:60

for x being real number st 1 < x & 1 <= ((x ^2 ) + 1) / (2 * x) holds
log number_e ,x = cosh1" (((x ^2 ) + 1) / (2 * x))

proof end;

theorem :: SIN_COS7:61

for x being real number st 0 < x & x < 1 & 1 <= ((x ^2 ) + 1) / (2 * x) holds
log number_e ,x = cosh2" (((x ^2 ) + 1) / (2 * x))

proof end;

theorem :: SIN_COS7:62

for x being real number st 0 < x holds
log number_e ,x = sinh" (((x ^2 ) - 1) / (2 * x))

proof end;

theorem :: SIN_COS7:63

for y, x being real number st y = (1 / 2) * ((exp_R x) - (exp_R (- x))) holds
x = log number_e ,(y + (sqrt ((y ^2 ) + 1)))

proof end;

theorem :: SIN_COS7:64

for y, x being real number st y = (1 / 2) * ((exp_R x) + (exp_R (- x))) & 1 <= y & not x = log number_e ,(y + (sqrt ((y ^2 ) - 1))) holds
x = - (log number_e ,(y + (sqrt ((y ^2 ) - 1))))

proof end;

theorem :: SIN_COS7:65

for y, x being real number st y = ((exp_R x) - (exp_R (- x))) / ((exp_R x) + (exp_R (- x))) holds
x = (1 / 2) * (log number_e ,((1 + y) / (1 - y)))

proof end;

theorem :: SIN_COS7:66

for y, x being real number st y = ((exp_R x) + (exp_R (- x))) / ((exp_R x) - (exp_R (- x))) & x <> 0 holds
x = (1 / 2) * (log number_e ,((y + 1) / (y - 1)))

proof end;

theorem :: SIN_COS7:67

for y, x being real number holds
( not y = 1 / (((exp_R x) + (exp_R (- x))) / 2) or x = log number_e ,((1 + (sqrt (1 - (y ^2 )))) / y) or x = - (log number_e ,((1 + (sqrt (1 - (y ^2 )))) / y)) )

proof end;

theorem :: SIN_COS7:68

for y, x being real number st y = 1 / (((exp_R x) - (exp_R (- x))) / 2) & x <> 0 & not x = log number_e ,((1 + (sqrt (1 + (y ^2 )))) / y) holds
x = log number_e ,((1 - (sqrt (1 + (y ^2 )))) / y)

proof end;

theorem Th69: :: SIN_COS7:69

for x being real number holds cosh . (2 * x) = 1 + (2 * ((sinh . x) ^2 ))

proof end;

theorem Th70: :: SIN_COS7:70

for x being real number holds (cosh . x) ^2 = 1 + ((sinh . x) ^2 )

proof end;

theorem Th71: :: SIN_COS7:71

for x being real number holds (sinh . x) ^2 = ((cosh . x) ^2 ) - 1

proof end;

theorem :: SIN_COS7:72

for x being real number holds sinh (5 * x) = ((5 * (sinh x)) + (20 * ((sinh x) |^ 3))) + (16 * ((sinh x) |^ 5))

proof end;

theorem :: SIN_COS7:73

for x being real number holds cosh (5 * x) = ((5 * (cosh x)) - (20 * ((cosh x) |^ 3))) + (16 * ((cosh x) |^ 5))

proof end;