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


begin

theorem Th1: :: SERIES_2:1
for n being Element of NAT holds abs ((- 1) |^ n) = 1
proofend;

Lm1:  for a being real number holds a |^ 3 = (a * a) * a
proofend;

Lm2:  for a being real number holds a |^ 3 = (a |^ 2) * a
proofend;

Lm3:  for a, b being real number holds
( 4 = 2 |^ 2 & (a + b) |^ 2 = ((a |^ 2) + ((2 * a) * b)) + (b |^ 2) )
proofend;

Lm4:  for a being real number holds (a + 1) |^ 3 = (((a |^ 3) + (3 * (a |^ 2))) + (3 * a)) + 1
proofend;

Lm5:  for n being Element of 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)
proofend;

Lm6:  for n being real number 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 )
proofend;

theorem :: SERIES_2:2
for n being real number 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 Element of NAT holds
( 1 - (1 / (n + 2)) = (n + 1) / (n + 2) & 1 / ((n + 1) !) = (n + 2) / (((n + 1) !) * (n + 2)) )
proofend;

Lm8:  for n being Element of NAT holds (1 / (n + 1)) - (2 / ((n + 1) * (n + 3))) = 1 / (n + 3)
proofend;

Lm9:  for n being Element of NAT holds (1 / (n + 1)) - (3 / ((n + 1) * (n + 4))) = 1 / (n + 4)
proofend;

Lm10:  for n being Element of NAT holds ((n |^ 2) + (3 * n)) + 2 = (n + 1) * (n + 2)
proofend;

Lm11:  for n being Element of NAT holds (((n * (4 * (n |^ 2))) + (11 * n)) + (12 * (n |^ 2))) + 3 = (n + 1) * ((4 * ((n + 1) |^ 2)) - 1)
proofend;

Lm12:  for n being Element of 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
proofend;

Lm13:  for n being Element of NAT holds (n + 2) * ((((n + 1) |^ 2) + (n + 1)) - 1) = (((n |^ 3) + (5 * (n |^ 2))) + (7 * n)) + 2
proofend;

Lm14:  for a, b being real number
for s being Real_Sequence st ( for n being Element of NAT holds s . n = (a * n) + b ) holds
for n being Element of NAT holds (Partial_Sums s) . n = ((((a * (n + 1)) * n) / 2) + (n * b)) + b
proofend;

theorem :: SERIES_2:3
for s being Real_Sequence st ( for n being Element of NAT holds s . n = n ) holds
for n being Element of NAT holds (Partial_Sums s) . n = (n * (n + 1)) / 2
proofend;

theorem :: SERIES_2:4
for s being Real_Sequence st ( for n being Element of NAT holds s . n = 2 * n ) holds
for n being Element of NAT holds (Partial_Sums s) . n = n * (n + 1)
proofend;

theorem :: SERIES_2:5
for s being Real_Sequence st ( for n being Element of NAT holds s . n = (2 * n) + 1 ) holds
for n being Element of NAT holds (Partial_Sums s) . n = (n + 1) |^ 2
proofend;

theorem :: SERIES_2:6
for s being Real_Sequence st ( for n being Element of NAT holds s . n = n * (n + 1) ) holds
for n being Element of NAT holds (Partial_Sums s) . n = ((n * (n + 1)) * (n + 2)) / 3
proofend;

theorem :: SERIES_2:7
for s being Real_Sequence st ( for n being Element of NAT holds s . n = (n * (n + 1)) * (n + 2) ) holds
for n being Element of NAT holds (Partial_Sums s) . n = (((n * (n + 1)) * (n + 2)) * (n + 3)) / 4
proofend;

theorem :: SERIES_2:8
for s being Real_Sequence st ( for n being Element of NAT holds s . n = ((n * (n + 1)) * (n + 2)) * (n + 3) ) holds
for n being Element of NAT holds (Partial_Sums s) . n = ((((n * (n + 1)) * (n + 2)) * (n + 3)) * (n + 4)) / 5
proofend;

