:: Convergence and the Limit of Complex Sequences. Series
:: by Yasunari Shidama and Artur Korni{\l}owicz
::
:: Received June 25, 1997
:: Copyright (c) 1997-2012 Association of Mizar Users


begin

Lm1:  0c = 0 + (0 * <i>)
;

theorem :: COMSEQ_3:1
for n being Element of NAT holds
( n + 1 <> 0c &amp; (n + 1) * <i> <> 0c ) ;

theorem Th2: :: COMSEQ_3:2
for rseq being Real_Sequence st ( for n being Element of NAT holds rseq . n = 0 ) holds
for m being Element of NAT holds (Partial_Sums (abs rseq)) . m = 0
proofend;

theorem Th3: :: COMSEQ_3:3
for rseq being Real_Sequence st ( for n being Element of NAT holds rseq . n = 0 ) holds
rseq is absolutely_summable
proofend;

reconsider C = NAT --> 0 as Real_Sequence by FUNCOP_1:45;

Lm2:  for n being Element of NAT holds C . n = 0
by FUNCOP_1:7;

registration
cluster Function-like V18( NAT , REAL ) summable  ->  convergent for Element of K19(K20(NAT,REAL));
coherence
 for b1 being Real_Sequence st b1 is summable holds
b1 is convergent by SERIES_1:4;
end;

registration
cluster Function-like V18( NAT , REAL ) absolutely_summable  ->  summable for Element of K19(K20(NAT,REAL));
coherence
 for b1 being Real_Sequence st b1 is absolutely_summable holds
b1 is summable ;
end;

registration
cluster Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued absolutely_summable for Element of K19(K20(NAT,REAL));
existence
 ex b1 being Real_Sequence st b1 is absolutely_summable by Lm2, Th3;
end;

theorem :: COMSEQ_3:4
for rseq being Real_Sequence st rseq is convergent holds
for p being Real st 0 < p holds
ex n being Element of NAT st
for m, l being Element of NAT st n <= m &amp; n <= l holds
abs ((rseq . m) - (rseq . l)) < p
proofend;

theorem :: COMSEQ_3:5
for rseq being Real_Sequence
for p being Real st ( for n being Element of NAT holds rseq . n <= p ) holds
for n, l being Element of NAT holds ((Partial_Sums rseq) . (n + l)) - ((Partial_Sums rseq) . n) <= p * l
proofend;

theorem :: COMSEQ_3:6
for rseq being Real_Sequence
for p being Real st ( for n being Element of NAT holds rseq . n <= p ) holds
for n being Element of NAT holds (Partial_Sums rseq) . n <= p * (n + 1)
proofend;

theorem :: COMSEQ_3:7
for rseq1, rseq2 being Real_Sequence
for m being Element of NAT
for p being Real st ( for n being Element of NAT st n <= m holds
rseq1 . n <= p * (rseq2 . n) ) holds
(Partial_Sums rseq1) . m <= p * ((Partial_Sums rseq2) . m)
proofend;

theorem :: COMSEQ_3:8
for rseq1, rseq2 being Real_Sequence
for m being Element of NAT
for p being Real st ( for n being Element of NAT st n <= m holds
rseq1 . n <= p * (rseq2 . n) ) holds
for n, l being Element of NAT st n + l <= m holds
((Partial_Sums rseq1) . (n + l)) - ((Partial_Sums rseq1) . n) <= p * (((Partial_Sums rseq2) . (n + l)) - ((Partial_Sums rseq2) . n))
proofend;

theorem :: COMSEQ_3:9
for rseq being Real_Sequence st ( for n being Element of NAT holds 0 <= rseq . n ) holds
( ( for n, m being Element of NAT st n <= m holds
abs (((Partial_Sums rseq) . m) - ((Partial_Sums rseq) . n)) = ((Partial_Sums rseq) . m) - ((Partial_Sums rseq) . n) ) &amp; ( for n being Element of NAT holds abs ((Partial_Sums rseq) . n) = (Partial_Sums rseq) . n ) )
proofend;

