:: SERIES_1 semantic presentation

Lemma1: ( 1 / 1 = 1 & 1 / (- 1) = - 1 )
;

theorem Th1: :: SERIES_1:1

for b₁ being real number
for b₂ being Real_Sequence st 0 < b₁ & b₁ < 1 & ( for b₃ being Nat holds b₂ . b₃ = b₁ to_power (b₃ + 1) ) holds
( b₂ is convergent & lim b₂ = 0 )

proof end;

theorem Th2: :: SERIES_1:2

for b₁ being Nat
for b₂ being real number st b₂ <> 0 holds
(abs b₂) to_power b₁ = abs (b₂ to_power b₁)

proof end;

theorem Th3: :: SERIES_1:3

for b₁ being real number
for b₂ being Real_Sequence st abs b₁ < 1 & ( for b₃ being Nat holds b₂ . b₃ = b₁ to_power (b₃ + 1) ) holds
( b₂ is convergent & lim b₂ = 0 )

proof end;

definition

let c₁ be Real_Sequence;
func Partial_Sums c₁ -> Real_Sequence means :Def1: :: SERIES_1:def 1
( a₂ . 0 = a₁ . 0 & ( for b₁ being Nat holds a₂ . (b₁ + 1) = (a₂ . b₁) + (a₁ . (b₁ + 1)) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines Partial_Sums SERIES_1:def 1 :

definition

let c₁ be Real_Sequence;
attr a₁ is summable means :Def2: :: SERIES_1:def 2
Partial_Sums a₁ is convergent;
func Sum c₁ -> Real equals :: SERIES_1:def 3
lim (Partial_Sums a₁);
correctness ;

end;

:: deftheorem Def2 defines summable SERIES_1:def 2 :

:: deftheorem Def3 defines Sum SERIES_1:def 3 :

theorem Th4: :: SERIES_1:4

canceled;

theorem Th5: :: SERIES_1:5

canceled;

theorem Th6: :: SERIES_1:6

canceled;

theorem Th7: :: SERIES_1:7

for b₁ being Real_Sequence st b₁ is summable holds
( b₁ is convergent & lim b₁ = 0 )

proof end;

theorem Th8: :: SERIES_1:8

for b₁, b₂ being Real_Sequence holds (Partial_Sums b₁) + (Partial_Sums b₂) = Partial_Sums (b₁ + b₂)

proof end;

theorem Th9: :: SERIES_1:9

for b₁, b₂ being Real_Sequence holds (Partial_Sums b₁) - (Partial_Sums b₂) = Partial_Sums (b₁ - b₂)

proof end;

theorem Th10: :: SERIES_1:10

for b₁, b₂ being Real_Sequence st b₁ is summable & b₂ is summable holds
( b₁ + b₂ is summable & Sum (b₁ + b₂) = (Sum b₁) + (Sum b₂) )

proof end;

theorem Th11: :: SERIES_1:11

for b₁, b₂ being Real_Sequence st b₁ is summable & b₂ is summable holds
( b₁ - b₂ is summable & Sum (b₁ - b₂) = (Sum b₁) - (Sum b₂) )

proof end;

theorem Th12: :: SERIES_1:12

for b₁ being real number
for b₂ being Real_Sequence holds Partial_Sums (b₁ (#) b₂) = b₁ (#) (Partial_Sums b₂)

proof end;

theorem Th13: :: SERIES_1:13

for b₁ being real number
for b₂ being Real_Sequence st b₂ is summable holds
( b₁ (#) b₂ is summable & Sum (b₁ (#) b₂) = b₁ * (Sum b₂) )

proof end;

theorem Th14: :: SERIES_1:14

for b₁, b₂ being Real_Sequence st ( for b₃ being Nat holds b₂ . b₃ = b₁ . 0 ) holds
Partial_Sums (b₁ ^\ 1) = ((Partial_Sums b₁) ^\ 1) - b₂

proof end;

theorem Th15: :: SERIES_1:15

for b₁ being Real_Sequence st b₁ is summable holds
for b₂ being Nat holds b₁ ^\ b₂ is summable

proof end;

theorem Th16: :: SERIES_1:16

for b₁ being Real_Sequence st ex b₂ being Nat st b₁ ^\ b₂ is summable holds
b₁ is summable

proof end;

theorem Th17: :: SERIES_1:17

for b₁, b₂ being Real_Sequence st ( for b₃ being Nat holds b₁ . b₃ <= b₂ . b₃ ) holds
for b₃ being Nat holds (Partial_Sums b₁) . b₃ <= (Partial_Sums b₂) . b₃

proof end;

theorem Th18: :: SERIES_1:18

for b₁ being Real_Sequence st b₁ is summable holds
for b₂ being Nat holds Sum b₁ = ((Partial_Sums b₁) . b₂) + (Sum (b₁ ^\ (b₂ + 1)))

proof end;

theorem Th19: :: SERIES_1:19

for b₁ being Real_Sequence st ( for b₂ being Nat holds 0 <= b₁ . b₂ ) holds
Partial_Sums b₁ is non-decreasing

proof end;

theorem Th20: :: SERIES_1:20

for b₁ being Real_Sequence st ( for b₂ being Nat holds 0 <= b₁ . b₂ ) holds
( Partial_Sums b₁ is bounded_above iff b₁ is summable )

proof end;

theorem Th21: :: SERIES_1:21

for b₁ being Real_Sequence st b₁ is summable & ( for b₂ being Nat holds 0 <= b₁ . b₂ ) holds
0 <= Sum b₁

proof end;

theorem Th22: :: SERIES_1:22

for b₁, b₂ being Real_Sequence st ( for b₃ being Nat holds 0 <= b₁ . b₃ ) & b₂ is summable & ex b₃ being Nat st
for b₄ being Nat st b₃ <= b₄ holds
b₁ . b₄ <= b₂ . b₄ holds
b₁ is summable

proof end;

theorem Th23: :: SERIES_1:23

canceled;

theorem Th24: :: SERIES_1:24

for b₁, b₂ being Real_Sequence st ( for b₃ being Nat holds
( 0 <= b₁ . b₃ & b₁ . b₃ <= b₂ . b₃ ) ) & b₂ is summable holds
( b₁ is summable & Sum b₁ <= Sum b₂ )

proof end;

theorem Th25: :: SERIES_1:25

for b₁ being Real_Sequence holds
( b₁ is summable iff for b₂ being real number st 0 < b₂ holds
ex b₃ being Nat st
for b₄ being Nat st b₃ <= b₄ holds
abs (((Partial_Sums b₁) . b₄) - ((Partial_Sums b₁) . b₃)) < b₂ )

proof end;

theorem Th26: :: SERIES_1:26

for b₁ being Nat
for b₂ being real number st b₂ <> 1 holds
(Partial_Sums (b₂ GeoSeq )) . b₁ = (1 - (b₂ to_power (b₁ + 1))) / (1 - b₂)

proof end;

theorem Th27: :: SERIES_1:27

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

proof end;

theorem Th28: :: SERIES_1:28

for b₁ being real number st abs b₁ < 1 holds
( b₁ GeoSeq is summable & Sum (b₁ GeoSeq ) = 1 / (1 - b₁) )

proof end;

theorem Th29: :: SERIES_1:29

for b₁ being real number
for b₂ being Real_Sequence st abs b₁ < 1 & ( for b₃ being Nat holds b₂ . (b₃ + 1) = b₁ * (b₂ . b₃) ) holds
( b₂ is summable & Sum b₂ = (b₂ . 0) / (1 - b₁) )

proof end;

theorem Th30: :: SERIES_1:30

for b₁, b₂ being Real_Sequence st ( for b₃ being Nat holds
( b₁ . b₃ > 0 & b₂ . b₃ = (b₁ . (b₃ + 1)) / (b₁ . b₃) ) ) & b₂ is convergent & lim b₂ < 1 holds
b₁ is summable

proof end;

theorem Th31: :: SERIES_1:31

for b₁ being Real_Sequence st ( for b₂ being Nat holds b₁ . b₂ > 0 ) & ex b₂ being Nat st
for b₃ being Nat st b₃ >= b₂ holds
(b₁ . (b₃ + 1)) / (b₁ . b₃) >= 1 holds
not b₁ is summable

proof end;

theorem Th32: :: SERIES_1:32

for b₁, b₂ being Real_Sequence st ( for b₃ being Nat holds
( b₁ . b₃ >= 0 & b₂ . b₃ = b₃ -root (b₁ . b₃) ) ) & b₂ is convergent & lim b₂ < 1 holds
b₁ is summable

proof end;

theorem Th33: :: SERIES_1:33

for b₁, b₂ being Real_Sequence st ( for b₃ being Nat holds
( b₁ . b₃ >= 0 & b₂ . b₃ = b₃ -root (b₁ . b₃) ) ) & ex b₃ being Nat st
for b₄ being Nat st b₃ <= b₄ holds
b₂ . b₄ >= 1 holds
not b₁ is summable

proof end;

theorem Th34: :: SERIES_1:34

for b₁, b₂ being Real_Sequence st ( for b₃ being Nat holds
( b₁ . b₃ >= 0 & b₂ . b₃ = b₃ -root (b₁ . b₃) ) ) & b₂ is convergent & lim b₂ > 1 holds
not b₁ is summable

proof end;

definition

let c₁, c₂ be Nat;
redefine func to_power as c₁ to_power c₂ -> Nat;
coherence

proof end;

end;

theorem Th35: :: SERIES_1:35

for b₁, b₂ being Real_Sequence st b₁ is non-increasing & ( for b₃ being Nat holds
( b₁ . b₃ >= 0 & b₂ . b₃ = (2 to_power b₃) * (b₁ . (2 to_power b₃)) ) ) holds
( b₁ is summable iff b₂ is summable )

proof end;

theorem Th36: :: SERIES_1:36

for b₁ being real number
for b₂ being Real_Sequence st b₁ > 1 & ( for b₃ being Nat st b₃ >= 1 holds
b₂ . b₃ = 1 / (b₃ to_power b₁) ) holds
b₂ is summable

proof end;

theorem Th37: :: SERIES_1:37

for b₁ being real number
for b₂ being Real_Sequence st b₁ <= 1 & ( for b₃ being Nat st b₃ >= 1 holds
b₂ . b₃ = 1 / (b₃ to_power b₁) ) holds
not b₂ is summable

proof end;

definition

let c₁ be Real_Sequence;
canceled;
attr a₁ is absolutely_summable means :Def5: :: SERIES_1:def 5
abs a₁ is summable;

end;

:: deftheorem Def4 SERIES_1:def 4 :

:: deftheorem Def5 defines absolutely_summable SERIES_1:def 5 :

theorem Th38: :: SERIES_1:38

canceled;

theorem Th39: :: SERIES_1:39

for b₁ being Real_Sequence
for b₂, b₃ being Nat st b₂ <= b₃ holds
abs (((Partial_Sums b₁) . b₃) - ((Partial_Sums b₁) . b₂)) <= abs (((Partial_Sums (abs b₁)) . b₃) - ((Partial_Sums (abs b₁)) . b₂))

proof end;

theorem Th40: :: SERIES_1:40

for b₁ being Real_Sequence st b₁ is absolutely_summable holds
b₁ is summable

proof end;

theorem Th41: :: SERIES_1:41

for b₁ being Real_Sequence st ( for b₂ being Nat holds 0 <= b₁ . b₂ ) & b₁ is summable holds
b₁ is absolutely_summable

proof end;

theorem Th42: :: SERIES_1:42

for b₁, b₂ being Real_Sequence st ( for b₃ being Nat holds
( b₁ . b₃ <> 0 & b₂ . b₃ = ((abs b₁) . (b₃ + 1)) / ((abs b₁) . b₃) ) ) & b₂ is convergent & lim b₂ < 1 holds
b₁ is absolutely_summable

proof end;

theorem Th43: :: SERIES_1:43

for b₁ being real number
for b₂ being Real_Sequence st b₁ > 0 & ex b₃ being Nat st
for b₄ being Nat st b₄ >= b₃ holds
abs (b₂ . b₄) >= b₁ & b₂ is convergent holds
lim b₂ <> 0

proof end;

theorem Th44: :: SERIES_1:44

for b₁ being Real_Sequence st ( for b₂ being Nat holds b₁ . b₂ <> 0 ) & ex b₂ being Nat st
for b₃ being Nat st b₃ >= b₂ holds
((abs b₁) . (b₃ + 1)) / ((abs b₁) . b₃) >= 1 holds
not b₁ is summable

proof end;

theorem Th45: :: SERIES_1:45

for b₁, b₂ being Real_Sequence st ( for b₃ being Nat holds b₁ . b₃ = b₃ -root ((abs b₂) . b₃) ) & b₁ is convergent & lim b₁ < 1 holds
b₂ is absolutely_summable

proof end;

theorem Th46: :: SERIES_1:46

for b₁, b₂ being Real_Sequence st ( for b₃ being Nat holds b₁ . b₃ = b₃ -root ((abs b₂) . b₃) ) & ex b₃ being Nat st
for b₄ being Nat st b₃ <= b₄ holds
b₁ . b₄ >= 1 holds
not b₂ is summable

proof end;

theorem Th47: :: SERIES_1:47

for b₁, b₂ being Real_Sequence st ( for b₃ being Nat holds b₁ . b₃ = b₃ -root ((abs b₂) . b₃) ) & b₁ is convergent & lim b₁ > 1 holds
not b₂ is summable

proof end;