theorem :: SERIES_2:9
for s being Real_Sequence st ( for n being Element of NAT holds s . n = 1 / (n * (n + 1)) ) holds
for n being Element of NAT holds (Partial_Sums s) . n = 1 - (1 / (n + 1))
proofend;

theorem :: SERIES_2:10
for s being Real_Sequence st ( for n being Element of NAT holds s . n = 1 / ((n * (n + 1)) * (n + 2)) ) holds
for n being Element of NAT holds (Partial_Sums s) . n = (1 / 4) - (1 / ((2 * (n + 1)) * (n + 2)))
proofend;

theorem :: SERIES_2:11
for s being Real_Sequence st ( for n being Element of NAT holds s . n = 1 / (((n * (n + 1)) * (n + 2)) * (n + 3)) ) holds
for n being Element of NAT holds (Partial_Sums s) . n = (1 / 18) - (1 / (((3 * (n + 1)) * (n + 2)) * (n + 3)))
proofend;

theorem :: SERIES_2:12
for s being Real_Sequence st ( for n being Element of NAT holds s . n = n |^ 2 ) holds
for n being Element of NAT holds (Partial_Sums s) . n = ((n * (n + 1)) * ((2 * n) + 1)) / 6
proofend;

theorem :: SERIES_2:13
for s being Real_Sequence st ( for n being Element of NAT holds s . n = ((- 1) |^ (n + 1)) * (n |^ 2) ) holds
for n being Element of NAT holds (Partial_Sums s) . n = ((((- 1) |^ (n + 1)) * n) * (n + 1)) / 2
proofend;

theorem :: SERIES_2:14
for s being Real_Sequence st ( for n being Element of NAT st n >= 1 holds
( s . n = ((2 * n) - 1) |^ 2 & s . 0 = 0 ) ) holds
for n being Element of NAT st n >= 1 holds
(Partial_Sums s) . n = (n * ((4 * (n |^ 2)) - 1)) / 3
proofend;

theorem :: SERIES_2:15
for s being Real_Sequence st ( for n being Element of NAT holds s . n = n |^ 3 ) holds
for n being Element of NAT holds (Partial_Sums s) . n = ((n |^ 2) * ((n + 1) |^ 2)) / 4
proofend;

theorem :: SERIES_2:16
for s being Real_Sequence st ( for n being Element of NAT st n >= 1 holds
( s . n = ((2 * n) - 1) |^ 3 & s . 0 = 0 ) ) holds
for n being Element of NAT st n >= 1 holds
(Partial_Sums s) . n = (n |^ 2) * ((2 * (n |^ 2)) - 1)
proofend;

theorem :: SERIES_2:17
for s being Real_Sequence st ( for n being Element of NAT holds s . n = n |^ 4 ) holds
for n being Element of NAT holds (Partial_Sums s) . n = (((n * (n + 1)) * ((2 * n) + 1)) * (((3 * (n |^ 2)) + (3 * n)) - 1)) / 30
proofend;

theorem :: SERIES_2:18
for s being Real_Sequence st ( for n being Element of NAT holds s . n = ((- 1) |^ (n + 1)) * (n |^ 4) ) holds
for n being Element of NAT holds (Partial_Sums s) . n = (((((- 1) |^ (n + 1)) * n) * (n + 1)) * (((n |^ 2) + n) - 1)) / 2
proofend;

Lm15:  for n being Element of 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)
proofend;

theorem :: SERIES_2:19
for s being Real_Sequence st ( for n being Element of NAT holds s . n = n |^ 5 ) holds
for n being Element of NAT holds (Partial_Sums s) . n = (((n |^ 2) * ((n + 1) |^ 2)) * (((2 * (n |^ 2)) + (2 * n)) - 1)) / 12
proofend;

Lm16:  for n being Element of 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
proofend;

theorem :: SERIES_2:20
for s being Real_Sequence st ( for n being Element of NAT holds s . n = n |^ 6 ) holds
for n being Element of NAT holds (Partial_Sums s) . n = (((n * (n + 1)) * ((2 * n) + 1)) * ((((3 * (n |^ 4)) + (6 * (n |^ 3))) - (3 * n)) + 1)) / 42
proofend;

Lm17:  for n being Element of 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)
proofend;