theorem :: COMSEQ_3:10
for seq1, seq2 being Complex_Sequence st seq1 is convergent &amp; seq2 is convergent &amp; lim (seq1 - seq2) = 0c holds
lim seq1 = lim seq2
proofend;

begin

Lm3:  for seq being Complex_Sequence
for n being Element of NAT holds
( |.(seq . n).| = |.seq.| . n &amp; 0 <= |.seq.| . n )
proofend;

definition
let z be complex number ;
funcz GeoSeq  ->  Complex_Sequence means :Def1: :: COMSEQ_3:def 1
( it . 0 = 1r &amp; ( for n being Element of NAT holds it . (n + 1) = (it . n) * z ) );
existence
 ex b1 being Complex_Sequence st
( b1 . 0 = 1r &amp; ( for n being Element of NAT holds b1 . (n + 1) = (b1 . n) * z ) )
proofend;
uniqueness
 for b1, b2 being Complex_Sequence st b1 . 0 = 1r &amp; ( for n being Element of NAT holds b1 . (n + 1) = (b1 . n) * z ) &amp; b2 . 0 = 1r &amp; ( for n being Element of NAT holds b2 . (n + 1) = (b2 . n) * z ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines GeoSeq COMSEQ_3:def_1_:_
 for z being complex number
for b2 being Complex_Sequence holds
( b2 = z GeoSeq iff ( b2 . 0 = 1r &amp; ( for n being Element of NAT holds b2 . (n + 1) = (b2 . n) * z ) ) );

notation
let z be complex number ;
let n be natural number ;
synonym z #N n for z |^ n;
end;

definition
let z be complex number ;
let n be natural number ;
:: original:#N
redefine funcz #N n ->  Element of COMPLEX  equals :: COMSEQ_3:def 2
(z GeoSeq) . n;
coherence
 z #N n is Element of COMPLEX by XCMPLX_0:def_2;
compatibility
 for b1 being Element of COMPLEX holds
( b1 = z #N n iff b1 = (z GeoSeq) . n )
proofend;
end;

:: deftheorem  defines #N COMSEQ_3:def_2_:_
 for z being complex number
for n being natural number holds z #N n = (z GeoSeq) . n;

theorem :: COMSEQ_3:11
for z being Element of COMPLEX holds z #N 0 = 1r by COMPLEX1:def_4, NEWTON:4;

definition
let f be complex-valued Function;
set A = dom f;
deffunc H1( set ) ->  Element of REAL = Re (f . $1);
func Re f ->  Function means :Def3: :: COMSEQ_3:def 3
( dom it = dom f &amp; ( for x being set st x in dom it holds
it . x = Re (f . x) ) );
existence
 ex b1 being Function st
( dom b1 = dom f &amp; ( for x being set st x in dom b1 holds
b1 . x = Re (f . x) ) )
proofend;
uniqueness
 for b1, b2 being Function st dom b1 = dom f &amp; ( for x being set st x in dom b1 holds
b1 . x = Re (f . x) ) &amp; dom b2 = dom f &amp; ( for x being set st x in dom b2 holds
b2 . x = Re (f . x) ) holds
b1 = b2
proofend;
deffunc H2( set ) ->  Element of REAL = Im (f . $1);
func Im f ->  Function means :Def4: :: COMSEQ_3:def 4
( dom it = dom f &amp; ( for x being set st x in dom it holds
it . x = Im (f . x) ) );
existence
 ex b1 being Function st
( dom b1 = dom f &amp; ( for x being set st x in dom b1 holds
b1 . x = Im (f . x) ) )
proofend;
uniqueness
 for b1, b2 being Function st dom b1 = dom f &amp; ( for x being set st x in dom b1 holds
b1 . x = Im (f . x) ) &amp; dom b2 = dom f &amp; ( for x being set st x in dom b2 holds
b2 . x = Im (f . x) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines Re COMSEQ_3:def_3_:_
 for f being complex-valued Function
for b2 being Function holds
( b2 = Re f iff ( dom b2 = dom f &amp; ( for x being set st x in dom b2 holds
b2 . x = Re (f . x) ) ) );

:: deftheorem Def4 defines Im COMSEQ_3:def_4_:_
 for f being complex-valued Function
for b2 being Function holds
( b2 = Im f iff ( dom b2 = dom f &amp; ( for x being set st x in dom b2 holds
b2 . x = Im (f . x) ) ) );

registration
let f be complex-valued Function;
cluster Re f ->  real-valued ;
coherence
 Re f is real-valued
proofend;
cluster Im f ->  real-valued ;
coherence
 Im f is real-valued
proofend;
end;

definition
let X be set ;
let f be PartFunc of X,COMPLEX;
:: original:Re
redefine func Re f ->  PartFunc of X,REAL;
coherence
 Re f is PartFunc of X,REAL
proofend;
:: original:Im
redefine func Im f ->  PartFunc of X,REAL;
coherence
 Im f is PartFunc of X,REAL
proofend;
end;

definition
let c be Complex_Sequence;
:: original:Re
redefine func Re c ->  Real_Sequence means :Def5: :: COMSEQ_3:def 5
 for n being Element of NAT holds it . n = Re (c . n);
coherence
 Re c is Real_Sequence
proofend;
compatibility
 for b1 being Real_Sequence holds
( b1 = Re c iff for n being Element of NAT holds b1 . n = Re (c . n) )
proofend;
:: original:Im
redefine func Im c ->  Real_Sequence means :Def6: :: COMSEQ_3:def 6
 for n being Element of NAT holds it . n = Im (c . n);
coherence
 Im c is Real_Sequence
proofend;
compatibility
 for b1 being Real_Sequence holds
( b1 = Im c iff for n being Element of NAT holds b1 . n = Im (c . n) )
proofend;
end;

:: deftheorem Def5 defines Re COMSEQ_3:def_5_:_
 for c being Complex_Sequence
for b2 being Real_Sequence holds
( b2 = Re c iff for n being Element of NAT holds b2 . n = Re (c . n) );

:: deftheorem Def6 defines Im COMSEQ_3:def_6_:_
 for c being Complex_Sequence
for b2 being Real_Sequence holds
( b2 = Im c iff for n being Element of NAT holds b2 . n = Im (c . n) );

theorem Th12: :: COMSEQ_3:12
for z being Element of COMPLEX holds |.z.| <= (abs (Re z)) + (abs (Im z))
proofend;

theorem Th13: :: COMSEQ_3:13
for z being Element of COMPLEX holds
( abs (Re z) <= |.z.| &amp; abs (Im z) <= |.z.| )
proofend;

theorem Th14: :: COMSEQ_3:14
for seq1, seq2 being Complex_Sequence st Re seq1 = Re seq2 &amp; Im seq1 = Im seq2 holds
seq1 = seq2
proofend;

theorem Th15: :: COMSEQ_3:15
for seq1, seq2 being Complex_Sequence holds
( (Re seq1) + (Re seq2) = Re (seq1 + seq2) &amp; (Im seq1) + (Im seq2) = Im (seq1 + seq2) )
proofend;

theorem Th16: :: COMSEQ_3:16
for seq being Complex_Sequence holds
( - (Re seq) = Re (- seq) &amp; - (Im seq) = Im (- seq) )
proofend;

theorem Th17: :: COMSEQ_3:17
for r being Real
for z being Element of COMPLEX holds
( r * (Re z) = Re (r * z) &amp; r * (Im z) = Im (r * z) )
proofend;

theorem Th18: :: COMSEQ_3:18
for seq1, seq2 being Complex_Sequence holds
( (Re seq1) - (Re seq2) = Re (seq1 - seq2) &amp; (Im seq1) - (Im seq2) = Im (seq1 - seq2) )
proofend;

theorem :: COMSEQ_3:19
for seq being Complex_Sequence
for r being Real holds
( r (#) (Re seq) = Re (r (#) seq) &amp; r (#) (Im seq) = Im (r (#) seq) )
proofend;

theorem :: COMSEQ_3:20
for seq being Complex_Sequence
for z being Element of COMPLEX holds
( Re (z (#) seq) = ((Re z) (#) (Re seq)) - ((Im z) (#) (Im seq)) &amp; Im (z (#) seq) = ((Re z) (#) (Im seq)) + ((Im z) (#) (Re seq)) )
proofend;

theorem :: COMSEQ_3:21
for seq1, seq2 being Complex_Sequence holds
( Re (seq1 (#) seq2) = ((Re seq1) (#) (Re seq2)) - ((Im seq1) (#) (Im seq2)) &amp; Im (seq1 (#) seq2) = ((Re seq1) (#) (Im seq2)) + ((Im seq1) (#) (Re seq2)) )
proofend;

definition
let Nseq be increasing sequence of NAT;
let seq be Complex_Sequence;
:: original:(#)
redefine funcseq * Nseq ->  Complex_Sequence;
coherence
 Nseq (#) seq is Complex_Sequence
proofend;
end;

theorem Th22: :: COMSEQ_3:22
for seq being Complex_Sequence
for Nseq being increasing sequence of NAT holds
( Re (seq * Nseq) = (Re seq) * Nseq &amp; Im (seq * Nseq) = (Im seq) * Nseq )
proofend;

theorem Th23: :: COMSEQ_3:23
for seq being Complex_Sequence
for k being Element of NAT holds
( (Re seq) ^\ k = Re (seq ^\ k) &amp; (Im seq) ^\ k = Im (seq ^\ k) )
proofend;

definition
let s be Complex_Sequence;
:: original:Partial_Sums
redefine func Partial_Sums s ->  Complex_Sequence;
coherence
 Partial_Sums s is Complex_Sequence
proofend;
end;

definition
let seq be Complex_Sequence;
func Sum seq ->  Element of COMPLEX  equals :: COMSEQ_3:def 7
 lim (Partial_Sums seq);
coherence
 lim (Partial_Sums seq) is Element of COMPLEX ;
end;

:: deftheorem  defines Sum COMSEQ_3:def_7_:_
 for seq being Complex_Sequence holds Sum seq = lim (Partial_Sums seq);

theorem Th24: :: COMSEQ_3:24
for seq being Complex_Sequence st ( for n being Element of NAT holds seq . n = 0c ) holds
for m being Element of NAT holds (Partial_Sums seq) . m = 0c
proofend;

theorem Th25: :: COMSEQ_3:25
for seq being Complex_Sequence st ( for n being Element of NAT holds seq . n = 0c ) holds
for m being Element of NAT holds (Partial_Sums |.seq.|) . m = 0
proofend;

theorem Th26: :: COMSEQ_3:26
for seq being Complex_Sequence holds
( Partial_Sums (Re seq) = Re (Partial_Sums seq) &amp; Partial_Sums (Im seq) = Im (Partial_Sums seq) )
proofend;

theorem Th27: :: COMSEQ_3:27
for seq1, seq2 being Complex_Sequence holds (Partial_Sums seq1) + (Partial_Sums seq2) = Partial_Sums (seq1 + seq2) by SERIES_1:5;

theorem Th28: :: COMSEQ_3:28
for seq1, seq2 being Complex_Sequence holds (Partial_Sums seq1) - (Partial_Sums seq2) = Partial_Sums (seq1 - seq2)
proofend;

theorem Th29: :: COMSEQ_3:29
for seq being Complex_Sequence
for z being complex number holds Partial_Sums (z (#) seq) = z (#) (Partial_Sums seq)
proofend;

theorem :: COMSEQ_3:30
for seq being Complex_Sequence
for k being Element of NAT holds |.((Partial_Sums seq) . k).| <= (Partial_Sums |.seq.|) . k
proofend;

theorem Th31: :: COMSEQ_3:31
for seq being Complex_Sequence
for m, n being Element of NAT holds |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n))
proofend;

theorem Th32: :: COMSEQ_3:32
for seq being Complex_Sequence
for k being Element of NAT holds
( (Partial_Sums (Re seq)) ^\ k = Re ((Partial_Sums seq) ^\ k) &amp; (Partial_Sums (Im seq)) ^\ k = Im ((Partial_Sums seq) ^\ k) )
proofend;

theorem :: COMSEQ_3:33
for seq1, seq being Complex_Sequence st ( for n being Element of NAT holds seq1 . n = seq . 0 ) holds
Partial_Sums (seq ^\ 1) = ((Partial_Sums seq) ^\ 1) - seq1
proofend;

theorem Th34: :: COMSEQ_3:34
for seq being Complex_Sequence holds Partial_Sums |.seq.| is non-decreasing
proofend;

registration
let seq be Complex_Sequence;
cluster Partial_Sums |.seq.| ->  non-decreasing for Real_Sequence;
coherence
 for b1 being Real_Sequence st b1 = Partial_Sums |.seq.| holds
b1 is non-decreasing by Th34;
end;

theorem :: COMSEQ_3:35
for seq1, seq2 being Complex_Sequence
for m being Element of NAT st ( for n being Element of NAT st n <= m holds
seq1 . n = seq2 . n ) holds
(Partial_Sums seq1) . m = (Partial_Sums seq2) . m
proofend;

theorem Th36: :: COMSEQ_3:36
for z being Element of COMPLEX st 1r <> z holds
for n being Element of NAT holds (Partial_Sums (z GeoSeq)) . n = (1r - (z #N (n + 1))) / (1r - z)
proofend;

theorem Th37: :: COMSEQ_3:37
for seq being Complex_Sequence
for z being Element of COMPLEX st z <> 1r &amp; ( for n being Element of NAT holds seq . (n + 1) = z * (seq . n) ) holds
for n being Element of NAT holds (Partial_Sums seq) . n = (seq . 0) * ((1r - (z #N (n + 1))) / (1r - z))
proofend;

begin

theorem Th38: :: COMSEQ_3:38
for a, b being Real_Sequence
for c being Complex_Sequence st ( for n being Element of NAT holds
( Re (c . n) = a . n &amp; Im (c . n) = b . n ) ) holds
( ( a is convergent &amp; b is convergent ) iff c is convergent )
proofend;

theorem Th39: :: COMSEQ_3:39
for a, b being convergent Real_Sequence
for c being Complex_Sequence st ( for n being Element of NAT holds
( Re (c . n) = a . n &amp; Im (c . n) = b . n ) ) holds
( c is convergent &amp; lim c = (lim a) + ((lim b) * <i>) )
proofend;

theorem Th40: :: COMSEQ_3:40
for a, b being Real_Sequence
for c being convergent Complex_Sequence st ( for n being Element of NAT holds
( Re (c . n) = a . n &amp; Im (c . n) = b . n ) ) holds
( a is convergent &amp; b is convergent &amp; lim a = Re (lim c) &amp; lim b = Im (lim c) )
proofend;

theorem Th41: :: COMSEQ_3:41
for c being convergent Complex_Sequence holds
( Re c is convergent &amp; Im c is convergent &amp; lim (Re c) = Re (lim c) &amp; lim (Im c) = Im (lim c) )
proofend;

registration
let c be convergent Complex_Sequence;
cluster Re c ->  convergent for Real_Sequence;
coherence
 for b1 being Real_Sequence st b1 = Re c holds
b1 is convergent by Th41;
cluster Im c ->  convergent for Real_Sequence;
coherence
 for b1 being Real_Sequence st b1 = Im c holds
b1 is convergent by Th41;
end;

theorem Th42: :: COMSEQ_3:42
for c being Complex_Sequence st Re c is convergent &amp; Im c is convergent holds
( c is convergent &amp; Re (lim c) = lim (Re c) &amp; Im (lim c) = lim (Im c) )
proofend;

theorem Th43: :: COMSEQ_3:43
for seq being Complex_Sequence
for z being Element of COMPLEX st 0 < |.z.| &amp; |.z.| < 1 &amp; seq . 0 = z &amp; ( for n being Element of NAT holds seq . (n + 1) = (seq . n) * z ) holds
( seq is convergent &amp; lim seq = 0c )
proofend;

theorem Th44: :: COMSEQ_3:44
for seq being Complex_Sequence
for z being Element of COMPLEX st |.z.| < 1 &amp; ( for n being Element of NAT holds seq . n = z #N (n + 1) ) holds
( seq is convergent &amp; lim seq = 0c )
proofend;

theorem :: COMSEQ_3:45
for seq being Complex_Sequence
for r being Real st r > 0 &amp; ex m being Element of NAT st
for n being Element of NAT st n >= m holds
|.(seq . n).| >= r &amp; |.seq.| is convergent holds
lim |.seq.| <> 0
proofend;

theorem Th46: :: COMSEQ_3:46
for seq being Complex_Sequence holds
( seq is convergent iff for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq . m) - (seq . n)).| < p )
proofend;

theorem :: COMSEQ_3:47
for seq being Complex_Sequence st seq is convergent holds
for p being Real st 0 < p holds
ex n being Element of NAT st
for m, l being Element of NAT st n <= m &amp; n <= l holds
|.((seq . m) - (seq . l)).| < p
proofend;

theorem :: COMSEQ_3:48
for rseq being Real_Sequence
for seq being Complex_Sequence st ( for n being Element of NAT holds |.(seq . n).| <= rseq . n ) &amp; rseq is convergent &amp; lim rseq = 0 holds
( seq is convergent &amp; lim seq = 0c )
proofend;

begin

theorem :: COMSEQ_3:49
for seq, seq1 being Complex_Sequence st seq is subsequence of seq1 holds
( Re seq is subsequence of Re seq1 &amp; Im seq is subsequence of Im seq1 )
proofend;

theorem :: COMSEQ_3:50
for seq being Complex_Sequence st seq is bounded holds
ex seq1 being Complex_Sequence st
( seq1 is subsequence of seq &amp; seq1 is convergent )
proofend;

definition
let seq be Complex_Sequence;
attrseq is summable  means :Def8: :: COMSEQ_3:def 8
 Partial_Sums seq is convergent ;
end;

:: deftheorem Def8 defines summable COMSEQ_3:def_8_:_
 for seq being Complex_Sequence holds
( seq is summable iff Partial_Sums seq is convergent );

set D = NAT --> 0c;

registration
cluster Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued summable for Element of K19(K20(NAT,COMPLEX));
existence
 ex b1 being Complex_Sequence st b1 is summable
proofend;
end;

registration
let seq be summable Complex_Sequence;
cluster Partial_Sums seq ->  convergent for Complex_Sequence;
coherence
 for b1 being Complex_Sequence st b1 = Partial_Sums seq holds
b1 is convergent by Def8;
end;

definition
let seq be Complex_Sequence;
attrseq is absolutely_summable  means :Def9: :: COMSEQ_3:def 9
|.seq.| is summable ;
end;

:: deftheorem Def9 defines absolutely_summable COMSEQ_3:def_9_:_
 for seq being Complex_Sequence holds
( seq is absolutely_summable iff |.seq.| is summable );

theorem Th51: :: COMSEQ_3:51
for seq being Complex_Sequence st ( for n being Element of NAT holds seq . n = 0c ) holds
seq is absolutely_summable
proofend;

registration
cluster Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued absolutely_summable for Element of K19(K20(NAT,COMPLEX));
existence
 ex b1 being Complex_Sequence st b1 is absolutely_summable
proofend;
end;

registration
let seq be absolutely_summable Complex_Sequence;
cluster|.seq.| ->  summable for Real_Sequence;
coherence
 for b1 being Real_Sequence st b1 = |.seq.| holds
b1 is summable by Def9;
end;

theorem Th52: :: COMSEQ_3:52
for seq being Complex_Sequence st seq is summable holds
( seq is convergent &amp; lim seq = 0c )
proofend;

registration
cluster Function-like V18( NAT , COMPLEX ) summable  ->  convergent for Element of K19(K20(NAT,COMPLEX));
coherence
 for b1 being Complex_Sequence st b1 is summable holds
b1 is convergent by Th52;
end;

theorem Th53: :: COMSEQ_3:53
for seq being Complex_Sequence st seq is summable holds
( Re seq is summable &amp; Im seq is summable &amp; Sum seq = (Sum (Re seq)) + ((Sum (Im seq)) * <i>) )
proofend;

registration
let seq be summable Complex_Sequence;
cluster Re seq ->  summable for Real_Sequence;
coherence
 for b1 being Real_Sequence st b1 = Re seq holds
b1 is summable by Th53;
cluster Im seq ->  summable for Real_Sequence;
coherence
 for b1 being Real_Sequence st b1 = Im seq holds
b1 is summable by Th53;
end;

theorem Th54: :: COMSEQ_3:54
for seq1, seq2 being Complex_Sequence st seq1 is summable &amp; seq2 is summable holds
( seq1 + seq2 is summable &amp; Sum (seq1 + seq2) = (Sum seq1) + (Sum seq2) )
proofend;

theorem Th55: :: COMSEQ_3:55
for seq1, seq2 being Complex_Sequence st seq1 is summable &amp; seq2 is summable holds
( seq1 - seq2 is summable &amp; Sum (seq1 - seq2) = (Sum seq1) - (Sum seq2) )
proofend;

registration
let seq1, seq2 be summable Complex_Sequence;
clusterseq1 + seq2 ->  summable for Complex_Sequence;
coherence
 for b1 being Complex_Sequence st b1 = seq1 + seq2 holds
b1 is summable by Th54;
clusterseq1 - seq2 ->  summable for Complex_Sequence;
coherence
 for b1 being Complex_Sequence st b1 = seq1 - seq2 holds
b1 is summable by Th55;
end;

theorem Th56: :: COMSEQ_3:56
for seq being Complex_Sequence st seq is summable holds
for z being complex number holds
( z (#) seq is summable &amp; Sum (z (#) seq) = z * (Sum seq) )
proofend;

registration
let z be Element of COMPLEX ;
let seq be summable Complex_Sequence;
clusterz (#) seq ->  summable for Complex_Sequence;
coherence
 for b1 being Complex_Sequence st b1 = z (#) seq holds
b1 is summable by Th56;
end;

theorem Th57: :: COMSEQ_3:57
for seq being Complex_Sequence st Re seq is summable &amp; Im seq is summable holds
( seq is summable &amp; Sum seq = (Sum (Re seq)) + ((Sum (Im seq)) * <i>) )
proofend;

theorem Th58: :: COMSEQ_3:58
for seq being Complex_Sequence st seq is summable holds
for n being Element of NAT holds seq ^\ n is summable
proofend;

registration
let seq be summable Complex_Sequence;
let n be Element of NAT ;
clusterseq ^\ n ->  summable for Complex_Sequence;
coherence
 for b1 being Complex_Sequence st b1 = seq ^\ n holds
b1 is summable by Th58;
end;

theorem :: COMSEQ_3:59
for seq being Complex_Sequence st ex n being Element of NAT st seq ^\ n is summable holds
seq is summable
proofend;

theorem :: COMSEQ_3:60
for seq being Complex_Sequence st seq is summable holds
for n being Element of NAT holds Sum seq = ((Partial_Sums seq) . n) + (Sum (seq ^\ (n + 1)))
proofend;

theorem Th61: :: COMSEQ_3:61
for seq being Complex_Sequence holds
( Partial_Sums |.seq.| is bounded_above iff seq is absolutely_summable )
proofend;

registration
let seq be absolutely_summable Complex_Sequence;
cluster Partial_Sums |.seq.| ->  bounded_above for Real_Sequence;
coherence
 for b1 being Real_Sequence st b1 = Partial_Sums |.seq.| holds
b1 is bounded_above by Th61;
end;

theorem Th62: :: COMSEQ_3:62
for seq being Complex_Sequence holds
( seq is summable iff for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| < p )
proofend;

theorem Th63: :: COMSEQ_3:63
for seq being Complex_Sequence st seq is absolutely_summable holds
seq is summable
proofend;

registration
cluster Function-like V18( NAT , COMPLEX ) absolutely_summable  ->  summable for Element of K19(K20(NAT,COMPLEX));
coherence
 for b1 being Complex_Sequence st b1 is absolutely_summable holds
b1 is summable by Th63;
end;

registration
cluster Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued absolutely_summable for Element of K19(K20(NAT,COMPLEX));
existence
 ex b1 being Complex_Sequence st b1 is absolutely_summable
proofend;
end;

theorem Th64: :: COMSEQ_3:64
for z being Element of COMPLEX st |.z.| < 1 holds
( z GeoSeq is summable &amp; Sum (z GeoSeq) = 1r / (1r - z) )
proofend;

theorem :: COMSEQ_3:65
for seq being Complex_Sequence
for z being Element of COMPLEX st |.z.| < 1 &amp; ( for n being Element of NAT holds seq . (n + 1) = z * (seq . n) ) holds
( seq is summable &amp; Sum seq = (seq . 0) / (1r - z) )
proofend;

theorem :: COMSEQ_3:66
for rseq1 being Real_Sequence
for seq2 being Complex_Sequence st rseq1 is summable &amp; ex m being Element of NAT st
for n being Element of NAT st m <= n holds
|.(seq2 . n).| <= rseq1 . n holds
seq2 is absolutely_summable
proofend;

theorem :: COMSEQ_3:67
for seq1, seq2 being Complex_Sequence st ( for n being Element of NAT holds
( 0 <= |.seq1.| . n &amp; |.seq1.| . n <= |.seq2.| . n ) ) &amp; seq2 is absolutely_summable holds
( seq1 is absolutely_summable &amp; Sum |.seq1.| <= Sum |.seq2.| )
proofend;

theorem :: COMSEQ_3:68
for seq being Complex_Sequence st ( for n being Element of NAT holds |.seq.| . n > 0 ) &amp; ex m being Element of NAT st
for n being Element of NAT st n >= m holds
(|.seq.| . (n + 1)) / (|.seq.| . n) >= 1 holds
not seq is absolutely_summable by SERIES_1:27;

theorem :: COMSEQ_3:69
for rseq1 being Real_Sequence
for seq being Complex_Sequence st ( for n being Element of NAT holds rseq1 . n = n -root (|.seq.| . n) ) &amp; rseq1 is convergent &amp; lim rseq1 < 1 holds
seq is absolutely_summable
proofend;

theorem :: COMSEQ_3:70
for rseq1 being Real_Sequence
for seq being Complex_Sequence st ( for n being Element of NAT holds rseq1 . n = n -root (|.seq.| . n) ) &amp; ex m being Element of NAT st
for n being Element of NAT st m <= n holds
rseq1 . n >= 1 holds
not |.seq.| is summable
proofend;

theorem :: COMSEQ_3:71
for rseq1 being Real_Sequence
for seq being Complex_Sequence st ( for n being Element of NAT holds rseq1 . n = n -root (|.seq.| . n) ) &amp; rseq1 is convergent &amp; lim rseq1 > 1 holds
not seq is absolutely_summable
proofend;

theorem :: COMSEQ_3:72
for rseq1 being Real_Sequence
for seq being Complex_Sequence st |.seq.| is non-increasing &amp; ( for n being Element of NAT holds rseq1 . n = (2 to_power n) * (|.seq.| . (2 to_power n)) ) holds
( seq is absolutely_summable iff rseq1 is summable )
proofend;

theorem :: COMSEQ_3:73
for seq being Complex_Sequence
for p being Real st p > 1 &amp; ( for n being Element of NAT st n >= 1 holds
|.seq.| . n = 1 / (n to_power p) ) holds
seq is absolutely_summable
proofend;

theorem :: COMSEQ_3:74
for seq being Complex_Sequence
for p being Real st p <= 1 &amp; ( for n being Element of NAT st n >= 1 holds
|.seq.| . n = 1 / (n to_power p) ) holds
not seq is absolutely_summable by SERIES_1:33;

theorem :: COMSEQ_3:75
for rseq1 being Real_Sequence
for seq being Complex_Sequence st ( for n being Element of NAT holds
( seq . n <> 0c &amp; rseq1 . n = (|.seq.| . (n + 1)) / (|.seq.| . n) ) ) &amp; rseq1 is convergent &amp; lim rseq1 < 1 holds
seq is absolutely_summable
proofend;

theorem :: COMSEQ_3:76
for seq being Complex_Sequence st ( for n being Element of NAT holds seq . n <> 0c ) &amp; ex m being Element of NAT st
for n being Element of NAT st n >= m holds
(|.seq.| . (n + 1)) / (|.seq.| . n) >= 1 holds
not seq is absolutely_summable
proofend;