:: Formulas And Identities of Inverse Hyperbolic Functions
:: by Fuguo Ge , Xiquan Liang and Yuzhong Ding
::
:: Received May 24, 2005
:: Copyright (c) 2005-2021 Association of Mizar Users


Lm1: number_e <> 1
by TAYLOR_1:11;

Lm2: for x, y being Real st x ^2 < 1 & y < 1 holds
(x ^2) * y < 1

proof end;

theorem Th1: :: SIN_COS7:1
for x being Real st x > 0 holds
1 / x = x to_power (- 1)
proof end;

theorem :: SIN_COS7:2
for x being Real st x > 1 holds
((sqrt ((x ^2) - 1)) / x) ^2 < 1
proof end;

theorem :: SIN_COS7:3
for x being Real holds (x / (sqrt ((x ^2) + 1))) ^2 < 1
proof end;

theorem Th4: :: SIN_COS7:4
for x being Real holds sqrt ((x ^2) + 1) > 0
proof end;

theorem Th5: :: SIN_COS7:5
for x being Real holds (sqrt ((x ^2) + 1)) + x > 0
proof end;

Lm3: for x being Real st 1 <= x holds
(x ^2) - 1 >= 0

proof end;

theorem :: SIN_COS7:6
for x, y being Real st y >= 0 & x >= 1 holds
(x + 1) / y >= 0 ;

theorem Th7: :: SIN_COS7:7
for x, y being Real st y >= 0 & x >= 1 holds
(x - 1) / y >= 0
proof end;

theorem Th8: :: SIN_COS7:8
for x being Real st x >= 1 holds
sqrt ((x + 1) / 2) >= 1
proof end;

theorem Th9: :: SIN_COS7:9
for x, y being Real st y >= 0 & x >= 1 holds
((x ^2) - 1) / y >= 0
proof end;

theorem Th10: :: SIN_COS7:10
for x being Real st x >= 1 holds
(sqrt ((x + 1) / 2)) + (sqrt ((x - 1) / 2)) > 0
proof end;

theorem Th11: :: SIN_COS7:11
for x being Real st x ^2 < 1 holds
( x + 1 > 0 & 1 - x > 0 )
proof end;

Lm4: for x being Real st x ^2 < 1 holds
(x + 1) / (1 - x) > 0

proof end;

theorem Th12: :: SIN_COS7:12
for x being Real st x <> 1 holds
(1 - x) ^2 > 0
proof end;

theorem Th13: :: SIN_COS7:13
for x being Real st x ^2 < 1 holds
((x ^2) + 1) / (1 - (x ^2)) >= 0
proof end;

theorem :: SIN_COS7:14
for x being Real st x ^2 < 1 holds
((2 * x) / (1 + (x ^2))) ^2 < 1
proof end;

theorem Th15: :: SIN_COS7:15
for x being Real st 0 < x & x < 1 holds
(1 + x) / (1 - x) > 0
proof end;

theorem :: SIN_COS7:16
for x being Real st 0 < x & x < 1 holds
x ^2 < 1
proof end;

Lm5: for x being Real st 0 < x & x < 1 holds
0 < 1 - (x ^2)

proof end;

theorem :: SIN_COS7:17
for x being Real st 0 < x & x < 1 holds
1 / (sqrt (1 - (x ^2))) > 1
proof end;

theorem Th18: :: SIN_COS7:18
for x being Real st 0 < x & x < 1 holds
(2 * x) / (1 - (x ^2)) > 0
proof end;

theorem Th19: :: SIN_COS7:19
for x being Real st 0 < x & x < 1 holds
0 < (1 - (x ^2)) ^2
proof end;

theorem :: SIN_COS7:20
for x being Real st 0 < x & x < 1 holds
(1 + (x ^2)) / (1 - (x ^2)) > 1
proof end;

theorem :: SIN_COS7:21
for x being Real st 1 < x ^2 holds
(1 / x) ^2 < 1
proof end;

theorem Th22: :: SIN_COS7:22
for x being Real st 0 < x & x <= 1 holds
1 - (x ^2) >= 0
proof end;

theorem Th23: :: SIN_COS7:23
for x being Real st 1 <= x holds
0 < x + (sqrt ((x ^2) - 1))
proof end;

theorem Th24: :: SIN_COS7:24
for x, y being Real 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 y being Real st 1 <= y holds
0 < y - (sqrt ((y ^2) - 1))
proof end;

