:: Partial Sum and Partial Product of Some Series
:: by Jianbing Cao , Fahui Zhai and Xiquan Liang
::
:: 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
() . 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 () . 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
() . 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
() . 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
() . 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 () . 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 () . 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 () . 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 () . 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 () . 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
() . 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 () . 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
() . 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
() . 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
() . 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
() . 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
() . 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
() . 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
() . 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
() . 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
() . n = (n + 1) / (2 * n)
proof end;