Lm18:  for n being Element of NAT holds (2 |^ (n + 2)) + ((- 1) |^ (n + 2)) > 0
proofend;

Lm19:  for n being Element of NAT holds (2 |^ (n + 3)) + ((- 1) |^ (n + 3)) > 0
proofend;

theorem :: SERIES_2:21
for s being Real_Sequence st ( for n being Element of NAT holds s . n = n |^ 7 ) holds
for n being Element of NAT holds (Partial_Sums s) . n = (((n |^ 2) * ((n + 1) |^ 2)) * (((((3 * (n |^ 4)) + (6 * (n |^ 3))) - (n |^ 2)) - (4 * n)) + 2)) / 24
proofend;

theorem :: SERIES_2:22
for s being Real_Sequence st ( for n being Element of NAT holds s . n = n * ((n + 1) |^ 2) ) holds
for n being Element of NAT holds (Partial_Sums s) . n = (((n * (n + 1)) * (n + 2)) * ((3 * n) + 5)) / 12
proofend;

theorem :: SERIES_2:23
for s being Real_Sequence st ( for n being Element of NAT holds s . n = (n * ((n + 1) |^ 2)) * (n + 2) ) holds
for n being Element of NAT holds (Partial_Sums s) . n = ((((n * (n + 1)) * (n + 2)) * (n + 3)) * ((2 * n) + 3)) / 10
proofend;

theorem :: SERIES_2:24
for s being Real_Sequence st ( for n being Element of NAT holds s . n = (n * (n + 1)) * (2 |^ n) ) holds
for n being Element of NAT holds (Partial_Sums s) . n = ((2 |^ (n + 1)) * (((n |^ 2) - n) + 2)) - 4
proofend;

theorem :: SERIES_2:25
for s being Real_Sequence st ( for n being Element of NAT st n >= 1 holds
( s . n = 1 / ((n - 1) * (n + 1)) & s . 0 = 0 ) ) holds
for n being Element of NAT st n >= 2 holds
(Partial_Sums s) . n = ((3 / 4) - (1 / (2 * n))) - (1 / (2 * (n + 1)))
proofend;

theorem :: SERIES_2:26
for s being Real_Sequence st ( for n being Element of NAT st n >= 1 holds
( s . n = 1 / (((2 * n) - 1) * ((2 * n) + 1)) & s . 0 = 0 ) ) holds
for n being Element of NAT st n >= 1 holds
(Partial_Sums s) . n = n / ((2 * n) + 1)
proofend;

theorem :: SERIES_2:27
for s being Real_Sequence st ( for n being Element of NAT st n >= 1 holds
( s . n = 1 / (((3 * n) - 2) * ((3 * n) + 1)) & s . 0 = 0 ) ) holds
for n being Element of NAT st n >= 1 holds
(Partial_Sums s) . n = n / ((3 * n) + 1)
proofend;

theorem :: SERIES_2:28
for s being Real_Sequence st ( for n being Element of NAT st n >= 1 holds
( s . n = 1 / ((((2 * n) - 1) * ((2 * n) + 1)) * ((2 * n) + 3)) & s . 0 = 0 ) ) holds
for n being Element of NAT st n >= 1 holds
(Partial_Sums s) . n = (1 / 12) - (1 / ((4 * ((2 * n) + 1)) * ((2 * n) + 3)))
proofend;

theorem :: SERIES_2:29
for s being Real_Sequence st ( for n being Element of NAT st n >= 1 holds
( s . n = 1 / ((((3 * n) - 2) * ((3 * n) + 1)) * ((3 * n) + 4)) & s . 0 = 0 ) ) holds
for n being Element of NAT st n >= 1 holds
(Partial_Sums s) . n = (1 / 24) - (1 / ((6 * ((3 * n) + 1)) * ((3 * n) + 4)))
proofend;

theorem :: SERIES_2:30
for s being Real_Sequence st ( for n being Element of NAT holds s . n = ((2 * n) - 1) / ((n * (n + 1)) * (n + 2)) ) holds
for n being Element of NAT st n >= 1 holds
(Partial_Sums s) . n = ((3 / 4) - (2 / (n + 2))) + (1 / ((2 * (n + 1)) * (n + 2)))
proofend;

