:: Partial Sum and Partial Product of Some Series
:: by Jianbing Cao , Fahui Zhai and Xiquan Liang
::
:: Received November 7, 2005
:: Copyright (c) 2005-2021 Association of Mizar Users

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

proof end;

Lm2: for n being Nat holds (((1 / 2) |^ (n + 1)) + (2 |^ (n + 1))) |^ 2 = (((1 / 4) |^ (n + 1)) + (4 |^ (n + 1))) + 2

proof end;

Lm3: for n being Nat holds (((1 / 3) |^ (n + 1)) + (3 |^ (n + 1))) |^ 2 = (((1 / 9) |^ (n + 1)) + (9 |^ (n + 1))) + 2

proof end;

Lm4: for a, b being Real holds (a - b) * (a + b) = (a |^ 2) - (b |^ 2)

proof end;

Lm5: for a, b being Real holds (a - b) |^ 2 = ((a |^ 2) - ((2 * a) * b)) + (b |^ 2)

proof end;

Lm6: for n being Nat
for a being Real st a <> 1 holds
((((a * (1 - (a |^ n))) / ((1 - a) |^ 2)) - ((n * (a |^ (n + 1))) / (1 - a))) + (n * (a |^ (n + 1)))) + (a |^ (n + 1)) = ((a * (1 - (a |^ (n + 1)))) / ((1 - a) |^ 2)) - (((n + 1) * (a |^ (n + 2))) / (1 - a))

proof end;

Lm7: for n being Nat holds 1 / ((2 -Root (n + 2)) + (2 -Root (n + 1))) = (2 -Root (n + 2)) - (2 -Root (n + 1))

proof end;

theorem Th1: :: SERIES_4:1

for a, b, c being Real holds ((a + b) + c) |^ 2 = (((((a |^ 2) + (b |^ 2)) + (c |^ 2)) + ((2 * a) * b)) + ((2 * a) * c)) + ((2 * b) * c)

proof end;

theorem Th2: :: SERIES_4:2

for a, b being Real holds (a + b) |^ 3 = (((a |^ 3) + ((3 * (a |^ 2)) * b)) + ((3 * (b |^ 2)) * a)) + (b |^ 3)

proof end;

theorem :: SERIES_4:3

for a, b, c being Real holds ((a - b) + c) |^ 2 = (((((a |^ 2) + (b |^ 2)) + (c |^ 2)) - ((2 * a) * b)) + ((2 * a) * c)) - ((2 * b) * c)

proof end;

theorem :: SERIES_4:4

for a, b, c being Real holds ((a - b) - c) |^ 2 = (((((a |^ 2) + (b |^ 2)) + (c |^ 2)) - ((2 * a) * b)) - ((2 * a) * c)) + ((2 * b) * c)

proof end;

theorem :: SERIES_4:5

for a, b being Real holds (a - b) |^ 3 = (((a |^ 3) - ((3 * (a |^ 2)) * b)) + ((3 * (b |^ 2)) * a)) - (b |^ 3)

proof end;

theorem :: SERIES_4:6

for a, b being Real holds (a + b) |^ 4 = ((((a |^ 4) + ((4 * (a |^ 3)) * b)) + ((6 * (a |^ 2)) * (b |^ 2))) + ((4 * (b |^ 3)) * a)) + (b |^ 4)

proof end;

theorem :: SERIES_4:7

for a, b, c, d being Real holds (((a + b) + c) + d) |^ 2 = ((((((a |^ 2) + (b |^ 2)) + (c |^ 2)) + (d |^ 2)) + ((((2 * a) * b) + ((2 * a) * c)) + ((2 * a) * d))) + (((2 * b) * c) + ((2 * b) * d))) + ((2 * c) * d)

proof end;

theorem :: SERIES_4:8

for a, b, c being Real holds ((a + b) + c) |^ 3 = ((((((a |^ 3) + (b |^ 3)) + (c |^ 3)) + (((3 * (a |^ 2)) * b) + ((3 * (a |^ 2)) * c))) + (((3 * (b |^ 2)) * a) + ((3 * (b |^ 2)) * c))) + (((3 * (c |^ 2)) * a) + ((3 * (c |^ 2)) * b))) + (((6 * a) * b) * c)

proof end;

theorem :: SERIES_4:9

for n being Nat
for a being Real st a <> 0 holds
(((1 / a) |^ (n + 1)) + (a |^ (n + 1))) |^ 2 = (((1 / a) |^ ((2 * n) + 2)) + (a |^ ((2 * n) + 2))) + 2

proof end;

:: Geometrical Series

theorem :: SERIES_4:10

for n being Nat
for a being Real
for s being Real_Sequence st a <> 1 & ( for n being Nat holds s . n = a |^ n ) holds
(Partial_Sums s) . n = (1 - (a |^ (n + 1))) / (1 - a)

proof end;

theorem :: SERIES_4:11

for a being Real
for s being Real_Sequence st a <> 1 & a <> 0 & ( for n being Nat holds s . n = (1 / a) |^ n ) holds
for n being Nat holds (Partial_Sums s) . n = (((1 / a) |^ n) - a) / (1 - a)

proof end;

:: Compositive Series

theorem :: SERIES_4:12

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

proof end;

theorem :: SERIES_4:13

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

proof end;

theorem :: SERIES_4:14

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

proof end;

theorem :: SERIES_4:15

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

proof end;

theorem :: SERIES_4:16

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

proof end;

theorem :: SERIES_4:17

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

proof end;

theorem :: SERIES_4:18

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

proof end;

theorem :: SERIES_4:19

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

proof end;

theorem :: SERIES_4:20

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

proof end;

theorem :: SERIES_4:21

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

proof end;

theorem :: SERIES_4:22

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

proof end;

theorem :: SERIES_4:23

for a being Real
for s being Real_Sequence st a <> 1 & ( for n being Nat st n >= 1 holds
( s . n = (a / (a - 1)) |^ n & s . 0 = 0 ) ) holds
for n being Nat st n >= 1 holds
(Partial_Sums s) . n = a * (((a / (a - 1)) |^ n) - 1)

proof end;

theorem :: SERIES_4:24

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

proof end;

:: Partial Product of Some Series

theorem :: SERIES_4:25

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

proof end;

theorem :: SERIES_4:26

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

proof end;

theorem :: SERIES_4:27

for s being Real_Sequence st ( for n being Nat st n >= 1 holds
( s . n = n & s . 0 = 1 ) ) holds
for n being Nat st n >= 1 holds
(Partial_Product s) . n = n !

proof end;

theorem :: SERIES_4:28

for a being Real
for s being Real_Sequence st ( for n being Nat st n >= 1 holds
( s . n = a / n & s . 0 = 1 ) ) holds
for n being Nat st n >= 1 holds
(Partial_Product s) . n = (a |^ n) / (n !)

proof end;

theorem :: SERIES_4:29

for a being Real
for s being Real_Sequence st ( for n being Nat st n >= 1 holds
( s . n = a & s . 0 = 1 ) ) holds
for n being Nat st n >= 1 holds
(Partial_Product s) . n = a |^ n

proof end;

theorem :: SERIES_4:30

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

proof end;