:: by Fuguo Ge , Xiquan Liang and Yuzhong Ding

::

:: Received May 24, 2005

:: Copyright (c) 2005-2016 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;

Lm3: for x being Real st 1 <= x holds

(x ^2) - 1 >= 0

proof end;

Lm4: for x being Real st x ^2 < 1 holds

(x + 1) / (1 - x) > 0

proof end;

Lm5: for x being Real st 0 < x & x < 1 holds

0 < 1 - (x ^2)

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

0 <= (x * (sqrt ((y ^2) - 1))) + (y * (sqrt ((x ^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)))

0 <= (y * (sqrt ((x ^2) - 1))) - (x * (sqrt ((y ^2) - 1)))

proof end;

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

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;

:: deftheorem defines sinh" SIN_COS7:def 1 :

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

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

:: deftheorem defines cosh1" SIN_COS7:def 2 :

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

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

:: deftheorem defines cosh2" SIN_COS7:def 3 :

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

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

:: deftheorem defines tanh" SIN_COS7:def 4 :

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

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

:: deftheorem defines coth" SIN_COS7:def 5 :

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

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

:: deftheorem defines sech1" SIN_COS7:def 6 :

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

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

definition
end;

:: deftheorem defines sech2" SIN_COS7:def 7 :

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

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

definition

let x be Real;

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_{1} being Real st 0 < x & x < 0 holds

( b_{1} = log (number_e,((1 + (sqrt (1 + (x ^2)))) / x)) iff b_{1} = log (number_e,((1 - (sqrt (1 + (x ^2)))) / x)) );

;

end;
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 log (number_e,((1 + (sqrt (1 + (x ^2)))) / x)) if 0 < x

log (number_e,((1 - (sqrt (1 + (x ^2)))) / x)) if x < 0

;

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

( b

;

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

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

(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))))

(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))))

(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))))

(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))))

(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)))

(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)))

(tanh" x) - (tanh" y) = tanh" ((x - y) / (1 - (x * y)))

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

log (number_e,x) = cosh2" (((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))))

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

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

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

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

( 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))

x = log (number_e,((1 - (sqrt (1 + (y ^2)))) / y))

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;