theorem :: SERIES_2:31
for s being Real_Sequence st ( for n being Element of NAT holds s . n = (n + 2) / ((n * (n + 1)) * (n + 3)) ) holds
for n being Element of 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)))
proofend;

theorem :: SERIES_2:32
for s being Real_Sequence st ( for n being Element of NAT holds s . n = ((n + 1) * (2 |^ n)) / ((n + 2) * (n + 3)) ) holds
for n being Element of NAT holds (Partial_Sums s) . n = ((2 |^ (n + 1)) / (n + 3)) - (1 / 2)
proofend;

theorem :: SERIES_2:33
for s being Real_Sequence st ( for n being Element of NAT holds s . n = ((n |^ 2) * (4 |^ n)) / ((n + 1) * (n + 2)) ) holds
for n being Element of NAT st n >= 1 holds
(Partial_Sums s) . n = (2 / 3) + (((n - 1) * (4 |^ (n + 1))) / (3 * (n + 2)))
proofend;

theorem :: SERIES_2:34
for s being Real_Sequence st ( for n being Element of NAT holds s . n = (n + 2) / ((n * (n + 1)) * (2 |^ n)) ) holds
for n being Element of NAT st n >= 1 holds
(Partial_Sums s) . n = 1 - (1 / ((n + 1) * (2 |^ n)))
proofend;

theorem :: SERIES_2:35
for s being Real_Sequence st ( for n being Element of NAT holds s . n = ((2 * n) + 3) / ((n * (n + 1)) * (3 |^ n)) ) holds
for n being Element of NAT st n >= 1 holds
(Partial_Sums s) . n = 1 - (1 / ((n + 1) * (3 |^ n)))
proofend;

theorem :: SERIES_2:36
for s being Real_Sequence st ( for n being Element of 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 Element of NAT holds (Partial_Sums s) . n = (1 / 3) + (((- 1) |^ (n + 2)) / (3 * ((2 |^ (n + 2)) + ((- 1) |^ (n + 2)))))
proofend;

theorem :: SERIES_2:37
for s being Real_Sequence st ( for n being Element of NAT holds s . n = (n !) * n ) holds
for n being Element of NAT st n >= 1 holds
(Partial_Sums s) . n = ((n + 1) !) - 1
proofend;

theorem :: SERIES_2:38
for s being Real_Sequence st ( for n being Element of NAT holds s . n = n / ((n + 1) !) ) holds
for n being Element of NAT st n >= 1 holds
(Partial_Sums s) . n = 1 - (1 / ((n + 1) !))
proofend;

theorem :: SERIES_2:39
for s being Real_Sequence st ( for n being Element of NAT st n >= 1 holds
( s . n = (((n |^ 2) + n) - 1) / ((n + 2) !) & s . 0 = 0 ) ) holds
for n being Element of NAT st n >= 1 holds
(Partial_Sums s) . n = (1 / 2) - ((n + 1) / ((n + 2) !))
proofend;

theorem :: SERIES_2:40
for s being Real_Sequence st ( for n being Element of NAT holds s . n = (n * (2 |^ n)) / ((n + 2) !) ) holds
for n being Element of NAT st n >= 1 holds
(Partial_Sums s) . n = 1 - ((2 |^ (n + 1)) / ((n + 2) !))
proofend;

:: Added by AG, 5.09.2005
theorem :: SERIES_2:41
for a, b being real number
for s being Real_Sequence st ( for n being Element of NAT holds s . n = (a * n) + b ) holds
for n being Element of NAT holds (Partial_Sums s) . n = ((((a * (n + 1)) * n) / 2) + (n * b)) + b by Lm14;

:: [WP: ] Sum_of_an_arithmetic_series
theorem :: SERIES_2:42
for a, b being real number
for s being Real_Sequence st ( for n being Element of NAT holds s . n = (a * n) + b ) holds
for n being Element of NAT holds (Partial_Sums s) . n = ((n + 1) * ((s . 0) + (s . n))) / 2
proofend;