:: COMSEQ_3 semantic presentation

Lemma1: 0c = 0 + (0 * )
;

theorem Th1: :: COMSEQ_3:1

for b₁ being Nat holds
( b₁ + 1 <> 0c & (b₁ + 1) * <> 0c ) by Lemma1;

theorem Th2: :: COMSEQ_3:2

for b₁ being Real_Sequence st ( for b₂ being Nat holds b₁ . b₂ = 0 ) holds
for b₂ being Nat holds (Partial_Sums (abs b₁)) . b₂ = 0

proof end;

theorem Th3: :: COMSEQ_3:3

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

proof end;

reconsider c₁ = NAT --> 0 as Real_Sequence by FUNCOP_1:57;

Lemma4: for b₁ being Nat holds c₁ . b₁ = 0
by FUNCOP_1:13;

registration

cluster summable -> convergent M5( NAT , REAL );
coherence by SERIES_1:7;

end;

registration

cluster absolutely_summable -> convergent summable M5( NAT , REAL );
coherence by SERIES_1:40;

end;

registration

cluster convergent summable absolutely_summable M5( NAT , REAL );
existence

proof end;

end;

theorem Th4: :: COMSEQ_3:4

for b₁ being Real_Sequence st b₁ is convergent holds
for b₂ being Real st 0 < b₂ holds
ex b₃ being Nat st
for b₄, b₅ being Nat st b₃ <= b₄ & b₃ <= b₅ holds
abs ((b₁ . b₄) - (b₁ . b₅)) < b₂

proof end;

theorem Th5: :: COMSEQ_3:5

for b₁ being Real_Sequence
for b₂ being Real st ( for b₃ being Nat holds b₁ . b₃ <= b₂ ) holds
for b₃, b₄ being Nat holds ((Partial_Sums b₁) . (b₃ + b₄)) - ((Partial_Sums b₁) . b₃) <= b₂ * b₄

proof end;

theorem Th6: :: COMSEQ_3:6

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

proof end;

theorem Th7: :: COMSEQ_3:7

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

proof end;

theorem Th8: :: COMSEQ_3:8

for b₁, b₂ being Real_Sequence
for b₃ being Nat
for b₄ being Real st ( for b₅ being Nat st b₅ <= b₃ holds
b₁ . b₅ <= b₄ * (b₂ . b₅) ) holds
for b₅ being Nat st b₅ <= b₃ holds
for b₆ being Nat st b₅ + b₆ <= b₃ holds
((Partial_Sums b₁) . (b₅ + b₆)) - ((Partial_Sums b₁) . b₅) <= b₄ * (((Partial_Sums b₂) . (b₅ + b₆)) - ((Partial_Sums b₂) . b₅))

proof end;

theorem Th9: :: COMSEQ_3:9

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

proof end;

theorem Th10: :: COMSEQ_3:10

for b₁, b₂ being Complex_Sequence st b₁ is convergent & b₂ is convergent & lim (b₁ - b₂) = 0c holds
lim b₁ = lim b₂

proof end;

Lemma5: for b₁ being Complex_Sequence
for b₂ being Nat holds
( |.(b₁ . b₂).| = |.b₁.| . b₂ & 0 <= |.b₁.| . b₂ )

proof end;

definition

