:: SERIES_2 semantic presentation

theorem Th1: :: SERIES_2:1

for b₁ being Nat holds abs ((- 1) |^ b₁) = 1

proof end;

Lemma2: for b₁ being real number holds b₁ |^ 3 = (b₁ * b₁) * b₁

proof end;

Lemma3: for b₁ being real number holds b₁ |^ 3 = (b₁ |^ 2) * b₁

proof end;

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

proof end;

Lemma5: for b₁ being real number holds (b₁ + 1) |^ 3 = (((b₁ |^ 3) + (3 * (b₁ |^ 2))) + (3 * b₁)) + 1

proof end;

Lemma6: for b₁ being Nat holds ((b₁ * ((2 * b₁) + 1)) * (((3 * (b₁ |^ 2)) + (3 * b₁)) - 1)) + (((b₁ + 1) |^ 3) * 30) = ((b₁ + 2) * ((2 * (b₁ + 1)) + 1)) * (((3 * ((b₁ + 1) |^ 2)) + (3 * (b₁ + 1))) - 1)

proof end;

Lemma7: for b₁ being real number holds
( (b₁ + 1) |^ 4 = ((((b₁ |^ 4) + (4 * (b₁ |^ 3))) + (6 * (b₁ |^ 2))) + (4 * b₁)) + 1 & (b₁ + 1) |^ 5 = (((((b₁ |^ 5) + (5 * (b₁ |^ 4))) + (10 * (b₁ |^ 3))) + (10 * (b₁ |^ 2))) + (5 * b₁)) + 1 )

proof end;

theorem Th2: :: SERIES_2:2

for b₁ being real number holds
( (b₁ + 1) |^ 3 = (((b₁ |^ 3) + (3 * (b₁ |^ 2))) + (3 * b₁)) + 1 & (b₁ + 1) |^ 4 = ((((b₁ |^ 4) + (4 * (b₁ |^ 3))) + (6 * (b₁ |^ 2))) + (4 * b₁)) + 1 & (b₁ + 1) |^ 5 = (((((b₁ |^ 5) + (5 * (b₁ |^ 4))) + (10 * (b₁ |^ 3))) + (10 * (b₁ |^ 2))) + (5 * b₁)) + 1 ) by Lemma5, Lemma7;

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

proof end;

Lemma9: for b₁ being Nat holds (1 / (b₁ + 1)) - (2 / ((b₁ + 1) * (b₁ + 3))) = 1 / (b₁ + 3)

proof end;

Lemma10: for b₁ being Nat holds (1 / (b₁ + 1)) - (3 / ((b₁ + 1) * (b₁ + 4))) = 1 / (b₁ + 4)

proof end;

Lemma11: for b₁ being Nat holds ((b₁ |^ 2) + (3 * b₁)) + 2 = (b₁ + 1) * (b₁ + 2)

proof end;

Lemma12: for b₁ being Nat holds (((b₁ * (4 * (b₁ |^ 2))) + (11 * b₁)) + (12 * (b₁ |^ 2))) + 3 = (b₁ + 1) * ((4 * ((b₁ + 1) |^ 2)) - 1)

proof end;

Lemma13: for b₁ being Nat holds ((b₁ + 1) |^ 2) * ((2 * ((b₁ + 1) |^ 2)) - 1) = ((((((b₁ |^ 2) * (b₁ |^ 2)) * 2) + ((12 - 1) * (b₁ |^ 2))) + (8 * (b₁ |^ 3))) + (6 * b₁)) + 1

proof end;

Lemma14: for b₁ being Nat holds (b₁ + 2) * ((((b₁ + 1) |^ 2) + (b₁ + 1)) - 1) = (((b₁ |^ 3) + (5 * (b₁ |^ 2))) + (7 * b₁)) + 2

proof end;

Lemma15: for b₁, b₂ being real number
for b₃ being Real_Sequence st ( for b₄ being Nat holds b₃ . b₄ = (b₁ * b₄) + b₂ ) holds
for b₄ being Nat holds (Partial_Sums b₃) . b₄ = ((((b₁ * (b₄ + 1)) * b₄) / 2) + (b₄ * b₂)) + b₂

proof end;

theorem Th3: :: SERIES_2:3

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

proof end;

theorem Th4: :: SERIES_2:4

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

proof end;

theorem Th5: :: SERIES_2:5

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

proof end;

theorem Th6: :: SERIES_2:6

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

proof end;

theorem Th7: :: SERIES_2:7

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

proof end;

theorem Th8: :: SERIES_2:8

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

proof end;

theorem Th9: :: SERIES_2:9

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

