sin_cos7.miz
begin
reserve x,y,t for
Real;
Lm1:
number_e
<> 1 by
TAYLOR_1: 11;
Lm2: (x
^2 )
< 1 & y
< 1 implies ((x
^2 )
* y)
< 1
proof
assume that
A1: (x
^2 )
< 1 and
A2: y
< 1;
per cases by
XREAL_1: 63;
suppose
0
= (x
^2 );
hence thesis;
end;
suppose
0
< (x
^2 );
then (y
* (x
^2 ))
< (1
* (x
^2 )) by
A2,
XREAL_1: 68;
hence thesis by
A1,
XXREAL_0: 2;
end;
end;
theorem ::
SIN_COS7:1
Th1: x
>
0 implies (1
/ x)
= (x
to_power (
- 1))
proof
assume x
>
0 ;
then (x
to_power (
- 1))
= ((1
/ x)
to_power 1) by
POWER: 32
.= (1
/ x) by
POWER: 25;
hence thesis;
end;
theorem ::
SIN_COS7:2
x
> 1 implies (((
sqrt ((x
^2 )
- 1))
/ x)
^2 )
< 1
proof
A1: ((
- 1)
+ (x
^2 ))
< (
0
+ (x
^2 )) by
XREAL_1: 6;
assume x
> 1;
then (x
^2 )
> ((1
^2 )
+
0 ) by
SQUARE_1: 16;
then
A2: ((x
^2 )
- 1)
>
0 by
XREAL_1: 20;
(((
sqrt ((x
^2 )
- 1))
/ x)
^2 )
= (((
sqrt ((x
^2 )
- 1))
^2 )
/ (x
^2 )) by
XCMPLX_1: 76
.= (((x
^2 )
- 1)
/ (x
^2 )) by
A2,
SQUARE_1:def 2;
hence thesis by
A2,
A1,
XREAL_1: 189;
end;
theorem ::
SIN_COS7:3
((x
/ (
sqrt ((x
^2 )
+ 1)))
^2 )
< 1
proof
A1: (x
^2 )
< ((x
^2 )
+ 1) by
XREAL_1: 29;
A2: (x
^2 )
>=
0 by
XREAL_1: 63;
then ((
sqrt ((x
^2 )
+ 1))
^2 )
= (
sqrt (((x
^2 )
+ 1)
^2 )) by
SQUARE_1: 29
.= ((x
^2 )
+ 1) by
A2,
SQUARE_1: 22;
then
A3: ((x
/ (
sqrt ((x
^2 )
+ 1)))
^2 )
= ((x
^2 )
/ ((x
^2 )
+ 1)) by
XCMPLX_1: 76;
per cases by
XREAL_1: 63;
suppose (x
^2 )
>
0 ;
hence thesis by
A1,
A3,
XREAL_1: 189;
end;
suppose (x
^2 )
=
0 ;
hence thesis by
A3;
end;
end;
theorem ::
SIN_COS7:4
Th4: (
sqrt ((x
^2 )
+ 1))
>
0
proof
(x
^2 )
>=
0 by
XREAL_1: 63;
hence thesis by
SQUARE_1: 25;
end;
theorem ::
SIN_COS7:5
Th5: ((
sqrt ((x
^2 )
+ 1))
+ x)
>
0
proof
per cases ;
suppose x
>
0 ;
hence thesis by
Th4,
XREAL_1: 29;
end;
suppose
A1: x
<=
0 ;
(x
^2 )
< ((x
^2 )
+ 1) by
XREAL_1: 29;
then (
sqrt (x
^2 ))
< (
sqrt ((x
^2 )
+ 1)) by
SQUARE_1: 27,
XREAL_1: 63;
then (
- x)
< (
sqrt ((x
^2 )
+ 1)) by
A1,
SQUARE_1: 23;
hence thesis by
XREAL_1: 62;
end;
end;
Lm3: 1
<= x implies ((x
^2 )
- 1)
>=
0
proof
assume 1
<= x;
then (x
^2 )
>= (1
^2 ) by
SQUARE_1: 15;
then (1
+ (
- 1))
<= ((x
^2 )
+ (
- 1)) by
XREAL_1: 6;
hence thesis;
end;
theorem ::
SIN_COS7:6
y
>=
0 & x
>= 1 implies ((x
+ 1)
/ y)
>=
0 ;
theorem ::
SIN_COS7:7
Th7: y
>=
0 & x
>= 1 implies ((x
- 1)
/ y)
>=
0
proof
assume that
A1: y
>=
0 and
A2: x
>= 1;
(x
+ (
- 1))
>= (1
+ (
- 1)) by
A2,
XREAL_1: 6;
hence thesis by
A1;
end;
theorem ::
SIN_COS7:8
Th8: x
>= 1 implies (
sqrt ((x
+ 1)
/ 2))
>= 1
proof
assume x
>= 1;
then (x
+ 1)
>= (1
+ 1) by
XREAL_1: 6;
then ((x
+ 1)
/ 2)
>= 1 by
XREAL_1: 181;
hence thesis by
SQUARE_1: 18,
SQUARE_1: 26;
end;
theorem ::
SIN_COS7:9
Th9: y
>=
0 & x
>= 1 implies (((x
^2 )
- 1)
/ y)
>=
0
proof
assume that
A1: y
>=
0 and
A2: x
>= 1;
((x
^2 )
- 1)
>=
0 by
A2,
Lm3;
hence thesis by
A1;
end;
theorem ::
SIN_COS7:10
Th10: x
>= 1 implies ((
sqrt ((x
+ 1)
/ 2))
+ (
sqrt ((x
- 1)
/ 2)))
>
0
proof
assume
A1: x
>= 1;
then ((x
- 1)
/ 2)
>=
0 by
Th7;
then
A2: (
sqrt ((x
- 1)
/ 2))
>=
0 by
SQUARE_1: 17,
SQUARE_1: 26;
(
sqrt ((x
+ 1)
/ 2))
>= 1 by
A1,
Th8;
hence thesis by
A2;
end;
theorem ::
SIN_COS7:11
Th11: (x
^2 )
< 1 implies (x
+ 1)
>
0 & (1
- x)
>
0
proof
assume (x
^2 )
< 1;
then (
- 1)
< x & x
< 1 by
SQUARE_1: 52;
hence thesis by
XREAL_1: 148,
XREAL_1: 149;
end;
Lm4: (x
^2 )
< 1 implies ((x
+ 1)
/ (1
- x))
>
0
proof
assume (x
^2 )
< 1;
then (x
+ 1)
>
0 & (1
- x)
>
0 by
Th11;
hence thesis;
end;
theorem ::
SIN_COS7:12
Th12: x
<> 1 implies ((1
- x)
^2 )
>
0
proof
assume x
<> 1;
then
0
<> (1
- x);
hence thesis by
SQUARE_1: 12;
end;
theorem ::
SIN_COS7:13
Th13: (x
^2 )
< 1 implies (((x
^2 )
+ 1)
/ (1
- (x
^2 )))
>=
0
proof
assume (x
^2 )
< 1;
then
A1:
0
< (1
- (x
^2 )) by
XREAL_1: 50;
(x
^2 )
>=
0 by
XREAL_1: 63;
hence thesis by
A1;
end;
theorem ::
SIN_COS7:14
(x
^2 )
< 1 implies (((2
* x)
/ (1
+ (x
^2 )))
^2 )
< 1
proof
assume (x
^2 )
< 1;
then ((x
^2 )
+ (
- 1))
< (1
+ (
- 1)) by
XREAL_1: 8;
then (((x
^2 )
- 1)
* ((x
^2 )
- 1))
> (
0
* ((x
^2 )
- 1));
then
A1: (x
^2 )
>=
0 & (((((x
^2 )
^2 )
- (2
* (x
^2 )))
+ 1)
+ (4
* (x
^2 )))
> (
0
+ (4
* (x
^2 ))) by
XREAL_1: 8,
XREAL_1: 63;
(((2
* x)
/ (1
+ (x
^2 )))
^2 )
= (((2
* x)
^2 )
/ ((1
+ (x
^2 ))
^2 )) by
XCMPLX_1: 76
.= ((4
* (x
^2 ))
/ ((((x
^2 )
^2 )
+ (2
* (x
^2 )))
+ 1));
hence thesis by
A1,
XREAL_1: 189;
end;
theorem ::
SIN_COS7:15
Th15:
0
< x & x
< 1 implies ((1
+ x)
/ (1
- x))
>
0
proof
assume that
A1:
0
< x and
A2: x
< 1;
(x
^2 )
< x by
A1,
A2,
SQUARE_1: 13;
then (x
^2 )
< 1 by
A2,
XXREAL_0: 2;
hence thesis by
Lm4;
end;
theorem ::
SIN_COS7:16
0
< x & x
< 1 implies (x
^2 )
< 1
proof
assume that
A1:
0
< x and
A2: x
< 1;
(x
^2 )
< x by
A1,
A2,
SQUARE_1: 13;
hence thesis by
A2,
XXREAL_0: 2;
end;
Lm5:
0
< x & x
< 1 implies
0
< (1
- (x
^2 ))
proof
assume that
A1:
0
< x and
A2: x
< 1;
(x
^2 )
< x by
A1,
A2,
SQUARE_1: 13;
then (x
^2 )
< 1 by
A2,
XXREAL_0: 2;
then ((x
^2 )
- (x
^2 ))
< (1
- (x
^2 )) by
XREAL_1: 9;
hence thesis;
end;
theorem ::
SIN_COS7:17
0
< x & x
< 1 implies (1
/ (
sqrt (1
- (x
^2 ))))
> 1
proof
assume that
A1:
0
< x and
A2: x
< 1;
A3:
0
< (1
- (x
^2 )) by
A1,
A2,
Lm5;
then
A4:
0
< (
sqrt (1
- (x
^2 ))) by
SQUARE_1: 25;
(x
* x)
> (
0
* x) by
A1;
then ((x
^2 )
* (
- 1))
< (
0
* (
- 1));
then ((
- (x
^2 ))
+ 1)
< (
0
+ 1) by
XREAL_1: 8;
then (
sqrt (1
- (x
^2 )))
< 1 by
A3,
SQUARE_1: 18,
SQUARE_1: 27;
hence thesis by
A4,
XREAL_1: 187;
end;
theorem ::
SIN_COS7:18
Th18:
0
< x & x
< 1 implies ((2
* x)
/ (1
- (x
^2 )))
>
0
proof
assume that
A1:
0
< x and
A2: x
< 1;
(x
^2 )
< x by
A1,
A2,
SQUARE_1: 13;
then (x
^2 )
< 1 by
A2,
XXREAL_0: 2;
then
A3: ((x
^2 )
+ (
- (x
^2 )))
< (1
+ (
- (x
^2 ))) by
XREAL_1: 8;
(
0
* 2)
< (x
* 2) by
A1;
hence thesis by
A3;
end;
theorem ::
SIN_COS7:19
Th19:
0
< x & x
< 1 implies
0
< ((1
- (x
^2 ))
^2 )
proof
assume that
A1:
0
< x and
A2: x
< 1;
(x
^2 )
< x by
A1,
A2,
SQUARE_1: 13;
then (x
^2 )
< 1 by
A2,
XXREAL_0: 2;
then ((x
^2 )
+ (
- (x
^2 )))
< (1
+ (
- (x
^2 ))) by
XREAL_1: 8;
hence thesis;
end;
theorem ::
SIN_COS7:20
0
< x & x
< 1 implies ((1
+ (x
^2 ))
/ (1
- (x
^2 )))
> 1
proof
assume that
A1:
0
< x and
A2: x
< 1;
(x
^2 )
< x by
A1,
A2,
SQUARE_1: 13;
then (x
^2 )
< 1 by
A2,
XXREAL_0: 2;
then
A3: ((x
^2 )
+ (
- (x
^2 )))
< (1
+ (
- (x
^2 ))) by
XREAL_1: 8;
(
0
* x)
< (x
* x) by
A1;
then ((
- (x
^2 ))
+ 1)
< ((x
^2 )
+ 1) by
XREAL_1: 8;
hence thesis by
A3,
XREAL_1: 187;
end;
theorem ::
SIN_COS7:21
1
< (x
^2 ) implies ((1
/ x)
^2 )
< 1
proof
assume
A1: 1
< (x
^2 );
then (1
/ (x
^2 ))
< ((x
^2 )
/ (x
^2 )) by
XREAL_1: 74;
then ((1
^2 )
/ (x
^2 ))
< 1 by
A1,
XCMPLX_1: 60;
hence thesis by
XCMPLX_1: 76;
end;
theorem ::
SIN_COS7:22
Th22:
0
< x & x
<= 1 implies (1
- (x
^2 ))
>=
0
proof
assume that
A1:
0
< x and
A2: x
<= 1;
A3: (x
- 1)
<= (1
- 1) by
A2,
XREAL_1: 9;
per cases by
A3;
suppose (x
- 1)
<
0 ;
then ((x
- 1)
+ 1)
< (
0
+ 1) by
XREAL_1: 8;
hence thesis by
A1,
Lm5;
end;
suppose (x
- 1)
=
0 ;
hence thesis;
end;
end;
theorem ::
SIN_COS7:23
Th23: 1
<= x implies
0
< (x
+ (
sqrt ((x
^2 )
- 1)))
proof
assume
A1: 1
<= x;
then ((x
^2 )
- 1)
>=
0 by
Lm3;
then
0
<= (
sqrt ((x
^2 )
- 1)) by
SQUARE_1:def 2;
hence thesis by
A1;
end;
theorem ::
SIN_COS7:24
Th24: 1
<= x & 1
<= y implies
0
<= ((x
* (
sqrt ((y
^2 )
- 1)))
+ (y
* (
sqrt ((x
^2 )
- 1))))
proof
assume that
A1: 1
<= x and
A2: 1
<= y;
0
<= ((y
^2 )
- 1) by
A2,
Lm3;
then
A3:
0
<= (
sqrt ((y
^2 )
- 1)) by
SQUARE_1:def 2;
0
<= ((x
^2 )
- 1) by
A1,
Lm3;
then
0
<= (
sqrt ((x
^2 )
- 1)) by
SQUARE_1:def 2;
hence thesis by
A1,
A2,
A3;
end;
theorem ::
SIN_COS7:25
Th25: 1
<= y implies
0
< (y
- (
sqrt ((y
^2 )
- 1)))
proof
assume
A1: 1
<= y;
then (1
* y)
<= (y
* y) by
XREAL_1: 64;
then 1
<= (y
^2 ) by
A1,
XXREAL_0: 2;
then
A2: (1
- 1)
<= ((y
^2 )
- 1) by
XREAL_1: 13;
((
- 1)
+ (y
^2 ))
< (
0
+ (y
^2 )) by
XREAL_1: 8;
then (
sqrt ((y
^2 )
- 1))
< (
sqrt (y
^2 )) by
A2,
SQUARE_1: 27;
then (
sqrt ((y
^2 )
- 1))
< y by
A1,
SQUARE_1: 22;
then ((
sqrt ((y
^2 )
- 1))
- (
sqrt ((y
^2 )
- 1)))
< (y
- (
sqrt ((y
^2 )
- 1))) by
XREAL_1: 14;
hence thesis;
end;
theorem ::
SIN_COS7:26
Th26: 1
<= x & 1
<= y &
|.y.|
<=
|.x.| implies
0
<= ((y
* (
sqrt ((x
^2 )
- 1)))
- (x
* (
sqrt ((y
^2 )
- 1))))
proof
assume that
A1: 1
<= x and
A2: 1
<= y and
A3:
|.y.|
<=
|.x.|;
A4:
0
<= ((y
^2 )
- 1) by
A2,
Lm3;
A5: (
|.x.|
^2 )
= (x
^2 ) & (
|.y.|
^2 )
= (y
^2 ) by
COMPLEX1: 75;
1
<=
|.y.| by
A2,
ABSVALUE:def 1;
then (y
^2 )
<= (x
^2 ) by
A3,
A5,
SQUARE_1: 15;
then ((
- 1)
* (x
^2 ))
<= ((
- 1)
* (y
^2 )) by
XREAL_1: 65;
then ((
- (x
^2 ))
+ ((x
^2 )
* (y
^2 )))
<= ((
- (y
^2 ))
+ ((x
^2 )
* (y
^2 ))) by
XREAL_1: 6;
then
0
<= (x
^2 ) & (
sqrt ((x
^2 )
* ((y
^2 )
- 1)))
<= (
sqrt ((y
^2 )
* ((x
^2 )
- 1))) by
A1,
A4,
SQUARE_1: 26;
then ((
sqrt (x
^2 ))
* (
sqrt ((y
^2 )
- 1)))
<= (
sqrt ((y
^2 )
* ((x
^2 )
- 1))) by
A4,
SQUARE_1: 29;
then
A6: (x
* (
sqrt ((y
^2 )
- 1)))
<= (
sqrt ((y
^2 )
* ((x
^2 )
- 1))) by
A1,
SQUARE_1: 22;
0
<= (y
^2 ) &
0
<= ((x
^2 )
- 1) by
A1,
Lm3,
XREAL_1: 63;
then (x
* (
sqrt ((y
^2 )
- 1)))
<= ((
sqrt (y
^2 ))
* (
sqrt ((x
^2 )
- 1))) by
A6,
SQUARE_1: 29;
then (x
* (
sqrt ((y
^2 )
- 1)))
<= (y
* (
sqrt ((x
^2 )
- 1))) by
A2,
SQUARE_1: 22;
then ((x
* (
sqrt ((y
^2 )
- 1)))
- (x
* (
sqrt ((y
^2 )
- 1))))
<= ((y
* (
sqrt ((x
^2 )
- 1)))
- (x
* (
sqrt ((y
^2 )
- 1)))) by
XREAL_1: 13;
hence thesis;
end;
theorem ::
SIN_COS7:27
Th27: (x
^2 )
< 1 & (y
^2 )
< 1 implies (x
* y)
<> (
- 1)
proof
assume
A1: (x
^2 )
< 1 & (y
^2 )
< 1;
assume (x
* y)
= (
- 1);
then ((x
* y)
* (x
* y))
= 1;
then ((x
* x)
* (y
* y))
= 1;
hence contradiction by
A1,
Lm2;
end;
theorem ::
SIN_COS7:28
Th28: (x
^2 )
< 1 & (y
^2 )
< 1 implies (x
* y)
<> 1
proof
assume
A1: (x
^2 )
< 1 & (y
^2 )
< 1;
assume (x
* y)
= 1;
then ((x
* y)
* (x
* y))
= 1;
then ((x
* x)
* (y
* y))
= 1;
hence contradiction by
A1,
Lm2;
end;
theorem ::
SIN_COS7:29
Th29: x
<>
0 implies (
exp_R x)
<> 1
proof
assume
A1: x
<>
0 ;
assume
A2: (
exp_R x)
= 1;
x
= (
log (
number_e ,(
exp_R x))) by
TAYLOR_1: 12
.=
0 by
A2,
Lm1,
POWER: 51,
TAYLOR_1: 11;
hence contradiction by
A1;
end;
theorem ::
SIN_COS7:30
Th30:
0
<> x implies (((
exp_R x)
^2 )
- 1)
<>
0
proof
assume
A1:
0
<> x;
assume (((
exp_R x)
^2 )
- 1)
=
0 ;
then (
exp_R x)
= 1 or (
exp_R x)
= (
- 1) by
XCMPLX_1: 182;
hence contradiction by
A1,
Th29,
SIN_COS: 55;
end;
Lm6: ((x
^2 )
+ 1)
>
0
proof
(x
^2 )
>=
0 by
XREAL_1: 63;
hence thesis;
end;
theorem ::
SIN_COS7:31
Th31: (((t
^2 )
- 1)
/ ((t
^2 )
+ 1))
< 1
proof
A1:
0
< ((t
^2 )
+ 1) by
Lm6;
((
- 1)
+ (t
^2 ))
< (1
+ (t
^2 )) by
XREAL_1: 8;
then (((
- 1)
+ (t
^2 ))
/ (1
+ (t
^2 )))
< ((1
+ (t
^2 ))
/ (1
+ (t
^2 ))) by
A1,
XREAL_1: 74;
hence thesis by
A1,
XCMPLX_1: 60;
end;
theorem ::
SIN_COS7:32
Th32: (
- 1)
< t & t
< 1 implies
0
< ((t
+ 1)
/ (1
- t))
proof
assume (
- 1)
< t & t
< 1;
then ((
- 1)
+ 1)
< (t
+ 1) & (t
- t)
< (1
- t) by
XREAL_1: 8;
then (
0
/ (1
- t))
< ((t
+ 1)
/ (1
- t));
hence thesis;
end;
Lm7: 1
< t or t
< (
- 1) implies
0
< ((t
+ 1)
/ (t
- 1))
proof
assume
A1: 1
< t or t
< (
- 1);
per cases by
A1;
suppose
A2: 1
< t;
then (1
- 1)
< (t
- 1) by
XREAL_1: 14;
then (
0
/ (t
- 1))
< ((t
+ 1)
/ (t
- 1)) by
A2;
hence thesis;
end;
suppose
A3: t
< (
- 1);
then (t
+ 1)
< ((
- 1)
+ 1) by
XREAL_1: 8;
then (
0
/ (t
- 1))
< ((t
+ 1)
/ (t
- 1)) by
A3;
hence thesis;
end;
end;
Lm8: (
sqrt ((x
^2 )
+ 1))
> x
proof
per cases ;
suppose
A1: x
>=
0 ;
((x
^2 )
+ 1)
> ((x
^2 )
+
0 ) by
XREAL_1: 8;
then (
sqrt ((x
^2 )
+ 1))
> (
sqrt (x
^2 )) by
SQUARE_1: 27,
XREAL_1: 63;
hence thesis by
A1,
SQUARE_1: 22;
end;
suppose x
<
0 ;
hence thesis by
Th4;
end;
end;
Lm9: (((
sqrt ((x
^2 )
+ 1))
* (
sqrt ((y
^2 )
+ 1)))
- (x
* y))
>
0
proof
A1: ((y
^2 )
+ 1)
>
0 by
Lm6;
assume (((
sqrt ((x
^2 )
+ 1))
* (
sqrt ((y
^2 )
+ 1)))
- (x
* y))
<=
0 ;
then
A2: ((
sqrt ((x
^2 )
+ 1))
* (
sqrt ((y
^2 )
+ 1)))
<= (x
* y) by
XREAL_1: 50;
(
sqrt ((x
^2 )
+ 1))
>
0 & (
sqrt ((y
^2 )
+ 1))
>
0 by
Th4;
then (((
sqrt ((x
^2 )
+ 1))
* (
sqrt ((y
^2 )
+ 1)))
^2 )
<= ((x
* y)
^2 ) by
A2,
SQUARE_1: 15;
then
A3: (((
sqrt ((x
^2 )
+ 1))
^2 )
* ((
sqrt ((y
^2 )
+ 1))
^2 ))
<= ((x
* y)
^2 );
((x
^2 )
+ 1)
>
0 by
Lm6;
then (((x
^2 )
+ 1)
* ((
sqrt ((y
^2 )
+ 1))
^2 ))
<= ((x
* y)
^2 ) by
A3,
SQUARE_1:def 2;
then (((x
^2 )
+ 1)
* ((y
^2 )
+ 1))
<= ((x
* y)
^2 ) by
A1,
SQUARE_1:def 2;
then
A4: ((((((x
* y)
^2 )
+ (x
^2 ))
+ (y
^2 ))
+ 1)
- ((x
* y)
^2 ))
<= (((x
* y)
^2 )
- ((x
* y)
^2 )) by
XREAL_1: 13;
0
<= (x
^2 ) &
0
<= (y
^2 ) by
XREAL_1: 63;
then (
0
+ 1)
<= (((x
^2 )
+ (y
^2 ))
+ 1) by
XREAL_1: 6;
hence contradiction by
A4;
end;
Lm10: 1
<= y implies (y
+ (
sqrt ((y
^2 )
- 1)))
>
0
proof
assume
A1: 1
<= y;
then
0
<= ((y
^2 )
- 1) by
Lm3;
then
0
<= (
sqrt ((y
^2 )
- 1)) by
SQUARE_1:def 2;
hence thesis by
A1;
end;
Lm11:
0
< t implies (
- 1)
< (((t
^2 )
- 1)
/ ((t
^2 )
+ 1))
proof
A1:
0
< ((t
^2 )
+ 1) by
Lm6;
assume
0
< t;
then
0
< (t
^2 );
then (
0
* 2)
< (2
* (t
^2 ));
then (
0
- ((t
^2 )
+ 1))
< ((2
* (t
^2 ))
- ((t
^2 )
+ 1)) by
XREAL_1: 14;
then ((
- ((t
^2 )
+ 1))
/ ((t
^2 )
+ 1))
< (((t
^2 )
- 1)
/ ((t
^2 )
+ 1)) by
A1,
XREAL_1: 74;
then (
- (((t
^2 )
+ 1)
/ ((t
^2 )
+ 1)))
< (((t
^2 )
- 1)
/ ((t
^2 )
+ 1));
hence thesis by
A1,
XCMPLX_1: 60;
end;
Lm12:
0
< t & t
<> 1 implies 1
< (((t
^2 )
+ 1)
/ ((t
^2 )
- 1)) or (((t
^2 )
+ 1)
/ ((t
^2 )
- 1))
< (
- 1)
proof
assume that
A1:
0
< t and
A2: t
<> 1;
1
< t or t
< 1 by
A2,
XXREAL_0: 1;
then
A3: (1
- 1)
< (t
- 1) or (t
- 1)
< (1
- 1) by
XREAL_1: 14;
per cases by
A3;
suppose
0
< (t
- 1);
then
A4: (
0
+ 1)
< ((t
- 1)
+ 1) by
XREAL_1: 8;
then t
< (t
^2 ) by
SQUARE_1: 14;
then 1
< (t
^2 ) by
A4,
XXREAL_0: 2;
then
A5: (1
- 1)
< ((t
^2 )
- 1) by
XREAL_1: 14;
((
- 1)
+ (t
^2 ))
< (1
+ (t
^2 )) by
XREAL_1: 8;
hence thesis by
A5,
XREAL_1: 187;
end;
suppose (t
- 1)
<
0 ;
then
A6: ((t
- 1)
+ 1)
< (
0
+ 1) by
XREAL_1: 8;
then (t
^2 )
< t by
A1,
SQUARE_1: 13;
then (t
^2 )
< 1 by
A6,
XXREAL_0: 2;
then
A7: ((t
^2 )
- (t
^2 ))
< (1
- (t
^2 )) by
XREAL_1: 14;
0
< (t
^2 ) by
A1;
then ((
- (t
^2 ))
+ 1)
< ((t
^2 )
+ 1) by
XREAL_1: 8;
then 1
< (((t
^2 )
+ 1)
/ (1
- (t
^2 ))) by
A7,
XREAL_1: 187;
then ((
- 1)
* (((t
^2 )
+ 1)
/ (1
- (t
^2 ))))
< (1
* (
- 1)) by
XREAL_1: 69;
then ((
- ((t
^2 )
+ 1))
/ (1
- (t
^2 )))
< (1
* (
- 1));
then (((t
^2 )
+ 1)
/ (
- (1
- (t
^2 ))))
< (1
* (
- 1)) by
XCMPLX_1: 192;
hence thesis;
end;
end;
Lm13:
0
< t implies
0
< ((2
* t)
/ (1
+ (t
^2 )));
Lm14:
0
< t implies ((2
* t)
/ (1
+ (t
^2 )))
<= 1
proof
0
<= ((t
- 1)
^2 ) by
XREAL_1: 63;
then
A1: (
0
+ (2
* t))
<= ((((t
^2 )
- (2
* t))
+ 1)
+ (2
* t)) by
XREAL_1: 6;
assume
0
< t;
hence thesis by
A1,
XREAL_1: 183;
end;
Lm15:
0
< t implies ((1
- (
sqrt (1
+ (t
^2 ))))
/ t)
<
0
proof
assume
A1:
0
< t;
then (
0
+ 1)
< ((t
^2 )
+ 1) by
XREAL_1: 8;
then 1
< (
sqrt ((t
^2 )
+ 1)) by
SQUARE_1: 18,
SQUARE_1: 27;
then (
- (
sqrt ((t
^2 )
+ 1)))
< (
- 1) by
XREAL_1: 24;
then ((
- (
sqrt ((t
^2 )
+ 1)))
+ 1)
< ((
- 1)
+ 1) by
XREAL_1: 8;
then ((1
- (
sqrt ((t
^2 )
+ 1)))
/ t)
< (
0
/ t) by
A1;
hence thesis;
end;
Lm16:
0
< t & t
<= 1 implies
0
<= (1
- (t
^2 ))
proof
assume
0
< t & t
<= 1;
then (t
^2 )
<= (1
^2 ) by
SQUARE_1: 15;
then ((t
^2 )
- (t
^2 ))
<= (1
- (t
^2 )) by
XREAL_1: 13;
hence thesis;
end;
Lm17:
0
< t & t
<= 1 implies
0
<= (4
- (4
* (t
^2 )))
proof
assume
0
< t & t
<= 1;
then
0
<= (1
- (t
^2 )) by
Lm16;
then (
0
* 4)
<= (4
* (1
- (t
^2 )));
hence thesis;
end;
Lm18:
0
< t & t
<= 1 implies
0
< (1
+ (
sqrt (1
- (t
^2 ))))
proof
assume
0
< t & t
<= 1;
then
0
<= (1
- (t
^2 )) by
Lm16;
then
0
<= (
sqrt (1
- (t
^2 ))) by
SQUARE_1: 17,
SQUARE_1: 26;
hence thesis;
end;
Lm19:
0
< t & t
<= 1 implies
0
< ((1
+ (
sqrt (1
- (t
^2 ))))
/ t)
proof
assume that
A1:
0
< t and
A2: t
<= 1;
0
< (1
+ (
sqrt (1
- (t
^2 )))) by
A1,
A2,
Lm18;
then (
0
/ t)
< ((1
+ (
sqrt (1
- (t
^2 ))))
/ t) by
A1;
hence thesis;
end;
Lm20:
0
< t & t
<> 1 implies ((2
* t)
/ ((t
^2 )
- 1))
<>
0
proof
assume that
A1:
0
< t and
A2: t
<> 1;
per cases by
A2,
XXREAL_0: 1;
suppose
A3: 1
< t;
then t
< (t
^2 ) by
SQUARE_1: 14;
then 1
< (t
^2 ) by
A3,
XXREAL_0: 2;
then
A4: (1
- 1)
< ((t
^2 )
- 1) by
XREAL_1: 14;
(2
* 1)
< (2
* t) by
A3,
XREAL_1: 68;
then (
0
/ ((t
^2 )
- 1))
< ((2
* t)
/ ((t
^2 )
- 1)) by
A4;
hence thesis;
end;
suppose
A5: t
< 1;
then (t
^2 )
< t by
A1,
SQUARE_1: 13;
then (t
^2 )
< 1 by
A5,
XXREAL_0: 2;
then
A6: ((t
^2 )
- 1)
< (1
- 1) by
XREAL_1: 14;
(
0
* 2)
< (2
* t) by
A1;
then ((2
* t)
/ ((t
^2 )
- 1))
< (
0
/ ((t
^2 )
- 1)) by
A6;
hence thesis;
end;
end;
Lm21: t
<
0 implies ((1
+ (
sqrt (1
+ (t
^2 ))))
/ t)
<
0
proof
assume
A1: t
<
0 ;
(
0
+ 1)
< ((
sqrt (1
+ (t
^2 )))
+ 1) by
Th4,
XREAL_1: 8;
then ((1
+ (
sqrt (1
+ (t
^2 ))))
/ t)
< (
0
/ t) by
A1;
hence thesis;
end;
begin
definition
let x be
Real;
::
SIN_COS7:def1
func
sinh" (x) ->
Real equals (
log (
number_e ,(x
+ (
sqrt ((x
^2 )
+ 1)))));
coherence ;
end
definition
let x be
Real;
::
SIN_COS7:def2
func
cosh1" (x) ->
Real equals (
log (
number_e ,(x
+ (
sqrt ((x
^2 )
- 1)))));
coherence ;
end
definition
let x be
Real;
::
SIN_COS7:def3
func
cosh2" (x) ->
Real equals (
- (
log (
number_e ,(x
+ (
sqrt ((x
^2 )
- 1))))));
coherence ;
end
definition
let x be
Real;
::
SIN_COS7:def4
func
tanh" (x) ->
Real equals ((1
/ 2)
* (
log (
number_e ,((1
+ x)
/ (1
- x)))));
coherence ;
end
definition
let x be
Real;
::
SIN_COS7:def5
func
coth" (x) ->
Real equals ((1
/ 2)
* (
log (
number_e ,((x
+ 1)
/ (x
- 1)))));
coherence ;
end
definition
let x be
Real;
::
SIN_COS7:def6
func
sech1" (x) ->
Real equals (
log (
number_e ,((1
+ (
sqrt (1
- (x
^2 ))))
/ x)));
coherence ;
end
definition
let x be
Real;
::
SIN_COS7:def7
func
sech2" (x) ->
Real equals (
- (
log (
number_e ,((1
+ (
sqrt (1
- (x
^2 ))))
/ x))));
coherence ;
end
definition
let x be
Real;
::
SIN_COS7:def8
func
csch" (x) ->
Real equals
:
Def8: (
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 ;
end
theorem ::
SIN_COS7:33
0
<= x implies (
sinh" x)
= (
cosh1" (
sqrt ((x
^2 )
+ 1)))
proof
assume
A1:
0
<= x;
(x
^2 )
>=
0 by
XREAL_1: 63;
then (
cosh1" (
sqrt ((x
^2 )
+ 1)))
= (
log (
number_e ,((
sqrt ((x
^2 )
+ 1))
+ (
sqrt (((x
^2 )
+ 1)
- 1))))) by
SQUARE_1:def 2
.= (
log (
number_e ,((
sqrt ((x
^2 )
+ 1))
+ x))) by
A1,
SQUARE_1: 22;
hence thesis;
end;
theorem ::
SIN_COS7:34
x
<
0 implies (
sinh" x)
= (
cosh2" (
sqrt ((x
^2 )
+ 1)))
proof
assume
A1: x
<
0 ;
A2: ((
sqrt ((x
^2 )
+ 1))
+ x)
>
0 by
Th5;
A3: (1
/ ((
sqrt ((x
^2 )
+ 1))
+ x))
= (((
sqrt ((x
^2 )
+ 1))
+ x)
to_power (
- 1)) by
Th1,
Th5;
A4: (x
^2 )
>=
0 by
XREAL_1: 63;
then (
cosh2" (
sqrt ((x
^2 )
+ 1)))
= (
- (
log (
number_e ,((
sqrt ((x
^2 )
+ 1))
+ (
sqrt (((x
^2 )
+ 1)
- 1)))))) by
SQUARE_1:def 2
.= (
- (
log (
number_e ,((
sqrt ((x
^2 )
+ 1))
+ (
- x))))) by
A1,
SQUARE_1: 23
.= (
- (
log (
number_e ,((((
sqrt ((x
^2 )
+ 1))
- x)
* ((
sqrt ((x
^2 )
+ 1))
+ x))
/ ((
sqrt ((x
^2 )
+ 1))
+ x))))) by
A2,
XCMPLX_1: 89
.= (
- (
log (
number_e ,((((
sqrt ((x
^2 )
+ 1))
^2 )
- (x
^2 ))
/ ((
sqrt ((x
^2 )
+ 1))
+ x)))))
.= (
- (
log (
number_e ,((((x
^2 )
+ 1)
- (x
^2 ))
/ ((
sqrt ((x
^2 )
+ 1))
+ x))))) by
A4,
SQUARE_1:def 2
.= (
- ((
- 1)
* (
log (
number_e ,((
sqrt ((x
^2 )
+ 1))
+ x))))) by
A2,
A3,
Lm1,
POWER: 55,
TAYLOR_1: 11
.= (
log (
number_e ,((
sqrt ((x
^2 )
+ 1))
+ x)));
hence thesis;
end;
theorem ::
SIN_COS7:35
(
sinh" x)
= (
tanh" (x
/ (
sqrt ((x
^2 )
+ 1))))
proof
set t = ((
sqrt ((x
^2 )
+ 1))
+ x);
A1: ((
sqrt ((x
^2 )
+ 1))
+ x)
>
0 by
Th5;
A2: ((x
^2 )
+ 1)
>
0 by
Lm6;
A3: (
sqrt ((x
^2 )
+ 1))
>
0 by
Th4;
then (
tanh" (x
/ (
sqrt ((x
^2 )
+ 1))))
= ((1
/ 2)
* (
log (
number_e ,(((((
sqrt ((x
^2 )
+ 1))
* 1)
+ x)
/ (
sqrt ((x
^2 )
+ 1)))
/ (1
- (x
/ (
sqrt ((x
^2 )
+ 1)))))))) by
XCMPLX_1: 113
.= ((1
/ 2)
* (
log (
number_e ,(((((
sqrt ((x
^2 )
+ 1))
* 1)
+ x)
/ (
sqrt ((x
^2 )
+ 1)))
/ (((1
* (
sqrt ((x
^2 )
+ 1)))
- x)
/ (
sqrt ((x
^2 )
+ 1))))))) by
A3,
XCMPLX_1: 127
.= ((1
/ 2)
* (
log (
number_e ,(t
/ ((
sqrt ((x
^2 )
+ 1))
- x))))) by
A3,
XCMPLX_1: 55
.= ((1
/ 2)
* (
log (
number_e ,((t
* t)
/ (((
sqrt ((x
^2 )
+ 1))
- x)
* t))))) by
A1,
XCMPLX_1: 91
.= ((1
/ 2)
* (
log (
number_e ,((t
* t)
/ (((
sqrt ((x
^2 )
+ 1))
* (
sqrt ((x
^2 )
+ 1)))
- (x
^2 ))))))
.= ((1
/ 2)
* (
log (
number_e ,((t
* t)
/ ((
sqrt (((x
^2 )
+ 1)
^2 ))
- (x
^2 )))))) by
A2,
SQUARE_1: 29
.= ((1
/ 2)
* (
log (
number_e ,((t
* t)
/ (((x
^2 )
+ 1)
- (x
^2 )))))) by
A2,
SQUARE_1: 22
.= ((1
/ 2)
* (
log (
number_e ,(t
^2 ))))
.= ((1
/ 2)
* (
log (
number_e ,(t
to_power 2)))) by
POWER: 46
.= ((1
/ 2)
* (2
* (
log (
number_e ,t)))) by
A1,
Lm1,
POWER: 55,
TAYLOR_1: 11
.= (
log (
number_e ,t));
hence thesis;
end;
theorem ::
SIN_COS7:36
x
>= 1 implies (
cosh1" x)
= (
sinh" (
sqrt ((x
^2 )
- 1)))
proof
assume
A1: x
>= 1;
then ((x
^2 )
- 1)
>=
0 by
Lm3;
then (
sinh" (
sqrt ((x
^2 )
- 1)))
= (
log (
number_e ,((
sqrt ((x
^2 )
- 1))
+ (
sqrt (((x
^2 )
- 1)
+ 1))))) by
SQUARE_1:def 2
.= (
log (
number_e ,((
sqrt ((x
^2 )
- 1))
+ x))) by
A1,
SQUARE_1: 22;
hence thesis;
end;
theorem ::
SIN_COS7:37
x
> 1 implies (
cosh1" x)
= (
tanh" ((
sqrt ((x
^2 )
- 1))
/ x))
proof
assume
A1: x
> 1;
then
A2: ((
sqrt ((x
^2 )
- 1))
+ x)
>
0 by
Th23;
(x
^2 )
> ((1
^2 )
+
0 ) by
A1,
SQUARE_1: 16;
then
A3: ((x
^2 )
- 1)
>
0 by
XREAL_1: 20;
(
tanh" ((
sqrt ((x
^2 )
- 1))
/ x))
= ((1
/ 2)
* (
log (
number_e ,((((
sqrt ((x
^2 )
- 1))
+ (x
* 1))
/ x)
/ (1
- ((
sqrt ((x
^2 )
- 1))
/ x)))))) by
A1,
XCMPLX_1: 113
.= ((1
/ 2)
* (
log (
number_e ,((((
sqrt ((x
^2 )
- 1))
+ x)
/ x)
/ (((1
* x)
- (
sqrt ((x
^2 )
- 1)))
/ x))))) by
A1,
XCMPLX_1: 127
.= ((1
/ 2)
* (
log (
number_e ,(((
sqrt ((x
^2 )
- 1))
+ x)
/ (x
- (
sqrt ((x
^2 )
- 1))))))) by
A1,
XCMPLX_1: 55
.= ((1
/ 2)
* (
log (
number_e ,((((
sqrt ((x
^2 )
- 1))
+ x)
* ((
sqrt ((x
^2 )
- 1))
+ x))
/ ((x
- (
sqrt ((x
^2 )
- 1)))
* ((
sqrt ((x
^2 )
- 1))
+ x)))))) by
A2,
XCMPLX_1: 91
.= ((1
/ 2)
* (
log (
number_e ,((((
sqrt ((x
^2 )
- 1))
+ x)
* ((
sqrt ((x
^2 )
- 1))
+ x))
/ ((x
^2 )
- ((
sqrt ((x
^2 )
- 1))
^2 ))))))
.= ((1
/ 2)
* (
log (
number_e ,((((
sqrt ((x
^2 )
- 1))
+ x)
* ((
sqrt ((x
^2 )
- 1))
+ x))
/ ((x
^2 )
- ((x
^2 )
- 1)))))) by
A3,
SQUARE_1:def 2
.= ((1
/ 2)
* (
log (
number_e ,(((
sqrt ((x
^2 )
- 1))
+ x)
^2 ))))
.= ((1
/ 2)
* (
log (
number_e ,(((
sqrt ((x
^2 )
- 1))
+ x)
to_power 2)))) by
POWER: 46
.= ((1
/ 2)
* (2
* (
log (
number_e ,((
sqrt ((x
^2 )
- 1))
+ x))))) by
A2,
Lm1,
POWER: 55,
TAYLOR_1: 11
.= (
log (
number_e ,((
sqrt ((x
^2 )
- 1))
+ x)));
hence thesis;
end;
theorem ::
SIN_COS7:38
x
>= 1 implies (
cosh1" x)
= (2
* (
cosh1" (
sqrt ((x
+ 1)
/ 2))))
proof
assume
A1: x
>= 1;
then
A2: ((x
- 1)
/ 2)
>=
0 by
Th7;
A3: (((x
^2 )
- 1)
/ 4)
>=
0 by
A1,
Th9;
A4: ((
sqrt ((x
+ 1)
/ 2))
+ (
sqrt ((x
- 1)
/ 2)))
>
0 by
A1,
Th10;
(2
* (
cosh1" (
sqrt ((x
+ 1)
/ 2))))
= (2
* (
log (
number_e ,((
sqrt ((x
+ 1)
/ 2))
+ (
sqrt (((x
+ 1)
/ 2)
- 1)))))) by
A1,
SQUARE_1:def 2
.= (
log (
number_e ,(((
sqrt ((x
+ 1)
/ 2))
+ (
sqrt ((x
- 1)
/ 2)))
to_power 2))) by
A4,
Lm1,
POWER: 55,
TAYLOR_1: 11
.= (
log (
number_e ,(((
sqrt ((x
+ 1)
/ 2))
+ (
sqrt ((x
- 1)
/ 2)))
^2 ))) by
POWER: 46
.= (
log (
number_e ,((((
sqrt ((x
+ 1)
/ 2))
^2 )
+ ((2
* (
sqrt ((x
+ 1)
/ 2)))
* (
sqrt ((x
- 1)
/ 2))))
+ ((
sqrt ((x
- 1)
/ 2))
^2 ))))
.= (
log (
number_e ,((((x
+ 1)
/ 2)
+ ((2
* (
sqrt ((x
+ 1)
/ 2)))
* (
sqrt ((x
- 1)
/ 2))))
+ ((
sqrt ((x
- 1)
/ 2))
^2 )))) by
A1,
SQUARE_1:def 2
.= (
log (
number_e ,((((x
+ 1)
/ 2)
+ ((2
* (
sqrt ((x
+ 1)
/ 2)))
* (
sqrt ((x
- 1)
/ 2))))
+ ((x
- 1)
/ 2)))) by
A2,
SQUARE_1:def 2
.= (
log (
number_e ,(x
+ (2
* ((
sqrt ((x
+ 1)
/ 2))
* (
sqrt ((x
- 1)
/ 2)))))))
.= (
log (
number_e ,(x
+ (2
* (
sqrt (((x
+ 1)
/ 2)
* ((x
- 1)
/ 2))))))) by
A1,
A2,
SQUARE_1: 29
.= (
log (
number_e ,(x
+ ((
sqrt (2
^2 ))
* (
sqrt (((x
^2 )
- 1)
/ 4)))))) by
SQUARE_1: 22
.= (
log (
number_e ,(x
+ (
sqrt (4
* (((x
^2 )
- 1)
/ 4)))))) by
A3,
SQUARE_1: 29
.= (
log (
number_e ,(x
+ (
sqrt ((x
^2 )
- 1)))));
hence thesis;
end;
theorem ::
SIN_COS7:39
x
>= 1 implies (
cosh2" x)
= (2
* (
cosh2" (
sqrt ((x
+ 1)
/ 2))))
proof
assume
A1: x
>= 1;
then
A2: ((x
- 1)
/ 2)
>=
0 by
Th7;
A3: (((x
^2 )
- 1)
/ 4)
>=
0 by
A1,
Th9;
A4: ((
sqrt ((x
+ 1)
/ 2))
+ (
sqrt ((x
- 1)
/ 2)))
>
0 by
A1,
Th10;
(2
* (
cosh2" (
sqrt ((x
+ 1)
/ 2))))
= (2
* (
- (
log (
number_e ,((
sqrt ((x
+ 1)
/ 2))
+ (
sqrt (((x
+ 1)
/ 2)
- 1))))))) by
A1,
SQUARE_1:def 2
.= (
- (2
* (
log (
number_e ,((
sqrt ((x
+ 1)
/ 2))
+ (
sqrt ((x
- 1)
/ 2)))))))
.= (
- (
log (
number_e ,(((
sqrt ((x
+ 1)
/ 2))
+ (
sqrt ((x
- 1)
/ 2)))
to_power 2)))) by
A4,
Lm1,
POWER: 55,
TAYLOR_1: 11
.= (
- (
log (
number_e ,(((
sqrt ((x
+ 1)
/ 2))
+ (
sqrt ((x
- 1)
/ 2)))
^2 )))) by
POWER: 46
.= (
- (
log (
number_e ,((((
sqrt ((x
+ 1)
/ 2))
^2 )
+ ((2
* (
sqrt ((x
+ 1)
/ 2)))
* (
sqrt ((x
- 1)
/ 2))))
+ ((
sqrt ((x
- 1)
/ 2))
^2 )))))
.= (
- (
log (
number_e ,((((x
+ 1)
/ 2)
+ ((2
* (
sqrt ((x
+ 1)
/ 2)))
* (
sqrt ((x
- 1)
/ 2))))
+ ((
sqrt ((x
- 1)
/ 2))
^2 ))))) by
A1,
SQUARE_1:def 2
.= (
- (
log (
number_e ,((((x
+ 1)
/ 2)
+ ((2
* (
sqrt ((x
+ 1)
/ 2)))
* (
sqrt ((x
- 1)
/ 2))))
+ ((x
- 1)
/ 2))))) by
A2,
SQUARE_1:def 2
.= (
- (
log (
number_e ,(x
+ (2
* ((
sqrt ((x
+ 1)
/ 2))
* (
sqrt ((x
- 1)
/ 2))))))))
.= (
- (
log (
number_e ,(x
+ (2
* (
sqrt (((x
+ 1)
/ 2)
* ((x
- 1)
/ 2)))))))) by
A1,
A2,
SQUARE_1: 29
.= (
- (
log (
number_e ,(x
+ ((
sqrt (2
^2 ))
* (
sqrt (((x
^2 )
- 1)
/ 4))))))) by
SQUARE_1: 22
.= (
- (
log (
number_e ,(x
+ (
sqrt (4
* (((x
^2 )
- 1)
/ 4))))))) by
A3,
SQUARE_1: 29
.= (
- (
log (
number_e ,(x
+ (
sqrt ((x
^2 )
- 1))))));
hence thesis;
end;
theorem ::
SIN_COS7:40
x
>= 1 implies (
cosh1" x)
= (2
* (
sinh" (
sqrt ((x
- 1)
/ 2))))
proof
assume
A1: x
>= 1;
then
A2: ((
sqrt ((x
+ 1)
/ 2))
+ (
sqrt ((x
- 1)
/ 2)))
>
0 by
Th10;
A3: (((x
^2 )
- 1)
/ 4)
>=
0 by
A1,
Th9;
A4: ((x
- 1)
/ 2)
>=
0 by
A1,
Th7;
then (2
* (
sinh" (
sqrt ((x
- 1)
/ 2))))
= (2
* (
log (
number_e ,((
sqrt ((x
- 1)
/ 2))
+ (
sqrt (((x
- 1)
/ 2)
+ 1)))))) by
SQUARE_1:def 2
.= (
log (
number_e ,(((
sqrt ((x
- 1)
/ 2))
+ (
sqrt ((x
+ 1)
/ 2)))
to_power 2))) by
A2,
Lm1,
POWER: 55,
TAYLOR_1: 11
.= (
log (
number_e ,(((
sqrt ((x
- 1)
/ 2))
+ (
sqrt ((x
+ 1)
/ 2)))
^2 ))) by
POWER: 46
.= (
log (
number_e ,((((
sqrt ((x
- 1)
/ 2))
^2 )
+ ((2
* (
sqrt ((x
- 1)
/ 2)))
* (
sqrt ((x
+ 1)
/ 2))))
+ ((
sqrt ((x
+ 1)
/ 2))
^2 ))))
.= (
log (
number_e ,((((x
- 1)
/ 2)
+ ((2
* (
sqrt ((x
- 1)
/ 2)))
* (
sqrt ((x
+ 1)
/ 2))))
+ ((
sqrt ((x
+ 1)
/ 2))
^2 )))) by
A4,
SQUARE_1:def 2
.= (
log (
number_e ,((((x
- 1)
/ 2)
+ ((2
* (
sqrt ((x
- 1)
/ 2)))
* (
sqrt ((x
+ 1)
/ 2))))
+ ((x
+ 1)
/ 2)))) by
A1,
SQUARE_1:def 2
.= (
log (
number_e ,(x
+ (2
* ((
sqrt ((x
- 1)
/ 2))
* (
sqrt ((x
+ 1)
/ 2)))))))
.= (
log (
number_e ,(x
+ (2
* (
sqrt (((x
- 1)
/ 2)
* ((x
+ 1)
/ 2))))))) by
A1,
A4,
SQUARE_1: 29
.= (
log (
number_e ,(x
+ ((
sqrt (2
^2 ))
* (
sqrt (((x
^2 )
- 1)
/ 4)))))) by
SQUARE_1: 22
.= (
log (
number_e ,(x
+ (
sqrt (4
* (((x
^2 )
- 1)
/ 4)))))) by
A3,
SQUARE_1: 29
.= (
log (
number_e ,(x
+ (
sqrt ((x
^2 )
- 1)))));
hence thesis;
end;
theorem ::
SIN_COS7:41
(x
^2 )
< 1 implies (
tanh" x)
= (
sinh" (x
/ (
sqrt (1
- (x
^2 )))))
proof
assume
A1: (x
^2 )
< 1;
then
A2: (x
+ 1)
>
0 by
Th11;
A3: (
sqrt (x
+ 1))
>
0 by
A1,
Th11,
SQUARE_1: 25;
A4: ((x
+ 1)
/ (1
- x))
>
0 by
A1,
Lm4;
A5: (1
- (x
^2 ))
>
0 by
A1,
XREAL_1: 50;
A6: (1
- x)
>
0 by
A1,
Th11;
then
A7: (
sqrt ((x
+ 1)
/ (1
- x)))
= (((x
+ 1)
/ (1
- x))
to_power (1
/ 2)) by
A2,
ASYMPT_1: 83;
(
sinh" (x
/ (
sqrt (1
- (x
^2 )))))
= (
log (
number_e ,((x
/ (
sqrt (1
- (x
^2 ))))
+ (
sqrt (((x
^2 )
/ ((
sqrt (1
- (x
^2 )))
^2 ))
+ 1))))) by
XCMPLX_1: 76
.= (
log (
number_e ,((x
/ (
sqrt (1
- (x
^2 ))))
+ (
sqrt (((x
^2 )
/ (1
- (x
^2 )))
+ 1))))) by
A5,
SQUARE_1:def 2
.= (
log (
number_e ,((x
/ (
sqrt (1
- (x
^2 ))))
+ (
sqrt (((x
^2 )
+ ((1
- (x
^2 ))
* 1))
/ (1
- (x
^2 ))))))) by
A5,
XCMPLX_1: 113
.= (
log (
number_e ,((x
/ (
sqrt (1
- (x
^2 ))))
+ ((
sqrt 1)
/ (
sqrt (1
- (x
^2 ))))))) by
A5,
SQUARE_1: 30
.= (
log (
number_e ,((x
+ 1)
/ (
sqrt ((1
- x)
* (1
+ x)))))) by
SQUARE_1: 18
.= (
log (
number_e ,((
sqrt ((x
+ 1)
^2 ))
/ (
sqrt ((1
- x)
* (1
+ x)))))) by
A2,
SQUARE_1: 22
.= (
log (
number_e ,(((
sqrt (x
+ 1))
* (
sqrt (x
+ 1)))
/ (
sqrt ((1
- x)
* (1
+ x)))))) by
A2,
SQUARE_1: 29
.= (
log (
number_e ,(((
sqrt (x
+ 1))
* (
sqrt (x
+ 1)))
/ ((
sqrt (1
- x))
* (
sqrt (1
+ x)))))) by
A2,
A6,
SQUARE_1: 29
.= (
log (
number_e ,((
sqrt (x
+ 1))
/ (
sqrt (1
- x))))) by
A3,
XCMPLX_1: 91
.= (
log (
number_e ,(
sqrt ((x
+ 1)
/ (1
- x))))) by
A2,
A6,
SQUARE_1: 30
.= ((1
/ 2)
* (
log (
number_e ,((1
+ x)
/ (1
- x))))) by
A4,
A7,
Lm1,
POWER: 55,
TAYLOR_1: 11;
hence thesis;
end;
theorem ::
SIN_COS7:42
0
< x & x
< 1 implies (
tanh" x)
= (
cosh1" (1
/ (
sqrt (1
- (x
^2 )))))
proof
assume that
A1:
0
< x and
A2: x
< 1;
A3: (1
- (x
^2 ))
>
0 by
A1,
A2,
Lm5;
A4: ((1
+ x)
/ (1
- x))
>
0 by
A1,
A2,
Th15;
A5: (1
- x)
>
0 by
A2,
XREAL_1: 50;
A6: (
sqrt (1
+ x))
>
0 by
A1,
SQUARE_1: 25;
((1
+ x)
/ (1
- x))
>
0 by
A1,
A2,
Th15;
then
A7: (
sqrt ((1
+ x)
/ (1
- x)))
= (((1
+ x)
/ (1
- x))
to_power (1
/ 2)) by
ASYMPT_1: 83;
A8: (x
^2 )
>=
0 by
XREAL_1: 63;
(
cosh1" (1
/ (
sqrt (1
- (x
^2 )))))
= (
log (
number_e ,((1
/ (
sqrt (1
- (x
^2 ))))
+ (
sqrt ((1
/ ((
sqrt (1
- (x
^2 )))
^2 ))
- (1
^2 )))))) by
XCMPLX_1: 76
.= (
log (
number_e ,((1
/ (
sqrt (1
- (x
^2 ))))
+ (
sqrt ((1
/ (1
- (x
^2 )))
- 1))))) by
A3,
SQUARE_1:def 2
.= (
log (
number_e ,((1
/ (
sqrt (1
- (x
^2 ))))
+ (
sqrt ((1
- (1
* (1
- (x
^2 ))))
/ (1
- (x
^2 ))))))) by
A3,
XCMPLX_1: 126
.= (
log (
number_e ,((1
/ (
sqrt (1
- (x
^2 ))))
+ ((
sqrt (x
^2 ))
/ (
sqrt (1
- (x
^2 ))))))) by
A3,
A8,
SQUARE_1: 30
.= (
log (
number_e ,((1
/ (
sqrt (1
- (x
^2 ))))
+ (x
/ (
sqrt (1
- (x
^2 ))))))) by
A1,
SQUARE_1: 22
.= (
log (
number_e ,((1
+ x)
/ (
sqrt ((1
- x)
* (1
+ x))))))
.= (
log (
number_e ,((1
+ x)
/ ((
sqrt (1
- x))
* (
sqrt (1
+ x)))))) by
A1,
A5,
SQUARE_1: 29
.= (
log (
number_e ,((
sqrt ((1
+ x)
^2 ))
/ ((
sqrt (1
- x))
* (
sqrt (1
+ x)))))) by
A1,
SQUARE_1: 22
.= (
log (
number_e ,(((
sqrt (1
+ x))
* (
sqrt (1
+ x)))
/ ((
sqrt (1
- x))
* (
sqrt (1
+ x)))))) by
A1,
SQUARE_1: 29
.= (
log (
number_e ,((
sqrt (1
+ x))
/ (
sqrt (1
- x))))) by
A6,
XCMPLX_1: 91
.= (
log (
number_e ,(
sqrt ((1
+ x)
/ (1
- x))))) by
A1,
A5,
SQUARE_1: 30
.= ((1
/ 2)
* (
log (
number_e ,((1
+ x)
/ (1
- x))))) by
A7,
A4,
Lm1,
POWER: 55,
TAYLOR_1: 11;
hence thesis;
end;
theorem ::
SIN_COS7:43
(x
^2 )
< 1 implies (
tanh" x)
= ((1
/ 2)
* (
sinh" ((2
* x)
/ (1
- (x
^2 )))))
proof
assume
A1: (x
^2 )
< 1;
then
A2: ((1
- (x
^2 ))
^2 )
>
0 by
Th12;
A3: (x
+ 1)
>
0 by
A1,
Th11;
((1
/ 2)
* (
sinh" ((2
* x)
/ (1
- (x
^2 )))))
= ((1
/ 2)
* (
log (
number_e ,(((2
* x)
/ (1
- (x
^2 )))
+ (
sqrt ((((2
* x)
^2 )
/ ((1
- (x
^2 ))
^2 ))
+ 1)))))) by
XCMPLX_1: 76
.= ((1
/ 2)
* (
log (
number_e ,(((2
* x)
/ (1
- (x
^2 )))
+ (
sqrt (((4
* (x
^2 ))
+ (((1
- (x
^2 ))
^2 )
* 1))
/ ((1
- (x
^2 ))
^2 ))))))) by
A2,
XCMPLX_1: 113
.= ((1
/ 2)
* (
log (
number_e ,(((2
* x)
/ (1
- (x
^2 )))
+ (
sqrt ((((x
^2 )
+ 1)
^2 )
/ ((1
- (x
^2 ))
^2 )))))))
.= ((1
/ 2)
* (
log (
number_e ,(((2
* x)
/ (1
- (x
^2 )))
+ (
sqrt ((((x
^2 )
+ 1)
/ (1
- (x
^2 )))
^2 )))))) by
XCMPLX_1: 76
.= ((1
/ 2)
* (
log (
number_e ,(((2
* x)
/ (1
- (x
^2 )))
+ (((x
^2 )
+ 1)
/ (1
- (x
^2 ))))))) by
A1,
Th13,
SQUARE_1: 22
.= ((1
/ 2)
* (
log (
number_e ,(((2
* x)
+ ((x
^2 )
+ 1))
/ (1
- (x
^2 ))))))
.= ((1
/ 2)
* (
log (
number_e ,(((x
+ 1)
* (x
+ 1))
/ ((1
- x)
* (1
+ x))))))
.= ((1
/ 2)
* (
log (
number_e ,((x
+ 1)
/ (1
- x))))) by
A3,
XCMPLX_1: 91;
hence thesis;
end;
theorem ::
SIN_COS7:44
x
>
0 & x
< 1 implies (
tanh" x)
= ((1
/ 2)
* (
cosh1" ((1
+ (x
^2 ))
/ (1
- (x
^2 )))))
proof
assume that
A1: x
>
0 and
A2: x
< 1;
A3:
0
< ((1
- (x
^2 ))
^2 ) by
A1,
A2,
Th19;
A4: ((2
* x)
/ (1
- (x
^2 )))
>
0 by
A1,
A2,
Th18;
((1
/ 2)
* (
cosh1" ((1
+ (x
^2 ))
/ (1
- (x
^2 )))))
= ((1
/ 2)
* (
log (
number_e ,(((1
+ (x
^2 ))
/ (1
- (x
^2 )))
+ (
sqrt ((((1
+ (x
^2 ))
^2 )
/ ((1
- (x
^2 ))
^2 ))
- 1)))))) by
XCMPLX_1: 76
.= ((1
/ 2)
* (
log (
number_e ,(((1
+ (x
^2 ))
/ (1
- (x
^2 )))
+ (
sqrt ((((1
+ (x
^2 ))
^2 )
- (1
* ((1
- (x
^2 ))
^2 )))
/ ((1
- (x
^2 ))
^2 ))))))) by
A3,
XCMPLX_1: 126
.= ((1
/ 2)
* (
log (
number_e ,(((1
+ (x
^2 ))
/ (1
- (x
^2 )))
+ (
sqrt (((2
* x)
^2 )
/ ((1
- (x
^2 ))
^2 )))))))
.= ((1
/ 2)
* (
log (
number_e ,(((1
+ (x
^2 ))
/ (1
- (x
^2 )))
+ (
sqrt (((2
* x)
/ (1
- (x
^2 )))
^2 )))))) by
XCMPLX_1: 76
.= ((1
/ 2)
* (
log (
number_e ,(((1
+ (x
^2 ))
/ (1
- (x
^2 )))
+ ((2
* x)
/ (1
- (x
^2 ))))))) by
A4,
SQUARE_1: 22
.= ((1
/ 2)
* (
log (
number_e ,(((1
+ (x
^2 ))
+ (2
* x))
/ (1
- (x
^2 ))))))
.= ((1
/ 2)
* (
log (
number_e ,(((x
+ 1)
* (x
+ 1))
/ ((1
- x)
* (1
+ x))))))
.= ((1
/ 2)
* (
log (
number_e ,((x
+ 1)
/ (1
- x))))) by
A1,
XCMPLX_1: 91;
hence thesis;
end;
theorem ::
SIN_COS7:45
(x
^2 )
< 1 implies (
tanh" x)
= ((1
/ 2)
* (
tanh" ((2
* x)
/ (1
+ (x
^2 )))))
proof
assume (x
^2 )
< 1;
then
A1: ((x
+ 1)
/ (1
- x))
>
0 by
Lm4;
A2: (1
+ (x
^2 ))
>
0 by
Lm6;
then ((1
/ 2)
* (
tanh" ((2
* x)
/ (1
+ (x
^2 )))))
= ((1
/ 2)
* ((1
/ 2)
* (
log (
number_e ,((((2
* x)
+ ((1
+ (x
^2 ))
* 1))
/ (1
+ (x
^2 )))
/ (1
- ((2
* x)
/ (1
+ (x
^2 ))))))))) by
XCMPLX_1: 113
.= ((1
/ 2)
* ((1
/ 2)
* (
log (
number_e ,(((((2
* x)
+ 1)
+ (x
^2 ))
/ (1
+ (x
^2 )))
/ (((1
* (1
+ (x
^2 )))
- (2
* x))
/ (1
+ (x
^2 )))))))) by
A2,
XCMPLX_1: 127
.= ((1
/ 2)
* ((1
/ 2)
* (
log (
number_e ,(((x
+ 1)
^2 )
/ ((1
- x)
^2 )))))) by
A2,
XCMPLX_1: 55
.= ((1
/ 2)
* ((1
/ 2)
* (
log (
number_e ,(((x
+ 1)
/ (1
- x))
^2 ))))) by
XCMPLX_1: 76
.= ((1
/ 2)
* ((1
/ 2)
* (
log (
number_e ,(((x
+ 1)
/ (1
- x))
to_power 2))))) by
POWER: 46
.= ((1
/ 2)
* ((1
/ 2)
* (2
* (
log (
number_e ,((x
+ 1)
/ (1
- x))))))) by
A1,
Lm1,
POWER: 55,
TAYLOR_1: 11
.= ((1
/ 2)
* (
log (
number_e ,((1
+ x)
/ (1
- x)))));
hence thesis;
end;
theorem ::
SIN_COS7:46
(x
^2 )
> 1 implies (
coth" x)
= (
tanh" (1
/ x))
proof
assume (x
^2 )
> 1;
then
A1: x
<>
0 ;
then (
tanh" (1
/ x))
= ((1
/ 2)
* (
log (
number_e ,(((1
+ (x
* 1))
/ x)
/ (1
- (1
/ x)))))) by
XCMPLX_1: 113
.= ((1
/ 2)
* (
log (
number_e ,(((1
+ (x
* 1))
/ x)
/ (((1
* x)
- 1)
/ x))))) by
A1,
XCMPLX_1: 127
.= ((1
/ 2)
* (
log (
number_e ,((1
+ x)
/ (x
- 1))))) by
A1,
XCMPLX_1: 55;
hence thesis;
end;
theorem ::
SIN_COS7:47
x
>
0 & x
<= 1 implies (
sech1" x)
= (
cosh1" (1
/ x))
proof
assume that
A1: x
>
0 and
A2: x
<= 1;
A3: (1
- (x
^2 ))
>=
0 by
A1,
A2,
Th22;
A4: (x
^2 )
>
0 by
A1;
(
cosh1" (1
/ x))
= (
log (
number_e ,((1
/ x)
+ (
sqrt ((1
/ (x
^2 ))
- (1
^2 )))))) by
XCMPLX_1: 76
.= (
log (
number_e ,((1
/ x)
+ (
sqrt ((1
- (1
* (x
^2 )))
/ (x
^2 )))))) by
A4,
XCMPLX_1: 126
.= (
log (
number_e ,((1
/ x)
+ ((
sqrt (1
- (x
^2 )))
/ (
sqrt (x
^2 )))))) by
A1,
A3,
SQUARE_1: 30
.= (
log (
number_e ,((1
/ x)
+ ((
sqrt (1
- (x
^2 )))
/ x)))) by
A1,
SQUARE_1: 22
.= (
log (
number_e ,((1
+ (
sqrt (1
- (x
^2 ))))
/ x)));
hence thesis;
end;
theorem ::
SIN_COS7:48
x
>
0 & x
<= 1 implies (
sech2" x)
= (
cosh2" (1
/ x))
proof
assume that
A1: x
>
0 and
A2: x
<= 1;
A3: (1
- (x
^2 ))
>=
0 by
A1,
A2,
Th22;
A4: (x
^2 )
>
0 by
A1;
(
cosh2" (1
/ x))
= (
- (
log (
number_e ,((1
/ x)
+ (
sqrt ((1
/ (x
^2 ))
- (1
^2 ))))))) by
XCMPLX_1: 76
.= (
- (
log (
number_e ,((1
/ x)
+ (
sqrt ((1
- (1
* (x
^2 )))
/ (x
^2 ))))))) by
A4,
XCMPLX_1: 126
.= (
- (
log (
number_e ,((1
/ x)
+ ((
sqrt (1
- (x
^2 )))
/ (
sqrt (x
^2 ))))))) by
A1,
A3,
SQUARE_1: 30
.= (
- (
log (
number_e ,((1
/ x)
+ ((
sqrt (1
- (x
^2 )))
/ x))))) by
A1,
SQUARE_1: 22
.= (
- (
log (
number_e ,((1
+ (
sqrt (1
- (x
^2 ))))
/ x))));
hence thesis;
end;
theorem ::
SIN_COS7:49
x
>
0 implies (
csch" x)
= (
sinh" (1
/ x))
proof
assume
A1: x
>
0 ;
then
A2: (x
^2 )
>
0 ;
(
sinh" (1
/ x))
= (
log (
number_e ,((1
/ x)
+ (
sqrt ((1
/ (x
^2 ))
+ (1
^2 )))))) by
XCMPLX_1: 76
.= (
log (
number_e ,((1
/ x)
+ (
sqrt ((1
+ ((x
^2 )
* 1))
/ (x
^2 )))))) by
A2,
XCMPLX_1: 113
.= (
log (
number_e ,((1
/ x)
+ ((
sqrt (1
+ (x
^2 )))
/ (
sqrt (x
^2 )))))) by
A1,
SQUARE_1: 30
.= (
log (
number_e ,((1
/ x)
+ ((
sqrt (1
+ (x
^2 )))
/ x)))) by
A1,
SQUARE_1: 22
.= (
log (
number_e ,((1
+ (
sqrt (1
+ (x
^2 ))))
/ x)));
hence thesis by
A1,
Def8;
end;
theorem ::
SIN_COS7:50
((x
* y)
+ ((
sqrt ((x
^2 )
+ 1))
* (
sqrt ((y
^2 )
+ 1))))
>=
0 implies ((
sinh" x)
+ (
sinh" y))
= (
sinh" ((x
* (
sqrt (1
+ (y
^2 ))))
+ (y
* (
sqrt (1
+ (x
^2 ))))))
proof
assume
A1: ((x
* y)
+ ((
sqrt ((x
^2 )
+ 1))
* (
sqrt ((y
^2 )
+ 1))))
>=
0 ;
((
sqrt ((x
^2 )
+ 1))
+ x)
>
0 & ((
sqrt ((y
^2 )
+ 1))
+ y)
>
0 by
Th5;
then
A2: ((
sinh" x)
+ (
sinh" y))
= (
log (
number_e ,((x
+ (
sqrt ((x
^2 )
+ 1)))
* (y
+ (
sqrt ((y
^2 )
+ 1)))))) by
Lm1,
POWER: 53,
TAYLOR_1: 11
.= (
log (
number_e ,(((x
* (
sqrt ((y
^2 )
+ 1)))
+ ((
sqrt ((x
^2 )
+ 1))
* y))
+ ((x
* y)
+ ((
sqrt ((x
^2 )
+ 1))
* (
sqrt ((y
^2 )
+ 1)))))))
.= (
log (
number_e ,(((x
* (
sqrt ((y
^2 )
+ 1)))
+ ((
sqrt ((x
^2 )
+ 1))
* y))
+ (
sqrt (((x
* y)
+ ((
sqrt ((x
^2 )
+ 1))
* (
sqrt ((y
^2 )
+ 1))))
^2 ))))) by
A1,
SQUARE_1: 22;
A3: ((y
^2 )
+ 1)
>=
0 by
Lm6;
set p = (
sqrt ((((x
* (
sqrt (1
+ (y
^2 ))))
+ (y
* (
sqrt (1
+ (x
^2 )))))
^2 )
+ 1));
set t = (
sqrt (((x
* y)
+ ((
sqrt ((x
^2 )
+ 1))
* (
sqrt ((y
^2 )
+ 1))))
^2 ));
A4: ((x
^2 )
+ 1)
>=
0 by
Lm6;
A5: p
= (
sqrt (((((x
^2 )
* ((
sqrt (1
+ (y
^2 )))
^2 ))
+ ((2
* (x
* (
sqrt (1
+ (y
^2 )))))
* (y
* (
sqrt (1
+ (x
^2 ))))))
+ ((y
* (
sqrt (1
+ (x
^2 ))))
^2 ))
+ 1))
.= (
sqrt (((((x
^2 )
* (1
+ (y
^2 )))
+ ((2
* (x
* (
sqrt (1
+ (y
^2 )))))
* (y
* (
sqrt (1
+ (x
^2 ))))))
+ ((y
* (
sqrt (1
+ (x
^2 ))))
^2 ))
+ 1)) by
A3,
SQUARE_1:def 2
.= (
sqrt (((((x
^2 )
+ ((x
* y)
^2 ))
+ ((2
* (x
* (
sqrt (1
+ (y
^2 )))))
* (y
* (
sqrt (1
+ (x
^2 ))))))
+ ((y
^2 )
* ((
sqrt (1
+ (x
^2 )))
^2 )))
+ 1))
.= (
sqrt (((((x
^2 )
+ ((x
* y)
^2 ))
+ ((2
* (x
* (
sqrt (1
+ (y
^2 )))))
* (y
* (
sqrt (1
+ (x
^2 ))))))
+ ((y
^2 )
* (1
+ (x
^2 ))))
+ 1)) by
A4,
SQUARE_1:def 2
.= (
sqrt (((((x
^2 )
+ (2
* ((x
* y)
^2 )))
+ (y
^2 ))
+ 1)
+ (((2
* x)
* y)
* ((
sqrt (1
+ (y
^2 )))
* (
sqrt (1
+ (x
^2 )))))))
.= (
sqrt (((((x
^2 )
+ (2
* ((x
* y)
^2 )))
+ (y
^2 ))
+ 1)
+ (((2
* x)
* y)
* (
sqrt ((1
+ (y
^2 ))
* (1
+ (x
^2 ))))))) by
A4,
A3,
SQUARE_1: 29;
t
= (
sqrt (((x
* y)
+ (
sqrt (((x
^2 )
+ 1)
* ((y
^2 )
+ 1))))
^2 )) by
A4,
A3,
SQUARE_1: 29
.= (
sqrt ((((x
* y)
^2 )
+ ((2
* (x
* y))
* (
sqrt (((x
^2 )
+ 1)
* ((y
^2 )
+ 1)))))
+ ((
sqrt (((x
^2 )
+ 1)
* ((y
^2 )
+ 1)))
^2 )))
.= (
sqrt ((((x
* y)
^2 )
+ ((2
* (x
* y))
* (
sqrt (((x
^2 )
+ 1)
* ((y
^2 )
+ 1)))))
+ (((((x
* y)
^2 )
+ (x
^2 ))
+ (y
^2 ))
+ 1))) by
A4,
A3,
SQUARE_1:def 2
.= (
sqrt (((((2
* ((x
* y)
^2 ))
+ (x
^2 ))
+ (y
^2 ))
+ 1)
+ ((2
* (x
* y))
* (
sqrt (((x
^2 )
+ 1)
* ((y
^2 )
+ 1))))));
hence thesis by
A2,
A5;
end;
theorem ::
SIN_COS7:51
((
sinh" x)
- (
sinh" y))
= (
sinh" ((x
* (
sqrt (1
+ (y
^2 ))))
- (y
* (
sqrt (1
+ (x
^2 ))))))
proof
set t = (((
sqrt ((x
^2 )
+ 1))
* (
sqrt ((y
^2 )
+ 1)))
- (x
* y));
set q = (
sqrt ((((x
* (
sqrt (1
+ (y
^2 ))))
- (y
* (
sqrt (1
+ (x
^2 )))))
^2 )
+ 1));
A1: ((x
^2 )
+ 1)
>=
0 by
Lm6;
(y
+
0 )
< (
sqrt ((y
^2 )
+ 1)) by
Lm8;
then
A2: ((
sqrt ((y
^2 )
+ 1))
- y)
>
0 by
XREAL_1: 20;
A3: ((y
^2 )
+ 1)
>=
0 by
Lm6;
(((
sqrt ((x
^2 )
+ 1))
* (
sqrt ((y
^2 )
+ 1)))
- (x
* y))
>=
0 by
Lm9;
then
A4: t
= (
sqrt ((((
sqrt ((x
^2 )
+ 1))
* (
sqrt ((y
^2 )
+ 1)))
- (x
* y))
^2 )) by
SQUARE_1: 22
.= (
sqrt (((((
sqrt ((x
^2 )
+ 1))
^2 )
* ((
sqrt ((y
^2 )
+ 1))
^2 ))
- ((2
* ((
sqrt ((x
^2 )
+ 1))
* (
sqrt ((y
^2 )
+ 1))))
* (x
* y)))
+ ((x
* y)
^2 )))
.= (
sqrt (((((x
^2 )
+ 1)
* ((
sqrt ((y
^2 )
+ 1))
^2 ))
- ((2
* ((
sqrt ((x
^2 )
+ 1))
* (
sqrt ((y
^2 )
+ 1))))
* (x
* y)))
+ ((x
* y)
^2 ))) by
A1,
SQUARE_1:def 2
.= (
sqrt (((((x
^2 )
+ 1)
* ((y
^2 )
+ 1))
- ((2
* ((
sqrt ((x
^2 )
+ 1))
* (
sqrt ((y
^2 )
+ 1))))
* (x
* y)))
+ ((x
* y)
^2 ))) by
A3,
SQUARE_1:def 2
.= (
sqrt (((((2
* ((x
* y)
^2 ))
+ (x
^2 ))
+ (y
^2 ))
+ 1)
- ((2
* (x
* y))
* ((
sqrt ((x
^2 )
+ 1))
* (
sqrt ((y
^2 )
+ 1))))));
A5: q
= (
sqrt (((((x
^2 )
* ((
sqrt (1
+ (y
^2 )))
^2 ))
- ((2
* (x
* (
sqrt (1
+ (y
^2 )))))
* (y
* (
sqrt (1
+ (x
^2 ))))))
+ ((y
* (
sqrt (1
+ (x
^2 ))))
^2 ))
+ 1))
.= (
sqrt (((((x
^2 )
* (1
+ (y
^2 )))
- ((2
* (x
* (
sqrt (1
+ (y
^2 )))))
* (y
* (
sqrt (1
+ (x
^2 ))))))
+ ((y
* (
sqrt (1
+ (x
^2 ))))
^2 ))
+ 1)) by
A3,
SQUARE_1:def 2
.= (
sqrt (((((x
^2 )
+ ((x
^2 )
* (y
^2 )))
- ((2
* (x
* (
sqrt (1
+ (y
^2 )))))
* (y
* (
sqrt (1
+ (x
^2 ))))))
+ ((y
^2 )
* ((
sqrt (1
+ (x
^2 )))
^2 )))
+ 1))
.= (
sqrt (((((x
^2 )
+ ((x
^2 )
* (y
^2 )))
- ((2
* (x
* (
sqrt (1
+ (y
^2 )))))
* (y
* (
sqrt (1
+ (x
^2 ))))))
+ ((y
^2 )
* (1
+ (x
^2 ))))
+ 1)) by
A1,
SQUARE_1:def 2
.= (
sqrt (((((x
^2 )
+ (y
^2 ))
+ (2
* ((x
* y)
^2 )))
+ 1)
- ((((2
* x)
* y)
* (
sqrt (1
+ (y
^2 ))))
* (
sqrt (1
+ (x
^2 ))))));
((
sqrt ((x
^2 )
+ 1))
+ x)
>
0 & ((
sqrt ((y
^2 )
+ 1))
+ y)
>
0 by
Th5;
then ((
sinh" x)
- (
sinh" y))
= (
log (
number_e ,((x
+ (
sqrt ((x
^2 )
+ 1)))
/ (y
+ (
sqrt ((y
^2 )
+ 1)))))) by
Lm1,
POWER: 54,
TAYLOR_1: 11
.= (
log (
number_e ,(((x
+ (
sqrt ((x
^2 )
+ 1)))
* ((
sqrt ((y
^2 )
+ 1))
- y))
/ ((y
+ (
sqrt ((y
^2 )
+ 1)))
* ((
sqrt ((y
^2 )
+ 1))
- y))))) by
A2,
XCMPLX_1: 91
.= (
log (
number_e ,(((x
+ (
sqrt ((x
^2 )
+ 1)))
* ((
sqrt ((y
^2 )
+ 1))
- y))
/ (((
sqrt ((y
^2 )
+ 1))
^2 )
- (y
^2 )))))
.= (
log (
number_e ,(((x
+ (
sqrt ((x
^2 )
+ 1)))
* ((
sqrt ((y
^2 )
+ 1))
- y))
/ (((y
^2 )
+ 1)
- (y
^2 ))))) by
A3,
SQUARE_1:def 2
.= (
log (
number_e ,((((x
* (
sqrt ((y
^2 )
+ 1)))
- (y
* (
sqrt ((x
^2 )
+ 1))))
+ ((
sqrt ((x
^2 )
+ 1))
* (
sqrt ((y
^2 )
+ 1))))
- (x
* y))));
hence thesis by
A4,
A5;
end;
theorem ::
SIN_COS7:52
1
<= x & 1
<= y implies ((
cosh1" x)
+ (
cosh1" y))
= (
cosh1" ((x
* y)
+ (
sqrt (((x
^2 )
- 1)
* ((y
^2 )
- 1)))))
proof
assume that
A1: 1
<= x and
A2: 1
<= y;
A3: ((y
^2 )
- 1)
>=
0 by
A2,
Lm3;
set t = ((x
* (
sqrt ((y
^2 )
- 1)))
+ (y
* (
sqrt ((x
^2 )
- 1))));
A4: ((x
^2 )
- 1)
>=
0 by
A1,
Lm3;
t
= (
sqrt (((x
* (
sqrt ((y
^2 )
- 1)))
+ (y
* (
sqrt ((x
^2 )
- 1))))
^2 )) by
A1,
A2,
Th24,
SQUARE_1: 22
.= (
sqrt ((((x
^2 )
* ((
sqrt ((y
^2 )
- 1))
^2 ))
+ ((2
* (x
* (
sqrt ((y
^2 )
- 1))))
* (y
* (
sqrt ((x
^2 )
- 1)))))
+ ((y
* (
sqrt ((x
^2 )
- 1)))
^2 )))
.= (
sqrt ((((x
^2 )
* ((y
^2 )
- 1))
+ ((2
* (x
* (
sqrt ((y
^2 )
- 1))))
* (y
* (
sqrt ((x
^2 )
- 1)))))
+ ((y
* (
sqrt ((x
^2 )
- 1)))
^2 ))) by
A3,
SQUARE_1:def 2
.= (
sqrt (((((x
^2 )
* (y
^2 ))
- (x
^2 ))
+ ((2
* (x
* (
sqrt ((y
^2 )
- 1))))
* (y
* (
sqrt ((x
^2 )
- 1)))))
+ ((y
^2 )
* ((
sqrt ((x
^2 )
- 1))
^2 ))))
.= (
sqrt (((((x
^2 )
* (y
^2 ))
- (x
^2 ))
+ ((2
* (x
* (
sqrt ((y
^2 )
- 1))))
* (y
* (
sqrt ((x
^2 )
- 1)))))
+ ((y
^2 )
* ((x
^2 )
- 1)))) by
A4,
SQUARE_1:def 2
.= (
sqrt ((((2
* ((x
* y)
^2 ))
- (x
^2 ))
- (y
^2 ))
+ ((2
* (x
* (
sqrt ((y
^2 )
- 1))))
* (y
* (
sqrt ((x
^2 )
- 1))))));
then
A5: (
log (
number_e ,((((x
* (
sqrt ((y
^2 )
- 1)))
+ (y
* (
sqrt ((x
^2 )
- 1))))
+ (
sqrt (((x
^2 )
- 1)
* ((y
^2 )
- 1))))
+ (x
* y))))
= (
log (
number_e ,(((
sqrt ((((2
* ((x
* y)
^2 ))
- (x
^2 ))
- (y
^2 ))
+ (((2
* x)
* y)
* ((
sqrt ((y
^2 )
- 1))
* (
sqrt ((x
^2 )
- 1))))))
+ (
sqrt (((x
^2 )
- 1)
* ((y
^2 )
- 1))))
+ (x
* y))))
.= (
log (
number_e ,(((
sqrt ((((2
* ((x
* y)
^2 ))
- (x
^2 ))
- (y
^2 ))
+ (((2
* x)
* y)
* (
sqrt (((y
^2 )
- 1)
* ((x
^2 )
- 1))))))
+ (
sqrt (((x
^2 )
- 1)
* ((y
^2 )
- 1))))
+ (x
* y)))) by
A4,
A3,
SQUARE_1: 29;
A6: (
cosh1" ((x
* y)
+ (
sqrt (((x
^2 )
- 1)
* ((y
^2 )
- 1)))))
= (
log (
number_e ,(((x
* y)
+ (
sqrt (((x
^2 )
- 1)
* ((y
^2 )
- 1))))
+ (
sqrt (((((x
* y)
^2 )
+ ((2
* (x
* y))
* (
sqrt (((x
^2 )
- 1)
* ((y
^2 )
- 1)))))
+ ((
sqrt (((x
^2 )
- 1)
* ((y
^2 )
- 1)))
^2 ))
- 1)))))
.= (
log (
number_e ,(((x
* y)
+ (
sqrt (((x
^2 )
- 1)
* ((y
^2 )
- 1))))
+ (
sqrt (((((x
* y)
^2 )
+ ((2
* (x
* y))
* (
sqrt (((x
^2 )
- 1)
* ((y
^2 )
- 1)))))
+ (((x
^2 )
- 1)
* ((y
^2 )
- 1)))
- 1))))) by
A4,
A3,
SQUARE_1:def 2
.= (
log (
number_e ,((
sqrt ((((2
* ((x
* y)
^2 ))
- (x
^2 ))
- (y
^2 ))
+ (((2
* x)
* y)
* (
sqrt (((y
^2 )
- 1)
* ((x
^2 )
- 1))))))
+ ((
sqrt (((x
^2 )
- 1)
* ((y
^2 )
- 1)))
+ (x
* y)))));
0
< (x
+ (
sqrt ((x
^2 )
- 1))) &
0
< (y
+ (
sqrt ((y
^2 )
- 1))) by
A1,
A2,
Th23;
then ((
cosh1" x)
+ (
cosh1" y))
= (
log (
number_e ,((x
+ (
sqrt ((x
^2 )
- 1)))
* (y
+ (
sqrt ((y
^2 )
- 1)))))) by
Lm1,
POWER: 53,
TAYLOR_1: 11
.= (
log (
number_e ,((((x
* (
sqrt ((y
^2 )
- 1)))
+ (y
* (
sqrt ((x
^2 )
- 1))))
+ ((
sqrt ((x
^2 )
- 1))
* (
sqrt ((y
^2 )
- 1))))
+ (x
* y))))
.= (
log (
number_e ,((((x
* (
sqrt ((y
^2 )
- 1)))
+ (y
* (
sqrt ((x
^2 )
- 1))))
+ (
sqrt (((x
^2 )
- 1)
* ((y
^2 )
- 1))))
+ (x
* y)))) by
A4,
A3,
SQUARE_1: 29;
hence thesis by
A5,
A6;
end;
theorem ::
SIN_COS7:53
1
<= x & 1
<= y implies ((
cosh2" x)
+ (
cosh2" y))
= (
cosh2" ((x
* y)
+ (
sqrt (((x
^2 )
- 1)
* ((y
^2 )
- 1)))))
proof
assume that
A1: 1
<= x and
A2: 1
<= y;
A3: ((y
^2 )
- 1)
>=
0 by
A2,
Lm3;
A4:
0
< (x
+ (
sqrt ((x
^2 )
- 1))) &
0
< (y
+ (
sqrt ((y
^2 )
- 1))) by
A1,
A2,
Th23;
set t = ((x
* (
sqrt ((y
^2 )
- 1)))
+ (y
* (
sqrt ((x
^2 )
- 1))));
A5: ((x
^2 )
- 1)
>=
0 by
A1,
Lm3;
t
= (
sqrt (((x
* (
sqrt ((y
^2 )
- 1)))
+ (y
* (
sqrt ((x
^2 )
- 1))))
^2 )) by
A1,
A2,
Th24,
SQUARE_1: 22
.= (
sqrt ((((x
^2 )
* ((
sqrt ((y
^2 )
- 1))
^2 ))
+ ((2
* (x
* (
sqrt ((y
^2 )
- 1))))
* (y
* (
sqrt ((x
^2 )
- 1)))))
+ ((y
* (
sqrt ((x
^2 )
- 1)))
^2 )))
.= (
sqrt ((((x
^2 )
* ((y
^2 )
- 1))
+ ((2
* (x
* (
sqrt ((y
^2 )
- 1))))
* (y
* (
sqrt ((x
^2 )
- 1)))))
+ ((y
* (
sqrt ((x
^2 )
- 1)))
^2 ))) by
A3,
SQUARE_1:def 2
.= (
sqrt (((((x
^2 )
* (y
^2 ))
- (x
^2 ))
+ ((2
* (x
* (
sqrt ((y
^2 )
- 1))))
* (y
* (
sqrt ((x
^2 )
- 1)))))
+ ((y
^2 )
* ((
sqrt ((x
^2 )
- 1))
^2 ))))
.= (
sqrt (((((x
^2 )
* (y
^2 ))
- (x
^2 ))
+ ((2
* (x
* (
sqrt ((y
^2 )
- 1))))
* (y
* (
sqrt ((x
^2 )
- 1)))))
+ ((y
^2 )
* ((x
^2 )
- 1)))) by
A5,
SQUARE_1:def 2
.= (
sqrt ((((2
* ((x
* y)
^2 ))
- (x
^2 ))
- (y
^2 ))
+ ((2
* (x
* (
sqrt ((y
^2 )
- 1))))
* (y
* (
sqrt ((x
^2 )
- 1))))));
then
A6: (
- (
log (
number_e ,((((x
* (
sqrt ((y
^2 )
- 1)))
+ (y
* (
sqrt ((x
^2 )
- 1))))
+ (
sqrt (((x
^2 )
- 1)
* ((y
^2 )
- 1))))
+ (x
* y)))))
= (
- (
log (
number_e ,(((
sqrt ((((2
* ((x
* y)
^2 ))
- (x
^2 ))
- (y
^2 ))
+ (((2
* x)
* y)
* ((
sqrt ((y
^2 )
- 1))
* (
sqrt ((x
^2 )
- 1))))))
+ (
sqrt (((x
^2 )
- 1)
* ((y
^2 )
- 1))))
+ (x
* y)))))
.= (
- (
log (
number_e ,(((
sqrt ((((2
* ((x
* y)
^2 ))
- (x
^2 ))
- (y
^2 ))
+ (((2
* x)
* y)
* (
sqrt (((y
^2 )
- 1)
* ((x
^2 )
- 1))))))
+ (
sqrt (((x
^2 )
- 1)
* ((y
^2 )
- 1))))
+ (x
* y))))) by
A5,
A3,
SQUARE_1: 29;
A7: (
cosh2" ((x
* y)
+ (
sqrt (((x
^2 )
- 1)
* ((y
^2 )
- 1)))))
= (
- (
log (
number_e ,(((x
* y)
+ (
sqrt (((x
^2 )
- 1)
* ((y
^2 )
- 1))))
+ (
sqrt (((((x
* y)
^2 )
+ ((2
* (x
* y))
* (
sqrt (((x
^2 )
- 1)
* ((y
^2 )
- 1)))))
+ ((
sqrt (((x
^2 )
- 1)
* ((y
^2 )
- 1)))
^2 ))
- 1))))))
.= (
- (
log (
number_e ,(((x
* y)
+ (
sqrt (((x
^2 )
- 1)
* ((y
^2 )
- 1))))
+ (
sqrt (((((x
* y)
^2 )
+ ((2
* (x
* y))
* (
sqrt (((x
^2 )
- 1)
* ((y
^2 )
- 1)))))
+ (((x
^2 )
- 1)
* ((y
^2 )
- 1)))
- 1)))))) by
A5,
A3,
SQUARE_1:def 2
.= (
- (
log (
number_e ,((
sqrt ((((2
* ((x
* y)
^2 ))
- (x
^2 ))
- (y
^2 ))
+ (((2
* x)
* y)
* (
sqrt (((y
^2 )
- 1)
* ((x
^2 )
- 1))))))
+ ((
sqrt (((x
^2 )
- 1)
* ((y
^2 )
- 1)))
+ (x
* y))))));
((
cosh2" x)
+ (
cosh2" y))
= ((
- 1)
* ((
log (
number_e ,(x
+ (
sqrt ((x
^2 )
- 1)))))
+ (
log (
number_e ,(y
+ (
sqrt ((y
^2 )
- 1)))))))
.= ((
- 1)
* (
log (
number_e ,((x
+ (
sqrt ((x
^2 )
- 1)))
* (y
+ (
sqrt ((y
^2 )
- 1))))))) by
A4,
Lm1,
POWER: 53,
TAYLOR_1: 11
.= (
- (
log (
number_e ,((((x
* (
sqrt ((y
^2 )
- 1)))
+ (y
* (
sqrt ((x
^2 )
- 1))))
+ ((
sqrt ((x
^2 )
- 1))
* (
sqrt ((y
^2 )
- 1))))
+ (x
* y)))))
.= (
- (
log (
number_e ,((((x
* (
sqrt ((y
^2 )
- 1)))
+ (y
* (
sqrt ((x
^2 )
- 1))))
+ (
sqrt (((x
^2 )
- 1)
* ((y
^2 )
- 1))))
+ (x
* y))))) by
A5,
A3,
SQUARE_1: 29;
hence thesis by
A6,
A7;
end;
theorem ::
SIN_COS7:54
1
<= x & 1
<= y &
|.y.|
<=
|.x.| implies ((
cosh1" x)
- (
cosh1" y))
= (
cosh1" ((x
* y)
- (
sqrt (((x
^2 )
- 1)
* ((y
^2 )
- 1)))))
proof
assume that
A1: 1
<= x and
A2: 1
<= y and
A3:
|.y.|
<=
|.x.|;
A4:
0
<= ((x
^2 )
- 1) by
A1,
Lm3;
set t = ((y
* (
sqrt ((x
^2 )
- 1)))
- (x
* (
sqrt ((y
^2 )
- 1))));
A5: (y
- (
sqrt ((y
^2 )
- 1)))
>
0 by
A2,
Th25;
A6:
0
<= ((y
^2 )
- 1) by
A2,
Lm3;
0
< (x
+ (
sqrt ((x
^2 )
- 1))) &
0
< (y
+ (
sqrt ((y
^2 )
- 1))) by
A1,
A2,
Th23;
then
A7: ((
cosh1" x)
- (
cosh1" y))
= (
log (
number_e ,((x
+ (
sqrt ((x
^2 )
- 1)))
/ (y
+ (
sqrt ((y
^2 )
- 1)))))) by
Lm1,
POWER: 54,
TAYLOR_1: 11
.= (
log (
number_e ,(((x
+ (
sqrt ((x
^2 )
- 1)))
* (y
- (
sqrt ((y
^2 )
- 1))))
/ ((y
+ (
sqrt ((y
^2 )
- 1)))
* (y
- (
sqrt ((y
^2 )
- 1))))))) by
A5,
XCMPLX_1: 91
.= (
log (
number_e ,(((x
+ (
sqrt ((x
^2 )
- 1)))
* (y
- (
sqrt ((y
^2 )
- 1))))
/ ((y
^2 )
- ((
sqrt ((y
^2 )
- 1))
^2 )))))
.= (
log (
number_e ,(((x
+ (
sqrt ((x
^2 )
- 1)))
* (y
- (
sqrt ((y
^2 )
- 1))))
/ ((y
^2 )
- ((y
^2 )
- 1))))) by
A6,
SQUARE_1:def 2
.= (
log (
number_e ,((((x
* y)
- (x
* (
sqrt ((y
^2 )
- 1))))
+ (y
* (
sqrt ((x
^2 )
- 1))))
- ((
sqrt ((x
^2 )
- 1))
* (
sqrt ((y
^2 )
- 1))))))
.= (
log (
number_e ,((((x
* y)
- (x
* (
sqrt ((y
^2 )
- 1))))
+ (y
* (
sqrt ((x
^2 )
- 1))))
- (
sqrt (((x
^2 )
- 1)
* ((y
^2 )
- 1)))))) by
A4,
A6,
SQUARE_1: 29
.= (
log (
number_e ,((((x
* y)
- (
sqrt (((x
^2 )
- 1)
* ((y
^2 )
- 1))))
+ (y
* (
sqrt ((x
^2 )
- 1))))
- (x
* (
sqrt ((y
^2 )
- 1))))));
A8: (
cosh1" ((x
* y)
- (
sqrt (((x
^2 )
- 1)
* ((y
^2 )
- 1)))))
= (
log (
number_e ,(((x
* y)
- (
sqrt (((x
^2 )
- 1)
* ((y
^2 )
- 1))))
+ (
sqrt (((((x
* y)
^2 )
- ((2
* (x
* y))
* (
sqrt (((x
^2 )
- 1)
* ((y
^2 )
- 1)))))
+ ((
sqrt (((x
^2 )
- 1)
* ((y
^2 )
- 1)))
^2 ))
- 1)))))
.= (
log (
number_e ,(((x
* y)
- (
sqrt (((x
^2 )
- 1)
* ((y
^2 )
- 1))))
+ (
sqrt (((((x
* y)
^2 )
- ((2
* (x
* y))
* (
sqrt (((x
^2 )
- 1)
* ((y
^2 )
- 1)))))
+ (((x
^2 )
- 1)
* ((y
^2 )
- 1)))
- 1))))) by
A4,
A6,
SQUARE_1:def 2
.= (
log (
number_e ,(((x
* y)
- (
sqrt (((x
^2 )
- 1)
* ((y
^2 )
- 1))))
+ (
sqrt ((((2
* ((x
* y)
^2 ))
- (x
^2 ))
- (y
^2 ))
- (((2
* x)
* y)
* (
sqrt (((x
^2 )
- 1)
* ((y
^2 )
- 1)))))))));
t
= (
sqrt (((y
* (
sqrt ((x
^2 )
- 1)))
- (x
* (
sqrt ((y
^2 )
- 1))))
^2 )) by
A1,
A2,
A3,
Th26,
SQUARE_1: 22
.= (
sqrt ((((y
^2 )
* ((
sqrt ((x
^2 )
- 1))
^2 ))
- ((2
* (y
* (
sqrt ((x
^2 )
- 1))))
* (x
* (
sqrt ((y
^2 )
- 1)))))
+ ((x
* (
sqrt ((y
^2 )
- 1)))
^2 )))
.= (
sqrt ((((y
^2 )
* ((x
^2 )
- 1))
- ((2
* (y
* (
sqrt ((x
^2 )
- 1))))
* (x
* (
sqrt ((y
^2 )
- 1)))))
+ ((x
* (
sqrt ((y
^2 )
- 1)))
^2 ))) by
A4,
SQUARE_1:def 2
.= (
sqrt (((((x
* y)
^2 )
- (y
^2 ))
- ((2
* (y
* (
sqrt ((x
^2 )
- 1))))
* (x
* (
sqrt ((y
^2 )
- 1)))))
+ ((x
^2 )
* ((
sqrt ((y
^2 )
- 1))
^2 ))))
.= (
sqrt (((((x
* y)
^2 )
- (y
^2 ))
- ((2
* (y
* (
sqrt ((x
^2 )
- 1))))
* (x
* (
sqrt ((y
^2 )
- 1)))))
+ ((x
^2 )
* ((y
^2 )
- 1)))) by
A6,
SQUARE_1:def 2
.= (
sqrt ((((2
* ((x
* y)
^2 ))
- (x
^2 ))
- (y
^2 ))
- (((2
* x)
* y)
* ((
sqrt ((x
^2 )
- 1))
* (
sqrt ((y
^2 )
- 1))))))
.= (
sqrt ((((2
* ((x
* y)
^2 ))
- (x
^2 ))
- (y
^2 ))
- (((2
* x)
* y)
* (
sqrt (((x
^2 )
- 1)
* ((y
^2 )
- 1)))))) by
A4,
A6,
SQUARE_1: 29;
hence thesis by
A7,
A8;
end;
theorem ::
SIN_COS7:55
1
<= x & 1
<= y &
|.y.|
<=
|.x.| implies ((
cosh2" x)
- (
cosh2" y))
= (
cosh2" ((x
* y)
- (
sqrt (((x
^2 )
- 1)
* ((y
^2 )
- 1)))))
proof
assume that
A1: 1
<= x and
A2: 1
<= y and
A3:
|.y.|
<=
|.x.|;
A4:
0
< (x
+ (
sqrt ((x
^2 )
- 1))) &
0
< (y
+ (
sqrt ((y
^2 )
- 1))) by
A1,
A2,
Th23;
A5:
0
<= ((y
^2 )
- 1) by
A2,
Lm3;
set t = ((y
* (
sqrt ((x
^2 )
- 1)))
- (x
* (
sqrt ((y
^2 )
- 1))));
A6: (y
- (
sqrt ((y
^2 )
- 1)))
>
0 by
A2,
Th25;
A7:
0
<= ((x
^2 )
- 1) by
A1,
Lm3;
A8: (
cosh2" ((x
* y)
- (
sqrt (((x
^2 )
- 1)
* ((y
^2 )
- 1)))))
= (
- (
log (
number_e ,(((x
* y)
- (
sqrt (((x
^2 )
- 1)
* ((y
^2 )
- 1))))
+ (
sqrt (((((x
* y)
^2 )
- ((2
* (x
* y))
* (
sqrt (((x
^2 )
- 1)
* ((y
^2 )
- 1)))))
+ ((
sqrt (((x
^2 )
- 1)
* ((y
^2 )
- 1)))
^2 ))
- 1))))))
.= (
- (
log (
number_e ,(((x
* y)
- (
sqrt (((x
^2 )
- 1)
* ((y
^2 )
- 1))))
+ (
sqrt (((((x
* y)
^2 )
- ((2
* (x
* y))
* (
sqrt (((x
^2 )
- 1)
* ((y
^2 )
- 1)))))
+ (((x
^2 )
- 1)
* ((y
^2 )
- 1)))
- 1)))))) by
A7,
A5,
SQUARE_1:def 2
.= (
- (
log (
number_e ,(((x
* y)
- (
sqrt (((x
^2 )
- 1)
* ((y
^2 )
- 1))))
+ (
sqrt ((((2
* ((x
* y)
^2 ))
- (x
^2 ))
- (y
^2 ))
- (((2
* x)
* y)
* (
sqrt (((x
^2 )
- 1)
* ((y
^2 )
- 1))))))))));
A9: ((
cosh2" x)
- (
cosh2" y))
= (
- ((
log (
number_e ,(x
+ (
sqrt ((x
^2 )
- 1)))))
- (
log (
number_e ,(y
+ (
sqrt ((y
^2 )
- 1)))))))
.= (
- (
log (
number_e ,((x
+ (
sqrt ((x
^2 )
- 1)))
/ (y
+ (
sqrt ((y
^2 )
- 1))))))) by
A4,
Lm1,
POWER: 54,
TAYLOR_1: 11
.= (
- (
log (
number_e ,(((x
+ (
sqrt ((x
^2 )
- 1)))
* (y
- (
sqrt ((y
^2 )
- 1))))
/ ((y
+ (
sqrt ((y
^2 )
- 1)))
* (y
- (
sqrt ((y
^2 )
- 1)))))))) by
A6,
XCMPLX_1: 91
.= (
- (
log (
number_e ,(((x
+ (
sqrt ((x
^2 )
- 1)))
* (y
- (
sqrt ((y
^2 )
- 1))))
/ ((y
^2 )
- ((
sqrt ((y
^2 )
- 1))
^2 ))))))
.= (
- (
log (
number_e ,(((x
+ (
sqrt ((x
^2 )
- 1)))
* (y
- (
sqrt ((y
^2 )
- 1))))
/ ((y
^2 )
- ((y
^2 )
- 1)))))) by
A5,
SQUARE_1:def 2
.= (
- (
log (
number_e ,((((x
* y)
- (x
* (
sqrt ((y
^2 )
- 1))))
+ (y
* (
sqrt ((x
^2 )
- 1))))
- ((
sqrt ((x
^2 )
- 1))
* (
sqrt ((y
^2 )
- 1)))))))
.= (
- (
log (
number_e ,((((x
* y)
- (x
* (
sqrt ((y
^2 )
- 1))))
+ (y
* (
sqrt ((x
^2 )
- 1))))
- (
sqrt (((x
^2 )
- 1)
* ((y
^2 )
- 1))))))) by
A7,
A5,
SQUARE_1: 29
.= (
- (
log (
number_e ,((((x
* y)
- (
sqrt (((x
^2 )
- 1)
* ((y
^2 )
- 1))))
+ (y
* (
sqrt ((x
^2 )
- 1))))
- (x
* (
sqrt ((y
^2 )
- 1)))))));
t
= (
sqrt (((y
* (
sqrt ((x
^2 )
- 1)))
- (x
* (
sqrt ((y
^2 )
- 1))))
^2 )) by
A1,
A2,
A3,
Th26,
SQUARE_1: 22
.= (
sqrt ((((y
^2 )
* ((
sqrt ((x
^2 )
- 1))
^2 ))
- ((2
* (y
* (
sqrt ((x
^2 )
- 1))))
* (x
* (
sqrt ((y
^2 )
- 1)))))
+ ((x
* (
sqrt ((y
^2 )
- 1)))
^2 )))
.= (
sqrt ((((y
^2 )
* ((x
^2 )
- 1))
- ((2
* (y
* (
sqrt ((x
^2 )
- 1))))
* (x
* (
sqrt ((y
^2 )
- 1)))))
+ ((x
* (
sqrt ((y
^2 )
- 1)))
^2 ))) by
A7,
SQUARE_1:def 2
.= (
sqrt (((((x
* y)
^2 )
- (y
^2 ))
- ((2
* (y
* (
sqrt ((x
^2 )
- 1))))
* (x
* (
sqrt ((y
^2 )
- 1)))))
+ ((x
^2 )
* ((
sqrt ((y
^2 )
- 1))
^2 ))))
.= (
sqrt (((((x
* y)
^2 )
- (y
^2 ))
- ((2
* (y
* (
sqrt ((x
^2 )
- 1))))
* (x
* (
sqrt ((y
^2 )
- 1)))))
+ ((x
^2 )
* ((y
^2 )
- 1)))) by
A5,
SQUARE_1:def 2
.= (
sqrt ((((2
* ((x
* y)
^2 ))
- (x
^2 ))
- (y
^2 ))
- (((2
* x)
* y)
* ((
sqrt ((x
^2 )
- 1))
* (
sqrt ((y
^2 )
- 1))))))
.= (
sqrt ((((2
* ((x
* y)
^2 ))
- (x
^2 ))
- (y
^2 ))
- (((2
* x)
* y)
* (
sqrt (((x
^2 )
- 1)
* ((y
^2 )
- 1)))))) by
A7,
A5,
SQUARE_1: 29;
hence thesis by
A9,
A8;
end;
theorem ::
SIN_COS7:56
(x
^2 )
< 1 & (y
^2 )
< 1 implies ((
tanh" x)
+ (
tanh" y))
= (
tanh" ((x
+ y)
/ (1
+ (x
* y))))
proof
assume
A1: (x
^2 )
< 1 & (y
^2 )
< 1;
then
A2:
0
< ((1
+ x)
/ (1
- x)) &
0
< ((1
+ y)
/ (1
- y)) by
Lm4;
A3: ((
tanh" x)
+ (
tanh" y))
= ((1
/ 2)
* ((
log (
number_e ,((1
+ x)
/ (1
- x))))
+ (
log (
number_e ,((1
+ y)
/ (1
- y))))))
.= ((1
/ 2)
* (
log (
number_e ,(((1
+ x)
/ (1
- x))
* ((1
+ y)
/ (1
- y)))))) by
A2,
Lm1,
POWER: 53,
TAYLOR_1: 11
.= ((1
/ 2)
* (
log (
number_e ,(((1
+ x)
* (1
+ y))
/ ((1
- x)
* (1
- y)))))) by
XCMPLX_1: 76
.= ((1
/ 2)
* (
log (
number_e ,((((1
+ x)
+ y)
+ (x
* y))
/ (((1
+ (x
* y))
- x)
- y)))));
A4: ((x
* y)
+ 1)
<>
0 by
A1,
Th27;
then (
tanh" ((x
+ y)
/ (1
+ (x
* y))))
= ((1
/ 2)
* (
log (
number_e ,((((x
+ y)
+ ((1
+ (x
* y))
* 1))
/ (1
+ (x
* y)))
/ (1
- ((x
+ y)
/ (1
+ (x
* y)))))))) by
XCMPLX_1: 113
.= ((1
/ 2)
* (
log (
number_e ,(((((x
+ y)
+ 1)
+ (x
* y))
/ (1
+ (x
* y)))
/ (((1
* (1
+ (x
* y)))
- (x
+ y))
/ (1
+ (x
* y))))))) by
A4,
XCMPLX_1: 127
.= ((1
/ 2)
* (
log (
number_e ,((((1
+ x)
+ y)
+ (x
* y))
/ (((1
+ (x
* y))
- x)
- y))))) by
A4,
XCMPLX_1: 55;
hence thesis by
A3;
end;
theorem ::
SIN_COS7:57
(x
^2 )
< 1 & (y
^2 )
< 1 implies ((
tanh" x)
- (
tanh" y))
= (
tanh" ((x
- y)
/ (1
- (x
* y))))
proof
assume
A1: (x
^2 )
< 1 & (y
^2 )
< 1;
then
A2:
0
< ((1
+ x)
/ (1
- x)) &
0
< ((1
+ y)
/ (1
- y)) by
Lm4;
A3: ((
tanh" x)
- (
tanh" y))
= ((1
/ 2)
* ((
log (
number_e ,((1
+ x)
/ (1
- x))))
- (
log (
number_e ,((1
+ y)
/ (1
- y))))))
.= ((1
/ 2)
* (
log (
number_e ,(((1
+ x)
/ (1
- x))
/ ((1
+ y)
/ (1
- y)))))) by
A2,
Lm1,
POWER: 54,
TAYLOR_1: 11
.= ((1
/ 2)
* (
log (
number_e ,(((1
+ x)
* (1
- y))
/ ((1
- x)
* (1
+ y)))))) by
XCMPLX_1: 84
.= ((1
/ 2)
* (
log (
number_e ,((((1
- y)
+ x)
- (x
* y))
/ (((1
+ y)
- x)
- (x
* y))))));
A4: (1
- (x
* y))
<>
0 by
A1,
Th28;
then (
tanh" ((x
- y)
/ (1
- (x
* y))))
= ((1
/ 2)
* (
log (
number_e ,((((x
- y)
+ ((1
- (x
* y))
* 1))
/ (1
- (x
* y)))
/ (1
- ((x
- y)
/ (1
- (x
* y)))))))) by
XCMPLX_1: 113
.= ((1
/ 2)
* (
log (
number_e ,(((((x
- y)
+ 1)
- (x
* y))
/ (1
- (x
* y)))
/ (((1
* (1
- (x
* y)))
- (x
- y))
/ (1
- (x
* y))))))) by
A4,
XCMPLX_1: 127
.= ((1
/ 2)
* (
log (
number_e ,((((1
- y)
+ x)
- (x
* y))
/ (((1
+ y)
- x)
- (x
* y)))))) by
A4,
XCMPLX_1: 55;
hence thesis by
A3;
end;
theorem ::
SIN_COS7:58
0
< x implies (
log (
number_e ,x))
= (2
* (
tanh" ((x
- 1)
/ (x
+ 1))))
proof
assume
A1:
0
< x;
then (2
* (
tanh" ((x
- 1)
/ (x
+ 1))))
= (
log (
number_e ,((((x
- 1)
+ ((x
+ 1)
* 1))
/ (x
+ 1))
/ (1
- ((x
- 1)
/ (x
+ 1)))))) by
XCMPLX_1: 113
.= (
log (
number_e ,(((2
* x)
/ (x
+ 1))
/ (((1
* (x
+ 1))
- (x
- 1))
/ (x
+ 1))))) by
A1,
XCMPLX_1: 127
.= (
log (
number_e ,((2
* x)
/ 2))) by
A1,
XCMPLX_1: 55
.= (
log (
number_e ,x));
hence thesis;
end;
theorem ::
SIN_COS7:59
0
< x implies (
log (
number_e ,x))
= (
tanh" (((x
^2 )
- 1)
/ ((x
^2 )
+ 1)))
proof
assume
A1:
0
< x;
A2: ((x
^2 )
+ 1)
>
0 by
Lm6;
then (
tanh" (((x
^2 )
- 1)
/ ((x
^2 )
+ 1)))
= ((1
/ 2)
* (
log (
number_e ,(((((x
^2 )
- 1)
+ (((x
^2 )
+ 1)
* 1))
/ ((x
^2 )
+ 1))
/ (1
- (((x
^2 )
- 1)
/ ((x
^2 )
+ 1))))))) by
XCMPLX_1: 113
.= ((1
/ 2)
* (
log (
number_e ,(((2
* (x
^2 ))
/ ((x
^2 )
+ 1))
/ (((1
* ((x
^2 )
+ 1))
- ((x
^2 )
- 1))
/ ((x
^2 )
+ 1)))))) by
A2,
XCMPLX_1: 127
.= ((1
/ 2)
* (
log (
number_e ,((2
* (x
^2 ))
/ 2)))) by
A2,
XCMPLX_1: 55
.= ((1
/ 2)
* (
log (
number_e ,(x
to_power 2)))) by
POWER: 46
.= ((1
/ 2)
* (2
* (
log (
number_e ,x)))) by
A1,
Lm1,
POWER: 55,
TAYLOR_1: 11
.= (
log (
number_e ,x));
hence thesis;
end;
theorem ::
SIN_COS7:60
1
< x implies (
log (
number_e ,x))
= (
cosh1" (((x
^2 )
+ 1)
/ (2
* x)))
proof
assume
A1: 1
< x;
then x
< (x
^2 ) by
SQUARE_1: 14;
then 1
< (x
^2 ) by
A1,
XXREAL_0: 2;
then
A2: (1
- 1)
< ((x
^2 )
- 1) by
XREAL_1: 14;
(1
* 2)
< (2
* x) by
A1,
XREAL_1: 68;
then 1
< (2
* x) by
XXREAL_0: 2;
then
A3: (1
^2 )
< ((2
* x)
^2 ) by
SQUARE_1: 16;
(
cosh1" (((x
^2 )
+ 1)
/ (2
* x)))
= (
log (
number_e ,((((x
^2 )
+ 1)
/ (2
* x))
+ (
sqrt (((((x
^2 )
+ 1)
^2 )
/ ((2
* x)
^2 ))
- 1))))) by
XCMPLX_1: 76
.= (
log (
number_e ,((((x
^2 )
+ 1)
/ (2
* x))
+ (
sqrt ((((((x
^2 )
^2 )
+ (2
* (x
^2 )))
+ 1)
- (1
* ((2
* x)
^2 )))
/ ((2
* x)
^2 )))))) by
A3,
XCMPLX_1: 126
.= (
log (
number_e ,((((x
^2 )
+ 1)
/ (2
* x))
+ ((
sqrt (((x
^2 )
- 1)
^2 ))
/ (
sqrt ((2
* x)
^2 )))))) by
A1,
A2,
SQUARE_1: 30
.= (
log (
number_e ,((((x
^2 )
+ 1)
/ (2
* x))
+ (((x
^2 )
- 1)
/ (
sqrt ((2
* x)
^2 )))))) by
A2,
SQUARE_1: 22
.= (
log (
number_e ,((((x
^2 )
+ 1)
/ (2
* x))
+ (((x
^2 )
- 1)
/ (2
* x))))) by
A1,
SQUARE_1: 22
.= (
log (
number_e ,((((x
^2 )
+ 1)
+ ((x
^2 )
- 1))
/ (2
* x))))
.= (
log (
number_e ,((2
* (x
^2 ))
/ (2
* x))))
.= (
log (
number_e ,((x
* x)
/ x))) by
XCMPLX_1: 91
.= (
log (
number_e ,(x
/ (x
/ x)))) by
XCMPLX_1: 77
.= (
log (
number_e ,(x
/ 1))) by
A1,
XCMPLX_1: 60
.= (
log (
number_e ,x));
hence thesis;
end;
theorem ::
SIN_COS7:61
0
< x & x
< 1 & 1
<= (((x
^2 )
+ 1)
/ (2
* x)) implies (
log (
number_e ,x))
= (
cosh2" (((x
^2 )
+ 1)
/ (2
* x)))
proof
assume that
A1:
0
< x and
A2: x
< 1 and 1
<= (((x
^2 )
+ 1)
/ (2
* x));
A3: (1
/ x)
= (x
to_power (
- 1)) by
A1,
Th1;
(x
^2 )
< x by
A1,
A2,
SQUARE_1: 13;
then (x
^2 )
< 1 by
A2,
XXREAL_0: 2;
then
A4: ((x
^2 )
- (x
^2 ))
< (1
- (x
^2 )) by
XREAL_1: 14;
(
0
* 2)
< (x
* 2) by
A1;
then
A5:
0
< ((2
* x)
^2 );
(
cosh2" (((x
^2 )
+ 1)
/ (2
* x)))
= (
- (
log (
number_e ,((((x
^2 )
+ 1)
/ (2
* x))
+ (
sqrt (((((x
^2 )
+ 1)
^2 )
/ ((2
* x)
^2 ))
- 1)))))) by
XCMPLX_1: 76
.= (
- (
log (
number_e ,((((x
^2 )
+ 1)
/ (2
* x))
+ (
sqrt ((((((x
^2 )
^2 )
+ (2
* (x
^2 )))
+ 1)
- (1
* ((2
* x)
^2 )))
/ ((2
* x)
^2 ))))))) by
A5,
XCMPLX_1: 126
.= (
- (
log (
number_e ,((((x
^2 )
+ 1)
/ (2
* x))
+ ((
sqrt ((1
- (x
^2 ))
^2 ))
/ (
sqrt ((2
* x)
^2 ))))))) by
A1,
A4,
SQUARE_1: 30
.= (
- (
log (
number_e ,((((x
^2 )
+ 1)
/ (2
* x))
+ ((1
- (x
^2 ))
/ (
sqrt ((2
* x)
^2 ))))))) by
A4,
SQUARE_1: 22
.= (
- (
log (
number_e ,((((x
^2 )
+ 1)
/ (2
* x))
+ ((1
- (x
^2 ))
/ (2
* x)))))) by
A1,
SQUARE_1: 22
.= (
- (
log (
number_e ,((((x
^2 )
+ 1)
+ (1
- (x
^2 )))
/ (2
* x)))))
.= (
- (
log (
number_e ,((2
* 1)
/ (2
* x)))))
.= (
- (
log (
number_e ,(1
/ x)))) by
XCMPLX_1: 91
.= (
- ((
- 1)
* (
log (
number_e ,x)))) by
A1,
A3,
Lm1,
POWER: 55,
TAYLOR_1: 11
.= (
log (
number_e ,x));
hence thesis;
end;
theorem ::
SIN_COS7:62
0
< x implies (
log (
number_e ,x))
= (
sinh" (((x
^2 )
- 1)
/ (2
* x)))
proof
A1: (x
^2 )
>=
0 by
XREAL_1: 63;
assume
A2:
0
< x;
then (
0
* 2)
< (x
* 2);
then
A3:
0
< ((2
* x)
^2 );
(
sinh" (((x
^2 )
- 1)
/ (2
* x)))
= (
log (
number_e ,((((x
^2 )
- 1)
/ (2
* x))
+ (
sqrt (((((x
^2 )
- 1)
^2 )
/ ((2
* x)
^2 ))
+ 1))))) by
XCMPLX_1: 76
.= (
log (
number_e ,((((x
^2 )
- 1)
/ (2
* x))
+ (
sqrt ((((((x
^2 )
^2 )
- (2
* (x
^2 )))
+ 1)
+ (((2
* x)
^2 )
* 1))
/ ((2
* x)
^2 )))))) by
A3,
XCMPLX_1: 113
.= (
log (
number_e ,((((x
^2 )
- 1)
/ (2
* x))
+ ((
sqrt (((x
^2 )
+ 1)
^2 ))
/ (
sqrt ((2
* x)
^2 )))))) by
A2,
SQUARE_1: 30
.= (
log (
number_e ,((((x
^2 )
- 1)
/ (2
* x))
+ (((x
^2 )
+ 1)
/ (
sqrt ((2
* x)
^2 )))))) by
A1,
SQUARE_1: 22
.= (
log (
number_e ,((((x
^2 )
- 1)
/ (2
* x))
+ (((x
^2 )
+ 1)
/ (2
* x))))) by
A2,
SQUARE_1: 22
.= (
log (
number_e ,((((x
^2 )
- 1)
+ ((x
^2 )
+ 1))
/ (2
* x))))
.= (
log (
number_e ,((2
* (x
^2 ))
/ (2
* x))))
.= (
log (
number_e ,((x
* x)
/ x))) by
XCMPLX_1: 91
.= (
log (
number_e ,(x
/ (x
/ x)))) by
XCMPLX_1: 77
.= (
log (
number_e ,(x
/ 1))) by
A2,
XCMPLX_1: 60
.= (
log (
number_e ,x));
hence thesis;
end;
theorem ::
SIN_COS7:63
y
= ((1
/ 2)
* ((
exp_R x)
- (
exp_R (
- x)))) implies x
= (
log (
number_e ,(y
+ (
sqrt ((y
^2 )
+ 1)))))
proof
A1: (
exp_R x)
>
0 by
SIN_COS: 55;
set t = (
exp_R x);
A2: (
delta (1,(
- (2
* y)),(
- 1)))
= ((((
- 2)
* y)
^2 )
- ((4
* 1)
* (
- 1))) by
QUIN_1:def 1
.= ((4
* (y
^2 ))
+ 4);
A3:
0
<= (y
^2 ) by
XREAL_1: 63;
assume y
= ((1
/ 2)
* ((
exp_R x)
- (
exp_R (
- x))));
then ((2
* y)
* (
exp_R x))
= (((
exp_R x)
- (1
/ (
exp_R x)))
* (
exp_R x)) by
TAYLOR_1: 4;
then ((2
* y)
* t)
= ((t
^2 )
- ((t
* 1)
/ t));
then (((2
* y)
* t)
- ((2
* y)
* t))
= (((t
^2 )
- 1)
- ((2
* y)
* t)) by
A1,
XCMPLX_1: 60;
then (((1
* (t
^2 ))
+ ((
- (2
* y))
* t))
+ (
- 1))
=
0 ;
then t
= (((
- (
- (2
* y)))
+ (
sqrt (
delta (1,(
- (2
* y)),(
- 1)))))
/ (2
* 1)) or t
= (((
- (
- (2
* y)))
- (
sqrt (
delta (1,(
- (2
* y)),(
- 1)))))
/ (2
* 1)) by
A2,
A3,
QUIN_1: 15;
then t
= (((2
* y)
+ ((
sqrt 4)
* (
sqrt ((y
^2 )
+ 1))))
/ 2) or t
= (((2
* y)
- (
sqrt (4
* ((y
^2 )
+ 1))))
/ 2) by
A2,
A3,
SQUARE_1: 29;
then t
= (((2
* y)
+ (2
* (
sqrt ((y
^2 )
+ 1))))
/ 2) or t
= (((2
* y)
- (2
* (
sqrt ((y
^2 )
+ 1))))
/ 2) by
A3,
SQUARE_1: 20,
SQUARE_1: 29;
then
A4: (
exp_R x)
= (y
+ (
sqrt ((y
^2 )
+ 1))) or (
exp_R x)
= (y
- (
sqrt ((y
^2 )
+ 1)));
y
< ((
sqrt ((y
^2 )
+ 1))
+
0 ) by
Lm8;
hence thesis by
A1,
A4,
TAYLOR_1: 12,
XREAL_1: 19;
end;
theorem ::
SIN_COS7:64
y
= ((1
/ 2)
* ((
exp_R x)
+ (
exp_R (
- x)))) & 1
<= y implies x
= (
log (
number_e ,(y
+ (
sqrt ((y
^2 )
- 1))))) or x
= (
- (
log (
number_e ,(y
+ (
sqrt ((y
^2 )
- 1))))))
proof
assume that
A1: y
= ((1
/ 2)
* ((
exp_R x)
+ (
exp_R (
- x)))) and
A2: 1
<= y;
A3: (y
+ (
sqrt ((y
^2 )
- 1)))
>
0 by
A2,
Lm10;
set t = (
exp_R x);
((2
* y)
* (
exp_R x))
= (((
exp_R x)
+ (1
/ (
exp_R x)))
* (
exp_R x)) by
A1,
TAYLOR_1: 4;
then
0
< (
exp_R x) & ((2
* y)
* t)
= ((t
^2 )
+ ((t
* 1)
/ t)) by
SIN_COS: 55;
then (((2
* y)
* t)
- ((2
* y)
* t))
= (((t
^2 )
+ 1)
- ((2
* y)
* t)) by
XCMPLX_1: 60;
then
A4:
0
= (((1
* (t
^2 ))
+ ((
- (2
* y))
* t))
+ 1);
A5: (
delta (1,(
- (2
* y)),1))
= ((((
- 2)
* y)
^2 )
- ((4
* 1)
* 1)) by
QUIN_1:def 1
.= ((4
* (y
^2 ))
- 4);
A6:
0
<= ((y
^2 )
- 1) by
A2,
Lm3;
then (
0
* 4)
<= (((y
^2 )
- 1)
* 4);
then t
= (((
- (
- (2
* y)))
+ (
sqrt (
delta (1,(
- (2
* y)),1))))
/ (2
* 1)) or t
= (((
- (
- (2
* y)))
- (
sqrt (
delta (1,(
- (2
* y)),1))))
/ (2
* 1)) by
A4,
A5,
QUIN_1: 15;
then t
= (((2
* y)
+ ((
sqrt 4)
* (
sqrt ((y
^2 )
- 1))))
/ 2) or t
= (((2
* y)
- (
sqrt (4
* ((y
^2 )
- 1))))
/ 2) by
A6,
A5,
SQUARE_1: 29;
then t
= (((2
* y)
+ (2
* (
sqrt ((y
^2 )
- 1))))
/ 2) or t
= (((2
* y)
- (2
* (
sqrt ((y
^2 )
- 1))))
/ 2) by
A6,
SQUARE_1: 20,
SQUARE_1: 29;
then (
log (
number_e ,(y
+ (
sqrt ((y
^2 )
- 1)))))
= x or (
log (
number_e ,(y
- (
sqrt ((y
^2 )
- 1)))))
= x by
TAYLOR_1: 12;
then (
log (
number_e ,(y
+ (
sqrt ((y
^2 )
- 1)))))
= x or (
log (
number_e ,(((y
- (
sqrt ((y
^2 )
- 1)))
* (y
+ (
sqrt ((y
^2 )
- 1))))
/ (y
+ (
sqrt ((y
^2 )
- 1))))))
= x by
A3,
XCMPLX_1: 89;
then (
log (
number_e ,(y
+ (
sqrt ((y
^2 )
- 1)))))
= x or (
log (
number_e ,(((y
^2 )
- ((
sqrt ((y
^2 )
- 1))
^2 ))
/ (y
+ (
sqrt ((y
^2 )
- 1))))))
= x;
then
A7: (
log (
number_e ,(y
+ (
sqrt ((y
^2 )
- 1)))))
= x or (
log (
number_e ,(((y
^2 )
- ((y
^2 )
- 1))
/ (y
+ (
sqrt ((y
^2 )
- 1))))))
= x by
A6,
SQUARE_1:def 2;
(1
/ (y
+ (
sqrt ((y
^2 )
- 1))))
= ((y
+ (
sqrt ((y
^2 )
- 1)))
to_power (
- 1)) by
A3,
Th1;
then (
log (
number_e ,(y
+ (
sqrt ((y
^2 )
- 1)))))
= x or ((
- 1)
* (
log (
number_e ,(y
+ (
sqrt ((y
^2 )
- 1))))))
= x by
A3,
A7,
Lm1,
POWER: 55,
TAYLOR_1: 11;
hence thesis;
end;
theorem ::
SIN_COS7:65
y
= (((
exp_R x)
- (
exp_R (
- x)))
/ ((
exp_R x)
+ (
exp_R (
- x)))) implies x
= ((1
/ 2)
* (
log (
number_e ,((1
+ y)
/ (1
- y)))))
proof
A1:
0
< (
exp_R x) by
SIN_COS: 55;
set t = (
exp_R x);
assume y
= (((
exp_R x)
- (
exp_R (
- x)))
/ ((
exp_R x)
+ (
exp_R (
- x))));
then y
= (((
exp_R x)
- (1
/ (
exp_R x)))
/ ((
exp_R x)
+ (
exp_R (
- x)))) by
TAYLOR_1: 4;
then y
= (((
exp_R x)
- (1
/ (
exp_R x)))
/ ((
exp_R x)
+ (1
/ (
exp_R x)))) by
TAYLOR_1: 4;
then y
= (((((
exp_R x)
* (
exp_R x))
- 1)
/ (
exp_R x))
/ ((
exp_R x)
+ (1
/ (
exp_R x)))) by
A1,
XCMPLX_1: 127;
then y
= (((((
exp_R x)
^2 )
- 1)
/ (
exp_R x))
/ ((1
+ ((
exp_R x)
* (
exp_R x)))
/ (
exp_R x))) by
A1,
XCMPLX_1: 113;
then
A2: y
= ((((
exp_R x)
^2 )
- 1)
/ (1
+ ((
exp_R x)
^2 ))) by
A1,
XCMPLX_1: 55;
then ((1
* y)
+ ((t
^2 )
* y))
= ((((t
^2 )
- 1)
/ (1
+ (t
^2 )))
* (1
+ (t
^2 )));
then ((y
+ ((t
^2 )
* y))
- ((t
^2 )
- 1))
= (((t
^2 )
- 1)
- ((t
^2 )
- 1)) by
A1,
XCMPLX_1: 87;
then (((t
^2 )
* (y
- 1))
/ (y
- 1))
= ((
- (y
+ 1))
/ (y
- 1));
then
A3: (((t
^2 )
* (y
- 1))
/ (y
- 1))
= ((y
+ 1)
/ (
- (y
- 1))) by
XCMPLX_1: 192;
(y
- 1)
<>
0 by
A2,
Th31;
then (
sqrt (t
^2 ))
= (
sqrt ((y
+ 1)
/ (1
- y))) by
A3,
XCMPLX_1: 89;
then
A4: (
exp_R x)
= (
sqrt ((y
+ 1)
/ (1
- y))) by
A1,
SQUARE_1: 22;
(
- 1)
< y by
A2,
Lm11,
SIN_COS: 55;
then
A5:
0
< ((y
+ 1)
/ (1
- y)) by
A2,
Th31,
Th32;
then (
sqrt ((y
+ 1)
/ (1
- y)))
= (((y
+ 1)
/ (1
- y))
to_power (1
/ 2)) by
ASYMPT_1: 83;
then (
log (
number_e ,(((y
+ 1)
/ (1
- y))
to_power (1
/ 2))))
= x by
A4,
TAYLOR_1: 12;
hence thesis by
A5,
Lm1,
POWER: 55,
TAYLOR_1: 11;
end;
theorem ::
SIN_COS7:66
y
= (((
exp_R x)
+ (
exp_R (
- x)))
/ ((
exp_R x)
- (
exp_R (
- x)))) & x
<>
0 implies x
= ((1
/ 2)
* (
log (
number_e ,((y
+ 1)
/ (y
- 1)))))
proof
A1:
0
< (
exp_R x) by
SIN_COS: 55;
set t = (
exp_R x);
assume that
A2: y
= (((
exp_R x)
+ (
exp_R (
- x)))
/ ((
exp_R x)
- (
exp_R (
- x)))) and
A3: x
<>
0 ;
y
= (((
exp_R x)
+ (1
/ (
exp_R x)))
/ ((
exp_R x)
- (
exp_R (
- x)))) by
A2,
TAYLOR_1: 4;
then y
= (((
exp_R x)
+ (1
/ (
exp_R x)))
/ ((
exp_R x)
- (1
/ (
exp_R x)))) by
TAYLOR_1: 4;
then y
= (((
exp_R x)
+ (1
/ (
exp_R x)))
/ ((((
exp_R x)
* (
exp_R x))
- 1)
/ (
exp_R x))) by
A1,
XCMPLX_1: 127;
then y
= (((1
+ ((
exp_R x)
* (
exp_R x)))
/ (
exp_R x))
/ ((((
exp_R x)
^2 )
- 1)
/ (
exp_R x))) by
A1,
XCMPLX_1: 113;
then
A4: y
= ((1
+ ((
exp_R x)
^2 ))
/ (((
exp_R x)
^2 )
- 1)) by
A1,
XCMPLX_1: 55;
then (y
* ((t
^2 )
- 1))
= (1
+ (t
^2 )) by
A3,
Th30,
XCMPLX_1: 87;
then
A5: (((t
^2 )
* (y
- 1))
/ (y
- 1))
= ((y
+ 1)
/ (y
- 1));
(
exp_R x)
<> 1 by
A3,
Th29;
then
A6: 1
< y or y
< (
- 1) by
A4,
Lm12,
SIN_COS: 55;
then (1
- 1)
< (y
- 1) or (y
- 1)
< ((
- 1)
- 1) by
XREAL_1: 14;
then (
sqrt (t
^2 ))
= (
sqrt ((y
+ 1)
/ (y
- 1))) by
A5,
XCMPLX_1: 89;
then
A7: (
exp_R x)
= (
sqrt ((y
+ 1)
/ (y
- 1))) by
A1,
SQUARE_1: 22;
A8:
0
< ((y
+ 1)
/ (y
- 1)) by
A6,
Lm7;
then (
sqrt ((y
+ 1)
/ (y
- 1)))
= (((y
+ 1)
/ (y
- 1))
to_power (1
/ 2)) by
ASYMPT_1: 83;
then (
log (
number_e ,(((y
+ 1)
/ (y
- 1))
to_power (1
/ 2))))
= x by
A7,
TAYLOR_1: 12;
hence thesis by
A8,
Lm1,
POWER: 55,
TAYLOR_1: 11;
end;
theorem ::
SIN_COS7:67
y
= (1
/ (((
exp_R x)
+ (
exp_R (
- x)))
/ 2)) implies x
= (
log (
number_e ,((1
+ (
sqrt (1
- (y
^2 ))))
/ y))) or x
= (
- (
log (
number_e ,((1
+ (
sqrt (1
- (y
^2 ))))
/ y))))
proof
set t = (
exp_R x);
A1: (
delta (y,(
- 2),y))
= (((
- 2)
^2 )
- ((4
* y)
* y)) by
QUIN_1:def 1
.= (4
- (4
* (y
^2 )));
assume y
= (1
/ (((
exp_R x)
+ (
exp_R (
- x)))
/ 2));
then y
= ((1
* 2)
/ (2
* (((
exp_R x)
+ (
exp_R (
- x)))
/ 2))) by
XCMPLX_1: 91;
then
0
< (
exp_R x) & y
= (2
/ ((
exp_R x)
+ (1
/ (
exp_R x)))) by
SIN_COS: 55,
TAYLOR_1: 4;
then y
= (2
/ ((1
+ ((
exp_R x)
* (
exp_R x)))
/ (
exp_R x))) by
XCMPLX_1: 113;
then y
= (2
* ((
exp_R x)
/ (1
+ ((
exp_R x)
^2 )))) by
XCMPLX_1: 79;
then
A2: y
= ((2
* t)
/ (1
+ (t
^2 )));
then
A3:
0
< y by
Lm13,
SIN_COS: 55;
(1
+ (t
^2 ))
>
0 by
Lm6;
then
A4: (y
* (1
+ (t
^2 )))
= (2
* t) by
A2,
XCMPLX_1: 87;
A5: y
<= 1 by
A2,
Lm14,
SIN_COS: 55;
then
A6:
0
<= (1
- (y
^2 )) by
A3,
Lm16;
(
Polynom (y,(
- 2),y,t))
= (((y
* (t
^2 ))
+ ((
- 2)
* t))
+ y) by
POLYEQ_1:def 2;
then t
= (((
- (
- 2))
+ (
sqrt (
delta (y,(
- 2),y))))
/ (2
* y)) or t
= (((
- (
- 2))
- (
sqrt (
delta (y,(
- 2),y))))
/ (2
* y)) by
A3,
A5,
A4,
A1,
Lm17,
QUIN_1: 15;
then t
= ((2
+ (
sqrt (4
* (1
- (y
^2 )))))
/ (2
* y)) or t
= ((2
- (
sqrt (4
* (1
- (y
^2 )))))
/ (2
* y)) by
A1;
then t
= ((2
+ (2
* (
sqrt (1
- (y
^2 )))))
/ (2
* y)) or t
= ((2
- (2
* (
sqrt (1
- (y
^2 )))))
/ (2
* y)) by
A6,
SQUARE_1: 20,
SQUARE_1: 29;
then t
= ((2
* (1
+ (
sqrt (1
- (y
^2 )))))
/ (2
* y)) or t
= ((2
* (1
- (
sqrt (1
- (y
^2 )))))
/ (2
* y));
then
A7: t
= ((1
+ (
sqrt (1
- (y
^2 ))))
/ y) or t
= ((1
- (
sqrt (1
- (y
^2 ))))
/ y) by
XCMPLX_1: 91;
0
< (1
+ (
sqrt (1
- (y
^2 )))) by
A3,
A5,
Lm18;
then t
= ((1
+ (
sqrt (1
- (y
^2 ))))
/ y) or t
= (((1
- (
sqrt (1
- (y
^2 ))))
* (1
+ (
sqrt (1
- (y
^2 )))))
/ (y
* (1
+ (
sqrt (1
- (y
^2 )))))) by
A7,
XCMPLX_1: 91;
then t
= ((1
+ (
sqrt (1
- (y
^2 ))))
/ y) or t
= ((1
- ((
sqrt (1
- (y
^2 )))
^2 ))
/ (y
* (1
+ (
sqrt (1
- (y
^2 ))))));
then t
= ((1
+ (
sqrt (1
- (y
^2 ))))
/ y) or t
= ((1
- (1
- (y
^2 )))
/ (y
* (1
+ (
sqrt (1
- (y
^2 )))))) by
A6,
SQUARE_1:def 2;
then
A8: t
= ((1
+ (
sqrt (1
- (y
^2 ))))
/ y) or t
= (y
/ (1
+ (
sqrt (1
- (y
^2 ))))) by
A3,
XCMPLX_1: 91;
(
log (
number_e ,(
exp_R x)))
= x & (1
/ ((1
+ (
sqrt (1
- (y
^2 ))))
/ y))
= (((1
+ (
sqrt (1
- (y
^2 ))))
/ y)
to_power (
- 1)) by
A3,
A5,
Lm19,
Th1,
TAYLOR_1: 12;
then
A9: (
log (
number_e ,((1
+ (
sqrt (1
- (y
^2 ))))
/ y)))
= x or (
log (
number_e ,(((1
+ (
sqrt (1
- (y
^2 ))))
/ y)
to_power (
- 1))))
= x by
A8,
XCMPLX_1: 57;
0
< ((1
+ (
sqrt (1
- (y
^2 ))))
/ y) by
A3,
A5,
Lm19;
then (
log (
number_e ,((1
+ (
sqrt (1
- (y
^2 ))))
/ y)))
= x or ((
- 1)
* (
log (
number_e ,((1
+ (
sqrt (1
- (y
^2 ))))
/ y))))
= x by
A9,
Lm1,
POWER: 55,
TAYLOR_1: 11;
hence thesis;
end;
theorem ::
SIN_COS7:68
y
= (1
/ (((
exp_R x)
- (
exp_R (
- x)))
/ 2)) & x
<>
0 implies x
= (
log (
number_e ,((1
+ (
sqrt (1
+ (y
^2 ))))
/ y))) or x
= (
log (
number_e ,((1
- (
sqrt (1
+ (y
^2 ))))
/ y)))
proof
A1:
0
< (
exp_R x) by
SIN_COS: 55;
set t = (
exp_R x);
assume that
A2: y
= (1
/ (((
exp_R x)
- (
exp_R (
- x)))
/ 2)) and
A3: x
<>
0 ;
A4: (
delta (y,(
- 2),(
- y)))
= (((
- 2)
^2 )
- ((4
* y)
* (
- y))) by
QUIN_1:def 1
.= (4
+ (4
* (y
^2 )));
y
= ((1
* 2)
/ (2
* (((
exp_R x)
- (
exp_R (
- x)))
/ 2))) by
A2,
XCMPLX_1: 91;
then y
= (2
/ ((
exp_R x)
- (1
/ (
exp_R x)))) by
TAYLOR_1: 4;
then y
= (2
/ ((((
exp_R x)
* (
exp_R x))
- 1)
/ (
exp_R x))) by
A1,
XCMPLX_1: 127;
then
A5: y
= (2
* ((
exp_R x)
/ (((
exp_R x)
^2 )
- 1))) by
XCMPLX_1: 79;
then
A6: y
= ((2
* (
exp_R x))
/ (((
exp_R x)
^2 )
- 1));
then (y
* ((t
^2 )
- 1))
= (2
* t) by
A3,
Th30,
XCMPLX_1: 87;
then
A7: (((y
* (t
^2 ))
+ ((
- 2)
* t))
+ (
- y))
=
0 ;
A8: (
exp_R x)
<> 1 by
A3,
Th29;
then
A9: ((2
* (
exp_R x))
/ (((
exp_R x)
^2 )
- 1))
<>
0 by
Lm20,
SIN_COS: 55;
per cases by
A9,
A5;
suppose
A10:
0
< y;
A11:
0
< (1
+ (y
^2 )) by
Lm6;
then (
0
* 4)
< (4
* (1
+ (y
^2 )));
then t
= ((2
+ (
sqrt (
delta (y,(
- 2),(
- y)))))
/ (2
* y)) or t
= (((
- (
- 2))
- (
sqrt (
delta (y,(
- 2),(
- y)))))
/ (2
* y)) by
A1,
A8,
A6,
A7,
A4,
Lm20,
QUIN_1: 15;
then t
= ((2
+ ((
sqrt 4)
* (
sqrt (1
+ (y
^2 )))))
/ (2
* y)) or t
= ((2
- (
sqrt (4
* (1
+ (y
^2 )))))
/ (2
* y)) by
A4,
A11,
SQUARE_1: 29;
then t
= ((2
* (1
+ (
sqrt (1
+ (y
^2 )))))
/ (2
* y)) or t
= ((2
- (2
* (
sqrt (1
+ (y
^2 )))))
/ (2
* y)) by
A11,
SQUARE_1: 20,
SQUARE_1: 29;
then
A12: t
= ((1
+ (
sqrt (1
+ (y
^2 ))))
/ y) or t
= ((2
* (1
- (
sqrt (1
+ (y
^2 )))))
/ (2
* y)) by
XCMPLX_1: 91;
((1
- (
sqrt (1
+ (y
^2 ))))
/ y)
<
0 by
A10,
Lm15;
hence thesis by
A1,
A12,
TAYLOR_1: 12,
XCMPLX_1: 91;
end;
suppose
A13: y
<
0 ;
A14:
0
< (1
+ (y
^2 )) by
Lm6;
then (
0
* 4)
< (4
* (1
+ (y
^2 )));
then t
= ((2
+ (
sqrt (
delta (y,(
- 2),(
- y)))))
/ (2
* y)) or t
= (((
- (
- 2))
- (
sqrt (
delta (y,(
- 2),(
- y)))))
/ (2
* y)) by
A1,
A8,
A6,
A7,
A4,
Lm20,
QUIN_1: 15;
then t
= ((2
+ ((
sqrt 4)
* (
sqrt (1
+ (y
^2 )))))
/ (2
* y)) or t
= ((2
- (
sqrt (4
* (1
+ (y
^2 )))))
/ (2
* y)) by
A4,
A14,
SQUARE_1: 29;
then t
= ((2
* (1
+ (
sqrt (1
+ (y
^2 )))))
/ (2
* y)) or t
= ((2
- (2
* (
sqrt (1
+ (y
^2 )))))
/ (2
* y)) by
A14,
SQUARE_1: 20,
SQUARE_1: 29;
then
A15: t
= ((1
+ (
sqrt (1
+ (y
^2 ))))
/ y) or t
= ((2
* (1
- (
sqrt (1
+ (y
^2 )))))
/ (2
* y)) by
XCMPLX_1: 91;
((1
+ (
sqrt (1
+ (y
^2 ))))
/ y)
<
0 by
A13,
Lm21;
then (
exp_R x)
= ((1
- (
sqrt (1
+ (y
^2 ))))
/ y) by
A15,
SIN_COS: 55,
XCMPLX_1: 91;
hence thesis by
TAYLOR_1: 12;
end;
end;
theorem ::
SIN_COS7:69
Th69: (
cosh
. (2
* x))
= (1
+ (2
* ((
sinh
. x)
^2 )))
proof
(2
* ((
sinh
. x)
^2 ))
= (2
* ((1
/ 2)
* ((
cosh
. (2
* x))
- 1))) by
SIN_COS2: 18;
hence thesis;
end;
theorem ::
SIN_COS7:70
Th70: ((
cosh
. x)
^2 )
= (1
+ ((
sinh
. x)
^2 ))
proof
(
cosh
. (2
* x))
= (
cosh
. (x
+ x))
.= (((
cosh
. x)
^2 )
+ ((
sinh
. x)
^2 )) by
SIN_COS2: 20;
then ((1
+ (2
* ((
sinh
. x)
^2 )))
- ((
sinh
. x)
^2 ))
= ((((
cosh
. x)
^2 )
+ ((
sinh
. x)
^2 ))
- ((
sinh
. x)
^2 )) by
Th69;
hence thesis;
end;
theorem ::
SIN_COS7:71
Th71: ((
sinh
. x)
^2 )
= (((
cosh
. x)
^2 )
- 1)
proof
((((
cosh
. x)
^2 )
- ((
sinh
. x)
^2 ))
- 1)
= (1
- 1) by
SIN_COS2: 14;
hence thesis;
end;
theorem ::
SIN_COS7:72
(
sinh (5
* x))
= (((5
* (
sinh x))
+ (20
* ((
sinh x)
|^ 3)))
+ (16
* ((
sinh x)
|^ 5)))
proof
set t = (
sinh
. x);
(
sinh (5
* x))
= (
sinh
. ((4
* x)
+ x)) by
SIN_COS2:def 2
.= (((
sinh
. (2
* (2
* x)))
* (
cosh
. x))
+ ((
cosh
. (4
* x))
* t)) by
SIN_COS2: 21
.= ((((2
* (
sinh
. (2
* x)))
* (
cosh
. (2
* x)))
* (
cosh
. x))
+ ((
cosh
. (4
* x))
* t)) by
SIN_COS2: 23
.= ((((2
* ((2
* t)
* (
cosh
. x)))
* (
cosh
. (2
* x)))
* (
cosh
. x))
+ ((
cosh
. (4
* x))
* t)) by
SIN_COS2: 23
.= ((((4
* t)
* ((
cosh
. x)
^2 ))
* (
cosh
. (2
* x)))
+ ((
cosh
. (4
* x))
* t))
.= ((((4
* t)
* ((
cosh
. x)
^2 ))
* (1
+ (2
* (t
^2 ))))
+ ((
cosh
. (2
* (2
* x)))
* t)) by
Th69
.= ((((4
* t)
* ((
cosh
. x)
^2 ))
* (1
+ (2
* (t
^2 ))))
+ ((1
+ (2
* ((
sinh
. (2
* x))
^2 )))
* t)) by
Th69
.= ((((4
* t)
* ((
cosh
. x)
^2 ))
* (1
+ (2
* (t
^2 ))))
+ ((1
+ (2
* (((2
* t)
* (
cosh
. x))
^2 )))
* t)) by
SIN_COS2: 23
.= (((((4
* t)
* ((
cosh
. x)
^2 ))
* (1
+ (2
* (t
^2 ))))
+ t)
+ (((8
* (t
^2 ))
* t)
* ((
cosh
. x)
^2 )))
.= (((((4
* t)
* ((
cosh
. x)
^2 ))
* (1
+ (2
* (t
^2 ))))
+ t)
+ (((8
* ((t
|^ 1)
* t))
* t)
* ((
cosh
. x)
^2 )))
.= (((((4
* t)
* ((
cosh
. x)
^2 ))
* (1
+ (2
* (t
^2 ))))
+ t)
+ (((8
* (t
|^ (1
+ 1)))
* t)
* ((
cosh
. x)
^2 ))) by
NEWTON: 6
.= (((((4
* t)
* ((
cosh
. x)
^2 ))
* (1
+ (2
* (t
^2 ))))
+ t)
+ ((8
* ((t
|^ 2)
* t))
* ((
cosh
. x)
^2 )))
.= (((((4
* t)
* ((
cosh
. x)
^2 ))
* (1
+ (2
* (t
^2 ))))
+ t)
+ ((8
* (t
|^ (2
+ 1)))
* ((
cosh
. x)
^2 ))) by
NEWTON: 6
.= ((((((4
* t)
* ((
cosh
. x)
^2 ))
* 1)
+ ((((4
* t)
* ((
cosh
. x)
^2 ))
* 2)
* (t
^2 )))
+ t)
+ ((8
* (t
|^ 3))
* ((
cosh
. x)
^2 )))
.= ((((((4
* t)
* (1
+ (t
^2 )))
* 1)
+ (((8
* t)
* ((
cosh
. x)
^2 ))
* (t
^2 )))
+ t)
+ ((8
* (t
|^ 3))
* ((
cosh
. x)
^2 ))) by
Th70
.= (((((4
* t)
+ (((4
* t)
* t)
* t))
+ (((8
* t)
* ((
cosh
. x)
^2 ))
* (t
^2 )))
+ (
sinh
. x))
+ ((8
* (t
|^ 3))
* ((
cosh
. x)
^2 )))
.= (((((4
* t)
+ (((4
* (t
|^ 1))
* t)
* t))
+ (((8
* t)
* ((
cosh
. x)
^2 ))
* (t
^2 )))
+ t)
+ ((8
* (t
|^ 3))
* ((
cosh
. x)
^2 )))
.= (((((4
* t)
+ ((4
* ((t
|^ 1)
* t))
* t))
+ (((8
* t)
* ((
cosh
. x)
^2 ))
* (t
^2 )))
+ t)
+ ((8
* (t
|^ 3))
* ((
cosh
. x)
^2 )))
.= (((((4
* t)
+ ((4
* (t
|^ (1
+ 1)))
* t))
+ (((8
* t)
* ((
cosh
. x)
^2 ))
* (t
^2 )))
+ t)
+ ((8
* (t
|^ 3))
* ((
cosh
. x)
^2 ))) by
NEWTON: 6
.= (((((4
* t)
+ (4
* ((t
|^ 2)
* t)))
+ (((8
* t)
* ((
cosh
. x)
^2 ))
* (t
^2 )))
+ t)
+ ((8
* (t
|^ 3))
* ((
cosh
. x)
^2 )))
.= (((((4
* t)
+ (4
* (t
|^ (2
+ 1))))
+ (((8
* t)
* ((
cosh
. x)
^2 ))
* (t
^2 )))
+ t)
+ ((8
* (t
|^ 3))
* ((
cosh
. x)
^2 ))) by
NEWTON: 6
.= (((((4
* t)
+ (4
* (t
|^ 3)))
+ ((((8
* t)
* t)
* t)
* ((
cosh
. x)
^2 )))
+ t)
+ ((8
* (t
|^ 3))
* ((
cosh
. x)
^2 )))
.= (((((4
* t)
+ (4
* (t
|^ 3)))
+ ((((8
* (t
|^ 1))
* t)
* t)
* ((
cosh
. x)
^2 )))
+ t)
+ ((8
* (t
|^ 3))
* ((
cosh
. x)
^2 )))
.= (((((4
* t)
+ (4
* (t
|^ 3)))
+ (((8
* ((t
|^ 1)
* t))
* t)
* ((
cosh
. x)
^2 )))
+ t)
+ ((8
* (t
|^ 3))
* ((
cosh
. x)
^2 )))
.= (((((4
* t)
+ (4
* (t
|^ 3)))
+ (((8
* (t
|^ (1
+ 1)))
* t)
* ((
cosh
. x)
^2 )))
+ t)
+ ((8
* (t
|^ 3))
* ((
cosh
. x)
^2 ))) by
NEWTON: 6
.= (((((4
* t)
+ (4
* (t
|^ 3)))
+ ((8
* ((t
|^ 2)
* t))
* ((
cosh
. x)
^2 )))
+ t)
+ ((8
* (t
|^ 3))
* ((
cosh
. x)
^2 )))
.= (((((4
* t)
+ (4
* (t
|^ 3)))
+ ((8
* (t
|^ (2
+ 1)))
* ((
cosh
. x)
^2 )))
+ t)
+ ((8
* (t
|^ 3))
* ((
cosh
. x)
^2 ))) by
NEWTON: 6
.= (((((4
* t)
+ (4
* (t
|^ 3)))
+ ((8
* (t
|^ 3))
* (1
+ (t
^2 ))))
+ t)
+ ((8
* (t
|^ 3))
* ((
cosh
. x)
^2 ))) by
Th70
.= ((((((4
* t)
+ (4
* (t
|^ 3)))
+ (8
* (t
|^ 3)))
+ ((8
* ((t
|^ 3)
* t))
* t))
+ t)
+ ((8
* (t
|^ 3))
* ((
cosh
. x)
^2 )))
.= ((((((4
* t)
+ (4
* (t
|^ 3)))
+ (8
* (t
|^ 3)))
+ ((8
* (t
|^ (3
+ 1)))
* t))
+ t)
+ ((8
* (t
|^ 3))
* ((
cosh
. x)
^2 ))) by
NEWTON: 6
.= ((((((4
* t)
+ (4
* (t
|^ 3)))
+ (8
* (t
|^ 3)))
+ (8
* ((t
|^ 4)
* t)))
+ t)
+ ((8
* (t
|^ 3))
* ((
cosh
. x)
^2 )))
.= ((((((4
* t)
+ (4
* (t
|^ 3)))
+ (8
* (t
|^ 3)))
+ (8
* (t
|^ (4
+ 1))))
+ t)
+ ((8
* (t
|^ 3))
* ((
cosh
. x)
^2 ))) by
NEWTON: 6
.= ((((((4
* t)
+ (4
* (t
|^ 3)))
+ (8
* (t
|^ 3)))
+ (8
* (t
|^ 5)))
+ t)
+ ((8
* (t
|^ 3))
* (1
+ (t
^2 )))) by
Th70
.= (((((((4
* t)
+ (4
* (t
|^ 3)))
+ (8
* (t
|^ 3)))
+ (8
* (t
|^ 5)))
+ t)
+ (8
* (t
|^ 3)))
+ ((8
* ((t
|^ 3)
* t))
* t))
.= (((((((4
* t)
+ (4
* (t
|^ 3)))
+ (8
* (t
|^ 3)))
+ (8
* (t
|^ 5)))
+ t)
+ (8
* (t
|^ 3)))
+ ((8
* (t
|^ (3
+ 1)))
* t)) by
NEWTON: 6
.= (((((((4
* t)
+ (4
* (t
|^ 3)))
+ (8
* (t
|^ 3)))
+ (8
* (t
|^ 5)))
+ t)
+ (8
* (t
|^ 3)))
+ (8
* ((t
|^ 4)
* t)))
.= (((((((4
* t)
+ (4
* (t
|^ 3)))
+ (8
* (t
|^ 3)))
+ (8
* (t
|^ 5)))
+ t)
+ (8
* (t
|^ 3)))
+ (8
* (t
|^ (4
+ 1)))) by
NEWTON: 6
.= (((5
* t)
+ (20
* (t
|^ 3)))
+ ((8
* (t
|^ 5))
+ (8
* (t
|^ 5))))
.= (((5
* (
sinh x))
+ (20
* (t
|^ 3)))
+ (16
* (t
|^ 5))) by
SIN_COS2:def 2
.= (((5
* (
sinh x))
+ (20
* ((
sinh x)
|^ 3)))
+ (16
* (t
|^ 5))) by
SIN_COS2:def 2
.= (((5
* (
sinh x))
+ (20
* ((
sinh x)
|^ 3)))
+ (16
* ((
sinh x)
|^ 5))) by
SIN_COS2:def 2;
hence thesis;
end;
theorem ::
SIN_COS7:73
(
cosh (5
* x))
= (((5
* (
cosh x))
- (20
* ((
cosh x)
|^ 3)))
+ (16
* ((
cosh x)
|^ 5)))
proof
set t = (
cosh
. x), u = (
sinh
. x);
(
cosh (5
* x))
= (
cosh
. ((4
* x)
+ x)) by
SIN_COS2:def 4
.= (((
cosh
. (2
* (2
* x)))
* t)
+ ((
sinh
. (4
* x))
* u)) by
SIN_COS2: 20
.= (((1
+ (2
* ((
sinh
. (2
* x))
^2 )))
* t)
+ ((
sinh
. (4
* x))
* u)) by
Th69
.= (((1
+ (2
* (((2
* u)
* t)
^2 )))
* t)
+ ((
sinh
. (2
* (2
* x)))
* u)) by
SIN_COS2: 23
.= ((t
+ ((8
* (u
^2 ))
* ((t
^2 )
* t)))
+ ((
sinh
. (2
* (2
* x)))
* u))
.= ((t
+ ((8
* (u
^2 ))
* (((t
|^ 1)
* t)
* t)))
+ ((
sinh
. (2
* (2
* x)))
* u))
.= ((t
+ ((8
* (u
^2 ))
* ((t
|^ (1
+ 1))
* t)))
+ ((
sinh
. (2
* (2
* x)))
* u)) by
NEWTON: 6
.= ((t
+ ((8
* ((
sinh
. x)
^2 ))
* (t
|^ (2
+ 1))))
+ ((
sinh
. (2
* (2
* x)))
* u)) by
NEWTON: 6
.= ((t
+ ((8
* ((t
^2 )
- 1))
* (t
|^ 3)))
+ ((
sinh
. (2
* (2
* x)))
* u)) by
Th71
.= (((t
+ (8
* (((t
|^ 3)
* t)
* t)))
- (8
* (t
|^ 3)))
+ ((
sinh
. (2
* (2
* x)))
* u))
.= (((t
+ (8
* ((t
|^ (3
+ 1))
* t)))
- (8
* (t
|^ 3)))
+ ((
sinh
. (2
* (2
* x)))
* u)) by
NEWTON: 6
.= (((t
+ (8
* (t
|^ (4
+ 1))))
- (8
* (t
|^ 3)))
+ ((
sinh
. (2
* (2
* x)))
* u)) by
NEWTON: 6
.= (((t
+ (8
* (t
|^ 5)))
- (8
* (t
|^ 3)))
+ (((2
* (
sinh
. (2
* x)))
* (
cosh
. (2
* x)))
* u)) by
SIN_COS2: 23
.= (((t
+ (8
* (t
|^ 5)))
- (8
* (t
|^ 3)))
+ (((2
* ((2
* u)
* t))
* (
cosh
. (2
* x)))
* u)) by
SIN_COS2: 23
.= (((t
+ (8
* (t
|^ 5)))
- (8
* (t
|^ 3)))
+ (((4
* (u
^2 ))
* t)
* (
cosh
. (2
* x))))
.= (((t
+ (8
* (t
|^ 5)))
- (8
* (t
|^ 3)))
+ (((4
* ((t
^2 )
- 1))
* t)
* (
cosh
. (2
* x)))) by
Th71
.= ((((t
+ (8
* (t
|^ 5)))
- (8
* (t
|^ 3)))
+ ((4
* ((t
* t)
* t))
* (
cosh
. (2
* x))))
- ((4
* t)
* (
cosh
. (2
* x))))
.= ((((t
+ (8
* (t
|^ 5)))
- (8
* (t
|^ 3)))
+ ((4
* (((t
|^ 1)
* t)
* t))
* (
cosh
. (2
* x))))
- ((4
* t)
* (
cosh
. (2
* x))))
.= ((((t
+ (8
* (t
|^ 5)))
- (8
* (t
|^ 3)))
+ ((4
* ((t
|^ (1
+ 1))
* t))
* (
cosh
. (2
* x))))
- ((4
* t)
* (
cosh
. (2
* x)))) by
NEWTON: 6
.= ((((t
+ (8
* (t
|^ 5)))
- (8
* (t
|^ 3)))
+ ((4
* (t
|^ (2
+ 1)))
* (
cosh
. (2
* x))))
- ((4
* t)
* (
cosh
. (2
* x)))) by
NEWTON: 6
.= ((((t
+ (8
* (t
|^ 5)))
- (8
* (t
|^ 3)))
+ ((4
* (t
|^ 3))
* ((2
* (t
^2 ))
- 1)))
- ((4
* t)
* (
cosh
. (2
* x)))) by
SIN_COS2: 23
.= (((((t
+ (8
* (t
|^ 5)))
- (8
* (t
|^ 3)))
+ (8
* (((t
|^ 3)
* t)
* t)))
- (4
* (t
|^ 3)))
- ((4
* t)
* (
cosh
. (2
* x))))
.= (((((t
+ (8
* (t
|^ 5)))
- (8
* (t
|^ 3)))
+ (8
* ((t
|^ (3
+ 1))
* t)))
- (4
* (t
|^ 3)))
- ((4
* t)
* (
cosh
. (2
* x)))) by
NEWTON: 6
.= (((((t
+ (8
* (t
|^ 5)))
- (8
* (t
|^ 3)))
+ (8
* (t
|^ (4
+ 1))))
- (4
* (t
|^ 3)))
- ((4
* t)
* (
cosh
. (2
* x)))) by
NEWTON: 6
.= (((t
+ (16
* (t
|^ 5)))
- (12
* (t
|^ 3)))
- ((4
* t)
* ((2
* (t
^2 ))
- 1))) by
SIN_COS2: 23
.= ((((5
* t)
+ (16
* (t
|^ 5)))
- (12
* (t
|^ 3)))
- (8
* ((t
* t)
* t)))
.= ((((5
* t)
+ (16
* (t
|^ 5)))
- (12
* (t
|^ 3)))
- (8
* (((t
|^ 1)
* t)
* t)))
.= ((((5
* t)
+ (16
* (t
|^ 5)))
- (12
* (t
|^ 3)))
- (8
* ((t
|^ (1
+ 1))
* t))) by
NEWTON: 6
.= ((((5
* t)
+ (16
* (t
|^ 5)))
- (12
* (t
|^ 3)))
- (8
* (t
|^ (2
+ 1)))) by
NEWTON: 6
.= (((5
* t)
- (20
* (t
|^ 3)))
+ (16
* (t
|^ 5)))
.= (((5
* (
cosh x))
- (20
* (t
|^ 3)))
+ (16
* (t
|^ 5))) by
SIN_COS2:def 4
.= (((5
* (
cosh x))
- (20
* ((
cosh x)
|^ 3)))
+ (16
* (t
|^ 5))) by
SIN_COS2:def 4
.= (((5
* (
cosh x))
- (20
* ((
cosh x)
|^ 3)))
+ (16
* ((
cosh x)
|^ 5))) by
SIN_COS2:def 4;
hence thesis;
end;