let c₂ be complex number ;
func c₁ GeoSeq -> Complex_Sequence means :Def1: :: COMSEQ_3:def 1
( a₂ . 0 = 1r & ( for b₁ being Nat holds a₂ . (b₁ + 1) = (a₂ . b₁) * a₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines GeoSeq COMSEQ_3:def 1 :

definition

let c₂ be complex number ;
let c₃ be natural number ;
func c₁ #N c₂ -> Element of COMPLEX equals :: COMSEQ_3:def 2
(a₁ GeoSeq ) . a₂;
coherence

proof end;

end;

:: deftheorem Def2 defines #N COMSEQ_3:def 2 :

theorem Th11: :: COMSEQ_3:11

for b₁ being Element of COMPLEX holds b₁ #N 0 = 1r by Def1;

definition

let c₂ be Complex_Sequence;
func Re c₁ -> Real_Sequence means :Def3: :: COMSEQ_3:def 3
for b₁ being Nat holds a₂ . b₁ = Re (a₁ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines Re COMSEQ_3:def 3 :

definition

let c₂ be Complex_Sequence;
func Im c₁ -> Real_Sequence means :Def4: :: COMSEQ_3:def 4
for b₁ being Nat holds a₂ . b₁ = Im (a₁ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines Im COMSEQ_3:def 4 :

theorem Th12: :: COMSEQ_3:12

for b₁ being Element of COMPLEX holds |.b₁.| <= (abs (Re b₁)) + (abs (Im b₁))

proof end;

theorem Th13: :: COMSEQ_3:13

for b₁ being Element of COMPLEX holds
( abs (Re b₁) <= |.b₁.| & abs (Im b₁) <= |.b₁.| )

proof end;

theorem Th14: :: COMSEQ_3:14

for b₁, b₂ being Complex_Sequence st Re b₁ = Re b₂ & Im b₁ = Im b₂ holds
b₁ = b₂

proof end;

theorem Th15: :: COMSEQ_3:15

for b₁, b₂ being Complex_Sequence holds
( (Re b₁) + (Re b₂) = Re (b₁ + b₂) & (Im b₁) + (Im b₂) = Im (b₁ + b₂) )

proof end;

theorem Th16: :: COMSEQ_3:16

for b₁ being Complex_Sequence holds
( - (Re b₁) = Re (- b₁) & - (Im b₁) = Im (- b₁) )

proof end;

theorem Th17: :: COMSEQ_3:17

for b₁ being Real
for b₂ being Element of COMPLEX holds
( b₁ * (Re b₂) = Re (b₁ * b₂) & b₁ * (Im b₂) = Im (b₁ * b₂) )

proof end;

theorem Th18: :: COMSEQ_3:18

for b₁, b₂ being Complex_Sequence holds
( (Re b₁) - (Re b₂) = Re (b₁ - b₂) & (Im b₁) - (Im b₂) = Im (b₁ - b₂) )

proof end;

theorem Th19: :: COMSEQ_3:19

for b₁ being Complex_Sequence
for b₂ being Real holds
( b₂ (#) (Re b₁) = Re (b₂ (#) b₁) & b₂ (#) (Im b₁) = Im (b₂ (#) b₁) )

proof end;

theorem Th20: :: COMSEQ_3:20

for b₁ being Complex_Sequence
for b₂ being Element of COMPLEX holds
( Re (b₂ (#) b₁) = ((Re b₂) (#) (Re b₁)) - ((Im b₂) (#) (Im b₁)) & Im (b₂ (#) b₁) = ((Re b₂) (#) (Im b₁)) + ((Im b₂) (#) (Re b₁)) )

proof end;

theorem Th21: :: COMSEQ_3:21

for b₁, b₂ being Complex_Sequence holds
( Re (b₁ (#) b₂) = ((Re b₁) (#) (Re b₂)) - ((Im b₁) (#) (Im b₂)) & Im (b₁ (#) b₂) = ((Re b₁) (#) (Im b₂)) + ((Im b₁) (#) (Re b₂)) )

proof end;

definition

let c₂ be increasing Seq_of_Nat;
let c₃ be Complex_Sequence;
redefine func * as c₂ * c₁ -> Complex_Sequence;
coherence

proof end;

end;

theorem Th22: :: COMSEQ_3:22

for b₁ being Complex_Sequence
for b₂ being increasing Seq_of_Nat holds
( Re (b₁ * b₂) = (Re b₁) * b₂ & Im (b₁ * b₂) = (Im b₁) * b₂ )

proof end;

definition

let c₂ be Complex_Sequence;
let c₃ be Nat;
canceled;
func c₁ ^\ c₂ -> Complex_Sequence means :Def6: :: COMSEQ_3:def 6
for b₁ being Nat holds a₃ . b₁ = a₁ . (b₁ + a₂);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 COMSEQ_3:def 5 :

:: deftheorem Def6 defines ^\ COMSEQ_3:def 6 :

theorem Th23: :: COMSEQ_3:23

for b₁ being Complex_Sequence
for b₂ being Nat holds
( (Re b₁) ^\ b₂ = Re (b₁ ^\ b₂) & (Im b₁) ^\ b₂ = Im (b₁ ^\ b₂) )

proof end;

definition

let c₂ be Complex_Sequence;
func Partial_Sums c₁ -> Complex_Sequence means :Def7: :: COMSEQ_3:def 7
( 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 Def7 defines Partial_Sums COMSEQ_3:def 7 :

definition

let c₂ be Complex_Sequence;
func Sum c₁ -> Element of COMPLEX equals :: COMSEQ_3:def 8
lim (Partial_Sums a₁);
coherence ;

end;

:: deftheorem Def8 defines Sum COMSEQ_3:def 8 :

theorem Th24: :: COMSEQ_3:24

for b₁ being Complex_Sequence st ( for b₂ being Nat holds b₁ . b₂ = 0c ) holds
for b₂ being Nat holds (Partial_Sums b₁) . b₂ = 0c

proof end;

theorem Th25: :: COMSEQ_3:25

for b₁ being Complex_Sequence st ( for b₂ being Nat holds b₁ . b₂ = 0c ) holds
for b₂ being Nat holds (Partial_Sums |.b₁.|) . b₂ = 0

proof end;

theorem Th26: :: COMSEQ_3:26

for b₁ being Complex_Sequence holds
( Partial_Sums (Re b₁) = Re (Partial_Sums b₁) & Partial_Sums (Im b₁) = Im (Partial_Sums b₁) )

proof end;

theorem Th27: :: COMSEQ_3:27

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

proof end;

theorem Th28: :: COMSEQ_3:28

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

proof end;

theorem Th29: :: COMSEQ_3:29

for b₁ being Complex_Sequence
for b₂ being Element of COMPLEX holds Partial_Sums (b₂ (#) b₁) = b₂ (#) (Partial_Sums b₁)

proof end;

theorem Th30: :: COMSEQ_3:30

for b₁ being Complex_Sequence
for b₂ being Nat holds |.((Partial_Sums b₁) . b₂).| <= (Partial_Sums |.b₁.|) . b₂

proof end;

theorem Th31: :: COMSEQ_3:31

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

proof end;

theorem Th32: :: COMSEQ_3:32

for b₁ being Complex_Sequence
for b₂ being Nat holds
( (Partial_Sums (Re b₁)) ^\ b₂ = Re ((Partial_Sums b₁) ^\ b₂) & (Partial_Sums (Im b₁)) ^\ b₂ = Im ((Partial_Sums b₁) ^\ b₂) )

proof end;

theorem Th33: :: COMSEQ_3:33

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

proof end;

theorem Th34: :: COMSEQ_3:34

for b₁ being Complex_Sequence holds Partial_Sums |.b₁.| is non-decreasing

proof end;

registration

let c₂ be Complex_Sequence;
cluster Partial_Sums |.a₁.| -> non-decreasing ;
coherence by Th34;

end;

theorem Th35: :: COMSEQ_3:35

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

proof end;

theorem Th36: :: COMSEQ_3:36

for b₁ being Element of COMPLEX st 1r <> b₁ holds
for b₂ being Nat holds (Partial_Sums (b₁ GeoSeq )) . b₂ = (1r - (b₁ #N (b₂ + 1))) / (1r - b₁)

proof end;

theorem Th37: :: COMSEQ_3:37

for b₁ being Complex_Sequence
for b₂ being Element of COMPLEX st b₂ <> 1r & ( for b₃ being Nat holds b₁ . (b₃ + 1) = b₂ * (b₁ . b₃) ) holds
for b₃ being Nat holds (Partial_Sums b₁) . b₃ = (b₁ . 0) * ((1r - (b₂ #N (b₃ + 1))) / (1r - b₂))

proof end;

theorem Th38: :: COMSEQ_3:38

for b₁, b₂ being Real_Sequence
for b₃ being Complex_Sequence st ( for b₄ being Nat holds
( Re (b₃ . b₄) = b₁ . b₄ & Im (b₃ . b₄) = b₂ . b₄ ) ) holds
( ( b₁ is convergent & b₂ is convergent ) iff b₃ is convergent )

proof end;

theorem Th39: :: COMSEQ_3:39

for b₁, b₂ being convergent Real_Sequence
for b₃ being Complex_Sequence st ( for b₄ being Nat holds
( Re (b₃ . b₄) = b₁ . b₄ & Im (b₃ . b₄) = b₂ . b₄ ) ) holds
( b₃ is convergent & lim b₃ = (lim b₁) + ((lim b₂) * ) )

proof end;

theorem Th40: :: COMSEQ_3:40

for b₁, b₂ being Real_Sequence
for b₃ being convergent Complex_Sequence st ( for b₄ being Nat holds
( Re (b₃ . b₄) = b₁ . b₄ & Im (b₃ . b₄) = b₂ . b₄ ) ) holds
( b₁ is convergent & b₂ is convergent & lim b₁ = Re (lim b₃) & lim b₂ = Im (lim b₃) )

proof end;

theorem Th41: :: COMSEQ_3:41

for b₁ being convergent Complex_Sequence holds
( Re b₁ is convergent & Im b₁ is convergent & lim (Re b₁) = Re (lim b₁) & lim (Im b₁) = Im (lim b₁) )

proof end;

registration

let c₂ be convergent Complex_Sequence;
cluster Re a₁ -> convergent ;
coherence by Th41;
cluster Im a₁ -> convergent ;
coherence by Th41;

end;

theorem Th42: :: COMSEQ_3:42

for b₁ being Complex_Sequence st Re b₁ is convergent & Im b₁ is convergent holds
( b₁ is convergent & Re (lim b₁) = lim (Re b₁) & Im (lim b₁) = lim (Im b₁) )

proof end;

theorem Th43: :: COMSEQ_3:43

for b₁ being Complex_Sequence
for b₂ being Element of COMPLEX st 0 < |.b₂.| & |.b₂.| < 1 & b₁ . 0 = b₂ & ( for b₃ being Nat holds b₁ . (b₃ + 1) = (b₁ . b₃) * b₂ ) holds
( b₁ is convergent & lim b₁ = 0c )

proof end;

theorem Th44: :: COMSEQ_3:44

for b₁ being Complex_Sequence
for b₂ being Element of COMPLEX st |.b₂.| < 1 & ( for b₃ being Nat holds b₁ . b₃ = b₂ #N (b₃ + 1) ) holds
( b₁ is convergent & lim b₁ = 0c )

proof end;

theorem Th45: :: COMSEQ_3:45

for b₁ being Complex_Sequence
for b₂ being Real st b₂ > 0 & ex b₃ being Nat st
for b₄ being Nat st b₄ >= b₃ holds
|.(b₁ . b₄).| >= b₂ & |.b₁.| is convergent holds
lim |.b₁.| <> 0

proof end;

theorem Th46: :: COMSEQ_3:46

for b₁ being Complex_Sequence holds
( b₁ is convergent iff for b₂ being Real st 0 < b₂ holds
ex b₃ being Nat st
for b₄ being Nat st b₃ <= b₄ holds
|.((b₁ . b₄) - (b₁ . b₃)).| < b₂ )

proof end;

theorem Th47: :: COMSEQ_3:47

for b₁ being Complex_Sequence st b₁ is convergent holds
for b₂ being Real st 0 < b₂ holds
ex b₃ being Nat st
for b₄, b₅ being Nat st b₃ <= b₄ & b₃ <= b₅ holds
|.((b₁ . b₄) - (b₁ . b₅)).| < b₂

proof end;

theorem Th48: :: COMSEQ_3:48

for b₁ being Real_Sequence
for b₂ being Complex_Sequence st ( for b₃ being Nat holds |.(b₂ . b₃).| <= b₁ . b₃ ) & b₁ is convergent & lim b₁ = 0 holds
( b₂ is convergent & lim b₂ = 0c )

proof end;

definition

let c₂ be Complex_Sequence;
mode subsequence of c₁ -> Complex_Sequence means :Def9: :: COMSEQ_3:def 9
ex b₁ being increasing Seq_of_Nat st a₂ = a₁ * b₁;
existence

proof end;

end;

:: deftheorem Def9 defines subsequence COMSEQ_3:def 9 :

theorem Th49: :: COMSEQ_3:49

for b₁, b₂ being Complex_Sequence st b₁ is subsequence of b₂ holds
( Re b₁ is subsequence of Re b₂ & Im b₁ is subsequence of Im b₂ )

proof end;

theorem Th50: :: COMSEQ_3:50

for b₁, b₂, b₃ being Complex_Sequence st b₁ is subsequence of b₂ & b₂ is subsequence of b₃ holds
b₁ is subsequence of b₃

proof end;

theorem Th51: :: COMSEQ_3:51

for b₁ being Complex_Sequence st b₁ is bounded holds
ex b₂ being Complex_Sequence st
( b₂ is subsequence of b₁ & b₂ is convergent )

proof end;

definition

let c₂ be Complex_Sequence;
attr a₁ is summable means :Def10: :: COMSEQ_3:def 10
Partial_Sums a₁ is convergent;

end;

:: deftheorem Def10 defines summable COMSEQ_3:def 10 :

reconsider c₂ = NAT --> 0c as Complex_Sequence by FUNCOP_1:57;

Lemma42: for b₁ being Nat holds c₁ . b₁ = 0c
by FUNCOP_1:13;

registration

cluster summable M5( NAT , COMPLEX );
existence

proof end;

end;

registration

let c₃ be summable Complex_Sequence;
cluster Partial_Sums a₁ -> convergent ;
coherence by Def10;

end;

definition

let c₃ be Complex_Sequence;
attr a₁ is absolutely_summable means :Def11: :: COMSEQ_3:def 11
|.a₁.| is summable;

end;

:: deftheorem Def11 defines absolutely_summable COMSEQ_3:def 11 :

theorem Th52: :: COMSEQ_3:52

for b₁ being Complex_Sequence st ( for b₂ being Nat holds b₁ . b₂ = 0c ) holds
b₁ is absolutely_summable

proof end;

registration

cluster absolutely_summable M5( NAT , COMPLEX );
existence

proof end;

end;

registration

let c₃ be absolutely_summable Complex_Sequence;
cluster |.a₁.| -> convergent summable ;
coherence by Def11;

end;

theorem Th53: :: COMSEQ_3:53

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

proof end;

registration

cluster summable -> convergent M5( NAT , COMPLEX );
coherence by Th53;

end;

theorem Th54: :: COMSEQ_3:54

for b₁ being Complex_Sequence st b₁ is summable holds
( Re b₁ is summable & Im b₁ is summable & Sum b₁ = (Sum (Re b₁)) + ((Sum (Im b₁)) * ) )

proof end;

registration

let c₃ be summable Complex_Sequence;
cluster Re a₁ -> convergent summable ;
coherence by Th54;
cluster Im a₁ -> convergent summable ;
coherence by Th54;

end;

theorem Th55: :: COMSEQ_3:55

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

proof end;

theorem Th56: :: COMSEQ_3:56

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

proof end;

registration

let c₃, c₄ be summable Complex_Sequence;
cluster a₁ + a₂ -> convergent summable ;
coherence by Th55;
cluster a₁ - a₂ -> convergent summable ;
coherence by Th56;

end;

theorem Th57: :: COMSEQ_3:57

for b₁ being Complex_Sequence
for b₂ being Element of COMPLEX st b₁ is summable holds
( b₂ (#) b₁ is summable & Sum (b₂ (#) b₁) = b₂ * (Sum b₁) )

proof end;

registration

let c₃ be Element of COMPLEX ;
let c₄ be summable Complex_Sequence;
cluster a₁ (#) a₂ -> convergent summable ;
coherence by Th57;

end;

theorem Th58: :: COMSEQ_3:58

for b₁ being Complex_Sequence st Re b₁ is summable & Im b₁ is summable holds
( b₁ is summable & Sum b₁ = (Sum (Re b₁)) + ((Sum (Im b₁)) * ) )

proof end;

theorem Th59: :: COMSEQ_3:59

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

proof end;

registration

let c₃ be summable Complex_Sequence;
let c₄ be Nat;
cluster a₁ ^\ a₂ -> convergent summable ;
coherence by Th59;

end;

theorem Th60: :: COMSEQ_3:60

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

proof end;

theorem Th61: :: COMSEQ_3:61

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

proof end;

theorem Th62: :: COMSEQ_3:62

for b₁ being Complex_Sequence holds
( Partial_Sums |.b₁.| is bounded_above iff b₁ is absolutely_summable )

proof end;

registration

let c₃ be absolutely_summable Complex_Sequence;
cluster Partial_Sums |.a₁.| -> bounded_above non-decreasing ;
coherence by Th62;

end;

theorem Th63: :: COMSEQ_3:63

for b₁ being Complex_Sequence holds
( b₁ is summable iff for b₂ being Real st 0 < b₂ holds
ex b₃ being Nat st
for b₄ being Nat st b₃ <= b₄ holds
|.(((Partial_Sums b₁) . b₄) - ((Partial_Sums b₁) . b₃)).| < b₂ )

proof end;

theorem Th64: :: COMSEQ_3:64

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

proof end;

registration

cluster absolutely_summable -> convergent summable M5( NAT , COMPLEX );
coherence by Th64;

end;

registration

cluster convergent summable absolutely_summable M5( NAT , COMPLEX );
existence

proof end;

end;

theorem Th65: :: COMSEQ_3:65

for b₁ being Element of COMPLEX st |.b₁.| < 1 holds
( b₁ GeoSeq is summable & Sum (b₁ GeoSeq ) = 1r / (1r - b₁) )

proof end;

theorem Th66: :: COMSEQ_3:66

for b₁ being Complex_Sequence
for b₂ being Element of COMPLEX st |.b₂.| < 1 & ( for b₃ being Nat holds b₁ . (b₃ + 1) = b₂ * (b₁ . b₃) ) holds
( b₁ is summable & Sum b₁ = (b₁ . 0) / (1r - b₂) )

proof end;

theorem Th67: :: COMSEQ_3:67

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

proof end;

theorem Th68: :: COMSEQ_3:68

for b₁, b₂ being Complex_Sequence st ( for b₃ being Nat holds
( 0 <= |.b₁.| . b₃ & |.b₁.| . b₃ <= |.b₂.| . b₃ ) ) & b₂ is absolutely_summable holds
( b₁ is absolutely_summable & Sum |.b₁.| <= Sum |.b₂.| )

proof end;

theorem Th69: :: COMSEQ_3:69

for b₁ being Complex_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 absolutely_summable

proof end;

theorem Th70: :: COMSEQ_3:70

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

proof end;

theorem Th71: :: COMSEQ_3:71

for b₁ being Real_Sequence
for b₂ being Complex_Sequence st ( for b₃ being Nat holds 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 Th72: :: COMSEQ_3:72

for b₁ being Real_Sequence
for b₂ being Complex_Sequence st ( for b₃ being Nat holds b₁ . b₃ = b₃ -root (|.b₂.| . b₃) ) & b₁ is convergent & lim b₁ > 1 holds
not b₂ is absolutely_summable

proof end;

theorem Th73: :: COMSEQ_3:73

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

proof end;

theorem Th74: :: COMSEQ_3:74

for b₁ being Complex_Sequence
for b₂ being Real st b₂ > 1 & ( for b₃ being Nat st b₃ >= 1 holds
|.b₁.| . b₃ = 1 / (b₃ to_power b₂) ) holds
b₁ is absolutely_summable

proof end;

theorem Th75: :: COMSEQ_3:75

for b₁ being Complex_Sequence
for b₂ being Real st b₂ <= 1 & ( for b₃ being Nat st b₃ >= 1 holds
|.b₁.| . b₃ = 1 / (b₃ to_power b₂) ) holds
not b₁ is absolutely_summable

proof end;

theorem Th76: :: COMSEQ_3:76

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

proof end;

theorem Th77: :: COMSEQ_3:77

for b₁ being Complex_Sequence st ( for b₂ being Nat holds b₁ . b₂ <> 0c ) & ex b₂ being Nat st
for b₃ being Nat st b₃ >= b₂ holds
(|.b₁.| . (b₃ + 1)) / (|.b₁.| . b₃) >= 1 holds
not b₁ is absolutely_summable

proof end;