proof end;

theorem Th10: :: SERIES_2:10

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

proof end;

theorem Th11: :: SERIES_2:11

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

proof end;

theorem Th12: :: SERIES_2:12

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

proof end;

theorem Th13: :: SERIES_2:13

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

proof end;

theorem Th14: :: SERIES_2:14

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

proof end;

theorem Th15: :: SERIES_2:15

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

proof end;

theorem Th16: :: SERIES_2:16

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

proof end;

theorem Th17: :: SERIES_2:17

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

proof end;

theorem Th18: :: SERIES_2:18

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

proof end;

Lemma16: for b₁ being Nat holds ((b₁ |^ 2) * (((2 * (b₁ |^ 2)) + (2 * b₁)) - 1)) + (((b₁ + 1) |^ 3) * 12) = ((b₁ + 2) |^ 2) * (((2 * ((b₁ + 1) |^ 2)) + (2 * (b₁ + 1))) - 1)

proof end;

theorem Th19: :: SERIES_2:19

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

proof end;

Lemma17: for b₁ being Nat holds ((b₁ + 2) * ((2 * (b₁ + 1)) + 1)) * ((((3 * ((b₁ + 1) |^ 4)) + (6 * ((b₁ + 1) |^ 3))) - (3 * (b₁ + 1))) + 1) = ((((((6 * (b₁ |^ 6)) + (57 * (b₁ |^ 5))) + (216 * (b₁ |^ 4))) + (414 * (b₁ |^ 3))) + (419 * (b₁ |^ 2))) + (211 * b₁)) + 42

proof end;

theorem Th20: :: SERIES_2:20

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

proof end;

Lemma18: for b₁ being Nat holds ((b₁ + 2) |^ 2) * (((((3 * ((b₁ + 1) |^ 4)) + (6 * ((b₁ + 1) |^ 3))) - ((b₁ + 1) |^ 2)) - (4 * (b₁ + 1))) + 2) = ((b₁ |^ 2) * (((((3 * (b₁ |^ 4)) + (6 * (b₁ |^ 3))) - (b₁ |^ 2)) - (4 * b₁)) + 2)) + (((b₁ + 1) |^ 5) * 24)

proof end;

Lemma19: for b₁ being Nat holds (2 |^ (b₁ + 2)) + ((- 1) |^ (b₁ + 2)) > 0

proof end;

Lemma20: for b₁ being Nat holds (2 |^ (b₁ + 3)) + ((- 1) |^ (b₁ + 3)) > 0

proof end;

theorem Th21: :: SERIES_2:21

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

proof end;

theorem Th22: :: SERIES_2:22

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

proof end;

theorem Th23: :: SERIES_2:23

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

proof end;

theorem Th24: :: SERIES_2:24

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

proof end;

theorem Th25: :: SERIES_2:25

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

proof end;

theorem Th26: :: SERIES_2:26

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

proof end;

theorem Th27: :: SERIES_2:27

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

proof end;

theorem Th28: :: SERIES_2:28

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

proof end;

theorem Th29: :: SERIES_2:29

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

proof end;

theorem Th30: :: SERIES_2:30

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

proof end;

theorem Th31: :: SERIES_2:31

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

proof end;

theorem Th32: :: SERIES_2:32

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

proof end;

theorem Th33: :: SERIES_2:33

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

proof end;

theorem Th34: :: SERIES_2:34

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

proof end;

theorem Th35: :: SERIES_2:35

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

proof end;

theorem Th36: :: SERIES_2:36

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

proof end;

theorem Th37: :: SERIES_2:37

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

proof end;

theorem Th38: :: SERIES_2:38

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

proof end;

theorem Th39: :: SERIES_2:39

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

proof end;

theorem Th40: :: SERIES_2:40

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

proof end;

theorem Th41: :: SERIES_2:41

for b₁, b₂ being real number
for b₃ being Real_Sequence st ( for b₄ being Nat holds b₃ . b₄ = (b₁ * b₄) + b₂ ) holds
for b₄ being Nat holds (Partial_Sums b₃) . b₄ = ((((b₁ * (b₄ + 1)) * b₄) / 2) + (b₄ * b₂)) + b₂ by Lemma15;

theorem Th42: :: SERIES_2:42

for b₁, b₂ being real number
for b₃ being Real_Sequence st ( for b₄ being Nat holds b₃ . b₄ = (b₁ * b₄) + b₂ ) holds
for b₄ being Nat holds (Partial_Sums b₃) . b₄ = ((b₄ + 1) * ((b₃ . 0) + (b₃ . b₄))) / 2

proof end;