:: SERIES_4 semantic presentation

Lemma1: for b₁ being real number holds b₁ |^ 2 = b₁ * b₁
by WSIERP_1:2;

Lemma2: for b₁, b₂ being real number holds
( 4 = 2 |^ 2 & (b₁ + b₂) |^ 2 = ((b₁ |^ 2) + ((2 * b₁) * b₂)) + (b₂ |^ 2) )

proof end;

Lemma3: for b₁ being Nat holds (((1 / 2) |^ (b₁ + 1)) + (2 |^ (b₁ + 1))) |^ 2 = (((1 / 4) |^ (b₁ + 1)) + (4 |^ (b₁ + 1))) + 2

proof end;

Lemma4: for b₁ being Nat holds (((1 / 3) |^ (b₁ + 1)) + (3 |^ (b₁ + 1))) |^ 2 = (((1 / 9) |^ (b₁ + 1)) + (9 |^ (b₁ + 1))) + 2

proof end;

Lemma5: for b₁, b₂ being real number holds (b₁ - b₂) * (b₁ + b₂) = (b₁ |^ 2) - (b₂ |^ 2)

proof end;

Lemma6: for b₁, b₂ being real number holds (b₁ - b₂) |^ 2 = ((b₁ |^ 2) - ((2 * b₁) * b₂)) + (b₂ |^ 2)

proof end;

Lemma7: for b₁ being Nat
for b₂ being real number st b₂ <> 1 holds
((((b₂ * (1 - (b₂ |^ b₁))) / ((1 - b₂) |^ 2)) - ((b₁ * (b₂ |^ (b₁ + 1))) / (1 - b₂))) + (b₁ * (b₂ |^ (b₁ + 1)))) + (b₂ |^ (b₁ + 1)) = ((b₂ * (1 - (b₂ |^ (b₁ + 1)))) / ((1 - b₂) |^ 2)) - (((b₁ + 1) * (b₂ |^ (b₁ + 2))) / (1 - b₂))

proof end;

Lemma8: for b₁ being Nat holds 1 / ((2 -Root (b₁ + 2)) + (2 -Root (b₁ + 1))) = (2 -Root (b₁ + 2)) - (2 -Root (b₁ + 1))

proof end;

theorem Th1: :: SERIES_4:1

for b₁, b₂, b₃ being real number holds ((b₁ + b₂) + b₃) |^ 2 = (((((b₁ |^ 2) + (b₂ |^ 2)) + (b₃ |^ 2)) + ((2 * b₁) * b₂)) + ((2 * b₁) * b₃)) + ((2 * b₂) * b₃)

proof end;

theorem Th2: :: SERIES_4:2

for b₁, b₂ being real number holds (b₁ + b₂) |^ 3 = (((b₁ |^ 3) + ((3 * (b₁ |^ 2)) * b₂)) + ((3 * (b₂ |^ 2)) * b₁)) + (b₂ |^ 3)

proof end;

theorem Th3: :: SERIES_4:3

for b₁, b₂, b₃ being real number holds ((b₁ - b₂) + b₃) |^ 2 = (((((b₁ |^ 2) + (b₂ |^ 2)) + (b₃ |^ 2)) - ((2 * b₁) * b₂)) + ((2 * b₁) * b₃)) - ((2 * b₂) * b₃)

proof end;

theorem Th4: :: SERIES_4:4

for b₁, b₂, b₃ being real number holds ((b₁ - b₂) - b₃) |^ 2 = (((((b₁ |^ 2) + (b₂ |^ 2)) + (b₃ |^ 2)) - ((2 * b₁) * b₂)) - ((2 * b₁) * b₃)) + ((2 * b₂) * b₃)

proof end;

theorem Th5: :: SERIES_4:5

for b₁, b₂ being real number holds (b₁ - b₂) |^ 3 = (((b₁ |^ 3) - ((3 * (b₁ |^ 2)) * b₂)) + ((3 * (b₂ |^ 2)) * b₁)) - (b₂ |^ 3)

proof end;

theorem Th6: :: SERIES_4:6

for b₁, b₂ being real number holds (b₁ + b₂) |^ 4 = ((((b₁ |^ 4) + ((4 * (b₁ |^ 3)) * b₂)) + ((6 * (b₁ |^ 2)) * (b₂ |^ 2))) + ((4 * (b₂ |^ 3)) * b₁)) + (b₂ |^ 4)

