series_2.miz
begin
reserve n for
Nat,
a,b for
Real,
s for
Real_Sequence;
theorem ::
SERIES_2:1
Th1:
|.((
- 1)
|^ n).|
= 1
proof
per cases ;
suppose
A1: n is
even;
((
- 1)
|^ n)
= ((
- 1)
to_power n) by
POWER: 41
.= (1
to_power n) by
A1,
POWER: 47
.= 1 by
POWER: 26;
hence thesis by
ABSVALUE:def 1;
end;
suppose
A2: n is
odd;
((
- 1)
|^ n)
= ((
- 1)
to_power n) by
POWER: 41
.= (
- (1
to_power n)) by
A2,
POWER: 48
.= (
- 1) by
POWER: 26;
then
|.((
- 1)
|^ n).|
= (
- (
- 1)) by
ABSVALUE:def 1;
hence thesis;
end;
end;
Lm1: (a
|^ 3)
= ((a
* a)
* a)
proof
(a
|^ (2
+ 1))
= ((a
|^ 2)
* a) by
NEWTON: 6;
hence thesis by
WSIERP_1: 1;
end;
Lm2: (a
|^ 3)
= ((a
|^ 2)
* a)
proof
(a
|^ (2
+ 1))
= ((a
|^ 2)
* a) by
NEWTON: 6;
hence thesis;
end;
Lm3: 4
= (2
|^ 2) & ((a
+ b)
|^ 2)
= (((a
|^ 2)
+ ((2
* a)
* b))
+ (b
|^ 2))
proof
A1: ((a
+ b)
|^ (1
+ 1))
= (((a
+ b)
|^ 1)
* (a
+ b)) by
NEWTON: 6
.= ((a
+ b)
* (a
+ b))
.= (((a
* a)
+ (a
* b))
+ ((a
* b)
+ (b
* b)))
.= (((a
* a)
+ (a
* b))
+ ((a
* b)
+ (b
|^ 2))) by
WSIERP_1: 1
.= (((a
|^ 2)
+ (a
* b))
+ ((a
* b)
+ (b
|^ 2))) by
WSIERP_1: 1
.= (((a
|^ 2)
+ (2
* (a
* b)))
+ (b
|^ 2));
(2
|^ 2)
= (2
* 2) by
WSIERP_1: 1
.= 4;
hence thesis by
A1;
end;
Lm4: ((a
+ 1)
|^ 3)
= ((((a
|^ 3)
+ (3
* (a
|^ 2)))
+ (3
* a))
+ 1)
proof
((a
+ 1)
|^ 3)
= (((a
+ 1)
|^ 2)
* (a
+ 1)) by
Lm2
.= ((((a
|^ 2)
+ ((2
* a)
* 1))
+ (1
|^ 2))
* (a
+ 1)) by
Lm3
.= ((((a
|^ 2)
+ (2
* a))
+ 1)
* (a
+ 1))
.= (((((a
|^ 2)
* a)
+ ((a
|^ 2)
* 1))
+ (((2
* a)
* a)
+ (2
* a)))
+ ((1
* a)
+ (1
* 1)))
.= (((((a
|^ 2)
* a)
+ ((a
|^ 2)
* 1))
+ (((2
* a)
* a)
+ ((2
* a)
* 1)))
+ (((1
|^ 2)
* a)
+ 1))
.= ((((a
|^ (2
+ 1))
+ (a
|^ 2))
+ (((2
* a)
* a)
+ (2
* a)))
+ (((1
|^ 2)
* a)
+ 1)) by
NEWTON: 6
.= ((((a
|^ 3)
+ (a
|^ 2))
+ ((2
* (a
* a))
+ (2
* a)))
+ ((1
* a)
+ 1))
.= ((((a
|^ 3)
+ (a
|^ 2))
+ ((2
* ((a
|^ 1)
* a))
+ (2
* a)))
+ (a
+ 1))
.= ((((a
|^ 3)
+ (a
|^ 2))
+ ((2
* (a
|^ (1
+ 1)))
+ (2
* a)))
+ (a
+ 1)) by
NEWTON: 6
.= (((((a
|^ 3)
+ (a
|^ 2))
+ (2
* (a
|^ 2)))
+ (2
* a))
+ (a
+ 1));
hence thesis;
end;
Lm5: (((n
* ((2
* n)
+ 1))
* (((3
* (n
|^ 2))
+ (3
* n))
- 1))
+ (((n
+ 1)
|^ 3)
* 30))
= (((n
+ 2)
* ((2
* (n
+ 1))
+ 1))
* (((3
* ((n
+ 1)
|^ 2))
+ (3
* (n
+ 1)))
- 1))
proof
(((n
+ 2)
* ((2
* (n
+ 1))
+ 1))
* (((3
* ((n
+ 1)
|^ 2))
+ (3
* (n
+ 1)))
- 1))
= (((n
+ 2)
* ((2
* n)
+ 3))
* (((3
* (((n
|^ 2)
+ ((2
* n)
* 1))
+ (1
|^ 2)))
+ ((3
* n)
+ 3))
- 1)) by
Lm3
.= ((((n
* (2
* n))
+ (2
* (2
* n)))
+ ((n
* 3)
+ (2
* 3)))
* ((((3
* (((n
|^ 2)
+ (2
* n))
+ (1
|^ 2)))
+ (3
* n))
+ 3)
- 1))
.= ((((n
* (2
* n))
+ (2
* (2
* n)))
+ ((n
* 3)
+ (2
* 3)))
* ((((3
* (((n
|^ 2)
+ (2
* n))
+ 1))
+ (3
* n))
+ 3)
- 1))
.= (((((n
* n)
* 2)
+ ((2
* 2)
* n))
+ ((n
* 3)
+ 6))
* (((((((n
|^ 2)
* 3)
+ (6
* n))
+ 3)
+ (3
* n))
+ 3)
- 1))
.= ((((2
* (n
|^ 2))
+ (4
* n))
+ ((n
* 3)
+ 6))
* ((((((3
* (n
|^ 2))
+ (6
* n))
+ 3)
+ (3
* n))
+ 3)
- 1)) by
WSIERP_1: 1
.= ((((((2
* ((n
|^ 2)
* (n
|^ 2)))
* 3)
+ (((2
* (n
|^ 2))
* n)
* 9))
+ (10
* (n
|^ 2)))
+ (((((7
* n)
* (n
|^ 2))
* 3)
+ (((7
* n)
* n)
* 9))
+ (35
* n)))
+ ((((6
* 3)
* (n
|^ 2))
+ ((6
* 9)
* n))
+ 30))
.= ((((((2
* (n
|^ (2
+ 2)))
* 3)
+ ((2
* ((n
|^ 2)
* n))
* 9))
+ (10
* (n
|^ 2)))
+ ((((7
* (n
* (n
|^ 2)))
* 3)
+ ((7
* (n
* n))
* 9))
+ (35
* n)))
+ (((18
* (n
|^ 2))
+ (54
* n))
+ 30)) by
NEWTON: 8
.= ((((((2
* (n
|^ 4))
* 3)
+ ((2
* (n
|^ (2
+ 1)))
* 9))
+ (10
* (n
|^ 2)))
+ ((((7
* (n
* (n
|^ 2)))
* 3)
+ ((7
* (n
* n))
* 9))
+ (35
* n)))
+ (((18
* (n
|^ 2))
+ (54
* n))
+ 30)) by
NEWTON: 6
.= (((((6
* (n
|^ 4))
+ ((2
* (n
|^ 3))
* 9))
+ (10
* (n
|^ 2)))
+ ((((7
* (n
|^ (2
+ 1)))
* 3)
+ ((7
* (n
* n))
* 9))
+ (35
* n)))
+ (((18
* (n
|^ 2))
+ (54
* n))
+ 30)) by
NEWTON: 6;
then
A1: (((n
+ 2)
* ((2
* (n
+ 1))
+ 1))
* (((3
* ((n
+ 1)
|^ 2))
+ (3
* (n
+ 1)))
- 1))
= (((((6
* (n
|^ 4))
+ (18
* (n
|^ 3)))
+ (10
* (n
|^ 2)))
+ ((((7
* (n
|^ 3))
* 3)
+ ((7
* (n
|^ 2))
* 9))
+ (35
* n)))
+ (((18
* (n
|^ 2))
+ (54
* n))
+ 30)) by
WSIERP_1: 1
.= (((((6
* (n
|^ 4))
+ (39
* (n
|^ 3)))
+ ((73
+ 18)
* (n
|^ 2)))
+ (89
* n))
+ 30);
(((n
* ((2
* n)
+ 1))
* (((3
* (n
|^ 2))
+ (3
* n))
- 1))
+ (((n
+ 1)
|^ 3)
* 30))
= ((((2
* (n
* n))
+ n)
* (((3
* (n
|^ 2))
+ (3
* n))
- 1))
+ (((n
+ 1)
|^ 3)
* 30))
.= ((((2
* ((n
|^ 1)
* n))
+ n)
* (((3
* (n
|^ 2))
+ (3
* n))
- 1))
+ (((n
+ 1)
|^ 3)
* 30))
.= ((((2
* (n
|^ (1
+ 1)))
+ n)
* (((3
* (n
|^ 2))
+ (3
* n))
- 1))
+ (((n
+ 1)
|^ 3)
* 30)) by
NEWTON: 6
.= ((((((2
* ((n
|^ 2)
* (n
|^ 2)))
* 3)
+ ((n
* (n
|^ 2))
* 3))
+ (((2
* ((n
|^ 2)
* n))
* 3)
+ ((n
* n)
* 3)))
- ((2
* (n
|^ 2))
+ n))
+ (((n
+ 1)
|^ 3)
* 30))
.= ((((((2
* (n
|^ (2
+ 2)))
* 3)
+ ((n
* (n
|^ 2))
* 3))
+ (((2
* ((n
|^ 2)
* n))
* 3)
+ ((n
* n)
* 3)))
- ((2
* (n
|^ 2))
+ n))
+ (((n
+ 1)
|^ 3)
* 30)) by
NEWTON: 8
.= ((((((2
* (n
|^ 4))
* 3)
+ ((n
* (n
|^ 2))
* 3))
+ (((2
* (n
|^ (2
+ 1)))
* 3)
+ ((n
* n)
* 3)))
- ((2
* (n
|^ 2))
+ n))
+ (((n
+ 1)
|^ 3)
* 30)) by
NEWTON: 6
.= ((((((2
* (n
|^ 4))
* 3)
+ ((n
* (n
|^ 2))
* 3))
+ (((2
* (n
|^ 3))
* 3)
+ ((n
|^ 2)
* 3)))
- ((2
* (n
|^ 2))
+ n))
+ (((n
+ 1)
|^ 3)
* 30)) by
WSIERP_1: 1
.= (((((6
* (n
|^ 4))
+ ((n
|^ (2
+ 1))
* 3))
+ ((6
* (n
|^ 3))
+ ((n
|^ 2)
* 3)))
- ((2
* (n
|^ 2))
+ n))
+ (((n
+ 1)
|^ 3)
* 30)) by
NEWTON: 6
.= (((((6
* (n
|^ 4))
+ (9
* (n
|^ 3)))
+ (1
* (n
|^ 2)))
- n)
+ (((((n
|^ 3)
+ (3
* (n
|^ 2)))
+ (3
* n))
+ 1)
* 30)) by
Lm4
.= (((((6
* (n
|^ 4))
+ (39
* (n
|^ 3)))
+ (91
* (n
|^ 2)))
+ ((90
- 1)
* n))
+ 30);
hence thesis by
A1;
end;
Lm6: for n be
Real holds ((n
+ 1)
|^ 4)
= (((((n
|^ 4)
+ (4
* (n
|^ 3)))
+ (6
* (n
|^ 2)))
+ (4
* n))
+ 1) & ((n
+ 1)
|^ 5)
= ((((((n
|^ 5)
+ (5
* (n
|^ 4)))
+ (10
* (n
|^ 3)))
+ (10
* (n
|^ 2)))
+ (5
* n))
+ 1)
proof
let n be
Real;
A1: ((n
+ 1)
|^ (3
+ 1))
= (((n
+ 1)
|^ 3)
* (n
+ 1)) by
NEWTON: 6
.= (((((n
|^ 3)
+ (3
* (n
|^ 2)))
+ (3
* n))
+ 1)
* (n
+ 1)) by
Lm4
.= ((((((n
|^ 3)
* n)
+ (n
|^ 3))
+ ((3
* ((n
|^ 2)
* n))
+ (3
* (n
|^ 2))))
+ ((3
* (n
* n))
+ (3
* n)))
+ (n
+ 1))
.= (((((n
|^ (3
+ 1))
+ (n
|^ 3))
+ ((3
* ((n
|^ 2)
* n))
+ (3
* (n
|^ 2))))
+ ((3
* (n
* n))
+ (3
* n)))
+ (n
+ 1)) by
NEWTON: 6
.= (((((n
|^ (3
+ 1))
+ (n
|^ 3))
+ ((3
* (n
|^ (2
+ 1)))
+ (3
* (n
|^ 2))))
+ ((3
* (n
* n))
+ (3
* n)))
+ (n
+ 1)) by
NEWTON: 6
.= (((((n
|^ 4)
+ (n
|^ 3))
+ ((3
* (n
|^ 3))
+ (3
* (n
|^ 2))))
+ ((3
* (n
|^ 2))
+ (3
* n)))
+ (n
+ 1)) by
WSIERP_1: 1;
((n
+ 1)
|^ (3
+ 2))
= (((n
+ 1)
|^ 3)
* ((n
+ 1)
|^ 2)) by
NEWTON: 8
.= (((((n
|^ 3)
+ (3
* (n
|^ 2)))
+ (3
* n))
+ 1)
* ((n
+ 1)
|^ 2)) by
Lm4
.= (((((n
|^ 3)
+ (3
* (n
|^ 2)))
+ (3
* n))
+ 1)
* (((n
|^ 2)
+ ((2
* n)
* 1))
+ (1
|^ 2))) by
Lm3
.= (((((n
|^ 3)
+ (3
* (n
|^ 2)))
+ (3
* n))
+ 1)
* (((n
|^ 2)
+ (2
* n))
+ 1))
.= (((((((n
|^ 3)
* (n
|^ 2))
+ ((2
* n)
* (n
|^ 3)))
+ ((n
|^ 3)
* 1))
+ ((((3
* (n
|^ 2))
* (n
|^ 2))
+ ((2
* n)
* (3
* (n
|^ 2))))
+ ((3
* (n
|^ 2))
* 1)))
+ ((((3
* n)
* (n
|^ 2))
+ ((3
* n)
* (2
* n)))
+ ((3
* n)
* 1)))
+ (((n
|^ 2)
+ (2
* n))
+ 1))
.= ((((((n
|^ (3
+ 2))
+ (2
* (n
* (n
|^ 3))))
+ (n
|^ 3))
+ (((3
* ((n
|^ 2)
* (n
|^ 2)))
+ ((2
* (n
* (n
|^ 2)))
* 3))
+ (3
* (n
|^ 2))))
+ (((3
* (n
* (n
|^ 2)))
+ ((3
* (n
* n))
* 2))
+ (3
* n)))
+ (((n
|^ 2)
+ (2
* n))
+ 1)) by
NEWTON: 8
.= ((((((n
|^ (3
+ 2))
+ (2
* (n
* (n
|^ 3))))
+ (n
|^ 3))
+ (((3
* (n
|^ (2
+ 2)))
+ ((2
* (n
* (n
|^ 2)))
* 3))
+ (3
* (n
|^ 2))))
+ (((3
* (n
* (n
|^ 2)))
+ ((3
* (n
* n))
* 2))
+ (3
* n)))
+ (((n
|^ 2)
+ (2
* n))
+ 1)) by
NEWTON: 8
.= ((((((n
|^ (3
+ 2))
+ (2
* (n
|^ (3
+ 1))))
+ (n
|^ 3))
+ (((3
* (n
|^ (2
+ 2)))
+ ((2
* (n
* (n
|^ 2)))
* 3))
+ (3
* (n
|^ 2))))
+ (((3
* (n
* (n
|^ 2)))
+ ((3
* (n
* n))
* 2))
+ (3
* n)))
+ (((n
|^ 2)
+ (2
* n))
+ 1)) by
NEWTON: 6
.= ((((((n
|^ (3
+ 2))
+ (2
* (n
|^ (3
+ 1))))
+ (n
|^ 3))
+ (((3
* (n
|^ (2
+ 2)))
+ ((2
* (n
|^ (2
+ 1)))
* 3))
+ (3
* (n
|^ 2))))
+ (((3
* (n
* (n
|^ 2)))
+ ((3
* (n
* n))
* 2))
+ (3
* n)))
+ (((n
|^ 2)
+ (2
* n))
+ 1)) by
NEWTON: 6
.= ((((((n
|^ 5)
+ (2
* (n
|^ 4)))
+ (n
|^ 3))
+ (((3
* (n
|^ 4))
+ ((2
* (n
|^ 3))
* 3))
+ (3
* (n
|^ 2))))
+ (((3
* (n
|^ 3))
+ ((3
* (n
* n))
* 2))
+ (3
* n)))
+ (((n
|^ 2)
+ (2
* n))
+ 1)) by
NEWTON: 6
.= ((((((n
|^ 5)
+ (2
* (n
|^ 4)))
+ (n
|^ 3))
+ (((3
* (n
|^ 4))
+ (6
* (n
|^ 3)))
+ (3
* (n
|^ 2))))
+ (((3
* (n
|^ 3))
+ ((3
* (n
|^ 2))
* 2))
+ (3
* n)))
+ (((n
|^ 2)
+ (2
* n))
+ 1)) by
WSIERP_1: 1;
hence thesis by
A1;
end;
theorem ::
SERIES_2:2
for n be
Real holds ((n
+ 1)
|^ 3)
= ((((n
|^ 3)
+ (3
* (n
|^ 2)))
+ (3
* n))
+ 1) & ((n
+ 1)
|^ 4)
= (((((n
|^ 4)
+ (4
* (n
|^ 3)))
+ (6
* (n
|^ 2)))
+ (4
* n))
+ 1) & ((n
+ 1)
|^ 5)
= ((((((n
|^ 5)
+ (5
* (n
|^ 4)))
+ (10
* (n
|^ 3)))
+ (10
* (n
|^ 2)))
+ (5
* n))
+ 1) by
Lm4,
Lm6;
Lm7: for n holds (1
- (1
/ (n
+ 2)))
= ((n
+ 1)
/ (n
+ 2)) & (1
/ ((n
+ 1)
! ))
= ((n
+ 2)
/ (((n
+ 1)
! )
* (n
+ 2)))
proof
let n;
n
>=
0 by
NAT_1: 2;
then (n
+ 1)
>
0 by
NAT_1: 13;
then
A1: ((n
+ 1)
+ 1)
>
0 by
NAT_1: 13;
then
A2: (1
/ ((n
+ 1)
! ))
= ((1
* (n
+ 2))
/ (((n
+ 1)
! )
* (n
+ 2))) by
XCMPLX_1: 91;
((n
+ 1)
/ (n
+ 2))
= (((n
+ 2)
- 1)
/ (n
+ 2))
.= (((n
+ 2)
/ (n
+ 2))
- (1
/ (n
+ 2))) by
XCMPLX_1: 120
.= (1
- (1
/ (n
+ 2))) by
A1,
XCMPLX_1: 60;
hence thesis by
A2;
end;
Lm8: ((1
/ (n
+ 1))
- (2
/ ((n
+ 1)
* (n
+ 3))))
= (1
/ (n
+ 3))
proof
n
>=
0 by
NAT_1: 2;
then
A1: (n
+ 1)
>
0 by
NAT_1: 13;
then ((n
+ 1)
+ 1)
>
0 by
NAT_1: 13;
then ((n
+ 2)
+ 1)
>
0 by
NAT_1: 13;
then ((1
/ (n
+ 1))
- (2
/ ((n
+ 1)
* (n
+ 3))))
= (((1
* (n
+ 3))
/ ((n
+ 1)
* (n
+ 3)))
- (2
/ ((n
+ 1)
* (n
+ 3)))) by
XCMPLX_1: 91
.= (((n
+ 3)
- 2)
/ ((n
+ 1)
* (n
+ 3))) by
XCMPLX_1: 120
.= (((n
+ 1)
* 1)
/ ((n
+ 1)
* (n
+ 3)))
.= (1
/ (n
+ 3)) by
A1,
XCMPLX_1: 91;
hence thesis;
end;
Lm9: ((1
/ (n
+ 1))
- (3
/ ((n
+ 1)
* (n
+ 4))))
= (1
/ (n
+ 4))
proof
n
>=
0 by
NAT_1: 2;
then
A1: (n
+ 1)
>
0 by
NAT_1: 13;
then ((n
+ 1)
+ 1)
>
0 by
NAT_1: 13;
then ((n
+ 2)
+ 1)
>
0 by
NAT_1: 13;
then ((n
+ 3)
+ 1)
>
0 by
NAT_1: 13;
then ((1
/ (n
+ 1))
- (3
/ ((n
+ 1)
* (n
+ 4))))
= (((1
* (n
+ 4))
/ ((n
+ 1)
* (n
+ 4)))
- (3
/ ((n
+ 1)
* (n
+ 4)))) by
XCMPLX_1: 91
.= (((n
+ 4)
- 3)
/ ((n
+ 1)
* (n
+ 4))) by
XCMPLX_1: 120
.= (((n
+ 1)
* 1)
/ ((n
+ 1)
* (n
+ 4)))
.= (1
/ (n
+ 4)) by
A1,
XCMPLX_1: 91;
hence thesis;
end;
Lm10: (((n
|^ 2)
+ (3
* n))
+ 2)
= ((n
+ 1)
* (n
+ 2))
proof
((n
+ 1)
* (n
+ 2))
= (((n
* n)
+ ((2
* n)
+ (1
* n)))
+ 2)
.= ((((n
|^ 1)
* n)
+ ((2
+ 1)
* n))
+ 2)
.= (((n
|^ (1
+ 1))
+ ((2
+ 1)
* n))
+ 2) by
NEWTON: 6;
hence thesis;
end;
Lm11: ((((n
* (4
* (n
|^ 2)))
+ (11
* n))
+ (12
* (n
|^ 2)))
+ 3)
= ((n
+ 1)
* ((4
* ((n
+ 1)
|^ 2))
- 1))
proof
((n
+ 1)
* ((4
* ((n
+ 1)
|^ 2))
- 1))
= ((n
+ 1)
* ((4
* (((n
|^ 2)
+ ((2
* n)
* 1))
+ (1
|^ 2)))
- 1)) by
Lm3
.= ((n
+ 1)
* ((4
* (((n
|^ 2)
+ (2
* n))
+ 1))
- 1))
.= ((((n
* (4
* (n
|^ 2)))
+ (4
* (n
|^ 2)))
+ ((8
* (n
* n))
+ (8
* n)))
+ ((3
* n)
+ (3
* 1)))
.= ((((n
* (4
* (n
|^ 2)))
+ (4
* (n
|^ 2)))
+ ((8
* (n
|^ 2))
+ (8
* n)))
+ ((3
* n)
+ (3
* 1))) by
WSIERP_1: 1
.= ((((n
* (4
* (n
|^ 2)))
+ ((4
* (n
|^ 2))
+ (8
* (n
|^ 2))))
+ ((8
* n)
+ (3
* n)))
+ 3);
hence thesis;
end;
Lm12: (((n
+ 1)
|^ 2)
* ((2
* ((n
+ 1)
|^ 2))
- 1))
= (((((((n
|^ 2)
* (n
|^ 2))
* 2)
+ ((12
- 1)
* (n
|^ 2)))
+ (8
* (n
|^ 3)))
+ (6
* n))
+ 1)
proof
(((n
+ 1)
|^ 2)
* ((2
* ((n
+ 1)
|^ 2))
- 1))
= ((((n
+ 1)
|^ 2)
* (2
* ((n
+ 1)
|^ 2)))
- (((n
+ 1)
|^ 2)
* 1))
.= (((((n
+ 1)
|^ 2)
* ((n
+ 1)
|^ 2))
* 2)
- (((n
|^ 2)
+ ((2
* n)
* 1))
+ (1
|^ 2))) by
Lm3
.= (((((n
+ 1)
|^ 2)
* ((n
+ 1)
|^ 2))
* 2)
- (((n
|^ 2)
+ (2
* n))
+ 1))
.= (((((n
+ 1)
|^ 2)
* (((n
|^ 2)
+ ((2
* n)
* 1))
+ (1
|^ 2)))
* 2)
- (((n
|^ 2)
+ (2
* n))
+ 1)) by
Lm3
.= ((((((n
|^ 2)
+ ((2
* n)
* 1))
+ (1
|^ 2))
* (((n
|^ 2)
+ (2
* n))
+ (1
|^ 2)))
* 2)
- (((n
|^ 2)
+ (2
* n))
+ 1)) by
Lm3
.= ((((((n
|^ 2)
+ (2
* n))
+ (1
|^ 2))
* (((n
|^ 2)
+ (2
* n))
+ 1))
* 2)
- (((n
|^ 2)
+ (2
* n))
+ 1))
.= ((((((n
|^ 2)
+ (2
* n))
+ 1)
* (((n
|^ 2)
+ (2
* n))
+ 1))
* 2)
- (((n
|^ 2)
+ (2
* n))
+ 1))
.= ((((((((n
|^ 2)
* (n
|^ 2))
+ ((2
* n)
* (n
|^ 2)))
+ (n
|^ 2))
+ ((((2
* n)
* (n
|^ 2))
+ (((2
* n)
* n)
* 2))
+ (2
* n)))
+ (((n
|^ 2)
+ (2
* n))
+ 1))
* 2)
- (((n
|^ 2)
+ (2
* n))
+ 1))
.= ((((((((n
|^ 2)
* (n
|^ 2))
+ (2
* (n
|^ (2
+ 1))))
+ (n
|^ 2))
+ (((2
* (n
* (n
|^ 2)))
+ ((2
* (n
* n))
* 2))
+ (2
* n)))
+ (((n
|^ 2)
+ (2
* n))
+ 1))
* 2)
- (((n
|^ 2)
+ (2
* n))
+ 1)) by
NEWTON: 6
.= ((((((((n
|^ 2)
* (n
|^ 2))
+ (2
* (n
|^ (2
+ 1))))
+ (n
|^ 2))
+ (((2
* (n
|^ (2
+ 1)))
+ ((2
* (n
* n))
* 2))
+ (2
* n)))
+ (((n
|^ 2)
+ (2
* n))
+ 1))
* 2)
- (((n
|^ 2)
+ (2
* n))
+ 1)) by
NEWTON: 6
.= ((((((((n
|^ 2)
* (n
|^ 2))
+ (2
* (n
|^ 3)))
+ (n
|^ 2))
+ (((2
* (n
|^ 3))
+ ((2
* ((n
|^ 1)
* n))
* 2))
+ (2
* n)))
+ (((n
|^ 2)
+ (2
* n))
+ 1))
* 2)
- (((n
|^ 2)
+ (2
* n))
+ 1))
.= ((((((((n
|^ 2)
* (n
|^ 2))
+ (2
* (n
|^ 3)))
+ (n
|^ 2))
+ (((2
* (n
|^ 3))
+ ((2
* (n
|^ (1
+ 1)))
* 2))
+ (2
* n)))
+ (((n
|^ 2)
+ (2
* n))
+ 1))
* 2)
- (((n
|^ 2)
+ (2
* n))
+ 1)) by
NEWTON: 6
.= ((((((((n
|^ 2)
* (n
|^ 2))
+ (2
* (n
|^ 3)))
+ (n
|^ 2))
+ (((2
* (n
|^ 3))
+ ((2
* (n
|^ 2))
* 2))
+ (2
* n)))
+ (((n
|^ 2)
+ (2
* n))
+ 1))
* 2)
- (((n
|^ 2)
+ (2
* n))
+ 1));
hence thesis;
end;
Lm13: ((n
+ 2)
* ((((n
+ 1)
|^ 2)
+ (n
+ 1))
- 1))
= ((((n
|^ 3)
+ (5
* (n
|^ 2)))
+ (7
* n))
+ 2)
proof
((n
+ 2)
* ((((n
+ 1)
|^ 2)
+ (n
+ 1))
- 1))
= ((n
+ 2)
* (((((n
|^ 2)
+ ((2
* n)
* 1))
+ (1
|^ 2))
+ (n
+ 1))
- 1)) by
Lm3
.= ((n
+ 2)
* (((((n
|^ 2)
+ ((2
* n)
* 1))
+ 1)
+ (n
+ 1))
- 1))
.= ((((((n
* (n
|^ 2))
+ (2
* (n
|^ 2)))
+ (3
* (n
* n)))
+ (6
* n))
+ n)
+ 2)
.= ((((((n
* (n
|^ 2))
+ (2
* (n
|^ 2)))
+ (3
* (n
|^ 2)))
+ (6
* n))
+ n)
+ 2) by
WSIERP_1: 1
.= ((((((n
|^ (2
+ 1))
+ (2
* (n
|^ 2)))
+ (3
* (n
|^ 2)))
+ (6
* n))
+ n)
+ 2) by
NEWTON: 6
.= ((((n
|^ (2
+ 1))
+ ((2
+ 3)
* (n
|^ 2)))
+ ((6
+ 1)
* n))
+ 2);
hence thesis;
end;
Lm14: (for n holds (s
. n)
= ((a
* n)
+ b)) implies for n holds ((
Partial_Sums s)
. n)
= (((((a
* (n
+ 1))
* n)
/ 2)
+ (n
* b))
+ b)
proof
defpred
X[
Nat] means ((
Partial_Sums s)
. $1)
= (((((a
* ($1
+ 1))
* $1)
/ 2)
+ ($1
* b))
+ b);
assume
A1: for n holds (s
. n)
= ((a
* n)
+ b);
A2: for n st
X[n] holds
X[(n
+ 1)]
proof
let n;
assume ((
Partial_Sums s)
. n)
= (((((a
* (n
+ 1))
* n)
/ 2)
+ (n
* b))
+ b);
then ((
Partial_Sums s)
. (n
+ 1))
= ((((((a
* (n
+ 1))
* n)
/ 2)
+ (n
* b))
+ b)
+ (s
. (n
+ 1))) by
SERIES_1:def 1
.= ((((((a
* (n
+ 1))
* n)
/ 2)
+ (n
* b))
+ b)
+ ((a
* (n
+ 1))
+ b)) by
A1
.= (((((a
* (n
+ 1))
* (n
+ 2))
/ 2)
+ ((n
+ 1)
* b))
+ b);
hence thesis;
end;
((
Partial_Sums s)
.
0 )
= (s
.
0 ) by
SERIES_1:def 1
.= (((((a
* (
0
+ 1))
*
0 )
/ 2)
+ (
0
* b))
+ b) by
A1;
then
A3:
X[
0 ];
for n holds
X[n] from
NAT_1:sch 2(
A3,
A2);
hence thesis;
end;
theorem ::
SERIES_2:3
(for n holds (s
. n)
= n) implies for n 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 holds (s
. n)
= n;
A2: for n st
X[n] holds
X[(n
+ 1)]
proof
let n;
assume ((
Partial_Sums s)
. n)
= ((n
* (n
+ 1))
/ 2);
then ((
Partial_Sums s)
. (n
+ 1))
= (((n
* (n
+ 1))
/ 2)
+ (s
. (n
+ 1))) by
SERIES_1:def 1
.= (((n
* (n
+ 1))
/ 2)
+ (n
+ 1)) by
A1
.= (((n
* (n
+ 1))
+ ((n
+ 1)
* 2))
/ 2);
hence thesis;
end;
((
Partial_Sums s)
.
0 )
= (s
.
0 ) by
SERIES_1:def 1
.= ((
0
* (
0
+ 1))
/ 2) by
A1;
then
A3:
X[
0 ];
for n holds
X[n] from
NAT_1:sch 2(
A3,
A2);
hence thesis;
end;
theorem ::
SERIES_2:4
(for n holds (s
. n)
= (2
* n)) implies for n holds ((
Partial_Sums s)
. n)
= (n
* (n
+ 1))
proof
defpred
X[
Nat] means ((
Partial_Sums s)
. $1)
= ($1
* ($1
+ 1));
assume
A1: for n holds (s
. n)
= (2
* n);
A2: for n st
X[n] holds
X[(n
+ 1)]
proof
let n;
assume ((
Partial_Sums s)
. n)
= (n
* (n
+ 1));
then ((
Partial_Sums s)
. (n
+ 1))
= ((n
* (n
+ 1))
+ (s
. (n
+ 1))) by
SERIES_1:def 1
.= ((n
* (n
+ 1))
+ (2
* (n
+ 1))) by
A1
.= ((n
+ 2)
* (n
+ 1));
hence thesis;
end;
((
Partial_Sums s)
.
0 )
= (s
.
0 ) by
SERIES_1:def 1
.= (2
*
0 ) by
A1
.= (
0
* (
0
+ 1));
then
A3:
X[
0 ];
for n holds
X[n] from
NAT_1:sch 2(
A3,
A2);
hence thesis;
end;
theorem ::
SERIES_2:5
(for n holds (s
. n)
= ((2
* n)
+ 1)) implies for n holds ((
Partial_Sums s)
. n)
= ((n
+ 1)
|^ 2)
proof
defpred
X[
Nat] means ((
Partial_Sums s)
. $1)
= (($1
+ 1)
|^ 2);
assume
A1: for n holds (s
. n)
= ((2
* n)
+ 1);
A2: for n st
X[n] holds
X[(n
+ 1)]
proof
let n;
assume ((
Partial_Sums s)
. n)
= ((n
+ 1)
|^ 2);
then ((
Partial_Sums s)
. (n
+ 1))
= (((n
+ 1)
|^ 2)
+ (s
. (n
+ 1))) by
SERIES_1:def 1
.= (((n
+ 1)
|^ 2)
+ ((2
* (n
+ 1))
+ 1)) by
A1
.= ((((n
+ 1)
|^ 2)
+ (2
* n))
+ 3)
.= (((((n
|^ 2)
+ ((2
* n)
* 1))
+ (1
|^ 2))
+ (2
* n))
+ 3) by
Lm3
.= (((((n
|^ 2)
+ (2
* n))
+ 1)
+ (2
* n))
+ 3)
.= (((n
|^ 2)
+ ((2
* n)
* 2))
+ (2
|^ 2)) by
Lm3
.= ((n
+ 2)
|^ 2) by
Lm3;
hence thesis;
end;
((
Partial_Sums s)
.
0 )
= (s
.
0 ) by
SERIES_1:def 1
.= ((2
*
0 )
+ 1) by
A1
.= ((
0
+ 1)
|^ 2);
then
A3:
X[
0 ];
for n holds
X[n] from
NAT_1:sch 2(
A3,
A2);
hence thesis;
end;
theorem ::
SERIES_2:6
(for n holds (s
. n)
= (n
* (n
+ 1))) implies for n holds ((
Partial_Sums s)
. n)
= (((n
* (n
+ 1))
* (n
+ 2))
/ 3)
proof
defpred
X[
Nat] means ((
Partial_Sums s)
. $1)
= ((($1
* ($1
+ 1))
* ($1
+ 2))
/ 3);
assume
A1: for n holds (s
. n)
= (n
* (n
+ 1));
A2: for n st
X[n] holds
X[(n
+ 1)]
proof
let n;
assume ((
Partial_Sums s)
. n)
= (((n
* (n
+ 1))
* (n
+ 2))
/ 3);
then ((
Partial_Sums s)
. (n
+ 1))
= ((((n
* (n
+ 1))
* (n
+ 2))
/ 3)
+ (s
. (n
+ 1))) by
SERIES_1:def 1
.= ((((n
* (n
+ 1))
* (n
+ 2))
/ 3)
+ ((n
+ 1)
* ((n
+ 1)
+ 1))) by
A1
.= ((((n
+ 1)
* (n
+ 2))
* (n
+ 3))
/ 3);
hence thesis;
end;
((
Partial_Sums s)
.
0 )
= (s
.
0 ) by
SERIES_1:def 1
.= (((
0
* (
0
+ 1))
* (
0
+ 2))
/ 3) by
A1;
then
A3:
X[
0 ];
for n holds
X[n] from
NAT_1:sch 2(
A3,
A2);
hence thesis;
end;
theorem ::
SERIES_2:7
(for n holds (s
. n)
= ((n
* (n
+ 1))
* (n
+ 2))) implies for n holds ((
Partial_Sums s)
. n)
= ((((n
* (n
+ 1))
* (n
+ 2))
* (n
+ 3))
/ 4)
proof
defpred
X[
Nat] means ((
Partial_Sums s)
. $1)
= (((($1
* ($1
+ 1))
* ($1
+ 2))
* ($1
+ 3))
/ 4);
assume
A1: for n holds (s
. n)
= ((n
* (n
+ 1))
* (n
+ 2));
A2: for n st
X[n] holds
X[(n
+ 1)]
proof
let n;
assume ((
Partial_Sums s)
. n)
= ((((n
* (n
+ 1))
* (n
+ 2))
* (n
+ 3))
/ 4);
then ((
Partial_Sums s)
. (n
+ 1))
= (((((n
* (n
+ 1))
* (n
+ 2))
* (n
+ 3))
/ 4)
+ (s
. (n
+ 1))) by
SERIES_1:def 1
.= (((((n
* (n
+ 1))
* (n
+ 2))
* (n
+ 3))
/ 4)
+ (((n
+ 1)
* ((n
+ 1)
+ 1))
* ((n
+ 1)
+ 2))) by
A1
.= (((((n
+ 1)
* ((n
+ 1)
+ 1))
* ((n
+ 1)
+ 2))
* ((n
+ 1)
+ 3))
/ 4);
hence thesis;
end;
((
Partial_Sums s)
.
0 )
= (s
.
0 ) by
SERIES_1:def 1
.= ((((
0
* (
0
+ 1))
* (
0
+ 2))
* (
0
+ 3))
/ 4) by
A1;
then
A3:
X[
0 ];
for n holds
X[n] from
NAT_1:sch 2(
A3,
A2);
hence thesis;
end;
theorem ::
SERIES_2:8
(for n holds (s
. n)
= (((n
* (n
+ 1))
* (n
+ 2))
* (n
+ 3))) implies for n holds ((
Partial_Sums s)
. n)
= (((((n
* (n
+ 1))
* (n
+ 2))
* (n
+ 3))
* (n
+ 4))
/ 5)
proof
defpred
X[
Nat] means ((
Partial_Sums s)
. $1)
= ((((($1
* ($1
+ 1))
* ($1
+ 2))
* ($1
+ 3))
* ($1
+ 4))
/ 5);
assume
A1: for n holds (s
. n)
= (((n
* (n
+ 1))
* (n
+ 2))
* (n
+ 3));
A2: for n st
X[n] holds
X[(n
+ 1)]
proof
let n;
assume ((
Partial_Sums s)
. n)
= (((((n
* (n
+ 1))
* (n
+ 2))
* (n
+ 3))
* (n
+ 4))
/ 5);
then ((
Partial_Sums s)
. (n
+ 1))
= ((((((n
* (n
+ 1))
* (n
+ 2))
* (n
+ 3))
* (n
+ 4))
/ 5)
+ (s
. (n
+ 1))) by
SERIES_1:def 1
.= ((((((n
* (n
+ 1))
* (n
+ 2))
* (n
+ 3))
* (n
+ 4))
/ 5)
+ ((((n
+ 1)
* ((n
+ 1)
+ 1))
* ((n
+ 1)
+ 2))
* ((n
+ 1)
+ 3))) by
A1
.= ((((((n
+ 1)
* (n
+ 2))
* (n
+ 3))
* (n
+ 4))
* (n
+ 5))
/ 5);
hence thesis;
end;
((
Partial_Sums s)
.
0 )
= (s
.
0 ) by
SERIES_1:def 1
.= (((((
0
* (
0
+ 1))
* (
0
+ 2))
* (
0
+ 3))
* (
0
+ 4))
/ 4) by
A1;
then
A3:
X[
0 ];
for n holds
X[n] from
NAT_1:sch 2(
A3,
A2);
hence thesis;
end;
theorem ::
SERIES_2:9
(for n holds (s
. n)
= (1
/ (n
* (n
+ 1)))) implies for n holds ((
Partial_Sums s)
. n)
= (1
- (1
/ (n
+ 1)))
proof
defpred
X[
Nat] means ((
Partial_Sums s)
. $1)
= (1
- (1
/ ($1
+ 1)));
assume
A1: for n holds (s
. n)
= (1
/ (n
* (n
+ 1)));
A2: for n st
X[n] holds
X[(n
+ 1)]
proof
let n;
A3: (n
+ 1)
<>
0 by
NAT_1: 5;
assume ((
Partial_Sums s)
. n)
= (1
- (1
/ (n
+ 1)));
then ((
Partial_Sums s)
. (n
+ 1))
= ((1
- (1
/ (n
+ 1)))
+ (s
. (n
+ 1))) by
SERIES_1:def 1
.= ((1
- (1
/ (n
+ 1)))
+ (1
/ ((n
+ 1)
* ((n
+ 1)
+ 1)))) by
A1
.= (1
- ((1
/ (n
+ 1))
- (1
/ ((n
+ 1)
* (n
+ 2)))))
.= (1
- ((1
* (1
/ (n
+ 1)))
- ((1
/ (n
+ 1))
* (1
/ (n
+ 2))))) by
XCMPLX_1: 102
.= (1
- ((1
/ (n
+ 1))
* (1
- (1
/ (n
+ 2)))))
.= (1
- ((1
/ (n
+ 1))
* (((1
* (n
+ 2))
- 1)
/ (n
+ 2)))) by
Lm7
.= (1
- (((1
/ (n
+ 1))
* (n
+ 1))
/ (n
+ 2))) by
XCMPLX_1: 74
.= (1
- (1
/ (n
+ 2))) by
A3,
XCMPLX_1: 87;
hence thesis;
end;
((
Partial_Sums s)
.
0 )
= (s
.
0 ) by
SERIES_1:def 1
.= (1
/ (
0
* (
0
+ 1))) by
A1
.= (1
- (1
/ 1)) by
XCMPLX_1: 49;
then
A4:
X[
0 ];
for n holds
X[n] from
NAT_1:sch 2(
A4,
A2);
hence thesis;
end;
theorem ::
SERIES_2:10
(for n holds (s
. n)
= (1
/ ((n
* (n
+ 1))
* (n
+ 2)))) implies for n holds ((
Partial_Sums s)
. n)
= ((1
/ 4)
- (1
/ ((2
* (n
+ 1))
* (n
+ 2))))
proof
defpred
X[
Nat] means ((
Partial_Sums s)
. $1)
= ((1
/ 4)
- (1
/ ((2
* ($1
+ 1))
* ($1
+ 2))));
assume
A1: for n holds (s
. n)
= (1
/ ((n
* (n
+ 1))
* (n
+ 2)));
A2: for n st
X[n] holds
X[(n
+ 1)]
proof
let n;
assume ((
Partial_Sums s)
. n)
= ((1
/ 4)
- (1
/ ((2
* (n
+ 1))
* (n
+ 2))));
then ((
Partial_Sums s)
. (n
+ 1))
= (((1
/ 4)
- (1
/ ((2
* (n
+ 1))
* (n
+ 2))))
+ (s
. (n
+ 1))) by
SERIES_1:def 1
.= (((1
/ 4)
- (1
/ ((2
* (n
+ 1))
* (n
+ 2))))
+ (1
/ (((n
+ 1)
* ((n
+ 1)
+ 1))
* ((n
+ 1)
+ 2)))) by
A1
.= ((1
/ 4)
- ((1
/ ((2
* (n
+ 1))
* (n
+ 2)))
- (1
/ (((n
+ 1)
* (n
+ 2))
* (n
+ 3)))))
.= ((1
/ 4)
- ((1
/ ((2
* (n
+ 2))
* (n
+ 1)))
- ((1
* 2)
/ ((((n
+ 2)
* (n
+ 1))
* (n
+ 3))
* 2)))) by
XCMPLX_1: 91
.= ((1
/ 4)
- ((1
/ ((2
* (n
+ 2))
* (n
+ 1)))
- ((1
* 2)
/ (((n
+ 2)
* 2)
* ((n
+ 1)
* (n
+ 3))))))
.= ((1
/ 4)
- ((1
/ ((2
* (n
+ 2))
* (n
+ 1)))
- ((1
/ ((n
+ 2)
* 2))
* (2
/ ((n
+ 1)
* (n
+ 3)))))) by
XCMPLX_1: 76
.= ((1
/ 4)
- (((1
/ (2
* (n
+ 2)))
* (1
/ (n
+ 1)))
- ((1
/ (2
* (n
+ 2)))
* (2
/ ((n
+ 1)
* (n
+ 3)))))) by
XCMPLX_1: 102
.= ((1
/ 4)
- ((1
/ (2
* (n
+ 2)))
* ((1
/ (n
+ 1))
- (2
/ ((n
+ 1)
* (n
+ 3))))))
.= ((1
/ 4)
- ((1
/ (2
* (n
+ 2)))
* (1
/ (n
+ 3)))) by
Lm8
.= ((1
/ 4)
- (1
/ ((2
* ((n
+ 1)
+ 1))
* ((n
+ 1)
+ 2)))) by
XCMPLX_1: 102;
hence thesis;
end;
((
Partial_Sums s)
.
0 )
= (s
.
0 ) by
SERIES_1:def 1
.= (1
/ ((
0
* (
0
+ 1))
* (
0
+ 2))) by
A1
.= ((1
/ 4)
- (1
/ ((2
* (
0
+ 1))
* (
0
+ 2)))) by
XCMPLX_1: 49;
then
A3:
X[
0 ];
for n holds
X[n] from
NAT_1:sch 2(
A3,
A2);
hence thesis;
end;
theorem ::
SERIES_2:11
(for n holds (s
. n)
= (1
/ (((n
* (n
+ 1))
* (n
+ 2))
* (n
+ 3)))) implies for n holds ((
Partial_Sums s)
. n)
= ((1
/ 18)
- (1
/ (((3
* (n
+ 1))
* (n
+ 2))
* (n
+ 3))))
proof
defpred
X[
Nat] means ((
Partial_Sums s)
. $1)
= ((1
/ 18)
- (1
/ (((3
* ($1
+ 1))
* ($1
+ 2))
* ($1
+ 3))));
assume
A1: for n holds (s
. n)
= (1
/ (((n
* (n
+ 1))
* (n
+ 2))
* (n
+ 3)));
A2: for n st
X[n] holds
X[(n
+ 1)]
proof
let n;
assume ((
Partial_Sums s)
. n)
= ((1
/ 18)
- (1
/ (((3
* (n
+ 1))
* (n
+ 2))
* (n
+ 3))));
then ((
Partial_Sums s)
. (n
+ 1))
= (((1
/ 18)
- (1
/ (((3
* (n
+ 1))
* (n
+ 2))
* (n
+ 3))))
+ (s
. (n
+ 1))) by
SERIES_1:def 1
.= (((1
/ 18)
- (1
/ (((3
* (n
+ 1))
* (n
+ 2))
* (n
+ 3))))
+ (1
/ ((((n
+ 1)
* ((n
+ 1)
+ 1))
* ((n
+ 1)
+ 2))
* ((n
+ 1)
+ 3)))) by
A1
.= ((1
/ 18)
- ((1
/ (((3
* (n
+ 1))
* (n
+ 2))
* (n
+ 3)))
- (1
/ ((((n
+ 1)
* (n
+ 2))
* (n
+ 3))
* (n
+ 4)))))
.= ((1
/ 18)
- ((1
/ (((3
* (n
+ 1))
* (n
+ 2))
* (n
+ 3)))
- ((1
* 3)
/ (((((n
+ 1)
* (n
+ 2))
* (n
+ 3))
* (n
+ 4))
* 3)))) by
XCMPLX_1: 91
.= ((1
/ 18)
- ((1
/ (((3
* (n
+ 2))
* (n
+ 3))
* (n
+ 1)))
- ((1
* 3)
/ (((3
* (n
+ 2))
* (n
+ 3))
* ((n
+ 1)
* (n
+ 4))))))
.= ((1
/ 18)
- ((1
/ (((3
* (n
+ 2))
* (n
+ 3))
* (n
+ 1)))
- ((1
/ ((3
* (n
+ 2))
* (n
+ 3)))
* (3
/ ((n
+ 1)
* (n
+ 4)))))) by
XCMPLX_1: 76
.= ((1
/ 18)
- (((1
/ ((3
* (n
+ 2))
* (n
+ 3)))
* (1
/ (n
+ 1)))
- ((1
/ ((3
* (n
+ 2))
* (n
+ 3)))
* (3
/ ((n
+ 1)
* (n
+ 4)))))) by
XCMPLX_1: 102
.= ((1
/ 18)
- ((1
/ ((3
* (n
+ 2))
* (n
+ 3)))
* ((1
/ (n
+ 1))
- (3
/ ((n
+ 1)
* (n
+ 4))))))
.= ((1
/ 18)
- ((1
/ ((3
* (n
+ 2))
* (n
+ 3)))
* (1
/ (n
+ 4)))) by
Lm9
.= ((1
/ 18)
- (1
/ (((3
* ((n
+ 1)
+ 1))
* ((n
+ 1)
+ 2))
* ((n
+ 1)
+ 3)))) by
XCMPLX_1: 102;
hence thesis;
end;
((
Partial_Sums s)
.
0 )
= (s
.
0 ) by
SERIES_1:def 1
.= (1
/ (((
0
* (
0
+ 1))
* (
0
+ 2))
* (
0
+ 3))) by
A1
.= ((1
/ 18)
- (1
/ (((3
* (
0
+ 1))
* (
0
+ 2))
* (
0
+ 3)))) by
XCMPLX_1: 49;
then
A3:
X[
0 ];
for n holds
X[n] from
NAT_1:sch 2(
A3,
A2);
hence thesis;
end;
theorem ::
SERIES_2:12
(for n holds (s
. n)
= (n
|^ 2)) implies for n holds ((
Partial_Sums s)
. n)
= (((n
* (n
+ 1))
* ((2
* n)
+ 1))
/ 6)
proof
defpred
X[
Nat] means ((
Partial_Sums s)
. $1)
= ((($1
* ($1
+ 1))
* ((2
* $1)
+ 1))
/ 6);
assume
A1: for n holds (s
. n)
= (n
|^ 2);
A2: for n st
X[n] holds
X[(n
+ 1)]
proof
let n;
assume ((
Partial_Sums s)
. n)
= (((n
* (n
+ 1))
* ((2
* n)
+ 1))
/ 6);
then ((
Partial_Sums s)
. (n
+ 1))
= ((((n
* (n
+ 1))
* ((2
* n)
+ 1))
/ 6)
+ (s
. (n
+ 1))) by
SERIES_1:def 1
.= ((((n
* (n
+ 1))
* ((2
* n)
+ 1))
/ 6)
+ ((n
+ 1)
|^ 2)) by
A1
.= ((((n
* (n
+ 1))
* ((2
* n)
+ 1))
+ (((n
+ 1)
|^ 2)
* 6))
/ 6)
.= (((((n
+ 1)
* n)
* ((2
* n)
+ 1))
+ (((n
+ 1)
* (n
+ 1))
* 6))
/ 6) by
WSIERP_1: 1;
hence thesis;
end;
((
Partial_Sums s)
.
0 )
= (s
.
0 ) by
SERIES_1:def 1
.= (
0
|^ 2) by
A1
.= (((
0
* (
0
+ 1))
* ((2
*
0 )
+ 1))
/ 6) by
NEWTON: 11;
then
A3:
X[
0 ];
for n holds
X[n] from
NAT_1:sch 2(
A3,
A2);
hence thesis;
end;
theorem ::
SERIES_2:13
(for n holds (s
. n)
= (((
- 1)
|^ (n
+ 1))
* (n
|^ 2))) implies for n holds ((
Partial_Sums s)
. n)
= (((((
- 1)
|^ (n
+ 1))
* n)
* (n
+ 1))
/ 2)
proof
defpred
X[
Nat] means ((
Partial_Sums s)
. $1)
= (((((
- 1)
|^ ($1
+ 1))
* $1)
* ($1
+ 1))
/ 2);
assume
A1: for n holds (s
. n)
= (((
- 1)
|^ (n
+ 1))
* (n
|^ 2));
A2: for n st
X[n] holds
X[(n
+ 1)]
proof
let n;
assume ((
Partial_Sums s)
. n)
= (((((
- 1)
|^ (n
+ 1))
* n)
* (n
+ 1))
/ 2);
then ((
Partial_Sums s)
. (n
+ 1))
= ((((((
- 1)
|^ (n
+ 1))
* n)
* (n
+ 1))
/ 2)
+ (s
. (n
+ 1))) by
SERIES_1:def 1
.= ((((((
- 1)
|^ (n
+ 1))
* n)
* (n
+ 1))
/ 2)
+ (((
- 1)
|^ ((n
+ 1)
+ 1))
* ((n
+ 1)
|^ 2))) by
A1
.= ((((((
- 1)
|^ (n
+ 1))
* n)
* (n
+ 1))
+ ((((
- 1)
|^ ((n
+ 1)
+ 1))
* ((n
+ 1)
|^ 2))
* 2))
/ 2)
.= ((((((
- 1)
|^ (n
+ 1))
* n)
* (n
+ 1))
+ (((((
- 1)
|^ (n
+ 1))
* (
- 1))
* ((n
+ 1)
|^ 2))
* 2))
/ 2) by
NEWTON: 6
.= (((((
- 1)
|^ (n
+ 1))
* (
- 1))
* (((
- 1)
* (n
* (n
+ 1)))
+ (((n
+ 1)
|^ 2)
* 2)))
/ 2)
.= ((((
- 1)
|^ ((n
+ 1)
+ 1))
* (((
- 1)
* (n
* (n
+ 1)))
+ (((n
+ 1)
|^ 2)
* 2)))
/ 2) by
NEWTON: 6
.= ((((
- 1)
|^ (n
+ 2))
* (((((
- 1)
* n)
* n)
+ (((
- 1)
* n)
* 1))
+ ((((n
|^ 2)
+ ((2
* n)
* 1))
+ (1
|^ 2))
* 2)))
/ 2) by
Lm3
.= ((((
- 1)
|^ (n
+ 2))
* (((((
- 1)
* n)
* n)
+ (((
- 1)
* n)
* 1))
+ ((((n
|^ 2)
+ (2
* n))
+ 1)
* 2)))
/ 2)
.= ((((
- 1)
|^ (n
+ 2))
* ((((
- 1)
* (n
* n))
+ ((
- 1)
* n))
+ (((2
* (n
|^ 2))
+ ((2
* n)
* 2))
+ (1
* 2))))
/ 2)
.= ((((
- 1)
|^ (n
+ 2))
* ((((
- 1)
* ((n
|^ 1)
* n))
+ ((
- 1)
* n))
+ (((2
* (n
|^ 2))
+ ((2
* n)
* 2))
+ (1
* 2))))
/ 2)
.= ((((
- 1)
|^ (n
+ 2))
* ((((
- 1)
* (n
|^ (1
+ 1)))
+ ((
- 1)
* n))
+ (((2
* (n
|^ 2))
+ ((2
* n)
* 2))
+ (1
* 2))))
/ 2) by
NEWTON: 6
.= ((((
- 1)
|^ (n
+ 2))
* (((1
* (n
|^ 2))
+ (3
* n))
+ 2))
/ 2)
.= ((((
- 1)
|^ (n
+ 2))
* ((n
+ 1)
* (n
+ 2)))
/ 2) by
Lm10
.= (((((
- 1)
|^ (n
+ 2))
* (n
+ 1))
* (n
+ 2))
/ 2);
hence thesis;
end;
((
Partial_Sums s)
.
0 )
= (s
.
0 ) by
SERIES_1:def 1
.= (((
- 1)
|^ (
0
+ 1))
* (
0
|^ 2)) by
A1
.= (((((
- 1)
|^ (
0
+ 1))
*
0 )
* (
0
+ 1))
/ 2) by
NEWTON: 11;
then
A3:
X[
0 ];
for n holds
X[n] from
NAT_1:sch 2(
A3,
A2);
hence thesis;
end;
theorem ::
SERIES_2:14
(for n st n
>= 1 holds (s
. n)
= (((2
* n)
- 1)
|^ 2) & (s
.
0 )
=
0 ) implies for n st n
>= 1 holds ((
Partial_Sums s)
. n)
= ((n
* ((4
* (n
|^ 2))
- 1))
/ 3)
proof
defpred
X[
Nat] means ((
Partial_Sums s)
. $1)
= (($1
* ((4
* ($1
|^ 2))
- 1))
/ 3);
assume
A1: for n st n
>= 1 holds (s
. n)
= (((2
* n)
- 1)
|^ 2) & (s
.
0 )
=
0 ;
A2: for n be
Nat st n
>= 1 &
X[n] holds
X[(n
+ 1)]
proof
let n be
Nat;
assume that n
>= 1 and
A3: ((
Partial_Sums s)
. n)
= ((n
* ((4
* (n
|^ 2))
- 1))
/ 3);
A4: (n
+ 1)
>= 1 by
NAT_1: 11;
((
Partial_Sums s)
. (n
+ 1))
= (((n
* ((4
* (n
|^ 2))
- 1))
/ 3)
+ (s
. (n
+ 1))) by
A3,
SERIES_1:def 1
.= (((n
* ((4
* (n
|^ 2))
- 1))
/ 3)
+ (((2
* (n
+ 1))
- 1)
|^ 2)) by
A1,
A4
.= (((n
* ((4
* (n
|^ 2))
- 1))
+ ((((2
* n)
+ 1)
|^ 2)
* 3))
/ 3)
.= (((n
* ((4
* (n
|^ 2))
- 1))
+ (((((2
* n)
|^ 2)
+ ((2
* (2
* n))
* 1))
+ (1
|^ 2))
* 3))
/ 3) by
Lm3
.= (((((n
* 4)
* (n
|^ 2))
- (n
* 1))
+ (((((2
* n)
|^ 2)
* 3)
+ ((2
* (2
* n))
* 3))
+ ((1
|^ 2)
* 3)))
/ 3)
.= ((((n
* (4
* (n
|^ 2)))
- n)
+ (((((2
|^ 2)
* (n
|^ 2))
* 3)
+ (((2
* 2)
* n)
* 3))
+ ((1
|^ 2)
* 3)))
/ 3) by
NEWTON: 7
.= ((((n
* (4
* (n
|^ 2)))
- n)
+ (((((2
|^ 2)
* (n
|^ 2))
* 3)
+ ((4
* n)
* 3))
+ (1
* 3)))
/ 3)
.= ((((n
* (4
* (n
|^ 2)))
- n)
+ (((((2
* 2)
* (n
|^ 2))
* 3)
+ (12
* n))
+ 3))
/ 3) by
WSIERP_1: 1
.= (((((n
* (4
* (n
|^ 2)))
+ ((12
- 1)
* n))
+ (12
* (n
|^ 2)))
+ 3)
/ 3)
.= (((n
+ 1)
* ((4
* ((n
+ 1)
|^ 2))
- 1))
/ 3) by
Lm11;
hence thesis;
end;
((
Partial_Sums s)
. (
0
+ 1))
= (((
Partial_Sums s)
.
0 )
+ (s
. (
0
+ 1))) by
SERIES_1:def 1
.= ((s
.
0 )
+ (s
. 1)) by
SERIES_1:def 1
.= (
0
+ (s
. 1)) by
A1
.= (
0
+ (((2
* 1)
- 1)
|^ 2)) by
A1
.= ((1
* ((4
* (1
* 1))
- 1))
/ 3)
.= ((1
* ((4
* (1
|^ 2))
- 1))
/ 3);
then
A5:
X[1];
for n be
Nat st n
>= 1 holds
X[n] from
NAT_1:sch 8(
A5,
A2);
hence thesis;
end;
theorem ::
SERIES_2:15
(for n holds (s
. n)
= (n
|^ 3)) implies for n holds ((
Partial_Sums s)
. n)
= (((n
|^ 2)
* ((n
+ 1)
|^ 2))
/ 4)
proof
defpred
X[
Nat] means ((
Partial_Sums s)
. $1)
= ((($1
|^ 2)
* (($1
+ 1)
|^ 2))
/ 4);
assume
A1: for n holds (s
. n)
= (n
|^ 3);
A2: for n st
X[n] holds
X[(n
+ 1)]
proof
let n;
assume ((
Partial_Sums s)
. n)
= (((n
|^ 2)
* ((n
+ 1)
|^ 2))
/ 4);
then ((
Partial_Sums s)
. (n
+ 1))
= ((((n
|^ 2)
* ((n
+ 1)
|^ 2))
/ 4)
+ (s
. (n
+ 1))) by
SERIES_1:def 1
.= ((((n
|^ 2)
* ((n
+ 1)
|^ 2))
/ 4)
+ ((n
+ 1)
|^ 3)) by
A1
.= ((((n
|^ 2)
* ((n
+ 1)
|^ 2))
+ (((n
+ 1)
|^ 3)
* 4))
/ 4)
.= ((((n
|^ 2)
* ((n
+ 1)
|^ 2))
+ ((((n
+ 1)
|^ 2)
* (n
+ 1))
* 4))
/ 4) by
Lm2
.= ((((n
+ 1)
|^ 2)
* ((n
|^ 2)
+ (((2
* 2)
* n)
+ 4)))
/ 4)
.= ((((n
+ 1)
|^ 2)
* ((n
+ 2)
|^ 2))
/ 4) by
Lm3;
hence thesis;
end;
((
Partial_Sums s)
.
0 )
= (s
.
0 ) by
SERIES_1:def 1
.= (
0
|^ 3) by
A1
.= ((
0
* ((
0
+ 1)
|^ 2))
/ 4) by
NEWTON: 11
.= (((
0
|^ 2)
* ((
0
+ 1)
|^ 2))
/ 4) by
NEWTON: 11;
then
A3:
X[
0 ];
for n holds
X[n] from
NAT_1:sch 2(
A3,
A2);
hence thesis;
end;
theorem ::
SERIES_2:16
(for n st n
>= 1 holds (s
. n)
= (((2
* n)
- 1)
|^ 3) & (s
.
0 )
=
0 ) implies for n st n
>= 1 holds ((
Partial_Sums s)
. n)
= ((n
|^ 2)
* ((2
* (n
|^ 2))
- 1))
proof
defpred
X[
Nat] means ((
Partial_Sums s)
. $1)
= (($1
|^ 2)
* ((2
* ($1
|^ 2))
- 1));
assume
A1: for n st n
>= 1 holds (s
. n)
= (((2
* n)
- 1)
|^ 3) & (s
.
0 )
=
0 ;
A2: for n be
Nat st n
>= 1 &
X[n] holds
X[(n
+ 1)]
proof
let n be
Nat;
assume that n
>= 1 and
A3: ((
Partial_Sums s)
. n)
= ((n
|^ 2)
* ((2
* (n
|^ 2))
- 1));
A4: (n
+ 1)
>= 1 by
NAT_1: 11;
((
Partial_Sums s)
. (n
+ 1))
= (((n
|^ 2)
* ((2
* (n
|^ 2))
- 1))
+ (s
. (n
+ 1))) by
A3,
SERIES_1:def 1
.= (((n
|^ 2)
* ((2
* (n
|^ 2))
- 1))
+ (((2
* (n
+ 1))
- 1)
|^ 3)) by
A1,
A4
.= (((n
|^ 2)
* ((2
* (n
|^ 2))
- 1))
+ (((2
* n)
+ 1)
|^ 3))
.= (((n
|^ 2)
* ((2
* (n
|^ 2))
- 1))
+ (((((2
* n)
|^ 3)
+ (3
* ((2
* n)
|^ 2)))
+ (3
* (2
* n)))
+ 1)) by
Lm4
.= ((((((((n
|^ 2)
* 2)
* (n
|^ 2))
- (n
|^ 2))
+ ((2
* n)
|^ 3))
+ (3
* ((2
* n)
|^ 2)))
+ ((3
* 2)
* n))
+ 1)
.= ((((((((n
|^ 2)
* 2)
* (n
|^ 2))
- (n
|^ 2))
+ ((2
* n)
|^ 3))
+ (3
* ((2
|^ 2)
* (n
|^ 2))))
+ (6
* n))
+ 1) by
NEWTON: 7
.= ((((((((n
|^ 2)
* 2)
* (n
|^ 2))
- (n
|^ 2))
+ ((2
|^ 3)
* (n
|^ 3)))
+ (3
* ((2
|^ 2)
* (n
|^ 2))))
+ (6
* n))
+ 1) by
NEWTON: 7
.= ((((((((n
|^ 2)
* 2)
* (n
|^ 2))
- (n
|^ 2))
+ ((2
|^ 3)
* (n
|^ 3)))
+ (3
* ((2
* 2)
* (n
|^ 2))))
+ (6
* n))
+ 1) by
WSIERP_1: 1
.= ((((((((n
|^ 2)
* 2)
* (n
|^ 2))
- (n
|^ 2))
+ (((2
* 2)
* 2)
* (n
|^ 3)))
+ (3
* ((2
* 2)
* (n
|^ 2))))
+ (6
* n))
+ 1) by
Lm1
.= (((((((n
|^ 2)
* (n
|^ 2))
* 2)
+ ((12
- 1)
* (n
|^ 2)))
+ (8
* (n
|^ 3)))
+ (6
* n))
+ 1)
.= (((n
+ 1)
|^ 2)
* ((2
* ((n
+ 1)
|^ 2))
- 1)) by
Lm12;
hence thesis;
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
.= ((s
. 1)
+
0 ) by
A1
.= (((2
* 1)
- 1)
|^ 3) by
A1
.= (1
|^ (2
+ 1))
.= ((1
|^ 2)
* ((2
* (1
* 1))
- 1))
.= ((1
|^ 2)
* ((2
* (1
|^ 2))
- 1));
then
A5:
X[1];
for n be
Nat st n
>= 1 holds
X[n] from
NAT_1:sch 8(
A5,
A2);
hence thesis;
end;
theorem ::
SERIES_2:17
(for n holds (s
. n)
= (n
|^ 4)) implies for n holds ((
Partial_Sums s)
. n)
= ((((n
* (n
+ 1))
* ((2
* n)
+ 1))
* (((3
* (n
|^ 2))
+ (3
* n))
- 1))
/ 30)
proof
defpred
X[
Nat] means ((
Partial_Sums s)
. $1)
= (((($1
* ($1
+ 1))
* ((2
* $1)
+ 1))
* (((3
* ($1
|^ 2))
+ (3
* $1))
- 1))
/ 30);
assume
A1: for n holds (s
. n)
= (n
|^ 4);
A2: for n st
X[n] holds
X[(n
+ 1)]
proof
let n;
assume ((
Partial_Sums s)
. n)
= ((((n
* (n
+ 1))
* ((2
* n)
+ 1))
* (((3
* (n
|^ 2))
+ (3
* n))
- 1))
/ 30);
then ((
Partial_Sums s)
. (n
+ 1))
= (((((n
* (n
+ 1))
* ((2
* n)
+ 1))
* (((3
* (n
|^ 2))
+ (3
* n))
- 1))
/ 30)
+ (s
. (n
+ 1))) by
SERIES_1:def 1
.= (((((n
* (n
+ 1))
* ((2
* n)
+ 1))
* (((3
* (n
|^ 2))
+ (3
* n))
- 1))
/ 30)
+ ((n
+ 1)
|^ 4)) by
A1
.= (((((n
* (n
+ 1))
* ((2
* n)
+ 1))
* (((3
* (n
|^ 2))
+ (3
* n))
- 1))
+ (((n
+ 1)
|^ (3
+ 1))
* 30))
/ 30)
.= (((((n
* (n
+ 1))
* ((2
* n)
+ 1))
* (((3
* (n
|^ 2))
+ (3
* n))
- 1))
+ ((((n
+ 1)
|^ 3)
* (n
+ 1))
* 30))
/ 30) by
NEWTON: 6
.= (((n
+ 1)
* (((n
* ((2
* n)
+ 1))
* (((3
* (n
|^ 2))
+ (3
* n))
- 1))
+ (((n
+ 1)
|^ 3)
* 30)))
/ 30)
.= (((n
+ 1)
* (((n
+ 2)
* ((2
* (n
+ 1))
+ 1))
* (((3
* ((n
+ 1)
|^ 2))
+ (3
* (n
+ 1)))
- 1)))
/ 30) by
Lm5;
hence thesis;
end;
((
Partial_Sums s)
.
0 )
= (s
.
0 ) by
SERIES_1:def 1
.= (
0
|^ 4) by
A1
.= ((((
0
* (
0
+ 1))
* ((2
*
0 )
+ 1))
* (((3
* (
0
|^ 2))
+ (3
*
0 ))
- 1))
/ 30) by
NEWTON: 11;
then
A3:
X[
0 ];
for n holds
X[n] from
NAT_1:sch 2(
A3,
A2);
hence thesis;
end;
theorem ::
SERIES_2:18
(for n holds (s
. n)
= (((
- 1)
|^ (n
+ 1))
* (n
|^ 4))) implies for n holds ((
Partial_Sums s)
. n)
= ((((((
- 1)
|^ (n
+ 1))
* n)
* (n
+ 1))
* (((n
|^ 2)
+ n)
- 1))
/ 2)
proof
defpred
X[
Nat] means ((
Partial_Sums s)
. $1)
= ((((((
- 1)
|^ ($1
+ 1))
* $1)
* ($1
+ 1))
* ((($1
|^ 2)
+ $1)
- 1))
/ 2);
assume
A1: for n holds (s
. n)
= (((
- 1)
|^ (n
+ 1))
* (n
|^ 4));
A2: for n st
X[n] holds
X[(n
+ 1)]
proof
let n;
assume ((
Partial_Sums s)
. n)
= ((((((
- 1)
|^ (n
+ 1))
* n)
* (n
+ 1))
* (((n
|^ 2)
+ n)
- 1))
/ 2);
then ((
Partial_Sums s)
. (n
+ 1))
= (((((((
- 1)
|^ (n
+ 1))
* n)
* (n
+ 1))
* (((n
|^ 2)
+ n)
- 1))
/ 2)
+ (s
. (n
+ 1))) by
SERIES_1:def 1
.= (((((((
- 1)
|^ (n
+ 1))
* n)
* (n
+ 1))
* (((n
|^ 2)
+ n)
- 1))
/ 2)
+ (((
- 1)
|^ ((n
+ 1)
+ 1))
* ((n
+ 1)
|^ 4))) by
A1
.= (((((((((
- 1)
|^ (n
+ 1))
* (
- 1))
* (
- 1))
* n)
* (n
+ 1))
* (((n
|^ 2)
+ n)
- 1))
+ ((((
- 1)
|^ (n
+ 2))
* ((n
+ 1)
|^ 4))
* 2))
/ 2)
.= ((((((((
- 1)
|^ ((n
+ 1)
+ 1))
* (
- 1))
* n)
* (n
+ 1))
* (((n
|^ 2)
+ n)
- 1))
+ ((((
- 1)
|^ (n
+ 2))
* ((n
+ 1)
|^ 4))
* 2))
/ 2) by
NEWTON: 6
.= ((((
- 1)
|^ (n
+ 2))
* (((((
- 1)
* n)
* (n
+ 1))
* (((n
|^ 2)
+ n)
- 1))
+ (((n
+ 1)
|^ (3
+ 1))
* 2)))
/ 2)
.= ((((
- 1)
|^ (n
+ 2))
* (((((
- 1)
* n)
* (n
+ 1))
* (((n
|^ 2)
+ n)
- 1))
+ ((((n
+ 1)
|^ 3)
* (n
+ 1))
* 2)))
/ 2) by
NEWTON: 6
.= (((((
- 1)
|^ (n
+ 2))
* (n
+ 1))
* (((
- 1)
* (((n
* (n
|^ 2))
+ (n
* n))
- (n
* 1)))
+ (((n
+ 1)
|^ 3)
* 2)))
/ 2)
.= (((((
- 1)
|^ (n
+ 2))
* (n
+ 1))
* (((
- 1)
* (((n
|^ (2
+ 1))
+ (n
* n))
- (n
* 1)))
+ (((n
+ 1)
|^ 3)
* 2)))
/ 2) by
NEWTON: 6
.= (((((
- 1)
|^ (n
+ 2))
* (n
+ 1))
* (((
- 1)
* (((n
|^ 3)
+ (n
|^ 2))
- n))
+ (((n
+ 1)
|^ 3)
* 2)))
/ 2) by
WSIERP_1: 1
.= (((((
- 1)
|^ (n
+ 2))
* (n
+ 1))
* (((
- 1)
* (((n
|^ 3)
+ (n
|^ 2))
- n))
+ (((((n
|^ 3)
+ (3
* (n
|^ 2)))
+ (3
* n))
+ 1)
* 2)))
/ 2) by
Lm4
.= (((((
- 1)
|^ (n
+ 2))
* (n
+ 1))
* ((((n
|^ 3)
+ (5
* (n
|^ 2)))
+ (7
* n))
+ 2))
/ 2)
.= (((((
- 1)
|^ (n
+ 2))
* (n
+ 1))
* ((n
+ 2)
* ((((n
+ 1)
|^ 2)
+ (n
+ 1))
- 1)))
/ 2) by
Lm13
.= ((((((
- 1)
|^ (n
+ 2))
* (n
+ 1))
* (n
+ 2))
* ((((n
+ 1)
|^ 2)
+ (n
+ 1))
- 1))
/ 2);
hence thesis;
end;
((
Partial_Sums s)
.
0 )
= (s
.
0 ) by
SERIES_1:def 1
.= (((
- 1)
|^ (
0
+ 1))
* (
0
|^ 4)) by
A1
.= ((((((
- 1)
|^ (
0
+ 1))
*
0 )
* (
0
+ 1))
* (((
0
|^ 2)
+
0 )
- 1))
/ 2) by
NEWTON: 11;
then
A3:
X[
0 ];
for n holds
X[n] from
NAT_1:sch 2(
A3,
A2);
hence thesis;
end;
Lm15: (((n
|^ 2)
* (((2
* (n
|^ 2))
+ (2
* n))
- 1))
+ (((n
+ 1)
|^ 3)
* 12))
= (((n
+ 2)
|^ 2)
* (((2
* ((n
+ 1)
|^ 2))
+ (2
* (n
+ 1)))
- 1))
proof
A1: (((n
|^ 2)
* (((2
* (n
|^ 2))
+ (2
* n))
- 1))
+ (((n
+ 1)
|^ 3)
* 12))
= ((((2
* ((n
|^ 2)
* (n
|^ 2)))
+ (2
* (n
* (n
|^ 2))))
- (n
|^ 2))
+ (((n
+ 1)
|^ 3)
* 12))
.= ((((2
* (n
|^ (2
+ 2)))
+ (2
* (n
* (n
|^ 2))))
- (n
|^ 2))
+ (((n
+ 1)
|^ 3)
* 12)) by
NEWTON: 8
.= ((((2
* (n
|^ (2
+ 2)))
+ (2
* (n
|^ (2
+ 1))))
- (n
|^ 2))
+ (((n
+ 1)
|^ 3)
* 12)) by
NEWTON: 6
.= ((((2
* (n
|^ 4))
+ (2
* (n
|^ 3)))
- (n
|^ 2))
+ (((((n
|^ 3)
+ (3
* (n
|^ 2)))
+ (3
* n))
+ 1)
* 12)) by
Lm4
.= (((((((2
* (n
|^ 4))
+ (2
* (n
|^ 3)))
- (n
|^ 2))
+ ((n
|^ 3)
* 12))
+ (36
* (n
|^ 2)))
+ (36
* n))
+ 12);
(((n
+ 2)
|^ 2)
* (((2
* ((n
+ 1)
|^ 2))
+ (2
* (n
+ 1)))
- 1))
= (((n
+ 2)
|^ 2)
* (((2
* (((n
|^ 2)
+ ((2
* n)
* 1))
+ (1
|^ 2)))
+ (2
* (n
+ 1)))
- 1)) by
Lm3
.= ((((n
|^ 2)
+ ((2
* n)
* 2))
+ (2
|^ 2))
* (((((2
* (n
|^ 2))
+ ((2
* n)
* 2))
+ (2
* (1
|^ 2)))
+ ((2
* n)
+ (2
* 1)))
- 1)) by
Lm3
.= ((((n
|^ 2)
+ ((2
* n)
* 2))
+ (2
|^ 2))
* (((((2
* (n
|^ 2))
+ (4
* n))
+ (2
* 1))
+ ((2
* n)
+ 2))
- 1))
.= ((((n
|^ 2)
+ (4
* n))
+ (2
* 2))
* ((((((2
* (n
|^ 2))
+ (4
* n))
+ 2)
+ (2
* n))
+ 2)
- 1)) by
WSIERP_1: 1
.= (((((2
* ((n
|^ 2)
* (n
|^ 2)))
+ (6
* (n
* (n
|^ 2))))
+ ((n
|^ 2)
* 3))
+ ((4
* n)
* (((2
* (n
|^ 2))
+ (6
* n))
+ 3)))
+ ((((2
* (n
|^ 2))
* 4)
+ (24
* n))
+ 12))
.= (((((2
* (n
|^ (2
+ 2)))
+ (6
* (n
* (n
|^ 2))))
+ ((n
|^ 2)
* 3))
+ ((4
* n)
* (((2
* (n
|^ 2))
+ (6
* n))
+ 3)))
+ ((((2
* (n
|^ 2))
* 4)
+ (24
* n))
+ 12)) by
NEWTON: 8
.= (((((2
* (n
|^ (2
+ 2)))
+ (6
* (n
|^ (2
+ 1))))
+ ((n
|^ 2)
* 3))
+ ((4
* n)
* (((2
* (n
|^ 2))
+ (6
* n))
+ 3)))
+ ((((2
* (n
|^ 2))
* 4)
+ (24
* n))
+ 12)) by
NEWTON: 6
.= (((((2
* (n
|^ 4))
+ (6
* (n
|^ 3)))
+ ((n
|^ 2)
* 3))
+ ((((4
* (n
* (n
|^ 2)))
* 2)
+ ((4
* (n
* n))
* 6))
+ ((4
* n)
* 3)))
+ (((8
* (n
|^ 2))
+ (24
* n))
+ 12))
.= (((((2
* (n
|^ 4))
+ (6
* (n
|^ 3)))
+ ((n
|^ 2)
* 3))
+ ((((4
* (n
|^ (2
+ 1)))
* 2)
+ (24
* (n
* n)))
+ ((4
* n)
* 3)))
+ (((8
* (n
|^ 2))
+ (24
* n))
+ 12)) by
NEWTON: 6
.= (((((2
* (n
|^ 4))
+ (6
* (n
|^ 3)))
+ ((n
|^ 2)
* 3))
+ ((((4
* (n
|^ 3))
* 2)
+ (24
* (n
|^ 2)))
+ (12
* n)))
+ (((8
* (n
|^ 2))
+ (24
* n))
+ 12)) by
WSIERP_1: 1
.= (((((((2
* (n
|^ 4))
+ (14
* (n
|^ 3)))
+ (27
* (n
|^ 2)))
+ (12
* n))
+ (8
* (n
|^ 2)))
+ (24
* n))
+ 12);
hence thesis by
A1;
end;
theorem ::
SERIES_2:19
(for n holds (s
. n)
= (n
|^ 5)) implies for n holds ((
Partial_Sums s)
. n)
= ((((n
|^ 2)
* ((n
+ 1)
|^ 2))
* (((2
* (n
|^ 2))
+ (2
* n))
- 1))
/ 12)
proof
defpred
X[
Nat] means ((
Partial_Sums s)
. $1)
= (((($1
|^ 2)
* (($1
+ 1)
|^ 2))
* (((2
* ($1
|^ 2))
+ (2
* $1))
- 1))
/ 12);
assume
A1: for n holds (s
. n)
= (n
|^ 5);
A2: for n st
X[n] holds
X[(n
+ 1)]
proof
let n;
assume ((
Partial_Sums s)
. n)
= ((((n
|^ 2)
* ((n
+ 1)
|^ 2))
* (((2
* (n
|^ 2))
+ (2
* n))
- 1))
/ 12);
then ((
Partial_Sums s)
. (n
+ 1))
= (((((n
|^ 2)
* ((n
+ 1)
|^ 2))
* (((2
* (n
|^ 2))
+ (2
* n))
- 1))
/ 12)
+ (s
. (n
+ 1))) by
SERIES_1:def 1
.= (((((n
|^ 2)
* ((n
+ 1)
|^ 2))
* (((2
* (n
|^ 2))
+ (2
* n))
- 1))
/ 12)
+ ((n
+ 1)
|^ 5)) by
A1
.= (((((n
|^ 2)
* ((n
+ 1)
|^ 2))
* (((2
* (n
|^ 2))
+ (2
* n))
- 1))
+ (((n
+ 1)
|^ (3
+ 2))
* 12))
/ 12)
.= (((((n
|^ 2)
* ((n
+ 1)
|^ 2))
* (((2
* (n
|^ 2))
+ (2
* n))
- 1))
+ ((((n
+ 1)
|^ 3)
* ((n
+ 1)
|^ 2))
* 12))
/ 12) by
NEWTON: 8
.= ((((n
+ 1)
|^ 2)
* (((n
|^ 2)
* (((2
* (n
|^ 2))
+ (2
* n))
- 1))
+ (((n
+ 1)
|^ 3)
* 12)))
/ 12)
.= ((((n
+ 1)
|^ 2)
* (((n
+ 2)
|^ 2)
* (((2
* ((n
+ 1)
|^ 2))
+ (2
* (n
+ 1)))
- 1)))
/ 12) by
Lm15
.= (((((n
+ 1)
|^ 2)
* ((n
+ 2)
|^ 2))
* (((2
* ((n
+ 1)
|^ 2))
+ (2
* (n
+ 1)))
- 1))
/ 12);
hence thesis;
end;
((
Partial_Sums s)
.
0 )
= (s
.
0 ) by
SERIES_1:def 1
.= (
0
|^ 5) by
A1
.= (((
0
* ((
0
+ 1)
|^ 2))
* (((2
* (
0
|^ 2))
+ (2
*
0 ))
- 1))
/ 12) by
NEWTON: 11
.= ((((
0
|^ 2)
* ((
0
+ 1)
|^ 2))
* (((2
* (
0
|^ 2))
+ (2
*
0 ))
- 1))
/ 12) by
NEWTON: 11;
then
A3:
X[
0 ];
for n holds
X[n] from
NAT_1:sch 2(
A3,
A2);
hence thesis;
end;
Lm16: (((n
+ 2)
* ((2
* (n
+ 1))
+ 1))
* ((((3
* ((n
+ 1)
|^ 4))
+ (6
* ((n
+ 1)
|^ 3)))
- (3
* (n
+ 1)))
+ 1))
= (((((((6
* (n
|^ 6))
+ (57
* (n
|^ 5)))
+ (216
* (n
|^ 4)))
+ (414
* (n
|^ 3)))
+ (419
* (n
|^ 2)))
+ (211
* n))
+ 42)
proof
(((n
+ 2)
* ((2
* (n
+ 1))
+ 1))
* ((((3
* ((n
+ 1)
|^ 4))
+ (6
* ((n
+ 1)
|^ 3)))
- (3
* (n
+ 1)))
+ 1))
= (((n
+ 2)
* ((2
* n)
+ 3))
* ((((3
* ((n
+ 1)
|^ 4))
+ (6
* ((n
+ 1)
|^ 3)))
- (3
* n))
- 2))
.= (((n
+ 2)
* ((2
* n)
+ 3))
* ((((3
* (((((n
|^ 4)
+ (4
* (n
|^ 3)))
+ (6
* (n
|^ 2)))
+ (4
* n))
+ 1))
+ (6
* ((n
+ 1)
|^ 3)))
- (3
* n))
- 2)) by
Lm6
.= (((n
+ 2)
* ((2
* n)
+ 3))
* ((((((((3
* (n
|^ 4))
+ (12
* (n
|^ 3)))
+ (18
* (n
|^ 2)))
+ (12
* n))
+ 3)
+ (6
* ((((n
|^ 3)
+ (3
* (n
|^ 2)))
+ (3
* n))
+ 1)))
- (3
* n))
- 2)) by
Lm4
.= ((((2
* (n
* n))
+ (3
* n))
+ ((4
* n)
+ 6))
* (((((3
* (n
|^ 4))
+ (18
* (n
|^ 3)))
+ (36
* (n
|^ 2)))
+ (27
* n))
+ 7))
.= ((((2
* (n
|^ 2))
+ (3
* n))
+ ((4
* n)
+ 6))
* (((((3
* (n
|^ 4))
+ (18
* (n
|^ 3)))
+ (36
* (n
|^ 2)))
+ (27
* n))
+ 7)) by
WSIERP_1: 1
.= ((((((3
* (n
|^ 4))
* (((2
* (n
|^ 2))
+ (7
* n))
+ 6))
+ ((18
* (n
|^ 3))
* (((2
* (n
|^ 2))
+ (7
* n))
+ 6)))
+ ((36
* (n
|^ 2))
* (((2
* (n
|^ 2))
+ (7
* n))
+ 6)))
+ ((((27
* (n
* (n
|^ 2)))
* 2)
+ ((27
* (n
* n))
* 7))
+ (162
* n)))
+ (((14
* (n
|^ 2))
+ (49
* n))
+ 42))
.= ((((((3
* (n
|^ 4))
* (((2
* (n
|^ 2))
+ (7
* n))
+ 6))
+ ((18
* (n
|^ 3))
* (((2
* (n
|^ 2))
+ (7
* n))
+ 6)))
+ ((36
* (n
|^ 2))
* (((2
* (n
|^ 2))
+ (7
* n))
+ 6)))
+ ((((27
* (n
|^ (2
+ 1)))
* 2)
+ ((27
* (n
* n))
* 7))
+ (162
* n)))
+ (((14
* (n
|^ 2))
+ (49
* n))
+ 42)) by
NEWTON: 6
.= ((((((3
* (n
|^ 4))
* (((2
* (n
|^ 2))
+ (7
* n))
+ 6))
+ ((18
* (n
|^ 3))
* (((2
* (n
|^ 2))
+ (7
* n))
+ 6)))
+ ((36
* (n
|^ 2))
* (((2
* (n
|^ 2))
+ (7
* n))
+ 6)))
+ (((54
* (n
|^ 3))
+ ((27
* (n
|^ 2))
* 7))
+ (162
* n)))
+ (((14
* (n
|^ 2))
+ (49
* n))
+ 42)) by
WSIERP_1: 1
.= (((((((3
* ((n
|^ 4)
* (n
|^ 2)))
* 2)
+ ((3
* ((n
|^ 4)
* n))
* 7))
+ (18
* (n
|^ 4)))
+ ((((18
* ((n
|^ 3)
* (n
|^ 2)))
* 2)
+ ((18
* ((n
|^ 3)
* n))
* 7))
+ (108
* (n
|^ 3))))
+ ((36
* (n
|^ 2))
* (((2
* (n
|^ 2))
+ (7
* n))
+ 6)))
+ ((((54
* (n
|^ 3))
+ (203
* (n
|^ 2)))
+ (211
* n))
+ 42))
.= (((((((3
* (n
|^ (4
+ 2)))
* 2)
+ ((3
* ((n
|^ 4)
* n))
* 7))
+ (18
* (n
|^ 4)))
+ ((((18
* ((n
|^ 3)
* (n
|^ 2)))
* 2)
+ ((18
* ((n
|^ 3)
* n))
* 7))
+ (108
* (n
|^ 3))))
+ ((36
* (n
|^ 2))
* (((2
* (n
|^ 2))
+ (7
* n))
+ 6)))
+ ((((54
* (n
|^ 3))
+ (203
* (n
|^ 2)))
+ (211
* n))
+ 42)) by
NEWTON: 8
.= ((((((6
* (n
|^ (4
+ 2)))
+ ((3
* (n
|^ (4
+ 1)))
* 7))
+ (18
* (n
|^ 4)))
+ (((36
* ((n
|^ 3)
* (n
|^ 2)))
+ (126
* ((n
|^ 3)
* n)))
+ (108
* (n
|^ 3))))
+ ((36
* (n
|^ 2))
* (((2
* (n
|^ 2))
+ (7
* n))
+ 6)))
+ ((((54
* (n
|^ 3))
+ (203
* (n
|^ 2)))
+ (211
* n))
+ 42)) by
NEWTON: 6
.= ((((((6
* (n
|^ (4
+ 2)))
+ (21
* (n
|^ (4
+ 1))))
+ (18
* (n
|^ 4)))
+ (((36
* ((n
|^ 3)
* (n
|^ 2)))
+ (126
* (n
|^ (3
+ 1))))
+ (108
* (n
|^ 3))))
+ ((36
* (n
|^ 2))
* (((2
* (n
|^ 2))
+ (7
* n))
+ 6)))
+ ((((54
* (n
|^ 3))
+ (203
* (n
|^ 2)))
+ (211
* n))
+ 42)) by
NEWTON: 6
.= ((((((6
* (n
|^ (4
+ 2)))
+ (21
* (n
|^ (4
+ 1))))
+ (18
* (n
|^ 4)))
+ (((36
* (n
|^ (3
+ 2)))
+ (126
* (n
|^ (3
+ 1))))
+ (108
* (n
|^ 3))))
+ ((36
* (n
|^ 2))
* (((2
* (n
|^ 2))
+ (7
* n))
+ 6)))
+ ((((54
* (n
|^ 3))
+ (203
* (n
|^ 2)))
+ (211
* n))
+ 42)) by
NEWTON: 8
.= ((((((6
* (n
|^ 6))
+ (21
* (n
|^ 5)))
+ (18
* (n
|^ 4)))
+ (((36
* (n
|^ 5))
+ (126
* (n
|^ 4)))
+ (108
* (n
|^ 3))))
+ ((((36
* ((n
|^ 2)
* (n
|^ 2)))
* 2)
+ ((36
* ((n
|^ 2)
* n))
* 7))
+ (216
* (n
|^ 2))))
+ ((((54
* (n
|^ 3))
+ (203
* (n
|^ 2)))
+ (211
* n))
+ 42))
.= ((((((6
* (n
|^ 6))
+ (21
* (n
|^ 5)))
+ (18
* (n
|^ 4)))
+ (((36
* (n
|^ 5))
+ (126
* (n
|^ 4)))
+ (108
* (n
|^ 3))))
+ ((((36
* (n
|^ (2
+ 2)))
* 2)
+ (252
* ((n
|^ 2)
* n)))
+ (216
* (n
|^ 2))))
+ ((((54
* (n
|^ 3))
+ (203
* (n
|^ 2)))
+ (211
* n))
+ 42)) by
NEWTON: 8
.= ((((((6
* (n
|^ 6))
+ (21
* (n
|^ 5)))
+ (18
* (n
|^ 4)))
+ (((36
* (n
|^ 5))
+ (126
* (n
|^ 4)))
+ (108
* (n
|^ 3))))
+ (((72
* (n
|^ (2
+ 2)))
+ (252
* (n
|^ (2
+ 1))))
+ (216
* (n
|^ 2))))
+ ((((54
* (n
|^ 3))
+ (203
* (n
|^ 2)))
+ (211
* n))
+ 42)) by
NEWTON: 6
.= ((((((6
* (n
|^ 6))
+ (21
* (n
|^ 5)))
+ (18
* (n
|^ 4)))
+ (((36
* (n
|^ 5))
+ (126
* (n
|^ 4)))
+ (108
* (n
|^ 3))))
+ (((72
* (n
|^ 4))
+ (252
* (n
|^ 3)))
+ (216
* (n
|^ 2))))
+ ((((54
* (n
|^ 3))
+ (203
* (n
|^ 2)))
+ (211
* n))
+ 42));
hence thesis;
end;
theorem ::
SERIES_2:20
(for n holds (s
. n)
= (n
|^ 6)) implies for n holds ((
Partial_Sums s)
. n)
= ((((n
* (n
+ 1))
* ((2
* n)
+ 1))
* ((((3
* (n
|^ 4))
+ (6
* (n
|^ 3)))
- (3
* n))
+ 1))
/ 42)
proof
defpred
X[
Nat] means ((
Partial_Sums s)
. $1)
= (((($1
* ($1
+ 1))
* ((2
* $1)
+ 1))
* ((((3
* ($1
|^ 4))
+ (6
* ($1
|^ 3)))
- (3
* $1))
+ 1))
/ 42);
assume
A1: for n holds (s
. n)
= (n
|^ 6);
A2: for n st
X[n] holds
X[(n
+ 1)]
proof
let n;
assume ((
Partial_Sums s)
. n)
= ((((n
* (n
+ 1))
* ((2
* n)
+ 1))
* ((((3
* (n
|^ 4))
+ (6
* (n
|^ 3)))
- (3
* n))
+ 1))
/ 42);
then ((
Partial_Sums s)
. (n
+ 1))
= (((((n
* (n
+ 1))
* ((2
* n)
+ 1))
* ((((3
* (n
|^ 4))
+ (6
* (n
|^ 3)))
- (3
* n))
+ 1))
/ 42)
+ (s
. (n
+ 1))) by
SERIES_1:def 1
.= (((((n
* (n
+ 1))
* ((2
* n)
+ 1))
* ((((3
* (n
|^ 4))
+ (6
* (n
|^ 3)))
- (3
* n))
+ 1))
/ 42)
+ ((n
+ 1)
|^ 6)) by
A1
.= (((((n
* (n
+ 1))
* ((2
* n)
+ 1))
* ((((3
* (n
|^ 4))
+ (6
* (n
|^ 3)))
- (3
* n))
+ 1))
+ (((n
+ 1)
|^ (5
+ 1))
* 42))
/ 42)
.= (((((n
* (n
+ 1))
* ((2
* n)
+ 1))
* ((((3
* (n
|^ 4))
+ (6
* (n
|^ 3)))
- (3
* n))
+ 1))
+ ((((n
+ 1)
|^ 5)
* (n
+ 1))
* 42))
/ 42) by
NEWTON: 6
.= (((n
+ 1)
* ((((2
* (n
* n))
+ n)
* ((((3
* (n
|^ 4))
+ (6
* (n
|^ 3)))
- (3
* n))
+ 1))
+ (((n
+ 1)
|^ 5)
* 42)))
/ 42)
.= (((n
+ 1)
* ((((2
* (n
|^ 2))
+ n)
* ((((3
* (n
|^ 4))
+ (6
* (n
|^ 3)))
- (3
* n))
+ 1))
+ (((n
+ 1)
|^ 5)
* 42)))
/ 42) by
WSIERP_1: 1
.= (((n
+ 1)
* (((((((3
* ((n
|^ 4)
* (n
|^ 2)))
* 2)
+ (3
* ((n
|^ 4)
* n)))
+ (((6
* ((n
|^ 3)
* (n
|^ 2)))
* 2)
+ (6
* ((n
|^ 3)
* n))))
- (((3
* (n
* (n
|^ 2)))
* 2)
+ (3
* (n
* n))))
+ ((2
* (n
|^ 2))
+ n))
+ (((n
+ 1)
|^ 5)
* 42)))
/ 42)
.= (((n
+ 1)
* (((((((3
* (n
|^ (4
+ 2)))
* 2)
+ (3
* ((n
|^ 4)
* n)))
+ (((6
* ((n
|^ 3)
* (n
|^ 2)))
* 2)
+ (6
* ((n
|^ 3)
* n))))
- (((3
* (n
* (n
|^ 2)))
* 2)
+ (3
* (n
* n))))
+ ((2
* (n
|^ 2))
+ n))
+ (((n
+ 1)
|^ 5)
* 42)))
/ 42) by
NEWTON: 8
.= (((n
+ 1)
* (((((((3
* (n
|^ (4
+ 2)))
* 2)
+ (3
* ((n
|^ 4)
* n)))
+ (((6
* (n
|^ (3
+ 2)))
* 2)
+ (6
* ((n
|^ 3)
* n))))
- (((3
* (n
* (n
|^ 2)))
* 2)
+ (3
* (n
* n))))
+ ((2
* (n
|^ 2))
+ n))
+ (((n
+ 1)
|^ 5)
* 42)))
/ 42) by
NEWTON: 8
.= (((n
+ 1)
* (((((((3
* (n
|^ (4
+ 2)))
* 2)
+ (3
* (n
|^ (4
+ 1))))
+ (((6
* (n
|^ (3
+ 2)))
* 2)
+ (6
* ((n
|^ 3)
* n))))
- (((3
* (n
* (n
|^ 2)))
* 2)
+ (3
* (n
* n))))
+ ((2
* (n
|^ 2))
+ n))
+ (((n
+ 1)
|^ 5)
* 42)))
/ 42) by
NEWTON: 6
.= (((n
+ 1)
* (((((((3
* (n
|^ (4
+ 2)))
* 2)
+ (3
* (n
|^ (4
+ 1))))
+ (((6
* (n
|^ (3
+ 2)))
* 2)
+ (6
* ((n
|^ 3)
* n))))
- (((3
* (n
|^ (2
+ 1)))
* 2)
+ (3
* (n
* n))))
+ ((2
* (n
|^ 2))
+ n))
+ (((n
+ 1)
|^ 5)
* 42)))
/ 42) by
NEWTON: 6
.= (((n
+ 1)
* (((((((3
* (n
|^ 6))
* 2)
+ (3
* (n
|^ 5)))
+ (((6
* (n
|^ 5))
* 2)
+ (6
* ((n
|^ 3)
* n))))
- (((3
* (n
|^ 3))
* 2)
+ (3
* (n
|^ 2))))
+ ((2
* (n
|^ 2))
+ n))
+ (((n
+ 1)
|^ 5)
* 42)))
/ 42) by
WSIERP_1: 1
.= (((n
+ 1)
* ((((((6
* (n
|^ 6))
+ (3
* (n
|^ 5)))
+ ((12
* (n
|^ 5))
+ (6
* (n
|^ (3
+ 1)))))
- ((6
* (n
|^ 3))
+ (3
* (n
|^ 2))))
+ ((2
* (n
|^ 2))
+ n))
+ (((n
+ 1)
|^ 5)
* 42)))
/ 42) by
NEWTON: 6
.= (((n
+ 1)
* (((((((6
* (n
|^ 6))
+ (6
* (n
|^ 4)))
+ (15
* (n
|^ 5)))
- (6
* (n
|^ 3)))
- (1
* (n
|^ 2)))
+ n)
+ (((((((n
|^ 5)
+ (5
* (n
|^ 4)))
+ (10
* (n
|^ 3)))
+ (10
* (n
|^ 2)))
+ (5
* n))
+ 1)
* 42)))
/ 42) by
Lm6
.= (((n
+ 1)
* (((((((6
* (n
|^ 6))
+ (57
* (n
|^ 5)))
+ (216
* (n
|^ 4)))
+ (414
* (n
|^ 3)))
+ (419
* (n
|^ 2)))
+ (211
* n))
+ 42))
/ 42)
.= (((n
+ 1)
* (((n
+ 2)
* ((2
* (n
+ 1))
+ 1))
* ((((3
* ((n
+ 1)
|^ 4))
+ (6
* ((n
+ 1)
|^ 3)))
- (3
* (n
+ 1)))
+ 1)))
/ 42) by
Lm16
.= (((((n
+ 1)
* ((n
+ 1)
+ 1))
* ((2
* (n
+ 1))
+ 1))
* ((((3
* ((n
+ 1)
|^ 4))
+ (6
* ((n
+ 1)
|^ 3)))
- (3
* (n
+ 1)))
+ 1))
/ 42);
hence thesis;
end;
((
Partial_Sums s)
.
0 )
= (s
.
0 ) by
SERIES_1:def 1
.= (
0
|^ 6) by
A1
.= ((((
0
* (
0
+ 1))
* ((2
*
0 )
+ 1))
* ((((3
* (
0
|^ 4))
+ (6
* (
0
|^ 3)))
- (3
*
0 ))
+ 1))
/ 42) by
NEWTON: 11;
then
A3:
X[
0 ];
for n holds
X[n] from
NAT_1:sch 2(
A3,
A2);
hence thesis;
end;
Lm17: (((n
+ 2)
|^ 2)
* (((((3
* ((n
+ 1)
|^ 4))
+ (6
* ((n
+ 1)
|^ 3)))
- ((n
+ 1)
|^ 2))
- (4
* (n
+ 1)))
+ 2))
= (((n
|^ 2)
* (((((3
* (n
|^ 4))
+ (6
* (n
|^ 3)))
- (n
|^ 2))
- (4
* n))
+ 2))
+ (((n
+ 1)
|^ 5)
* 24))
proof
A1: (((n
|^ 2)
* (((((3
* (n
|^ 4))
+ (6
* (n
|^ 3)))
- (n
|^ 2))
- (4
* n))
+ 2))
+ (((n
+ 1)
|^ 5)
* 24))
= ((((((3
* ((n
|^ 4)
* (n
|^ 2)))
+ (6
* ((n
|^ 3)
* (n
|^ 2))))
- ((n
|^ 2)
* (n
|^ 2)))
- (4
* (n
* (n
|^ 2))))
+ ((n
|^ 2)
* 2))
+ (((n
+ 1)
|^ 5)
* 24))
.= ((((((3
* (n
|^ (4
+ 2)))
+ (6
* ((n
|^ 3)
* (n
|^ 2))))
- ((n
|^ 2)
* (n
|^ 2)))
- (4
* (n
* (n
|^ 2))))
+ ((n
|^ 2)
* 2))
+ (((n
+ 1)
|^ 5)
* 24)) by
NEWTON: 8
.= ((((((3
* (n
|^ (4
+ 2)))
+ (6
* (n
|^ (3
+ 2))))
- ((n
|^ 2)
* (n
|^ 2)))
- (4
* (n
* (n
|^ 2))))
+ ((n
|^ 2)
* 2))
+ (((n
+ 1)
|^ 5)
* 24)) by
NEWTON: 8
.= ((((((3
* (n
|^ (4
+ 2)))
+ (6
* (n
|^ (3
+ 2))))
- (n
|^ (2
+ 2)))
- (4
* (n
* (n
|^ 2))))
+ ((n
|^ 2)
* 2))
+ (((n
+ 1)
|^ 5)
* 24)) by
NEWTON: 8
.= ((((((3
* (n
|^ (4
+ 2)))
+ (6
* (n
|^ (3
+ 2))))
- (n
|^ (2
+ 2)))
- (4
* (n
|^ (2
+ 1))))
+ ((n
|^ 2)
* 2))
+ (((n
+ 1)
|^ 5)
* 24)) by
NEWTON: 6
.= ((((((3
* (n
|^ 6))
+ (6
* (n
|^ 5)))
- (n
|^ 4))
- (4
* (n
|^ 3)))
+ ((n
|^ 2)
* 2))
+ (((((((n
|^ 5)
+ (5
* (n
|^ 4)))
+ (10
* (n
|^ 3)))
+ (10
* (n
|^ 2)))
+ (5
* n))
+ 1)
* 24)) by
Lm6
.= (((((((3
* (n
|^ 6))
+ (30
* (n
|^ 5)))
+ (119
* (n
|^ 4)))
+ (236
* (n
|^ 3)))
+ ((n
|^ 2)
* 242))
+ (120
* n))
+ 24);
(((n
+ 2)
|^ 2)
* (((((3
* ((n
+ 1)
|^ 4))
+ (6
* ((n
+ 1)
|^ 3)))
- ((n
+ 1)
|^ 2))
- (4
* (n
+ 1)))
+ 2))
= (((n
+ 2)
|^ 2)
* ((((((3
* ((n
+ 1)
|^ 4))
+ (6
* ((n
+ 1)
|^ 3)))
- ((n
+ 1)
|^ 2))
- (4
* n))
- 4)
+ 2))
.= (((n
+ 2)
|^ 2)
* ((((((3
* ((n
+ 1)
|^ 4))
+ (6
* ((n
+ 1)
|^ 3)))
- (((n
|^ 2)
+ ((2
* n)
* 1))
+ (1
|^ 2)))
- (4
* n))
- 4)
+ 2)) by
Lm3
.= (((n
+ 2)
|^ 2)
* (((((3
* ((n
+ 1)
|^ 4))
+ (6
* ((n
+ 1)
|^ 3)))
- (((n
|^ 2)
+ ((2
* n)
* 1))
+ (1
|^ 2)))
- (4
* n))
- 2))
.= (((n
+ 2)
|^ 2)
* (((((3
* ((n
+ 1)
|^ 4))
+ (6
* ((((n
|^ 3)
+ (3
* (n
|^ 2)))
+ (3
* n))
+ 1)))
- (((n
|^ 2)
+ (2
* n))
+ (1
|^ 2)))
- (4
* n))
- 2)) by
Lm4
.= (((n
+ 2)
|^ 2)
* (((((3
* ((n
+ 1)
|^ 4))
+ (6
* ((((n
|^ 3)
+ (3
* (n
|^ 2)))
+ (3
* n))
+ 1)))
- (((n
|^ 2)
+ (2
* n))
+ 1))
- (4
* n))
- 2))
.= (((n
+ 2)
|^ 2)
* (((((3
* ((n
+ 1)
|^ 4))
+ (6
* (n
|^ 3)))
+ ((18
- 1)
* (n
|^ 2)))
+ (((18
- 2)
- 4)
* n))
+ 3))
.= (((n
+ 2)
|^ 2)
* (((((3
* (((((n
|^ 4)
+ (4
* (n
|^ 3)))
+ (6
* (n
|^ 2)))
+ (4
* n))
+ 1))
+ (6
* (n
|^ 3)))
+ (17
* (n
|^ 2)))
+ (12
* n))
+ 3)) by
Lm6
.= ((((n
|^ 2)
+ ((2
* n)
* 2))
+ (2
* 2))
* (((((3
* (n
|^ 4))
+ (18
* (n
|^ 3)))
+ (35
* (n
|^ 2)))
+ (24
* n))
+ 6)) by
Lm3
.= (((((((3
* ((n
|^ 4)
* (n
|^ 2)))
+ (18
* ((n
|^ 3)
* (n
|^ 2))))
+ (35
* ((n
|^ 2)
* (n
|^ 2))))
+ (24
* (n
* (n
|^ 2))))
+ ((n
|^ 2)
* 6))
+ ((4
* n)
* (((((3
* (n
|^ 4))
+ (18
* (n
|^ 3)))
+ (35
* (n
|^ 2)))
+ (24
* n))
+ 6)))
+ (((((12
* (n
|^ 4))
+ (72
* (n
|^ 3)))
+ (140
* (n
|^ 2)))
+ (96
* n))
+ 24))
.= (((((((3
* (n
|^ (4
+ 2)))
+ (18
* ((n
|^ 3)
* (n
|^ 2))))
+ (35
* ((n
|^ 2)
* (n
|^ 2))))
+ (24
* (n
* (n
|^ 2))))
+ ((n
|^ 2)
* 6))
+ ((4
* n)
* (((((3
* (n
|^ 4))
+ (18
* (n
|^ 3)))
+ (35
* (n
|^ 2)))
+ (24
* n))
+ 6)))
+ (((((12
* (n
|^ 4))
+ (72
* (n
|^ 3)))
+ (140
* (n
|^ 2)))
+ (96
* n))
+ 24)) by
NEWTON: 8
.= (((((((3
* (n
|^ (4
+ 2)))
+ (18
* (n
|^ (3
+ 2))))
+ (35
* ((n
|^ 2)
* (n
|^ 2))))
+ (24
* (n
* (n
|^ 2))))
+ ((n
|^ 2)
* 6))
+ ((4
* n)
* (((((3
* (n
|^ 4))
+ (18
* (n
|^ 3)))
+ (35
* (n
|^ 2)))
+ (24
* n))
+ 6)))
+ (((((12
* (n
|^ 4))
+ (72
* (n
|^ 3)))
+ (140
* (n
|^ 2)))
+ (96
* n))
+ 24)) by
NEWTON: 8
.= (((((((3
* (n
|^ (4
+ 2)))
+ (18
* (n
|^ (3
+ 2))))
+ (35
* (n
|^ (2
+ 2))))
+ (24
* (n
* (n
|^ 2))))
+ ((n
|^ 2)
* 6))
+ ((4
* n)
* (((((3
* (n
|^ 4))
+ (18
* (n
|^ 3)))
+ (35
* (n
|^ 2)))
+ (24
* n))
+ 6)))
+ (((((12
* (n
|^ 4))
+ (72
* (n
|^ 3)))
+ (140
* (n
|^ 2)))
+ (96
* n))
+ 24)) by
NEWTON: 8
.= (((((((3
* (n
|^ (4
+ 2)))
+ (18
* (n
|^ (3
+ 2))))
+ (35
* (n
|^ (2
+ 2))))
+ (24
* (n
|^ (2
+ 1))))
+ ((n
|^ 2)
* 6))
+ ((4
* n)
* (((((3
* (n
|^ 4))
+ (18
* (n
|^ 3)))
+ (35
* (n
|^ 2)))
+ (24
* n))
+ 6)))
+ (((((12
* (n
|^ 4))
+ (72
* (n
|^ 3)))
+ (140
* (n
|^ 2)))
+ (96
* n))
+ 24)) by
NEWTON: 6
.= (((((((3
* (n
|^ 6))
+ (18
* (n
|^ 5)))
+ (35
* (n
|^ 4)))
+ (24
* (n
|^ 3)))
+ ((n
|^ 2)
* 6))
+ (((((12
* ((n
|^ 4)
* n))
+ (72
* ((n
|^ 3)
* n)))
+ (140
* ((n
|^ 2)
* n)))
+ (96
* (n
* n)))
+ (24
* n)))
+ (((((12
* (n
|^ 4))
+ (72
* (n
|^ 3)))
+ (140
* (n
|^ 2)))
+ (96
* n))
+ 24))
.= (((((((3
* (n
|^ 6))
+ (18
* (n
|^ 5)))
+ (35
* (n
|^ 4)))
+ (24
* (n
|^ 3)))
+ ((n
|^ 2)
* 6))
+ (((((12
* (n
|^ (4
+ 1)))
+ (72
* ((n
|^ 3)
* n)))
+ (140
* ((n
|^ 2)
* n)))
+ (96
* (n
* n)))
+ (24
* n)))
+ (((((12
* (n
|^ 4))
+ (72
* (n
|^ 3)))
+ (140
* (n
|^ 2)))
+ (96
* n))
+ 24)) by
NEWTON: 6
.= (((((((3
* (n
|^ 6))
+ (18
* (n
|^ 5)))
+ (35
* (n
|^ 4)))
+ (24
* (n
|^ 3)))
+ ((n
|^ 2)
* 6))
+ (((((12
* (n
|^ (4
+ 1)))
+ (72
* (n
|^ (3
+ 1))))
+ (140
* ((n
|^ 2)
* n)))
+ (96
* (n
* n)))
+ (24
* n)))
+ (((((12
* (n
|^ 4))
+ (72
* (n
|^ 3)))
+ (140
* (n
|^ 2)))
+ (96
* n))
+ 24)) by
NEWTON: 6
.= (((((((3
* (n
|^ 6))
+ (18
* (n
|^ 5)))
+ (35
* (n
|^ 4)))
+ (24
* (n
|^ 3)))
+ ((n
|^ 2)
* 6))
+ (((((12
* (n
|^ (4
+ 1)))
+ (72
* (n
|^ (3
+ 1))))
+ (140
* (n
|^ (2
+ 1))))
+ (96
* (n
* n)))
+ (24
* n)))
+ (((((12
* (n
|^ 4))
+ (72
* (n
|^ 3)))
+ (140
* (n
|^ 2)))
+ (96
* n))
+ 24)) by
NEWTON: 6
.= (((((((3
* (n
|^ 6))
+ (18
* (n
|^ 5)))
+ (35
* (n
|^ 4)))
+ (24
* (n
|^ 3)))
+ ((n
|^ 2)
* 6))
+ (((((12
* (n
|^ 5))
+ (72
* (n
|^ 4)))
+ (140
* (n
|^ 3)))
+ (96
* (n
|^ 2)))
+ (24
* n)))
+ (((((12
* (n
|^ 4))
+ (72
* (n
|^ 3)))
+ (140
* (n
|^ 2)))
+ (96
* n))
+ 24)) by
WSIERP_1: 1
.= (((((((3
* (n
|^ 6))
+ (30
* (n
|^ 5)))
+ (119
* (n
|^ 4)))
+ (236
* (n
|^ 3)))
+ (242
* (n
|^ 2)))
+ (120
* n))
+ 24);
hence thesis by
A1;
end;
Lm18: ((2
|^ (n
+ 2))
+ ((
- 1)
|^ (n
+ 2)))
>
0
proof
A1: ((
- 1)
|^ (n
+ 2))
=
|.((
- 1)
|^ (n
+ 2)).| or (
- ((
- 1)
|^ (n
+ 2)))
=
|.((
- 1)
|^ (n
+ 2)).| by
ABSVALUE: 1;
A2:
|.((
- 1)
|^ (n
+ 2)).|
= 1 by
Th1;
(n
+ 2)
>= 2 by
NAT_1: 11;
then (n
+ 2)
>
0 by
XXREAL_0: 2;
then (2
|^ (n
+ 2))
> 1 by
PEPIN: 25;
then
A3: ((2
|^ (n
+ 2))
+ ((
- 1)
|^ (n
+ 2)))
> (1
+ ((
- 1)
|^ (n
+ 2))) by
XREAL_1: 8;
per cases by
A2,
A1;
suppose ((
- 1)
|^ (n
+ 2))
= (
- 1);
hence thesis by
A3;
end;
suppose ((
- 1)
|^ (n
+ 2))
= 1;
hence thesis by
A3,
XXREAL_0: 2;
end;
end;
Lm19: ((2
|^ (n
+ 3))
+ ((
- 1)
|^ (n
+ 3)))
>
0
proof
A1: ((
- 1)
|^ (n
+ 3))
=
|.((
- 1)
|^ (n
+ 3)).| or (
- ((
- 1)
|^ (n
+ 3)))
=
|.((
- 1)
|^ (n
+ 3)).| by
ABSVALUE: 1;
A2:
|.((
- 1)
|^ (n
+ 3)).|
= 1 by
Th1;
(n
+ 3)
>= 3 by
NAT_1: 11;
then (n
+ 3)
>
0 by
XXREAL_0: 2;
then (2
|^ (n
+ 3))
> 1 by
PEPIN: 25;
then
A3: ((2
|^ (n
+ 3))
+ ((
- 1)
|^ (n
+ 3)))
> (1
+ ((
- 1)
|^ (n
+ 3))) by
XREAL_1: 8;
per cases by
A2,
A1;
suppose ((
- 1)
|^ (n
+ 3))
= (
- 1);
hence thesis by
A3;
end;
suppose ((
- 1)
|^ (n
+ 3))
= 1;
hence thesis by
A3,
XXREAL_0: 2;
end;
end;
theorem ::
SERIES_2:21
(for n holds (s
. n)
= (n
|^ 7)) implies for n holds ((
Partial_Sums s)
. n)
= ((((n
|^ 2)
* ((n
+ 1)
|^ 2))
* (((((3
* (n
|^ 4))
+ (6
* (n
|^ 3)))
- (n
|^ 2))
- (4
* n))
+ 2))
/ 24)
proof
defpred
X[
Nat] means ((
Partial_Sums s)
. $1)
= (((($1
|^ 2)
* (($1
+ 1)
|^ 2))
* (((((3
* ($1
|^ 4))
+ (6
* ($1
|^ 3)))
- ($1
|^ 2))
- (4
* $1))
+ 2))
/ 24);
assume
A1: for n holds (s
. n)
= (n
|^ 7);
A2: for n st
X[n] holds
X[(n
+ 1)]
proof
let n;
assume ((
Partial_Sums s)
. n)
= ((((n
|^ 2)
* ((n
+ 1)
|^ 2))
* (((((3
* (n
|^ 4))
+ (6
* (n
|^ 3)))
- (n
|^ 2))
- (4
* n))
+ 2))
/ 24);
then ((
Partial_Sums s)
. (n
+ 1))
= (((((n
|^ 2)
* ((n
+ 1)
|^ 2))
* (((((3
* (n
|^ 4))
+ (6
* (n
|^ 3)))
- (n
|^ 2))
- (4
* n))
+ 2))
/ 24)
+ (s
. (n
+ 1))) by
SERIES_1:def 1
.= (((((n
|^ 2)
* ((n
+ 1)
|^ 2))
* (((((3
* (n
|^ 4))
+ (6
* (n
|^ 3)))
- (n
|^ 2))
- (4
* n))
+ 2))
/ 24)
+ ((n
+ 1)
|^ 7)) by
A1
.= (((((n
|^ 2)
* ((n
+ 1)
|^ 2))
* (((((3
* (n
|^ 4))
+ (6
* (n
|^ 3)))
- (n
|^ 2))
- (4
* n))
+ 2))
+ (((n
+ 1)
|^ (5
+ 2))
* 24))
/ 24)
.= (((((n
|^ 2)
* ((n
+ 1)
|^ 2))
* (((((3
* (n
|^ 4))
+ (6
* (n
|^ 3)))
- (n
|^ 2))
- (4
* n))
+ 2))
+ ((((n
+ 1)
|^ 5)
* ((n
+ 1)
|^ 2))
* 24))
/ 24) by
NEWTON: 8
.= ((((n
+ 1)
|^ 2)
* (((n
|^ 2)
* (((((3
* (n
|^ 4))
+ (6
* (n
|^ 3)))
- (n
|^ 2))
- (4
* n))
+ 2))
+ (((n
+ 1)
|^ 5)
* 24)))
/ 24)
.= ((((n
+ 1)
|^ 2)
* (((n
+ 2)
|^ 2)
* (((((3
* ((n
+ 1)
|^ 4))
+ (6
* ((n
+ 1)
|^ 3)))
- ((n
+ 1)
|^ 2))
- (4
* (n
+ 1)))
+ 2)))
/ 24) by
Lm17
.= (((((n
+ 1)
|^ 2)
* (((n
+ 1)
+ 1)
|^ 2))
* (((((3
* ((n
+ 1)
|^ 4))
+ (6
* ((n
+ 1)
|^ 3)))
- ((n
+ 1)
|^ 2))
- (4
* (n
+ 1)))
+ 2))
/ 24);
hence thesis;
end;
((
Partial_Sums s)
.
0 )
= (s
.
0 ) by
SERIES_1:def 1
.= (
0
|^ 7) by
A1
.= (((
0
* ((
0
+ 1)
|^ 2))
* (((((3
* (
0
|^ 4))
+ (6
* (
0
|^ 3)))
- (
0
|^ 2))
- (4
*
0 ))
+ 2))
/ 24) by
NEWTON: 11
.= ((((
0
|^ 2)
* ((
0
+ 1)
|^ 2))
* (((((3
* (
0
|^ 4))
+ (6
* (
0
|^ 3)))
- (
0
|^ 2))
- (4
*
0 ))
+ 2))
/ 24) by
NEWTON: 11;
then
A3:
X[
0 ];
for n holds
X[n] from
NAT_1:sch 2(
A3,
A2);
hence thesis;
end;
theorem ::
SERIES_2:22
(for n holds (s
. n)
= (n
* ((n
+ 1)
|^ 2))) implies for n holds ((
Partial_Sums s)
. n)
= ((((n
* (n
+ 1))
* (n
+ 2))
* ((3
* n)
+ 5))
/ 12)
proof
defpred
X[
Nat] means ((
Partial_Sums s)
. $1)
= (((($1
* ($1
+ 1))
* ($1
+ 2))
* ((3
* $1)
+ 5))
/ 12);
assume
A1: for n holds (s
. n)
= (n
* ((n
+ 1)
|^ 2));
A2: for n st
X[n] holds
X[(n
+ 1)]
proof
let n;
assume ((
Partial_Sums s)
. n)
= ((((n
* (n
+ 1))
* (n
+ 2))
* ((3
* n)
+ 5))
/ 12);
then ((
Partial_Sums s)
. (n
+ 1))
= (((((n
* (n
+ 1))
* (n
+ 2))
* ((3
* n)
+ 5))
/ 12)
+ (s
. (n
+ 1))) by
SERIES_1:def 1
.= (((((n
* (n
+ 1))
* (n
+ 2))
* ((3
* n)
+ 5))
/ 12)
+ ((n
+ 1)
* (((n
+ 1)
+ 1)
|^ 2))) by
A1
.= (((n
+ 1)
* (((n
* (n
+ 2))
* ((3
* n)
+ 5))
+ (((n
+ 2)
|^ 2)
* 12)))
/ 12)
.= (((n
+ 1)
* (((n
* (n
+ 2))
* ((3
* n)
+ 5))
+ (((n
+ 2)
* (n
+ 2))
* 12)))
/ 12) by
WSIERP_1: 1
.= (((((n
+ 1)
* (n
+ 2))
* (n
+ 3))
* ((3
* (n
+ 1))
+ 5))
/ 12);
hence thesis;
end;
((
Partial_Sums s)
.
0 )
= (s
.
0 ) by
SERIES_1:def 1
.= (
0
* ((
0
+ 1)
|^ 2)) by
A1
.= ((((
0
* (
0
+ 1))
* (
0
+ 2))
* ((3
*
0 )
+ 5))
/ 12);
then
A3:
X[
0 ];
for n holds
X[n] from
NAT_1:sch 2(
A3,
A2);
hence thesis;
end;
theorem ::
SERIES_2:23
(for n holds (s
. n)
= ((n
* ((n
+ 1)
|^ 2))
* (n
+ 2))) implies for n holds ((
Partial_Sums s)
. n)
= (((((n
* (n
+ 1))
* (n
+ 2))
* (n
+ 3))
* ((2
* n)
+ 3))
/ 10)
proof
defpred
X[
Nat] means ((
Partial_Sums s)
. $1)
= ((((($1
* ($1
+ 1))
* ($1
+ 2))
* ($1
+ 3))
* ((2
* $1)
+ 3))
/ 10);
assume
A1: for n holds (s
. n)
= ((n
* ((n
+ 1)
|^ 2))
* (n
+ 2));
A2: for n st
X[n] holds
X[(n
+ 1)]
proof
let n;
assume ((
Partial_Sums s)
. n)
= (((((n
* (n
+ 1))
* (n
+ 2))
* (n
+ 3))
* ((2
* n)
+ 3))
/ 10);
then ((
Partial_Sums s)
. (n
+ 1))
= ((((((n
* (n
+ 1))
* (n
+ 2))
* (n
+ 3))
* ((2
* n)
+ 3))
/ 10)
+ (s
. (n
+ 1))) by
SERIES_1:def 1
.= ((((((n
* (n
+ 1))
* (n
+ 2))
* (n
+ 3))
* ((2
* n)
+ 3))
/ 10)
+ (((n
+ 1)
* (((n
+ 1)
+ 1)
|^ 2))
* ((n
+ 1)
+ 2))) by
A1
.= ((((((n
* (n
+ 1))
* (n
+ 2))
* (n
+ 3))
* ((2
* n)
+ 3))
/ 10)
+ (((((n
+ 1)
* ((n
+ 2)
* (n
+ 2)))
* (n
+ 3))
* 10)
/ 10)) by
WSIERP_1: 1
.= ((((((n
+ 1)
* (n
+ 2))
* (n
+ 3))
* (n
+ 4))
* ((2
* (n
+ 1))
+ 3))
/ 10);
hence thesis;
end;
((
Partial_Sums s)
.
0 )
= (s
.
0 ) by
SERIES_1:def 1
.= ((
0
* ((
0
+ 1)
|^ 2))
* (
0
+ 2)) by
A1
.= (((((
0
* (
0
+ 1))
* (
0
+ 2))
* (
0
+ 3))
* ((2
*
0 )
+ 3))
/ 10);
then
A3:
X[
0 ];
for n holds
X[n] from
NAT_1:sch 2(
A3,
A2);
hence thesis;
end;
theorem ::
SERIES_2:24
(for n holds (s
. n)
= ((n
* (n
+ 1))
* (2
|^ n))) implies for n holds ((
Partial_Sums s)
. n)
= (((2
|^ (n
+ 1))
* (((n
|^ 2)
- n)
+ 2))
- 4)
proof
defpred
X[
Nat] means ((
Partial_Sums s)
. $1)
= (((2
|^ ($1
+ 1))
* ((($1
|^ 2)
- $1)
+ 2))
- 4);
assume
A1: for n holds (s
. n)
= ((n
* (n
+ 1))
* (2
|^ n));
A2: for n st
X[n] holds
X[(n
+ 1)]
proof
let n;
assume ((
Partial_Sums s)
. n)
= (((2
|^ (n
+ 1))
* (((n
|^ 2)
- n)
+ 2))
- 4);
then ((
Partial_Sums s)
. (n
+ 1))
= ((((2
|^ (n
+ 1))
* (((n
|^ 2)
- n)
+ 2))
- 4)
+ (s
. (n
+ 1))) by
SERIES_1:def 1
.= ((((2
|^ (n
+ 1))
* (((n
|^ 2)
- n)
+ 2))
- 4)
+ (((n
+ 1)
* ((n
+ 1)
+ 1))
* (2
|^ (n
+ 1)))) by
A1
.= (((((2
|^ (n
+ 1))
* 2)
* ((((n
|^ 2)
- n)
+ 2)
+ ((n
+ 1)
* (n
+ 2))))
/ 2)
- 4)
.= ((((2
|^ ((n
+ 1)
+ 1))
* ((((n
|^ 2)
- n)
+ 2)
+ ((n
+ 1)
* (n
+ 2))))
/ 2)
- 4) by
NEWTON: 6
.= ((((2
|^ (n
+ 2))
* (((((((n
|^ 2)
- n)
+ 2)
+ (n
* n))
+ (1
* n))
+ (n
* 2))
+ 2))
/ 2)
- 4)
.= ((((2
|^ (n
+ 2))
* (((((((n
|^ 2)
- n)
+ 2)
+ (n
|^ 2))
+ (1
* n))
+ (n
* 2))
+ 2))
/ 2)
- 4) by
WSIERP_1: 1
.= (((2
|^ (n
+ 2))
* ((((((n
|^ 2)
+ (2
* n))
+ 1)
- 1)
- n)
+ 2))
- 4)
.= (((2
|^ (n
+ 2))
* ((((((n
|^ 2)
+ ((2
* n)
* 1))
+ (1
|^ 2))
- 1)
- n)
+ 2))
- 4)
.= (((2
|^ (n
+ 2))
* (((((n
+ 1)
|^ 2)
- 1)
- n)
+ 2))
- 4) by
Lm3
.= (((2
|^ (n
+ 2))
* ((((n
+ 1)
|^ 2)
- (1
+ n))
+ 2))
- 4);
hence thesis;
end;
((
Partial_Sums s)
.
0 )
= (s
.
0 ) by
SERIES_1:def 1
.= ((
0
* (
0
+ 1))
* (2
|^
0 )) by
A1
.= ((2
* 2)
- 4)
.= (((2
|^ (
0
+ 1))
* ((
0
-
0 )
+ 2))
- 4)
.= (((2
|^ (
0
+ 1))
* (((
0
|^ 2)
-
0 )
+ 2))
- 4) by
NEWTON: 11;
then
A3:
X[
0 ];
for n holds
X[n] from
NAT_1:sch 2(
A3,
A2);
hence thesis;
end;
theorem ::
SERIES_2:25
(for n st n
>= 1 holds (s
. n)
= (1
/ ((n
- 1)
* (n
+ 1))) & (s
.
0 )
=
0 ) implies for n st n
>= 2 holds ((
Partial_Sums s)
. n)
= (((3
/ 4)
- (1
/ (2
* n)))
- (1
/ (2
* (n
+ 1))))
proof
defpred
X[
Nat] means ((
Partial_Sums s)
. $1)
= (((3
/ 4)
- (1
/ (2
* $1)))
- (1
/ (2
* ($1
+ 1))));
assume
A1: for n st n
>= 1 holds (s
. n)
= (1
/ ((n
- 1)
* (n
+ 1))) & (s
.
0 )
=
0 ;
then
A2: (s
. 1)
= (1
/ ((1
- 1)
* (1
+ 1)))
.=
0 by
XCMPLX_1: 49;
A3: for n be
Nat st n
>= 2 &
X[n] holds
X[(n
+ 1)]
proof
let n be
Nat;
assume that
A4: n
>= 2 and
A5: ((
Partial_Sums s)
. n)
= (((3
/ 4)
- (1
/ (2
* n)))
- (1
/ (2
* (n
+ 1))));
A6: n
>
0 by
A4,
XXREAL_0: 2;
then
A7: (n
+ 1)
> 1 by
XREAL_1: 29;
A8: (n
+ 2)
>= n by
NAT_1: 11;
((
Partial_Sums s)
. (n
+ 1))
= ((((3
/ 4)
- (1
/ (2
* n)))
- (1
/ (2
* (n
+ 1))))
+ (s
. (n
+ 1))) by
A5,
SERIES_1:def 1
.= ((((3
/ 4)
- (1
/ (2
* n)))
- (1
/ (2
* (n
+ 1))))
+ (1
/ (((n
+ 1)
- 1)
* ((n
+ 1)
+ 1)))) by
A1,
A7
.= (((3
/ 4)
- (1
/ (2
* (n
+ 1))))
+ ((1
/ (n
* (n
+ 2)))
- (1
/ (2
* n))))
.= (((3
/ 4)
- (1
/ (2
* (n
+ 1))))
+ ((1
/ (n
* (n
+ 2)))
- ((1
/ 2)
* (1
/ n)))) by
XCMPLX_1: 102
.= (((3
/ 4)
- (1
/ (2
* (n
+ 1))))
+ (((1
/ n)
* (1
/ (n
+ 2)))
- ((1
/ 2)
* (1
/ n)))) by
XCMPLX_1: 102
.= (((3
/ 4)
- (1
/ (2
* (n
+ 1))))
+ (((1
/ (n
+ 2))
- (1
/ 2))
* (1
/ n)))
.= (((3
/ 4)
- (1
/ (2
* (n
+ 1))))
+ ((((1
* 2)
- (1
* (n
+ 2)))
/ ((n
+ 2)
* 2))
* (1
/ n))) by
A6,
A8,
XCMPLX_1: 130
.= (((3
/ 4)
- (1
/ (2
* (n
+ 1))))
+ (((
- n)
/ n)
* (1
/ ((n
+ 2)
* 2)))) by
XCMPLX_1: 85
.= (((3
/ 4)
- (1
/ (2
* (n
+ 1))))
+ ((
- 1)
* (1
/ ((n
+ 2)
* 2)))) by
A6,
XCMPLX_1: 197
.= (((3
/ 4)
- (1
/ (2
* (n
+ 1))))
+ (
- (1
/ (2
* ((n
+ 1)
+ 1)))));
hence thesis;
end;
((
Partial_Sums s)
. (1
+ 1))
= (((
Partial_Sums s)
. (1
+
0 ))
+ (s
. 2)) by
SERIES_1:def 1
.= ((((
Partial_Sums s)
.
0 )
+ (s
. 1))
+ (s
. 2)) by
SERIES_1:def 1
.= (((s
.
0 )
+ (s
. 1))
+ (s
. 2)) by
SERIES_1:def 1
.= ((
0
+ (s
. 1))
+ (s
. 2)) by
A1
.= (1
/ ((2
- 1)
* (2
+ 1))) by
A1,
A2
.= (((3
/ 4)
- (1
/ (2
* 2)))
- (1
/ (2
* (2
+ 1))));
then
A9:
X[2];
for n be
Nat st n
>= 2 holds
X[n] from
NAT_1:sch 8(
A9,
A3);
hence thesis;
end;
theorem ::
SERIES_2:26
(for n st n
>= 1 holds (s
. n)
= (1
/ (((2
* n)
- 1)
* ((2
* n)
+ 1))) & (s
.
0 )
=
0 ) implies for n st n
>= 1 holds ((
Partial_Sums s)
. n)
= (n
/ ((2
* n)
+ 1))
proof
defpred
X[
Nat] means ((
Partial_Sums s)
. $1)
= ($1
/ ((2
* $1)
+ 1));
assume
A1: for n st n
>= 1 holds (s
. n)
= (1
/ (((2
* n)
- 1)
* ((2
* 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 n
>= 1 and
A3: ((
Partial_Sums s)
. n)
= (n
/ ((2
* n)
+ 1));
A4: (n
+ 1)
>= 1 by
NAT_1: 11;
((2
* n)
+ 1)
>= 1 by
NAT_1: 11;
then
A5: ((2
* n)
+ 1)
>
0 by
XXREAL_0: 2;
((2
* n)
+ 3)
>= 3 by
NAT_1: 11;
then
A6: ((2
* n)
+ 3)
>
0 by
XXREAL_0: 2;
((
Partial_Sums s)
. (n
+ 1))
= ((n
/ ((2
* n)
+ 1))
+ (s
. (n
+ 1))) by
A3,
SERIES_1:def 1
.= ((n
/ ((2
* n)
+ 1))
+ (1
/ (((2
* (n
+ 1))
- 1)
* ((2
* (n
+ 1))
+ 1)))) by
A1,
A4
.= ((n
/ ((2
* n)
+ 1))
+ ((1
/ ((2
* n)
+ 1))
* (1
/ ((2
* n)
+ 3)))) by
XCMPLX_1: 102
.= ((n
* (1
/ ((2
* n)
+ 1)))
+ ((1
/ ((2
* n)
+ 1))
* (1
/ ((2
* n)
+ 3)))) by
XCMPLX_1: 99
.= ((n
+ (1
/ ((2
* n)
+ 3)))
* (1
/ ((2
* n)
+ 1)))
.= ((((n
* ((2
* n)
+ 3))
+ 1)
/ ((2
* n)
+ 3))
* (1
/ ((2
* n)
+ 1))) by
A6,
XCMPLX_1: 113
.= ((((n
+ 1)
* ((2
* n)
+ 1))
/ ((2
* n)
+ 3))
* (1
/ ((2
* n)
+ 1)))
.= ((((2
* n)
+ 1)
* ((n
+ 1)
/ ((2
* n)
+ 3)))
* (1
/ ((2
* n)
+ 1))) by
XCMPLX_1: 74
.= ((n
+ 1)
/ ((2
* (n
+ 1))
+ 1)) by
A5,
XCMPLX_1: 107;
hence thesis;
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
/ (((2
* 1)
- 1)
* ((2
* 1)
+ 1))) by
A1
.= (1
/ ((2
* 1)
+ 1));
then
A7:
X[1];
for n be
Nat st n
>= 1 holds
X[n] from
NAT_1:sch 8(
A7,
A2);
hence thesis;
end;
theorem ::
SERIES_2:27
(for n st n
>= 1 holds (s
. n)
= (1
/ (((3
* n)
- 2)
* ((3
* n)
+ 1))) & (s
.
0 )
=
0 ) implies for n st n
>= 1 holds ((
Partial_Sums s)
. n)
= (n
/ ((3
* n)
+ 1))
proof
defpred
X[
Nat] means ((
Partial_Sums s)
. $1)
= ($1
/ ((3
* $1)
+ 1));
assume
A1: for n st n
>= 1 holds (s
. n)
= (1
/ (((3
* n)
- 2)
* ((3
* 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 n
>= 1 and
A3: ((
Partial_Sums s)
. n)
= (n
/ ((3
* n)
+ 1));
A4: (n
+ 1)
>= 1 by
NAT_1: 11;
((3
* n)
+ 1)
>= 1 by
NAT_1: 11;
then
A5: ((3
* n)
+ 1)
>
0 by
XXREAL_0: 2;
((3
* n)
+ 4)
>= 4 by
NAT_1: 11;
then
A6: ((3
* n)
+ 4)
>
0 by
XXREAL_0: 2;
((
Partial_Sums s)
. (n
+ 1))
= ((n
/ ((3
* n)
+ 1))
+ (s
. (n
+ 1))) by
A3,
SERIES_1:def 1
.= ((n
/ ((3
* n)
+ 1))
+ (1
/ (((3
* (n
+ 1))
- 2)
* ((3
* (n
+ 1))
+ 1)))) by
A1,
A4
.= ((n
/ ((3
* n)
+ 1))
+ ((1
/ ((3
* n)
+ 1))
* (1
/ ((3
* n)
+ 4)))) by
XCMPLX_1: 102
.= ((n
* (1
/ ((3
* n)
+ 1)))
+ ((1
/ ((3
* n)
+ 1))
* (1
/ ((3
* n)
+ 4)))) by
XCMPLX_1: 99
.= ((n
+ (1
/ ((3
* n)
+ 4)))
* (1
/ ((3
* n)
+ 1)))
.= ((((n
* ((3
* n)
+ 4))
+ 1)
/ ((3
* n)
+ 4))
* (1
/ ((3
* n)
+ 1))) by
A6,
XCMPLX_1: 113
.= ((((n
+ 1)
* ((3
* n)
+ 1))
/ ((3
* n)
+ 4))
* (1
/ ((3
* n)
+ 1)))
.= ((((3
* n)
+ 1)
* ((n
+ 1)
/ ((3
* n)
+ 4)))
* (1
/ ((3
* n)
+ 1))) by
XCMPLX_1: 74
.= ((n
+ 1)
/ ((3
* (n
+ 1))
+ 1)) by
A5,
XCMPLX_1: 107;
hence thesis;
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
/ (((3
* 1)
- 2)
* ((3
* 1)
+ 1))) by
A1
.= (1
/ ((3
* 1)
+ 1));
then
A7:
X[1];
for n be
Nat st n
>= 1 holds
X[n] from
NAT_1:sch 8(
A7,
A2);
hence thesis;
end;
theorem ::
SERIES_2:28
(for n st n
>= 1 holds (s
. n)
= (1
/ ((((2
* n)
- 1)
* ((2
* n)
+ 1))
* ((2
* n)
+ 3))) & (s
.
0 )
=
0 ) implies for n st n
>= 1 holds ((
Partial_Sums s)
. n)
= ((1
/ 12)
- (1
/ ((4
* ((2
* n)
+ 1))
* ((2
* n)
+ 3))))
proof
defpred
X[
Nat] means ((
Partial_Sums s)
. $1)
= ((1
/ 12)
- (1
/ ((4
* ((2
* $1)
+ 1))
* ((2
* $1)
+ 3))));
assume
A1: for n st n
>= 1 holds (s
. n)
= (1
/ ((((2
* n)
- 1)
* ((2
* n)
+ 1))
* ((2
* n)
+ 3))) & (s
.
0 )
=
0 ;
A2: for n be
Nat st n
>= 1 &
X[n] holds
X[(n
+ 1)]
proof
let n be
Nat;
assume that n
>= 1 and
A3: ((
Partial_Sums s)
. n)
= ((1
/ 12)
- (1
/ ((4
* ((2
* n)
+ 1))
* ((2
* n)
+ 3))));
A4: (n
+ 1)
>= 1 by
NAT_1: 11;
((2
* n)
+ 1)
>= 1 by
NAT_1: 11;
then
A5: ((2
* n)
+ 1)
>
0 by
XXREAL_0: 2;
((2
* n)
+ 5)
>= 5 by
NAT_1: 11;
then
A6: ((2
* n)
+ 5)
>
0 by
XXREAL_0: 2;
((
Partial_Sums s)
. (n
+ 1))
= (((1
/ 12)
- (1
/ ((4
* ((2
* n)
+ 1))
* ((2
* n)
+ 3))))
+ (s
. (n
+ 1))) by
A3,
SERIES_1:def 1
.= (((1
/ 12)
- (1
/ ((4
* ((2
* n)
+ 1))
* ((2
* n)
+ 3))))
+ (1
/ ((((2
* (n
+ 1))
- 1)
* ((2
* (n
+ 1))
+ 1))
* ((2
* (n
+ 1))
+ 3)))) by
A1,
A4
.= (((1
/ 12)
- (1
/ (4
* (((2
* n)
+ 1)
* ((2
* n)
+ 3)))))
+ (1
/ ((((2
* n)
+ 1)
* ((2
* n)
+ 3))
* ((2
* n)
+ 5))))
.= (((1
/ 12)
- ((1
/ 4)
* (1
/ (((2
* n)
+ 1)
* ((2
* n)
+ 3)))))
+ (1
/ ((((2
* n)
+ 1)
* ((2
* n)
+ 3))
* ((2
* n)
+ 5)))) by
XCMPLX_1: 102
.= (((1
/ 12)
- ((1
/ 4)
* (1
/ (((2
* n)
+ 1)
* ((2
* n)
+ 3)))))
+ ((1
/ (((2
* n)
+ 1)
* ((2
* n)
+ 3)))
* (1
/ ((2
* n)
+ 5)))) by
XCMPLX_1: 102
.= ((1
/ 12)
- ((1
/ (((2
* n)
+ 1)
* ((2
* n)
+ 3)))
* ((1
/ 4)
- (1
/ ((2
* n)
+ 5)))))
.= ((1
/ 12)
- ((1
/ (((2
* n)
+ 1)
* ((2
* n)
+ 3)))
* (((1
* ((2
* n)
+ 5))
- (1
* 4))
/ (4
* ((2
* n)
+ 5))))) by
A6,
XCMPLX_1: 130
.= ((1
/ 12)
- (((1
/ ((2
* n)
+ 1))
* (1
/ ((2
* n)
+ 3)))
* (((2
* n)
+ 1)
/ (4
* ((2
* n)
+ 5))))) by
XCMPLX_1: 102
.= ((1
/ 12)
- ((((1
/ ((2
* n)
+ 1))
* (1
/ ((2
* n)
+ 3)))
* ((2
* n)
+ 1))
/ (4
* ((2
* n)
+ 5)))) by
XCMPLX_1: 74
.= ((1
/ 12)
- ((1
/ ((2
* n)
+ 3))
/ (4
* ((2
* n)
+ 5)))) by
A5,
XCMPLX_1: 109
.= ((1
/ 12)
- (1
/ (((2
* n)
+ 3)
* (4
* ((2
* n)
+ 5))))) by
XCMPLX_1: 78
.= ((1
/ 12)
- (1
/ ((4
* ((2
* (n
+ 1))
+ 1))
* ((2
* (n
+ 1))
+ 3))));
hence thesis;
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
/ ((((2
* 1)
- 1)
* ((2
* 1)
+ 1))
* ((2
* 1)
+ 3))) by
A1
.= ((1
/ 12)
- (1
/ ((4
* ((2
* 1)
+ 1))
* ((2
* 1)
+ 3))));
then
A7:
X[1];
for n be
Nat st n
>= 1 holds
X[n] from
NAT_1:sch 8(
A7,
A2);
hence thesis;
end;
theorem ::
SERIES_2:29
(for n st n
>= 1 holds (s
. n)
= (1
/ ((((3
* n)
- 2)
* ((3
* n)
+ 1))
* ((3
* n)
+ 4))) & (s
.
0 )
=
0 ) implies for n st n
>= 1 holds ((
Partial_Sums s)
. n)
= ((1
/ 24)
- (1
/ ((6
* ((3
* n)
+ 1))
* ((3
* n)
+ 4))))
proof
defpred
X[
Nat] means ((
Partial_Sums s)
. $1)
= ((1
/ 24)
- (1
/ ((6
* ((3
* $1)
+ 1))
* ((3
* $1)
+ 4))));
assume
A1: for n st n
>= 1 holds (s
. n)
= (1
/ ((((3
* n)
- 2)
* ((3
* n)
+ 1))
* ((3
* n)
+ 4))) & (s
.
0 )
=
0 ;
A2: for n be
Nat st n
>= 1 &
X[n] holds
X[(n
+ 1)]
proof
let n be
Nat;
assume that n
>= 1 and
A3: ((
Partial_Sums s)
. n)
= ((1
/ 24)
- (1
/ ((6
* ((3
* n)
+ 1))
* ((3
* n)
+ 4))));
A4: (n
+ 1)
>= 1 by
NAT_1: 11;
((3
* n)
+ 1)
>= 1 by
NAT_1: 11;
then
A5: ((3
* n)
+ 1)
>
0 by
XXREAL_0: 2;
((3
* n)
+ 7)
>= 7 by
NAT_1: 11;
then
A6: ((3
* n)
+ 7)
>
0 by
XXREAL_0: 2;
((
Partial_Sums s)
. (n
+ 1))
= (((1
/ 24)
- (1
/ ((6
* ((3
* n)
+ 1))
* ((3
* n)
+ 4))))
+ (s
. (n
+ 1))) by
A3,
SERIES_1:def 1
.= (((1
/ 24)
- (1
/ ((6
* ((3
* n)
+ 1))
* ((3
* n)
+ 4))))
+ (1
/ ((((3
* (n
+ 1))
- 2)
* ((3
* (n
+ 1))
+ 1))
* ((3
* (n
+ 1))
+ 4)))) by
A1,
A4
.= (((1
/ 24)
- (1
/ (6
* (((3
* n)
+ 1)
* ((3
* n)
+ 4)))))
+ (1
/ ((((3
* n)
+ 1)
* ((3
* n)
+ 4))
* ((3
* n)
+ 7))))
.= (((1
/ 24)
- ((1
/ 6)
* (1
/ (((3
* n)
+ 1)
* ((3
* n)
+ 4)))))
+ (1
/ ((((3
* n)
+ 1)
* ((3
* n)
+ 4))
* ((3
* n)
+ 7)))) by
XCMPLX_1: 102
.= (((1
/ 24)
- ((1
/ 6)
* (1
/ (((3
* n)
+ 1)
* ((3
* n)
+ 4)))))
+ ((1
/ (((3
* n)
+ 1)
* ((3
* n)
+ 4)))
* (1
/ ((3
* n)
+ 7)))) by
XCMPLX_1: 102
.= ((1
/ 24)
- ((1
/ (((3
* n)
+ 1)
* ((3
* n)
+ 4)))
* ((1
/ 6)
- (1
/ ((3
* n)
+ 7)))))
.= ((1
/ 24)
- ((1
/ (((3
* n)
+ 1)
* ((3
* n)
+ 4)))
* (((1
* ((3
* n)
+ 7))
- (1
* 6))
/ (6
* ((3
* n)
+ 7))))) by
A6,
XCMPLX_1: 130
.= ((1
/ 24)
- (((1
/ ((3
* n)
+ 4))
* (1
/ ((3
* n)
+ 1)))
* (((3
* n)
+ 1)
/ (6
* ((3
* n)
+ 7))))) by
XCMPLX_1: 102
.= ((1
/ 24)
- ((((1
/ ((3
* n)
+ 4))
* (1
/ ((3
* n)
+ 1)))
* ((3
* n)
+ 1))
/ (6
* ((3
* n)
+ 7)))) by
XCMPLX_1: 74
.= ((1
/ 24)
- ((1
/ ((3
* n)
+ 4))
/ (6
* ((3
* n)
+ 7)))) by
A5,
XCMPLX_1: 109
.= ((1
/ 24)
- (1
/ (((3
* n)
+ 4)
* (6
* ((3
* n)
+ 7))))) by
XCMPLX_1: 78
.= ((1
/ 24)
- (1
/ ((6
* ((3
* (n
+ 1))
+ 1))
* ((3
* (n
+ 1))
+ 4))));
hence thesis;
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
/ ((((3
* 1)
- 2)
* ((3
* 1)
+ 1))
* ((3
* 1)
+ 4))) by
A1
.= ((1
/ 24)
- (1
/ ((6
* ((3
* 1)
+ 1))
* ((3
* 1)
+ 4))));
then
A7:
X[1];
for n be
Nat st n
>= 1 holds
X[n] from
NAT_1:sch 8(
A7,
A2);
hence thesis;
end;
theorem ::
SERIES_2:30
(for n holds (s
. n)
= (((2
* n)
- 1)
/ ((n
* (n
+ 1))
* (n
+ 2)))) implies for n st n
>= 1 holds ((
Partial_Sums s)
. n)
= (((3
/ 4)
- (2
/ (n
+ 2)))
+ (1
/ ((2
* (n
+ 1))
* (n
+ 2))))
proof
defpred
X[
Nat] means ((
Partial_Sums s)
. $1)
= (((3
/ 4)
- (2
/ ($1
+ 2)))
+ (1
/ ((2
* ($1
+ 1))
* ($1
+ 2))));
assume
A1: for n holds (s
. n)
= (((2
* n)
- 1)
/ ((n
* (n
+ 1))
* (n
+ 2)));
then
A2: (s
.
0 )
= (((2
*
0 )
- 1)
/ ((
0
* (
0
+ 1))
* (
0
+ 2)))
.=
0 by
XCMPLX_1: 49;
A3: for n be
Nat st n
>= 1 &
X[n] holds
X[(n
+ 1)]
proof
let n be
Nat;
assume that n
>= 1 and
A4: ((
Partial_Sums s)
. n)
= (((3
/ 4)
- (2
/ (n
+ 2)))
+ (1
/ ((2
* (n
+ 1))
* (n
+ 2))));
(n
+ 1)
>= (1
+
0 ) by
NAT_1: 11;
then
A5: (n
+ 1)
>
0 by
NAT_1: 13;
(n
+ 2)
>= 2 by
NAT_1: 11;
then (n
+ 2)
>
0 by
XXREAL_0: 2;
then
A6: ((n
+ 1)
* (n
+ 2))
>
0 by
A5,
XREAL_1: 129;
(n
+ 3)
>= 3 by
NAT_1: 11;
then
A7: (n
+ 3)
>
0 by
XXREAL_0: 2;
((
Partial_Sums s)
. (n
+ 1))
= ((((3
/ 4)
- (2
/ (n
+ 2)))
+ (1
/ ((2
* (n
+ 1))
* (n
+ 2))))
+ (s
. (n
+ 1))) by
A4,
SERIES_1:def 1
.= ((((3
/ 4)
- (2
/ (n
+ 2)))
+ (1
/ ((2
* (n
+ 1))
* (n
+ 2))))
+ (((2
* (n
+ 1))
- 1)
/ (((n
+ 1)
* ((n
+ 1)
+ 1))
* ((n
+ 1)
+ 2)))) by
A1
.= (((3
/ 4)
- ((2
/ (n
+ 2))
- (1
/ (2
* ((n
+ 1)
* (n
+ 2))))))
+ (((2
* n)
+ 1)
/ (((n
+ 1)
* (n
+ 2))
* (n
+ 3))))
.= (((3
/ 4)
- (((2
* (n
+ 1))
/ ((n
+ 2)
* (n
+ 1)))
- (1
/ (2
* ((n
+ 1)
* (n
+ 2))))))
+ (((2
* n)
+ 1)
/ (((n
+ 1)
* (n
+ 2))
* (n
+ 3)))) by
A5,
XCMPLX_1: 91
.= (((3
/ 4)
- ((((2
* (n
+ 1))
* 2)
/ ((2
* (n
+ 2))
* (n
+ 1)))
- (1
/ (2
* ((n
+ 1)
* (n
+ 2))))))
+ (((2
* n)
+ 1)
/ (((n
+ 1)
* (n
+ 2))
* (n
+ 3)))) by
XCMPLX_1: 91
.= (((3
/ 4)
- (((4
* (n
+ 1))
- 1)
/ (2
* ((n
+ 2)
* (n
+ 1)))))
+ (((2
* n)
+ 1)
/ (((n
+ 1)
* (n
+ 2))
* (n
+ 3)))) by
XCMPLX_1: 120
.= (((3
/ 4)
- ((((4
* n)
+ 3)
* (n
+ 3))
/ ((2
* ((n
+ 2)
* (n
+ 1)))
* (n
+ 3))))
+ (((2
* n)
+ 1)
/ (((n
+ 1)
* (n
+ 2))
* (n
+ 3)))) by
A7,
XCMPLX_1: 91
.= (((3
/ 4)
- ((((4
* n)
+ 3)
* (n
+ 3))
/ ((2
* ((n
+ 2)
* (n
+ 1)))
* (n
+ 3))))
+ ((((2
* n)
+ 1)
* 2)
/ ((((n
+ 1)
* (n
+ 2))
* (n
+ 3))
* 2))) by
XCMPLX_1: 91
.= ((3
/ 4)
- (((((4
* n)
+ 3)
* (n
+ 3))
/ ((2
* ((n
+ 2)
* (n
+ 1)))
* (n
+ 3)))
- ((((2
* n)
+ 1)
* 2)
/ ((((n
+ 1)
* (n
+ 2))
* (n
+ 3))
* 2))))
.= ((3
/ 4)
- (((((4
* n)
+ 3)
* (n
+ 3))
- (((2
* n)
+ 1)
* 2))
/ ((2
* ((n
+ 2)
* (n
+ 1)))
* (n
+ 3)))) by
XCMPLX_1: 120
.= ((3
/ 4)
- ((((4
* (n
+ 1))
* (n
+ 2))
- (n
+ 1))
/ ((2
* ((n
+ 2)
* (n
+ 1)))
* (n
+ 3))))
.= ((3
/ 4)
- (((4
* ((n
+ 1)
* (n
+ 2)))
/ ((2
* (n
+ 3))
* ((n
+ 2)
* (n
+ 1))))
- ((n
+ 1)
/ ((2
* ((n
+ 2)
* (n
+ 1)))
* (n
+ 3))))) by
XCMPLX_1: 120
.= ((3
/ 4)
- ((4
/ (2
* (n
+ 3)))
- ((1
* (n
+ 1))
/ (((2
* (n
+ 2))
* (n
+ 3))
* (n
+ 1))))) by
A6,
XCMPLX_1: 91
.= ((3
/ 4)
- (((2
* 2)
/ ((n
+ 3)
* 2))
- (1
/ ((2
* (n
+ 2))
* (n
+ 3))))) by
A5,
XCMPLX_1: 91
.= ((3
/ 4)
- ((2
/ ((n
+ 1)
+ 2))
- (1
/ ((2
* ((n
+ 1)
+ 1))
* ((n
+ 1)
+ 2))))) by
XCMPLX_1: 91;
hence thesis;
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
.= (((2
* 1)
- 1)
/ ((1
* (1
+ 1))
* (1
+ 2))) by
A1,
A2
.= (((3
/ 4)
- (2
/ (1
+ 2)))
+ (1
/ ((2
* (1
+ 1))
* (1
+ 2))));
then
A8:
X[1];
for n be
Nat st n
>= 1 holds
X[n] from
NAT_1:sch 8(
A8,
A3);
hence thesis;
end;
theorem ::
SERIES_2:31
(for n holds (s
. n)
= ((n
+ 2)
/ ((n
* (n
+ 1))
* (n
+ 3)))) implies for n st n
>= 1 holds ((
Partial_Sums s)
. n)
= ((((29
/ 36)
- (1
/ (n
+ 3)))
- (3
/ ((2
* (n
+ 2))
* (n
+ 3))))
- (4
/ (((3
* (n
+ 1))
* (n
+ 2))
* (n
+ 3))))
proof
defpred
X[
Nat] means ((
Partial_Sums s)
. $1)
= ((((29
/ 36)
- (1
/ ($1
+ 3)))
- (3
/ ((2
* ($1
+ 2))
* ($1
+ 3))))
- (4
/ (((3
* ($1
+ 1))
* ($1
+ 2))
* ($1
+ 3))));
assume
A1: for n holds (s
. n)
= ((n
+ 2)
/ ((n
* (n
+ 1))
* (n
+ 3)));
then
A2: (s
.
0 )
= ((
0
+ 2)
/ ((
0
* (
0
+ 1))
* (
0
+ 3)))
.=
0 by
XCMPLX_1: 49;
A3: for n be
Nat st n
>= 1 &
X[n] holds
X[(n
+ 1)]
proof
let n be
Nat;
assume that n
>= 1 and
A4: ((
Partial_Sums s)
. n)
= ((((29
/ 36)
- (1
/ (n
+ 3)))
- (3
/ ((2
* (n
+ 2))
* (n
+ 3))))
- (4
/ (((3
* (n
+ 1))
* (n
+ 2))
* (n
+ 3))));
(n
+ 4)
>= 4 by
NAT_1: 11;
then
A5: (n
+ 4)
>
0 by
XXREAL_0: 2;
(n
+ 1)
>= (1
+
0 ) by
NAT_1: 11;
then
A6: (n
+ 1)
>
0 by
NAT_1: 13;
then
A7: (2
* (n
+ 1))
>
0 by
XREAL_1: 129;
(n
+ 2)
>= 2 by
NAT_1: 11;
then
A8: (n
+ 2)
>
0 by
XXREAL_0: 2;
then
A9: ((n
+ 1)
* (n
+ 2))
>
0 by
A6,
XREAL_1: 129;
then
A10: (((n
+ 1)
* (n
+ 2))
* 3)
>
0 by
XREAL_1: 129;
(n
+ 3)
>= 3 by
NAT_1: 11;
then
A11: (n
+ 3)
>
0 by
XXREAL_0: 2;
then (((n
+ 1)
* (n
+ 2))
* (n
+ 3))
>
0 by
A9,
XREAL_1: 129;
then
A12: ((((n
+ 1)
* (n
+ 2))
* (n
+ 3))
* 6)
>
0 by
XREAL_1: 129;
((
Partial_Sums s)
. (n
+ 1))
= (((((29
/ 36)
- (1
/ (n
+ 3)))
- (3
/ ((2
* (n
+ 2))
* (n
+ 3))))
- (4
/ (((3
* (n
+ 1))
* (n
+ 2))
* (n
+ 3))))
+ (s
. (n
+ 1))) by
A4,
SERIES_1:def 1
.= (((((29
/ 36)
- (1
/ (n
+ 3)))
- (3
/ ((2
* (n
+ 2))
* (n
+ 3))))
- (4
/ (((3
* (n
+ 1))
* (n
+ 2))
* (n
+ 3))))
+ (((n
+ 1)
+ 2)
/ (((n
+ 1)
* ((n
+ 1)
+ 1))
* ((n
+ 1)
+ 3)))) by
A1
.= (((((29
/ 36)
- ((1
* (n
+ 2))
/ ((n
+ 3)
* (n
+ 2))))
- (3
/ ((2
* (n
+ 2))
* (n
+ 3))))
- (4
/ (((3
* (n
+ 1))
* (n
+ 2))
* (n
+ 3))))
+ ((n
+ 3)
/ (((n
+ 1)
* (n
+ 2))
* (n
+ 4)))) by
A8,
XCMPLX_1: 91
.= (((((29
/ 36)
- (((n
+ 2)
* 2)
/ (((n
+ 2)
* (n
+ 3))
* 2)))
- (3
/ ((2
* (n
+ 2))
* (n
+ 3))))
- (4
/ (((3
* (n
+ 1))
* (n
+ 2))
* (n
+ 3))))
+ ((n
+ 3)
/ (((n
+ 1)
* (n
+ 2))
* (n
+ 4)))) by
XCMPLX_1: 91
.= ((((29
/ 36)
- ((((n
+ 2)
* 2)
/ (((n
+ 2)
* (n
+ 3))
* 2))
+ (3
/ ((2
* (n
+ 2))
* (n
+ 3)))))
- (4
/ (((3
* (n
+ 1))
* (n
+ 2))
* (n
+ 3))))
+ ((n
+ 3)
/ (((n
+ 1)
* (n
+ 2))
* (n
+ 4))))
.= ((((29
/ 36)
- ((((n
+ 2)
* 2)
+ 3)
/ ((2
* (n
+ 2))
* (n
+ 3))))
- (4
/ (((3
* (n
+ 1))
* (n
+ 2))
* (n
+ 3))))
+ ((n
+ 3)
/ (((n
+ 1)
* (n
+ 2))
* (n
+ 4)))) by
XCMPLX_1: 62
.= ((((29
/ 36)
- ((((n
* 2)
+ 7)
* (n
+ 1))
/ (((2
* (n
+ 2))
* (n
+ 3))
* (n
+ 1))))
- (4
/ (((3
* (n
+ 1))
* (n
+ 2))
* (n
+ 3))))
+ ((n
+ 3)
/ (((n
+ 1)
* (n
+ 2))
* (n
+ 4)))) by
A6,
XCMPLX_1: 91
.= ((((29
/ 36)
- (((((n
* 2)
+ 7)
* (n
+ 1))
* 3)
/ ((((2
* (n
+ 2))
* (n
+ 3))
* (n
+ 1))
* 3)))
- (4
/ (((3
* (n
+ 1))
* (n
+ 2))
* (n
+ 3))))
+ ((n
+ 3)
/ (((n
+ 1)
* (n
+ 2))
* (n
+ 4)))) by
XCMPLX_1: 91
.= ((((29
/ 36)
- (((((n
* 2)
+ 7)
* (n
+ 1))
* 3)
/ ((((2
* (n
+ 2))
* (n
+ 3))
* (n
+ 1))
* 3)))
- ((4
* 2)
/ ((((3
* (n
+ 1))
* (n
+ 2))
* (n
+ 3))
* 2)))
+ ((n
+ 3)
/ (((n
+ 1)
* (n
+ 2))
* (n
+ 4)))) by
XCMPLX_1: 91
.= (((29
/ 36)
- ((((((n
* 2)
+ 7)
* (n
+ 1))
* 3)
/ (((6
* (n
+ 2))
* (n
+ 3))
* (n
+ 1)))
+ (8
/ (((6
* (n
+ 1))
* (n
+ 2))
* (n
+ 3)))))
+ ((n
+ 3)
/ (((n
+ 1)
* (n
+ 2))
* (n
+ 4))))
.= (((29
/ 36)
- (((((((n
* 2)
+ 7)
* (n
+ 1))
* 3)
* (n
+ 4))
/ ((((6
* (n
+ 2))
* (n
+ 3))
* (n
+ 1))
* (n
+ 4)))
+ (8
/ (((6
* (n
+ 1))
* (n
+ 2))
* (n
+ 3)))))
+ ((n
+ 3)
/ (((n
+ 1)
* (n
+ 2))
* (n
+ 4)))) by
A5,
XCMPLX_1: 91
.= (((29
/ 36)
- (((((((n
* 2)
+ 7)
* (n
+ 1))
* 3)
* (n
+ 4))
/ ((((6
* (n
+ 1))
* (n
+ 2))
* (n
+ 3))
* (n
+ 4)))
+ ((8
* (n
+ 4))
/ ((((6
* (n
+ 1))
* (n
+ 2))
* (n
+ 3))
* (n
+ 4)))))
+ ((n
+ 3)
/ (((n
+ 1)
* (n
+ 2))
* (n
+ 4)))) by
A5,
XCMPLX_1: 91
.= (((29
/ 36)
- (((((((n
* 2)
+ 7)
* (n
+ 1))
* 3)
* (n
+ 4))
+ (8
* (n
+ 4)))
/ ((((6
* (n
+ 1))
* (n
+ 2))
* (n
+ 3))
* (n
+ 4))))
+ ((n
+ 3)
/ (((n
+ 1)
* (n
+ 2))
* (n
+ 4)))) by
XCMPLX_1: 62
.= (((29
/ 36)
- (((((((n
* 2)
+ 7)
* (n
+ 1))
* 3)
* (n
+ 4))
+ (8
* (n
+ 4)))
/ ((((6
* (n
+ 1))
* (n
+ 2))
* (n
+ 3))
* (n
+ 4))))
+ (((n
+ 3)
* 6)
/ ((((n
+ 1)
* (n
+ 2))
* (n
+ 4))
* 6))) by
XCMPLX_1: 91
.= (((29
/ 36)
- (((((((n
* 2)
+ 7)
* (n
+ 1))
* 3)
* (n
+ 4))
+ (8
* (n
+ 4)))
/ ((((6
* (n
+ 1))
* (n
+ 2))
* (n
+ 3))
* (n
+ 4))))
+ ((((n
+ 3)
* 6)
* (n
+ 3))
/ (((((n
+ 1)
* (n
+ 2))
* (n
+ 4))
* 6)
* (n
+ 3)))) by
A11,
XCMPLX_1: 91
.= ((29
/ 36)
- ((((((((n
* 2)
+ 7)
* (n
+ 1))
* 3)
* (n
+ 4))
+ (8
* (n
+ 4)))
/ ((((6
* (n
+ 1))
* (n
+ 2))
* (n
+ 3))
* (n
+ 4)))
- ((((n
+ 3)
* 6)
* (n
+ 3))
/ (((((n
+ 1)
* (n
+ 2))
* (n
+ 4))
* 6)
* (n
+ 3)))))
.= ((29
/ 36)
- ((((((((n
* 2)
+ 7)
* (n
+ 1))
* 3)
* (n
+ 4))
+ (8
* (n
+ 4)))
- (((n
+ 3)
* 6)
* (n
+ 3)))
/ ((((6
* (n
+ 1))
* (n
+ 2))
* (n
+ 3))
* (n
+ 4)))) by
XCMPLX_1: 120
.= ((29
/ 36)
- ((((((6
* (n
+ 1))
* (n
+ 2))
* (n
+ 3))
+ ((9
* (n
+ 1))
* (n
+ 2)))
+ (8
* (n
+ 1)))
/ ((((6
* (n
+ 1))
* (n
+ 2))
* (n
+ 3))
* (n
+ 4))))
.= ((29
/ 36)
- ((((((6
* (n
+ 1))
* (n
+ 2))
* (n
+ 3))
+ ((9
* (n
+ 1))
* (n
+ 2)))
/ ((((6
* (n
+ 1))
* (n
+ 2))
* (n
+ 3))
* (n
+ 4)))
+ ((8
* (n
+ 1))
/ ((((6
* (n
+ 1))
* (n
+ 2))
* (n
+ 3))
* (n
+ 4))))) by
XCMPLX_1: 62
.= ((29
/ 36)
- ((((1
* (((6
* (n
+ 1))
* (n
+ 2))
* (n
+ 3)))
/ ((n
+ 4)
* (((6
* (n
+ 1))
* (n
+ 2))
* (n
+ 3))))
+ (((9
* (n
+ 1))
* (n
+ 2))
/ ((((6
* (n
+ 1))
* (n
+ 2))
* (n
+ 3))
* (n
+ 4))))
+ ((8
* (n
+ 1))
/ ((((6
* (n
+ 1))
* (n
+ 2))
* (n
+ 3))
* (n
+ 4))))) by
XCMPLX_1: 62
.= ((29
/ 36)
- (((1
/ (n
+ 4))
+ ((3
* ((3
* (n
+ 1))
* (n
+ 2)))
/ (((2
* (n
+ 3))
* (n
+ 4))
* ((3
* (n
+ 1))
* (n
+ 2)))))
+ ((8
* (n
+ 1))
/ ((((6
* (n
+ 1))
* (n
+ 2))
* (n
+ 3))
* (n
+ 4))))) by
A12,
XCMPLX_1: 91
.= ((29
/ 36)
- (((1
/ (n
+ 4))
+ (3
/ ((2
* (n
+ 3))
* (n
+ 4))))
+ ((4
* (2
* (n
+ 1)))
/ ((((3
* (n
+ 2))
* (n
+ 3))
* (n
+ 4))
* (2
* (n
+ 1)))))) by
A10,
XCMPLX_1: 91
.= ((29
/ 36)
- (((1
/ (n
+ 4))
+ (3
/ ((2
* (n
+ 3))
* (n
+ 4))))
+ (4
/ (((3
* (n
+ 2))
* (n
+ 3))
* (n
+ 4))))) by
A7,
XCMPLX_1: 91
.= ((((29
/ 36)
- (1
/ ((n
+ 1)
+ 3)))
- (3
/ ((2
* ((n
+ 1)
+ 2))
* ((n
+ 1)
+ 3))))
- (4
/ (((3
* ((n
+ 1)
+ 1))
* ((n
+ 1)
+ 2))
* ((n
+ 1)
+ 3))));
hence thesis;
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
.= ((1
+ 2)
/ ((1
* (1
+ 1))
* (1
+ 3))) by
A1,
A2
.= ((((29
/ 36)
- (1
/ (1
+ 3)))
- (3
/ ((2
* (1
+ 2))
* (1
+ 3))))
- (4
/ (((3
* (1
+ 1))
* (1
+ 2))
* (1
+ 3))));
then
A13:
X[1];
for n be
Nat st n
>= 1 holds
X[n] from
NAT_1:sch 8(
A13,
A3);
hence thesis;
end;
theorem ::
SERIES_2:32
(for n holds (s
. n)
= (((n
+ 1)
* (2
|^ n))
/ ((n
+ 2)
* (n
+ 3)))) implies for n holds ((
Partial_Sums s)
. n)
= (((2
|^ (n
+ 1))
/ (n
+ 3))
- (1
/ 2))
proof
defpred
X[
Nat] means ((
Partial_Sums s)
. $1)
= (((2
|^ ($1
+ 1))
/ ($1
+ 3))
- (1
/ 2));
assume
A1: for n holds (s
. n)
= (((n
+ 1)
* (2
|^ n))
/ ((n
+ 2)
* (n
+ 3)));
A2: for n st
X[n] holds
X[(n
+ 1)]
proof
let n;
(n
+ 3)
>= 3 by
NAT_1: 11;
then
A3: (n
+ 3)
>
0 by
XXREAL_0: 2;
(n
+ 4)
>= 4 by
NAT_1: 11;
then
A4: (n
+ 4)
>
0 by
XXREAL_0: 2;
assume ((
Partial_Sums s)
. n)
= (((2
|^ (n
+ 1))
/ (n
+ 3))
- (1
/ 2));
then ((
Partial_Sums s)
. (n
+ 1))
= ((((2
|^ (n
+ 1))
/ (n
+ 3))
- (1
/ 2))
+ (s
. (n
+ 1))) by
SERIES_1:def 1
.= ((((2
|^ (n
+ 1))
/ (n
+ 3))
- (1
/ 2))
+ ((((n
+ 1)
+ 1)
* (2
|^ (n
+ 1)))
/ (((n
+ 1)
+ 2)
* ((n
+ 1)
+ 3)))) by
A1
.= ((((2
|^ (n
+ 1))
/ (n
+ 3))
+ (((n
+ 2)
* (2
|^ (n
+ 1)))
/ ((n
+ 3)
* (n
+ 4))))
- (1
/ 2))
.= (((((2
|^ (n
+ 1))
* (n
+ 4))
/ ((n
+ 3)
* (n
+ 4)))
+ (((n
+ 2)
* (2
|^ (n
+ 1)))
/ ((n
+ 3)
* (n
+ 4))))
- (1
/ 2)) by
A4,
XCMPLX_1: 91
.= (((((2
|^ (n
+ 1))
* (n
+ 4))
+ ((n
+ 2)
* (2
|^ (n
+ 1))))
/ ((n
+ 3)
* (n
+ 4)))
- (1
/ 2)) by
XCMPLX_1: 62
.= (((((2
|^ (n
+ 1))
* 2)
* (n
+ 3))
/ ((n
+ 4)
* (n
+ 3)))
- (1
/ 2))
.= ((((2
|^ (n
+ 1))
* 2)
/ (n
+ 4))
- (1
/ 2)) by
A3,
XCMPLX_1: 91
.= (((2
|^ ((n
+ 1)
+ 1))
/ ((n
+ 1)
+ 3))
- (1
/ 2)) by
NEWTON: 6;
hence thesis;
end;
((
Partial_Sums s)
.
0 )
= (s
.
0 ) by
SERIES_1:def 1
.= (((
0
+ 1)
* (2
|^
0 ))
/ ((
0
+ 2)
* (
0
+ 3))) by
A1
.= ((1
* 1)
/ 6) by
NEWTON: 4
.= ((2
/ 3)
- (1
/ 2))
.= (((2
|^ (
0
+ 1))
/ (
0
+ 3))
- (1
/ 2));
then
A5:
X[
0 ];
for n holds
X[n] from
NAT_1:sch 2(
A5,
A2);
hence thesis;
end;
theorem ::
SERIES_2:33
(for n holds (s
. n)
= (((n
|^ 2)
* (4
|^ n))
/ ((n
+ 1)
* (n
+ 2)))) implies for n st n
>= 1 holds ((
Partial_Sums s)
. n)
= ((2
/ 3)
+ (((n
- 1)
* (4
|^ (n
+ 1)))
/ (3
* (n
+ 2))))
proof
defpred
X[
Nat] means ((
Partial_Sums s)
. $1)
= ((2
/ 3)
+ ((($1
- 1)
* (4
|^ ($1
+ 1)))
/ (3
* ($1
+ 2))));
assume
A1: for n holds (s
. n)
= (((n
|^ 2)
* (4
|^ n))
/ ((n
+ 1)
* (n
+ 2)));
then
A2: (s
.
0 )
= (((
0
|^ 2)
* (4
|^
0 ))
/ ((
0
+ 1)
* (
0
+ 2)))
.= ((
0
* (4
|^
0 ))
/ (1
* 2)) by
NEWTON: 11
.=
0 ;
A3: for n be
Nat st n
>= 1 &
X[n] holds
X[(n
+ 1)]
proof
let n be
Nat;
assume that n
>= 1 and
A4: ((
Partial_Sums s)
. n)
= ((2
/ 3)
+ (((n
- 1)
* (4
|^ (n
+ 1)))
/ (3
* (n
+ 2))));
(n
+ 2)
>= 2 by
NAT_1: 11;
then
A5: (n
+ 2)
>
0 by
XXREAL_0: 2;
(n
+ 3)
>= 3 by
NAT_1: 11;
then
A6: (n
+ 3)
>
0 by
XXREAL_0: 2;
((
Partial_Sums s)
. (n
+ 1))
= (((2
/ 3)
+ (((n
- 1)
* (4
|^ (n
+ 1)))
/ (3
* (n
+ 2))))
+ (s
. (n
+ 1))) by
A4,
SERIES_1:def 1
.= (((2
/ 3)
+ (((n
- 1)
* (4
|^ (n
+ 1)))
/ (3
* (n
+ 2))))
+ ((((n
+ 1)
|^ 2)
* (4
|^ (n
+ 1)))
/ (((n
+ 1)
+ 1)
* ((n
+ 1)
+ 2)))) by
A1
.= (((2
/ 3)
+ ((((n
- 1)
* (4
|^ (n
+ 1)))
* (n
+ 3))
/ ((3
* (n
+ 2))
* (n
+ 3))))
+ ((((n
+ 1)
|^ 2)
* (4
|^ (n
+ 1)))
/ ((n
+ 2)
* (n
+ 3)))) by
A6,
XCMPLX_1: 91
.= (((2
/ 3)
+ ((((n
- 1)
* (4
|^ (n
+ 1)))
* (n
+ 3))
/ ((3
* (n
+ 2))
* (n
+ 3))))
+ (((((n
+ 1)
|^ 2)
* (4
|^ (n
+ 1)))
* 3)
/ (((n
+ 2)
* (n
+ 3))
* 3))) by
XCMPLX_1: 91
.= ((2
/ 3)
+ (((((n
- 1)
* (4
|^ (n
+ 1)))
* (n
+ 3))
/ ((3
* (n
+ 2))
* (n
+ 3)))
+ (((((n
+ 1)
|^ 2)
* (4
|^ (n
+ 1)))
* 3)
/ ((3
* (n
+ 2))
* (n
+ 3)))))
.= ((2
/ 3)
+ (((((n
- 1)
* (4
|^ (n
+ 1)))
* (n
+ 3))
+ ((((n
+ 1)
|^ 2)
* (4
|^ (n
+ 1)))
* 3))
/ ((3
* (n
+ 2))
* (n
+ 3)))) by
XCMPLX_1: 62
.= ((2
/ 3)
+ (((((n
- 1)
* (n
+ 3))
+ (((n
+ 1)
|^ 2)
* 3))
* (4
|^ (n
+ 1)))
/ ((3
* (n
+ 2))
* (n
+ 3))))
.= ((2
/ 3)
+ (((((n
- 1)
* (n
+ 3))
+ (((n
+ 1)
* (n
+ 1))
* 3))
* (4
|^ (n
+ 1)))
/ ((3
* (n
+ 2))
* (n
+ 3)))) by
WSIERP_1: 1
.= ((2
/ 3)
+ ((((4
* (4
|^ (n
+ 1)))
* n)
* (n
+ 2))
/ ((3
* (n
+ 3))
* (n
+ 2))))
.= ((2
/ 3)
+ ((((4
|^ (n
+ 1))
* 4)
* n)
/ (3
* (n
+ 3)))) by
A5,
XCMPLX_1: 91
.= ((2
/ 3)
+ ((((n
+ 1)
- 1)
* (4
|^ ((n
+ 1)
+ 1)))
/ (3
* ((n
+ 1)
+ 2)))) by
NEWTON: 6;
hence thesis;
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
.= (((1
|^ 2)
* (4
|^ 1))
/ ((1
+ 1)
* (1
+ 2))) by
A1,
A2
.= ((1
* (4
|^ 1))
/ ((1
+ 1)
* (1
+ 2)))
.= ((1
* 4)
/ ((1
+ 1)
* (1
+ 2)))
.= ((2
/ 3)
+ (((1
- 1)
* (4
|^ (1
+ 1)))
/ (3
* (1
+ 2))));
then
A7:
X[1];
for n be
Nat st n
>= 1 holds
X[n] from
NAT_1:sch 8(
A7,
A3);
hence thesis;
end;
theorem ::
SERIES_2:34
(for n holds (s
. n)
= ((n
+ 2)
/ ((n
* (n
+ 1))
* (2
|^ n)))) implies for n st n
>= 1 holds ((
Partial_Sums s)
. n)
= (1
- (1
/ ((n
+ 1)
* (2
|^ n))))
proof
defpred
X[
Nat] means ((
Partial_Sums s)
. $1)
= (1
- (1
/ (($1
+ 1)
* (2
|^ $1))));
assume
A1: for n holds (s
. n)
= ((n
+ 2)
/ ((n
* (n
+ 1))
* (2
|^ n)));
then
A2: (s
.
0 )
= ((
0
+ 2)
/ ((
0
* (
0
+ 1))
* (2
|^
0 )))
.=
0 by
XCMPLX_1: 49;
A3: for n be
Nat st n
>= 1 &
X[n] holds
X[(n
+ 1)]
proof
let n be
Nat;
assume that n
>= 1 and
A4: ((
Partial_Sums s)
. n)
= (1
- (1
/ ((n
+ 1)
* (2
|^ n))));
(n
+ 1)
>= (1
+
0 ) by
NAT_1: 11;
then
A5: (n
+ 1)
>
0 by
NAT_1: 13;
(n
+ 2)
>= 2 by
NAT_1: 11;
then
A6: (n
+ 2)
>
0 by
XXREAL_0: 2;
((
Partial_Sums s)
. (n
+ 1))
= ((1
- (1
/ ((n
+ 1)
* (2
|^ n))))
+ (s
. (n
+ 1))) by
A4,
SERIES_1:def 1
.= ((1
- (1
/ ((n
+ 1)
* (2
|^ n))))
+ (((n
+ 1)
+ 2)
/ (((n
+ 1)
* ((n
+ 1)
+ 1))
* (2
|^ (n
+ 1))))) by
A1
.= (1
- ((1
/ ((n
+ 1)
* (2
|^ n)))
- ((n
+ 3)
/ (((n
+ 1)
* (n
+ 2))
* (2
|^ (n
+ 1))))))
.= (1
- (((1
* 2)
/ (((n
+ 1)
* (2
|^ n))
* 2))
- ((n
+ 3)
/ (((n
+ 1)
* (n
+ 2))
* (2
|^ (n
+ 1)))))) by
XCMPLX_1: 91
.= (1
- (((1
* 2)
/ ((n
+ 1)
* ((2
|^ n)
* 2)))
- ((n
+ 3)
/ (((n
+ 1)
* (n
+ 2))
* (2
|^ (n
+ 1))))))
.= (1
- (((1
* 2)
/ ((n
+ 1)
* (2
|^ (n
+ 1))))
- ((n
+ 3)
/ (((n
+ 1)
* (n
+ 2))
* (2
|^ (n
+ 1)))))) by
NEWTON: 6
.= (1
- (((2
* (n
+ 2))
/ (((n
+ 1)
* (2
|^ (n
+ 1)))
* (n
+ 2)))
- ((n
+ 3)
/ (((n
+ 1)
* (n
+ 2))
* (2
|^ (n
+ 1)))))) by
A6,
XCMPLX_1: 91
.= (1
- (((2
* (n
+ 2))
- (n
+ 3))
/ (((n
+ 1)
* (n
+ 2))
* (2
|^ (n
+ 1))))) by
XCMPLX_1: 120
.= (1
- ((1
* (n
+ 1))
/ (((n
+ 2)
* (2
|^ (n
+ 1)))
* (n
+ 1))))
.= (1
- (1
/ (((n
+ 1)
+ 1)
* (2
|^ (n
+ 1))))) by
A5,
XCMPLX_1: 91;
hence thesis;
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
.= ((1
+ 2)
/ ((1
* (1
+ 1))
* (2
|^ 1))) by
A1,
A2
.= ((1
+ 2)
/ ((1
* (1
+ 1))
* 2))
.= (1
- (1
/ ((1
+ 1)
* 2)))
.= (1
- (1
/ ((1
+ 1)
* (2
|^ 1))));
then
A7:
X[1];
for n be
Nat st n
>= 1 holds
X[n] from
NAT_1:sch 8(
A7,
A3);
hence thesis;
end;
theorem ::
SERIES_2:35
(for n holds (s
. n)
= (((2
* n)
+ 3)
/ ((n
* (n
+ 1))
* (3
|^ n)))) implies for n st n
>= 1 holds ((
Partial_Sums s)
. n)
= (1
- (1
/ ((n
+ 1)
* (3
|^ n))))
proof
defpred
X[
Nat] means ((
Partial_Sums s)
. $1)
= (1
- (1
/ (($1
+ 1)
* (3
|^ $1))));
assume
A1: for n holds (s
. n)
= (((2
* n)
+ 3)
/ ((n
* (n
+ 1))
* (3
|^ n)));
then
A2: (s
.
0 )
= (((2
*
0 )
+ 3)
/ ((
0
* (
0
+ 1))
* (3
|^
0 )))
.=
0 by
XCMPLX_1: 49;
A3: for n be
Nat st n
>= 1 &
X[n] holds
X[(n
+ 1)]
proof
let n be
Nat;
assume that n
>= 1 and
A4: ((
Partial_Sums s)
. n)
= (1
- (1
/ ((n
+ 1)
* (3
|^ n))));
(n
+ 1)
>= (1
+
0 ) by
NAT_1: 11;
then
A5: (n
+ 1)
>
0 by
NAT_1: 13;
(n
+ 2)
>= 2 by
NAT_1: 11;
then
A6: (n
+ 2)
>
0 by
XXREAL_0: 2;
((
Partial_Sums s)
. (n
+ 1))
= ((1
- (1
/ ((n
+ 1)
* (3
|^ n))))
+ (s
. (n
+ 1))) by
A4,
SERIES_1:def 1
.= ((1
- (1
/ ((n
+ 1)
* (3
|^ n))))
+ (((2
* (n
+ 1))
+ 3)
/ (((n
+ 1)
* ((n
+ 1)
+ 1))
* (3
|^ (n
+ 1))))) by
A1
.= ((1
- ((1
* 3)
/ (((n
+ 1)
* (3
|^ n))
* 3)))
+ (((2
* n)
+ 5)
/ (((n
+ 1)
* (n
+ 2))
* (3
|^ (n
+ 1))))) by
XCMPLX_1: 91
.= ((1
- (3
/ ((n
+ 1)
* ((3
|^ n)
* 3))))
+ (((2
* n)
+ 5)
/ (((n
+ 1)
* (n
+ 2))
* (3
|^ (n
+ 1)))))
.= ((1
- (3
/ ((n
+ 1)
* (3
|^ (n
+ 1)))))
+ (((2
* n)
+ 5)
/ (((n
+ 1)
* (n
+ 2))
* (3
|^ (n
+ 1))))) by
NEWTON: 6
.= ((1
- ((3
* (n
+ 2))
/ (((n
+ 1)
* (3
|^ (n
+ 1)))
* (n
+ 2))))
+ (((2
* n)
+ 5)
/ (((n
+ 1)
* (n
+ 2))
* (3
|^ (n
+ 1))))) by
A6,
XCMPLX_1: 91
.= (1
- (((3
* (n
+ 2))
/ (((n
+ 1)
* (3
|^ (n
+ 1)))
* (n
+ 2)))
- (((2
* n)
+ 5)
/ (((n
+ 1)
* (n
+ 2))
* (3
|^ (n
+ 1))))))
.= (1
- (((3
* (n
+ 2))
- ((2
* n)
+ 5))
/ (((n
+ 1)
* (n
+ 2))
* (3
|^ (n
+ 1))))) by
XCMPLX_1: 120
.= (1
- ((1
* (n
+ 1))
/ (((n
+ 2)
* (3
|^ (n
+ 1)))
* (n
+ 1))))
.= (1
- (1
/ (((n
+ 1)
+ 1)
* (3
|^ (n
+ 1))))) by
A5,
XCMPLX_1: 91;
hence thesis;
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
.= (((2
* 1)
+ 3)
/ ((1
* (1
+ 1))
* (3
|^ 1))) by
A1,
A2
.= (((2
* 1)
+ 3)
/ ((1
* (1
+ 1))
* 3))
.= (1
- (1
/ ((1
+ 1)
* 3)))
.= (1
- (1
/ ((1
+ 1)
* (3
|^ 1))));
then
A7:
X[1];
for n be
Nat st n
>= 1 holds
X[n] from
NAT_1:sch 8(
A7,
A3);
hence thesis;
end;
theorem ::
SERIES_2:36
(for n holds (s
. n)
= ((((
- 1)
|^ n)
* (2
|^ (n
+ 1)))
/ (((2
|^ (n
+ 1))
+ ((
- 1)
|^ (n
+ 1)))
* ((2
|^ (n
+ 2))
+ ((
- 1)
|^ (n
+ 2)))))) implies for n holds ((
Partial_Sums s)
. n)
= ((1
/ 3)
+ (((
- 1)
|^ (n
+ 2))
/ (3
* ((2
|^ (n
+ 2))
+ ((
- 1)
|^ (n
+ 2))))))
proof
defpred
X[
Nat] means ((
Partial_Sums s)
. $1)
= ((1
/ 3)
+ (((
- 1)
|^ ($1
+ 2))
/ (3
* ((2
|^ ($1
+ 2))
+ ((
- 1)
|^ ($1
+ 2))))));
assume
A1: for n holds (s
. n)
= ((((
- 1)
|^ n)
* (2
|^ (n
+ 1)))
/ (((2
|^ (n
+ 1))
+ ((
- 1)
|^ (n
+ 1)))
* ((2
|^ (n
+ 2))
+ ((
- 1)
|^ (n
+ 2)))));
A2: for n st
X[n] holds
X[(n
+ 1)]
proof
let n;
set b = ((2
|^ (n
+ 2))
+ ((
- 1)
|^ (n
+ 2)));
set p = ((2
|^ (n
+ 3))
+ ((
- 1)
|^ (n
+ 3)));
A3: b
>
0 by
Lm18;
assume ((
Partial_Sums s)
. n)
= ((1
/ 3)
+ (((
- 1)
|^ (n
+ 2))
/ (3
* ((2
|^ (n
+ 2))
+ ((
- 1)
|^ (n
+ 2))))));
then
A4: ((
Partial_Sums s)
. (n
+ 1))
= (((1
/ 3)
+ (((
- 1)
|^ (n
+ 2))
/ (3
* ((2
|^ (n
+ 2))
+ ((
- 1)
|^ (n
+ 2))))))
+ (s
. (n
+ 1))) by
SERIES_1:def 1
.= (((1
/ 3)
+ (((
- 1)
|^ (n
+ 2))
/ (3
* ((2
|^ (n
+ 2))
+ ((
- 1)
|^ (n
+ 2))))))
+ ((((
- 1)
|^ (n
+ 1))
* (2
|^ ((n
+ 1)
+ 1)))
/ (((2
|^ ((n
+ 1)
+ 1))
+ ((
- 1)
|^ ((n
+ 1)
+ 1)))
* ((2
|^ ((n
+ 1)
+ 2))
+ ((
- 1)
|^ ((n
+ 1)
+ 2)))))) by
A1
.= (((1
/ 3)
+ (((
- 1)
|^ (n
+ 2))
/ (3
* ((2
|^ (n
+ 2))
+ ((
- 1)
|^ (n
+ 2))))))
+ ((((
- 1)
|^ (n
+ 1))
* (2
|^ (n
+ 2)))
/ (((2
|^ (n
+ 2))
+ ((
- 1)
|^ (n
+ 2)))
* ((2
|^ (n
+ 3))
+ ((
- 1)
|^ (n
+ 3))))));
p
>
0 by
Lm19;
then ((
Partial_Sums s)
. (n
+ 1))
= (((1
/ 3)
+ ((((
- 1)
|^ (n
+ 2))
* p)
/ ((3
* b)
* p)))
+ ((((
- 1)
|^ (n
+ 1))
* (2
|^ (n
+ 2)))
/ (b
* p))) by
A4,
XCMPLX_1: 91
.= (((1
/ 3)
+ ((((
- 1)
|^ (n
+ 2))
* p)
/ ((3
* b)
* p)))
+ (((((
- 1)
|^ (n
+ 1))
* (2
|^ (n
+ 2)))
* 3)
/ ((b
* p)
* 3))) by
XCMPLX_1: 91
.= ((1
/ 3)
+ (((((
- 1)
|^ (n
+ 2))
* p)
/ ((3
* b)
* p))
+ (((((
- 1)
|^ (n
+ 1))
* (2
|^ (n
+ 2)))
* 3)
/ ((3
* b)
* p))))
.= ((1
/ 3)
+ (((((((
- 1)
|^ (n
+ 2))
* (
- 1))
/ (
- 1))
* p)
+ ((((
- 1)
|^ (n
+ 1))
* (2
|^ (n
+ 2)))
* 3))
/ ((3
* b)
* p))) by
XCMPLX_1: 62
.= ((1
/ 3)
+ ((((((
- 1)
|^ ((n
+ 2)
+ 1))
/ (
- 1))
* p)
+ ((((
- 1)
|^ (n
+ 1))
* (2
|^ (n
+ 2)))
* 3))
/ ((3
* b)
* p))) by
NEWTON: 6
.= ((1
/ 3)
+ ((((((
- 1)
|^ (n
+ 3))
/ (
- 1))
* p)
+ ((((((
- 1)
|^ (n
+ 1))
* (
- 1))
/ (
- 1))
* (2
|^ (n
+ 2)))
* 3))
/ ((3
* b)
* p)))
.= ((1
/ 3)
+ ((((((
- 1)
|^ (n
+ 3))
/ (
- 1))
* p)
+ (((((
- 1)
|^ ((n
+ 1)
+ 1))
/ (
- 1))
* (2
|^ (n
+ 2)))
* 3))
/ ((3
* b)
* p))) by
NEWTON: 6
.= ((1
/ 3)
+ ((((((
- 1)
|^ (n
+ 3))
/ (
- 1))
* p)
+ ((((((
- 1)
|^ (n
+ 2))
* (
- 1))
/ ((
- 1)
* (
- 1)))
* (2
|^ (n
+ 2)))
* 3))
/ ((3
* b)
* p)))
.= ((1
/ 3)
+ ((((((
- 1)
|^ (n
+ 3))
/ (
- 1))
* p)
+ (((((
- 1)
|^ ((n
+ 2)
+ 1))
/ ((
- 1)
* (
- 1)))
* (2
|^ (n
+ 2)))
* 3))
/ ((3
* b)
* p))) by
NEWTON: 6
.= ((1
/ 3)
+ ((((
- 1)
|^ (n
+ 3))
* ((((2
|^ (n
+ 2))
+ ((2
|^ (n
+ 2))
* 2))
- (2
|^ (n
+ 3)))
- ((
- 1)
|^ (n
+ 3))))
/ ((3
* b)
* p)))
.= ((1
/ 3)
+ ((((
- 1)
|^ (n
+ 3))
* ((((2
|^ (n
+ 2))
+ (2
|^ ((n
+ 2)
+ 1)))
- (2
|^ (n
+ 3)))
- ((
- 1)
|^ (n
+ 3))))
/ ((3
* b)
* p))) by
NEWTON: 6
.= ((1
/ 3)
+ ((((
- 1)
|^ (n
+ 3))
* ((2
|^ (n
+ 2))
- (((
- 1)
|^ (n
+ 2))
* (
- 1))))
/ ((3
* b)
* p))) by
NEWTON: 6
.= ((1
/ 3)
+ ((((
- 1)
|^ (n
+ 3))
* b)
/ ((3
* p)
* b)))
.= ((1
/ 3)
+ (((
- 1)
|^ ((n
+ 2)
+ 1))
/ (3
* ((2
|^ ((n
+ 2)
+ 1))
+ ((
- 1)
|^ ((n
+ 2)
+ 1)))))) by
A3,
XCMPLX_1: 91;
hence thesis;
end;
((
Partial_Sums s)
.
0 )
= (s
.
0 ) by
SERIES_1:def 1
.= ((((
- 1)
|^
0 )
* (2
|^ (
0
+ 1)))
/ (((2
|^ (
0
+ 1))
+ ((
- 1)
|^ (
0
+ 1)))
* ((2
|^ (
0
+ 2))
+ ((
- 1)
|^ (
0
+ 2))))) by
A1
.= ((1
* (2
|^ (
0
+ 1)))
/ (((2
|^ (
0
+ 1))
+ ((
- 1)
|^ (
0
+ 1)))
* ((2
|^ (
0
+ 2))
+ ((
- 1)
|^ (
0
+ 2))))) by
NEWTON: 4
.= ((1
* 2)
/ (((2
|^ (
0
+ 1))
+ ((
- 1)
|^ (
0
+ 1)))
* ((2
|^ (
0
+ 2))
+ ((
- 1)
|^ (
0
+ 2)))))
.= ((1
* 2)
/ ((2
+ ((
- 1)
|^ (
0
+ 1)))
* ((2
|^ (
0
+ 2))
+ ((
- 1)
|^ (
0
+ 2)))))
.= ((1
* 2)
/ ((2
+ (
- 1))
* ((2
|^ (
0
+ 2))
+ ((
- 1)
|^ (
0
+ 2)))))
.= ((1
* 2)
/ ((2
+ (
- 1))
* ((2
* 2)
+ ((
- 1)
|^ (
0
+ 2))))) by
WSIERP_1: 1
.= ((1
* 2)
/ ((2
+ (
- 1))
* ((2
* 2)
+ ((
- 1)
* (
- 1))))) by
WSIERP_1: 1
.= ((1
/ 3)
+ (((
- 1)
* (
- 1))
/ (3
* ((2
* 2)
+ ((
- 1)
* (
- 1))))))
.= ((1
/ 3)
+ (((
- 1)
|^ 2)
/ (3
* ((2
* 2)
+ ((
- 1)
* (
- 1)))))) by
WSIERP_1: 1
.= ((1
/ 3)
+ (((
- 1)
|^ 2)
/ (3
* ((2
* 2)
+ ((
- 1)
|^ 2))))) by
WSIERP_1: 1
.= ((1
/ 3)
+ (((
- 1)
|^ (
0
+ 2))
/ (3
* ((2
|^ (
0
+ 2))
+ ((
- 1)
|^ (
0
+ 2)))))) by
WSIERP_1: 1;
then
A5:
X[
0 ];
for n holds
X[n] from
NAT_1:sch 2(
A5,
A2);
hence thesis;
end;
theorem ::
SERIES_2:37
(for n holds (s
. n)
= ((n
! )
* n)) implies for n st n
>= 1 holds ((
Partial_Sums s)
. n)
= (((n
+ 1)
! )
- 1)
proof
defpred
X[
Nat] means ((
Partial_Sums s)
. $1)
= ((($1
+ 1)
! )
- 1);
assume
A1: for n holds (s
. n)
= ((n
! )
* n);
then
A2: (s
.
0 )
= ((
0
! )
*
0 )
.=
0 ;
A3: for n be
Nat st n
>= 1 &
X[n] holds
X[(n
+ 1)]
proof
let n be
Nat;
assume that n
>= 1 and
A4: ((
Partial_Sums s)
. n)
= (((n
+ 1)
! )
- 1);
((
Partial_Sums s)
. (n
+ 1))
= ((((n
+ 1)
! )
- 1)
+ (s
. (n
+ 1))) by
A4,
SERIES_1:def 1
.= ((((n
+ 1)
! )
- 1)
+ (((n
+ 1)
! )
* (n
+ 1))) by
A1
.= ((((n
+ 1)
! )
* ((n
+ 1)
+ 1))
- 1)
.= ((((n
+ 1)
+ 1)
! )
- 1) by
NEWTON: 15;
hence thesis;
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
.= ((1
! )
* 1) by
A1,
A2
.= (((1
+ 1)
! )
- 1) by
NEWTON: 13,
NEWTON: 14;
then
A5:
X[1];
for n be
Nat st n
>= 1 holds
X[n] from
NAT_1:sch 8(
A5,
A3);
hence thesis;
end;
theorem ::
SERIES_2:38
(for n holds (s
. n)
= (n
/ ((n
+ 1)
! ))) implies for n st n
>= 1 holds ((
Partial_Sums s)
. n)
= (1
- (1
/ ((n
+ 1)
! )))
proof
defpred
X[
Nat] means ((
Partial_Sums s)
. $1)
= (1
- (1
/ (($1
+ 1)
! )));
assume
A1: for n holds (s
. n)
= (n
/ ((n
+ 1)
! ));
then
A2: (s
.
0 )
= (
0
/ ((
0
+ 1)
! ))
.=
0 ;
A3: for n be
Nat st n
>= 1 &
X[n] holds
X[(n
+ 1)]
proof
let n be
Nat;
assume that n
>= 1 and
A4: ((
Partial_Sums s)
. n)
= (1
- (1
/ ((n
+ 1)
! )));
(n
+ 2)
>= 2 by
NAT_1: 11;
then
A5: (n
+ 2)
>
0 by
XXREAL_0: 2;
((
Partial_Sums s)
. (n
+ 1))
= ((1
- (1
/ ((n
+ 1)
! )))
+ (s
. (n
+ 1))) by
A4,
SERIES_1:def 1
.= ((1
- (1
/ ((n
+ 1)
! )))
+ ((n
+ 1)
/ (((n
+ 1)
+ 1)
! ))) by
A1
.= ((1
- ((1
* (n
+ 2))
/ (((n
+ 1)
! )
* ((n
+ 1)
+ 1))))
+ ((n
+ 1)
/ ((n
+ 2)
! ))) by
A5,
XCMPLX_1: 91
.= ((1
- ((1
* (n
+ 2))
/ (((n
+ 1)
+ 1)
! )))
+ ((n
+ 1)
/ ((n
+ 2)
! ))) by
NEWTON: 15
.= (1
- (((n
+ 2)
/ (((n
+ 1)
+ 1)
! ))
- ((n
+ 1)
/ ((n
+ 2)
! ))))
.= (1
- (((n
+ 2)
- (n
+ 1))
/ ((n
+ 2)
! ))) by
XCMPLX_1: 120
.= (1
- (1
/ (((n
+ 1)
+ 1)
! )));
hence thesis;
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
.= (1
- (1
/ ((1
+ 1)
! ))) by
A1,
A2,
NEWTON: 14;
then
A6:
X[1];
for n be
Nat st n
>= 1 holds
X[n] from
NAT_1:sch 8(
A6,
A3);
hence thesis;
end;
theorem ::
SERIES_2:39
(for n st n
>= 1 holds (s
. n)
= ((((n
|^ 2)
+ n)
- 1)
/ ((n
+ 2)
! )) & (s
.
0 )
=
0 ) implies for n st n
>= 1 holds ((
Partial_Sums s)
. n)
= ((1
/ 2)
- ((n
+ 1)
/ ((n
+ 2)
! )))
proof
defpred
X[
Nat] means ((
Partial_Sums s)
. $1)
= ((1
/ 2)
- (($1
+ 1)
/ (($1
+ 2)
! )));
assume
A1: for n st n
>= 1 holds (s
. n)
= ((((n
|^ 2)
+ n)
- 1)
/ ((n
+ 2)
! )) & (s
.
0 )
=
0 ;
A2: for n be
Nat st n
>= 1 &
X[n] holds
X[(n
+ 1)]
proof
let n be
Nat;
assume that n
>= 1 and
A3: ((
Partial_Sums s)
. n)
= ((1
/ 2)
- ((n
+ 1)
/ ((n
+ 2)
! )));
A4: (n
+ 1)
>= 1 by
NAT_1: 11;
(n
+ 3)
>= 3 by
NAT_1: 11;
then
A5: (n
+ 3)
>
0 by
XXREAL_0: 2;
((
Partial_Sums s)
. (n
+ 1))
= (((1
/ 2)
- ((n
+ 1)
/ ((n
+ 2)
! )))
+ (s
. (n
+ 1))) by
A3,
SERIES_1:def 1
.= (((1
/ 2)
- ((n
+ 1)
/ ((n
+ 2)
! )))
+ (((((n
+ 1)
|^ 2)
+ (n
+ 1))
- 1)
/ (((n
+ 1)
+ 2)
! ))) by
A1,
A4
.= (((1
/ 2)
- (((n
+ 1)
* (n
+ 3))
/ (((n
+ 2)
! )
* ((n
+ 2)
+ 1))))
+ ((((n
+ 1)
|^ 2)
+ n)
/ ((n
+ 3)
! ))) by
A5,
XCMPLX_1: 91
.= (((1
/ 2)
- (((n
+ 1)
* (n
+ 3))
/ (((n
+ 2)
+ 1)
! )))
+ ((((n
+ 1)
|^ 2)
+ n)
/ ((n
+ 3)
! ))) by
NEWTON: 15
.= ((1
/ 2)
- ((((n
+ 1)
* (n
+ 3))
/ ((n
+ 3)
! ))
- ((((n
+ 1)
|^ 2)
+ n)
/ ((n
+ 3)
! ))))
.= ((1
/ 2)
- ((((n
+ 1)
* (n
+ 3))
- (((n
+ 1)
|^ 2)
+ n))
/ ((n
+ 3)
! ))) by
XCMPLX_1: 120
.= ((1
/ 2)
- (((((n
+ 1)
* (n
+ 3))
- ((n
+ 1)
|^ 2))
- n)
/ ((n
+ 3)
! )))
.= ((1
/ 2)
- (((((n
+ 1)
* (n
+ 3))
- ((n
+ 1)
* (n
+ 1)))
- n)
/ ((n
+ 3)
! ))) by
WSIERP_1: 1
.= ((1
/ 2)
- (((n
+ 1)
+ 1)
/ (((n
+ 1)
+ 2)
! )));
hence thesis;
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
|^ 2)
+ 1)
- 1)
/ ((1
+ 2)
! )) by
A1
.= ((1
* 1)
/ ((2
+ 1)
! ))
.= (1
/ (2
* 3)) by
NEWTON: 14,
NEWTON: 15
.= ((1
/ 2)
- (2
/ ((2
! )
* (2
+ 1)))) by
NEWTON: 14
.= ((1
/ 2)
- (2
/ ((2
+ 1)
! ))) by
NEWTON: 15;
then
A6:
X[1];
for n be
Nat st n
>= 1 holds
X[n] from
NAT_1:sch 8(
A6,
A2);
hence thesis;
end;
theorem ::
SERIES_2:40
(for n holds (s
. n)
= ((n
* (2
|^ n))
/ ((n
+ 2)
! ))) implies for n st n
>= 1 holds ((
Partial_Sums s)
. n)
= (1
- ((2
|^ (n
+ 1))
/ ((n
+ 2)
! )))
proof
defpred
X[
Nat] means ((
Partial_Sums s)
. $1)
= (1
- ((2
|^ ($1
+ 1))
/ (($1
+ 2)
! )));
assume
A1: for n holds (s
. n)
= ((n
* (2
|^ n))
/ ((n
+ 2)
! ));
then
A2: (s
.
0 )
= ((
0
* (2
|^
0 ))
/ ((
0
+ 2)
! ))
.=
0 ;
A3: for n be
Nat st n
>= 1 &
X[n] holds
X[(n
+ 1)]
proof
let n be
Nat;
assume that n
>= 1 and
A4: ((
Partial_Sums s)
. n)
= (1
- ((2
|^ (n
+ 1))
/ ((n
+ 2)
! )));
(n
+ 3)
>= 3 by
NAT_1: 11;
then
A5: (n
+ 3)
>
0 by
XXREAL_0: 2;
((
Partial_Sums s)
. (n
+ 1))
= ((1
- ((2
|^ (n
+ 1))
/ ((n
+ 2)
! )))
+ (s
. (n
+ 1))) by
A4,
SERIES_1:def 1
.= ((1
- ((2
|^ (n
+ 1))
/ ((n
+ 2)
! )))
+ (((n
+ 1)
* (2
|^ (n
+ 1)))
/ (((n
+ 1)
+ 2)
! ))) by
A1
.= ((1
- (((2
|^ (n
+ 1))
* (n
+ 3))
/ (((n
+ 2)
! )
* ((n
+ 2)
+ 1))))
+ (((n
+ 1)
* (2
|^ (n
+ 1)))
/ ((n
+ 3)
! ))) by
A5,
XCMPLX_1: 91
.= ((1
- (((2
|^ (n
+ 1))
* (n
+ 3))
/ (((n
+ 2)
+ 1)
! )))
+ (((n
+ 1)
* (2
|^ (n
+ 1)))
/ ((n
+ 3)
! ))) by
NEWTON: 15
.= (1
- ((((2
|^ (n
+ 1))
* (n
+ 3))
/ (((n
+ 2)
+ 1)
! ))
- (((n
+ 1)
* (2
|^ (n
+ 1)))
/ ((n
+ 3)
! ))))
.= (1
- ((((2
|^ (n
+ 1))
* (n
+ 3))
- ((2
|^ (n
+ 1))
* (n
+ 1)))
/ ((n
+ 3)
! ))) by
XCMPLX_1: 120
.= (1
- (((2
|^ (n
+ 1))
* 2)
/ ((n
+ 3)
! )))
.= (1
- ((2
|^ ((n
+ 1)
+ 1))
/ (((n
+ 1)
+ 2)
! ))) by
NEWTON: 6;
hence thesis;
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
.= ((1
* (2
|^ 1))
/ ((1
+ 2)
! )) by
A1,
A2
.= (2
/ ((2
+ 1)
! ))
.= (2
/ (2
* 3)) by
NEWTON: 14,
NEWTON: 15
.= (1
- ((2
* 2)
/ ((2
! )
* (2
+ 1)))) by
NEWTON: 14
.= (1
- ((2
|^ 2)
/ ((2
! )
* (2
+ 1)))) by
WSIERP_1: 1
.= (1
- ((2
|^ (1
+ 1))
/ ((1
+ 2)
! ))) by
NEWTON: 15;
then
A6:
X[1];
for n be
Nat st n
>= 1 holds
X[n] from
NAT_1:sch 8(
A6,
A3);
hence thesis;
end;
theorem ::
SERIES_2:41
(for n holds (s
. n)
= ((a
* n)
+ b)) implies for n holds ((
Partial_Sums s)
. n)
= (((((a
* (n
+ 1))
* n)
/ 2)
+ (n
* b))
+ b) by
Lm14;
::$Notion-Name
theorem ::
SERIES_2:42
(for n holds (s
. n)
= ((a
* n)
+ b)) implies for n holds ((
Partial_Sums s)
. n)
= (((n
+ 1)
* ((s
.
0 )
+ (s
. n)))
/ 2)
proof
assume
A1: for n holds (s
. n)
= ((a
* n)
+ b);
let n;
((
Partial_Sums s)
. n)
= (((((a
* (n
+ 1))
* n)
/ 2)
+ (n
* b))
+ b) by
A1,
Lm14
.= (((n
+ 1)
* (((n
* a)
+ b)
+ b))
/ 2)
.= (((n
+ 1)
* ((s
. n)
+ ((a
*
0 )
+ b)))
/ 2) by
A1
.= (((n
+ 1)
* ((s
. n)
+ (s
.
0 )))
/ 2) by
A1;
hence thesis;
end;