:: Formulas And Identities of Inverse Hyperbolic Functions :: by Fuguo Ge , Xiquan Liang and Yuzhong Ding :: :: Received May 24, 2005 :: Copyright (c) 2005-2012 Association of Mizar Users begin Lm1: number_e <> 1 by TAYLOR_1:11; Lm2: for x, y being real number st x ^2 < 1 & y < 1 holds (x ^2) * y < 1 proofend; theorem Th1: :: SIN_COS7:1 for x being real number st x > 0 holds 1 / x = x to_power (- 1) proofend; theorem :: SIN_COS7:2 for x being real number st x > 1 holds ((sqrt ((x ^2) - 1)) / x) ^2 < 1 proofend; theorem :: SIN_COS7:3 for x being real number holds (x / (sqrt ((x ^2) + 1))) ^2 < 1 proofend; theorem Th4: :: SIN_COS7:4 for x being real number holds sqrt ((x ^2) + 1) > 0 proofend; theorem Th5: :: SIN_COS7:5 for x being real number holds (sqrt ((x ^2) + 1)) + x > 0 proofend; Lm3: for x being real number st 1 <= x holds (x ^2) - 1 >= 0 proofend; 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 proofend; theorem Th8: :: SIN_COS7:8 for x being real number st x >= 1 holds sqrt ((x + 1) / 2) >= 1 proofend; theorem Th9: :: SIN_COS7:9 for y, x being real number st y >= 0 & x >= 1 holds ((x ^2) - 1) / y >= 0 proofend; theorem Th10: :: SIN_COS7:10 for x being real number st x >= 1 holds (sqrt ((x + 1) / 2)) + (sqrt ((x - 1) / 2)) > 0 proofend; theorem Th11: :: SIN_COS7:11 for x being real number st x ^2 < 1 holds ( x + 1 > 0 & 1 - x > 0 ) proofend; Lm4: for x being real number st x ^2 < 1 holds (x + 1) / (1 - x) > 0 proofend; theorem Th12: :: SIN_COS7:12 for x being real number st x <> 1 holds (1 - x) ^2 > 0 proofend; theorem Th13: :: SIN_COS7:13 for x being real number st x ^2 < 1 holds ((x ^2) + 1) / (1 - (x ^2)) >= 0 proofend; theorem :: SIN_COS7:14 for x being real number st x ^2 < 1 holds ((2 * x) / (1 + (x ^2))) ^2 < 1 proofend; theorem Th15: :: SIN_COS7:15 for x being real number st 0 < x & x < 1 holds (1 + x) / (1 - x) > 0 proofend; theorem :: SIN_COS7:16 for x being real number st 0 < x & x < 1 holds x ^2 < 1 proofend; Lm5: for x being real number st 0 < x & x < 1 holds 0 < 1 - (x ^2) proofend; theorem :: SIN_COS7:17 for x being real number st 0 < x & x < 1 holds 1 / (sqrt (1 - (x ^2))) > 1 proofend; theorem Th18: :: SIN_COS7:18 for x being real number st 0 < x & x < 1 holds (2 * x) / (1 - (x ^2)) > 0 proofend; theorem Th19: :: SIN_COS7:19 for x being real number st 0 < x & x < 1 holds 0 < (1 - (x ^2)) ^2 proofend; theorem :: SIN_COS7:20 for x being real number st 0 < x & x < 1 holds (1 + (x ^2)) / (1 - (x ^2)) > 1 proofend; theorem :: SIN_COS7:21 for x being real number st 1 < x ^2 holds (1 / x) ^2 < 1 proofend; theorem Th22: :: SIN_COS7:22 for x being real number st 0 < x & x <= 1 holds 1 - (x ^2) >= 0 proofend; theorem Th23: :: SIN_COS7:23 for x being real number st 1 <= x holds 0 < x + (sqrt ((x ^2) - 1)) proofend; 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))) proofend; theorem Th25: :: SIN_COS7:25 for y being real number st 1 <= y holds 0 < y - (sqrt ((y ^2) - 1)) proofend; 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))) proofend; theorem Th27: :: SIN_COS7:27 for x, y being real number st x ^2 < 1 & y ^2 < 1 holds x * y <> - 1 proofend; theorem Th28: :: SIN_COS7:28 for x, y being real number st x ^2 < 1 & y ^2 < 1 holds x * y <> 1 proofend; theorem Th29: :: SIN_COS7:29 for x being real number st x <> 0 holds exp_R x <> 1 proofend; theorem Th30: :: SIN_COS7:30 for x being real number st 0 <> x holds ((exp_R x) ^2) - 1 <> 0 proofend; Lm6: for x being real number holds (x ^2) + 1 > 0 proofend; theorem Th31: :: SIN_COS7:31 for t being real number holds ((t ^2) - 1) / ((t ^2) + 1) < 1 proofend; theorem Th32: :: SIN_COS7:32 for t being real number st - 1 < t & t < 1 holds 0 < (t + 1) / (1 - t) proofend; Lm7: for t being real number st ( 1 < t or t < - 1 ) holds 0 < (t + 1) / (t - 1) proofend; Lm8: for x being real number holds sqrt ((x ^2) + 1) > x proofend; Lm9: for x, y being real number holds ((sqrt ((x ^2) + 1)) * (sqrt ((y ^2) + 1))) - (x * y) > 0 proofend; Lm10: for y being real number st 1 <= y holds y + (sqrt ((y ^2) - 1)) > 0 proofend; Lm11: for t being real number st 0 < t holds - 1 < ((t ^2) - 1) / ((t ^2) + 1) proofend; Lm12: 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 proofend; Lm13: for t being real number st 0 < t holds 0 < (2 * t) / (1 + (t ^2)) proofend; Lm14: for t being real number st 0 < t holds (2 * t) / (1 + (t ^2)) <= 1 proofend; Lm15: for t being real number st 0 < t holds (1 - (sqrt (1 + (t ^2)))) / t < 0 proofend; Lm16: for t being real number st 0 < t & t <= 1 holds 0 <= 1 - (t ^2) proofend; Lm17: for t being real number st 0 < t & t <= 1 holds 0 <= 4 - (4 * (t ^2)) proofend; Lm18: for t being real number st 0 < t & t <= 1 holds 0 < 1 + (sqrt (1 - (t ^2))) proofend; Lm19: for t being real number st 0 < t & t <= 1 holds 0 < (1 + (sqrt (1 - (t ^2)))) / t proofend; Lm20: for t being real number st 0 < t & t <> 1 holds (2 * t) / ((t ^2) - 1) <> 0 proofend; Lm21: for t being real number st t < 0 holds (1 + (sqrt (1 + (t ^2)))) / t < 0 proofend; begin 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 b1 being real number 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 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)) proofend; theorem :: SIN_COS7:34 for x being real number st x < 0 holds sinh" x = cosh2" (sqrt ((x ^2) + 1)) proofend; theorem :: SIN_COS7:35 for x being real number holds sinh" x = tanh" (x / (sqrt ((x ^2) + 1))) proofend; theorem :: SIN_COS7:36 for x being real number st x >= 1 holds cosh1" x = sinh" (sqrt ((x ^2) - 1)) proofend; theorem :: SIN_COS7:37 for x being real number st x > 1 holds cosh1" x = tanh" ((sqrt ((x ^2) - 1)) / x) proofend; theorem :: SIN_COS7:38 for x being real number st x >= 1 holds cosh1" x = 2 * (cosh1" (sqrt ((x + 1) / 2))) proofend; theorem :: SIN_COS7:39 for x being real number st x >= 1 holds cosh2" x = 2 * (cosh2" (sqrt ((x + 1) / 2))) proofend; theorem :: SIN_COS7:40 for x being real number st x >= 1 holds cosh1" x = 2 * (sinh" (sqrt ((x - 1) / 2))) proofend; theorem :: SIN_COS7:41 for x being real number st x ^2 < 1 holds tanh" x = sinh" (x / (sqrt (1 - (x ^2)))) proofend; theorem :: SIN_COS7:42 for x being real number st 0 < x & x < 1 holds tanh" x = cosh1" (1 / (sqrt (1 - (x ^2)))) proofend; theorem :: SIN_COS7:43 for x being real number st x ^2 < 1 holds tanh" x = (1 / 2) * (sinh" ((2 * x) / (1 - (x ^2)))) proofend; 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)))) proofend; theorem :: SIN_COS7:45 for x being real number st x ^2 < 1 holds tanh" x = (1 / 2) * (tanh" ((2 * x) / (1 + (x ^2)))) proofend; theorem :: SIN_COS7:46 for x being real number st x ^2 > 1 holds coth" x = tanh" (1 / x) proofend; theorem :: SIN_COS7:47 for x being real number st x > 0 & x <= 1 holds sech1" x = cosh1" (1 / x) proofend; theorem :: SIN_COS7:48 for x being real number st x > 0 & x <= 1 holds sech2" x = cosh2" (1 / x) proofend; theorem :: SIN_COS7:49 for x being real number st x > 0 holds csch" x = sinh" (1 / x) proofend; 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))))) proofend; 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))))) proofend; 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)))) proofend; 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)))) proofend; 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)))) proofend; 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)))) proofend; 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))) proofend; 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))) proofend; theorem :: SIN_COS7:58 for x being real number st 0 < x holds log (number_e,x) = 2 * (tanh" ((x - 1) / (x + 1))) proofend; theorem :: SIN_COS7:59 for x being real number st 0 < x holds log (number_e,x) = tanh" (((x ^2) - 1) / ((x ^2) + 1)) proofend; theorem :: SIN_COS7:60 for x being real number st 1 < x holds log (number_e,x) = cosh1" (((x ^2) + 1) / (2 * x)) proofend; 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)) proofend; theorem :: SIN_COS7:62 for x being real number st 0 < x holds log (number_e,x) = sinh" (((x ^2) - 1) / (2 * x)) proofend; 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)))) proofend; 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))))) proofend; 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)))) proofend; 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)))) proofend; 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))) ) proofend; 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)) proofend; theorem Th69: :: SIN_COS7:69 for x being real number holds cosh . (2 * x) = 1 + (2 * ((sinh . x) ^2)) proofend; theorem Th70: :: SIN_COS7:70 for x being real number holds (cosh . x) ^2 = 1 + ((sinh . x) ^2) proofend; theorem Th71: :: SIN_COS7:71 for x being real number holds (sinh . x) ^2 = ((cosh . x) ^2) - 1 proofend; theorem :: SIN_COS7:72 for x being real number holds sinh (5 * x) = ((5 * (sinh x)) + (20 * ((sinh x) |^ 3))) + (16 * ((sinh x) |^ 5)) proofend; theorem :: SIN_COS7:73 for x being real number holds cosh (5 * x) = ((5 * (cosh x)) - (20 * ((cosh x) |^ 3))) + (16 * ((cosh x) |^ 5)) proofend;