theorem Th26: :: SIN_COS7:26
for x, y being Real st 1 <= x & 1 <= y & |.y.| <= |.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 st x ^2 < 1 & y ^2 < 1 holds
x * y <> - 1
proof end;

theorem Th28: :: SIN_COS7:28
for x, y being Real st x ^2 < 1 & y ^2 < 1 holds
x * y <> 1
proof end;

theorem Th29: :: SIN_COS7:29
for x being Real st x <> 0 holds
exp_R x <> 1
proof end;

theorem Th30: :: SIN_COS7:30
for x being Real st 0 <> x holds
((exp_R x) ^2) - 1 <> 0
proof end;

Lm6: for x being Real holds (x ^2) + 1 > 0
proof end;

theorem Th31: :: SIN_COS7:31
for t being Real holds ((t ^2) - 1) / ((t ^2) + 1) < 1
proof end;

theorem Th32: :: SIN_COS7:32
for t being Real st - 1 < t & t < 1 holds
0 < (t + 1) / (1 - t)
proof end;

Lm7: for t being Real st ( 1 < t or t < - 1 ) holds
0 < (t + 1) / (t - 1)

proof end;

Lm8: for x being Real holds sqrt ((x ^2) + 1) > x
proof end;

Lm9: for x, y being Real holds ((sqrt ((x ^2) + 1)) * (sqrt ((y ^2) + 1))) - (x * y) > 0
proof end;

Lm10: for y being Real st 1 <= y holds
y + (sqrt ((y ^2) - 1)) > 0

proof end;

Lm11: for t being Real st 0 < t holds
- 1 < ((t ^2) - 1) / ((t ^2) + 1)

proof end;

Lm12: for t being Real st 0 < t & t <> 1 & not 1 < ((t ^2) + 1) / ((t ^2) - 1) holds
((t ^2) + 1) / ((t ^2) - 1) < - 1

proof end;

Lm13: for t being Real st 0 < t holds
0 < (2 * t) / (1 + (t ^2))

;

Lm14: for t being Real st 0 < t holds
(2 * t) / (1 + (t ^2)) <= 1

proof end;

Lm15: for t being Real st 0 < t holds
(1 - (sqrt (1 + (t ^2)))) / t < 0

proof end;

Lm16: for t being Real st 0 < t & t <= 1 holds
0 <= 1 - (t ^2)

proof end;

Lm17: for t being Real st 0 < t & t <= 1 holds
0 <= 4 - (4 * (t ^2))

proof end;

Lm18: for t being Real st 0 < t & t <= 1 holds
0 < 1 + (sqrt (1 - (t ^2)))

proof end;

Lm19: for t being Real st 0 < t & t <= 1 holds
0 < (1 + (sqrt (1 - (t ^2)))) / t

proof end;

Lm20: for t being Real st 0 < t & t <> 1 holds
(2 * t) / ((t ^2) - 1) <> 0

proof end;

Lm21: for t being Real st t < 0 holds
(1 + (sqrt (1 + (t ^2)))) / t < 0

proof end;

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

:: deftheorem defines sinh" SIN_COS7:def 1 :
for x being Real holds sinh" x = log (number_e,(x + (sqrt ((x ^2) + 1))));

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

:: deftheorem defines cosh1" SIN_COS7:def 2 :
for x being Real holds cosh1" x = log (number_e,(x + (sqrt ((x ^2) - 1))));

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

:: deftheorem defines cosh2" SIN_COS7:def 3 :
for x being Real holds cosh2" x = - (log (number_e,(x + (sqrt ((x ^2) - 1)))));

definition
let x be Real;
func tanh" x -> Real 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
;
end;

:: deftheorem defines tanh" SIN_COS7:def 4 :
for x being Real holds tanh" x = (1 / 2) * (log (number_e,((1 + x) / (1 - x))));

definition
let x be Real;
func coth" x -> Real 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
;
end;

:: deftheorem defines coth" SIN_COS7:def 5 :
for x being Real holds coth" x = (1 / 2) * (log (number_e,((x + 1) / (x - 1))));

definition
let x be Real;
func sech1" x -> Real 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
;
end;

:: deftheorem defines sech1" SIN_COS7:def 6 :
for x being Real holds sech1" x = log (number_e,((1 + (sqrt (1 - (x ^2)))) / x));

definition
let x be Real;
func sech2" x -> Real 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
;
end;

:: deftheorem defines sech2" SIN_COS7:def 7 :
for x being Real holds sech2" x = - (log (number_e,((1 + (sqrt (1 - (x ^2)))) / x)));

