:: by Yasunari Shidama and Artur Korni{\l}owicz

::

:: Received June 25, 1997

:: Copyright (c) 1997-2018 Association of Mizar Users

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

;

theorem Th2: :: COMSEQ_3:2

for rseq being Real_Sequence st ( for n being Nat holds rseq . n = 0 ) holds

for m being Nat holds (Partial_Sums (abs rseq)) . m = 0

for m being Nat holds (Partial_Sums (abs rseq)) . m = 0

proof end;

theorem Th3: :: COMSEQ_3:3

for rseq being Real_Sequence st ( for n being Nat holds rseq . n = 0 ) holds

rseq is absolutely_summable

rseq is absolutely_summable

proof end;

set C = seq_const 0;

Lm2: for n being Nat holds (seq_const 0) . n = 0

by SEQ_1:57;

registration

coherence

for b_{1} being Real_Sequence st b_{1} is summable holds

b_{1} is convergent
by SERIES_1:4;

end;
for b

b

registration
end;

registration

ex b_{1} being Real_Sequence st b_{1} is absolutely_summable
by Lm2, Th3;

end;

cluster Relation-like NAT -defined REAL -valued Function-like V11() total V18( NAT , REAL ) complex-valued ext-real-valued real-valued absolutely_summable for Real_Sequence;

existence ex b

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 Nat st

for m, l being Nat st n <= m & n <= l holds

|.((rseq . m) - (rseq . l)).| < p

for p being Real st 0 < p holds

ex n being Nat st

for m, l being Nat st n <= m & n <= l holds

|.((rseq . m) - (rseq . l)).| < p

proof end;

theorem :: COMSEQ_3:5

for rseq being Real_Sequence

for p being Real st ( for n being Nat holds rseq . n <= p ) holds

for n, l being Nat holds ((Partial_Sums rseq) . (n + l)) - ((Partial_Sums rseq) . n) <= p * l

for p being Real st ( for n being Nat holds rseq . n <= p ) holds

for n, l being Nat holds ((Partial_Sums rseq) . (n + l)) - ((Partial_Sums rseq) . n) <= p * l

proof end;

theorem :: COMSEQ_3:6

for rseq being Real_Sequence

for p being Real st ( for n being Nat holds rseq . n <= p ) holds

for n being Nat holds (Partial_Sums rseq) . n <= p * (n + 1)

for p being Real st ( for n being Nat holds rseq . n <= p ) holds

for n being Nat holds (Partial_Sums rseq) . n <= p * (n + 1)

proof end;

theorem :: COMSEQ_3:7

for rseq1, rseq2 being Real_Sequence

for m being Nat

for p being Real st ( for n being Nat st n <= m holds

rseq1 . n <= p * (rseq2 . n) ) holds

(Partial_Sums rseq1) . m <= p * ((Partial_Sums rseq2) . m)

for m being Nat

for p being Real st ( for n being Nat st n <= m holds

rseq1 . n <= p * (rseq2 . n) ) holds

(Partial_Sums rseq1) . m <= p * ((Partial_Sums rseq2) . m)

proof end;

theorem :: COMSEQ_3:8

for rseq1, rseq2 being Real_Sequence

for m being Nat

for p being Real st ( for n being Nat st n <= m holds

rseq1 . n <= p * (rseq2 . n) ) holds

for n, l being 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))

for m being Nat

for p being Real st ( for n being Nat st n <= m holds

rseq1 . n <= p * (rseq2 . n) ) holds

for n, l being 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))

proof end;

theorem :: COMSEQ_3:9

for rseq being Real_Sequence st ( for n being Nat holds 0 <= rseq . n ) holds

( ( for n, m being Nat st n <= m holds

|.(((Partial_Sums rseq) . m) - ((Partial_Sums rseq) . n)).| = ((Partial_Sums rseq) . m) - ((Partial_Sums rseq) . n) ) & ( for n being Nat holds |.((Partial_Sums rseq) . n).| = (Partial_Sums rseq) . n ) )

( ( for n, m being Nat st n <= m holds

|.(((Partial_Sums rseq) . m) - ((Partial_Sums rseq) . n)).| = ((Partial_Sums rseq) . m) - ((Partial_Sums rseq) . n) ) & ( for n being Nat holds |.((Partial_Sums rseq) . n).| = (Partial_Sums rseq) . n ) )

proof end;

theorem :: COMSEQ_3:10

for seq1, seq2 being Complex_Sequence st seq1 is convergent & seq2 is convergent & lim (seq1 - seq2) = 0c holds

lim seq1 = lim seq2

