:: Partial Sum of Some Series
:: by Ming Liang and Yuzhong Ding
::
:: Copyright (c) 2004-2018 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 ;

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 () . 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 () . 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 () . 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 () . 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 () . 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 () . 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 () . 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 () . 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 () . 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 () . 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 () . 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 () . 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
() . 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 () . 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
() . 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 () . 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 () . 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 () . 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 () . 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 () . 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 () . 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 () . 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 () . 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
() . 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
() . 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
() . 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
() . 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
() . 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
() . 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
() . 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 () . 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
() . 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
() . 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
() . 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 () . 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
() . 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
() . 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
() . 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
() . n = 1 - ((2 |^ (n + 1)) / ((n + 2) !))
proof end;