definition
let x be Real;
func csch" x -> Real 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 ) & ( x < 0 implies log (number_e,((1 - (sqrt (1 + (x ^2)))) / x)) is Real ) )
;
consistency
for b1 being Real st 0 < x & x < 0 holds
( b1 = log (number_e,((1 + (sqrt (1 + (x ^2)))) / x)) iff b1 = log (number_e,((1 - (sqrt (1 + (x ^2)))) / x)) )
;
;
end;

:: deftheorem Def8 defines csch" SIN_COS7:def 8 :
for x being Real 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 st 0 <= x holds
sinh" x = cosh1" (sqrt ((x ^2) + 1))
proof end;

theorem :: SIN_COS7:34
for x being Real st x < 0 holds
sinh" x = cosh2" (sqrt ((x ^2) + 1))
proof end;

theorem :: SIN_COS7:35
for x being Real holds sinh" x = tanh" (x / (sqrt ((x ^2) + 1)))
proof end;

theorem :: SIN_COS7:36
for x being Real st x >= 1 holds
cosh1" x = sinh" (sqrt ((x ^2) - 1))
proof end;

theorem :: SIN_COS7:37
for x being Real st x > 1 holds
cosh1" x = tanh" ((sqrt ((x ^2) - 1)) / x)
proof end;

theorem :: SIN_COS7:38
for x being Real st x >= 1 holds
cosh1" x = 2 * (cosh1" (sqrt ((x + 1) / 2)))
proof end;

theorem :: SIN_COS7:39
for x being Real st x >= 1 holds
cosh2" x = 2 * (cosh2" (sqrt ((x + 1) / 2)))
proof end;

theorem :: SIN_COS7:40
for x being Real st x >= 1 holds
cosh1" x = 2 * (sinh" (sqrt ((x - 1) / 2)))
proof end;

theorem :: SIN_COS7:41
for x being Real st x ^2 < 1 holds
tanh" x = sinh" (x / (sqrt (1 - (x ^2))))
proof end;

theorem :: SIN_COS7:42
for x being Real st 0 < x & x < 1 holds
tanh" x = cosh1" (1 / (sqrt (1 - (x ^2))))
proof end;

theorem :: SIN_COS7:43
for x being Real 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 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 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 st x ^2 > 1 holds
coth" x = tanh" (1 / x)
proof end;

theorem :: SIN_COS7:47
for x being Real st x > 0 & x <= 1 holds
sech1" x = cosh1" (1 / x)
proof end;

theorem :: SIN_COS7:48
for x being Real st x > 0 & x <= 1 holds
sech2" x = cosh2" (1 / x)
proof end;

theorem :: SIN_COS7:49
for x being Real st x > 0 holds
csch" x = sinh" (1 / x)
proof end;

theorem :: SIN_COS7:50
for x, y being Real 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 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 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 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 st 1 <= x & 1 <= y & |.y.| <= |.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 st 1 <= x & 1 <= y & |.y.| <= |.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 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 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 st 0 < x holds
log (number_e,x) = 2 * (tanh" ((x - 1) / (x + 1)))
proof end;

theorem :: SIN_COS7:59
for x being Real st 0 < x holds
log (number_e,x) = tanh" (((x ^2) - 1) / ((x ^2) + 1))
proof end;

theorem :: SIN_COS7:60
for x being Real st 1 < x holds
log (number_e,x) = cosh1" (((x ^2) + 1) / (2 * x))
proof end;

theorem :: SIN_COS7:61
for x being Real 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 st 0 < x holds
log (number_e,x) = sinh" (((x ^2) - 1) / (2 * x))
proof end;

theorem :: SIN_COS7:63
for x, y being Real 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 x, y being Real 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 x, y being Real 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 x, y being Real 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 x, y being Real 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 x, y being Real 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 holds cosh . (2 * x) = 1 + (2 * ((sinh . x) ^2))
proof end;

theorem Th70: :: SIN_COS7:70
for x being Real holds (cosh . x) ^2 = 1 + ((sinh . x) ^2)
proof end;

theorem Th71: :: SIN_COS7:71
for x being Real holds (sinh . x) ^2 = ((cosh . x) ^2) - 1
proof end;

theorem :: SIN_COS7:72
for x being Real 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 holds cosh (5 * x) = ((5 * (cosh x)) - (20 * ((cosh x) |^ 3))) + (16 * ((cosh x) |^ 5))
proof end;