lim seq1 = lim seq2

proof end;

Lm3: for seq being Complex_Sequence

for n being Nat holds

( |.(seq . n).| = |.seq.| . n & 0 <= |.seq.| . n )

proof end;

definition

let z be Complex;

ex b_{1} being Complex_Sequence st

( b_{1} . 0 = 1r & ( for n being Nat holds b_{1} . (n + 1) = (b_{1} . n) * z ) )

for b_{1}, b_{2} being Complex_Sequence st b_{1} . 0 = 1r & ( for n being Nat holds b_{1} . (n + 1) = (b_{1} . n) * z ) & b_{2} . 0 = 1r & ( for n being Nat holds b_{2} . (n + 1) = (b_{2} . n) * z ) holds

b_{1} = b_{2}

end;
func z GeoSeq -> Complex_Sequence means :Def1: :: COMSEQ_3:def 1

( it . 0 = 1r & ( for n being Nat holds it . (n + 1) = (it . n) * z ) );

existence ( it . 0 = 1r & ( for n being Nat holds it . (n + 1) = (it . n) * z ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines GeoSeq COMSEQ_3:def 1 :

for z being Complex

for b_{2} being Complex_Sequence holds

( b_{2} = z GeoSeq iff ( b_{2} . 0 = 1r & ( for n being Nat holds b_{2} . (n + 1) = (b_{2} . n) * z ) ) );

for z being Complex

for b

( b

definition

let z be Complex;

let n be Nat;

coherence

z |^ n is Element of COMPLEX by XCMPLX_0:def 2;

compatibility

for b_{1} being Element of COMPLEX holds

( b_{1} = z |^ n iff b_{1} = (z GeoSeq) . n )

end;
let n be Nat;

coherence

z |^ n is Element of COMPLEX by XCMPLX_0:def 2;

compatibility

for b

( b

proof end;

:: deftheorem defines |^ COMSEQ_3:def 2 :

for z being Complex

for n being Nat holds z |^ n = (z GeoSeq) . n;

for z being Complex

for n being Nat holds z |^ n = (z GeoSeq) . n;

definition

let f be complex-valued Function;

set A = dom f;

deffunc H_{1}( object ) -> Element of REAL = Re (f . $1);

ex b_{1} being Function st

( dom b_{1} = dom f & ( for x being object st x in dom b_{1} holds

b_{1} . x = Re (f . x) ) )

for b_{1}, b_{2} being Function st dom b_{1} = dom f & ( for x being object st x in dom b_{1} holds

b_{1} . x = Re (f . x) ) & dom b_{2} = dom f & ( for x being object st x in dom b_{2} holds

b_{2} . x = Re (f . x) ) holds

b_{1} = b_{2}
_{2}( object ) -> Element of REAL = Im (f . $1);

ex b_{1} being Function st

( dom b_{1} = dom f & ( for x being object st x in dom b_{1} holds

b_{1} . x = Im (f . x) ) )

for b_{1}, b_{2} being Function st dom b_{1} = dom f & ( for x being object st x in dom b_{1} holds

b_{1} . x = Im (f . x) ) & dom b_{2} = dom f & ( for x being object st x in dom b_{2} holds

b_{2} . x = Im (f . x) ) holds

b_{1} = b_{2}

end;
set A = dom f;

deffunc H

func Re f -> Function means :Def3: :: COMSEQ_3:def 3

( dom it = dom f & ( for x being object st x in dom it holds

it . x = Re (f . x) ) );

existence ( dom it = dom f & ( for x being object st x in dom it holds

it . x = Re (f . x) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

deffunc H
func Im f -> Function means :Def4: :: COMSEQ_3:def 4

( dom it = dom f & ( for x being object st x in dom it holds

it . x = Im (f . x) ) );

existence ( dom it = dom f & ( for x being object st x in dom it holds

it . x = Im (f . x) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def3 defines Re COMSEQ_3:def 3 :

for f being complex-valued Function

for b_{2} being Function holds

( b_{2} = Re f iff ( dom b_{2} = dom f & ( for x being object st x in dom b_{2} holds

b_{2} . x = Re (f . x) ) ) );

for f being complex-valued Function

for b

( b

b

:: deftheorem Def4 defines Im COMSEQ_3:def 4 :

for f being complex-valued Function

for b_{2} being Function holds

( b_{2} = Im f iff ( dom b_{2} = dom f & ( for x being object st x in dom b_{2} holds

b_{2} . x = Im (f . x) ) ) );

for f being complex-valued Function

for b

( b

b

registration

let f be complex-valued Function;

coherence

Re f is real-valued

Im f is real-valued

end;
coherence

Re f is real-valued

proof end;

coherence Im f is real-valued

proof 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

redefine func Im f -> PartFunc of X,REAL;

coherence

Im f is PartFunc of X,REAL

end;
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

proof end;

:: original: Imredefine func Im f -> PartFunc of X,REAL;

coherence

Im f is PartFunc of X,REAL

proof end;

definition

let c be Complex_Sequence;

Re c is Real_Sequence

for b_{1} being Real_Sequence holds

( b_{1} = Re c iff for n being Nat holds b_{1} . n = Re (c . n) )

Im c is Real_Sequence

for b_{1} being Real_Sequence holds

( b_{1} = Im c iff for n being Nat holds b_{1} . n = Im (c . n) )

end;
:: original: Re

redefine func Re c -> Real_Sequence means :Def5: :: COMSEQ_3:def 5

for n being Nat holds it . n = Re (c . n);

coherence redefine func Re c -> Real_Sequence means :Def5: :: COMSEQ_3:def 5

for n being Nat holds it . n = Re (c . n);

Re c is Real_Sequence

proof end;

compatibility for b

( b

proof end;

:: original: Im

redefine func Im c -> Real_Sequence means :Def6: :: COMSEQ_3:def 6

for n being Nat holds it . n = Im (c . n);

coherence redefine func Im c -> Real_Sequence means :Def6: :: COMSEQ_3:def 6

for n being Nat holds it . n = Im (c . n);

Im c is Real_Sequence

proof end;

compatibility for b

( b

proof end;

:: deftheorem Def5 defines Re COMSEQ_3:def 5 :

for c being Complex_Sequence

for b_{2} being Real_Sequence holds

( b_{2} = Re c iff for n being Nat holds b_{2} . n = Re (c . n) );

for c being Complex_Sequence

for b

( b

:: deftheorem Def6 defines Im COMSEQ_3:def 6 :

for c being Complex_Sequence

for b_{2} being Real_Sequence holds

( b_{2} = Im c iff for n being Nat holds b_{2} . n = Im (c . n) );

for c being Complex_Sequence

for b

( b

theorem Th15: :: COMSEQ_3:15

for seq1, seq2 being Complex_Sequence holds

( (Re seq1) + (Re seq2) = Re (seq1 + seq2) & (Im seq1) + (Im seq2) = Im (seq1 + seq2) )

( (Re seq1) + (Re seq2) = Re (seq1 + seq2) & (Im seq1) + (Im seq2) = Im (seq1 + seq2) )

proof end;

theorem Th18: :: COMSEQ_3:18

for seq1, seq2 being Complex_Sequence holds

( (Re seq1) - (Re seq2) = Re (seq1 - seq2) & (Im seq1) - (Im seq2) = Im (seq1 - seq2) )

( (Re seq1) - (Re seq2) = Re (seq1 - seq2) & (Im seq1) - (Im seq2) = Im (seq1 - seq2) )

proof end;

theorem :: COMSEQ_3:19

for seq being Complex_Sequence

for r being Real holds

( r (#) (Re seq) = Re (r (#) seq) & r (#) (Im seq) = Im (r (#) seq) )

for r being Real holds

( r (#) (Re seq) = Re (r (#) seq) & r (#) (Im seq) = Im (r (#) seq) )

proof end;

theorem :: COMSEQ_3:20

for seq being Complex_Sequence

for z being Complex holds

( Re (z (#) seq) = ((Re z) (#) (Re seq)) - ((Im z) (#) (Im seq)) & Im (z (#) seq) = ((Re z) (#) (Im seq)) + ((Im z) (#) (Re seq)) )

for z being Complex holds

( Re (z (#) seq) = ((Re z) (#) (Re seq)) - ((Im z) (#) (Im seq)) & Im (z (#) seq) = ((Re z) (#) (Im seq)) + ((Im z) (#) (Re seq)) )

proof end;

theorem :: COMSEQ_3:21

for seq1, seq2 being Complex_Sequence holds

( Re (seq1 (#) seq2) = ((Re seq1) (#) (Re seq2)) - ((Im seq1) (#) (Im seq2)) & Im (seq1 (#) seq2) = ((Re seq1) (#) (Im seq2)) + ((Im seq1) (#) (Re seq2)) )

( Re (seq1 (#) seq2) = ((Re seq1) (#) (Re seq2)) - ((Im seq1) (#) (Im seq2)) & Im (seq1 (#) seq2) = ((Re seq1) (#) (Im seq2)) + ((Im seq1) (#) (Re seq2)) )

proof end;

definition

let Nseq be increasing sequence of NAT;

let seq be Complex_Sequence;

:: original: (#)

redefine func seq * Nseq -> Complex_Sequence;

coherence

Nseq (#) seq is Complex_Sequence

end;
let seq be Complex_Sequence;

:: original: (#)

redefine func seq * Nseq -> Complex_Sequence;

coherence

Nseq (#) seq is Complex_Sequence

proof 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 & Im (seq * Nseq) = (Im seq) * Nseq )

for Nseq being increasing sequence of NAT holds

( Re (seq * Nseq) = (Re seq) * Nseq & Im (seq * Nseq) = (Im seq) * Nseq )

proof end;

theorem Th23: :: COMSEQ_3:23

for seq being Complex_Sequence

for k being Nat holds

( (Re seq) ^\ k = Re (seq ^\ k) & (Im seq) ^\ k = Im (seq ^\ k) )

for k being Nat holds

( (Re seq) ^\ k = Re (seq ^\ k) & (Im seq) ^\ k = Im (seq ^\ k) )

proof end;

definition

let s be Complex_Sequence;

:: original: Partial_Sums

redefine func Partial_Sums s -> Complex_Sequence;

coherence

Partial_Sums s is Complex_Sequence

end;
:: original: Partial_Sums

redefine func Partial_Sums s -> Complex_Sequence;

coherence

Partial_Sums s is Complex_Sequence

proof end;

definition

let seq be Complex_Sequence;

coherence

lim (Partial_Sums seq) is Element of COMPLEX by XCMPLX_0:def 2;

end;
coherence

lim (Partial_Sums seq) is Element of COMPLEX by XCMPLX_0:def 2;

:: deftheorem defines Sum COMSEQ_3:def 7 :

for seq being Complex_Sequence holds Sum seq = lim (Partial_Sums seq);

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 Nat holds seq . n = 0c ) holds

for m being Nat holds (Partial_Sums seq) . m = 0c

for m being Nat holds (Partial_Sums seq) . m = 0c

proof end;

theorem Th25: :: COMSEQ_3:25

for seq being Complex_Sequence st ( for n being Nat holds seq . n = 0c ) holds

for m being Nat holds (Partial_Sums |.seq.|) . m = 0

for m being Nat holds (Partial_Sums |.seq.|) . m = 0

proof end;

theorem Th26: :: COMSEQ_3:26

for seq being Complex_Sequence holds

( Partial_Sums (Re seq) = Re (Partial_Sums seq) & Partial_Sums (Im seq) = Im (Partial_Sums seq) )

( Partial_Sums (Re seq) = Re (Partial_Sums seq) & Partial_Sums (Im seq) = Im (Partial_Sums seq) )

proof end;

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)

proof end;

theorem Th29: :: COMSEQ_3:29

for seq being Complex_Sequence

for z being Complex holds Partial_Sums (z (#) seq) = z (#) (Partial_Sums seq)

for z being Complex holds Partial_Sums (z (#) seq) = z (#) (Partial_Sums seq)

proof end;

theorem :: COMSEQ_3:30

for seq being Complex_Sequence

for k being Nat holds |.((Partial_Sums seq) . k).| <= (Partial_Sums |.seq.|) . k

for k being Nat holds |.((Partial_Sums seq) . k).| <= (Partial_Sums |.seq.|) . k

proof end;

theorem Th31: :: COMSEQ_3:31

for seq being Complex_Sequence

for n, m being Nat holds |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= |.(((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)).|

for n, m being Nat holds |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= |.(((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)).|

proof end;

theorem Th32: :: COMSEQ_3:32

for seq being Complex_Sequence

for k being Nat holds

( (Partial_Sums (Re seq)) ^\ k = Re ((Partial_Sums seq) ^\ k) & (Partial_Sums (Im seq)) ^\ k = Im ((Partial_Sums seq) ^\ k) )

for k being Nat holds

( (Partial_Sums (Re seq)) ^\ k = Re ((Partial_Sums seq) ^\ k) & (Partial_Sums (Im seq)) ^\ k = Im ((Partial_Sums seq) ^\ k) )

proof end;

theorem :: COMSEQ_3:33

for seq, seq1 being Complex_Sequence st ( for n being Nat holds seq1 . n = seq . 0 ) holds

Partial_Sums (seq ^\ 1) = ((Partial_Sums seq) ^\ 1) - seq1

Partial_Sums (seq ^\ 1) = ((Partial_Sums seq) ^\ 1) - seq1

proof end;

registration

let seq be Complex_Sequence;

coherence

for b_{1} being Real_Sequence st b_{1} = Partial_Sums |.seq.| holds

b_{1} is non-decreasing
by Th34;

end;
coherence

for b

b

theorem :: COMSEQ_3:35

for seq1, seq2 being Complex_Sequence

for m being Nat st ( for n being Nat st n <= m holds

seq1 . n = seq2 . n ) holds

(Partial_Sums seq1) . m = (Partial_Sums seq2) . m

for m being Nat st ( for n being Nat st n <= m holds

seq1 . n = seq2 . n ) holds

(Partial_Sums seq1) . m = (Partial_Sums seq2) . m

proof end;

theorem Th36: :: COMSEQ_3:36

for z being Complex st 1r <> z holds

for n being Nat holds (Partial_Sums (z GeoSeq)) . n = (1r - (z |^ (n + 1))) / (1r - z)

for n being Nat holds (Partial_Sums (z GeoSeq)) . n = (1r - (z |^ (n + 1))) / (1r - z)

proof end;

theorem Th37: :: COMSEQ_3:37

for seq being Complex_Sequence

for z being Complex st z <> 1r & ( for n being Nat holds seq . (n + 1) = z * (seq . n) ) holds

for n being Nat holds (Partial_Sums seq) . n = (seq . 0) * ((1r - (z |^ (n + 1))) / (1r - z))

for z being Complex st z <> 1r & ( for n being Nat holds seq . (n + 1) = z * (seq . n) ) holds

for n being Nat holds (Partial_Sums seq) . n = (seq . 0) * ((1r - (z |^ (n + 1))) / (1r - z))

proof end;

theorem Th38: :: COMSEQ_3:38

for a, b being Real_Sequence

for c being Complex_Sequence st ( for n being Nat holds

( Re (c . n) = a . n & Im (c . n) = b . n ) ) holds

( ( a is convergent & b is convergent ) iff c is convergent )

for c being Complex_Sequence st ( for n being Nat holds

( Re (c . n) = a . n & Im (c . n) = b . n ) ) holds

( ( a is convergent & b is convergent ) iff c is convergent )

proof end;

theorem Th39: :: COMSEQ_3:39

for a, b being convergent Real_Sequence

for c being Complex_Sequence st ( for n being Nat holds

( Re (c . n) = a . n & Im (c . n) = b . n ) ) holds

( c is convergent & lim c = (lim a) + ((lim b) * <i>) )

for c being Complex_Sequence st ( for n being Nat holds

( Re (c . n) = a . n & Im (c . n) = b . n ) ) holds

( c is convergent & lim c = (lim a) + ((lim b) * <i>) )

proof end;

theorem Th40: :: COMSEQ_3:40

for a, b being Real_Sequence

for c being convergent Complex_Sequence st ( for n being Nat holds

( Re (c . n) = a . n & Im (c . n) = b . n ) ) holds

( a is convergent & b is convergent & lim a = Re (lim c) & lim b = Im (lim c) )

for c being convergent Complex_Sequence st ( for n being Nat holds

( Re (c . n) = a . n & Im (c . n) = b . n ) ) holds

( a is convergent & b is convergent & lim a = Re (lim c) & lim b = Im (lim c) )

proof end;

theorem Th41: :: COMSEQ_3:41

for c being convergent Complex_Sequence holds

( Re c is convergent & Im c is convergent & lim (Re c) = Re (lim c) & lim (Im c) = Im (lim c) )

( Re c is convergent & Im c is convergent & lim (Re c) = Re (lim c) & lim (Im c) = Im (lim c) )

proof end;

registration

let c be convergent Complex_Sequence;

coherence

for b_{1} being Real_Sequence st b_{1} = Re c holds

b_{1} is convergent
by Th41;

coherence

for b_{1} being Real_Sequence st b_{1} = Im c holds

b_{1} is convergent
by Th41;

end;
coherence

for b

b

coherence

for b

b

theorem Th42: :: COMSEQ_3:42

for c being Complex_Sequence st Re c is convergent & Im c is convergent holds

( c is convergent & Re (lim c) = lim (Re c) & Im (lim c) = lim (Im c) )

( c is convergent & Re (lim c) = lim (Re c) & Im (lim c) = lim (Im c) )

proof end;

theorem Th43: :: COMSEQ_3:43

for seq being Complex_Sequence

for z being Complex st 0 < |.z.| & |.z.| < 1 & seq . 0 = z & ( for n being Nat holds seq . (n + 1) = (seq . n) * z ) holds

( seq is convergent & lim seq = 0c )

for z being Complex st 0 < |.z.| & |.z.| < 1 & seq . 0 = z & ( for n being Nat holds seq . (n + 1) = (seq . n) * z ) holds

( seq is convergent & lim seq = 0c )

proof end;

theorem Th44: :: COMSEQ_3:44

for seq being Complex_Sequence

for z being Complex st |.z.| < 1 & ( for n being Nat holds seq . n = z |^ (n + 1) ) holds

( seq is convergent & lim seq = 0c )

for z being Complex st |.z.| < 1 & ( for n being Nat holds seq . n = z |^ (n + 1) ) holds

( seq is convergent & lim seq = 0c )

proof end;

theorem :: COMSEQ_3:45

for seq being Complex_Sequence

for r being Real st r > 0 & ex m being Nat st

for n being Nat st n >= m holds

|.(seq . n).| >= r & |.seq.| is convergent holds

lim |.seq.| <> 0

for r being Real st r > 0 & ex m being Nat st

for n being Nat st n >= m holds

|.(seq . n).| >= r & |.seq.| is convergent holds

lim |.seq.| <> 0

proof end;

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 Nat st

for m being Nat st n <= m holds

|.((seq . m) - (seq . n)).| < p )

( seq is convergent iff for p being Real st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - (seq . n)).| < p )

proof end;

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 Nat st

for m, l being Nat st n <= m & n <= l holds

|.((seq . m) - (seq . l)).| < p

for p being Real st 0 < p holds

ex n being Nat st

for m, l being Nat st n <= m & n <= l holds

|.((seq . m) - (seq . l)).| < p

proof end;

theorem :: COMSEQ_3:48

for rseq being Real_Sequence

for seq being Complex_Sequence st ( for n being Nat holds |.(seq . n).| <= rseq . n ) & rseq is convergent & lim rseq = 0 holds

( seq is convergent & lim seq = 0c )

for seq being Complex_Sequence st ( for n being Nat holds |.(seq . n).| <= rseq . n ) & rseq is convergent & lim rseq = 0 holds

( seq is convergent & lim seq = 0c )

proof end;

theorem :: COMSEQ_3:49

for seq, seq1 being Complex_Sequence st seq is subsequence of seq1 holds

( Re seq is subsequence of Re seq1 & Im seq is subsequence of Im seq1 )

( Re seq is subsequence of Re seq1 & Im seq is subsequence of Im seq1 )

proof end;

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 & seq1 is convergent )

ex seq1 being Complex_Sequence st

( seq1 is subsequence of seq & seq1 is convergent )

proof end;

:: deftheorem Def8 defines summable COMSEQ_3:def 8 :

for seq being Complex_Sequence holds

( seq is summable iff Partial_Sums seq is convergent );

for seq being Complex_Sequence holds

( seq is summable iff Partial_Sums seq is convergent );

set D = NAT --> 0c;

registration

ex b_{1} being Complex_Sequence st b_{1} is summable
end;

cluster Relation-like NAT -defined COMPLEX -valued Function-like V11() total V18( NAT , COMPLEX ) complex-valued summable for Complex_Sequence;

existence ex b

proof end;

registration

let seq be summable Complex_Sequence;

coherence

for b_{1} being Complex_Sequence st b_{1} = Partial_Sums seq holds

b_{1} is convergent
by Def8;

end;
coherence

for b

b

:: deftheorem Def9 defines absolutely_summable COMSEQ_3:def 9 :

for seq being Complex_Sequence holds

( seq is absolutely_summable iff |.seq.| is summable );

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 Nat holds seq . n = 0c ) holds

seq is absolutely_summable

seq is absolutely_summable

proof end;

registration

ex b_{1} being Complex_Sequence st b_{1} is absolutely_summable
end;

cluster Relation-like NAT -defined COMPLEX -valued Function-like V11() total V18( NAT , COMPLEX ) complex-valued absolutely_summable for Complex_Sequence;

existence ex b

proof end;

registration

let seq be absolutely_summable Complex_Sequence;

coherence

for b_{1} being Real_Sequence st b_{1} = |.seq.| holds

b_{1} is summable
by Def9;

end;
coherence

for b

b

registration
end;

theorem Th53: :: COMSEQ_3:53

for seq being Complex_Sequence st seq is summable holds

( Re seq is summable & Im seq is summable & Sum seq = (Sum (Re seq)) + ((Sum (Im seq)) * <i>) )

( Re seq is summable & Im seq is summable & Sum seq = (Sum (Re seq)) + ((Sum (Im seq)) * <i>) )

proof end;

registration

let seq be summable Complex_Sequence;

coherence

for b_{1} being Real_Sequence st b_{1} = Re seq holds

b_{1} is summable
by Th53;

coherence

for b_{1} being Real_Sequence st b_{1} = Im seq holds

b_{1} is summable
by Th53;

end;
coherence

for b

b

coherence

for b

b

theorem Th54: :: COMSEQ_3:54

for seq1, seq2 being Complex_Sequence st seq1 is summable & seq2 is summable holds

( seq1 + seq2 is summable & Sum (seq1 + seq2) = (Sum seq1) + (Sum seq2) )

( seq1 + seq2 is summable & Sum (seq1 + seq2) = (Sum seq1) + (Sum seq2) )

proof end;

theorem Th55: :: COMSEQ_3:55

for seq1, seq2 being Complex_Sequence st seq1 is summable & seq2 is summable holds

( seq1 - seq2 is summable & Sum (seq1 - seq2) = (Sum seq1) - (Sum seq2) )

( seq1 - seq2 is summable & Sum (seq1 - seq2) = (Sum seq1) - (Sum seq2) )

proof end;

registration

let seq1, seq2 be summable Complex_Sequence;

coherence

for b_{1} being Complex_Sequence st b_{1} = seq1 + seq2 holds

b_{1} is summable
by Th54;

coherence

for b_{1} being Complex_Sequence st b_{1} = seq1 - seq2 holds

b_{1} is summable
by Th55;

end;
coherence

for b

b

coherence

for b

b

theorem Th56: :: COMSEQ_3:56

for seq being Complex_Sequence st seq is summable holds

for z being Complex holds

( z (#) seq is summable & Sum (z (#) seq) = z * (Sum seq) )

for z being Complex holds

( z (#) seq is summable & Sum (z (#) seq) = z * (Sum seq) )

proof end;

registration

let z be Element of COMPLEX ;

let seq be summable Complex_Sequence;

coherence

for b_{1} being Complex_Sequence st b_{1} = z (#) seq holds

b_{1} is summable
by Th56;

end;
let seq be summable Complex_Sequence;

coherence

for b

b

theorem Th57: :: COMSEQ_3:57

for seq being Complex_Sequence st Re seq is summable & Im seq is summable holds

( seq is summable & Sum seq = (Sum (Re seq)) + ((Sum (Im seq)) * <i>) )

( seq is summable & Sum seq = (Sum (Re seq)) + ((Sum (Im seq)) * <i>) )

proof end;

registration

let seq be summable Complex_Sequence;

let n be Nat;

coherence

for b_{1} being Complex_Sequence st b_{1} = seq ^\ n holds

b_{1} is summable
by Th58;

end;
let n be Nat;

coherence

for b

b

theorem :: COMSEQ_3:60

for seq being Complex_Sequence st seq is summable holds

for n being Nat holds Sum seq = ((Partial_Sums seq) . n) + (Sum (seq ^\ (n + 1)))

for n being Nat holds Sum seq = ((Partial_Sums seq) . n) + (Sum (seq ^\ (n + 1)))

proof end;

theorem Th61: :: COMSEQ_3:61

for seq being Complex_Sequence holds

( Partial_Sums |.seq.| is bounded_above iff seq is absolutely_summable )

( Partial_Sums |.seq.| is bounded_above iff seq is absolutely_summable )

proof end;

registration

let seq be absolutely_summable Complex_Sequence;

coherence

for b_{1} being Real_Sequence st b_{1} = Partial_Sums |.seq.| holds

b_{1} is bounded_above
by Th61;

end;
coherence

for b

b

registration

coherence

for b_{1} being Complex_Sequence st b_{1} is absolutely_summable holds

b_{1} is summable
by Th63;

end;
for b

b

registration

ex b_{1} being Complex_Sequence st b_{1} is absolutely_summable
end;

cluster Relation-like NAT -defined COMPLEX -valued Function-like V11() total V18( NAT , COMPLEX ) complex-valued absolutely_summable for Complex_Sequence;

existence ex b

proof end;

theorem :: COMSEQ_3:65

for seq being Complex_Sequence

for z being Complex st |.z.| < 1 & ( for n being Nat holds seq . (n + 1) = z * (seq . n) ) holds

( seq is summable & Sum seq = (seq . 0) / (1r - z) )

for z being Complex st |.z.| < 1 & ( for n being Nat holds seq . (n + 1) = z * (seq . n) ) holds

( seq is summable & Sum seq = (seq . 0) / (1r - z) )

proof end;

theorem :: COMSEQ_3:66

for rseq1 being Real_Sequence

for seq2 being Complex_Sequence st rseq1 is summable & ex m being Nat st

for n being Nat st m <= n holds

|.(seq2 . n).| <= rseq1 . n holds

seq2 is absolutely_summable

for seq2 being Complex_Sequence st rseq1 is summable & ex m being Nat st

for n being Nat st m <= n holds

|.(seq2 . n).| <= rseq1 . n holds

seq2 is absolutely_summable

proof end;

theorem :: COMSEQ_3:67

theorem :: COMSEQ_3:68

theorem :: COMSEQ_3:69

for rseq1 being Real_Sequence

for seq being Complex_Sequence st ( for n being Nat holds rseq1 . n = n -root (|.seq.| . n) ) & rseq1 is convergent & lim rseq1 < 1 holds

seq is absolutely_summable

for seq being Complex_Sequence st ( for n being Nat holds rseq1 . n = n -root (|.seq.| . n) ) & rseq1 is convergent & lim rseq1 < 1 holds

seq is absolutely_summable

proof end;

theorem :: COMSEQ_3:70

for rseq1 being Real_Sequence

for seq being Complex_Sequence st ( for n being Nat holds rseq1 . n = n -root (|.seq.| . n) ) & ex m being Nat st

for n being Nat st m <= n holds

rseq1 . n >= 1 holds

not |.seq.| is summable

for seq being Complex_Sequence st ( for n being Nat holds rseq1 . n = n -root (|.seq.| . n) ) & ex m being Nat st

for n being Nat st m <= n holds

rseq1 . n >= 1 holds

not |.seq.| is summable

proof end;

theorem :: COMSEQ_3:71

for rseq1 being Real_Sequence

for seq being Complex_Sequence st ( for n being Nat holds rseq1 . n = n -root (|.seq.| . n) ) & rseq1 is convergent & lim rseq1 > 1 holds

not seq is absolutely_summable

for seq being Complex_Sequence st ( for n being Nat holds rseq1 . n = n -root (|.seq.| . n) ) & rseq1 is convergent & lim rseq1 > 1 holds

not seq is absolutely_summable

proof end;

theorem :: COMSEQ_3:72

for rseq1 being Real_Sequence

for seq being Complex_Sequence st |.seq.| is non-increasing & ( for n being Nat holds rseq1 . n = (2 to_power n) * (|.seq.| . (2 to_power n)) ) holds

( seq is absolutely_summable iff rseq1 is summable )

for seq being Complex_Sequence st |.seq.| is non-increasing & ( for n being Nat holds rseq1 . n = (2 to_power n) * (|.seq.| . (2 to_power n)) ) holds

( seq is absolutely_summable iff rseq1 is summable )

proof end;

theorem :: COMSEQ_3:73

for seq being Complex_Sequence

for p being Real st p > 1 & ( for n being Nat st n >= 1 holds

|.seq.| . n = 1 / (n to_power p) ) holds

seq is absolutely_summable by SERIES_1:32;

for p being Real st p > 1 & ( for n being Nat st n >= 1 holds

|.seq.| . n = 1 / (n to_power p) ) holds

seq is absolutely_summable by SERIES_1:32;

theorem :: COMSEQ_3:74

for seq being Complex_Sequence

for p being Real st p <= 1 & ( for n being Nat st n >= 1 holds

|.seq.| . n = 1 / (n to_power p) ) holds

not seq is absolutely_summable by SERIES_1:33;

for p being Real st p <= 1 & ( for n being 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 Nat holds

( seq . n <> 0c & rseq1 . n = (|.seq.| . (n + 1)) / (|.seq.| . n) ) ) & rseq1 is convergent & lim rseq1 < 1 holds

seq is absolutely_summable

for seq being Complex_Sequence st ( for n being Nat holds

( seq . n <> 0c & rseq1 . n = (|.seq.| . (n + 1)) / (|.seq.| . n) ) ) & rseq1 is convergent & lim rseq1 < 1 holds

seq is absolutely_summable

proof end;

theorem :: COMSEQ_3:76

for seq being Complex_Sequence st ( for n being Nat holds seq . n <> 0c ) & ex m being Nat st

for n being Nat st n >= m holds

(|.seq.| . (n + 1)) / (|.seq.| . n) >= 1 holds

not seq is absolutely_summable

for n being Nat st n >= m holds

(|.seq.| . (n + 1)) / (|.seq.| . n) >= 1 holds

not seq is absolutely_summable

proof end;