proof end;

theorem Th7: :: SERIES_4:7

for b₁, b₂, b₃, b₄ being real number holds (((b₁ + b₂) + b₃) + b₄) |^ 2 = ((((((b₁ |^ 2) + (b₂ |^ 2)) + (b₃ |^ 2)) + (b₄ |^ 2)) + ((((2 * b₁) * b₂) + ((2 * b₁) * b₃)) + ((2 * b₁) * b₄))) + (((2 * b₂) * b₃) + ((2 * b₂) * b₄))) + ((2 * b₃) * b₄)

proof end;

theorem Th8: :: SERIES_4:8

for b₁, b₂, b₃ being real number holds ((b₁ + b₂) + b₃) |^ 3 = ((((((b₁ |^ 3) + (b₂ |^ 3)) + (b₃ |^ 3)) + (((3 * (b₁ |^ 2)) * b₂) + ((3 * (b₁ |^ 2)) * b₃))) + (((3 * (b₂ |^ 2)) * b₁) + ((3 * (b₂ |^ 2)) * b₃))) + (((3 * (b₃ |^ 2)) * b₁) + ((3 * (b₃ |^ 2)) * b₂))) + (((6 * b₁) * b₂) * b₃)

proof end;

theorem Th9: :: SERIES_4:9

for b₁ being Nat
for b₂ being real number st b₂ <> 0 holds
(((1 / b₂) |^ (b₁ + 1)) + (b₂ |^ (b₁ + 1))) |^ 2 = (((1 / b₂) |^ ((2 * b₁) + 2)) + (b₂ |^ ((2 * b₁) + 2))) + 2

proof end;

theorem Th10: :: SERIES_4:10

for b₁ being Nat
for b₂ being real number
for b₃ being Real_Sequence st b₂ <> 1 & ( for b₄ being Nat holds b₃ . b₄ = b₂ |^ b₄ ) holds
(Partial_Sums b₃) . b₁ = (1 - (b₂ |^ (b₁ + 1))) / (1 - b₂)

proof end;

theorem Th11: :: SERIES_4:11

for b₁ being real number
for b₂ being Real_Sequence st b₁ <> 1 & b₁ <> 0 & ( for b₃ being Nat holds b₂ . b₃ = (1 / b₁) |^ b₃ ) holds
for b₃ being Nat holds (Partial_Sums b₂) . b₃ = (((1 / b₁) |^ b₃) - b₁) / (1 - b₁)

proof end;

theorem Th12: :: SERIES_4:12

for b₁ being Nat
for b₂ being Real_Sequence st ( for b₃ being Nat holds b₂ . b₃ = ((10 |^ b₃) + (2 * b₃)) + 1 ) holds
(Partial_Sums b₂) . b₁ = (((10 |^ (b₁ + 1)) / 9) - (1 / 9)) + ((b₁ + 1) |^ 2)

proof end;

theorem Th13: :: SERIES_4:13

for b₁ being Nat
for b₂ being Real_Sequence st ( for b₃ being Nat holds b₂ . b₃ = ((2 * b₃) - 1) + ((1 / 2) |^ b₃) ) holds
(Partial_Sums b₂) . b₁ = ((b₁ |^ 2) + 1) - ((1 / 2) |^ b₁)

proof end;

theorem Th14: :: SERIES_4:14

for b₁ being Nat
for b₂ being Real_Sequence st ( for b₃ being Nat holds b₂ . b₃ = b₃ * ((1 / 2) |^ b₃) ) holds
(Partial_Sums b₂) . b₁ = 2 - ((2 + b₁) * ((1 / 2) |^ b₁))

proof end;

theorem Th15: :: SERIES_4:15

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

proof end;

theorem Th16: :: SERIES_4:16

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

proof end;

theorem Th17: :: SERIES_4:17

for b₁ being Real_Sequence st ( for b₂ being Nat holds b₁ . b₂ = b₂ * (2 |^ b₂) ) holds
for b₂ being Nat holds (Partial_Sums b₁) . b₂ = ((b₂ * (2 |^ (b₂ + 1))) - (2 |^ (b₂ + 1))) + 2

proof end;

theorem Th18: :: SERIES_4:18

