:: 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 b₁ being Real 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 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;