:: Partial Sum of Some Series
:: by Ming Liang and Yuzhong Ding
::
:: Received September 25, 2004
:: Copyright (c) 2004-2021 Association of Mizar Users

theorem Th1: :: SERIES_2:1

for n being Nat holds |.((- 1) |^ n).| = 1

proof end;

Lm1: for a being Real holds a |^ 3 = (a * a) * a

proof end;

Lm2: for a being Real holds a |^ 3 = (a |^ 2) * a

proof end;

Lm3: for a, b being Real holds
( 4 = 2 |^ 2 & (a + b) |^ 2 = ((a |^ 2) + ((2 * a) * b)) + (b |^ 2) )

proof end;

Lm4: for a being Real holds (a + 1) |^ 3 = (((a |^ 3) + (3 * (a |^ 2))) + (3 * a)) + 1

proof end;

Lm5: for n being Nat holds ((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 end;

Lm6: for n being 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 end;

theorem :: SERIES_2:2

for n being 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 being Nat holds
( 1 - (1 / (n + 2)) = (n + 1) / (n + 2) & 1 / ((n + 1) !) = (n + 2) / (((n + 1) !) * (n + 2)) )

proof end;

Lm8: for n being Nat holds (1 / (n + 1)) - (2 / ((n + 1) * (n + 3))) = 1 / (n + 3)

proof end;

Lm9: for n being Nat holds (1 / (n + 1)) - (3 / ((n + 1) * (n + 4))) = 1 / (n + 4)

proof end;

Lm10: for n being Nat holds ((n |^ 2) + (3 * n)) + 2 = (n + 1) * (n + 2)

proof end;

Lm11: for n being Nat holds (((n * (4 * (n |^ 2))) + (11 * n)) + (12 * (n |^ 2))) + 3 = (n + 1) * ((4 * ((n + 1) |^ 2)) - 1)

proof end;

Lm12: for n being Nat holds ((n + 1) |^ 2) * ((2 * ((n + 1) |^ 2)) - 1) = ((((((n |^ 2) * (n |^ 2)) * 2) + ((12 - 1) * (n |^ 2))) + (8 * (n |^ 3))) + (6 * n)) + 1

proof end;

Lm13: for n being Nat holds (n + 2) * ((((n + 1) |^ 2) + (n + 1)) - 1) = (((n |^ 3) + (5 * (n |^ 2))) + (7 * n)) + 2

proof end;

Lm14: for a, b being Real
for s being Real_Sequence st ( for n being Nat holds s . n = (a * n) + b ) holds
for n being Nat holds (Partial_Sums s) . n = ((((a * (n + 1)) * n) / 2) + (n * b)) + b

proof end;

theorem :: SERIES_2:3

for s being Real_Sequence st ( for n being Nat holds s . n = n ) holds
for n being Nat holds (Partial_Sums s) . n = (n * (n + 1)) / 2

proof end;

theorem :: SERIES_2:4

for s being Real_Sequence st ( for n being Nat holds s . n = 2 * n ) holds
for n being Nat holds (Partial_Sums s) . n = n * (n + 1)

proof end;

theorem :: SERIES_2:5

for s being Real_Sequence st ( for n being Nat holds s . n = (2 * n) + 1 ) holds
for n being Nat holds (Partial_Sums s) . n = (n + 1) |^ 2

proof end;

theorem :: SERIES_2:6

for s being Real_Sequence st ( for n being Nat holds s . n = n * (n + 1) ) holds
for n being Nat holds (Partial_Sums s) . n = ((n * (n + 1)) * (n + 2)) / 3

proof end;

theorem :: SERIES_2:7

for s being Real_Sequence st ( for n being Nat holds s . n = (n * (n + 1)) * (n + 2) ) holds
for n being Nat holds (Partial_Sums s) . n = (((n * (n + 1)) * (n + 2)) * (n + 3)) / 4

proof end;

theorem :: SERIES_2:8

for s being Real_Sequence st ( for n being Nat holds s . n = ((n * (n + 1)) * (n + 2)) * (n + 3) ) holds
for n being Nat holds (Partial_Sums s) . n = ((((n * (n + 1)) * (n + 2)) * (n + 3)) * (n + 4)) / 5

proof end;

theorem :: SERIES_2:9

for s being Real_Sequence st ( for n being Nat holds s . n = 1 / (n * (n + 1)) ) holds
for n being Nat holds (Partial_Sums s) . n = 1 - (1 / (n + 1))

proof end;

theorem :: SERIES_2:10

for s being Real_Sequence st ( for n being Nat holds s . n = 1 / ((n * (n + 1)) * (n + 2)) ) holds
for n being Nat holds (Partial_Sums s) . n = (1 / 4) - (1 / ((2 * (n + 1)) * (n + 2)))

proof end;

theorem :: SERIES_2:11

for s being Real_Sequence st ( for n being Nat holds s . n = 1 / (((n * (n + 1)) * (n + 2)) * (n + 3)) ) holds
for n being Nat holds (Partial_Sums s) . n = (1 / 18) - (1 / (((3 * (n + 1)) * (n + 2)) * (n + 3)))

proof end;

theorem :: SERIES_2:12

for s being Real_Sequence st ( for n being Nat holds s . n = n |^ 2 ) holds
for n being Nat holds (Partial_Sums s) . n = ((n * (n + 1)) * ((2 * n) + 1)) / 6

proof end;

theorem :: SERIES_2:13

for s being Real_Sequence st ( for n being Nat holds s . n = ((- 1) |^ (n + 1)) * (n |^ 2) ) holds
for n being Nat holds (Partial_Sums s) . n = ((((- 1) |^ (n + 1)) * n) * (n + 1)) / 2

proof end;

theorem :: SERIES_2:14

for s being Real_Sequence st ( for n being Nat st n >= 1 holds
( s . n = ((2 * n) - 1) |^ 2 & s . 0 = 0 ) ) holds
for n being Nat st n >= 1 holds
(Partial_Sums s) . n = (n * ((4 * (n |^ 2)) - 1)) / 3

proof end;

theorem :: SERIES_2:15

for s being Real_Sequence st ( for n being Nat holds s . n = n |^ 3 ) holds
for n being Nat holds (Partial_Sums s) . n = ((n |^ 2) * ((n + 1) |^ 2)) / 4

proof end;

theorem :: SERIES_2:16

for s being Real_Sequence st ( for n being Nat st n >= 1 holds
( s . n = ((2 * n) - 1) |^ 3 & s . 0 = 0 ) ) holds
for n being Nat st n >= 1 holds
(Partial_Sums s) . n = (n |^ 2) * ((2 * (n |^ 2)) - 1)

proof end;

theorem :: SERIES_2:17

for s being Real_Sequence st ( for n being Nat holds s . n = n |^ 4 ) holds
for n being Nat holds (Partial_Sums s) . n = (((n * (n + 1)) * ((2 * n) + 1)) * (((3 * (n |^ 2)) + (3 * n)) - 1)) / 30

proof end;

theorem :: SERIES_2:18

for s being Real_Sequence st ( for n being Nat holds s . n = ((- 1) |^ (n + 1)) * (n |^ 4) ) holds
for n being Nat holds (Partial_Sums s) . n = (((((- 1) |^ (n + 1)) * n) * (n + 1)) * (((n |^ 2) + n) - 1)) / 2

proof end;

Lm15: for n being Nat holds ((n |^ 2) * (((2 * (n |^ 2)) + (2 * n)) - 1)) + (((n + 1) |^ 3) * 12) = ((n + 2) |^ 2) * (((2 * ((n + 1) |^ 2)) + (2 * (n + 1))) - 1)

proof end;

theorem :: SERIES_2:19

for s being Real_Sequence st ( for n being Nat holds s . n = n |^ 5 ) holds
for n being Nat holds (Partial_Sums s) . n = (((n |^ 2) * ((n + 1) |^ 2)) * (((2 * (n |^ 2)) + (2 * n)) - 1)) / 12

proof end;

Lm16: for n being Nat holds ((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 end;

theorem :: SERIES_2:20

for s being Real_Sequence st ( for n being Nat holds s . n = n |^ 6 ) holds
for n being Nat holds (Partial_Sums s) . n = (((n * (n + 1)) * ((2 * n) + 1)) * ((((3 * (n |^ 4)) + (6 * (n |^ 3))) - (3 * n)) + 1)) / 42

proof end;

Lm17: for n being Nat holds ((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 end;

Lm18: for n being Nat holds (2 |^ (n + 2)) + ((- 1) |^ (n + 2)) > 0

proof end;

Lm19: for n being Nat holds (2 |^ (n + 3)) + ((- 1) |^ (n + 3)) > 0

proof end;

theorem :: SERIES_2:21

for s being Real_Sequence st ( for n being Nat holds s . n = n |^ 7 ) holds
for n being Nat holds (Partial_Sums s) . n = (((n |^ 2) * ((n + 1) |^ 2)) * (((((3 * (n |^ 4)) + (6 * (n |^ 3))) - (n |^ 2)) - (4 * n)) + 2)) / 24

proof end;

theorem :: SERIES_2:22

for s being Real_Sequence st ( for n being Nat holds s . n = n * ((n + 1) |^ 2) ) holds
for n being Nat holds (Partial_Sums s) . n = (((n * (n + 1)) * (n + 2)) * ((3 * n) + 5)) / 12

proof end;

theorem :: SERIES_2:23

for s being Real_Sequence st ( for n being Nat holds s . n = (n * ((n + 1) |^ 2)) * (n + 2) ) holds
for n being Nat holds (Partial_Sums s) . n = ((((n * (n + 1)) * (n + 2)) * (n + 3)) * ((2 * n) + 3)) / 10

proof end;

theorem :: SERIES_2:24

for s being Real_Sequence st ( for n being Nat holds s . n = (n * (n + 1)) * (2 |^ n) ) holds
for n being Nat holds (Partial_Sums s) . n = ((2 |^ (n + 1)) * (((n |^ 2) - n) + 2)) - 4

proof end;

theorem :: SERIES_2:25

for s being Real_Sequence st ( for n being Nat st n >= 1 holds
( s . n = 1 / ((n - 1) * (n + 1)) & s . 0 = 0 ) ) holds
for n being Nat st n >= 2 holds
(Partial_Sums s) . n = ((3 / 4) - (1 / (2 * n))) - (1 / (2 * (n + 1)))

proof end;

theorem :: SERIES_2:26

for s being Real_Sequence st ( for n being Nat st n >= 1 holds
( s . n = 1 / (((2 * n) - 1) * ((2 * n) + 1)) & s . 0 = 0 ) ) holds
for n being Nat st n >= 1 holds
(Partial_Sums s) . n = n / ((2 * n) + 1)

proof end;

theorem :: SERIES_2:27

for s being Real_Sequence st ( for n being Nat st n >= 1 holds
( s . n = 1 / (((3 * n) - 2) * ((3 * n) + 1)) & s . 0 = 0 ) ) holds
for n being Nat st n >= 1 holds
(Partial_Sums s) . n = n / ((3 * n) + 1)

proof end;

theorem :: SERIES_2:28

for s being Real_Sequence st ( for n being Nat st n >= 1 holds
( s . n = 1 / ((((2 * n) - 1) * ((2 * n) + 1)) * ((2 * n) + 3)) & s . 0 = 0 ) ) holds
for n being Nat st n >= 1 holds
(Partial_Sums s) . n = (1 / 12) - (1 / ((4 * ((2 * n) + 1)) * ((2 * n) + 3)))

proof end;

theorem :: SERIES_2:29

for s being Real_Sequence st ( for n being Nat st n >= 1 holds
( s . n = 1 / ((((3 * n) - 2) * ((3 * n) + 1)) * ((3 * n) + 4)) & s . 0 = 0 ) ) holds
for n being Nat st n >= 1 holds
(Partial_Sums s) . n = (1 / 24) - (1 / ((6 * ((3 * n) + 1)) * ((3 * n) + 4)))

proof end;

theorem :: SERIES_2:30

for s being Real_Sequence st ( for n being Nat holds s . n = ((2 * n) - 1) / ((n * (n + 1)) * (n + 2)) ) holds
for n being Nat st n >= 1 holds
(Partial_Sums s) . n = ((3 / 4) - (2 / (n + 2))) + (1 / ((2 * (n + 1)) * (n + 2)))

proof end;

theorem :: SERIES_2:31

for s being Real_Sequence st ( for n being Nat holds s . n = (n + 2) / ((n * (n + 1)) * (n + 3)) ) holds
for n being Nat 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 end;

theorem :: SERIES_2:32

for s being Real_Sequence st ( for n being Nat holds s . n = ((n + 1) * (2 |^ n)) / ((n + 2) * (n + 3)) ) holds
for n being Nat holds (Partial_Sums s) . n = ((2 |^ (n + 1)) / (n + 3)) - (1 / 2)

proof end;

theorem :: SERIES_2:33

for s being Real_Sequence st ( for n being Nat holds s . n = ((n |^ 2) * (4 |^ n)) / ((n + 1) * (n + 2)) ) holds
for n being Nat st n >= 1 holds
(Partial_Sums s) . n = (2 / 3) + (((n - 1) * (4 |^ (n + 1))) / (3 * (n + 2)))

proof end;

theorem :: SERIES_2:34

for s being Real_Sequence st ( for n being Nat holds s . n = (n + 2) / ((n * (n + 1)) * (2 |^ n)) ) holds
for n being Nat st n >= 1 holds
(Partial_Sums s) . n = 1 - (1 / ((n + 1) * (2 |^ n)))

proof end;

theorem :: SERIES_2:35

for s being Real_Sequence st ( for n being Nat holds s . n = ((2 * n) + 3) / ((n * (n + 1)) * (3 |^ n)) ) holds
for n being Nat st n >= 1 holds
(Partial_Sums s) . n = 1 - (1 / ((n + 1) * (3 |^ n)))

proof end;

theorem :: SERIES_2:36

for s being Real_Sequence st ( for n being Nat holds s . n = (((- 1) |^ n) * (2 |^ (n + 1))) / (((2 |^ (n + 1)) + ((- 1) |^ (n + 1))) * ((2 |^ (n + 2)) + ((- 1) |^ (n + 2)))) ) holds
for n being Nat holds (Partial_Sums s) . n = (1 / 3) + (((- 1) |^ (n + 2)) / (3 * ((2 |^ (n + 2)) + ((- 1) |^ (n + 2)))))

proof end;

theorem :: SERIES_2:37

for s being Real_Sequence st ( for n being Nat holds s . n = (n !) * n ) holds
for n being Nat st n >= 1 holds
(Partial_Sums s) . n = ((n + 1) !) - 1

proof end;

theorem :: SERIES_2:38

for s being Real_Sequence st ( for n being Nat holds s . n = n / ((n + 1) !) ) holds
for n being Nat st n >= 1 holds
(Partial_Sums s) . n = 1 - (1 / ((n + 1) !))

proof end;

theorem :: SERIES_2:39

for s being Real_Sequence st ( for n being Nat st n >= 1 holds
( s . n = (((n |^ 2) + n) - 1) / ((n + 2) !) & s . 0 = 0 ) ) holds
for n being Nat st n >= 1 holds
(Partial_Sums s) . n = (1 / 2) - ((n + 1) / ((n + 2) !))

proof end;

theorem :: SERIES_2:40

for s being Real_Sequence st ( for n being Nat holds s . n = (n * (2 |^ n)) / ((n + 2) !) ) holds
for n being Nat st n >= 1 holds
(Partial_Sums s) . n = 1 - ((2 |^ (n + 1)) / ((n + 2) !))

proof end;

:: Added by AG, 5.09.2005

theorem :: SERIES_2:41

for a, b being Real
for s being Real_Sequence st ( for n being Nat holds s . n = (a * n) + b ) holds
for n being Nat holds (Partial_Sums s) . n = ((((a * (n + 1)) * n) / 2) + (n * b)) + b by Lm14;

:: Sum of an arithmetic series

theorem :: SERIES_2:42

for a, b being Real
for s being Real_Sequence st ( for n being Nat holds s . n = (a * n) + b ) holds
for n being Nat holds (Partial_Sums s) . n = ((n + 1) * ((s . 0) + (s . n))) / 2

proof end;