for b₁ being Real_Sequence st ( for b₂ being Nat holds b₁ . b₂ = ((2 * b₂) + 1) * (3 |^ b₂) ) holds
for b₂ being Nat holds (Partial_Sums b₁) . b₂ = (b₂ * (3 |^ (b₂ + 1))) + 1

proof end;

theorem Th19: :: SERIES_4:19

for b₁ being real number
for b₂ being Real_Sequence st b₁ <> 1 & ( for b₃ being Nat holds b₂ . b₃ = b₃ * (b₁ |^ b₃) ) holds
for b₃ being Nat holds (Partial_Sums b₂) . b₃ = ((b₁ * (1 - (b₁ |^ b₃))) / ((1 - b₁) |^ 2)) - ((b₃ * (b₁ |^ (b₃ + 1))) / (1 - b₁))

proof end;

theorem Th20: :: SERIES_4:20

for b₁ being Nat
for b₂ being Real_Sequence st ( for b₃ being Nat holds b₂ . b₃ = 1 / ((2 -Root (b₃ + 1)) + (2 -Root b₃)) ) holds
(Partial_Sums b₂) . b₁ = 2 -Root (b₁ + 1)

proof end;

theorem Th21: :: SERIES_4:21

for b₁ being Real_Sequence st ( for b₂ being Nat holds b₁ . b₂ = (2 |^ b₂) + ((1 / 2) |^ b₂) ) holds
for b₂ being Nat holds (Partial_Sums b₁) . b₂ = ((2 |^ (b₂ + 1)) - ((1 / 2) |^ b₂)) + 1

proof end;

theorem Th22: :: SERIES_4:22

for b₁ being Real_Sequence st ( for b₂ being Nat holds b₁ . b₂ = ((b₂ ! ) * b₂) + (b₂ / ((b₂ + 1) ! )) ) holds
for b₂ being Nat st b₂ >= 1 holds
(Partial_Sums b₁) . b₂ = ((b₂ + 1) ! ) - (1 / ((b₂ + 1) ! ))

proof end;

theorem Th23: :: SERIES_4:23

for b₁ being real number
for b₂ being Real_Sequence st b₁ <> 1 & ( for b₃ being Nat st b₃ >= 1 holds
( b₂ . b₃ = (b₁ / (b₁ - 1)) |^ b₃ & b₂ . 0 = 0 ) ) holds
for b₃ being Nat st b₃ >= 1 holds
(Partial_Sums b₂) . b₃ = b₁ * (((b₁ / (b₁ - 1)) |^ b₃) - 1)

proof end;

theorem Th24: :: SERIES_4:24

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

proof end;

theorem Th25: :: SERIES_4:25

for b₁ being Nat
for b₂ being Real_Sequence st ( for b₃ being Nat holds b₂ . b₃ = (b₃ + 1) / (b₃ + 2) ) holds
(Partial_Product b₂) . b₁ = 1 / (b₁ + 2)

proof end;

theorem Th26: :: SERIES_4:26

for b₁ being Nat
for b₂ being Real_Sequence st ( for b₃ being Nat holds b₂ . b₃ = 1 / (b₃ + 1) ) holds
(Partial_Product b₂) . b₁ = 1 / ((b₁ + 1) ! )

proof end;

theorem Th27: :: SERIES_4:27

for b₁ being Real_Sequence st ( for b₂ being Nat st b₂ >= 1 holds
( b₁ . b₂ = b₂ & b₁ . 0 = 1 ) ) holds
for b₂ being Nat st b₂ >= 1 holds
(Partial_Product b₁) . b₂ = b₂ !

proof end;

theorem Th28: :: SERIES_4:28

for b₁ being real number
for b₂ being Real_Sequence st ( for b₃ being Nat st b₃ >= 1 holds
( b₂ . b₃ = b₁ / b₃ & b₂ . 0 = 1 ) ) holds
for b₃ being Nat st b₃ >= 1 holds
(Partial_Product b₂) . b₃ = (b₁ |^ b₃) / (b₃ ! )

proof end;

theorem Th29: :: SERIES_4:29

for b₁ being real number
for b₂ being Real_Sequence st ( for b₃ being Nat st b₃ >= 1 holds
( b₂ . b₃ = b₁ & b₂ . 0 = 1 ) ) holds
for b₃ being Nat st b₃ >= 1 holds
(Partial_Product b₂) . b₃ = b₁ |^ b₃

proof end;

theorem Th30: :: SERIES_4:30

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

proof end;