series_5.miz
begin
reserve a,b,c,d for
positive
Real,
m,u,w,x,y,z for
Real,
n,k for
Nat,
s,s1 for
Real_Sequence;
Lm1: ((x
|^ 3)
- (y
|^ 3))
= ((x
- y)
* (((x
^2 )
+ (x
* y))
+ (y
^2 )))
proof
((x
- y)
* (((x
^2 )
+ (x
* y))
+ (y
^2 )))
= ((((x
* (x
^2 ))
+ ((x
* x)
* y))
+ (x
* (y
^2 )))
- (((y
* (x
^2 ))
+ ((y
* x)
* y))
+ (y
* (y
^2 ))))
.= ((((x
* (x
|^ 2))
+ ((x
* x)
* y))
+ (x
* (y
^2 )))
- (((y
* (x
^2 ))
+ ((y
* x)
* y))
+ (y
* (y
^2 )))) by
NEWTON: 81
.= ((((x
|^ (2
+ 1))
+ ((x
* x)
* y))
+ (x
* (y
^2 )))
- (((y
* (x
^2 ))
+ ((y
* x)
* y))
+ (y
* (y
^2 )))) by
NEWTON: 6
.= ((((x
|^ 3)
+ (x
* (y
* y)))
- ((y
* x)
* y))
- (y
* (y
^2 )))
.= ((x
|^ 3)
- ((y
|^ 2)
* y)) by
NEWTON: 81
.= ((x
|^ 3)
- (y
|^ (2
+ 1))) by
NEWTON: 6;
hence thesis;
end;
Lm2: (2
/ ((1
/ a)
+ (1
/ b)))
= ((2
* (a
* b))
/ (a
+ b))
proof
(1
/ ((1
/ a)
+ (1
/ b)))
= (1
/ (((1
* b)
+ (1
* a))
/ (a
* b))) by
XCMPLX_1: 116
.= (((a
* b)
* 1)
/ (b
+ a)) by
XCMPLX_1: 77
.= ((a
* b)
/ (b
+ a));
then ((2
* 1)
/ ((1
/ a)
+ (1
/ b)))
= (2
* ((a
* b)
/ (b
+ a))) by
XCMPLX_1: 74;
hence thesis by
XCMPLX_1: 74;
end;
Lm3: (((1
/ x)
* (1
/ y))
* (1
/ z))
= (1
/ ((x
* y)
* z))
proof
(((1
/ x)
* (1
/ y))
* (1
/ z))
= ((1
/ (x
* y))
* (1
/ z)) by
XCMPLX_1: 102
.= (1
/ ((x
* y)
* z)) by
XCMPLX_1: 102;
hence thesis;
end;
Lm4: for b be
Real holds ((a
/ c)
to_power (
- b))
= ((c
/ a)
to_power b)
proof
let b be
Real;
((a
/ c)
to_power (
- b))
= ((1
/ (a
/ c))
to_power b) by
POWER: 32
.= (((c
/ a)
* 1)
to_power b) by
XCMPLX_1: 80
.= ((c
/ a)
to_power b);
hence thesis;
end;
Lm5: ((((
sqrt (a
* b))
^2 )
+ ((
sqrt (c
* d))
^2 ))
* (((
sqrt (a
* c))
^2 )
+ ((
sqrt (b
* d))
^2 )))
>= ((b
* c)
* ((a
+ d)
^2 ))
proof
(((a
* (b
^2 ))
* d)
+ (((c
^2 )
* d)
* a))
>= (2
* (
sqrt (((a
* (b
^2 ))
* d)
* (((c
^2 )
* d)
* a)))) by
SIN_COS2: 1;
then ((((a
* (b
^2 ))
* d)
+ (((c
^2 )
* d)
* a))
+ ((((a
^2 )
* b)
* c)
+ ((b
* c)
* (d
^2 ))))
>= ((2
* (
sqrt ((((a
^2 )
* (b
^2 ))
* (c
^2 ))
* (d
^2 ))))
+ ((((a
^2 )
* b)
* c)
+ ((b
* c)
* (d
^2 )))) by
XREAL_1: 7;
then (((((a
* (b
^2 ))
* d)
+ (((c
^2 )
* d)
* a))
+ (((a
^2 )
* b)
* c))
+ ((b
* c)
* (d
^2 )))
>= (((2
* (
sqrt (((a
* b)
* (c
* d))
^2 )))
+ (((a
^2 )
* b)
* c))
+ ((b
* c)
* (d
^2 )));
then
A1: (((((a
* (b
^2 ))
* d)
+ (((c
^2 )
* d)
* a))
+ (((a
^2 )
* b)
* c))
+ ((b
* c)
* (d
^2 )))
>= (((2
* (((a
* b)
* c)
* d))
+ (((a
^2 )
* b)
* c))
+ ((b
* c)
* (d
^2 ))) by
SQUARE_1: 22;
((((
sqrt (a
* b))
^2 )
+ ((
sqrt (c
* d))
^2 ))
* (((
sqrt (a
* c))
^2 )
+ ((
sqrt (b
* d))
^2 )))
= (((a
* b)
+ ((
sqrt (c
* d))
^2 ))
* (((
sqrt (a
* c))
^2 )
+ ((
sqrt (b
* d))
^2 ))) by
SQUARE_1:def 2
.= (((a
* b)
+ (c
* d))
* (((
sqrt (a
* c))
^2 )
+ ((
sqrt (b
* d))
^2 ))) by
SQUARE_1:def 2
.= (((a
* b)
+ (c
* d))
* ((a
* c)
+ ((
sqrt (b
* d))
^2 ))) by
SQUARE_1:def 2
.= (((a
* b)
+ (c
* d))
* ((a
* c)
+ (b
* d))) by
SQUARE_1:def 2
.= ((((((a
^2 )
* b)
* c)
+ ((a
* (b
^2 ))
* d))
+ (((c
^2 )
* d)
* a))
+ ((b
* c)
* (d
^2 )));
hence thesis by
A1;
end;
Lm6: (((x
+ y)
+ z)
^2 )
= ((((((x
^2 )
+ (y
^2 ))
+ (z
^2 ))
+ ((2
* x)
* y))
+ ((2
* y)
* z))
+ ((2
* z)
* x));
Lm7:
|.x.|
< 1 implies (x
^2 )
< 1
proof
assume
|.x.|
< 1;
then (
|.x.|
^2 )
< (1
^2 ) by
SQUARE_1: 16;
hence thesis by
COMPLEX1: 75;
end;
Lm8: (x
^2 )
< 1 implies
|.x.|
< 1
proof
assume (x
^2 )
< 1;
then (
sqrt (x
^2 ))
< 1 by
SQUARE_1: 18,
SQUARE_1: 27,
XREAL_1: 63;
hence thesis by
COMPLEX1: 72;
end;
Lm9: ((((((((2
* (a
^2 ))
* (
sqrt (b
* c)))
* 2)
* (b
^2 ))
* (
sqrt (a
* c)))
* 2)
* (c
^2 ))
* (
sqrt (a
* b)))
= ((((2
* a)
* b)
* c)
|^ 3)
proof
((((((((2
* (a
^2 ))
* (
sqrt (b
* c)))
* 2)
* (b
^2 ))
* (
sqrt (a
* c)))
* 2)
* (c
^2 ))
* (
sqrt (a
* b)))
= ((((((((2
^2 )
* 2)
* (a
^2 ))
* (b
^2 ))
* (c
^2 ))
* (
sqrt (b
* c)))
* (
sqrt (a
* c)))
* (
sqrt (a
* b)))
.= ((((((((2
|^ 2)
* 2)
* (a
^2 ))
* (b
^2 ))
* (c
^2 ))
* (
sqrt (b
* c)))
* (
sqrt (a
* c)))
* (
sqrt (a
* b))) by
NEWTON: 81
.= (((((((2
|^ (2
+ 1))
* (a
^2 ))
* (b
^2 ))
* (c
^2 ))
* (
sqrt (b
* c)))
* (
sqrt (a
* c)))
* (
sqrt (a
* b))) by
NEWTON: 6
.= ((((((2
|^ 3)
* (a
^2 ))
* (b
^2 ))
* (c
^2 ))
* ((
sqrt (b
* c))
* (
sqrt (a
* c))))
* (
sqrt (a
* b)))
.= ((((((2
|^ 3)
* (a
^2 ))
* (b
^2 ))
* (c
^2 ))
* (
sqrt ((b
* c)
* (a
* c))))
* (
sqrt (a
* b))) by
SQUARE_1: 29
.= (((((2
|^ 3)
* (a
^2 ))
* (b
^2 ))
* (c
^2 ))
* ((
sqrt (((b
* c)
* a)
* c))
* (
sqrt (a
* b))))
.= (((((2
|^ 3)
* (a
^2 ))
* (b
^2 ))
* (c
^2 ))
* (
sqrt ((((b
* c)
* a)
* c)
* (a
* b)))) by
SQUARE_1: 29
.= (((((2
|^ 3)
* (a
^2 ))
* (b
^2 ))
* (c
^2 ))
* (
sqrt (((a
* b)
* c)
^2 )))
.= (((((2
|^ 3)
* (a
^2 ))
* (b
^2 ))
* (c
^2 ))
* ((a
* b)
* c)) by
SQUARE_1: 22
.= ((((2
|^ 3)
* ((a
^2 )
* a))
* ((b
^2 )
* b))
* ((c
^2 )
* c))
.= ((((2
|^ 3)
* ((a
|^ 2)
* a))
* ((b
^2 )
* b))
* ((c
^2 )
* c)) by
NEWTON: 81
.= ((((2
|^ 3)
* ((a
|^ 2)
* a))
* ((b
|^ 2)
* b))
* ((c
^2 )
* c)) by
NEWTON: 81
.= ((((2
|^ 3)
* ((a
|^ 2)
* a))
* ((b
|^ 2)
* b))
* ((c
|^ 2)
* c)) by
NEWTON: 81
.= ((((2
|^ 3)
* (a
|^ (2
+ 1)))
* ((b
|^ 2)
* b))
* ((c
|^ 2)
* c)) by
NEWTON: 6
.= ((((2
|^ 3)
* (a
|^ 3))
* (b
|^ 3))
* ((c
|^ 2)
* c)) by
NEWTON: 6
.= ((((2
|^ 3)
* (a
|^ 3))
* (b
|^ 3))
* (c
|^ (2
+ 1))) by
NEWTON: 6
.= ((((2
* a)
|^ 3)
* (b
|^ 3))
* (c
|^ 3)) by
NEWTON: 7
.= ((((2
* a)
* b)
|^ 3)
* (c
|^ 3)) by
NEWTON: 7
.= ((((2
* a)
* b)
* c)
|^ 3) by
NEWTON: 7;
hence thesis;
end;
Lm10: (
sqrt (((a
^2 )
+ (a
* b))
+ (b
^2 )))
= ((1
/ 2)
* (
sqrt ((4
* ((a
^2 )
+ (b
^2 )))
+ ((4
* a)
* b))))
proof
A1: (((1
/ 2)
* (
sqrt ((4
* ((a
^2 )
+ (b
^2 )))
+ ((4
* a)
* b))))
^2 )
= (((1
/ 2)
* (1
/ 2))
* ((
sqrt ((4
* ((a
^2 )
+ (b
^2 )))
+ ((4
* a)
* b)))
^2 ))
.= ((1
/ 4)
* ((4
* ((a
^2 )
+ (b
^2 )))
+ ((4
* a)
* b))) by
SQUARE_1:def 2
.= ((
sqrt (((a
^2 )
+ (a
* b))
+ (b
^2 )))
^2 ) by
SQUARE_1:def 2;
A2: (
sqrt (((a
^2 )
+ (a
* b))
+ (b
^2 )))
>
0 by
SQUARE_1: 25;
(
sqrt ((4
* ((a
^2 )
+ (b
^2 )))
+ ((4
* a)
* b)))
>
0 by
SQUARE_1: 25;
then (
sqrt ((
sqrt (((a
^2 )
+ (a
* b))
+ (b
^2 )))
^2 ))
= ((1
/ 2)
* (
sqrt ((4
* ((a
^2 )
+ (b
^2 )))
+ ((4
* a)
* b)))) by
A1,
SQUARE_1: 22;
hence thesis by
A2,
SQUARE_1: 22;
end;
Lm11: (
sqrt (((a
^2 )
+ (a
* b))
+ (b
^2 )))
>= (((1
/ 2)
* (
sqrt 3))
* (a
+ b))
proof
((a
^2 )
+ (b
^2 ))
>= ((2
* a)
* b) by
SERIES_3: 6;
then (((a
^2 )
+ (b
^2 ))
+ ((3
* ((a
^2 )
+ (b
^2 )))
+ ((4
* a)
* b)))
>= (((2
* a)
* b)
+ ((3
* ((a
^2 )
+ (b
^2 )))
+ ((4
* a)
* b))) by
XREAL_1: 6;
then (
sqrt ((4
* ((a
^2 )
+ (b
^2 )))
+ ((4
* a)
* b)))
>= (
sqrt ((3
* ((a
^2 )
+ (b
^2 )))
+ ((6
* a)
* b))) by
SQUARE_1: 26;
then
A1: ((1
/ 2)
* (
sqrt ((4
* ((a
^2 )
+ (b
^2 )))
+ ((4
* a)
* b))))
>= ((1
/ 2)
* (
sqrt ((3
* ((a
^2 )
+ (b
^2 )))
+ ((6
* a)
* b)))) by
XREAL_1: 64;
(
sqrt ((3
* ((a
^2 )
+ (b
^2 )))
+ ((6
* a)
* b)))
= (
sqrt (3
* ((a
+ b)
^2 )));
then (
sqrt ((3
* ((a
^2 )
+ (b
^2 )))
+ ((6
* a)
* b)))
= ((
sqrt 3)
* (
sqrt ((a
+ b)
^2 ))) by
SQUARE_1: 29
.= ((
sqrt 3)
* (a
+ b)) by
SQUARE_1: 22;
hence thesis by
A1,
Lm10;
end;
Lm12: (
sqrt ((((a
^2 )
+ (a
* b))
+ (b
^2 ))
/ 3))
<= (
sqrt (((a
^2 )
+ (b
^2 ))
/ 2))
proof
(((a
^2 )
+ (b
^2 ))
/ 2)
>= (a
* b) by
SERIES_3: 7;
then ((((a
^2 )
+ (b
^2 ))
/ 2)
+ ((a
^2 )
+ (b
^2 )))
>= ((a
* b)
+ ((a
^2 )
+ (b
^2 ))) by
XREAL_1: 6;
then ((((a
^2 )
+ (b
^2 ))
+ (((a
^2 )
+ (b
^2 ))
/ 2))
/ 3)
>= ((((a
^2 )
+ (a
* b))
+ (b
^2 ))
/ 3) by
XREAL_1: 72;
hence thesis by
SQUARE_1: 26;
end;
Lm13: ((((b
* c)
/ a)
^2 )
+ (((c
* a)
/ b)
^2 ))
>= (2
* (c
^2 ))
proof
((((b
* c)
/ a)
^2 )
+ (((c
* a)
/ b)
^2 ))
>= ((2
* ((b
* c)
/ a))
* ((c
* a)
/ b)) by
SERIES_3: 6;
then ((((b
* c)
/ a)
^2 )
+ (((c
* a)
/ b)
^2 ))
>= (2
* (((b
* c)
/ a)
* ((c
* a)
/ b)));
then ((((b
* c)
/ a)
^2 )
+ (((c
* a)
/ b)
^2 ))
>= (2
* (((b
* c)
* (c
* a))
/ (a
* b))) by
XCMPLX_1: 76;
then ((((b
* c)
/ a)
^2 )
+ (((c
* a)
/ b)
^2 ))
>= (2
* (((b
* a)
* (c
* c))
/ ((a
* b)
* 1)));
then ((((b
* c)
/ a)
^2 )
+ (((c
* a)
/ b)
^2 ))
>= (2
* ((c
* c)
/ 1)) by
XCMPLX_1: 91;
hence thesis;
end;
Lm14: (((b
* c)
/ a)
* ((c
* a)
/ b))
= (c
^2 )
proof
(((b
* c)
/ a)
* ((c
* a)
/ b))
= (((b
* c)
* (c
* a))
/ (a
* b)) by
XCMPLX_1: 76
.= (((c
* c)
* (a
* b))
/ (a
* b))
.= ((c
* c)
* ((a
* b)
/ (a
* b))) by
XCMPLX_1: 74
.= ((c
* c)
* 1) by
XCMPLX_1: 60;
hence thesis;
end;
Lm15: ((((2
* ((b
* c)
/ a))
* ((c
* a)
/ b))
+ ((2
* ((b
* c)
/ a))
* ((a
* b)
/ c)))
+ ((2
* ((c
* a)
/ b))
* ((a
* b)
/ c)))
= (2
* (((a
^2 )
+ (b
^2 ))
+ (c
^2 )))
proof
((((2
* ((b
* c)
/ a))
* ((c
* a)
/ b))
+ ((2
* ((b
* c)
/ a))
* ((a
* b)
/ c)))
+ ((2
* ((c
* a)
/ b))
* ((a
* b)
/ c)))
= (((2
* (((b
* c)
/ a)
* ((c
* a)
/ b)))
+ ((2
* ((b
* c)
/ a))
* ((a
* b)
/ c)))
+ ((2
* ((c
* a)
/ b))
* ((a
* b)
/ c)))
.= (((2
* (c
^2 ))
+ (2
* (((b
* c)
/ a)
* ((a
* b)
/ c))))
+ ((2
* ((c
* a)
/ b))
* ((a
* b)
/ c))) by
Lm14
.= (((2
* (c
^2 ))
+ (2
* (b
^2 )))
+ (2
* (((c
* a)
/ b)
* ((a
* b)
/ c)))) by
Lm14
.= (((2
* (c
^2 ))
+ (2
* (b
^2 )))
+ (2
* (a
^2 ))) by
Lm14
.= (2
* (((c
^2 )
+ (b
^2 ))
+ (a
^2 )));
hence thesis;
end;
Lm16: (((((b
* c)
/ a)
+ ((c
* a)
/ b))
+ ((a
* b)
/ c))
^2 )
= ((((((c
* a)
/ b)
^2 )
+ (((a
* b)
/ c)
^2 ))
+ (((b
* c)
/ a)
^2 ))
+ (2
* (((a
^2 )
+ (b
^2 ))
+ (c
^2 ))))
proof
(((((b
* c)
/ a)
+ ((c
* a)
/ b))
+ ((a
* b)
/ c))
^2 )
= ((((((b
* c)
/ a)
^2 )
+ (((c
* a)
/ b)
^2 ))
+ (((a
* b)
/ c)
^2 ))
+ ((((2
* ((b
* c)
/ a))
* ((c
* a)
/ b))
+ ((2
* ((b
* c)
/ a))
* ((a
* b)
/ c)))
+ ((2
* ((c
* a)
/ b))
* ((a
* b)
/ c))))
.= ((((((b
* c)
/ a)
^2 )
+ (((c
* a)
/ b)
^2 ))
+ (((a
* b)
/ c)
^2 ))
+ (2
* (((a
^2 )
+ (b
^2 ))
+ (c
^2 )))) by
Lm15;
hence thesis;
end;
Lm17: ((a
+ b)
+ c)
= 1 implies ((1
/ a)
- 1)
= ((b
+ c)
/ a)
proof
assume ((a
+ b)
+ c)
= 1;
then ((1
/ a)
- 1)
= (((a
+ (b
+ c))
/ a)
- 1)
.= (((a
/ a)
+ ((b
+ c)
/ a))
- 1) by
XCMPLX_1: 62
.= ((1
+ ((b
+ c)
/ a))
- 1) by
XCMPLX_1: 60;
hence thesis;
end;
Lm18: ((((2
* (
sqrt (b
* c)))
/ a)
* ((2
* (
sqrt (a
* c)))
/ b))
* ((2
* (
sqrt (a
* b)))
/ c))
= 8
proof
((((2
* (
sqrt (b
* c)))
/ a)
* ((2
* (
sqrt (a
* c)))
/ b))
* ((2
* (
sqrt (a
* b)))
/ c))
= ((((2
* (
sqrt (b
* c)))
* (2
* (
sqrt (a
* c))))
/ (a
* b))
* ((2
* (
sqrt (a
* b)))
/ c)) by
XCMPLX_1: 76
.= (((4
* ((
sqrt (b
* c))
* (
sqrt (a
* c))))
/ (a
* b))
* ((2
* (
sqrt (a
* b)))
/ c))
.= (((4
* (
sqrt ((b
* c)
* (a
* c))))
/ (a
* b))
* ((2
* (
sqrt (a
* b)))
/ c)) by
SQUARE_1: 29
.= (((4
* (
sqrt ((b
* a)
* (c
^2 ))))
* (2
* (
sqrt (a
* b))))
/ ((a
* b)
* c)) by
XCMPLX_1: 76
.= ((8
* ((
sqrt ((b
* a)
* (c
^2 )))
* (
sqrt (a
* b))))
/ ((a
* b)
* c))
.= ((8
* (
sqrt (((b
* a)
* (c
^2 ))
* (a
* b))))
/ ((a
* b)
* c)) by
SQUARE_1: 29
.= ((8
* (
sqrt (((a
* b)
* c)
^2 )))
/ ((a
* b)
* c))
.= ((8
* ((a
* b)
* c))
/ ((a
* b)
* c)) by
SQUARE_1: 22
.= (8
* (((a
* b)
* c)
/ ((a
* b)
* c))) by
XCMPLX_1: 74
.= (8
* 1) by
XCMPLX_1: 60;
hence thesis;
end;
Lm19: ((a
+ b)
+ c)
= 1 implies (1
+ (1
/ a))
= (2
+ ((b
+ c)
/ a))
proof
assume ((a
+ b)
+ c)
= 1;
then (1
+ (1
/ a))
= (1
+ ((a
+ (b
+ c))
/ a))
.= (1
+ ((a
/ a)
+ ((b
+ c)
/ a))) by
XCMPLX_1: 62
.= ((1
+ (a
/ a))
+ ((b
+ c)
/ a))
.= ((1
+ 1)
+ ((b
+ c)
/ a)) by
XCMPLX_1: 60;
hence thesis;
end;
Lm20: ((1
+ ((
sqrt (a
* c))
/ b))
* ((
sqrt (a
* b))
/ c))
= (((
sqrt (a
* b))
/ c)
+ (a
/ (
sqrt (b
* c))))
proof
A1: (
sqrt (b
* c))
>
0 by
SQUARE_1: 25;
((1
+ ((
sqrt (a
* c))
/ b))
* ((
sqrt (a
* b))
/ c))
= ((1
* ((
sqrt (a
* b))
/ c))
+ (((
sqrt (a
* c))
/ b)
* ((
sqrt (a
* b))
/ c)))
.= (((
sqrt (a
* b))
/ c)
+ (((
sqrt (a
* c))
* (
sqrt (a
* b)))
/ (b
* c))) by
XCMPLX_1: 76
.= (((
sqrt (a
* b))
/ c)
+ ((
sqrt ((a
* c)
* (a
* b)))
/ (b
* c))) by
SQUARE_1: 29
.= (((
sqrt (a
* b))
/ c)
+ ((
sqrt ((a
^2 )
* (c
* b)))
/ (b
* c)))
.= (((
sqrt (a
* b))
/ c)
+ (((
sqrt (a
^2 ))
* (
sqrt (c
* b)))
/ (b
* c))) by
SQUARE_1: 29
.= (((
sqrt (a
* b))
/ c)
+ (((
sqrt (a
^2 ))
* (
sqrt (c
* b)))
/ ((
sqrt (b
* c))
^2 ))) by
SQUARE_1:def 2
.= (((
sqrt (a
* b))
/ c)
+ (((
sqrt (a
^2 ))
/ (
sqrt (b
* c)))
* ((
sqrt (c
* b))
/ (
sqrt (b
* c))))) by
XCMPLX_1: 76
.= (((
sqrt (a
* b))
/ c)
+ (((
sqrt (a
^2 ))
/ (
sqrt (b
* c)))
* 1)) by
A1,
XCMPLX_1: 60
.= (((
sqrt (a
* b))
/ c)
+ (a
/ (
sqrt (b
* c)))) by
SQUARE_1: 22;
hence thesis;
end;
Lm21: ((((
sqrt (b
* c))
/ a)
+ (c
/ (
sqrt (b
* a))))
* ((
sqrt (a
* b))
/ c))
= ((b
/ (
sqrt (a
* c)))
+ 1)
proof
A1: (
sqrt (a
* c))
>
0 by
SQUARE_1: 25;
A2: (
sqrt (a
* b))
>
0 by
SQUARE_1: 25;
((((
sqrt (b
* c))
/ a)
+ (c
/ (
sqrt (b
* a))))
* ((
sqrt (a
* b))
/ c))
= ((((
sqrt (b
* c))
/ a)
* ((
sqrt (a
* b))
/ c))
+ ((c
/ (
sqrt (b
* a)))
* ((
sqrt (a
* b))
/ c)))
.= ((((
sqrt (b
* c))
* (
sqrt (a
* b)))
/ (a
* c))
+ ((c
/ (
sqrt (b
* a)))
* ((
sqrt (a
* b))
/ c))) by
XCMPLX_1: 76
.= (((
sqrt ((b
* c)
* (a
* b)))
/ (a
* c))
+ ((c
/ (
sqrt (b
* a)))
* ((
sqrt (a
* b))
/ c))) by
SQUARE_1: 29
.= (((
sqrt ((a
* c)
* (b
^2 )))
/ (a
* c))
+ ((c
/ (
sqrt (b
* a)))
* ((
sqrt (a
* b))
/ c)))
.= ((((
sqrt (a
* c))
* (
sqrt (b
^2 )))
/ (a
* c))
+ ((c
/ (
sqrt (b
* a)))
* ((
sqrt (a
* b))
/ c))) by
SQUARE_1: 29
.= ((((
sqrt (b
^2 ))
* (
sqrt (a
* c)))
/ ((
sqrt (a
* c))
^2 ))
+ ((c
/ (
sqrt (b
* a)))
* ((
sqrt (a
* b))
/ c))) by
SQUARE_1:def 2
.= ((((
sqrt (b
^2 ))
/ (
sqrt (a
* c)))
* ((
sqrt (a
* c))
/ (
sqrt (a
* c))))
+ ((c
/ (
sqrt (b
* a)))
* ((
sqrt (a
* b))
/ c))) by
XCMPLX_1: 76
.= ((((
sqrt (b
^2 ))
/ (
sqrt (a
* c)))
* 1)
+ ((c
/ (
sqrt (b
* a)))
* ((
sqrt (a
* b))
/ c))) by
A1,
XCMPLX_1: 60
.= ((b
/ (
sqrt (a
* c)))
+ ((c
/ (
sqrt (b
* a)))
* ((
sqrt (a
* b))
/ c))) by
SQUARE_1: 22
.= ((b
/ (
sqrt (a
* c)))
+ ((c
/ c)
* ((
sqrt (a
* b))
/ (
sqrt (b
* a))))) by
XCMPLX_1: 85
.= ((b
/ (
sqrt (a
* c)))
+ (1
* ((
sqrt (a
* b))
/ (
sqrt (b
* a))))) by
XCMPLX_1: 60
.= ((b
/ (
sqrt (a
* c)))
+ 1) by
A2,
XCMPLX_1: 60;
hence thesis;
end;
Lm22: (((1
+ ((
sqrt (b
* c))
/ a))
* (1
+ ((
sqrt (a
* c))
/ b)))
* (1
+ ((
sqrt (a
* b))
/ c)))
= ((((((2
+ ((
sqrt (a
* c))
/ b))
+ (b
/ (
sqrt (a
* c))))
+ ((
sqrt (a
* b))
/ c))
+ (c
/ (
sqrt (b
* a))))
+ (a
/ (
sqrt (b
* c))))
+ ((
sqrt (b
* c))
/ a))
proof
A1: (
sqrt (b
* a))
>
0 by
SQUARE_1: 25;
(((1
+ ((
sqrt (b
* c))
/ a))
* (1
+ ((
sqrt (a
* c))
/ b)))
* (1
+ ((
sqrt (a
* b))
/ c)))
= (((((1
* 1)
+ (1
* ((
sqrt (a
* c))
/ b)))
+ (((
sqrt (b
* c))
/ a)
* 1))
+ (((
sqrt (b
* c))
/ a)
* ((
sqrt (a
* c))
/ b)))
* (1
+ ((
sqrt (a
* b))
/ c)))
.= ((((1
+ ((
sqrt (a
* c))
/ b))
+ ((
sqrt (b
* c))
/ a))
+ (((
sqrt (b
* c))
* (
sqrt (a
* c)))
/ (a
* b)))
* (1
+ ((
sqrt (a
* b))
/ c))) by
XCMPLX_1: 76
.= ((((1
+ ((
sqrt (a
* c))
/ b))
+ ((
sqrt (b
* c))
/ a))
+ ((
sqrt ((b
* c)
* (a
* c)))
/ (a
* b)))
* (1
+ ((
sqrt (a
* b))
/ c))) by
SQUARE_1: 29
.= ((((1
+ ((
sqrt (a
* c))
/ b))
+ ((
sqrt (b
* c))
/ a))
+ ((
sqrt ((b
* a)
* (c
^2 )))
/ (a
* b)))
* (1
+ ((
sqrt (a
* b))
/ c)))
.= ((((1
+ ((
sqrt (a
* c))
/ b))
+ ((
sqrt (b
* c))
/ a))
+ (((
sqrt (b
* a))
* (
sqrt (c
^2 )))
/ (a
* b)))
* (1
+ ((
sqrt (a
* b))
/ c))) by
SQUARE_1: 29
.= ((((1
+ ((
sqrt (a
* c))
/ b))
+ ((
sqrt (b
* c))
/ a))
+ (((
sqrt (b
* a))
* c)
/ (a
* b)))
* (1
+ ((
sqrt (a
* b))
/ c))) by
SQUARE_1: 22
.= ((((1
+ ((
sqrt (a
* c))
/ b))
+ ((
sqrt (b
* c))
/ a))
+ (((
sqrt (b
* a))
* c)
/ ((
sqrt (a
* b))
^2 )))
* (1
+ ((
sqrt (a
* b))
/ c))) by
SQUARE_1:def 2
.= ((((1
+ ((
sqrt (a
* c))
/ b))
+ ((
sqrt (b
* c))
/ a))
+ (((
sqrt (b
* a))
/ (
sqrt (b
* a)))
* (c
/ (
sqrt (b
* a)))))
* (1
+ ((
sqrt (a
* b))
/ c))) by
XCMPLX_1: 76
.= ((((1
+ ((
sqrt (a
* c))
/ b))
+ ((
sqrt (b
* c))
/ a))
+ (1
* (c
/ (
sqrt (b
* a)))))
* (1
+ ((
sqrt (a
* b))
/ c))) by
A1,
XCMPLX_1: 60
.= (((((1
+ ((
sqrt (a
* c))
/ b))
+ ((1
+ ((
sqrt (a
* c))
/ b))
* ((
sqrt (a
* b))
/ c)))
+ ((
sqrt (b
* c))
/ a))
+ (c
/ (
sqrt (b
* a))))
+ ((((
sqrt (b
* c))
/ a)
+ (c
/ (
sqrt (b
* a))))
* ((
sqrt (a
* b))
/ c)))
.= (((((1
+ ((
sqrt (a
* c))
/ b))
+ (((
sqrt (a
* b))
/ c)
+ (a
/ (
sqrt (b
* c)))))
+ ((
sqrt (b
* c))
/ a))
+ (c
/ (
sqrt (b
* a))))
+ ((((
sqrt (b
* c))
/ a)
+ (c
/ (
sqrt (b
* a))))
* ((
sqrt (a
* b))
/ c))) by
Lm20
.= ((((((1
+ ((
sqrt (a
* c))
/ b))
+ ((
sqrt (a
* b))
/ c))
+ (a
/ (
sqrt (b
* c))))
+ ((
sqrt (b
* c))
/ a))
+ (c
/ (
sqrt (b
* a))))
+ ((b
/ (
sqrt (a
* c)))
+ 1)) by
Lm21
.= ((((((2
+ ((
sqrt (a
* c))
/ b))
+ (b
/ (
sqrt (a
* c))))
+ ((
sqrt (a
* b))
/ c))
+ (c
/ (
sqrt (b
* a))))
+ (a
/ (
sqrt (b
* c))))
+ ((
sqrt (b
* c))
/ a));
hence thesis;
end;
Lm23: (((((((
sqrt (a
* c))
/ b)
+ (b
/ (
sqrt (a
* c))))
+ ((
sqrt (a
* b))
/ c))
+ (c
/ (
sqrt (b
* a))))
+ (a
/ (
sqrt (b
* c))))
+ ((
sqrt (b
* c))
/ a))
>= 6
proof
(
sqrt (a
* c))
>
0 by
SQUARE_1: 25;
then
A1: (((
sqrt (a
* c))
/ b)
+ (b
/ (
sqrt (a
* c))))
>= 2 by
SERIES_3: 3;
(
sqrt (b
* c))
>
0 by
SQUARE_1: 25;
then
A2: ((a
/ (
sqrt (b
* c)))
+ ((
sqrt (b
* c))
/ a))
>= 2 by
SERIES_3: 3;
(
sqrt (b
* a))
>
0 by
SQUARE_1: 25;
then (((
sqrt (a
* b))
/ c)
+ (c
/ (
sqrt (b
* a))))
>= 2 by
SERIES_3: 3;
then ((((
sqrt (a
* c))
/ b)
+ (b
/ (
sqrt (a
* c))))
+ (((
sqrt (a
* b))
/ c)
+ (c
/ (
sqrt (b
* a)))))
>= (2
+ 2) by
A1,
XREAL_1: 7;
then ((((((
sqrt (a
* c))
/ b)
+ (b
/ (
sqrt (a
* c))))
+ ((
sqrt (a
* b))
/ c))
+ (c
/ (
sqrt (b
* a))))
+ ((a
/ (
sqrt (b
* c)))
+ ((
sqrt (b
* c))
/ a)))
>= (4
+ 2) by
A2,
XREAL_1: 7;
hence thesis;
end;
theorem ::
SERIES_5:1
((a
+ b)
* ((1
/ a)
+ (1
/ b)))
>= 4
proof
((a
/ b)
+ (b
/ a))
>= (2
* (
sqrt ((a
/ b)
* (b
/ a)))) by
SIN_COS2: 1;
then ((a
/ b)
+ (b
/ a))
>= (2
* (
sqrt ((a
* b)
/ (b
* a)))) by
XCMPLX_1: 76;
then ((a
/ b)
+ (b
/ a))
>= (2
* (
sqrt (((a
/ b)
* b)
/ a))) by
XCMPLX_1: 83;
then ((a
/ b)
+ (b
/ a))
>= (2
* (
sqrt (a
/ a))) by
XCMPLX_1: 87;
then ((a
/ b)
+ (b
/ a))
>= (2
* 1) by
SQUARE_1: 18,
XCMPLX_1: 60;
then (((a
/ b)
+ (b
/ a))
+ 2)
>= (2
+ 2) by
XREAL_1: 7;
then ((((a
/ b)
+ (b
/ a))
+ 1)
+ 1)
>= 4;
then ((((a
* (1
/ b))
+ (b
/ a))
+ 1)
+ 1)
>= 4 by
XCMPLX_1: 99;
then ((((a
* (1
/ b))
+ (b
* (1
/ a)))
+ 1)
+ 1)
>= 4 by
XCMPLX_1: 99;
then ((((a
* (1
/ b))
+ (b
* (1
/ a)))
+ (a
* (1
/ a)))
+ 1)
>= 4 by
XCMPLX_1: 106;
then ((((a
* (1
/ b))
+ (b
* (1
/ a)))
+ (a
* (1
/ a)))
+ (b
* (1
/ b)))
>= 4 by
XCMPLX_1: 106;
hence thesis;
end;
theorem ::
SERIES_5:2
((a
|^ 4)
+ (b
|^ 4))
>= (((a
|^ 3)
* b)
+ (a
* (b
|^ 3)))
proof
((a
- b)
^2 )
>=
0 by
XREAL_1: 63;
then (((a
- b)
* (a
- b))
* (((a
^2 )
+ (a
* b))
+ (b
^2 )))
>=
0 ;
then ((a
- b)
* ((a
- b)
* (((a
^2 )
+ (a
* b))
+ (b
^2 ))))
>=
0 ;
then ((a
- b)
* ((a
|^ 3)
- (b
|^ 3)))
>=
0 by
Lm1;
then ((((a
|^ 3)
* a)
- ((a
|^ 3)
* b))
- ((b
|^ 3)
* (a
- b)))
>=
0 ;
then (((a
|^ (3
+ 1))
- ((a
|^ 3)
* b))
- ((b
|^ 3)
* (a
- b)))
>=
0 by
NEWTON: 6;
then (((a
|^ 4)
- ((a
|^ 3)
* b))
- (((b
|^ 3)
* a)
- ((b
|^ 3)
* b)))
>=
0 ;
then (((a
|^ 4)
- ((a
|^ 3)
* b))
- (((b
|^ 3)
* a)
- (b
|^ (3
+ 1))))
>=
0 by
NEWTON: 6;
then (((((a
|^ 4)
+ (b
|^ 4))
- ((a
|^ 3)
* b))
- ((b
|^ 3)
* a))
+ (((a
|^ 3)
* b)
+ ((b
|^ 3)
* a)))
>= (
0
+ (((a
|^ 3)
* b)
+ ((b
|^ 3)
* a))) by
XREAL_1: 7;
hence thesis;
end;
theorem ::
SERIES_5:3
Th3: a
< b implies 1
< ((b
+ c)
/ (a
+ c))
proof
assume a
< b;
then (a
+ c)
< (b
+ c) by
XREAL_1: 8;
hence thesis by
XREAL_1: 187;
end;
theorem ::
SERIES_5:4
Th4: a
< b implies (a
/ b)
< (
sqrt (a
/ b))
proof
(b
^2 )
>
0 ;
then (b
|^ 2)
>
0 by
NEWTON: 81;
then ((b
|^ 2)
* b)
>
0 ;
then
A1: (b
|^ (2
+ 1))
>
0 by
NEWTON: 6;
assume a
< b;
then (a
- b)
<
0 by
XREAL_1: 49;
then ((a
* b)
* (a
- b))
<
0 ;
then ((((a
^2 )
* b)
- (a
* (b
^2 )))
+ (a
* (b
^2 )))
< (
0
+ (a
* (b
^2 ))) by
XREAL_1: 8;
then (((a
^2 )
* b)
/ (b
|^ (2
+ 1)))
< ((a
* (b
^2 ))
/ (b
|^ (2
+ 1))) by
A1,
XREAL_1: 74;
then (((a
^2 )
* b)
/ ((b
|^ 2)
* b))
< ((a
* (b
^2 ))
/ (b
|^ (2
+ 1))) by
NEWTON: 6;
then (((a
^2 )
* b)
/ ((b
|^ 2)
* b))
< ((a
* (b
^2 ))
/ ((b
|^ 2)
* b)) by
NEWTON: 6;
then (((a
^2 )
* b)
/ ((b
^2 )
* b))
< ((a
* (b
^2 ))
/ ((b
|^ 2)
* b)) by
NEWTON: 81;
then (((a
^2 )
* b)
/ ((b
^2 )
* b))
< ((a
* (b
^2 ))
/ ((b
^2 )
* b)) by
NEWTON: 81;
then ((a
^2 )
/ (b
^2 ))
< ((a
* (b
^2 ))
/ (b
* (b
^2 ))) by
XCMPLX_1: 91;
then ((a
^2 )
/ (b
^2 ))
< (a
/ b) by
XCMPLX_1: 91;
then ((a
/ b)
^2 )
< (a
/ b) by
XCMPLX_1: 76;
then (
sqrt ((a
/ b)
^2 ))
< (
sqrt (a
/ b)) by
SQUARE_1: 27;
hence thesis by
SQUARE_1: 22;
end;
theorem ::
SERIES_5:5
Th5: a
< b implies (
sqrt (a
/ b))
< ((b
+ (
sqrt (((a
^2 )
+ (b
^2 ))
/ 2)))
/ (a
+ (
sqrt (((a
^2 )
+ (b
^2 ))
/ 2))))
proof
assume
A1: a
< b;
then (a
/ b)
< 1 by
XREAL_1: 189;
then
A2: (
sqrt (a
/ b))
< 1 by
SQUARE_1: 18,
SQUARE_1: 27;
(
sqrt (((a
^2 )
+ (b
^2 ))
/ 2))
>
0 by
SQUARE_1: 25;
then 1
< ((b
+ (
sqrt (((a
^2 )
+ (b
^2 ))
/ 2)))
/ (a
+ (
sqrt (((a
^2 )
+ (b
^2 ))
/ 2)))) by
A1,
Th3;
hence thesis by
A2,
XXREAL_0: 2;
end;
theorem ::
SERIES_5:6
a
< b implies (a
/ b)
< ((b
+ (
sqrt (((a
^2 )
+ (b
^2 ))
/ 2)))
/ (a
+ (
sqrt (((a
^2 )
+ (b
^2 ))
/ 2))))
proof
assume
A1: a
< b;
then
A2: (
sqrt (a
/ b))
< ((b
+ (
sqrt (((a
^2 )
+ (b
^2 ))
/ 2)))
/ (a
+ (
sqrt (((a
^2 )
+ (b
^2 ))
/ 2)))) by
Th5;
(a
/ b)
< (
sqrt (a
/ b)) by
A1,
Th4;
hence thesis by
A2,
XXREAL_0: 2;
end;
theorem ::
SERIES_5:7
Th7: (2
/ ((1
/ a)
+ (1
/ b)))
<= (
sqrt (a
* b))
proof
A1: (
sqrt (a
* b))
>
0 by
SQUARE_1: 25;
then ((2
* (
sqrt (a
* b)))
/ (a
+ b))
<= 1 by
SIN_COS2: 1,
XREAL_1: 183;
then (((2
* (
sqrt (a
* b)))
/ (a
+ b))
* (
sqrt (a
* b)))
<= (1
* (
sqrt (a
* b))) by
A1,
XREAL_1: 64;
then ((2
* (
sqrt (a
* b)))
/ ((a
+ b)
/ (
sqrt (a
* b))))
<= (
sqrt (a
* b)) by
XCMPLX_1: 82;
then (((2
* (
sqrt (a
* b)))
* (
sqrt (a
* b)))
/ (a
+ b))
<= (
sqrt (a
* b)) by
XCMPLX_1: 77;
then ((2
* ((
sqrt (a
* b))
^2 ))
/ (a
+ b))
<= (
sqrt (a
* b));
then ((2
* (a
* b))
/ (a
+ b))
<= (
sqrt (a
* b)) by
SQUARE_1:def 2;
hence thesis by
Lm2;
end;
theorem ::
SERIES_5:8
Th8: ((a
+ b)
/ 2)
<= (
sqrt (((a
^2 )
+ (b
^2 ))
/ 2))
proof
((a
^2 )
+ (b
^2 ))
>= ((2
* a)
* b) by
SERIES_3: 6;
then (((a
^2 )
+ (b
^2 ))
+ ((a
^2 )
+ (b
^2 )))
>= (((2
* a)
* b)
+ ((a
^2 )
+ (b
^2 ))) by
XREAL_1: 7;
then (
sqrt (2
* ((a
^2 )
+ (b
^2 ))))
>= (
sqrt ((a
+ b)
^2 )) by
SQUARE_1: 26;
then (
sqrt (2
* ((a
^2 )
+ (b
^2 ))))
>= (a
+ b) by
SQUARE_1: 22;
then ((
sqrt (2
* ((a
^2 )
+ (b
^2 ))))
/ (
sqrt (2
* 2)))
>= ((a
+ b)
/ 2) by
SQUARE_1: 20,
XREAL_1: 72;
then ((
sqrt (2
* ((a
^2 )
+ (b
^2 ))))
/ ((
sqrt 2)
* (
sqrt 2)))
>= ((a
+ b)
/ 2) by
SQUARE_1: 29;
then (((
sqrt 2)
* (
sqrt ((a
^2 )
+ (b
^2 ))))
/ ((
sqrt 2)
* (
sqrt 2)))
>= ((a
+ b)
/ 2) by
SQUARE_1: 29;
then
A1: ((((
sqrt 2)
/ (
sqrt 2))
* (
sqrt ((a
^2 )
+ (b
^2 ))))
/ (
sqrt 2))
>= ((a
+ b)
/ 2) by
XCMPLX_1: 83;
(
sqrt 2)
>
0 by
SQUARE_1: 25;
then ((1
* (
sqrt ((a
^2 )
+ (b
^2 ))))
/ (
sqrt 2))
>= ((a
+ b)
/ 2) by
A1,
XCMPLX_1: 60;
hence thesis by
SQUARE_1: 30;
end;
theorem ::
SERIES_5:9
(x
+ y)
<= (
sqrt (2
* ((x
^2 )
+ (y
^2 ))))
proof
((x
^2 )
+ (y
^2 ))
>= ((2
* x)
* y) by
SERIES_3: 6;
then
A1: (((x
^2 )
+ (y
^2 ))
+ ((x
^2 )
+ (y
^2 )))
>= (((2
* x)
* y)
+ ((x
^2 )
+ (y
^2 ))) by
XREAL_1: 6;
then
A2: (2
* ((x
^2 )
+ (y
^2 )))
>= ((x
+ y)
^2 );
A3: ((x
+ y)
^2 )
>=
0 by
XREAL_1: 63;
then
A4: (
sqrt (2
* ((x
^2 )
+ (y
^2 ))))
>= (
sqrt ((x
+ y)
^2 )) by
A1,
SQUARE_1: 26;
per cases ;
suppose (x
+ y)
>
0 ;
hence thesis by
A4,
SQUARE_1: 22;
end;
suppose (x
+ y)
=
0 ;
hence thesis by
A2,
SQUARE_1: 17,
SQUARE_1: 26;
end;
suppose (x
+ y)
<
0 ;
hence thesis by
A1,
A3,
SQUARE_1:def 2;
end;
end;
theorem ::
SERIES_5:10
Th10: (2
/ ((1
/ a)
+ (1
/ b)))
<= ((a
+ b)
/ 2)
proof
A1: ((a
+ b)
/ 2)
>= (
sqrt (a
* b)) by
SERIES_3: 2;
(2
/ ((1
/ a)
+ (1
/ b)))
<= (
sqrt (a
* b)) by
Th7;
hence thesis by
A1,
XXREAL_0: 2;
end;
theorem ::
SERIES_5:11
(
sqrt (a
* b))
<= (
sqrt (((a
^2 )
+ (b
^2 ))
/ 2))
proof
A1: ((a
+ b)
/ 2)
>= (
sqrt (a
* b)) by
SERIES_3: 2;
((a
+ b)
/ 2)
<= (
sqrt (((a
^2 )
+ (b
^2 ))
/ 2)) by
Th8;
hence thesis by
A1,
XXREAL_0: 2;
end;
theorem ::
SERIES_5:12
(2
/ ((1
/ a)
+ (1
/ b)))
<= (
sqrt (((a
^2 )
+ (b
^2 ))
/ 2))
proof
A1: (2
/ ((1
/ a)
+ (1
/ b)))
<= ((a
+ b)
/ 2) by
Th10;
((a
+ b)
/ 2)
<= (
sqrt (((a
^2 )
+ (b
^2 ))
/ 2)) by
Th8;
hence thesis by
A1,
XXREAL_0: 2;
end;
theorem ::
SERIES_5:13
|.x.|
< 1 &
|.y.|
< 1 implies
|.((x
+ y)
/ (1
+ (x
* y))).|
<= 1
proof
assume that
A1:
|.x.|
< 1 and
A2:
|.y.|
< 1;
per cases ;
suppose
A3: (1
+ (x
* y))
<>
0 ;
(y
^2 )
< 1 by
A2,
Lm7;
then
A4: ((y
^2 )
- (y
^2 ))
< (1
- (y
^2 )) by
XREAL_1: 14;
(x
^2 )
< 1 by
A1,
Lm7;
then ((x
^2 )
- (x
^2 ))
< (1
- (x
^2 )) by
XREAL_1: 14;
then
0
< ((1
- (x
^2 ))
* (1
- (y
^2 ))) by
A4;
then (
0
+ ((x
^2 )
+ (y
^2 )))
< ((((1
- (y
^2 ))
- (x
^2 ))
+ ((x
^2 )
* (y
^2 )))
+ ((x
^2 )
+ (y
^2 ))) by
XREAL_1: 8;
then
A5: (((x
^2 )
+ (y
^2 ))
+ ((2
* x)
* y))
< ((1
+ ((x
^2 )
* (y
^2 )))
+ ((2
* x)
* y)) by
XREAL_1: 8;
((1
+ (x
* y))
^2 )
>
0 by
A3,
SQUARE_1: 12;
then (((x
+ y)
^2 )
/ ((1
+ (x
* y))
^2 ))
< ((((x
* y)
+ 1)
^2 )
/ ((1
+ (x
* y))
^2 )) by
A5,
XREAL_1: 74;
then (((x
+ y)
^2 )
/ ((1
+ (x
* y))
^2 ))
< 1 by
A3,
XCMPLX_1: 60;
then (((x
+ y)
/ (1
+ (x
* y)))
^2 )
< 1 by
XCMPLX_1: 76;
hence thesis by
Lm8;
end;
suppose (1
+ (x
* y))
=
0 ;
then
|.((x
+ y)
/ (1
+ (x
* y))).|
=
|.
0 .| by
XCMPLX_1: 49
.=
0 by
ABSVALUE: 2;
hence thesis;
end;
end;
theorem ::
SERIES_5:14
(
|.(x
+ y).|
/ (1
+
|.(x
+ y).|))
<= ((
|.x.|
/ (1
+
|.x.|))
+ (
|.y.|
/ (1
+
|.y.|)))
proof
per cases ;
suppose
|.(x
+ y).|
=
0 ;
hence thesis;
end;
suppose
A1:
|.(x
+ y).|
>
0 ;
(1
+
|.y.|)
>= 1 by
XREAL_1: 31;
then ((1
+
|.y.|)
+
|.x.|)
>= (1
+
|.x.|) by
XREAL_1: 6;
then
A2: (
|.x.|
/ ((1
+
|.x.|)
+
|.y.|))
<= (
|.x.|
/ (1
+
|.x.|)) by
XREAL_1: 118;
(1
+
|.x.|)
>= 1 by
XREAL_1: 31;
then ((1
+
|.x.|)
+
|.y.|)
>= (1
+
|.y.|) by
XREAL_1: 6;
then (
|.y.|
/ ((1
+
|.x.|)
+
|.y.|))
<= (
|.y.|
/ (1
+
|.y.|)) by
XREAL_1: 118;
then
A3: ((
|.x.|
/ ((1
+
|.x.|)
+
|.y.|))
+ (
|.y.|
/ ((1
+
|.x.|)
+
|.y.|)))
<= ((
|.x.|
/ (1
+
|.x.|))
+ (
|.y.|
/ (1
+
|.y.|))) by
A2,
XREAL_1: 7;
(1
/ (
|.x.|
+
|.y.|))
<= (1
/
|.(x
+ y).|) by
A1,
COMPLEX1: 56,
XREAL_1: 118;
then ((1
/ (
|.x.|
+
|.y.|))
+ 1)
<= ((1
/
|.(x
+ y).|)
+ 1) by
XREAL_1: 7;
then
A4: (1
/ ((1
/
|.(x
+ y).|)
+ 1))
<= (1
/ ((1
/ (
|.x.|
+
|.y.|))
+ 1)) by
XREAL_1: 118;
A5:
0
< (
|.x.|
+
|.y.|) by
A1,
COMPLEX1: 56;
then
A6: (1
/ ((1
/ (
|.x.|
+
|.y.|))
+ 1))
= ((1
* (
|.x.|
+
|.y.|))
/ (((1
/ (
|.x.|
+
|.y.|))
+ 1)
* (
|.x.|
+
|.y.|))) by
XCMPLX_1: 91
.= ((
|.x.|
+
|.y.|)
/ (((1
/ (
|.x.|
+
|.y.|))
* (
|.x.|
+
|.y.|))
+ (
|.x.|
+
|.y.|)))
.= ((
|.x.|
+
|.y.|)
/ (1
+ (
|.x.|
+
|.y.|))) by
A5,
XCMPLX_1: 87
.= ((
|.x.|
/ ((1
+
|.x.|)
+
|.y.|))
+ (
|.y.|
/ ((1
+
|.x.|)
+
|.y.|))) by
XCMPLX_1: 62;
(
|.(x
+ y).|
/ (1
+
|.(x
+ y).|))
= ((
|.(x
+ y).|
/
|.(x
+ y).|)
/ ((1
+
|.(x
+ y).|)
/
|.(x
+ y).|)) by
A1,
XCMPLX_1: 55
.= (1
/ ((1
+
|.(x
+ y).|)
/
|.(x
+ y).|)) by
A1,
XCMPLX_1: 60
.= (1
/ ((1
/
|.(x
+ y).|)
+ (
|.(x
+ y).|
/
|.(x
+ y).|))) by
XCMPLX_1: 62
.= (1
/ ((1
/
|.(x
+ y).|)
+ 1)) by
A1,
XCMPLX_1: 60;
hence thesis by
A4,
A6,
A3,
XXREAL_0: 2;
end;
end;
theorem ::
SERIES_5:15
((((a
/ ((a
+ b)
+ d))
+ (b
/ ((a
+ b)
+ c)))
+ (c
/ ((b
+ c)
+ d)))
+ (d
/ ((a
+ c)
+ d)))
> 1
proof
(d
+ ((a
+ b)
+ c))
> (
0
+ ((a
+ b)
+ c)) by
XREAL_1: 8;
then
A1: (b
/ (((a
+ b)
+ c)
+ d))
< (b
/ ((a
+ b)
+ c)) by
XREAL_1: 76;
(((b
+ c)
+ d)
+ a)
> (
0
+ ((b
+ c)
+ d)) by
XREAL_1: 8;
then
A2: (c
/ ((b
+ c)
+ d))
> (c
/ (((a
+ b)
+ c)
+ d)) by
XREAL_1: 76;
(c
+ ((a
+ b)
+ d))
> (
0
+ ((a
+ b)
+ d)) by
XREAL_1: 8;
then (a
/ (((a
+ b)
+ c)
+ d))
< (a
/ ((a
+ b)
+ d)) by
XREAL_1: 76;
then ((a
/ (((a
+ b)
+ c)
+ d))
+ (b
/ (((a
+ b)
+ c)
+ d)))
< ((a
/ ((a
+ b)
+ d))
+ (b
/ ((a
+ b)
+ c))) by
A1,
XREAL_1: 8;
then ((a
+ b)
/ (((a
+ b)
+ c)
+ d))
< ((a
/ ((a
+ b)
+ d))
+ (b
/ ((a
+ b)
+ c))) by
XCMPLX_1: 62;
then (((a
+ b)
/ (((a
+ b)
+ c)
+ d))
+ (c
/ (((a
+ b)
+ c)
+ d)))
< (((a
/ ((a
+ b)
+ d))
+ (b
/ ((a
+ b)
+ c)))
+ (c
/ ((b
+ c)
+ d))) by
A2,
XREAL_1: 8;
then
A3: (((a
+ b)
+ c)
/ (((a
+ b)
+ c)
+ d))
< (((a
/ ((a
+ b)
+ d))
+ (b
/ ((a
+ b)
+ c)))
+ (c
/ ((b
+ c)
+ d))) by
XCMPLX_1: 62;
(b
+ ((a
+ c)
+ d))
> (
0
+ ((a
+ c)
+ d)) by
XREAL_1: 8;
then (d
/ ((a
+ c)
+ d))
> (d
/ (((a
+ b)
+ c)
+ d)) by
XREAL_1: 76;
then ((((a
+ b)
+ c)
/ (((a
+ b)
+ c)
+ d))
+ (d
/ (((a
+ b)
+ c)
+ d)))
< ((((a
/ ((a
+ b)
+ d))
+ (b
/ ((a
+ b)
+ c)))
+ (c
/ ((b
+ c)
+ d)))
+ (d
/ ((a
+ c)
+ d))) by
A3,
XREAL_1: 8;
then ((((a
+ b)
+ c)
+ d)
/ (((a
+ b)
+ c)
+ d))
< ((((a
/ ((a
+ b)
+ d))
+ (b
/ ((a
+ b)
+ c)))
+ (c
/ ((b
+ c)
+ d)))
+ (d
/ ((a
+ c)
+ d))) by
XCMPLX_1: 62;
hence thesis by
XCMPLX_1: 60;
end;
theorem ::
SERIES_5:16
((((a
/ ((a
+ b)
+ d))
+ (b
/ ((a
+ b)
+ c)))
+ (c
/ ((b
+ c)
+ d)))
+ (d
/ ((a
+ c)
+ d)))
< 2
proof
A1: (b
/ (a
+ b))
> (b
/ ((a
+ b)
+ c)) by
XREAL_1: 29,
XREAL_1: 76;
(a
/ (a
+ b))
> (a
/ ((a
+ b)
+ d)) by
XREAL_1: 29,
XREAL_1: 76;
then ((a
/ (a
+ b))
+ (b
/ (a
+ b)))
> ((a
/ ((a
+ b)
+ d))
+ (b
/ ((a
+ b)
+ c))) by
A1,
XREAL_1: 8;
then ((a
+ b)
/ (a
+ b))
> ((a
/ ((a
+ b)
+ d))
+ (b
/ ((a
+ b)
+ c))) by
XCMPLX_1: 62;
then
A2: 1
> ((a
/ ((a
+ b)
+ d))
+ (b
/ ((a
+ b)
+ c))) by
XCMPLX_1: 60;
(a
+ (c
+ d))
> (c
+ d) by
XREAL_1: 29;
then
A3: (d
/ (c
+ d))
> (d
/ ((a
+ c)
+ d)) by
XREAL_1: 76;
(b
+ (c
+ d))
> (c
+ d) by
XREAL_1: 29;
then (c
/ (c
+ d))
> (c
/ ((b
+ c)
+ d)) by
XREAL_1: 76;
then (1
+ (c
/ (c
+ d)))
> (((a
/ ((a
+ b)
+ d))
+ (b
/ ((a
+ b)
+ c)))
+ (c
/ ((b
+ c)
+ d))) by
A2,
XREAL_1: 8;
then ((1
+ (c
/ (c
+ d)))
+ (d
/ (c
+ d)))
> ((((a
/ ((a
+ b)
+ d))
+ (b
/ ((a
+ b)
+ c)))
+ (c
/ ((b
+ c)
+ d)))
+ (d
/ ((a
+ c)
+ d))) by
A3,
XREAL_1: 8;
then (1
+ ((c
/ (c
+ d))
+ (d
/ (c
+ d))))
> ((((a
/ ((a
+ b)
+ d))
+ (b
/ ((a
+ b)
+ c)))
+ (c
/ ((b
+ c)
+ d)))
+ (d
/ ((a
+ c)
+ d)));
then (1
+ ((c
+ d)
/ (c
+ d)))
> ((((a
/ ((a
+ b)
+ d))
+ (b
/ ((a
+ b)
+ c)))
+ (c
/ ((b
+ c)
+ d)))
+ (d
/ ((a
+ c)
+ d))) by
XCMPLX_1: 62;
then (1
+ 1)
> ((((a
/ ((a
+ b)
+ d))
+ (b
/ ((a
+ b)
+ c)))
+ (c
/ ((b
+ c)
+ d)))
+ (d
/ ((a
+ c)
+ d))) by
XCMPLX_1: 60;
hence thesis;
end;
theorem ::
SERIES_5:17
(a
+ b)
> c & (b
+ c)
> a & (a
+ c)
> b implies (((1
/ ((a
+ b)
- c))
+ (1
/ ((b
+ c)
- a)))
+ (1
/ ((c
+ a)
- b)))
>= (9
/ ((a
+ b)
+ c))
proof
assume that
A1: (a
+ b)
> c and
A2: (b
+ c)
> a and
A3: (a
+ c)
> b;
A4: ((a
+ c)
- b)
>
0 by
A3,
XREAL_1: 50;
set f = ((c
+ a)
- b);
set e = ((b
+ c)
- a);
set d = ((a
+ b)
- c);
A5: ((b
+ c)
- a)
>
0 by
A2,
XREAL_1: 50;
A6: ((a
+ b)
- c)
>
0 by
A1,
XREAL_1: 50;
then
A7: ((d
+ e)
+ f)
>= (3
* (3
-root ((d
* e)
* f))) by
A5,
A4,
SERIES_3: 15;
(((1
/ d)
+ (1
/ e))
+ (1
/ f))
>= (3
* (3
-root (((1
/ d)
* (1
/ e))
* (1
/ f)))) by
A6,
A5,
A4,
SERIES_3: 15;
then
A8: (((1
/ d)
+ (1
/ e))
+ (1
/ f))
>= (3
* (3
-root (1
/ ((d
* e)
* f)))) by
Lm3;
A9: (3
-root ((d
* e)
* f))
>=
0 by
A6,
A5,
A4,
POWER: 7;
(3
-root (1
/ ((d
* e)
* f)))
>=
0 by
A6,
A5,
A4,
POWER: 7;
then (((d
+ e)
+ f)
* (((1
/ d)
+ (1
/ e))
+ (1
/ f)))
>= ((3
* (3
-root ((d
* e)
* f)))
* (3
* (3
-root (1
/ ((d
* e)
* f))))) by
A7,
A9,
A8,
XREAL_1: 66;
then (((d
+ e)
+ f)
* (((1
/ d)
+ (1
/ e))
+ (1
/ f)))
>= (9
* ((3
-root ((d
* e)
* f))
* (3
-root (1
/ ((d
* e)
* f)))));
then (((d
+ e)
+ f)
* (((1
/ d)
+ (1
/ e))
+ (1
/ f)))
>= (9
* (3
-root (((d
* e)
* f)
* (1
/ ((d
* e)
* f))))) by
A6,
A5,
A4,
POWER: 11;
then (((d
+ e)
+ f)
* (((1
/ d)
+ (1
/ e))
+ (1
/ f)))
>= (9
* (3
-root (((d
* e)
* f)
/ (((d
* e)
* f)
/ 1)))) by
XCMPLX_1: 79;
then (((d
+ e)
+ f)
* (((1
/ d)
+ (1
/ e))
+ (1
/ f)))
>= (9
* (3
-root 1)) by
A6,
A5,
A4,
XCMPLX_1: 60;
then (((d
+ e)
+ f)
* (((1
/ d)
+ (1
/ e))
+ (1
/ f)))
>= (9
* 1) by
POWER: 6;
hence thesis by
XREAL_1: 79;
end;
theorem ::
SERIES_5:18
(
sqrt ((a
+ b)
* (c
+ d)))
>= ((
sqrt (a
* c))
+ (
sqrt (b
* d)))
proof
A1: (
sqrt ((a
+ b)
* (c
+ d)))
>
0 by
SQUARE_1: 25;
A2: (
sqrt (b
* d))
>
0 by
SQUARE_1: 25;
((a
* d)
+ (b
* c))
>= (2
* (
sqrt ((a
* d)
* (b
* c)))) by
SIN_COS2: 1;
then (((a
* d)
+ (b
* c))
+ ((a
* c)
+ (b
* d)))
>= ((2
* (
sqrt ((a
* d)
* (b
* c))))
+ ((a
* c)
+ (b
* d))) by
XREAL_1: 7;
then ((a
+ b)
* (c
+ d))
>= (((2
* (
sqrt ((a
* d)
* (b
* c))))
+ (a
* c))
+ (b
* d));
then ((a
+ b)
* (c
+ d))
>= (((2
* (
sqrt ((a
* d)
* (b
* c))))
+ ((
sqrt (a
* c))
^2 ))
+ (b
* d)) by
SQUARE_1:def 2;
then ((a
+ b)
* (c
+ d))
>= (((2
* (
sqrt ((a
* d)
* (b
* c))))
+ ((
sqrt (a
* c))
^2 ))
+ ((
sqrt (b
* d))
^2 )) by
SQUARE_1:def 2;
then ((
sqrt ((a
+ b)
* (c
+ d)))
^2 )
>= (((2
* (
sqrt ((a
* c)
* (b
* d))))
+ ((
sqrt (a
* c))
^2 ))
+ ((
sqrt (b
* d))
^2 )) by
SQUARE_1:def 2;
then
A3: ((
sqrt ((a
+ b)
* (c
+ d)))
^2 )
>= ((((
sqrt (a
* c))
^2 )
+ (2
* ((
sqrt (a
* c))
* (
sqrt (b
* d)))))
+ ((
sqrt (b
* d))
^2 )) by
SQUARE_1: 29;
(((
sqrt (a
* c))
+ (
sqrt (b
* d)))
^2 )
>=
0 by
XREAL_1: 63;
then
A4: (
sqrt ((
sqrt ((a
+ b)
* (c
+ d)))
^2 ))
>= (
sqrt (((
sqrt (a
* c))
+ (
sqrt (b
* d)))
^2 )) by
A3,
SQUARE_1: 26;
(
sqrt (a
* c))
>
0 by
SQUARE_1: 25;
then (
sqrt ((
sqrt ((a
+ b)
* (c
+ d)))
^2 ))
>= ((
sqrt (a
* c))
+ (
sqrt (b
* d))) by
A4,
A2,
SQUARE_1: 22;
hence thesis by
A1,
SQUARE_1: 22;
end;
theorem ::
SERIES_5:19
(((a
* b)
+ (c
* d))
* ((a
* c)
+ (b
* d)))
>= ((((4
* a)
* b)
* c)
* d)
proof
(
sqrt (a
* d))
>
0 by
SQUARE_1: 25;
then ((a
+ d)
^2 )
>= ((2
* (
sqrt (a
* d)))
^2 ) by
SIN_COS2: 1,
SQUARE_1: 15;
then ((a
+ d)
^2 )
>= ((2
^2 )
* ((
sqrt (a
* d))
^2 ));
then ((a
+ d)
^2 )
>= ((2
* 2)
* (a
* d)) by
SQUARE_1:def 2;
then
A1: (((a
+ d)
^2 )
* (b
* c))
>= (((4
* a)
* d)
* (b
* c)) by
XREAL_1: 64;
(((a
* b)
+ (c
* d))
* ((a
* c)
+ (b
* d)))
= ((((
sqrt (a
* b))
^2 )
+ (c
* d))
* ((a
* c)
+ (b
* d))) by
SQUARE_1:def 2
.= ((((
sqrt (a
* b))
^2 )
+ ((
sqrt (c
* d))
^2 ))
* ((a
* c)
+ (b
* d))) by
SQUARE_1:def 2
.= ((((
sqrt (a
* b))
^2 )
+ ((
sqrt (c
* d))
^2 ))
* (((
sqrt (a
* c))
^2 )
+ (b
* d))) by
SQUARE_1:def 2
.= ((((
sqrt (a
* b))
^2 )
+ ((
sqrt (c
* d))
^2 ))
* (((
sqrt (a
* c))
^2 )
+ ((
sqrt (b
* d))
^2 ))) by
SQUARE_1:def 2;
then (((a
* b)
+ (c
* d))
* ((a
* c)
+ (b
* d)))
>= ((b
* c)
* ((a
+ d)
^2 )) by
Lm5;
hence thesis by
A1,
XXREAL_0: 2;
end;
theorem ::
SERIES_5:20
Th20: (((a
/ b)
+ (b
/ c))
+ (c
/ a))
>= 3
proof
(((a
/ b)
+ (b
/ c))
+ (c
/ a))
>= (3
* (3
-root (((a
/ b)
* (b
/ c))
* (c
/ a)))) by
SERIES_3: 15;
then (((a
/ b)
+ (b
/ c))
+ (c
/ a))
>= (3
* (3
-root (((a
* b)
/ (b
* c))
* (c
/ a)))) by
XCMPLX_1: 76;
then (((a
/ b)
+ (b
/ c))
+ (c
/ a))
>= (3
* (3
-root ((a
/ c)
* (c
/ a)))) by
XCMPLX_1: 91;
then (((a
/ b)
+ (b
/ c))
+ (c
/ a))
>= (3
* (3
-root ((a
* c)
/ (c
* a)))) by
XCMPLX_1: 76;
then (((a
/ b)
+ (b
/ c))
+ (c
/ a))
>= (3
* (3
-root 1)) by
XCMPLX_1: 60;
then (((a
/ b)
+ (b
/ c))
+ (c
/ a))
>= (3
* 1) by
POWER: 6;
hence thesis;
end;
theorem ::
SERIES_5:21
(((a
* b)
+ (b
* c))
+ (c
* a))
= 1 implies ((a
+ b)
+ c)
>= (
sqrt 3)
proof
assume
A1: (((a
* b)
+ (b
* c))
+ (c
* a))
= 1;
then (((a
^2 )
+ (b
^2 ))
+ (c
^2 ))
>= 1 by
SERIES_3: 10;
then ((((a
^2 )
+ (b
^2 ))
+ (c
^2 ))
+ 2)
>= (1
+ 2) by
XREAL_1: 6;
then (
sqrt (((a
+ b)
+ c)
^2 ))
>= (
sqrt 3) by
A1,
SQUARE_1: 26;
hence thesis by
SQUARE_1: 22;
end;
theorem ::
SERIES_5:22
(((((b
+ c)
- a)
/ a)
+ (((c
+ a)
- b)
/ b))
+ (((a
+ b)
- c)
/ c))
>= 3
proof
A1: (((b
/ a)
+ (c
/ b))
+ (a
/ c))
>= 3 by
Th20;
(((a
/ b)
+ (b
/ c))
+ (c
/ a))
>= 3 by
Th20;
then ((((a
/ b)
+ (b
/ c))
+ (c
/ a))
+ (((b
/ a)
+ (c
/ b))
+ (a
/ c)))
>= (3
+ 3) by
A1,
XREAL_1: 7;
then
A2: (((((((a
/ b)
+ (b
/ c))
+ (c
/ a))
+ (b
/ a))
+ (c
/ b))
+ (a
/ c))
- 3)
>= (6
- 3) by
XREAL_1: 9;
(((((b
+ c)
- a)
/ a)
+ (((c
+ a)
- b)
/ b))
+ (((a
+ b)
- c)
/ c))
= (((((b
+ c)
/ a)
- (a
/ a))
+ (((c
+ a)
- b)
/ b))
+ (((a
+ b)
- c)
/ c)) by
XCMPLX_1: 120
.= (((((b
+ c)
/ a)
- 1)
+ (((c
+ a)
- b)
/ b))
+ (((a
+ b)
- c)
/ c)) by
XCMPLX_1: 60
.= (((((b
+ c)
/ a)
- 1)
+ (((c
+ a)
/ b)
- (b
/ b)))
+ (((a
+ b)
- c)
/ c)) by
XCMPLX_1: 120
.= (((((b
+ c)
/ a)
- 1)
+ (((c
+ a)
/ b)
- 1))
+ (((a
+ b)
- c)
/ c)) by
XCMPLX_1: 60
.= ((((((b
+ c)
/ a)
- 1)
+ ((c
+ a)
/ b))
- 1)
+ (((a
+ b)
/ c)
- (c
/ c))) by
XCMPLX_1: 120
.= ((((((b
+ c)
/ a)
- 1)
+ ((c
+ a)
/ b))
- 1)
+ (((a
+ b)
/ c)
- 1)) by
XCMPLX_1: 60
.= (((((b
+ c)
/ a)
+ ((c
+ a)
/ b))
+ ((a
+ b)
/ c))
- 3)
.= (((((b
/ a)
+ (c
/ a))
+ ((c
+ a)
/ b))
+ ((a
+ b)
/ c))
- 3) by
XCMPLX_1: 62
.= (((((b
/ a)
+ (c
/ a))
+ ((c
/ b)
+ (a
/ b)))
+ ((a
+ b)
/ c))
- 3) by
XCMPLX_1: 62
.= (((((b
/ a)
+ (c
/ a))
+ ((c
/ b)
+ (a
/ b)))
+ ((a
/ c)
+ (b
/ c)))
- 3) by
XCMPLX_1: 62
.= (((((((a
/ b)
+ (b
/ c))
+ (c
/ a))
+ (b
/ a))
+ (c
/ b))
+ (a
/ c))
- 3);
hence thesis by
A2;
end;
theorem ::
SERIES_5:23
((a
+ (1
/ a))
* (b
+ (1
/ b)))
>= (((
sqrt (a
* b))
+ (1
/ (
sqrt (a
* b))))
^2 )
proof
A1: (
sqrt (a
* b))
>
0 by
SQUARE_1: 25;
A2: ((a
+ (1
/ a))
* (b
+ (1
/ b)))
= ((((a
* b)
+ (a
* (1
/ b)))
+ ((1
/ a)
* b))
+ ((1
/ a)
* (1
/ b)))
.= ((((a
* b)
+ ((a
* 1)
/ b))
+ ((1
/ a)
* b))
+ ((1
/ a)
* (1
/ b))) by
XCMPLX_1: 74
.= ((((a
* b)
+ ((a
* 1)
/ b))
+ ((b
* 1)
/ a))
+ ((1
/ a)
* (1
/ b))) by
XCMPLX_1: 74
.= ((((a
* b)
+ ((a
* 1)
/ b))
+ ((b
* 1)
/ a))
+ ((1
* 1)
/ (a
* b))) by
XCMPLX_1: 76
.= ((((a
* b)
+ (a
/ b))
+ (b
/ a))
+ (1
/ (a
* b)));
((a
/ b)
+ (b
/ a))
>= (2
* (
sqrt ((a
/ b)
* (b
/ a)))) by
SIN_COS2: 1;
then ((a
/ b)
+ (b
/ a))
>= (2
* (
sqrt ((a
* b)
/ (b
* a)))) by
XCMPLX_1: 76;
then ((a
/ b)
+ (b
/ a))
>= (2
* 1) by
SQUARE_1: 18,
XCMPLX_1: 60;
then
A3: (((a
/ b)
+ (b
/ a))
+ ((a
* b)
+ (1
/ (a
* b))))
>= (2
+ ((a
* b)
+ (1
/ (a
* b)))) by
XREAL_1: 6;
(((
sqrt (a
* b))
+ (1
/ (
sqrt (a
* b))))
^2 )
= ((((
sqrt (a
* b))
^2 )
+ ((2
* (
sqrt (a
* b)))
* (1
/ (
sqrt (a
* b)))))
+ ((1
/ (
sqrt (a
* b)))
^2 ))
.= (((a
* b)
+ ((2
* (
sqrt (a
* b)))
* (1
/ (
sqrt (a
* b)))))
+ ((1
/ (
sqrt (a
* b)))
^2 )) by
SQUARE_1:def 2
.= (((a
* b)
+ ((2
* (
sqrt (a
* b)))
* (1
/ (
sqrt (a
* b)))))
+ ((1
^2 )
/ ((
sqrt (a
* b))
^2 ))) by
XCMPLX_1: 76
.= (((a
* b)
+ (2
* ((
sqrt (a
* b))
* (1
/ (
sqrt (a
* b))))))
+ (1
/ (a
* b))) by
SQUARE_1:def 2
.= (((a
* b)
+ (2
* (((
sqrt (a
* b))
* 1)
/ (
sqrt (a
* b)))))
+ (1
/ (a
* b))) by
XCMPLX_1: 74
.= (((a
* b)
+ (2
* 1))
+ (1
/ (a
* b))) by
A1,
XCMPLX_1: 60
.= (((a
* b)
+ 2)
+ (1
/ (a
* b)));
hence thesis by
A2,
A3;
end;
theorem ::
SERIES_5:24
((((b
* c)
/ a)
+ ((a
* c)
/ b))
+ ((a
* b)
/ c))
>= ((a
+ b)
+ c)
proof
A1: (((a
* c)
/ b)
+ ((a
* b)
/ c))
= ((a
* (c
/ b))
+ ((a
* b)
/ c)) by
XCMPLX_1: 74
.= ((a
* (c
/ b))
+ (a
* (b
/ c))) by
XCMPLX_1: 74
.= (a
* ((c
/ b)
+ (b
/ c)));
A2: (((a
* b)
/ c)
+ ((b
* c)
/ a))
= ((b
* (a
/ c))
+ ((b
* c)
/ a)) by
XCMPLX_1: 74
.= ((b
* (a
/ c))
+ (b
* (c
/ a))) by
XCMPLX_1: 74
.= (b
* ((a
/ c)
+ (c
/ a)));
A3: (b
* ((a
/ c)
+ (c
/ a)))
>= (b
* 2) by
SERIES_3: 3,
XREAL_1: 64;
A4: (c
* ((b
/ a)
+ (a
/ b)))
>= (c
* 2) by
SERIES_3: 3,
XREAL_1: 64;
(a
* ((c
/ b)
+ (b
/ c)))
>= (a
* 2) by
SERIES_3: 3,
XREAL_1: 64;
then ((a
* ((c
/ b)
+ (b
/ c)))
+ (b
* ((a
/ c)
+ (c
/ a))))
>= ((a
* 2)
+ (b
* 2)) by
A3,
XREAL_1: 7;
then
A5: (((a
* ((c
/ b)
+ (b
/ c)))
+ (b
* ((a
/ c)
+ (c
/ a))))
+ (c
* ((b
/ a)
+ (a
/ b))))
>= (((a
* 2)
+ (b
* 2))
+ (c
* 2)) by
A4,
XREAL_1: 7;
(((b
* c)
/ a)
+ ((a
* c)
/ b))
= ((c
* (b
/ a))
+ ((a
* c)
/ b)) by
XCMPLX_1: 74
.= ((c
* (b
/ a))
+ (c
* (a
/ b))) by
XCMPLX_1: 74
.= (c
* ((b
/ a)
+ (a
/ b)));
then ((2
* ((((b
* c)
/ a)
+ ((a
* c)
/ b))
+ ((a
* b)
/ c)))
/ 2)
>= ((2
* ((a
+ b)
+ c))
/ 2) by
A1,
A2,
A5,
XREAL_1: 72;
hence thesis;
end;
theorem ::
SERIES_5:25
x
> y & y
> z implies ((((x
^2 )
* y)
+ ((y
^2 )
* z))
+ ((z
^2 )
* x))
> (((x
* (y
^2 ))
+ (y
* (z
^2 )))
+ (z
* (x
^2 )))
proof
assume that
A1: x
> y and
A2: y
> z;
A3: (y
- z)
>
0 by
A2,
XREAL_1: 50;
x
> z by
A1,
A2,
XXREAL_0: 2;
then
A4: (x
- z)
>
0 by
XREAL_1: 50;
(x
- y)
>
0 by
A1,
XREAL_1: 50;
then (((x
- y)
* (y
- z))
* (x
- z))
>
0 by
A3,
A4;
then (((((x
^2 )
* y)
+ ((y
^2 )
* z))
+ ((z
^2 )
* x))
- (((x
* (y
^2 ))
+ (y
* (z
^2 )))
+ (z
* (x
^2 ))))
>
0 ;
hence thesis by
XREAL_1: 47;
end;
theorem ::
SERIES_5:26
a
> b & b
> c implies (b
/ (a
- b))
> (c
/ (a
- c))
proof
assume that
A1: a
> b and
A2: b
> c;
A3: (a
- b)
>
0 by
A1,
XREAL_1: 50;
(b
* (
- 1))
< (c
* (
- 1)) by
A2,
XREAL_1: 69;
then ((
- b)
+ a)
< ((
- c)
+ a) by
XREAL_1: 8;
then
A4: (c
/ (a
- b))
> (c
/ (a
- c)) by
A3,
XREAL_1: 76;
(b
/ (a
- b))
> (c
/ (a
- b)) by
A2,
A3,
XREAL_1: 74;
hence thesis by
A4,
XXREAL_0: 2;
end;
theorem ::
SERIES_5:27
b
> a & c
> d implies (c
/ (c
+ a))
> (d
/ (d
+ b))
proof
assume that
A1: b
> a and
A2: c
> d;
(b
* c)
> (a
* d) by
A1,
A2,
XREAL_1: 96;
then ((b
* c)
+ (c
* d))
> ((a
* d)
+ (c
* d)) by
XREAL_1: 8;
then (c
* (b
+ d))
> (d
* (a
+ c));
hence thesis by
XREAL_1: 106;
end;
theorem ::
SERIES_5:28
((m
* x)
+ (z
* y))
<= ((
sqrt ((m
^2 )
+ (z
^2 )))
* (
sqrt ((x
^2 )
+ (y
^2 ))))
proof
A1: (z
^2 )
>=
0 by
XREAL_1: 63;
A2: (m
^2 )
>=
0 by
XREAL_1: 63;
then
A3: (
sqrt ((m
^2 )
+ (z
^2 )))
>=
0 by
A1,
SQUARE_1:def 2;
A4: (((m
* x)
+ (z
* y))
^2 )
>=
0 by
XREAL_1: 63;
(((m
* y)
^2 )
+ ((z
* x)
^2 ))
>= ((2
* (m
* y))
* (z
* x)) by
SERIES_3: 6;
then
A5: ((((m
* y)
^2 )
+ ((z
* x)
^2 ))
+ (((m
^2 )
* (x
^2 ))
+ ((z
^2 )
* (y
^2 ))))
>= (((((2
* m)
* x)
* y)
* z)
+ (((m
^2 )
* (x
^2 ))
+ ((z
^2 )
* (y
^2 )))) by
XREAL_1: 6;
A6: (y
^2 )
>=
0 by
XREAL_1: 63;
A7: (x
^2 )
>=
0 by
XREAL_1: 63;
then
A8: (
sqrt ((x
^2 )
+ (y
^2 )))
>=
0 by
A6,
SQUARE_1:def 2;
(((
sqrt ((m
^2 )
+ (z
^2 )))
* (
sqrt ((x
^2 )
+ (y
^2 ))))
^2 )
= (((
sqrt ((m
^2 )
+ (z
^2 )))
^2 )
* ((
sqrt ((x
^2 )
+ (y
^2 )))
^2 ))
.= (((m
^2 )
+ (z
^2 ))
* ((
sqrt ((x
^2 )
+ (y
^2 )))
^2 )) by
A2,
A1,
SQUARE_1:def 2
.= (((m
^2 )
+ (z
^2 ))
* ((x
^2 )
+ (y
^2 ))) by
A7,
A6,
SQUARE_1:def 2
.= (((((m
^2 )
* (x
^2 ))
+ ((m
* y)
^2 ))
+ ((z
* x)
^2 ))
+ ((z
^2 )
* (y
^2 )));
then (
sqrt (((
sqrt ((m
^2 )
+ (z
^2 )))
* (
sqrt ((x
^2 )
+ (y
^2 ))))
^2 ))
>= (
sqrt (((m
* x)
+ (z
* y))
^2 )) by
A5,
A4,
SQUARE_1: 26;
then
A9: ((
sqrt ((m
^2 )
+ (z
^2 )))
* (
sqrt ((x
^2 )
+ (y
^2 ))))
>= (
sqrt (((m
* x)
+ (z
* y))
^2 )) by
A3,
A8,
SQUARE_1: 22;
per cases ;
suppose ((m
* x)
+ (z
* y))
>
0 ;
hence thesis by
A9,
SQUARE_1: 22;
end;
suppose ((m
* x)
+ (z
* y))
=
0 ;
hence thesis by
A3,
A8;
end;
suppose ((m
* x)
+ (z
* y))
<
0 ;
hence thesis by
A3,
A8;
end;
end;
theorem ::
SERIES_5:29
Th29: ((((m
* x)
+ (u
* y))
+ (w
* z))
^2 )
<= ((((m
^2 )
+ (u
^2 ))
+ (w
^2 ))
* (((x
^2 )
+ (y
^2 ))
+ (z
^2 )))
proof
(((m
^2 )
* (z
^2 ))
+ ((w
^2 )
* (x
^2 )))
= (((m
* z)
^2 )
+ ((w
* x)
^2 ));
then
A1: (((m
^2 )
* (z
^2 ))
+ ((w
^2 )
* (x
^2 )))
>= ((2
* (m
* z))
* (w
* x)) by
SERIES_3: 6;
(((u
^2 )
* (z
^2 ))
+ ((w
^2 )
* (y
^2 )))
= (((u
* z)
^2 )
+ ((w
* y)
^2 ));
then
A2: (((u
^2 )
* (z
^2 ))
+ ((w
^2 )
* (y
^2 )))
>= ((2
* (u
* z))
* (w
* y)) by
SERIES_3: 6;
(((m
* y)
^2 )
+ ((u
* x)
^2 ))
>= ((2
* (m
* y))
* (u
* x)) by
SERIES_3: 6;
then ((((m
^2 )
* (y
^2 ))
+ ((u
^2 )
* (x
^2 )))
+ (((m
^2 )
* (z
^2 ))
+ ((w
^2 )
* (x
^2 ))))
>= (((((2
* m)
* y)
* u)
* x)
+ ((((2
* m)
* z)
* w)
* x)) by
A1,
XREAL_1: 7;
then ((((((m
^2 )
* (y
^2 ))
+ ((u
^2 )
* (x
^2 )))
+ ((m
^2 )
* (z
^2 )))
+ ((w
^2 )
* (x
^2 )))
+ (((u
^2 )
* (z
^2 ))
+ ((w
^2 )
* (y
^2 ))))
>= ((((((2
* m)
* y)
* u)
* x)
+ ((((2
* m)
* z)
* w)
* x))
+ ((((2
* u)
* z)
* w)
* y)) by
A2,
XREAL_1: 7;
then ((((((((m
^2 )
* (y
^2 ))
+ ((u
^2 )
* (x
^2 )))
+ ((m
^2 )
* (z
^2 )))
+ ((w
^2 )
* (x
^2 )))
+ ((u
^2 )
* (z
^2 )))
+ ((w
^2 )
* (y
^2 )))
+ ((((m
* x)
^2 )
+ ((u
* y)
^2 ))
+ ((w
* z)
^2 )))
>= (((((((2
* m)
* y)
* u)
* x)
+ ((((2
* m)
* z)
* w)
* x))
+ ((((2
* u)
* z)
* w)
* y))
+ ((((m
* x)
^2 )
+ ((u
* y)
^2 ))
+ ((w
* z)
^2 ))) by
XREAL_1: 6;
hence thesis;
end;
theorem ::
SERIES_5:30
((((9
* a)
* b)
* c)
/ (((a
^2 )
+ (b
^2 ))
+ (c
^2 )))
<= ((a
+ b)
+ c)
proof
A1: ((b
^2 )
* (a
+ c))
>= ((b
^2 )
* (2
* (
sqrt (a
* c)))) by
SIN_COS2: 1,
XREAL_1: 64;
A2: ((c
^2 )
* (a
+ b))
>= ((c
^2 )
* (2
* (
sqrt (a
* b)))) by
SIN_COS2: 1,
XREAL_1: 64;
A3: (
sqrt (a
* b))
>
0 by
SQUARE_1: 25;
A4: (
sqrt (a
* c))
>
0 by
SQUARE_1: 25;
(
sqrt (b
* c))
>
0 by
SQUARE_1: 25;
then ((((2
* (a
^2 ))
* (
sqrt (b
* c)))
+ ((2
* (b
^2 ))
* (
sqrt (a
* c))))
+ ((2
* (c
^2 ))
* (
sqrt (a
* b))))
>= (3
* (3
-root ((((2
* (a
^2 ))
* (
sqrt (b
* c)))
* ((2
* (b
^2 ))
* (
sqrt (a
* c))))
* ((2
* (c
^2 ))
* (
sqrt (a
* b)))))) by
A4,
A3,
SERIES_3: 15;
then ((((2
* (a
^2 ))
* (
sqrt (b
* c)))
+ ((2
* (b
^2 ))
* (
sqrt (a
* c))))
+ ((2
* (c
^2 ))
* (
sqrt (a
* b))))
>= (3
* (3
-root ((((((((2
* (a
^2 ))
* (
sqrt (b
* c)))
* 2)
* (b
^2 ))
* (
sqrt (a
* c)))
* 2)
* (c
^2 ))
* (
sqrt (a
* b)))));
then ((((2
* (a
^2 ))
* (
sqrt (b
* c)))
+ ((2
* (b
^2 ))
* (
sqrt (a
* c))))
+ ((2
* (c
^2 ))
* (
sqrt (a
* b))))
>= (3
* (3
-root ((((2
* a)
* b)
* c)
|^ 3))) by
Lm9;
then
A5: ((((2
* (a
^2 ))
* (
sqrt (b
* c)))
+ ((2
* (b
^2 ))
* (
sqrt (a
* c))))
+ ((2
* (c
^2 ))
* (
sqrt (a
* b))))
>= (3
* (((2
* a)
* b)
* c)) by
POWER: 4;
A6: (((a
|^ 3)
+ (b
|^ 3))
+ (c
|^ 3))
>= (((3
* a)
* b)
* c) by
SERIES_3: 12;
((a
^2 )
* (b
+ c))
>= ((a
^2 )
* (2
* (
sqrt (b
* c)))) by
SIN_COS2: 1,
XREAL_1: 64;
then (((a
^2 )
* (b
+ c))
+ ((b
^2 )
* (a
+ c)))
>= (((a
^2 )
* (2
* (
sqrt (b
* c))))
+ ((b
^2 )
* (2
* (
sqrt (a
* c))))) by
A1,
XREAL_1: 7;
then ((((a
^2 )
* (b
+ c))
+ ((b
^2 )
* (a
+ c)))
+ ((c
^2 )
* (a
+ b)))
>= ((((2
* (a
^2 ))
* (
sqrt (b
* c)))
+ ((2
* (b
^2 ))
* (
sqrt (a
* c))))
+ ((2
* (c
^2 ))
* (
sqrt (a
* b)))) by
A2,
XREAL_1: 7;
then ((((((a
* (b
^2 ))
+ (a
* (c
^2 )))
+ (b
* (a
^2 )))
+ (b
* (c
^2 )))
+ (c
* (a
^2 )))
+ (c
* (b
^2 )))
>= (((6
* a)
* b)
* c) by
A5,
XXREAL_0: 2;
then
A7: ((((a
|^ 3)
+ (b
|^ 3))
+ (c
|^ 3))
+ ((((((a
* (b
^2 ))
+ (a
* (c
^2 )))
+ (b
* (a
^2 )))
+ (b
* (c
^2 )))
+ (c
* (a
^2 )))
+ (c
* (b
^2 ))))
>= ((((3
* a)
* b)
* c)
+ (((6
* a)
* b)
* c)) by
A6,
XREAL_1: 7;
((((a
^2 )
+ (b
^2 ))
+ (c
^2 ))
* ((a
+ b)
+ c))
= (((((((((a
* (a
^2 ))
+ (a
* (b
^2 )))
+ (a
* (c
^2 )))
+ (b
* (a
^2 )))
+ (b
* (b
^2 )))
+ (b
* (c
^2 )))
+ (c
* (a
^2 )))
+ (c
* (b
^2 )))
+ (c
* (c
^2 )))
.= (((((((((a
* (a
|^ 2))
+ (a
* (b
^2 )))
+ (a
* (c
^2 )))
+ (b
* (a
^2 )))
+ (b
* (b
^2 )))
+ (b
* (c
^2 )))
+ (c
* (a
^2 )))
+ (c
* (b
^2 )))
+ (c
* (c
^2 ))) by
NEWTON: 81
.= (((((((((a
|^ (2
+ 1))
+ (a
* (b
^2 )))
+ (a
* (c
^2 )))
+ (b
* (a
^2 )))
+ (b
* (b
^2 )))
+ (b
* (c
^2 )))
+ (c
* (a
^2 )))
+ (c
* (b
^2 )))
+ (c
* (c
^2 ))) by
NEWTON: 6
.= (((((((((a
|^ 3)
+ (a
* (b
^2 )))
+ (a
* (c
^2 )))
+ (b
* (a
^2 )))
+ (b
* (b
|^ 2)))
+ (b
* (c
^2 )))
+ (c
* (a
^2 )))
+ (c
* (b
^2 )))
+ (c
* (c
^2 ))) by
NEWTON: 81
.= (((((((((a
|^ 3)
+ (a
* (b
^2 )))
+ (a
* (c
^2 )))
+ (b
* (a
^2 )))
+ (b
|^ (2
+ 1)))
+ (b
* (c
^2 )))
+ (c
* (a
^2 )))
+ (c
* (b
^2 )))
+ (c
* (c
^2 ))) by
NEWTON: 6
.= (((((((((a
|^ 3)
+ (a
* (b
^2 )))
+ (a
* (c
^2 )))
+ (b
* (a
^2 )))
+ (b
|^ 3))
+ (b
* (c
^2 )))
+ (c
* (a
^2 )))
+ (c
* (b
^2 )))
+ (c
* (c
|^ 2))) by
NEWTON: 81
.= (((((((((a
|^ 3)
+ (a
* (b
^2 )))
+ (a
* (c
^2 )))
+ (b
* (a
^2 )))
+ (b
|^ 3))
+ (b
* (c
^2 )))
+ (c
* (a
^2 )))
+ (c
* (b
^2 )))
+ (c
|^ (2
+ 1))) by
NEWTON: 6
.= (((((((((a
|^ 3)
+ (b
|^ 3))
+ (c
|^ 3))
+ (a
* (b
^2 )))
+ (a
* (c
^2 )))
+ (b
* (a
^2 )))
+ (b
* (c
^2 )))
+ (c
* (a
^2 )))
+ (c
* (b
^2 )));
then ((((a
+ b)
+ c)
* (((a
^2 )
+ (b
^2 ))
+ (c
^2 )))
/ (((a
^2 )
+ (b
^2 ))
+ (c
^2 )))
>= ((((9
* a)
* b)
* c)
/ (((a
^2 )
+ (b
^2 ))
+ (c
^2 ))) by
A7,
XREAL_1: 72;
then (((a
+ b)
+ c)
/ ((((a
^2 )
+ (b
^2 ))
+ (c
^2 ))
/ (((a
^2 )
+ (b
^2 ))
+ (c
^2 ))))
>= ((((9
* a)
* b)
* c)
/ (((a
^2 )
+ (b
^2 ))
+ (c
^2 ))) by
XCMPLX_1: 77;
then (((a
+ b)
+ c)
/ 1)
>= ((((9
* a)
* b)
* c)
/ (((a
^2 )
+ (b
^2 ))
+ (c
^2 ))) by
XCMPLX_1: 60;
hence thesis;
end;
theorem ::
SERIES_5:31
((a
+ b)
+ c)
<= (((
sqrt ((((a
^2 )
+ (a
* b))
+ (b
^2 ))
/ 3))
+ (
sqrt ((((b
^2 )
+ (b
* c))
+ (c
^2 ))
/ 3)))
+ (
sqrt ((((c
^2 )
+ (c
* a))
+ (a
^2 ))
/ 3)))
proof
A1: (
sqrt 3)
>
0 by
SQUARE_1: 25;
A2: (
sqrt (((c
^2 )
+ (c
* a))
+ (a
^2 )))
>= (((1
/ 2)
* (
sqrt 3))
* (c
+ a)) by
Lm11;
A3: (
sqrt (((b
^2 )
+ (b
* c))
+ (c
^2 )))
>= (((1
/ 2)
* (
sqrt 3))
* (b
+ c)) by
Lm11;
(
sqrt (((a
^2 )
+ (a
* b))
+ (b
^2 )))
>= (((1
/ 2)
* (
sqrt 3))
* (a
+ b)) by
Lm11;
then ((
sqrt (((a
^2 )
+ (a
* b))
+ (b
^2 )))
+ (
sqrt (((b
^2 )
+ (b
* c))
+ (c
^2 ))))
>= ((((1
/ 2)
* (
sqrt 3))
* (a
+ b))
+ (((1
/ 2)
* (
sqrt 3))
* (b
+ c))) by
A3,
XREAL_1: 7;
then (((
sqrt (((a
^2 )
+ (a
* b))
+ (b
^2 )))
+ (
sqrt (((b
^2 )
+ (b
* c))
+ (c
^2 ))))
+ (
sqrt (((c
^2 )
+ (c
* a))
+ (a
^2 ))))
>= (((((1
/ 2)
* (
sqrt 3))
* (a
+ b))
+ (((1
/ 2)
* (
sqrt 3))
* (b
+ c)))
+ (((1
/ 2)
* (
sqrt 3))
* (c
+ a))) by
A2,
XREAL_1: 7;
then ((((
sqrt (((a
^2 )
+ (a
* b))
+ (b
^2 )))
+ (
sqrt (((b
^2 )
+ (b
* c))
+ (c
^2 ))))
+ (
sqrt (((c
^2 )
+ (c
* a))
+ (a
^2 ))))
/ (
sqrt 3))
>= ((((a
+ b)
+ c)
* (
sqrt 3))
/ (
sqrt 3)) by
A1,
XREAL_1: 72;
then ((((
sqrt (((a
^2 )
+ (a
* b))
+ (b
^2 )))
+ (
sqrt (((b
^2 )
+ (b
* c))
+ (c
^2 ))))
+ (
sqrt (((c
^2 )
+ (c
* a))
+ (a
^2 ))))
/ (
sqrt 3))
>= (((a
+ b)
+ c)
* ((
sqrt 3)
/ (
sqrt 3))) by
XCMPLX_1: 74;
then ((((
sqrt (((a
^2 )
+ (a
* b))
+ (b
^2 )))
+ (
sqrt (((b
^2 )
+ (b
* c))
+ (c
^2 ))))
+ (
sqrt (((c
^2 )
+ (c
* a))
+ (a
^2 ))))
/ (
sqrt 3))
>= (((a
+ b)
+ c)
* 1) by
A1,
XCMPLX_1: 60;
then ((((
sqrt (((a
^2 )
+ (a
* b))
+ (b
^2 )))
+ (
sqrt (((b
^2 )
+ (b
* c))
+ (c
^2 ))))
/ (
sqrt 3))
+ ((
sqrt (((c
^2 )
+ (c
* a))
+ (a
^2 )))
/ (
sqrt 3)))
>= ((a
+ b)
+ c) by
XCMPLX_1: 62;
then ((((
sqrt (((a
^2 )
+ (a
* b))
+ (b
^2 )))
/ (
sqrt 3))
+ ((
sqrt (((b
^2 )
+ (b
* c))
+ (c
^2 )))
/ (
sqrt 3)))
+ ((
sqrt (((c
^2 )
+ (c
* a))
+ (a
^2 )))
/ (
sqrt 3)))
>= ((a
+ b)
+ c) by
XCMPLX_1: 62;
then (((
sqrt ((((a
^2 )
+ (a
* b))
+ (b
^2 ))
/ 3))
+ ((
sqrt (((b
^2 )
+ (b
* c))
+ (c
^2 )))
/ (
sqrt 3)))
+ ((
sqrt (((c
^2 )
+ (c
* a))
+ (a
^2 )))
/ (
sqrt 3)))
>= ((a
+ b)
+ c) by
SQUARE_1: 30;
then (((
sqrt ((((a
^2 )
+ (a
* b))
+ (b
^2 ))
/ 3))
+ (
sqrt ((((b
^2 )
+ (b
* c))
+ (c
^2 ))
/ 3)))
+ ((
sqrt (((c
^2 )
+ (c
* a))
+ (a
^2 )))
/ (
sqrt 3)))
>= ((a
+ b)
+ c) by
SQUARE_1: 30;
hence thesis by
SQUARE_1: 30;
end;
theorem ::
SERIES_5:32
(((
sqrt ((((a
^2 )
+ (a
* b))
+ (b
^2 ))
/ 3))
+ (
sqrt ((((b
^2 )
+ (b
* c))
+ (c
^2 ))
/ 3)))
+ (
sqrt ((((c
^2 )
+ (c
* a))
+ (a
^2 ))
/ 3)))
<= (((
sqrt (((a
^2 )
+ (b
^2 ))
/ 2))
+ (
sqrt (((b
^2 )
+ (c
^2 ))
/ 2)))
+ (
sqrt (((c
^2 )
+ (a
^2 ))
/ 2)))
proof
A1: (
sqrt ((((b
^2 )
+ (b
* c))
+ (c
^2 ))
/ 3))
<= (
sqrt (((b
^2 )
+ (c
^2 ))
/ 2)) by
Lm12;
A2: (
sqrt ((((c
^2 )
+ (c
* a))
+ (a
^2 ))
/ 3))
<= (
sqrt (((c
^2 )
+ (a
^2 ))
/ 2)) by
Lm12;
(
sqrt ((((a
^2 )
+ (a
* b))
+ (b
^2 ))
/ 3))
<= (
sqrt (((a
^2 )
+ (b
^2 ))
/ 2)) by
Lm12;
then ((
sqrt ((((a
^2 )
+ (a
* b))
+ (b
^2 ))
/ 3))
+ (
sqrt ((((b
^2 )
+ (b
* c))
+ (c
^2 ))
/ 3)))
<= ((
sqrt (((a
^2 )
+ (b
^2 ))
/ 2))
+ (
sqrt (((b
^2 )
+ (c
^2 ))
/ 2))) by
A1,
XREAL_1: 7;
hence thesis by
A2,
XREAL_1: 7;
end;
theorem ::
SERIES_5:33
(((
sqrt (((a
^2 )
+ (b
^2 ))
/ 2))
+ (
sqrt (((b
^2 )
+ (c
^2 ))
/ 2)))
+ (
sqrt (((c
^2 )
+ (a
^2 ))
/ 2)))
<= (
sqrt (3
* (((a
^2 )
+ (b
^2 ))
+ (c
^2 ))))
proof
A1: ((
sqrt (((a
^2 )
+ (b
^2 ))
/ 2))
^2 )
= (((a
^2 )
+ (b
^2 ))
/ 2) by
SQUARE_1:def 2;
A2: ((
sqrt (((b
^2 )
+ (c
^2 ))
/ 2))
^2 )
= (((b
^2 )
+ (c
^2 ))
/ 2) by
SQUARE_1:def 2;
A3: (
sqrt (((c
^2 )
+ (a
^2 ))
/ 2))
>
0 by
SQUARE_1: 25;
A4: (
sqrt (((b
^2 )
+ (c
^2 ))
/ 2))
>
0 by
SQUARE_1: 25;
A5: ((((
sqrt (((a
^2 )
+ (b
^2 ))
/ 2))
+ (
sqrt (((b
^2 )
+ (c
^2 ))
/ 2)))
+ (
sqrt (((c
^2 )
+ (a
^2 ))
/ 2)))
^2 )
>=
0 by
XREAL_1: 63;
A6: (
sqrt (((a
^2 )
+ (b
^2 ))
/ 2))
>
0 by
SQUARE_1: 25;
A7: ((
sqrt (((c
^2 )
+ (a
^2 ))
/ 2))
^2 )
= (((c
^2 )
+ (a
^2 ))
/ 2) by
SQUARE_1:def 2;
((((1
* (
sqrt (((a
^2 )
+ (b
^2 ))
/ 2)))
+ (1
* (
sqrt (((b
^2 )
+ (c
^2 ))
/ 2))))
+ (1
* (
sqrt (((c
^2 )
+ (a
^2 ))
/ 2))))
^2 )
<= ((((1
^2 )
+ (1
^2 ))
+ (1
^2 ))
* ((((
sqrt (((a
^2 )
+ (b
^2 ))
/ 2))
^2 )
+ ((
sqrt (((b
^2 )
+ (c
^2 ))
/ 2))
^2 ))
+ ((
sqrt (((c
^2 )
+ (a
^2 ))
/ 2))
^2 ))) by
Th29;
then (
sqrt ((((
sqrt (((a
^2 )
+ (b
^2 ))
/ 2))
+ (
sqrt (((b
^2 )
+ (c
^2 ))
/ 2)))
+ (
sqrt (((c
^2 )
+ (a
^2 ))
/ 2)))
^2 ))
<= (
sqrt (3
* (((a
^2 )
+ (b
^2 ))
+ (c
^2 )))) by
A1,
A2,
A7,
A5,
SQUARE_1: 26;
hence thesis by
A6,
A4,
A3,
SQUARE_1: 22;
end;
theorem ::
SERIES_5:34
(
sqrt (3
* (((a
^2 )
+ (b
^2 ))
+ (c
^2 ))))
<= ((((b
* c)
/ a)
+ ((c
* a)
/ b))
+ ((a
* b)
/ c))
proof
A1: ((((b
* c)
/ a)
^2 )
+ (((c
* a)
/ b)
^2 ))
>= (2
* (c
^2 )) by
Lm13;
A2: ((((c
* a)
/ b)
^2 )
+ (((a
* b)
/ c)
^2 ))
>= (2
* (a
^2 )) by
Lm13;
((((b
* c)
/ a)
^2 )
+ (((a
* b)
/ c)
^2 ))
>= (2
* (b
^2 )) by
Lm13;
then (((((c
* a)
/ b)
^2 )
+ (((a
* b)
/ c)
^2 ))
+ ((((b
* c)
/ a)
^2 )
+ (((a
* b)
/ c)
^2 )))
>= ((2
* (a
^2 ))
+ (2
* (b
^2 ))) by
A2,
XREAL_1: 7;
then (((((((c
* a)
/ b)
^2 )
+ (((a
* b)
/ c)
^2 ))
+ (((b
* c)
/ a)
^2 ))
+ (((a
* b)
/ c)
^2 ))
+ ((((b
* c)
/ a)
^2 )
+ (((c
* a)
/ b)
^2 )))
>= (((2
* (a
^2 ))
+ (2
* (b
^2 )))
+ (2
* (c
^2 ))) by
A1,
XREAL_1: 7;
then (((((((c
* a)
/ b)
^2 )
+ (((a
* b)
/ c)
^2 ))
+ (((b
* c)
/ a)
^2 ))
* 2)
/ 2)
>= (((((a
^2 )
+ (b
^2 ))
+ (c
^2 ))
* 2)
/ 2) by
XREAL_1: 72;
then ((((((c
* a)
/ b)
^2 )
+ (((a
* b)
/ c)
^2 ))
+ (((b
* c)
/ a)
^2 ))
+ (2
* (((a
^2 )
+ (b
^2 ))
+ (c
^2 ))))
>= ((((a
^2 )
+ (b
^2 ))
+ (c
^2 ))
+ (2
* (((a
^2 )
+ (b
^2 ))
+ (c
^2 )))) by
XREAL_1: 6;
then (((((b
* c)
/ a)
+ ((c
* a)
/ b))
+ ((a
* b)
/ c))
^2 )
>= (3
* (((a
^2 )
+ (b
^2 ))
+ (c
^2 ))) by
Lm16;
then (
sqrt (((((b
* c)
/ a)
+ ((c
* a)
/ b))
+ ((a
* b)
/ c))
^2 ))
>= (
sqrt (3
* (((a
^2 )
+ (b
^2 ))
+ (c
^2 )))) by
SQUARE_1: 26;
hence thesis by
SQUARE_1: 22;
end;
theorem ::
SERIES_5:35
(a
+ b)
= 1 implies (((1
/ (a
^2 ))
- 1)
* ((1
/ (b
^2 ))
- 1))
>= 9
proof
assume
A1: (a
+ b)
= 1;
(
sqrt (a
* b))
>
0 by
SQUARE_1: 25;
then (1
^2 )
>= ((2
* (
sqrt (a
* b)))
^2 ) by
A1,
SIN_COS2: 1,
SQUARE_1: 15;
then 1
>= ((2
* 2)
* ((
sqrt (a
* b))
^2 ));
then 1
>= (4
* (a
* b)) by
SQUARE_1:def 2;
then (8
/ 1)
<= (8
/ ((4
* a)
* b)) by
XREAL_1: 118;
then 8
<= (8
/ (4
* (a
* b)));
then 8
<= ((8
/ 4)
/ (a
* b)) by
XCMPLX_1: 78;
then
A2: (8
+ 1)
<= ((2
/ (a
* b))
+ 1) by
XREAL_1: 7;
(((1
/ (a
^2 ))
- 1)
* ((1
/ (b
^2 ))
- 1))
= (((1
- (1
* (a
^2 )))
/ (a
^2 ))
* ((1
/ (b
^2 ))
- 1)) by
XCMPLX_1: 126
.= (((1
- (1
* (a
^2 )))
/ (a
^2 ))
* ((1
- (1
* (b
^2 )))
/ (b
^2 ))) by
XCMPLX_1: 126
.= ((((1
- a)
* (1
+ a))
* ((1
- b)
* (1
+ b)))
/ ((a
^2 )
* (b
^2 ))) by
XCMPLX_1: 76;
then (((1
/ (a
^2 ))
- 1)
* ((1
/ (b
^2 ))
- 1))
= (((a
* b)
* ((1
+ a)
* (1
+ b)))
/ ((a
* b)
* (a
* b))) by
A1
.= (((a
* b)
/ (a
* b))
* (((1
+ a)
* (1
+ b))
/ (a
* b))) by
XCMPLX_1: 76
.= (1
* (((1
+ a)
* (1
+ b))
/ (a
* b))) by
XCMPLX_1: 60
.= (((1
+ (a
+ b))
+ (a
* b))
/ (a
* b))
.= ((2
/ (a
* b))
+ ((a
* b)
/ (a
* b))) by
A1,
XCMPLX_1: 62
.= ((2
/ (a
* b))
+ 1) by
XCMPLX_1: 60;
hence thesis by
A2;
end;
theorem ::
SERIES_5:36
(a
+ b)
= 1 implies ((a
* b)
+ (1
/ (a
* b)))
>= (17
/ 4)
proof
A1: (
sqrt (a
* b))
>
0 by
SQUARE_1: 25;
assume (a
+ b)
= 1;
then (1
^2 )
>= ((2
* (
sqrt (a
* b)))
^2 ) by
A1,
SIN_COS2: 1,
SQUARE_1: 15;
then 1
>= ((2
* 2)
* ((
sqrt (a
* b))
^2 ));
then 1
>= (4
* (a
* b)) by
SQUARE_1:def 2;
then
A2: (1
/ 4)
>= (((a
* b)
* 4)
/ 4) by
XREAL_1: 72;
then ((1
/ 4)
* (
- 1))
<= ((a
* b)
* (
- 1)) by
XREAL_1: 65;
then ((
- (1
/ 4))
+ 1)
<= ((
- (a
* b))
+ 1) by
XREAL_1: 7;
then ((3
/ 4)
^2 )
<= ((1
- (a
* b))
^2 ) by
SQUARE_1: 15;
then ((9
/ (4
^2 ))
/ (1
/ 4))
<= (((1
- (a
* b))
^2 )
/ (1
/ 4)) by
XREAL_1: 72;
then
A3: ((9
/ 4)
+ (8
/ 4))
<= ((((1
- (a
* b))
^2 )
* 4)
+ 2) by
XREAL_1: 7;
((1
- (a
* b))
^2 )
>=
0 by
XREAL_1: 63;
then (((1
- (a
* b))
^2 )
/ (1
/ 4))
<= (((1
- (a
* b))
^2 )
/ (a
* b)) by
A2,
XREAL_1: 118;
then
A4: ((((1
- (a
* b))
^2 )
* 4)
+ 2)
<= ((((1
- (a
* b))
^2 )
/ (a
* b))
+ 2) by
XREAL_1: 7;
((1
/ (a
* b))
+ (a
* b))
= ((1
+ ((a
* b)
* (a
* b)))
/ (a
* b)) by
XCMPLX_1: 113
.= (((((1
^2 )
- ((2
* 1)
* (a
* b)))
+ ((a
* b)
^2 ))
+ (2
* (a
* b)))
/ (a
* b))
.= ((((1
- (a
* b))
^2 )
/ (a
* b))
+ ((2
* (a
* b))
/ (a
* b))) by
XCMPLX_1: 62
.= ((((1
- (a
* b))
^2 )
/ (a
* b))
+ (2
* ((a
* b)
/ (a
* b)))) by
XCMPLX_1: 74
.= ((((1
- (a
* b))
^2 )
/ (a
* b))
+ (2
* 1)) by
XCMPLX_1: 60
.= ((((1
- (a
* b))
^2 )
/ (a
* b))
+ 2);
hence thesis by
A4,
A3,
XXREAL_0: 2;
end;
theorem ::
SERIES_5:37
((a
+ b)
+ c)
= 1 implies (((1
/ a)
+ (1
/ b))
+ (1
/ c))
>= 9
proof
assume
A1: ((a
+ b)
+ c)
= 1;
A2: (3
-root ((a
* b)
* c))
>=
0 by
POWER: 7;
(((1
/ a)
+ (1
/ b))
+ (1
/ c))
>= (3
* (3
-root (((1
/ a)
* (1
/ b))
* (1
/ c)))) by
SERIES_3: 15;
then
A3: (((1
/ a)
+ (1
/ b))
+ (1
/ c))
>= (3
* (3
-root (1
/ ((a
* b)
* c)))) by
Lm3;
A4: (3
-root (1
/ ((a
* b)
* c)))
>=
0 by
POWER: 7;
((a
+ b)
+ c)
>= (3
* (3
-root ((a
* b)
* c))) by
SERIES_3: 15;
then (((a
+ b)
+ c)
* (((1
/ a)
+ (1
/ b))
+ (1
/ c)))
>= ((3
* (3
-root ((a
* b)
* c)))
* (3
* (3
-root (1
/ ((a
* b)
* c))))) by
A2,
A3,
A4,
XREAL_1: 66;
then (((1
/ a)
+ (1
/ b))
+ (1
/ c))
>= (9
* ((3
-root ((a
* b)
* c))
* (3
-root (1
/ ((a
* b)
* c))))) by
A1;
then (((1
/ a)
+ (1
/ b))
+ (1
/ c))
>= (9
* (3
-root (((a
* b)
* c)
* (1
/ ((a
* b)
* c))))) by
POWER: 11;
then (((1
/ a)
+ (1
/ b))
+ (1
/ c))
>= (9
* (3
-root (((a
* b)
* c)
/ (((a
* b)
* c)
/ 1)))) by
XCMPLX_1: 79;
then (((1
/ a)
+ (1
/ b))
+ (1
/ c))
>= (9
* (3
-root 1)) by
XCMPLX_1: 60;
then (((1
/ a)
+ (1
/ b))
+ (1
/ c))
>= (9
* 1) by
POWER: 6;
hence thesis;
end;
theorem ::
SERIES_5:38
((a
+ b)
+ c)
= 1 implies ((((1
/ a)
- 1)
* ((1
/ b)
- 1))
* ((1
/ c)
- 1))
>= 8
proof
A1: ((a
+ c)
/ b)
>= ((2
* (
sqrt (a
* c)))
/ b) by
SIN_COS2: 1,
XREAL_1: 72;
A2: ((a
+ b)
/ c)
>= ((2
* (
sqrt (a
* b)))
/ c) by
SIN_COS2: 1,
XREAL_1: 72;
A3: (
sqrt (a
* b))
>
0 by
SQUARE_1: 25;
A4: (
sqrt (a
* c))
>
0 by
SQUARE_1: 25;
assume
A5: ((a
+ b)
+ c)
= 1;
then
A6: ((((1
/ a)
- 1)
* ((1
/ b)
- 1))
* ((1
/ c)
- 1))
= ((((b
+ c)
/ a)
* ((1
/ b)
- 1))
* ((1
/ c)
- 1)) by
Lm17
.= ((((b
+ c)
/ a)
* ((a
+ c)
/ b))
* ((1
/ c)
- 1)) by
A5,
Lm17
.= ((((b
+ c)
/ a)
* ((a
+ c)
/ b))
* ((((a
+ b)
/ c)
+ (c
/ c))
- 1)) by
A5,
XCMPLX_1: 62
.= ((((b
+ c)
/ a)
* ((a
+ c)
/ b))
* ((((a
+ b)
/ c)
+ 1)
- 1)) by
XCMPLX_1: 60
.= ((((b
+ c)
/ a)
* ((a
+ c)
/ b))
* ((a
+ b)
/ c));
A7: (
sqrt (b
* c))
>
0 by
SQUARE_1: 25;
((b
+ c)
/ a)
>= ((2
* (
sqrt (b
* c)))
/ a) by
SIN_COS2: 1,
XREAL_1: 72;
then (((b
+ c)
/ a)
* ((a
+ c)
/ b))
>= (((2
* (
sqrt (b
* c)))
/ a)
* ((2
* (
sqrt (a
* c)))
/ b)) by
A1,
A7,
A4,
XREAL_1: 66;
then ((((1
/ a)
- 1)
* ((1
/ b)
- 1))
* ((1
/ c)
- 1))
>= ((((2
* (
sqrt (b
* c)))
/ a)
* ((2
* (
sqrt (a
* c)))
/ b))
* ((2
* (
sqrt (a
* b)))
/ c)) by
A6,
A2,
A7,
A4,
A3,
XREAL_1: 66;
hence thesis by
Lm18;
end;
theorem ::
SERIES_5:39
((a
+ b)
+ c)
= 1 implies (((1
+ (1
/ a))
* (1
+ (1
/ b)))
* (1
+ (1
/ c)))
>= 64
proof
A1: (
sqrt (b
* c))
>
0 by
SQUARE_1: 25;
((a
+ b)
/ c)
>= ((2
* (
sqrt (a
* b)))
/ c) by
SIN_COS2: 1,
XREAL_1: 72;
then (2
+ ((a
+ b)
/ c))
>= (2
+ ((2
* (
sqrt (a
* b)))
/ c)) by
XREAL_1: 6;
then
A2: (2
+ ((a
+ b)
/ c))
>= (2
+ (2
* ((
sqrt (a
* b))
/ c))) by
XCMPLX_1: 74;
A3: (
sqrt (a
* b))
>
0 by
SQUARE_1: 25;
((a
+ c)
/ b)
>= ((2
* (
sqrt (a
* c)))
/ b) by
SIN_COS2: 1,
XREAL_1: 72;
then (2
+ ((a
+ c)
/ b))
>= (2
+ ((2
* (
sqrt (a
* c)))
/ b)) by
XREAL_1: 6;
then
A4: (2
+ ((a
+ c)
/ b))
>= (2
+ (2
* ((
sqrt (a
* c))
/ b))) by
XCMPLX_1: 74;
A5: (
sqrt (a
* c))
>
0 by
SQUARE_1: 25;
((b
+ c)
/ a)
>= ((2
* (
sqrt (b
* c)))
/ a) by
SIN_COS2: 1,
XREAL_1: 72;
then (2
+ ((b
+ c)
/ a))
>= (2
+ ((2
* (
sqrt (b
* c)))
/ a)) by
XREAL_1: 6;
then (2
+ ((b
+ c)
/ a))
>= (2
+ (2
* ((
sqrt (b
* c))
/ a))) by
XCMPLX_1: 74;
then ((2
+ ((b
+ c)
/ a))
* (2
+ ((a
+ c)
/ b)))
>= ((2
* (1
+ ((
sqrt (b
* c))
/ a)))
* (2
* (1
+ ((
sqrt (a
* c))
/ b)))) by
A4,
A1,
A5,
XREAL_1: 66;
then
A6: (((2
+ ((b
+ c)
/ a))
* (2
+ ((a
+ c)
/ b)))
* (2
+ ((a
+ b)
/ c)))
>= (((2
* (1
+ ((
sqrt (b
* c))
/ a)))
* (2
* (1
+ ((
sqrt (a
* c))
/ b))))
* (2
* (1
+ ((
sqrt (a
* b))
/ c)))) by
A2,
A1,
A5,
A3,
XREAL_1: 66;
(((((((
sqrt (a
* c))
/ b)
+ (b
/ (
sqrt (a
* c))))
+ ((
sqrt (a
* b))
/ c))
+ (c
/ (
sqrt (b
* a))))
+ (a
/ (
sqrt (b
* c))))
+ ((
sqrt (b
* c))
/ a))
>= 6 by
Lm23;
then (2
+ (((((((
sqrt (a
* c))
/ b)
+ (b
/ (
sqrt (a
* c))))
+ ((
sqrt (a
* b))
/ c))
+ (c
/ (
sqrt (b
* a))))
+ (a
/ (
sqrt (b
* c))))
+ ((
sqrt (b
* c))
/ a)))
>= (6
+ 2) by
XREAL_1: 6;
then
A7: (8
* ((((((2
+ ((
sqrt (a
* c))
/ b))
+ (b
/ (
sqrt (a
* c))))
+ ((
sqrt (a
* b))
/ c))
+ (c
/ (
sqrt (b
* a))))
+ (a
/ (
sqrt (b
* c))))
+ ((
sqrt (b
* c))
/ a)))
>= (8
* 8) by
XREAL_1: 64;
assume
A8: ((a
+ b)
+ c)
= 1;
then (((1
+ (1
/ a))
* (1
+ (1
/ b)))
* (1
+ (1
/ c)))
= (((2
+ ((b
+ c)
/ a))
* (1
+ (1
/ b)))
* (1
+ (1
/ c))) by
Lm19
.= (((2
+ ((b
+ c)
/ a))
* (2
+ ((a
+ c)
/ b)))
* (1
+ (1
/ c))) by
A8,
Lm19
.= (((2
+ ((b
+ c)
/ a))
* (2
+ ((a
+ c)
/ b)))
* (1
+ (((a
+ b)
/ c)
+ (c
/ c)))) by
A8,
XCMPLX_1: 62
.= (((2
+ ((b
+ c)
/ a))
* (2
+ ((a
+ c)
/ b)))
* ((1
+ ((a
+ b)
/ c))
+ 1)) by
XCMPLX_1: 60
.= (((2
+ ((b
+ c)
/ a))
* (2
+ ((a
+ c)
/ b)))
* (2
+ ((a
+ b)
/ c)));
then (((1
+ (1
/ a))
* (1
+ (1
/ b)))
* (1
+ (1
/ c)))
>= (8
* (((1
+ ((
sqrt (b
* c))
/ a))
* (1
+ ((
sqrt (a
* c))
/ b)))
* (1
+ ((
sqrt (a
* b))
/ c)))) by
A6;
then (((1
+ (1
/ a))
* (1
+ (1
/ b)))
* (1
+ (1
/ c)))
>= (8
* ((((((2
+ ((
sqrt (a
* c))
/ b))
+ (b
/ (
sqrt (a
* c))))
+ ((
sqrt (a
* b))
/ c))
+ (c
/ (
sqrt (b
* a))))
+ (a
/ (
sqrt (b
* c))))
+ ((
sqrt (b
* c))
/ a))) by
Lm22;
hence thesis by
A7,
XXREAL_0: 2;
end;
theorem ::
SERIES_5:40
((x
+ y)
+ z)
= 1 implies (((x
^2 )
+ (y
^2 ))
+ (z
^2 ))
>= (1
/ 3)
proof
A1: (((y
^2 )
+ (z
^2 ))
/ 2)
>= (y
* z) by
SERIES_3: 7;
A2: (((x
^2 )
+ (z
^2 ))
/ 2)
>= (x
* z) by
SERIES_3: 7;
(((x
^2 )
+ (y
^2 ))
/ 2)
>= (x
* y) by
SERIES_3: 7;
then ((((x
^2 )
+ (y
^2 ))
/ 2)
+ (((y
^2 )
+ (z
^2 ))
/ 2))
>= ((y
* z)
+ (x
* y)) by
A1,
XREAL_1: 7;
then (((((x
^2 )
+ (y
^2 ))
/ 2)
+ (((y
^2 )
+ (z
^2 ))
/ 2))
+ (((x
^2 )
+ (z
^2 ))
/ 2))
>= (((y
* z)
+ (x
* y))
+ (x
* z)) by
A2,
XREAL_1: 7;
then (
- (((((x
^2 )
+ (y
^2 ))
/ 2)
+ (((y
^2 )
+ (z
^2 ))
/ 2))
+ (((x
^2 )
+ (z
^2 ))
/ 2)))
<= (
- (((y
* z)
+ (x
* y))
+ (x
* z))) by
XREAL_1: 24;
then ((
- (((((x
^2 )
+ (y
^2 ))
/ 2)
+ (((y
^2 )
+ (z
^2 ))
/ 2))
+ (((x
^2 )
+ (z
^2 ))
/ 2)))
* 2)
<= ((
- (((y
* z)
+ (x
* y))
+ (x
* z)))
* 2) by
XREAL_1: 64;
then ((
- ((((((x
^2 )
+ (y
^2 ))
/ 2)
+ (((y
^2 )
+ (z
^2 ))
/ 2))
+ (((x
^2 )
+ (z
^2 ))
/ 2))
* 2))
+ 1)
<= ((
- ((((y
* z)
+ (x
* y))
+ (x
* z))
* 2))
+ 1) by
XREAL_1: 6;
then
A3: (1
- ((((x
^2 )
+ (y
^2 ))
+ (z
^2 ))
* 2))
<= (1
- ((((y
* z)
+ (x
* y))
+ (x
* z))
* 2));
assume ((x
+ y)
+ z)
= 1;
then ((((((x
^2 )
+ (y
^2 ))
+ (z
^2 ))
+ ((2
* x)
* y))
+ ((2
* y)
* z))
+ ((2
* z)
* x))
= (1
^2 ) by
Lm6;
then 1
<= ((((x
^2 )
+ (y
^2 ))
+ (z
^2 ))
+ ((((x
^2 )
+ (y
^2 ))
+ (z
^2 ))
* 2)) by
A3,
XREAL_1: 20;
then (1
/ 3)
<= (((((x
^2 )
+ (y
^2 ))
+ (z
^2 ))
* 3)
/ 3) by
XREAL_1: 72;
hence thesis;
end;
theorem ::
SERIES_5:41
((x
+ y)
+ z)
= 1 implies (((x
* y)
+ (y
* z))
+ (z
* x))
<= (1
/ 3)
proof
(((x
^2 )
+ (y
^2 ))
+ (z
^2 ))
>= (((x
* y)
+ (y
* z))
+ (x
* z)) by
SERIES_3: 10;
then
A1: ((((x
^2 )
+ (y
^2 ))
+ (z
^2 ))
+ (2
* (((x
* y)
+ (y
* z))
+ (z
* x))))
>= ((((x
* y)
+ (y
* z))
+ (x
* z))
+ (2
* (((x
* y)
+ (y
* z))
+ (z
* x)))) by
XREAL_1: 7;
assume ((x
+ y)
+ z)
= 1;
then (1
^2 )
= ((((((x
^2 )
+ (y
^2 ))
+ (z
^2 ))
+ ((2
* x)
* y))
+ ((2
* y)
* z))
+ ((2
* z)
* x)) by
Lm6;
then (1
/ 3)
>= ((3
* (((x
* y)
+ (y
* z))
+ (z
* x)))
/ 3) by
A1,
XREAL_1: 72;
hence thesis;
end;
theorem ::
SERIES_5:42
a
> b & b
> c implies (((a
to_power (2
* a))
* (b
to_power (2
* b)))
* (c
to_power (2
* c)))
> (((a
to_power (b
+ c))
* (b
to_power (a
+ c)))
* (c
to_power (a
+ b)))
proof
assume that
A1: a
> b and
A2: b
> c;
A3: (b
/ c)
> 1 by
A2,
XREAL_1: 187;
set e = (((a
to_power (b
+ c))
* (b
to_power (a
+ c)))
* (c
to_power (a
+ b)));
A4: (b
to_power (c
+ a))
>
0 by
POWER: 34;
(b
- c)
>
0 by
A2,
XREAL_1: 50;
then
A5: ((b
/ c)
to_power (b
- c))
> 1 by
A3,
POWER: 35;
A6: (a
/ b)
> 1 by
A1,
XREAL_1: 187;
(a
- b)
>
0 by
A1,
XREAL_1: 50;
then ((a
/ b)
to_power (a
- b))
> 1 by
A6,
POWER: 35;
then
A7: (((a
/ b)
to_power (a
- b))
* ((b
/ c)
to_power (b
- c)))
> 1 by
A5,
XREAL_1: 161;
A8: (c
to_power (a
+ b))
>
0 by
POWER: 34;
A9: a
> c by
A1,
A2,
XXREAL_0: 2;
then
A10: (a
/ c)
> 1 by
XREAL_1: 187;
set d = (((a
to_power (2
* a))
* (b
to_power (2
* b)))
* (c
to_power (2
* c)));
A11: (a
to_power (b
+ c))
>
0 by
POWER: 34;
(a
- c)
>
0 by
A9,
XREAL_1: 50;
then ((a
/ c)
to_power (a
- c))
> 1 by
A10,
POWER: 35;
then ((((a
/ b)
to_power (a
- b))
* ((b
/ c)
to_power (b
- c)))
* ((a
/ c)
to_power (
- (c
- a))))
> 1 by
A7,
XREAL_1: 161;
then ((((a
/ b)
to_power (a
- b))
* ((b
/ c)
to_power (b
- c)))
* ((c
/ a)
to_power (c
- a)))
> 1 by
Lm4;
then ((((a
to_power (a
- b))
/ (b
to_power (a
- b)))
* ((b
/ c)
to_power (b
- c)))
* ((c
/ a)
to_power (c
- a)))
> 1 by
POWER: 31;
then ((((a
to_power (a
- b))
/ (b
to_power (a
- b)))
* ((b
to_power (b
- c))
/ (c
to_power (b
- c))))
* ((c
/ a)
to_power (c
- a)))
> 1 by
POWER: 31;
then ((((a
to_power (a
- b))
/ (b
to_power (a
- b)))
* ((b
to_power (b
- c))
/ (c
to_power (b
- c))))
* ((c
to_power (c
- a))
/ (a
to_power (c
- a))))
> 1 by
POWER: 31;
then ((((a
to_power (a
- b))
* (b
to_power (b
- c)))
/ ((c
to_power (b
- c))
* (b
to_power (a
- b))))
* ((c
to_power (c
- a))
/ (a
to_power (c
- a))))
> 1 by
XCMPLX_1: 76;
then ((((a
to_power (a
- b))
/ (c
to_power (b
- c)))
* ((b
to_power (b
- c))
/ (b
to_power (a
- b))))
* ((c
to_power (c
- a))
/ (a
to_power (c
- a))))
> 1 by
XCMPLX_1: 76;
then ((((a
to_power (a
- b))
/ (c
to_power (b
- c)))
* (b
to_power ((b
- c)
- (a
- b))))
* ((c
to_power (c
- a))
/ (a
to_power (c
- a))))
> 1 by
POWER: 29;
then ((((a
to_power (a
- b))
/ (c
to_power (b
- c)))
* ((c
to_power (c
- a))
/ (a
to_power (c
- a))))
* (b
to_power (((2
* b)
- a)
- c)))
> 1;
then ((((a
to_power (a
- b))
/ (a
to_power (c
- a)))
* ((c
to_power (c
- a))
/ (c
to_power (b
- c))))
* (b
to_power (((2
* b)
- a)
- c)))
> 1 by
XCMPLX_1: 85;
then (((a
to_power ((a
- b)
- (c
- a)))
* ((c
to_power (c
- a))
/ (c
to_power (b
- c))))
* (b
to_power (((2
* b)
- a)
- c)))
> 1 by
POWER: 29;
then (((a
to_power (((2
* a)
- b)
- c))
* (c
to_power ((c
- a)
- (b
- c))))
* (b
to_power (((2
* b)
- a)
- c)))
> 1 by
POWER: 29;
then (((a
to_power ((2
* a)
- (b
+ c)))
* (c
to_power ((2
* c)
- (a
+ b))))
* (b
to_power ((2
* b)
- (a
+ c))))
> 1;
then ((((a
to_power (2
* a))
/ (a
to_power (b
+ c)))
* (c
to_power ((2
* c)
- (a
+ b))))
* (b
to_power ((2
* b)
- (a
+ c))))
> 1 by
POWER: 29;
then ((((a
to_power (2
* a))
/ (a
to_power (b
+ c)))
* ((c
to_power (2
* c))
/ (c
to_power (a
+ b))))
* (b
to_power ((2
* b)
- (a
+ c))))
> 1 by
POWER: 29;
then ((((a
to_power (2
* a))
* (c
to_power (2
* c)))
/ ((a
to_power (b
+ c))
* (c
to_power (a
+ b))))
* (b
to_power ((2
* b)
- (a
+ c))))
> 1 by
XCMPLX_1: 76;
then ((((a
to_power (2
* a))
* (c
to_power (2
* c)))
/ ((a
to_power (b
+ c))
* (c
to_power (a
+ b))))
* ((b
to_power (2
* b))
/ (b
to_power (a
+ c))))
> 1 by
POWER: 29;
then ((((a
to_power (2
* a))
* (c
to_power (2
* c)))
* (b
to_power (2
* b)))
/ (((a
to_power (b
+ c))
* (c
to_power (a
+ b)))
* (b
to_power (a
+ c))))
> 1 by
XCMPLX_1: 76;
then ((d
/ e)
* e)
> (1
* e) by
A11,
A4,
A8,
XREAL_1: 68;
hence thesis by
A11,
A4,
A8,
XCMPLX_1: 87;
end;
theorem ::
SERIES_5:43
n
>= 1 implies ((a
|^ (n
+ 1))
+ (b
|^ (n
+ 1)))
>= (((a
|^ n)
* b)
+ (a
* (b
|^ n)))
proof
assume
A1: n
>= 1;
per cases ;
suppose
A2: (a
- b)
>
0 ;
then ((a
- b)
+ b)
> (
0
+ b) by
XREAL_1: 8;
then (a
|^ n)
> (b
|^ n) by
A1,
PREPOWER: 10;
then ((a
|^ n)
- (b
|^ n))
>
0 by
XREAL_1: 50;
then ((a
- b)
* ((a
|^ n)
- (b
|^ n)))
>
0 by
A2;
then ((((a
* (a
|^ n))
- (a
* (b
|^ n)))
- (b
* (a
|^ n)))
+ (b
* (b
|^ n)))
>
0 ;
then ((((a
|^ (n
+ 1))
- (a
* (b
|^ n)))
- (b
* (a
|^ n)))
+ (b
* (b
|^ n)))
>
0 by
NEWTON: 6;
then ((((a
|^ (n
+ 1))
- (a
* (b
|^ n)))
- (b
* (a
|^ n)))
+ (b
|^ (n
+ 1)))
>
0 by
NEWTON: 6;
then (((((a
|^ (n
+ 1))
+ (b
|^ (n
+ 1)))
- (a
* (b
|^ n)))
- (b
* (a
|^ n)))
+ ((a
* (b
|^ n))
+ (b
* (a
|^ n))))
> (
0
+ ((a
* (b
|^ n))
+ (b
* (a
|^ n)))) by
XREAL_1: 8;
hence thesis;
end;
suppose
A3: (a
- b)
=
0 ;
then (((a
|^ n)
* b)
+ (a
* (b
|^ n)))
= ((a
|^ (n
+ 1))
+ ((a
|^ n)
* a)) by
NEWTON: 6
.= ((a
|^ (n
+ 1))
+ (a
|^ (n
+ 1))) by
NEWTON: 6
.= (2
* (a
|^ (n
+ 1)));
hence thesis by
A3;
end;
suppose
A4: (a
- b)
<
0 ;
then ((a
- b)
+ b)
< (
0
+ b) by
XREAL_1: 8;
then (a
|^ n)
< (b
|^ n) by
A1,
PREPOWER: 10;
then ((a
|^ n)
- (b
|^ n))
<
0 by
XREAL_1: 49;
then ((a
- b)
* ((a
|^ n)
- (b
|^ n)))
>
0 by
A4;
then ((((a
* (a
|^ n))
- (a
* (b
|^ n)))
- (b
* (a
|^ n)))
+ (b
* (b
|^ n)))
>
0 ;
then ((((a
|^ (n
+ 1))
- (a
* (b
|^ n)))
- (b
* (a
|^ n)))
+ (b
* (b
|^ n)))
>
0 by
NEWTON: 6;
then ((((a
|^ (n
+ 1))
- (a
* (b
|^ n)))
- (b
* (a
|^ n)))
+ (b
|^ (n
+ 1)))
>
0 by
NEWTON: 6;
then (((((a
|^ (n
+ 1))
+ (b
|^ (n
+ 1)))
- (a
* (b
|^ n)))
- (b
* (a
|^ n)))
+ ((a
* (b
|^ n))
+ (b
* (a
|^ n))))
> (
0
+ ((a
* (b
|^ n))
+ (b
* (a
|^ n)))) by
XREAL_1: 8;
hence thesis;
end;
end;
theorem ::
SERIES_5:44
((a
^2 )
+ (b
^2 ))
= (c
^2 ) & n
>= 3 implies ((a
|^ (n
+ 2))
+ (b
|^ (n
+ 2)))
< (c
|^ (n
+ 2))
proof
assume that
A1: ((a
^2 )
+ (b
^2 ))
= (c
^2 ) and
A2: n
>= 3;
A3: n
>= 1 by
A2,
XXREAL_0: 2;
(b
^2 )
>
0 ;
then
A4: (b
|^ 2)
>
0 by
NEWTON: 81;
(((c
^2 )
- (b
^2 ))
+ (b
^2 ))
> (
0
+ (b
^2 )) by
A1,
XREAL_1: 8;
then (
sqrt (c
^2 ))
> (
sqrt (b
^2 )) by
SQUARE_1: 27;
then c
> (
sqrt (b
^2 )) by
SQUARE_1: 22;
then c
> b by
SQUARE_1: 22;
then (c
|^ n)
> (b
|^ n) by
A3,
PREPOWER: 10;
then ((c
|^ n)
* (b
|^ 2))
> ((b
|^ n)
* (b
|^ 2)) by
A4,
XREAL_1: 68;
then
A5: ((c
|^ n)
* (b
|^ 2))
> (b
|^ (n
+ 2)) by
NEWTON: 8;
(a
^2 )
>
0 ;
then
A6: (a
|^ 2)
>
0 by
NEWTON: 81;
(((c
^2 )
- (a
^2 ))
+ (a
^2 ))
> (
0
+ (a
^2 )) by
A1,
XREAL_1: 8;
then (
sqrt (c
^2 ))
> (
sqrt (a
^2 )) by
SQUARE_1: 27;
then c
> (
sqrt (a
^2 )) by
SQUARE_1: 22;
then c
> a by
SQUARE_1: 22;
then (c
|^ n)
> (a
|^ n) by
A3,
PREPOWER: 10;
then ((c
|^ n)
* (a
|^ 2))
> ((a
|^ n)
* (a
|^ 2)) by
A6,
XREAL_1: 68;
then ((c
|^ n)
* (a
|^ 2))
> (a
|^ (n
+ 2)) by
NEWTON: 8;
then (((c
|^ n)
* (a
|^ 2))
+ ((c
|^ n)
* (b
|^ 2)))
> ((a
|^ (n
+ 2))
+ (b
|^ (n
+ 2))) by
A5,
XREAL_1: 8;
then ((c
|^ n)
* ((a
|^ 2)
+ (b
|^ 2)))
> ((a
|^ (n
+ 2))
+ (b
|^ (n
+ 2)));
then ((c
|^ n)
* ((a
^2 )
+ (b
|^ 2)))
> ((a
|^ (n
+ 2))
+ (b
|^ (n
+ 2))) by
NEWTON: 81;
then ((c
|^ n)
* (c
^2 ))
> ((a
|^ (n
+ 2))
+ (b
|^ (n
+ 2))) by
A1,
NEWTON: 81;
then ((c
|^ n)
* (c
|^ 2))
> ((a
|^ (n
+ 2))
+ (b
|^ (n
+ 2))) by
NEWTON: 81;
hence thesis by
NEWTON: 8;
end;
theorem ::
SERIES_5:45
n
>= 1 implies ((1
+ (1
/ (n
+ 1)))
|^ n)
< ((1
+ (1
/ n))
|^ (n
+ 1))
proof
assume
A1: n
>= 1;
(n
+ 1)
> (n
+
0 ) by
XREAL_1: 8;
then (1
/ (n
+ 1))
< (1
/ n) by
A1,
XREAL_1: 76;
then ((1
/ (n
+ 1))
+ 1)
< ((1
/ n)
+ 1) by
XREAL_1: 8;
then
A2: ((1
+ (1
/ (n
+ 1)))
|^ n)
< ((1
+ (1
/ n))
|^ n) by
A1,
PREPOWER: 10;
A3: ((1
+ (1
/ n))
|^ n)
>
0 by
PREPOWER: 6;
(((1
+ (1
/ n))
|^ (n
+ 1))
- ((1
+ (1
/ n))
|^ n))
= ((((1
+ (1
/ n))
|^ n)
* (1
+ (1
/ n)))
- ((1
+ (1
/ n))
|^ n)) by
NEWTON: 6
.= (((1
+ (1
/ n))
|^ n)
* (1
/ n));
then ((((1
+ (1
/ n))
|^ (n
+ 1))
- ((1
+ (1
/ n))
|^ n))
+ ((1
+ (1
/ n))
|^ n))
> (
0
+ ((1
+ (1
/ n))
|^ n)) by
A1,
A3,
XREAL_1: 8;
hence thesis by
A2,
XXREAL_0: 2;
end;
theorem ::
SERIES_5:46
n
>= 1 & k
>= 1 implies (((a
|^ k)
+ (b
|^ k))
* ((a
|^ n)
+ (b
|^ n)))
<= (2
* ((a
|^ (k
+ n))
+ (b
|^ (k
+ n))))
proof
assume that
A1: n
>= 1 and
A2: k
>= 1;
A3: ((((a
|^ k)
+ (b
|^ k))
* ((a
|^ n)
+ (b
|^ n)))
- (2
* ((a
|^ (k
+ n))
+ (b
|^ (k
+ n)))))
= (((((((a
|^ k)
* (a
|^ n))
+ ((a
|^ k)
* (b
|^ n)))
+ ((b
|^ k)
* (a
|^ n)))
+ ((b
|^ k)
* (b
|^ n)))
- (2
* (a
|^ (k
+ n))))
- (2
* (b
|^ (k
+ n))))
.= ((((((a
|^ (k
+ n))
+ ((a
|^ k)
* (b
|^ n)))
+ ((b
|^ k)
* (a
|^ n)))
+ ((b
|^ k)
* (b
|^ n)))
- (2
* (a
|^ (k
+ n))))
- (2
* (b
|^ (k
+ n)))) by
NEWTON: 8
.= ((((((a
|^ (k
+ n))
+ ((a
|^ k)
* (b
|^ n)))
+ ((b
|^ k)
* (a
|^ n)))
+ (b
|^ (k
+ n)))
- (2
* (a
|^ (k
+ n))))
- (2
* (b
|^ (k
+ n)))) by
NEWTON: 8
.= (((((a
|^ k)
* (b
|^ n))
+ ((b
|^ k)
* (a
|^ n)))
- (a
|^ (k
+ n)))
- (b
|^ (k
+ n)))
.= (((((a
|^ k)
* (b
|^ n))
+ ((b
|^ k)
* (a
|^ n)))
- ((a
|^ k)
* (a
|^ n)))
- (b
|^ (k
+ n))) by
NEWTON: 8
.= (((((a
|^ k)
* (b
|^ n))
+ ((b
|^ k)
* (a
|^ n)))
- ((a
|^ k)
* (a
|^ n)))
- ((b
|^ k)
* (b
|^ n))) by
NEWTON: 8
.= (((a
|^ n)
- (b
|^ n))
* ((b
|^ k)
- (a
|^ k)));
per cases ;
suppose (a
- b)
>
0 ;
then
A4: ((a
- b)
+ b)
> (
0
+ b) by
XREAL_1: 8;
then (a
|^ k)
> (b
|^ k) by
A2,
PREPOWER: 10;
then
A5: ((b
|^ k)
- (a
|^ k))
<
0 by
XREAL_1: 49;
(a
|^ n)
> (b
|^ n) by
A1,
A4,
PREPOWER: 10;
then ((a
|^ n)
- (b
|^ n))
>
0 by
XREAL_1: 50;
hence thesis by
A3,
A5,
XREAL_1: 48;
end;
suppose (a
- b)
=
0 ;
then (a
|^ n)
= (b
|^ n);
hence thesis by
A3;
end;
suppose (a
- b)
<
0 ;
then
A6: ((a
- b)
+ b)
< (
0
+ b) by
XREAL_1: 8;
then (a
|^ k)
< (b
|^ k) by
A2,
PREPOWER: 10;
then
A7: ((b
|^ k)
- (a
|^ k))
>
0 by
XREAL_1: 50;
(a
|^ n)
< (b
|^ n) by
A1,
A6,
PREPOWER: 10;
then ((a
|^ n)
- (b
|^ n))
<
0 by
XREAL_1: 49;
hence thesis by
A3,
A7,
XREAL_1: 48;
end;
end;
theorem ::
SERIES_5:47
(for n holds (s
. n)
= (1
/ (
sqrt (n
+ 1)))) implies for n holds ((
Partial_Sums s)
. n)
< (2
* (
sqrt (n
+ 1)))
proof
defpred
X[
Nat] means ((
Partial_Sums s)
. $1)
< (2
* (
sqrt ($1
+ 1)));
assume
A1: for n holds (s
. n)
= (1
/ (
sqrt (n
+ 1)));
A2: for n st
X[n] holds
X[(n
+ 1)]
proof
let n;
A3: (
sqrt (n
+ 2))
>
0 by
SQUARE_1: 25;
(((4
* (n
^2 ))
+ (12
* n))
+ 8)
< (((4
* (n
^2 ))
+ (12
* n))
+ 9) by
XREAL_1: 8;
then (
sqrt (4
* ((n
+ 2)
* (n
+ 1))))
< (
sqrt (((2
* n)
+ 3)
^2 )) by
SQUARE_1: 27;
then (2
* (
sqrt ((n
+ 2)
* (n
+ 1))))
< (
sqrt (((2
* n)
+ 3)
^2 )) by
SQUARE_1: 20,
SQUARE_1: 29;
then (2
* (
sqrt ((n
+ 2)
* (n
+ 1))))
< ((2
* n)
+ 3) by
SQUARE_1: 22;
then ((2
* (
sqrt ((n
+ 2)
* (n
+ 1))))
+ 1)
< (((2
* n)
+ 3)
+ 1) by
XREAL_1: 8;
then ((2
* ((
sqrt (n
+ 2))
* (
sqrt (n
+ 1))))
+ 1)
< (2
* (n
+ 2)) by
SQUARE_1: 29;
then ((2
* ((
sqrt (n
+ 2))
* (
sqrt (n
+ 1))))
+ 1)
< (2
* (
sqrt ((n
+ 2)
^2 ))) by
SQUARE_1: 22;
then (((2
* ((
sqrt (n
+ 2))
* (
sqrt (n
+ 1))))
+ 1)
/ (
sqrt (n
+ 2)))
< ((2
* (
sqrt ((n
+ 2)
* (n
+ 2))))
/ (
sqrt (n
+ 2))) by
A3,
XREAL_1: 74;
then (((2
* ((
sqrt (n
+ 2))
* (
sqrt (n
+ 1))))
+ 1)
/ (
sqrt (n
+ 2)))
< ((2
* ((
sqrt (n
+ 2))
* (
sqrt (n
+ 2))))
/ (
sqrt (n
+ 2))) by
SQUARE_1: 29;
then (((2
* ((
sqrt (n
+ 2))
* (
sqrt (n
+ 1))))
+ 1)
/ (
sqrt (n
+ 2)))
< (((2
* (
sqrt (n
+ 2)))
* (
sqrt (n
+ 2)))
/ (
sqrt (n
+ 2)));
then (((2
* ((
sqrt (n
+ 2))
* (
sqrt (n
+ 1))))
+ 1)
/ (
sqrt (n
+ 2)))
< (2
* (
sqrt (n
+ 2))) by
A3,
XCMPLX_1: 89;
then ((((2
* (
sqrt (n
+ 1)))
* (
sqrt (n
+ 2)))
/ (
sqrt (n
+ 2)))
+ (1
/ (
sqrt (n
+ 2))))
< (2
* (
sqrt (n
+ 2))) by
XCMPLX_1: 62;
then
A4: ((2
* (
sqrt (n
+ 1)))
+ (1
/ (
sqrt (n
+ 2))))
< (2
* (
sqrt (n
+ 2))) by
A3,
XCMPLX_1: 89;
assume ((
Partial_Sums s)
. n)
< (2
* (
sqrt (n
+ 1)));
then (((
Partial_Sums s)
. n)
+ (1
/ (
sqrt (n
+ 2))))
< ((2
* (
sqrt (n
+ 1)))
+ (1
/ (
sqrt (n
+ 2)))) by
XREAL_1: 8;
then (((
Partial_Sums s)
. n)
+ (1
/ (
sqrt ((n
+ 1)
+ 1))))
< (2
* (
sqrt (n
+ 2))) by
A4,
XXREAL_0: 2;
then (((
Partial_Sums s)
. n)
+ (s
. (n
+ 1)))
< (2
* (
sqrt (n
+ 2))) by
A1;
hence thesis by
SERIES_1:def 1;
end;
((
Partial_Sums s)
.
0 )
= (s
.
0 ) by
SERIES_1:def 1
.= (1
/ (
sqrt (
0
+ 1))) by
A1
.= 1 by
SQUARE_1: 18;
then
A5:
X[
0 ] by
SQUARE_1: 18;
for n holds
X[n] from
NAT_1:sch 2(
A5,
A2);
hence thesis;
end;
theorem ::
SERIES_5:48
Th48: (for n holds (s
. n)
= (1
/ ((n
+ 1)
^2 ))) implies for n holds ((
Partial_Sums s)
. n)
<= (2
- (1
/ (n
+ 1)))
proof
defpred
X[
Nat] means ((
Partial_Sums s)
. $1)
<= (2
- (1
/ ($1
+ 1)));
assume
A1: for n holds (s
. n)
= (1
/ ((n
+ 1)
^2 ));
A2: for n st
X[n] holds
X[(n
+ 1)]
proof
let n;
assume ((
Partial_Sums s)
. n)
<= (2
- (1
/ (n
+ 1)));
then
A3: (((
Partial_Sums s)
. n)
+ (1
/ ((n
+ 2)
^2 )))
<= ((2
- (1
/ (n
+ 1)))
+ (1
/ ((n
+ 2)
^2 ))) by
XREAL_1: 7;
(((n
^2 )
+ (3
* n))
+ 3)
> (((n
^2 )
+ (3
* n))
+ 2) by
XREAL_1: 8;
then ((((n
^2 )
+ (3
* n))
+ 3)
/ ((n
+ 1)
* ((n
+ 2)
^2 )))
> (((n
+ 2)
* (n
+ 1))
/ (((n
+ 2)
^2 )
* (n
+ 1))) by
XREAL_1: 74;
then ((((n
^2 )
+ (3
* n))
+ 3)
/ ((n
+ 1)
* ((n
+ 2)
^2 )))
> ((n
+ 2)
/ ((n
+ 2)
* (n
+ 2))) by
XCMPLX_1: 91;
then ((((n
^2 )
+ (3
* n))
+ 3)
/ ((n
+ 1)
* ((n
+ 2)
^2 )))
> (((n
+ 2)
/ (n
+ 2))
/ (n
+ 2)) by
XCMPLX_1: 78;
then ((((n
^2 )
+ (3
* n))
+ 3)
/ ((n
+ 1)
* ((n
+ 2)
^2 )))
> (1
/ (n
+ 2)) by
XCMPLX_1: 60;
then ((
- 1)
* ((((n
^2 )
+ (3
* n))
+ 3)
/ ((n
+ 1)
* ((n
+ 2)
^2 ))))
< ((
- 1)
* (1
/ (n
+ 2))) by
XREAL_1: 69;
then
A4: ((
- ((((n
^2 )
+ (3
* n))
+ 3)
/ ((n
+ 1)
* ((n
+ 2)
^2 ))))
+ 2)
< ((
- (1
/ (n
+ 2)))
+ 2) by
XREAL_1: 8;
((
Partial_Sums s)
. (n
+ 1))
= (((
Partial_Sums s)
. n)
+ (s
. (n
+ 1))) by
SERIES_1:def 1
.= (((
Partial_Sums s)
. n)
+ (1
/ (((n
+ 1)
+ 1)
^2 ))) by
A1;
then ((
Partial_Sums s)
. (n
+ 1))
<= (2
- ((1
/ (n
+ 1))
- (1
/ ((n
+ 2)
^2 )))) by
A3;
then ((
Partial_Sums s)
. (n
+ 1))
<= (2
- (((1
* ((n
+ 2)
^2 ))
- (1
* (n
+ 1)))
/ ((n
+ 1)
* ((n
+ 2)
^2 )))) by
XCMPLX_1: 130;
hence thesis by
A4,
XXREAL_0: 2;
end;
((
Partial_Sums s)
.
0 )
= (s
.
0 ) by
SERIES_1:def 1
.= (1
/ ((
0
+ 1)
^2 )) by
A1
.= 1;
then
A5:
X[
0 ];
for n holds
X[n] from
NAT_1:sch 2(
A5,
A2);
hence thesis;
end;
theorem ::
SERIES_5:49
(for n holds (s
. n)
= (1
/ ((n
+ 1)
^2 ))) implies ((
Partial_Sums s)
. n)
< 2
proof
assume for n holds (s
. n)
= (1
/ ((n
+ 1)
^2 ));
then
A1: ((
Partial_Sums s)
. n)
<= (2
- (1
/ (n
+ 1))) by
Th48;
((
- (1
/ (n
+ 1)))
+ 2)
< (
0
+ 2) by
XREAL_1: 8;
hence thesis by
A1,
XXREAL_0: 2;
end;
theorem ::
SERIES_5:50
Th50: (for n holds (s
. n)
< 1) implies for n holds ((
Partial_Sums s)
. n)
< (n
+ 1)
proof
defpred
X[
Nat] means ((
Partial_Sums s)
. $1)
< ($1
+ 1);
assume
A1: for n holds (s
. n)
< 1;
A2: for n st
X[n] holds
X[(n
+ 1)]
proof
let n;
A3: ((
Partial_Sums s)
. (n
+ 1))
= (((
Partial_Sums s)
. n)
+ (s
. (n
+ 1))) by
SERIES_1:def 1;
assume ((
Partial_Sums s)
. n)
< (n
+ 1);
hence thesis by
A1,
A3,
XREAL_1: 8;
end;
((
Partial_Sums s)
.
0 )
= (s
.
0 ) by
SERIES_1:def 1;
then
A4:
X[
0 ] by
A1;
for n holds
X[n] from
NAT_1:sch 2(
A4,
A2);
hence thesis;
end;
theorem ::
SERIES_5:51
(for n holds (s
. n)
>
0 & (s
. n)
< 1) implies for n holds ((
Partial_Product s)
. n)
>= (((
Partial_Sums s)
. n)
- n)
proof
defpred
X[
Nat] means ((
Partial_Product s)
. $1)
>= (((
Partial_Sums s)
. $1)
- $1);
assume
A1: for n holds (s
. n)
>
0 & (s
. n)
< 1;
A2: for n st
X[n] holds
X[(n
+ 1)]
proof
let n;
assume
A3: ((
Partial_Product s)
. n)
>= (((
Partial_Sums s)
. n)
- n);
A4: (s
. (n
+ 1))
< 1 by
A1;
(((
Partial_Sums s)
. n)
- (n
+ 1))
<
0 by
A1,
Th50,
XREAL_1: 49;
then ((s
. (n
+ 1))
* ((((
Partial_Sums s)
. n)
- n)
- 1))
> (1
* ((((
Partial_Sums s)
. n)
- n)
- 1)) by
A4,
XREAL_1: 69;
then
A5: (((((s
. (n
+ 1))
* ((
Partial_Sums s)
. n))
- ((s
. (n
+ 1))
* n))
- (s
. (n
+ 1)))
+ (s
. (n
+ 1)))
> (((((
Partial_Sums s)
. n)
- n)
- 1)
+ (s
. (n
+ 1))) by
XREAL_1: 8;
(s
. (n
+ 1))
>
0 by
A1;
then (((
Partial_Product s)
. n)
* (s
. (n
+ 1)))
>= ((((
Partial_Sums s)
. n)
- n)
* (s
. (n
+ 1))) by
A3,
XREAL_1: 64;
then (((
Partial_Product s)
. n)
* (s
. (n
+ 1)))
> ((((
Partial_Sums s)
. n)
+ (s
. (n
+ 1)))
- (n
+ 1)) by
A5,
XXREAL_0: 2;
then ((
Partial_Product s)
. (n
+ 1))
> ((((
Partial_Sums s)
. n)
+ (s
. (n
+ 1)))
- (n
+ 1)) by
SERIES_3:def 1;
hence thesis by
SERIES_1:def 1;
end;
(((
Partial_Sums s)
.
0 )
-
0 )
= (s
.
0 ) by
SERIES_1:def 1;
then
A6:
X[
0 ] by
SERIES_3:def 1;
for n holds
X[n] from
NAT_1:sch 2(
A6,
A2);
hence thesis;
end;
theorem ::
SERIES_5:52
Th52: (for n be
Nat holds (s
. n)
>
0 & (s1
. n)
= (1
/ (s
. n))) implies for n holds ((
Partial_Sums s1)
. n)
>
0
proof
defpred
X[
Nat] means ((
Partial_Sums s1)
. $1)
>
0 ;
assume
A1: for n be
Nat holds (s
. n)
>
0 & (s1
. n)
= (1
/ (s
. n));
then
A2: (s1
.
0 )
= (1
/ (s
.
0 ));
A3: for n st
X[n] holds
X[(n
+ 1)]
proof
let n;
assume
A4: ((
Partial_Sums s1)
. n)
>
0 ;
A5: ((
Partial_Sums s1)
. (n
+ 1))
= (((
Partial_Sums s1)
. n)
+ (s1
. (n
+ 1))) by
SERIES_1:def 1;
A6: (s
. (n
+ 1))
>
0 by
A1;
(s1
. (n
+ 1))
= (1
/ (s
. (n
+ 1))) by
A1;
hence thesis by
A4,
A5,
A6;
end;
(s
.
0 )
>
0 by
A1;
then
A7:
X[
0 ] by
A2,
SERIES_1:def 1;
for n holds
X[n] from
NAT_1:sch 2(
A7,
A3);
hence thesis;
end;
theorem ::
SERIES_5:53
(for n be
Nat holds (s
. n)
>
0 & (s1
. n)
= (1
/ (s
. n))) implies for n holds (((
Partial_Sums s)
. n)
* ((
Partial_Sums s1)
. n))
>= ((n
+ 1)
^2 )
proof
defpred
X[
Nat] means (((
Partial_Sums s)
. $1)
* ((
Partial_Sums s1)
. $1))
>= (($1
+ 1)
^2 );
assume
A1: for n be
Nat holds (s
. n)
>
0 & (s1
. n)
= (1
/ (s
. n));
then
A2: (s
.
0 )
>
0 ;
A3: for n st
X[n] holds
X[(n
+ 1)]
proof
let n;
set x = ((
Partial_Sums s)
. n);
set y = ((
Partial_Sums s1)
. n);
assume
A4: (((
Partial_Sums s)
. n)
* ((
Partial_Sums s1)
. n))
>= ((n
+ 1)
^2 );
then
A5: ((x
* y)
+ (((x
/ (s
. (n
+ 1)))
+ (y
* (s
. (n
+ 1))))
+ 1))
>= (((n
+ 1)
^2 )
+ (((x
/ (s
. (n
+ 1)))
+ (y
* (s
. (n
+ 1))))
+ 1)) by
XREAL_1: 7;
(
sqrt (x
* y))
>= (
sqrt ((n
+ 1)
^2 )) by
A4,
SQUARE_1: 26;
then (
sqrt (x
* y))
>= (n
+ 1) by
SQUARE_1: 22;
then
A6: (2
* (
sqrt (x
* y)))
>= (2
* (n
+ 1)) by
XREAL_1: 64;
A7: (s
. (n
+ 1))
>
0 by
A1;
A8: x
>
0 by
A1,
SERIES_3: 33;
y
>
0 by
A1,
Th52;
then ((x
/ (s
. (n
+ 1)))
+ (y
* (s
. (n
+ 1))))
>= (2
* (
sqrt ((y
* (s
. (n
+ 1)))
* (x
/ (s
. (n
+ 1)))))) by
A7,
A8,
SIN_COS2: 1;
then ((x
/ (s
. (n
+ 1)))
+ (y
* (s
. (n
+ 1))))
>= (2
* (
sqrt (x
/ ((1
* (s
. (n
+ 1)))
/ (y
* (s
. (n
+ 1))))))) by
XCMPLX_1: 81;
then ((x
/ (s
. (n
+ 1)))
+ (y
* (s
. (n
+ 1))))
>= (2
* (
sqrt (x
/ (1
/ y)))) by
A7,
XCMPLX_1: 91;
then ((x
/ (s
. (n
+ 1)))
+ (y
* (s
. (n
+ 1))))
>= (2
* (
sqrt (y
* (x
/ 1)))) by
XCMPLX_1: 81;
then ((x
/ (s
. (n
+ 1)))
+ (y
* (s
. (n
+ 1))))
>= ((2
* n)
+ 2) by
A6,
XXREAL_0: 2;
then
A9: (((x
/ (s
. (n
+ 1)))
+ (y
* (s
. (n
+ 1))))
+ (((n
^2 )
+ (2
* n))
+ 2))
>= (((2
* n)
+ 2)
+ (((n
^2 )
+ (2
* n))
+ 2)) by
XREAL_1: 7;
(((
Partial_Sums s)
. (n
+ 1))
* ((
Partial_Sums s1)
. (n
+ 1)))
= ((x
+ (s
. (n
+ 1)))
* ((
Partial_Sums s1)
. (n
+ 1))) by
SERIES_1:def 1
.= ((x
+ (s
. (n
+ 1)))
* (y
+ (s1
. (n
+ 1)))) by
SERIES_1:def 1
.= ((((x
* y)
+ (x
* (s1
. (n
+ 1))))
+ ((s
. (n
+ 1))
* y))
+ ((s
. (n
+ 1))
* (s1
. (n
+ 1))))
.= ((((x
* y)
+ (x
* (1
/ (s
. (n
+ 1)))))
+ ((s
. (n
+ 1))
* y))
+ ((s
. (n
+ 1))
* (s1
. (n
+ 1)))) by
A1
.= ((((x
* y)
+ (x
* (1
/ (s
. (n
+ 1)))))
+ ((s
. (n
+ 1))
* y))
+ ((s
. (n
+ 1))
* (1
/ (s
. (n
+ 1))))) by
A1
.= ((((x
* y)
+ (x
* (1
/ (s
. (n
+ 1)))))
+ ((s
. (n
+ 1))
* y))
+ (((s
. (n
+ 1))
* 1)
/ (s
. (n
+ 1)))) by
XCMPLX_1: 74
.= ((((x
* y)
+ (x
* (1
/ (s
. (n
+ 1)))))
+ ((s
. (n
+ 1))
* y))
+ 1) by
A7,
XCMPLX_1: 60
.= ((((x
* y)
+ (x
/ ((s
. (n
+ 1))
/ 1)))
+ ((s
. (n
+ 1))
* y))
+ 1) by
XCMPLX_1: 79
.= ((((x
* y)
+ (x
/ (s
. (n
+ 1))))
+ ((s
. (n
+ 1))
* y))
+ 1);
hence thesis by
A9,
A5,
XXREAL_0: 2;
end;
(((
Partial_Sums s)
.
0 )
* ((
Partial_Sums s1)
.
0 ))
= ((s
.
0 )
* ((
Partial_Sums s1)
.
0 )) by
SERIES_1:def 1
.= ((s
.
0 )
* (s1
.
0 )) by
SERIES_1:def 1
.= ((s
.
0 )
* (1
/ (s
.
0 ))) by
A1
.= ((s
.
0 )
/ ((s
.
0 )
/ 1)) by
XCMPLX_1: 79
.= 1 by
A2,
XCMPLX_1: 60;
then
A10:
X[
0 ];
for n holds
X[n] from
NAT_1:sch 2(
A10,
A3);
hence thesis;
end;
theorem ::
SERIES_5:54
(for n st n
>= 1 holds (s
. n)
= (
sqrt n) & (s
.
0 )
=
0 ) implies for n st n
>= 1 holds ((
Partial_Sums s)
. n)
< (((1
/ 6)
* ((4
* n)
+ 3))
* (
sqrt n))
proof
defpred
X[
Nat] means ((
Partial_Sums s)
. $1)
< (((1
/ 6)
* ((4
* $1)
+ 3))
* (
sqrt $1));
assume
A1: for n st n
>= 1 holds (s
. n)
= (
sqrt n) & (s
.
0 )
=
0 ;
A2: for n be
Nat st n
>= 1 &
X[n] holds
X[(n
+ 1)]
proof
let n be
Nat;
assume that
A3: n
>= 1 and
A4: ((
Partial_Sums s)
. n)
< (((1
/ 6)
* ((4
* n)
+ 3))
* (
sqrt n));
(n
+ 1)
>= (1
+ 1) by
A3,
XREAL_1: 7;
then (n
+ 1)
>= 1 by
XXREAL_0: 2;
then
A5: (s
. (n
+ 1))
= (
sqrt (n
+ 1)) by
A1;
(
0
+ ((16
* (n
^2 ))
+ (8
* n)))
< (1
+ ((16
* (n
^2 ))
+ (8
* n))) by
XREAL_1: 8;
then (((16
* n)
+ 8)
* n)
< (1
* (((16
* (n
^2 ))
+ (8
* n))
+ 1));
then (((4
* ((4
* n)
+ 1))
+ 4)
/ (((4
* n)
+ 1)
^2 ))
< (1
/ n) by
A3,
XREAL_1: 106;
then (((4
* ((4
* n)
+ 1))
/ (((4
* n)
+ 1)
* ((4
* n)
+ 1)))
+ (4
/ (((4
* n)
+ 1)
^2 )))
< (1
/ n) by
XCMPLX_1: 62;
then ((4
/ ((4
* n)
+ 1))
+ (4
/ (((4
* n)
+ 1)
^2 )))
< (1
/ n) by
XCMPLX_1: 91;
then (1
+ ((4
/ ((4
* n)
+ 1))
+ (4
/ (((4
* n)
+ 1)
^2 ))))
< (1
+ (1
/ n)) by
XREAL_1: 8;
then ((1
+ (4
/ ((4
* n)
+ 1)))
+ (4
/ (((4
* n)
+ 1)
^2 )))
< (1
+ (1
/ n));
then ((1
+ ((2
* 2)
/ ((4
* n)
+ 1)))
+ ((2
/ ((4
* n)
+ 1))
^2 ))
< (1
+ (1
/ n)) by
XCMPLX_1: 76;
then ((1
+ (2
* (2
/ ((4
* n)
+ 1))))
+ ((2
/ ((4
* n)
+ 1))
^2 ))
< (1
+ (1
/ n)) by
XCMPLX_1: 74;
then (((2
/ ((4
* n)
+ 1))
+ 1)
^2 )
< ((1
+ (n
* 1))
/ n) by
A3,
XCMPLX_1: 113;
then (
sqrt (((2
/ ((4
* n)
+ 1))
+ 1)
^2 ))
< (
sqrt ((1
+ n)
/ n)) by
SQUARE_1: 27;
then ((2
/ ((4
* n)
+ 1))
+ 1)
< (
sqrt ((1
+ n)
/ n)) by
SQUARE_1: 22;
then ((2
+ (((4
* n)
+ 1)
* 1))
/ ((4
* n)
+ 1))
< (
sqrt ((1
+ n)
/ n)) by
XCMPLX_1: 113;
then
A6: (((4
* n)
+ 3)
/ ((4
* n)
+ 1))
< ((
sqrt (1
+ n))
/ (
sqrt n)) by
SQUARE_1: 30;
(
sqrt n)
>
0 by
A3,
SQUARE_1: 25;
then ((1
/ 6)
* (((4
* n)
+ 3)
* (
sqrt n)))
< ((1
/ 6)
* ((
sqrt (1
+ n))
* ((4
* n)
+ 1))) by
A6,
XREAL_1: 68,
XREAL_1: 102;
then ((
Partial_Sums s)
. n)
< ((((1
/ 6)
* (
sqrt (1
+ n)))
* ((4
* n)
+ 7))
- (
sqrt (1
+ n))) by
A4,
XXREAL_0: 2;
then
A7: (((
Partial_Sums s)
. n)
+ (
sqrt (1
+ n)))
< (((((1
/ 6)
* (
sqrt (1
+ n)))
* ((4
* n)
+ 7))
- (
sqrt (1
+ n)))
+ (
sqrt (1
+ n))) by
XREAL_1: 8;
thus thesis by
A5,
A7,
SERIES_1:def 1;
end;
((
Partial_Sums s)
. (1
+
0 ))
= (((
Partial_Sums s)
.
0 )
+ (s
. (1
+
0 ))) by
SERIES_1:def 1
.= ((s
.
0 )
+ (s
. 1)) by
SERIES_1:def 1
.= (
0
+ (s
. 1)) by
A1
.= 1 by
A1,
SQUARE_1: 18;
then
A8:
X[1] by
SQUARE_1: 18;
for n be
Nat st n
>= 1 holds
X[n] from
NAT_1:sch 8(
A8,
A2);
hence thesis;
end;
theorem ::
SERIES_5:55
(for n st n
>= 1 holds (s
. n)
= (
sqrt n) & (s
.
0 )
=
0 ) implies for n st n
>= 1 holds ((
Partial_Sums s)
. n)
> (((2
/ 3)
* n)
* (
sqrt n))
proof
defpred
X[
Nat] means ((
Partial_Sums s)
. $1)
> (((2
/ 3)
* $1)
* (
sqrt $1));
assume
A1: for n st n
>= 1 holds (s
. n)
= (
sqrt n) & (s
.
0 )
=
0 ;
A2: for n be
Nat st n
>= 1 &
X[n] holds
X[(n
+ 1)]
proof
let n be
Nat;
assume that
A3: n
>= 1 and
A4: ((
Partial_Sums s)
. n)
> (((2
/ 3)
* n)
* (
sqrt n));
(2
* n)
>= (2
* 1) by
A3,
XREAL_1: 64;
then (2
* n)
> 1 by
XXREAL_0: 2;
then
A5: ((2
* n)
- 1)
>
0 by
XREAL_1: 50;
(3
* n)
>= (3
* 1) by
A3,
XREAL_1: 64;
then (3
* n)
> 1 by
XXREAL_0: 2;
then (1
- (3
* n))
<
0 by
XREAL_1: 49;
then (((1
+ (n
- (4
* n)))
+ ((4
* (n
^2 ))
- (4
* (n
^2 ))))
+ (4
* (n
|^ 3)))
< (
0
+ (4
* (n
|^ 3))) by
XREAL_1: 8;
then ((((4
* (n
|^ (2
+ 1)))
- (4
* (n
^2 )))
+ n)
+ (((4
* (n
^2 ))
- (4
* n))
+ 1))
< (4
* (n
|^ 3));
then ((((4
* ((n
|^ 2)
* n))
- (4
* (n
* n)))
+ n)
+ (((4
* (n
^2 ))
- (4
* n))
+ 1))
< (4
* (n
|^ 3)) by
NEWTON: 6;
then (((((4
* (n
|^ 2))
- (4
* n))
+ 1)
* n)
+ ((((4
* (n
^2 ))
- (4
* n))
+ 1)
* 1))
< (4
* (n
|^ 3));
then (((((4
* (n
^2 ))
- (4
* n))
+ 1)
* n)
+ ((((4
* (n
^2 ))
- (4
* n))
+ 1)
* 1))
< (4
* (n
|^ 3)) by
NEWTON: 81;
then ((((4
* (n
^2 ))
- (4
* n))
+ 1)
* (n
+ 1))
< (4
* (n
|^ (2
+ 1)));
then ((((4
* (n
^2 ))
- (4
* n))
+ 1)
* (n
+ 1))
< (4
* ((n
|^ 2)
* n)) by
NEWTON: 6;
then ((((4
* (n
^2 ))
- (4
* n))
+ 1)
* (n
+ 1))
< ((4
* (n
|^ 2))
* n);
then ((((2
* n)
- 1)
^2 )
* (n
+ 1))
< ((4
* (n
^2 ))
* n) by
NEWTON: 81;
then ((n
+ 1)
/ n)
< (((2
* n)
^2 )
/ (((2
* n)
- 1)
^2 )) by
A3,
A5,
XREAL_1: 106;
then ((n
+ 1)
/ n)
< (((2
* n)
/ ((2
* n)
- 1))
^2 ) by
XCMPLX_1: 76;
then (
sqrt ((n
+ 1)
/ n))
< (
sqrt (((2
* n)
/ ((2
* n)
- 1))
^2 )) by
SQUARE_1: 27;
then (
sqrt ((n
+ 1)
/ n))
< ((2
* n)
/ ((2
* n)
- 1)) by
A5,
SQUARE_1: 22;
then
A6: ((
sqrt (n
+ 1))
/ (
sqrt n))
< ((2
* n)
/ ((2
* n)
- 1)) by
SQUARE_1: 30;
(
sqrt n)
>
0 by
A3,
SQUARE_1: 25;
then ((1
/ 3)
* ((
sqrt (n
+ 1))
* ((2
* n)
- 1)))
< ((1
/ 3)
* ((2
* n)
* (
sqrt n))) by
A5,
A6,
XREAL_1: 68,
XREAL_1: 102;
then ((
Partial_Sums s)
. n)
> ((((2
/ 3)
* (n
+ 1))
* (
sqrt (n
+ 1)))
- (
sqrt (n
+ 1))) by
A4,
XXREAL_0: 2;
then
A7: (((
Partial_Sums s)
. n)
+ (
sqrt (n
+ 1)))
> (((((2
/ 3)
* (n
+ 1))
* (
sqrt (n
+ 1)))
- (
sqrt (n
+ 1)))
+ (
sqrt (n
+ 1))) by
XREAL_1: 8;
(n
+ 1)
>= (1
+ 1) by
A3,
XREAL_1: 7;
then (n
+ 1)
>= 1 by
XXREAL_0: 2;
then (((
Partial_Sums s)
. n)
+ (s
. (n
+ 1)))
> (((2
/ 3)
* (n
+ 1))
* (
sqrt (n
+ 1))) by
A1,
A7;
hence thesis by
SERIES_1:def 1;
end;
((
Partial_Sums s)
. (1
+
0 ))
= (((
Partial_Sums s)
.
0 )
+ (s
. (1
+
0 ))) by
SERIES_1:def 1
.= ((s
.
0 )
+ (s
. 1)) by
SERIES_1:def 1
.= (
0
+ (s
. 1)) by
A1
.= 1 by
A1,
SQUARE_1: 18;
then
A8:
X[1] by
SQUARE_1: 18;
for n be
Nat st n
>= 1 holds
X[n] from
NAT_1:sch 8(
A8,
A2);
hence thesis;
end;
theorem ::
SERIES_5:56
(for n st n
>= 1 holds (s
. n)
= (1
+ (1
/ ((2
* n)
+ 1))) & (s
.
0 )
= 1) implies for n st n
>= 1 holds ((
Partial_Product s)
. n)
> ((1
/ 2)
* (
sqrt ((2
* n)
+ 3)))
proof
defpred
X[
Nat] means ((
Partial_Product s)
. $1)
> ((1
/ 2)
* (
sqrt ((2
* $1)
+ 3)));
A1: ((1
/ 2)
* (
sqrt ((2
* 1)
+ 3)))
= ((
sqrt 5)
/ 2);
assume
A2: for n st n
>= 1 holds (s
. n)
= (1
+ (1
/ ((2
* n)
+ 1))) & (s
.
0 )
= 1;
A3: for n be
Nat st n
>= 1 &
X[n] holds
X[(n
+ 1)]
proof
let n be
Nat;
assume that
A4: n
>= 1 and
A5: ((
Partial_Product s)
. n)
> ((1
/ 2)
* (
sqrt ((2
* n)
+ 3)));
(n
+ 1)
>= (1
+ 1) by
A4,
XREAL_1: 7;
then
A6: (n
+ 1)
>= 1 by
XXREAL_0: 2;
A7: (
sqrt ((2
* n)
+ 3))
>
0 by
SQUARE_1: 25;
((1
/ ((2
* n)
+ 3))
+ ((2
* n)
+ 5))
> (
0
+ ((2
* n)
+ 5)) by
XREAL_1: 8;
then (((1
/ ((2
* n)
+ 3))
+ 2)
+ ((2
* n)
+ 3))
> ((2
* n)
+ 5);
then ((((1
^2 )
/ ((
sqrt ((2
* n)
+ 3))
^2 ))
+ 2)
+ ((2
* n)
+ 3))
> ((2
* n)
+ 5) by
SQUARE_1:def 2;
then ((((1
/ (
sqrt ((2
* n)
+ 3)))
^2 )
+ 2)
+ ((2
* n)
+ 3))
> ((2
* n)
+ 5) by
XCMPLX_1: 76;
then ((((1
/ (
sqrt ((2
* n)
+ 3)))
^2 )
+ (2
* 1))
+ ((
sqrt ((2
* n)
+ 3))
^2 ))
> ((2
* n)
+ 5) by
SQUARE_1:def 2;
then ((((1
/ (
sqrt ((2
* n)
+ 3)))
^2 )
+ (2
* ((
sqrt ((2
* n)
+ 3))
* (1
/ (
sqrt ((2
* n)
+ 3))))))
+ ((
sqrt ((2
* n)
+ 3))
^2 ))
> ((2
* n)
+ 5) by
A7,
XCMPLX_1: 106;
then (
sqrt (((1
/ (
sqrt ((2
* n)
+ 3)))
+ (
sqrt ((2
* n)
+ 3)))
^2 ))
> (
sqrt ((2
* n)
+ 5)) by
SQUARE_1: 27;
then ((
sqrt ((2
* n)
+ 3))
+ (1
/ (
sqrt ((2
* n)
+ 3))))
> (
sqrt ((2
* n)
+ 5)) by
A7,
SQUARE_1: 22;
then
A8: ((1
/ 2)
* ((
sqrt ((2
* n)
+ 3))
+ (1
/ (
sqrt ((2
* n)
+ 3)))))
> ((1
/ 2)
* (
sqrt ((2
* n)
+ 5))) by
XREAL_1: 68;
(((
Partial_Product s)
. n)
* (1
+ (1
/ ((2
* n)
+ 3))))
> (((1
/ 2)
* (
sqrt ((2
* n)
+ 3)))
* (1
+ (1
/ ((2
* n)
+ 3)))) by
A5,
XREAL_1: 68;
then (((
Partial_Product s)
. n)
* (1
+ (1
/ ((2
* n)
+ 3))))
> ((((1
/ 2)
* (
sqrt ((2
* n)
+ 3)))
* 1)
+ (((1
/ 2)
* (
sqrt ((2
* n)
+ 3)))
* (1
/ ((2
* n)
+ 3))));
then (((
Partial_Product s)
. n)
* (1
+ (1
/ ((2
* n)
+ 3))))
> (((1
/ 2)
* (
sqrt ((2
* n)
+ 3)))
+ (((1
/ 2)
* (
sqrt ((2
* n)
+ 3)))
/ ((2
* n)
+ 3))) by
XCMPLX_1: 74;
then (((
Partial_Product s)
. n)
* (1
+ (1
/ ((2
* n)
+ 3))))
> (((1
/ 2)
* (
sqrt ((2
* n)
+ 3)))
+ ((1
/ 2)
* ((
sqrt ((2
* n)
+ 3))
/ ((2
* n)
+ 3)))) by
XCMPLX_1: 74;
then (((
Partial_Product s)
. n)
* (1
+ (1
/ ((2
* n)
+ 3))))
> (((1
/ 2)
* (
sqrt ((2
* n)
+ 3)))
+ ((1
/ 2)
* ((
sqrt ((2
* n)
+ 3))
/ (
sqrt (((2
* n)
+ 3)
^2 ))))) by
SQUARE_1: 22;
then (((
Partial_Product s)
. n)
* (1
+ (1
/ ((2
* n)
+ 3))))
> (((1
/ 2)
* (
sqrt ((2
* n)
+ 3)))
+ ((1
/ 2)
* (((
sqrt ((2
* n)
+ 3))
* 1)
/ ((
sqrt ((2
* n)
+ 3))
* (
sqrt ((2
* n)
+ 3)))))) by
SQUARE_1: 29;
then (((
Partial_Product s)
. n)
* (1
+ (1
/ ((2
* n)
+ 3))))
> (((1
/ 2)
* (
sqrt ((2
* n)
+ 3)))
+ ((1
/ 2)
* (((
sqrt ((2
* n)
+ 3))
/ (
sqrt ((2
* n)
+ 3)))
* (1
/ (
sqrt ((2
* n)
+ 3)))))) by
XCMPLX_1: 76;
then (((
Partial_Product s)
. n)
* (1
+ (1
/ ((2
* n)
+ 3))))
> (((1
/ 2)
* (
sqrt ((2
* n)
+ 3)))
+ ((1
/ 2)
* (1
* (1
/ (
sqrt ((2
* n)
+ 3)))))) by
A7,
XCMPLX_1: 60;
then (((
Partial_Product s)
. n)
* (1
+ (1
/ ((2
* (n
+ 1))
+ 1))))
> ((1
/ 2)
* (
sqrt ((2
* n)
+ 5))) by
A8,
XXREAL_0: 2;
then (((
Partial_Product s)
. n)
* (s
. (n
+ 1)))
> ((1
/ 2)
* (
sqrt ((2
* n)
+ 5))) by
A2,
A6;
hence thesis by
SERIES_3:def 1;
end;
(
sqrt (16
/ 9))
> (
sqrt (5
/ 4)) by
SQUARE_1: 27;
then ((
sqrt (4
^2 ))
/ (
sqrt (3
^2 )))
> (
sqrt (5
/ 4)) by
SQUARE_1: 30;
then (4
/ (
sqrt (3
^2 )))
> (
sqrt (5
/ 4)) by
SQUARE_1: 22;
then (4
/ 3)
> (
sqrt (5
/ 4)) by
SQUARE_1: 22;
then
A9: (4
/ 3)
> ((
sqrt 5)
/ (
sqrt (2
^2 ))) by
SQUARE_1: 30;
((
Partial_Product s)
. (1
+
0 ))
= (((
Partial_Product s)
.
0 )
* (s
. (1
+
0 ))) by
SERIES_3:def 1
.= ((s
.
0 )
* (s
. 1)) by
SERIES_3:def 1
.= (1
* (s
. 1)) by
A2
.= (1
+ (1
/ ((2
* 1)
+ 1))) by
A2
.= (4
/ 3);
then
A10:
X[1] by
A1,
A9,
SQUARE_1: 22;
for n be
Nat st n
>= 1 holds
X[n] from
NAT_1:sch 8(
A10,
A3);
hence thesis;
end;
theorem ::
SERIES_5:57
(for n st n
>= 1 holds (s
. n)
= (
sqrt (n
* (n
+ 1))) & (s
.
0 )
=
0 ) implies for n st n
>= 1 holds ((
Partial_Sums s)
. n)
> ((n
* (n
+ 1))
/ 2)
proof
defpred
X[
Nat] means ((
Partial_Sums s)
. $1)
> (($1
* ($1
+ 1))
/ 2);
assume
A1: for n st n
>= 1 holds (s
. n)
= (
sqrt (n
* (n
+ 1))) & (s
.
0 )
=
0 ;
A2: for n be
Nat st n
>= 1 &
X[n] holds
X[(n
+ 1)]
proof
let n be
Nat;
assume that
A3: n
>= 1 and
A4: ((
Partial_Sums s)
. n)
> ((n
* (n
+ 1))
/ 2);
(n
+ 1)
>= (1
+ 1) by
A3,
XREAL_1: 7;
then (n
+ 1)
>= 1 by
XXREAL_0: 2;
then
A5: (s
. (n
+ 1))
= (
sqrt ((n
+ 1)
* ((n
+ 1)
+ 1))) by
A1;
(n
+ 2)
> (n
+ 1) by
XREAL_1: 8;
then ((n
+ 2)
* (n
+ 1))
> ((n
+ 1)
^2 ) by
XREAL_1: 68;
then (
sqrt ((n
+ 2)
* (n
+ 1)))
> (
sqrt ((n
+ 1)
^2 )) by
SQUARE_1: 27;
then
A6: (
sqrt ((n
+ 2)
* (n
+ 1)))
> (n
+ 1) by
SQUARE_1: 22;
(((
Partial_Sums s)
. n)
+ ((
sqrt ((n
+ 1)
* (n
+ 2)))
- (((n
+ 1)
* (n
+ 2))
/ 2)))
> (((n
* (n
+ 1))
/ 2)
+ ((
sqrt ((n
+ 1)
* (n
+ 2)))
- (((n
+ 1)
* (n
+ 2))
/ 2))) by
A4,
XREAL_1: 8;
then ((((
Partial_Sums s)
. n)
+ (
sqrt ((n
+ 1)
* (n
+ 2))))
- (((n
+ 1)
* (n
+ 2))
/ 2))
> ((
sqrt ((n
+ 1)
* (n
+ 2)))
- (n
+ 1));
then ((((
Partial_Sums s)
. n)
+ (
sqrt ((n
+ 1)
* (n
+ 2))))
- (((n
+ 1)
* (n
+ 2))
/ 2))
>
0 by
A6,
XREAL_1: 50;
then
A7: (((((
Partial_Sums s)
. n)
+ (
sqrt ((n
+ 1)
* (n
+ 2))))
- (((n
+ 1)
* (n
+ 2))
/ 2))
+ (((n
+ 1)
* (n
+ 2))
/ 2))
> (
0
+ (((n
+ 1)
* (n
+ 2))
/ 2)) by
XREAL_1: 8;
thus thesis by
A5,
A7,
SERIES_1:def 1;
end;
A8: ((
Partial_Sums s)
. 1)
= ((
Partial_Sums s)
. (
0
+ 1))
.= (((
Partial_Sums s)
.
0 )
+ (s
. 1)) by
SERIES_1:def 1
.= ((s
.
0 )
+ (s
. 1)) by
SERIES_1:def 1
.= (
0
+ (s
. 1)) by
A1
.= (
sqrt (1
* (1
+ 1))) by
A1
.= (
sqrt 2);
then (((
Partial_Sums s)
. 1)
^2 )
= 2 by
SQUARE_1:def 2;
then (
sqrt (((
Partial_Sums s)
. 1)
^2 ))
> (
sqrt (((1
* (1
+ 1))
/ 2)
^2 )) by
SQUARE_1: 27;
then
A9: (
sqrt (((
Partial_Sums s)
. 1)
^2 ))
> ((1
* (1
+ 1))
/ 2) by
SQUARE_1: 22;
((
Partial_Sums s)
. 1)
>
0 by
A8,
SQUARE_1: 25;
then
A10:
X[1] by
A9,
SQUARE_1: 22;
for n be
Nat st n
>= 1 holds
X[n] from
NAT_1:sch 8(
A10,
A2);
hence thesis;
end;