comseq_3.miz

begin

 reserve rseq,rseq1,rseq2 for Real_Sequence;

 reserve seq,seq1,seq2 for Complex_Sequence;

 reserve k,n,n1,n2,m for Nat;

 reserve p,r for Real;



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

 theorem :: COMSEQ_3:1

 (n + 1) <> 0c & ((n + 1) * ) <> 0c ;

 theorem :: COMSEQ_3:2



 Th2: (for n holds (rseq . n) = 0 ) implies for m holds (( Partial_Sums ( abs rseq)) . m) = 0

 proof

 defpred P[ Nat] means (( abs rseq) . $1) = (( Partial_Sums ( abs rseq)) . $1);

 assume

 A1: for n holds (rseq . n) = 0 ;



 A2: for k st P[k] holds P[(k + 1)]

 proof

 let k be Nat such that

 A3: P[k];



 thus (( abs rseq) . (k + 1)) = ( 0 + (( abs rseq) . (k + 1)))

 .= ( |. 0 .| + (( abs rseq) . (k + 1))) by ABSVALUE:def 1

 .= ( |.(rseq . k).| + (( abs rseq) . (k + 1))) by A1

 .= ((( Partial_Sums ( abs rseq)) . k) + (( abs rseq) . (k + 1))) by A3, SEQ_1: 12

 .= (( Partial_Sums ( abs rseq)) . (k + 1)) by SERIES_1:def 1;

 end;

 let m;



 A4: P[ 0 ] by SERIES_1:def 1;

 for n holds P[n] from NAT_1:sch 2( A4, A2);



 hence (( Partial_Sums ( abs rseq)) . m) = (( abs rseq) . m)

 .= |.(rseq . m).| by SEQ_1: 12

 .= |. 0 .| by A1

 .= 0 by ABSVALUE:def 1;

 end;

 theorem :: COMSEQ_3:3



 Th3: (for n holds (rseq . n) = 0 ) implies rseq is absolutely_summable

 proof

 assume

 A1: for n holds (rseq . n) = 0 ;

 take 0 ;

 let p be Real such that

 A2: 0 < p;

 take 0 ;

 let m be Nat such that 0 <= m;

 |.((( Partial_Sums ( abs rseq)) . m) - 0 ).| = |.( 0 - 0 ).| by A1, Th2

 .= 0 by ABSVALUE:def 1;

 hence |.((( Partial_Sums ( abs rseq)) . m) - 0 ).| convergent for Real_Sequence;

 coherence by SERIES_1: 4;

 end

 registration

 cluster absolutely_summable -> summable for Real_Sequence;

 coherence ;

 end

 registration

 cluster absolutely_summable for Real_Sequence;

 existence by Lm2, Th3;

 end

 theorem :: COMSEQ_3:4

 rseq is convergent implies for p st 0 < p holds ex n st for m,l be Nat st n <= m & n <= l holds |.((rseq . m) - (rseq . l)).| < p

 proof

 assume

 A1: rseq is convergent;

 let p;

 assume 0 < p;

 then

 consider n such that

 A2: for m st n <= m holds |.((rseq . m) - (rseq . n)).| < (p / 2) by A1, SEQ_4: 41;

 take n;

 now

 let m,l be Nat;

 assume n <= m & n <= l;

 then |.((rseq . m) - (rseq . n)).| < (p / 2) & |.((rseq . l) - (rseq . n)).| < (p / 2) by A2;

 then

 A3: ( |.((rseq . m) - (rseq . n)).| + |.((rseq . l) - (rseq . n)).|) < ((p / 2) + (p / 2)) by XREAL_1: 8;

 |.((rseq . m) - (rseq . l)).| = |.(((rseq . m) - (rseq . n)) - ((rseq . l) - (rseq . n))).|;

 then |.((rseq . m) - (rseq . l)).| <= ( |.((rseq . m) - (rseq . n)).| + |.((rseq . l) - (rseq . n)).|) by COMPLEX1: 57;

 hence |.((rseq . m) - (rseq . l)).| < p by A3, XXREAL_0: 2;

 end;

 hence thesis;

 end;

 theorem :: COMSEQ_3:5

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

 proof

 assume

 A1: for n holds (rseq . n) <= p;

 let n;

 defpred P[ Nat] means ((( Partial_Sums rseq) . (n + $1)) - (( Partial_Sums rseq) . n)) <= (p * $1);

 A2:

 now

 let l be Nat such that

 A3: P[l];

 (rseq . ((n + l) + 1)) <= p by A1;

 then

 A4: ((p * l) + (rseq . ((n + l) + 1))) <= ((p * l) + p) by XREAL_1: 6;

 ((( Partial_Sums rseq) . (n + (l + 1))) - (( Partial_Sums rseq) . n)) = (((( Partial_Sums rseq) . (n + l)) + (rseq . ((n + l) + 1))) - (( Partial_Sums rseq) . n)) by SERIES_1:def 1

 .= (((( Partial_Sums rseq) . (n + l)) - (( Partial_Sums rseq) . n)) + (rseq . ((n + l) + 1)));

 then ((( Partial_Sums rseq) . (n + (l + 1))) - (( Partial_Sums rseq) . n)) <= ((p * l) + (rseq . ((n + l) + 1))) by A3, XREAL_1: 6;

 hence P[(l + 1)] by A4, XXREAL_0: 2;

 end;



 A5: P[ 0 ];

 thus for l be Nat holds P[l] from NAT_1:sch 2( A5, A2);

 end;

 theorem :: COMSEQ_3:6

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

 proof

 defpred P[ Nat] means (( Partial_Sums rseq) . $1) <= (p * ($1 + 1));

 assume

 A1: for n holds (rseq . n) <= p;

 A2:

 now

 let n be Nat such that

 A3: P[n];

 (rseq . (n + 1)) <= p by A1;

 then

 A4: ((p * (n + 1)) + (rseq . (n + 1))) <= ((p * (n + 1)) + p) by XREAL_1: 6;

 (( Partial_Sums rseq) . (n + 1)) = ((( Partial_Sums rseq) . n) + (rseq . (n + 1))) by SERIES_1:def 1;

 then (( Partial_Sums rseq) . (n + 1)) <= ((p * (n + 1)) + (rseq . (n + 1))) by A3, XREAL_1: 6;

 hence P[(n + 1)] by A4, XXREAL_0: 2;

 end;

 (( Partial_Sums rseq) . 0 ) = (rseq . 0 ) by SERIES_1:def 1;

 then

 A5: P[ 0 ] by A1;

 thus for n be Nat holds P[n] from NAT_1:sch 2( A5, A2);

 end;

 theorem :: COMSEQ_3:7

 (for n st n <= m holds (rseq1 . n) <= (p * (rseq2 . n))) implies (( Partial_Sums rseq1) . m) <= (p * (( Partial_Sums rseq2) . m))

 proof

 defpred P[ Nat] means $1 <= m implies (( Partial_Sums rseq1) . $1) <= (p * (( Partial_Sums rseq2) . $1));

 assume

 A1: for n st n <= m holds (rseq1 . n) <= (p * (rseq2 . n));

 A2:

 now

 let n be Nat such that

 A3: P[n];

 now

 assume

 A4: (n + 1) <= m;

 then (rseq1 . (n + 1)) <= (p * (rseq2 . (n + 1))) by A1;

 then

 A5: ((p * (( Partial_Sums rseq2) . n)) + (rseq1 . (n + 1))) <= ((p * (( Partial_Sums rseq2) . n)) + (p * (rseq2 . (n + 1)))) by XREAL_1: 6;

 n < (n + 1) & (( Partial_Sums rseq1) . (n + 1)) = ((( Partial_Sums rseq1) . n) + (rseq1 . (n + 1))) by SERIES_1:def 1, XREAL_1: 29;

 then

 A6: (( Partial_Sums rseq1) . (n + 1)) <= ((p * (( Partial_Sums rseq2) . n)) + (rseq1 . (n + 1))) by A3, A4, XREAL_1: 6, XXREAL_0: 2;

 ((p * (( Partial_Sums rseq2) . n)) + (p * (rseq2 . (n + 1)))) = (p * ((( Partial_Sums rseq2) . n) + (rseq2 . (n + 1))))

 .= (p * (( Partial_Sums rseq2) . (n + 1))) by SERIES_1:def 1;

 hence (( Partial_Sums rseq1) . (n + 1)) <= (p * (( Partial_Sums rseq2) . (n + 1))) by A6, A5, XXREAL_0: 2;

 end;

 hence P[(n + 1)];

 end;



 A7: P[ 0 ]

 proof

 assume 0 <= m;

 (( Partial_Sums rseq1) . 0 ) = (rseq1 . 0 ) & (p * (( Partial_Sums rseq2) . 0 )) = (p * (rseq2 . 0 )) by SERIES_1:def 1;

 hence thesis by A1;

 end;

 for n be Nat holds P[n] from NAT_1:sch 2( A7, A2);

 hence thesis;

 end;

 theorem :: COMSEQ_3:8

 (for n st n <= m holds (rseq1 . n) <= (p * (rseq2 . n))) implies for n holds for l be 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

 assume

 A1: for n st n <= m holds (rseq1 . n) <= (p * (rseq2 . n));

 let n;

 defpred P[ Nat] means (n + $1) <= m implies ((( Partial_Sums rseq1) . (n + $1)) - (( Partial_Sums rseq1) . n)) <= (p * ((( Partial_Sums rseq2) . (n + $1)) - (( Partial_Sums rseq2) . n)));



 A2: for l be Nat st P[l] holds P[(l + 1)]

 proof

 let l be Nat such that

 A3: P[l];

 assume

 A4: (n + (l + 1)) <= m;

 then (( Partial_Sums rseq1) . (n + (l + 1))) = ((( Partial_Sums rseq1) . (n + l)) + (rseq1 . ((n + l) + 1))) & (rseq1 . ((n + l) + 1)) <= (p * (rseq2 . ((n + l) + 1))) by A1, SERIES_1:def 1;

 then (( Partial_Sums rseq1) . (n + (l + 1))) <= ((( Partial_Sums rseq1) . (n + l)) + (p * (rseq2 . ((n + l) + 1)))) by XREAL_1: 6;

 then

 A5: ((( Partial_Sums rseq1) . (n + (l + 1))) - (( Partial_Sums rseq1) . n)) <= (((( Partial_Sums rseq1) . (n + l)) + (p * (rseq2 . ((n + l) + 1)))) - (( Partial_Sums rseq1) . n)) by XREAL_1: 9;

 (n + l) < ((n + l) + 1) by XREAL_1: 29;

 then

 A6: (((( Partial_Sums rseq1) . (n + l)) - (( Partial_Sums rseq1) . n)) + (p * (rseq2 . ((n + l) + 1)))) <= ((p * ((( Partial_Sums rseq2) . (n + l)) - (( Partial_Sums rseq2) . n))) + (p * (rseq2 . ((n + l) + 1)))) by A3, A4, XREAL_1: 6, XXREAL_0: 2;

 ((p * ((( Partial_Sums rseq2) . (n + l)) - (( Partial_Sums rseq2) . n))) + (p * (rseq2 . ((n + l) + 1)))) = (p * (((( Partial_Sums rseq2) . (n + l)) + (rseq2 . ((n + l) + 1))) - (( Partial_Sums rseq2) . n)))

 .= (p * ((( Partial_Sums rseq2) . (n + (l + 1))) - (( Partial_Sums rseq2) . n))) by SERIES_1:def 1;

 hence thesis by A5, A6, XXREAL_0: 2;

 end;



 A7: P[ 0 ];

 thus for l be Nat holds P[l] from NAT_1:sch 2( A7, A2);

 end;

 theorem :: COMSEQ_3:9

 (for n holds 0 <= (rseq . n)) implies (for n, m st n <= m holds |.((( Partial_Sums rseq) . m) - (( Partial_Sums rseq) . n)).| = ((( Partial_Sums rseq) . m) - (( Partial_Sums rseq) . n))) & for n holds |.(( Partial_Sums rseq) . n).| = (( Partial_Sums rseq) . n)

 proof

 assume

 A1: for n holds 0 <= (rseq . n);

 then

 A2: ( Partial_Sums rseq) is non-decreasing by SERIES_1: 16;

 A3:

 now

 let n, m;

 assume n <= m;

 then (( Partial_Sums rseq) . n) <= (( Partial_Sums rseq) . m) by A2, SEQM_3: 6;

 then ((( Partial_Sums rseq) . n) - (( Partial_Sums rseq) . n)) <= ((( Partial_Sums rseq) . m) - (( Partial_Sums rseq) . n)) by XREAL_1: 9;

 hence |.((( Partial_Sums rseq) . m) - (( Partial_Sums rseq) . n)).| = ((( Partial_Sums rseq) . m) - (( Partial_Sums rseq) . n)) by ABSVALUE:def 1;

 end;

 now

 let n;



 A4: (( Partial_Sums rseq) . 0 ) <= (( Partial_Sums rseq) . n) by A2, SEQM_3: 6;

 (( Partial_Sums rseq) . 0 ) = (rseq . 0 ) & 0 <= (rseq . 0 ) by A1, SERIES_1:def 1;

 hence |.(( Partial_Sums rseq) . n).| = (( Partial_Sums rseq) . n) by A4, ABSVALUE:def 1;

 end;

 hence thesis by A3;

 end;

 theorem :: COMSEQ_3:10

 seq1 is convergent & seq2 is convergent & ( lim (seq1 - seq2)) = 0c implies ( lim seq1) = ( lim seq2)

 proof

 assume that

 A1: seq1 is convergent & seq2 is convergent and

 A2: ( lim (seq1 - seq2)) = 0c ;

 ( lim (seq1 - seq2)) = (( lim seq1) - ( lim seq2)) by A1, COMSEQ_2: 26;

 hence thesis by A2;

 end;

 begin

 reserve z for Complex;

 reserve Nseq,Nseq1 for increasing sequence of NAT ;



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

 proof

 |.(seq . n).| = ( |.seq.| . n) by VALUED_1: 18;

 hence thesis by COMPLEX1: 46;

 end;

 definition

 let z be Complex;

 :: COMSEQ_3:def1

 func z GeoSeq -> Complex_Sequence means

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

 existence

 proof

 reconsider z9 = z as Element of COMPLEX by XCMPLX_0:def 2;

 deffunc f( set, Element of COMPLEX ) = ( In (($2 * z9), COMPLEX ));

 consider f be sequence of COMPLEX such that

 A1: (f . 0 ) = 1r & for n be Nat holds (f . (n + 1)) = f(n,.) from NAT_1:sch 12;

 take f;

 thus (f . 0 ) = 1r by A1;

 let n;

 (f . (n + 1)) = f(n,.) by A1;

 hence thesis;

 end;

 uniqueness

 proof

 let seq1, seq2;

 assume that

 A2: (seq1 . 0 ) = 1r and

 A3: for n holds (seq1 . (n + 1)) = ((seq1 . n) * z) and

 A4: (seq2 . 0 ) = 1r and

 A5: for n holds (seq2 . (n + 1)) = ((seq2 . n) * z);

 defpred P[ Nat] means (seq1 . $1) = (seq2 . $1);



 A6: for k be Nat st P[k] holds P[(k + 1)]

 proof

 let k be Nat;

 assume P[k];



 hence (seq1 . (k + 1)) = ((seq2 . k) * z) by A3

 .= (seq2 . (k + 1)) by A5;

 end;



 A7: P[ 0 ] by A2, A4;

 for n be Nat holds P[n] from NAT_1:sch 2( A7, A6);

 hence seq1 = seq2;

 end;

 end

 definition

 let z be Complex, n be Nat;

 :: original: |^

 redefine

 :: COMSEQ_3:def2

 func z |^ n -> Element of COMPLEX equals ((z GeoSeq ) . n);

 coherence by XCMPLX_0:def 2;

 compatibility

 proof

 reconsider n as Element of NAT by ORDINAL1:def 12;

 defpred P[ Nat] means (z |^ $1) = ((z GeoSeq ) . $1);

 let w be Element of COMPLEX ;



 A1: for n be Nat st P[n] holds P[(n + 1)]

 proof

 let n be Nat;

 assume P[n];



 hence (z |^ (n + 1)) = (((z GeoSeq ) . n) * z) by NEWTON: 6

 .= ((z GeoSeq ) . (n + 1)) by Def1;

 end;

 (z |^ 0 ) = 1r by COMPLEX1:def 4, NEWTON: 4

 .= ((z GeoSeq ) . 0 ) by Def1;

 then

 A2: P[ 0 ];

 for n be Nat holds P[n] from NAT_1:sch 2( A2, A1);

 then (z |^ n) = ((z GeoSeq ) . n);

 hence thesis;

 end;

 end

 theorem :: COMSEQ_3:11

 (z |^ 0 ) = 1r by COMPLEX1:def 4, NEWTON: 4;

 definition

 let f be complex-valued Function;

 set A = ( dom f);

 deffunc F( object) = ( Re (f . $1));

 :: COMSEQ_3:def3

 func Re f -> Function means

 : Def3: ( dom it ) = ( dom f) & for x be object st x in ( dom it ) holds (it . x) = ( Re (f . x));

 existence

 proof

 ex f be Function st ( dom f) = A & for x be object st x in A holds (f . x) = F(x) from FUNCT_1:sch 3;

 hence thesis;

 end;

 uniqueness

 proof

 let g,h be Function such that

 A1: ( dom g) = ( dom f) and

 A2: for x be object st x in ( dom g) holds (g . x) = F(x) and

 A3: ( dom h) = ( dom f) and

 A4: for x be object st x in ( dom h) holds (h . x) = F(x);

 now

 let x be object;

 assume

 A5: x in ( dom g);



 hence (g . x) = F(x) by A2

 .= (h . x) by A1, A3, A4, A5;

 end;

 hence thesis by A1, A3, FUNCT_1: 2;

 end;

 deffunc F( object) = ( Im (f . $1));

 :: COMSEQ_3:def4

 func Im f -> Function means

 : Def4: ( dom it ) = ( dom f) & for x be object st x in ( dom it ) holds (it . x) = ( Im (f . x));

 existence

 proof

 ex f be Function st ( dom f) = A & for x be object st x in A holds (f . x) = F(x) from FUNCT_1:sch 3;

 hence thesis;

 end;

 uniqueness

 proof

 let g,h be Function such that

 A6: ( dom g) = ( dom f) and

 A7: for x be object st x in ( dom g) holds (g . x) = F(x) and

 A8: ( dom h) = ( dom f) and

 A9: for x be object st x in ( dom h) holds (h . x) = F(x);

 now

 let x be object;

 assume

 A10: x in ( dom g);



 hence (g . x) = F(x) by A7

 .= (h . x) by A6, A8, A9, A10;

 end;

 hence thesis by A6, A8, FUNCT_1: 2;

 end;

 end

 registration

 let f be complex-valued Function;

 cluster ( Re f) -> real-valued;

 coherence

 proof

 let x be object;

 assume x in ( dom ( Re f));

 then (( Re f) . x) = ( Re (f . x)) by Def3;

 hence thesis;

 end;

 cluster ( Im f) -> real-valued;

 coherence

 proof

 let x be object;

 assume x in ( dom ( Im f));

 then (( Im f) . x) = ( Im (f . x)) by Def4;

 hence thesis;

 end;

 end

 definition

 let X be set, f be PartFunc of X, COMPLEX ;

 :: original: Re

 redefine

 func Re f -> PartFunc of X, REAL ;

 coherence

 proof



 A1: ( dom f) c= X by RELAT_1:def 18;



 A2: ( rng ( Re f)) c= REAL by VALUED_0:def 3;

 ( dom ( Re f)) = ( dom f) by Def3;

 hence thesis by A1, A2, RELSET_1: 4;

 end;

 :: original: Im

 redefine

 func Im f -> PartFunc of X, REAL ;

 coherence

 proof



 A3: ( dom f) c= X by RELAT_1:def 18;



 A4: ( rng ( Im f)) c= REAL by VALUED_0:def 3;

 ( dom ( Im f)) = ( dom f) by Def4;

 hence thesis by A3, A4, RELSET_1: 4;

 end;

 end

 definition

 let c be Complex_Sequence;

 :: original: Re

 redefine

 :: COMSEQ_3:def5

 func Re c -> Real_Sequence means

 : Def5: for n holds (it . n) = ( Re (c . n));

 coherence

 proof

 ( dom ( Re c)) = ( dom c) by Def3

 .= NAT by FUNCT_2:def 1;

 then ( Re c) is total by PARTFUN1:def 2;

 hence thesis;

 end;

 compatibility

 proof

 let f be Real_Sequence;



 A1: ( dom ( Re c)) = ( dom c) by Def3;



 A2: ( dom c) = NAT by FUNCT_2:def 1;



 A3: ( dom f) = NAT by FUNCT_2:def 1;

 thus f = ( Re c) implies for n holds (f . n) = ( Re (c . n)) by A1, A2, Def3, ORDINAL1:def 12;

 assume

 A4: for n holds (f . n) = ( Re (c . n));

 now

 let x be object;

 assume

 A5: x in ( dom f);



 hence (f . x) = ( Re (c . x)) by A4

 .= (( Re c) . x) by A1, A2, A3, A5, Def3;

 end;

 hence thesis by A1, A2, A3, FUNCT_1: 2;

 end;

 :: original: Im

 redefine

 :: COMSEQ_3:def6

 func Im c -> Real_Sequence means

 : Def6: for n holds (it . n) = ( Im (c . n));

 coherence

 proof

 ( dom ( Im c)) = ( dom c) by Def4

 .= NAT by FUNCT_2:def 1;

 then ( Im c) is total by PARTFUN1:def 2;

 hence thesis;

 end;

 compatibility

 proof

 let f be Real_Sequence;



 A6: ( dom ( Im c)) = ( dom c) by Def4;



 A7: ( dom c) = NAT by FUNCT_2:def 1;



 A8: ( dom f) = NAT by FUNCT_2:def 1;

 thus f = ( Im c) implies for n holds (f . n) = ( Im (c . n)) by A6, A7, ORDINAL1:def 12, Def4;

 assume

 A9: for n holds (f . n) = ( Im (c . n));

 now

 let x be object;

 assume

 A10: x in ( dom f);



 hence (f . x) = ( Im (c . x)) by A9

 .= (( Im c) . x) by A6, A7, A8, A10, Def4;

 end;

 hence thesis by A6, A7, A8, FUNCT_1: 2;

 end;

 end

 theorem :: COMSEQ_3:12



 Th12: |.z.| <= ( |.( Re z).| + |.( Im z).|)

 proof

 z = (( Re z) + (( Im z) * )) by COMPLEX1: 13;

 then

 A1: |.z.| <= ( |.(( Re z) + ( 0 * )).| + |.( 0 + (( Im z) * )).|) by COMPLEX1: 56;

 ( Re ( 0 + (( Im z) * ))) = 0 & ( Im ( 0 + (( Im z) * ))) = ( Im z) by COMPLEX1: 12;

 hence thesis by A1, COMPLEX1: 51;

 end;

 theorem :: COMSEQ_3:13



 Th13: |.( Re z).| <= |.z.| & |.( Im z).| <= |.z.|

 proof

 0 <= (( Re z) ^2 ) by XREAL_1: 63;

 then

 A1: ( 0 + (( Im z) ^2 )) <= ((( Re z) ^2 ) + (( Im z) ^2 )) by XREAL_1: 6;

 0 <= (( Im z) ^2 ) by XREAL_1: 63;

 then

 A2: ( sqrt (( Im z) ^2 )) <= ( sqrt ((( Re z) ^2 ) + (( Im z) ^2 ))) by A1, SQUARE_1: 26;

 0 <= (( Im z) ^2 ) by XREAL_1: 63;

 then

 A3: ( 0 + (( Re z) ^2 )) <= ((( Im z) ^2 ) + (( Re z) ^2 )) by XREAL_1: 6;

 0 <= (( Re z) ^2 ) by XREAL_1: 63;

 then |.z.| = ( sqrt ((( Re z) ^2 ) + (( Im z) ^2 ))) & ( sqrt (( Re z) ^2 )) <= ( sqrt ((( Re z) ^2 ) + (( Im z) ^2 ))) by A3, COMPLEX1:def 12, SQUARE_1: 26;

 hence thesis by A2, COMPLEX1: 72;

 end;

 theorem :: COMSEQ_3:14



 Th14: ( Re seq1) = ( Re seq2) & ( Im seq1) = ( Im seq2) implies seq1 = seq2

 proof

 assume that

 A1: ( Re seq1) = ( Re seq2) and

 A2: ( Im seq1) = ( Im seq2);

 now

 let n be Element of NAT ;



 A3: ( Im (seq1 . n)) = (( Im seq2) . n) by A2, Def6

 .= ( Im (seq2 . n)) by Def6;

 ( Re (seq1 . n)) = (( Re seq2) . n) by A1, Def5

 .= ( Re (seq2 . n)) by Def5;

 hence (seq1 . n) = (seq2 . n) by A3, COMPLEX1: 3;

 end;

 hence thesis;

 end;

 theorem :: COMSEQ_3:15



 Th15: (( Re seq1) + ( Re seq2)) = ( Re (seq1 + seq2)) & (( Im seq1) + ( Im seq2)) = ( Im (seq1 + seq2) qua Complex_Sequence)

 proof

 now

 let n be Element of NAT ;



 thus ((( Re seq1) + ( Re seq2)) . n) = ((( Re seq1) . n) + (( Re seq2) . n)) by SEQ_1: 7

 .= (( Re (seq1 . n)) + (( Re seq2) . n)) by Def5

 .= (( Re (seq1 . n)) + ( Re (seq2 . n))) by Def5

 .= ( Re ((seq1 . n) + (seq2 . n))) by COMPLEX1: 8

 .= ( Re ((seq1 + seq2) . n)) by VALUED_1: 1

 .= (( Re (seq1 + seq2)) . n) by Def5;

 end;

 hence (( Re seq1) + ( Re seq2)) = ( Re (seq1 + seq2));

 now

 let n be Element of NAT ;



 thus ((( Im seq1) + ( Im seq2)) . n) = ((( Im seq1) . n) + (( Im seq2) . n)) by SEQ_1: 7

 .= (( Im (seq1 . n)) + (( Im seq2) . n)) by Def6

 .= (( Im (seq1 . n)) + ( Im (seq2 . n))) by Def6

 .= ( Im ((seq1 . n) + (seq2 . n))) by COMPLEX1: 8

 .= ( Im ((seq1 + seq2) . n)) by VALUED_1: 1

 .= (( Im (seq1 + seq2)) . n) by Def6;

 end;

 hence thesis;

 end;

 theorem :: COMSEQ_3:16



 Th16: ( - ( Re seq)) = ( Re ( - seq)) & ( - ( Im seq)) = ( Im ( - seq))

 proof

 now

 let n be Element of NAT ;



 thus (( - ( Re seq)) . n) = ( - (( Re seq) . n)) by SEQ_1: 10

 .= ( - ( Re (seq . n))) by Def5

 .= ( Re ( - (seq . n))) by COMPLEX1: 17

 .= ( Re (( - seq) . n)) by VALUED_1: 8

 .= (( Re ( - seq)) . n) by Def5;

 end;

 hence ( - ( Re seq)) = ( Re ( - seq));

 now

 let n be Element of NAT ;



 thus (( - ( Im seq)) . n) = ( - (( Im seq) . n)) by SEQ_1: 10

 .= ( - ( Im (seq . n))) by Def6

 .= ( Im ( - (seq . n))) by COMPLEX1: 17

 .= ( Im (( - seq) . n)) by VALUED_1: 8

 .= (( Im ( - seq)) . n) by Def6;

 end;

 hence thesis;

 end;

 theorem :: COMSEQ_3:17



 Th17: (r * ( Re z)) = ( Re (r * z)) & (r * ( Im z)) = ( Im (r * z))

 proof

 reconsider r9 = r as Element of COMPLEX by XCMPLX_0:def 2;

 r = (r + ( 0 * ));

 then

 A1: ( Re r) = r & ( Im r) = 0 by COMPLEX1: 12;

 (r * z) = (((( Re r9) * ( Re z)) - (( Im r9) * ( Im z))) + (((( Re r9) * ( Im z)) + (( Re z) * ( Im r9))) * )) by COMPLEX1: 82

 .= ((r * ( Re z)) + ((r * ( Im z)) * )) by A1;

 hence thesis by COMPLEX1: 12;

 end;

 theorem :: COMSEQ_3:18



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

 proof

 now

 let n be Element of NAT ;



 thus ((( Re seq1) - ( Re seq2)) . n) = ((( Re seq1) . n) + (( - ( Re seq2)) . n)) by SEQ_1: 7

 .= ((( Re seq1) . n) + (( Re ( - seq2)) . n)) by Th16

 .= ((( Re seq1) + ( Re ( - seq2))) . n) by SEQ_1: 7

 .= (( Re (seq1 - seq2)) . n) by Th15;

 end;

 hence (( Re seq1) - ( Re seq2)) = ( Re (seq1 - seq2));

 now

 let n be Element of NAT ;



 thus ((( Im seq1) - ( Im seq2)) . n) = ((( Im seq1) . n) + (( - ( Im seq2)) . n)) by SEQ_1: 7

 .= ((( Im seq1) . n) + (( Im ( - seq2)) . n)) by Th16

 .= ((( Im seq1) + ( Im ( - seq2))) . n) by SEQ_1: 7

 .= (( Im (seq1 - seq2)) . n) by Th15;

 end;

 hence thesis;

 end;

 theorem :: COMSEQ_3:19

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

 proof

 now

 let n be Element of NAT ;



 thus ((r (#) ( Re seq)) . n) = (r * (( Re seq) . n)) by SEQ_1: 9

 .= (r * ( Re (seq . n))) by Def5

 .= ( Re (r * (seq . n))) by Th17

 .= ( Re ((r (#) seq) . n)) by VALUED_1: 6

 .= (( Re (r (#) seq)) . n) by Def5;

 end;

 hence (r (#) ( Re seq)) = ( Re (r (#) seq));

 now

 let n be Element of NAT ;



 thus ((r (#) ( Im seq)) . n) = (r * (( Im seq) . n)) by SEQ_1: 9

 .= (r * ( Im (seq . n))) by Def6

 .= ( Im (r * (seq . n))) by Th17

 .= ( Im ((r (#) seq) . n)) by VALUED_1: 6

 .= (( Im (r (#) seq)) . n) by Def6;

 end;

 hence thesis;

 end;

 theorem :: COMSEQ_3:20

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

 proof

 now

 let n be Element of NAT ;



 thus (( Re (z (#) seq)) . n) = ( Re ((z (#) seq) . n)) by Def5

 .= ( Re (z * (seq . n))) by VALUED_1: 6

 .= ( Re (((( Re z) * ( Re (seq . n))) - (( Im z) * ( Im (seq . n)))) + (((( Re z) * ( Im (seq . n))) + (( Re (seq . n)) * ( Im z))) * ))) by COMPLEX1: 82

 .= ((( Re z) * ( Re (seq . n))) - (( Im z) * ( Im (seq . n)))) by COMPLEX1: 12

 .= ((( Re z) * (( Re seq) . n)) - (( Im z) * ( Im (seq . n)))) by Def5

 .= ((( Re z) * (( Re seq) . n)) - (( Im z) * (( Im seq) . n))) by Def6

 .= (((( Re z) (#) ( Re seq)) . n) - (( Im z) * (( Im seq) . n))) by SEQ_1: 9

 .= (((( Re z) (#) ( Re seq)) . n) - ((( Im z) (#) ( Im seq)) . n)) by SEQ_1: 9

 .= (((( Re z) (#) ( Re seq)) . n) + ( - ((( Im z) (#) ( Im seq)) . n)))

 .= (((( Re z) (#) ( Re seq)) . n) + (( - (( Im z) (#) ( Im seq))) . n)) by SEQ_1: 10

 .= (((( Re z) (#) ( Re seq)) - (( Im z) (#) ( Im seq))) . n) by SEQ_1: 7;

 end;

 hence ( Re (z (#) seq)) = ((( Re z) (#) ( Re seq)) - (( Im z) (#) ( Im seq)));

 now

 let n be Element of NAT ;



 thus (( Im (z (#) seq)) . n) = ( Im ((z (#) seq) . n)) by Def6

 .= ( Im (z * (seq . n))) by VALUED_1: 6

 .= ( Im (((( Re z) * ( Re (seq . n))) - (( Im z) * ( Im (seq . n)))) + (((( Re z) * ( Im (seq . n))) + (( Re (seq . n)) * ( Im z))) * ))) by COMPLEX1: 82

 .= ((( Re z) * ( Im (seq . n))) + (( Re (seq . n)) * ( Im z))) by COMPLEX1: 12

 .= ((( Re z) * ( Im (seq . n))) + (( Im z) * (( Re seq) . n))) by Def5

 .= ((( Re z) * (( Im seq) . n)) + (( Im z) * (( Re seq) . n))) by Def6

 .= (((( Re z) (#) ( Im seq)) . n) + (( Im z) * (( Re seq) . n))) by SEQ_1: 9

 .= (((( Re z) (#) ( Im seq)) . n) + ((( Im z) (#) ( Re seq)) . n)) by SEQ_1: 9

 .= (((( Re z) (#) ( Im seq)) + (( Im z) (#) ( Re seq))) . n) by SEQ_1: 7;

 end;

 hence thesis;

 end;

 theorem :: COMSEQ_3:21

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

 proof

 now

 let n be Element of NAT ;



 thus (( Re (seq1 (#) seq2)) . n) = ( Re ((seq1 (#) seq2) . n)) by Def5

 .= ( Re ((seq1 . n) * (seq2 . n))) by VALUED_1: 5

 .= ( Re (((( Re (seq1 . n)) * ( Re (seq2 . n))) - (( Im (seq1 . n)) * ( Im (seq2 . n)))) + (((( Re (seq1 . n)) * ( Im (seq2 . n))) + (( Re (seq2 . n)) * ( Im (seq1 . n)))) * ))) by COMPLEX1: 82

 .= ((( Re (seq1 . n)) * ( Re (seq2 . n))) - (( Im (seq1 . n)) * ( Im (seq2 . n)))) by COMPLEX1: 12

 .= (((( Re seq1) . n) * ( Re (seq2 . n))) - (( Im (seq1 . n)) * ( Im (seq2 . n)))) by Def5

 .= (((( Re seq1) . n) * (( Re seq2) . n)) - (( Im (seq1 . n)) * ( Im (seq2 . n)))) by Def5

 .= (((( Re seq1) . n) * (( Re seq2) . n)) - (( Im (seq1 . n)) * (( Im seq2) . n))) by Def6

 .= (((( Re seq1) . n) * (( Re seq2) . n)) - ((( Im seq1) . n) * (( Im seq2) . n))) by Def6

 .= (((( Re seq1) (#) ( Re seq2)) . n) - ((( Im seq1) . n) * (( Im seq2) . n))) by SEQ_1: 8

 .= (((( Re seq1) (#) ( Re seq2)) . n) - ((( Im seq1) (#) ( Im seq2)) . n)) by SEQ_1: 8

 .= (((( Re seq1) (#) ( Re seq2)) . n) + ( - ((( Im seq1) (#) ( Im seq2)) . n)))

 .= (((( Re seq1) (#) ( Re seq2)) . n) + (( - (( Im seq1) (#) ( Im seq2))) . n)) by SEQ_1: 10

 .= (((( Re seq1) (#) ( Re seq2)) - (( Im seq1) (#) ( Im seq2))) . n) by SEQ_1: 7;

 end;

 hence ( Re (seq1 (#) seq2)) = ((( Re seq1) (#) ( Re seq2)) - (( Im seq1) (#) ( Im seq2)));

 now

 let n be Element of NAT ;



 thus (( Im (seq1 (#) seq2)) . n) = ( Im ((seq1 (#) seq2) . n)) by Def6

 .= ( Im ((seq1 . n) * (seq2 . n))) by VALUED_1: 5

 .= ( Im (((( Re (seq1 . n)) * ( Re (seq2 . n))) - (( Im (seq1 . n)) * ( Im (seq2 . n)))) + (((( Re (seq1 . n)) * ( Im (seq2 . n))) + (( Re (seq2 . n)) * ( Im (seq1 . n)))) * ))) by COMPLEX1: 82

 .= ((( Re (seq1 . n)) * ( Im (seq2 . n))) + (( Re (seq2 . n)) * ( Im (seq1 . n)))) by COMPLEX1: 12

 .= ((( Re (seq1 . n)) * ( Im (seq2 . n))) + (( Im (seq1 . n)) * (( Re seq2) . n))) by Def5

 .= (((( Re seq1) . n) * ( Im (seq2 . n))) + (( Im (seq1 . n)) * (( Re seq2) . n))) by Def5

 .= (((( Re seq1) . n) * (( Im seq2) . n)) + (( Im (seq1 . n)) * (( Re seq2) . n))) by Def6

 .= (((( Re seq1) . n) * (( Im seq2) . n)) + ((( Im seq1) . n) * (( Re seq2) . n))) by Def6

 .= (((( Re seq1) (#) ( Im seq2)) . n) + ((( Im seq1) . n) * (( Re seq2) . n))) by SEQ_1: 8

 .= (((( Re seq1) (#) ( Im seq2)) . n) + ((( Im seq1) (#) ( Re seq2)) . n)) by SEQ_1: 8

 .= (((( Re seq1) (#) ( Im seq2)) + (( Im seq1) (#) ( Re seq2))) . n) by SEQ_1: 7;

 end;

 hence thesis;

 end;

 definition

 let Nseq be increasing sequence of NAT , seq be Complex_Sequence;

 :: original: *

 redefine

 func seq * Nseq -> Complex_Sequence ;

 coherence

 proof

 ( dom (seq * Nseq)) = NAT by FUNCT_2:def 1;

 hence thesis;

 end;

 end

 theorem :: COMSEQ_3:22



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

 proof

 now

 let n be Element of NAT ;



 thus (( Re (seq * Nseq)) . n) = ( Re ((seq * Nseq) . n)) by Def5

 .= ( Re (seq . (Nseq . n))) by FUNCT_2: 15

 .= (( Re seq) . (Nseq . n)) by Def5

 .= ((( Re seq) * Nseq) . n) by FUNCT_2: 15;

 end;

 hence ( Re (seq * Nseq)) = (( Re seq) * Nseq);

 now

 let n be Element of NAT ;



 thus (( Im (seq * Nseq)) . n) = ( Im ((seq * Nseq) . n)) by Def6

 .= ( Im (seq . (Nseq . n))) by FUNCT_2: 15

 .= (( Im seq) . (Nseq . n)) by Def6

 .= ((( Im seq) * Nseq) . n) by FUNCT_2: 15;

 end;

 hence thesis;

 end;

 theorem :: COMSEQ_3:23



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

 proof

 now

 let n be Element of NAT ;



 thus ((( Re seq) ^\ k) . n) = (( Re seq) . (n + k)) by NAT_1:def 3

 .= ( Re (seq . (n + k))) by Def5

 .= ( Re ((seq ^\ k) . n)) by NAT_1:def 3

 .= (( Re (seq ^\ k)) . n) by Def5;



 thus ((( Im seq) ^\ k) . n) = (( Im seq) . (n + k)) by NAT_1:def 3

 .= ( Im (seq . (n + k))) by Def6

 .= ( Im ((seq ^\ k) . n)) by NAT_1:def 3

 .= (( Im (seq ^\ k)) . n) by Def6;

 end;

 hence thesis;

 end;

 definition

 let s be Complex_Sequence;

 :: original: Partial_Sums

 redefine

 func Partial_Sums s -> Complex_Sequence ;

 coherence

 proof



 A1: ( dom ( Partial_Sums s)) = NAT by PARTFUN1:def 2;

 ( rng ( Partial_Sums s)) c= COMPLEX by VALUED_0:def 1;

 then ( Partial_Sums s) is PartFunc of NAT , COMPLEX by A1, RELSET_1: 4;

 hence ( Partial_Sums s) is Complex_Sequence;

 end;

 end

 definition

 let seq be Complex_Sequence;

 :: COMSEQ_3:def7

 func Sum seq -> Element of COMPLEX equals ( lim ( Partial_Sums seq));

 coherence by XCMPLX_0:def 2;

 end

 theorem :: COMSEQ_3:24



 Th24: (for n holds (seq . n) = 0c ) implies for m holds (( Partial_Sums seq) . m) = 0c

 proof

 defpred P[ Nat] means (seq . $1) = (( Partial_Sums seq) . $1);

 assume

 A1: for n holds (seq . n) = 0c ;



 A2: for k be Nat st P[k] holds P[(k + 1)]

 proof

 let k be Nat such that

 A3: P[k];



 thus (seq . (k + 1)) = ( 0c + (seq . (k + 1)))

 .= ((( Partial_Sums seq) . k) + (seq . (k + 1))) by A1, A3

 .= (( Partial_Sums seq) . (k + 1)) by SERIES_1:def 1;

 end;

 let m;



 A4: P[ 0 ] by SERIES_1:def 1;

 for n be Nat holds P[n] from NAT_1:sch 2( A4, A2);

 then seq = ( Partial_Sums seq);

 hence thesis by A1;

 end;

 theorem :: COMSEQ_3:25



 Th25: (for n holds (seq . n) = 0c ) implies for m holds (( Partial_Sums |.seq.|) . m) = 0

 proof

 defpred P[ Nat] means ( |.seq.| . $1) = (( Partial_Sums |.seq.|) . $1);

 assume

 A1: for n holds (seq . n) = 0c ;



 A2: for k be Nat st P[k] holds P[(k + 1)]

 proof

 let k be Nat such that

 A3: P[k];



 thus ( |.seq.| . (k + 1)) = ( |. 0c .| + ( |.seq.| . (k + 1))) by COMPLEX1: 44

 .= ( |.(seq . k).| + ( |.seq.| . (k + 1))) by A1

 .= ((( Partial_Sums |.seq.|) . k) + ( |.seq.| . (k + 1))) by A3, VALUED_1: 18

 .= (( Partial_Sums |.seq.|) . (k + 1)) by SERIES_1:def 1;

 end;

 let m;



 A4: P[ 0 ] by SERIES_1:def 1;

 for n be Nat holds P[n] from NAT_1:sch 2( A4, A2);



 hence (( Partial_Sums |.seq.|) . m) = ( |.seq.| . m)

 .= |.(seq . m).| by VALUED_1: 18

 .= 0 by A1, COMPLEX1: 44;

 end;

 theorem :: COMSEQ_3:26



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

 proof

 defpred P[ Nat] means (( Partial_Sums ( Re seq)) . $1) = (( Re ( Partial_Sums seq)) . $1);

 defpred R[ Nat] means (( Partial_Sums ( Im seq)) . $1) = (( Im ( Partial_Sums seq)) . $1);



 A1: for k be Nat st P[k] holds P[(k + 1)]

 proof

 let k be Nat;

 assume P[k];



 then (( Partial_Sums ( Re seq)) . (k + 1)) = ((( Re ( Partial_Sums seq)) . k) + (( Re seq) . (k + 1))) by SERIES_1:def 1

 .= ((( Re ( Partial_Sums seq)) . k) + ( Re (seq . (k + 1)))) by Def5

 .= (( Re (( Partial_Sums seq) . k)) + ( Re (seq . (k + 1)))) by Def5

 .= ( Re ((( Partial_Sums seq) . k) + (seq . (k + 1)))) by COMPLEX1: 8

 .= ( Re (( Partial_Sums seq) . (k + 1))) by SERIES_1:def 1

 .= (( Re ( Partial_Sums seq)) . (k + 1)) by Def5;

 hence thesis;

 end;



 A2: for k be Nat st R[k] holds R[(k + 1)]

 proof

 let k be Nat;

 assume R[k];



 then (( Partial_Sums ( Im seq)) . (k + 1)) = ((( Im ( Partial_Sums seq)) . k) + (( Im seq) . (k + 1))) by SERIES_1:def 1

 .= ((( Im ( Partial_Sums seq)) . k) + ( Im (seq . (k + 1)))) by Def6

 .= (( Im (( Partial_Sums seq) . k)) + ( Im (seq . (k + 1)))) by Def6

 .= ( Im ((( Partial_Sums seq) . k) + (seq . (k + 1)))) by COMPLEX1: 8

 .= ( Im (( Partial_Sums seq) . (k + 1))) by SERIES_1:def 1

 .= (( Im ( Partial_Sums seq)) . (k + 1)) by Def6;

 hence thesis;

 end;

 (( Partial_Sums ( Im seq)) . 0 ) = (( Im seq) . 0 ) by SERIES_1:def 1

 .= ( Im (seq . 0 )) by Def6

 .= ( Im (( Partial_Sums seq) . 0 )) by SERIES_1:def 1

 .= (( Im ( Partial_Sums seq)) . 0 ) by Def6;

 then

 A3: R[ 0 ];



 A4: for n be Nat holds R[n] from NAT_1:sch 2( A3, A2);

 (( Partial_Sums ( Re seq)) . 0 ) = (( Re seq) . 0 ) by SERIES_1:def 1

 .= ( Re (seq . 0 )) by Def5

 .= ( Re (( Partial_Sums seq) . 0 )) by SERIES_1:def 1

 .= (( Re ( Partial_Sums seq)) . 0 ) by Def5;

 then

 A5: P[ 0 ];

 for n be Nat holds P[n] from NAT_1:sch 2( A5, A1);

 hence thesis by A4;

 end;

 theorem :: COMSEQ_3:27



 Th27: (( Partial_Sums seq1) + ( Partial_Sums seq2)) = ( Partial_Sums (seq1 + seq2)) by SERIES_1: 5;

 theorem :: COMSEQ_3:28



 Th28: (( Partial_Sums seq1) - ( Partial_Sums seq2)) = ( Partial_Sums (seq1 - seq2))

 proof



 A1: ( Im (( Partial_Sums seq1) - ( Partial_Sums seq2))) = (( Im ( Partial_Sums seq1)) - ( Im ( Partial_Sums seq2))) by Th18

 .= (( Partial_Sums ( Im seq1)) - ( Im ( Partial_Sums seq2))) by Th26

 .= (( Partial_Sums ( Im seq1)) - ( Partial_Sums ( Im seq2))) by Th26

 .= ( Partial_Sums (( Im seq1) - ( Im seq2))) by SERIES_1: 6

 .= ( Partial_Sums ( Im (seq1 - seq2))) by Th18

 .= ( Im ( Partial_Sums (seq1 - seq2))) by Th26;

 ( Re (( Partial_Sums seq1) - ( Partial_Sums seq2))) = (( Re ( Partial_Sums seq1)) - ( Re ( Partial_Sums seq2))) by Th18

 .= (( Partial_Sums ( Re seq1)) - ( Re ( Partial_Sums seq2))) by Th26

 .= (( Partial_Sums ( Re seq1)) - ( Partial_Sums ( Re seq2))) by Th26

 .= ( Partial_Sums (( Re seq1) - ( Re seq2))) by SERIES_1: 6

 .= ( Partial_Sums ( Re (seq1 - seq2))) by Th18

 .= ( Re ( Partial_Sums (seq1 - seq2))) by Th26;

 hence thesis by A1, Th14;

 end;

 theorem :: COMSEQ_3:29



 Th29: for z be Complex holds ( Partial_Sums (z (#) seq)) = (z (#) ( Partial_Sums seq))

 proof

 let z be Complex;

 defpred P[ Nat] means (( Partial_Sums (z (#) seq)) . $1) = ((z (#) ( Partial_Sums seq)) . $1);

 A1:

 now

 let n be Nat;

 assume

 A2: P[n];

 (( Partial_Sums (z (#) seq)) . (n + 1)) = ((( Partial_Sums (z (#) seq)) . n) + ((z (#) seq) . (n + 1))) by SERIES_1:def 1

 .= ((z * (( Partial_Sums seq) . n)) + ((z (#) seq) . (n + 1))) by A2, VALUED_1: 6

 .= ((z * (( Partial_Sums seq) . n)) + (z * (seq . (n + 1)))) by VALUED_1: 6

 .= (z * ((( Partial_Sums seq) . n) + (seq . (n + 1))))

 .= (z * (( Partial_Sums seq) . (n + 1))) by SERIES_1:def 1

 .= ((z (#) ( Partial_Sums seq)) . (n + 1)) by VALUED_1: 6;

 hence P[(n + 1)];

 end;

 (( Partial_Sums (z (#) seq)) . 0 ) = ((z (#) seq) . 0 ) by SERIES_1:def 1

 .= (z * (seq . 0 )) by VALUED_1: 6

 .= (z * (( Partial_Sums seq) . 0 )) by SERIES_1:def 1

 .= ((z (#) ( Partial_Sums seq)) . 0 ) by VALUED_1: 6;

 then

 A3: P[ 0 ];

 for n be Nat holds P[n] from NAT_1:sch 2( A3, A1);

 hence thesis;

 end;

 theorem :: COMSEQ_3:30

 |.(( Partial_Sums seq) . k).| <= (( Partial_Sums |.seq.|) . k)

 proof

 defpred P[ Nat] means |.(( Partial_Sums seq) . $1).| <= (( Partial_Sums |.seq.|) . $1);

 A1:

 now

 let k;

 assume P[k];

 then

 A2: ( |.(( Partial_Sums seq) . k).| + |.(seq . (k + 1)).|) <= ((( Partial_Sums |.seq.|) . k) + |.(seq . (k + 1)).|) by XREAL_1: 6;

 |.(( Partial_Sums seq) . (k + 1)).| = |.((( Partial_Sums seq) . k) + (seq . (k + 1))).| & |.((( Partial_Sums seq) . k) + (seq . (k + 1))).| <= ( |.(( Partial_Sums seq) . k).| + |.(seq . (k + 1)).|) by COMPLEX1: 56, SERIES_1:def 1;

 then |.(( Partial_Sums seq) . (k + 1)).| <= ((( Partial_Sums |.seq.|) . k) + |.(seq . (k + 1)).|) by A2, XXREAL_0: 2;

 then |.(( Partial_Sums seq) . (k + 1)).| <= ((( Partial_Sums |.seq.|) . k) + ( |.seq.| . (k + 1))) by VALUED_1: 18;

 hence P[(k + 1)] by SERIES_1:def 1;

 end;

 (( Partial_Sums |.seq.|) . 0 ) = ( |.seq.| . 0 ) by SERIES_1:def 1

 .= |.(seq . 0 ).| by VALUED_1: 18;

 then

 A3: P[ 0 ] by SERIES_1:def 1;

 for k be Nat holds P[k] from NAT_1:sch 2( A3, A1);

 hence thesis;

 end;

 theorem :: COMSEQ_3:31



 Th31: |.((( Partial_Sums seq) . m) - (( Partial_Sums seq) . n)).| <= |.((( Partial_Sums |.seq.|) . m) - (( Partial_Sums |.seq.|) . n)).|

 proof



 A1: for n,k be Nat holds 0 <= ((( Partial_Sums |.seq.|) . (n + k)) - (( Partial_Sums |.seq.|) . n))

 proof

 let n;

 defpred P[ Nat] means 0 <= ((( Partial_Sums |.seq.|) . (n + $1)) - (( Partial_Sums |.seq.|) . n));

 A2:

 now

 let k;



 A3: ((( Partial_Sums |.seq.|) . (n + (k + 1))) - (( Partial_Sums |.seq.|) . n)) = (((( Partial_Sums |.seq.|) . (n + k)) + ( |.seq.| . ((n + k) + 1))) - (( Partial_Sums |.seq.|) . n)) by SERIES_1:def 1

 .= (((( Partial_Sums |.seq.|) . (n + k)) + |.(seq . ((n + k) + 1)).|) - (( Partial_Sums |.seq.|) . n)) by VALUED_1: 18

 .= (((( Partial_Sums |.seq.|) . (n + k)) - (( Partial_Sums |.seq.|) . n)) + |.(seq . ((n + k) + 1)).|);



 A4: 0 <= |.(seq . ((n + k) + 1)).| by COMPLEX1: 46;

 assume P[k];

 hence P[(k + 1)] by A3, A4;

 end;



 A5: P[ 0 ];

 thus for k be Nat holds P[k] from NAT_1:sch 2( A5, A2);

 end;



 A6: for n,k be Nat holds |.((( Partial_Sums |.seq.|) . (n + k)) - (( Partial_Sums |.seq.|) . n)).| = ((( Partial_Sums |.seq.|) . (n + k)) - (( Partial_Sums |.seq.|) . n)) by A1, ABSVALUE:def 1;



 A7: for n, m st n <= m holds |.((( Partial_Sums seq) . m) - (( Partial_Sums seq) . n)).| <= |.((( Partial_Sums |.seq.|) . m) - (( Partial_Sums |.seq.|) . n)).|

 proof

 let n,m be Nat;

 assume n <= m;

 then

 consider k be Nat such that

 A8: m = (n + k) by NAT_1: 10;



 A9: for k be Nat holds |.((( Partial_Sums seq) . (n + k)) - (( Partial_Sums seq) . n)).| <= |.((( Partial_Sums |.seq.|) . (n + k)) - (( Partial_Sums |.seq.|) . n)).|

 proof

 defpred P[ Nat] means |.((( Partial_Sums seq) . (n + $1)) - (( Partial_Sums seq) . n)).| <= |.((( Partial_Sums |.seq.|) . (n + $1)) - (( Partial_Sums |.seq.|) . n)).|;

 A10:

 now

 let k be Nat;

 assume P[k];

 then

 A11: |.(((( Partial_Sums seq) . (n + k)) - (( Partial_Sums seq) . n)) + (seq . ((n + k) + 1))).| <= ( |.((( Partial_Sums seq) . (n + k)) - (( Partial_Sums seq) . n)).| + |.(seq . ((n + k) + 1)).|) & ( |.((( Partial_Sums seq) . (n + k)) - (( Partial_Sums seq) . n)).| + |.(seq . ((n + k) + 1)).|) <= ( |.((( Partial_Sums |.seq.|) . (n + k)) - (( Partial_Sums |.seq.|) . n)).| + |.(seq . ((n + k) + 1)).|) by COMPLEX1: 56, XREAL_1: 6;



 A12: |.((( Partial_Sums seq) . (n + (k + 1))) - (( Partial_Sums seq) . n)).| = |.(((( Partial_Sums seq) . (n + k)) + (seq . ((n + k) + 1))) - (( Partial_Sums seq) . n)).| by SERIES_1:def 1

 .= |.(((( Partial_Sums seq) . (n + k)) - (( Partial_Sums seq) . n)) + (seq . ((n + k) + 1))).|;

 ( |.((( Partial_Sums |.seq.|) . (n + k)) - (( Partial_Sums |.seq.|) . n)).| + |.(seq . ((n + k) + 1)).|) = (((( Partial_Sums |.seq.|) . (n + k)) - (( Partial_Sums |.seq.|) . n)) + |.(seq . ((n + k) + 1)).|) by A6

 .= (((( Partial_Sums |.seq.|) . (n + k)) + |.(seq . ((n + k) + 1)).|) - (( Partial_Sums |.seq.|) . n))

 .= (((( Partial_Sums |.seq.|) . (n + k)) + ( |.seq.| . ((n + k) + 1))) - (( Partial_Sums |.seq.|) . n)) by VALUED_1: 18

 .= ((( Partial_Sums |.seq.|) . (n + (k + 1))) - (( Partial_Sums |.seq.|) . n)) by SERIES_1:def 1

 .= |.((( Partial_Sums |.seq.|) . (n + (k + 1))) - (( Partial_Sums |.seq.|) . n)).| by A6;

 hence P[(k + 1)] by A12, A11, XXREAL_0: 2;

 end;



 A13: P[ 0 ];

 thus for k be Nat holds P[k] from NAT_1:sch 2( A13, A10);

 end;

 thus thesis by A9, A8;

 end;

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

 proof

 let n, m;

 m <= n implies |.((( Partial_Sums seq) . m) - (( Partial_Sums seq) . n)).| <= |.((( Partial_Sums |.seq.|) . m) - (( Partial_Sums |.seq.|) . n)).|

 proof

 assume m <= n;

 then

 A14: |.((( Partial_Sums seq) . n) - (( Partial_Sums seq) . m)).| <= |.((( Partial_Sums |.seq.|) . n) - (( Partial_Sums |.seq.|) . m)).| by A7;

 |.((( Partial_Sums |.seq.|) . n) - (( Partial_Sums |.seq.|) . m)).| = |.( - ((( Partial_Sums |.seq.|) . n) - (( Partial_Sums |.seq.|) . m))).| by COMPLEX1: 52

 .= |.((( Partial_Sums |.seq.|) . m) - (( Partial_Sums |.seq.|) . n)).|;

 hence thesis by A14, COMPLEX1: 60;

 end;

 hence thesis by A7;

 end;

 hence thesis;

 end;

 theorem :: COMSEQ_3:32



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

 proof

 now

 let n be Element of NAT ;



 thus ((( Partial_Sums ( Re seq)) ^\ k) . n) = (( Partial_Sums ( Re seq)) . (n + k)) by NAT_1:def 3

 .= (( Re ( Partial_Sums seq)) . (n + k)) by Th26

 .= ( Re (( Partial_Sums seq) . (n + k))) by Def5

 .= ( Re ((( Partial_Sums seq) ^\ k) . n)) by NAT_1:def 3

 .= (( Re (( Partial_Sums seq) ^\ k)) . n) by Def5;



 thus ((( Partial_Sums ( Im seq)) ^\ k) . n) = (( Partial_Sums ( Im seq)) . (n + k)) by NAT_1:def 3

 .= (( Im ( Partial_Sums seq)) . (n + k)) by Th26

 .= ( Im (( Partial_Sums seq) . (n + k))) by Def6

 .= ( Im ((( Partial_Sums seq) ^\ k) . n)) by NAT_1:def 3

 .= (( Im (( Partial_Sums seq) ^\ k)) . n) by Def6;

 end;

 hence thesis;

 end;

 theorem :: COMSEQ_3:33

 (for n holds (seq1 . n) = (seq . 0 )) implies ( Partial_Sums (seq ^\ 1)) = ((( Partial_Sums seq) ^\ 1) - seq1)

 proof

 assume

 A1: for n holds (seq1 . n) = (seq . 0 );

 A2:

 now

 let n;



 thus (( Re seq1) . n) = ( Re (seq1 . n)) by Def5

 .= ( Re (seq . 0 )) by A1

 .= (( Re seq) . 0 ) by Def5;



 thus (( Im seq1) . n) = ( Im (seq1 . n)) by Def6

 .= ( Im (seq . 0 )) by A1

 .= (( Im seq) . 0 ) by Def6;

 end;



 A3: ( Im ( Partial_Sums (seq ^\ 1))) = ( Partial_Sums ( Im (seq ^\ 1))) by Th26

 .= ( Partial_Sums (( Im seq) ^\ 1)) by Th23

 .= ((( Partial_Sums ( Im seq)) ^\ 1) - ( Im seq1)) by A2, SERIES_1: 11

 .= (( Im (( Partial_Sums seq) ^\ 1)) - ( Im seq1)) by Th32

 .= ( Im ((( Partial_Sums seq) ^\ 1) - seq1)) by Th18;

 ( Re ( Partial_Sums (seq ^\ 1))) = ( Partial_Sums ( Re (seq ^\ 1))) by Th26

 .= ( Partial_Sums (( Re seq) ^\ 1)) by Th23

 .= ((( Partial_Sums ( Re seq)) ^\ 1) - ( Re seq1)) by A2, SERIES_1: 11

 .= (( Re (( Partial_Sums seq) ^\ 1)) - ( Re seq1)) by Th32

 .= ( Re ((( Partial_Sums seq) ^\ 1) - seq1)) by Th18;

 hence thesis by A3, Th14;

 end;

 theorem :: COMSEQ_3:34



 Th34: ( Partial_Sums |.seq.|) is non-decreasing

 proof

 for n holds 0 <= ( |.seq.| . n) by Lm3;

 hence thesis by SERIES_1: 16;

 end;

 registration

 let seq be Complex_Sequence;

 cluster ( Partial_Sums |.seq.|) -> non-decreasing;

 coherence by Th34;

 end

 theorem :: COMSEQ_3:35

 (for n st n <= m holds (seq1 . n) = (seq2 . n)) implies (( Partial_Sums seq1) . m) = (( Partial_Sums seq2) . m)

 proof

 defpred P[ Nat] means $1 <= m implies (( Partial_Sums seq1) . $1) = (( Partial_Sums seq2) . $1);

 assume

 A1: for n st n <= m holds (seq1 . n) = (seq2 . n);



 A2: for k be Nat st P[k] holds P[(k + 1)]

 proof

 let k be Nat such that

 A3: P[k];

 assume

 A4: (k + 1) <= m;

 k < (k + 1) by XREAL_1: 29;



 hence (( Partial_Sums seq1) . (k + 1)) = ((( Partial_Sums seq2) . k) + (seq1 . (k + 1))) by A3, A4, SERIES_1:def 1, XXREAL_0: 2

 .= ((( Partial_Sums seq2) . k) + (seq2 . (k + 1))) by A1, A4

 .= (( Partial_Sums seq2) . (k + 1)) by SERIES_1:def 1;

 end;



 A5: P[ 0 ]

 proof

 assume 0 <= m;



 thus (( Partial_Sums seq1) . 0 ) = (seq1 . 0 ) by SERIES_1:def 1

 .= (seq2 . 0 ) by A1

 .= (( Partial_Sums seq2) . 0 ) by SERIES_1:def 1;

 end;

 for k holds P[k] from NAT_1:sch 2( A5, A2);

 hence thesis;

 end;

 theorem :: COMSEQ_3:36



 Th36: 1r <> z implies for n holds (( Partial_Sums (z GeoSeq )) . n) = (( 1r - (z |^ (n + 1))) / ( 1r - z))

 proof

 now

 let z;

 defpred P[ Nat] means (( Partial_Sums (z GeoSeq )) . $1) = (( 1r - (z |^ ($1 + 1))) / ( 1r - z));

 assume 1r <> z;

 then

 A1: ( 1r - z) <> 0c ;



 A2: for n st P[n] holds P[(n + 1)]

 proof

 let n;

 assume P[n];



 hence (( Partial_Sums (z GeoSeq )) . (n + 1)) = ((( 1r - (z |^ (n + 1))) / ( 1r - z)) + ((z |^ (n + 1)) * 1r )) by COMPLEX1:def 4, SERIES_1:def 1

 .= ((( 1r - (z |^ (n + 1))) / ( 1r - z)) + ((z |^ (n + 1)) * (( 1r - z) / ( 1r - z)))) by A1, COMPLEX1:def 4, XCMPLX_1: 60

 .= ((( 1r - (z |^ (n + 1))) / ( 1r - z)) + (((z |^ (n + 1)) * ( 1r - z)) / ( 1r - z))) by XCMPLX_1: 74

 .= ((( 1r - (z |^ (n + 1))) + ((z |^ (n + 1)) - ((z |^ (n + 1)) * z))) / ( 1r - z)) by COMPLEX1:def 4, XCMPLX_1: 62

 .= (( 1r - ((z |^ (n + 1)) * z)) / ( 1r - z))

 .= (( 1r - (z |^ ((n + 1) + 1))) / ( 1r - z)) by NEWTON: 6;

 end;

 (( Partial_Sums (z GeoSeq )) . 0 ) = ((z GeoSeq ) . 0 ) by SERIES_1:def 1

 .= 1r by Def1

 .= (( 1r - (1 * z)) / ( 1r - z)) by A1, COMPLEX1:def 4, XCMPLX_1: 60

 .= (( 1r - (z |^ ( 0 + 1))) / ( 1r - z));

 then

 A3: P[ 0 ];

 thus for n holds P[n] from NAT_1:sch 2( A3, A2);

 end;

 hence thesis;

 end;

 theorem :: COMSEQ_3:37



 Th37: z <> 1r & (for n holds (seq . (n + 1)) = (z * (seq . n))) implies for n holds (( Partial_Sums seq) . n) = ((seq . 0 ) * (( 1r - (z |^ (n + 1))) / ( 1r - z)))

 proof

 assume that

 A1: z <> 1r and

 A2: for n holds (seq . (n + 1)) = (z * (seq . n));

 defpred P[ Nat] means (seq . $1) = ((seq . 0 ) * ((z GeoSeq ) . $1));

 A3:

 now

 let n be Nat;

 assume P[n];



 then (seq . (n + 1)) = (z * ((seq . 0 ) * ((z GeoSeq ) . n))) by A2

 .= ((seq . 0 ) * (z * ((z GeoSeq ) . n)))

 .= ((seq . 0 ) * ((z GeoSeq ) . (n + 1))) by Def1;

 hence P[(n + 1)];

 end;

 let n;

 (seq . 0 ) = ((seq . 0 ) * 1r ) by COMPLEX1:def 4

 .= ((seq . 0 ) * ((z GeoSeq ) . 0 )) by Def1;

 then

 A4: P[ 0 ];

 for n be Nat holds P[n] from NAT_1:sch 2( A4, A3);

 then for n be Element of NAT holds P[n];



 then ( Partial_Sums seq) = ( Partial_Sums ((seq . 0 ) (#) (z GeoSeq ))) by VALUED_1: 7

 .= ((seq . 0 ) (#) ( Partial_Sums (z GeoSeq ))) by Th29;



 hence (( Partial_Sums seq) . n) = ((seq . 0 ) * (( Partial_Sums (z GeoSeq )) . n)) by VALUED_1: 6

 .= ((seq . 0 ) * (( 1r - (z |^ (n + 1))) / ( 1r - z))) by A1, Th36;

 end;

 begin

 theorem :: COMSEQ_3:38



 Th38: for a,b be Real_Sequence, c be Complex_Sequence st (for n holds ( Re (c . n)) = (a . n) & ( Im (c . n)) = (b . n)) holds a is convergent & b is convergent iff c is convergent

 proof

 let a,b be Real_Sequence, c be Complex_Sequence such that

 A1: for n holds ( Re (c . n)) = (a . n) & ( Im (c . n)) = (b . n);

 thus a is convergent & b is convergent implies c is convergent

 proof

 assume that

 A2: a is convergent and

 A3: b is convergent;

 consider a1 be Real such that

 A4: for p be Real st 0 < p holds ex n st for m st n <= m holds |.((a . m) - a1).| < p by A2, SEQ_2:def 6;

 consider b1 be Real such that

 A5: for p be Real st 0 )) as Element of COMPLEX by XCMPLX_0:def 2;

 take g;

 for p st 0 < p holds ex n st for m st n <= m holds |.((c . m) - g).| < p

 proof

 let p;

 assume

 A6: 0 < p;

 then

 consider n1 such that

 A7: for m st n1 <= m holds |.((a . m) - a1).| < (p / 2) by A4;

 consider n2 such that

 A8: for m st n2 <= m holds |.((b . m) - b1).| < (p / 2) by A5, A6;

 n1 <= (n1 + n2) & n2 <= (n1 + n2) by NAT_1: 11;

 then

 consider n such that

 A9: n1 <= n and

 A10: n2 <= n;

 take n;

 for m st n <= m holds |.((c . m) - g).| < p

 proof

 let m;

 ( Re (c . m)) = (a . m) & ( Re g) = a1 by A1, COMPLEX1: 12;

 then

 A11: ( Re ((c . m) - g)) = ((a . m) - a1) by COMPLEX1: 19;

 ( Im (c . m)) = (b . m) & ( Im g) = b1 by A1, COMPLEX1: 12;

 then

 A12: ( Im ((c . m) - g)) = ((b . m) - b1) by COMPLEX1: 19;

 assume

 A13: n <= m;

 then n2 <= m by A10, XXREAL_0: 2;

 then

 A14: |.((b . m) - b1).| < (p / 2) by A8;

 n1 <= m by A9, A13, XXREAL_0: 2;

 then |.((a . m) - a1).| < (p / 2) by A7;

 then

 A15: ( |.((a . m) - a1).| + |.((b . m) - b1).|) < ((p / 2) + (p / 2)) by A14, XREAL_1: 8;

 |.((c . m) - g).| <= ( |.( Re ((c . m) - g)).| + |.( Im ((c . m) - g)).|) by Th12;

 hence thesis by A15, A11, A12, XXREAL_0: 2;

 end;

 hence thesis;

 end;

 hence thesis;

 end;

 assume c is convergent;

 then

 consider z be Complex such that

 A16: for p be Real st 0 < p holds ex n st for m st n <= m holds |.((c . m) - z).| < p;

 thus a is convergent

 proof

 reconsider z as Element of COMPLEX by XCMPLX_0:def 2;

 take ( Re z);

 let p be Real;

 assume

 A17: 0 < p;

 consider n such that

 A18: for m st n <= m holds |.((c . m) - z).| < p by A16, A17;

 take n;

 let m;

 assume n <= m;

 then

 A19: |.((c . m) - z).| < p by A18;

 ( Re (c . m)) = (a . m) & ( Re ((c . m) - z)) = (( Re (c . m)) - ( Re z)) by A1, COMPLEX1: 19;

 then |.((a . m) - ( Re z)).| <= |.((c . m) - z).| by Th13;

 hence thesis by A19, XXREAL_0: 2;

 end;

 take ( Im z);

 let p be Real;

 assume

 A20: p > 0 ;

 consider n such that

 A21: for m st n <= m holds |.((c . m) - z).| < p by A16, A20;

 take n;

 let m;

 assume n <= m;

 then

 A22: |.((c . m) - z).| < p by A21;



 A23: ( Im ((c . m) - z)) = (( Im (c . m)) - ( Im z)) by COMPLEX1: 19;

 ( Im (c . m)) = (b . m) by A1;

 then |.((b . m) - ( Im z)).| <= |.((c . m) - z).| by A23, Th13;

 hence thesis by A22, XXREAL_0: 2;

 end;

 theorem :: COMSEQ_3:39



 Th39: for a,b be convergent Real_Sequence, c be Complex_Sequence st (for n holds ( Re (c . n)) = (a . n) & ( Im (c . n)) = (b . n)) holds c is convergent & ( lim c) = (( lim a) + (( lim b) * ))

 proof

 let a,b be convergent Real_Sequence, c be Complex_Sequence;

 reconsider g = (( lim a) + (( lim b) * )) as Element of COMPLEX by XCMPLX_0:def 2;

 assume

 A1: for n holds ( Re (c . n)) = (a . n) & ( Im (c . n)) = (b . n);

 hence

 A2: c is convergent by Th38;

 for p be Real st 0 < p holds ex n st for m st n <= m holds |.((c . m) - g).| < p

 proof

 let p be Real;

 assume

 A3: 0 < p;

 then

 consider n1 such that

 A4: for m st n1 <= m holds |.((a . m) - ( lim a)).| < (p / 2) by SEQ_2:def 7;

 consider n2 such that

 A5: for m st n2 <= m holds |.((b . m) - ( lim b)).| < (p / 2) by A3, SEQ_2:def 7;

 n1 <= (n1 + n2) & n2 <= (n1 + n2) by NAT_1: 11;

 then

 consider n such that

 A6: n1 <= n and

 A7: n2 <= n;

 take n;

 let m;

 assume

 A8: n <= m;

 then n2 <= m by A7, XXREAL_0: 2;

 then

 A9: |.((b . m) - ( lim b)).| < (p / 2) by A5;

 n1 <= m by A6, A8, XXREAL_0: 2;

 then |.((a . m) - ( lim a)).| < (p / 2) by A4;

 then

 A10: ( |.((a . m) - ( lim a)).| + |.((b . m) - ( lim b)).|) < ((p / 2) + (p / 2)) by A9, XREAL_1: 8;

 ( Re (c . m)) = (a . m) & ( Re g) = ( lim a) by A1, COMPLEX1: 12;

 then

 A11: ( Re ((c . m) - g)) = ((a . m) - ( lim a)) by COMPLEX1: 19;

 ( Im (c . m)) = (b . m) & ( Im g) = ( lim b) by A1, COMPLEX1: 12;

 then

 A12: ( Im ((c . m) - g)) = ((b . m) - ( lim b)) by COMPLEX1: 19;

 |.((c . m) - g).| <= ( |.( Re ((c . m) - g)).| + |.( Im ((c . m) - g)).|) by Th12;

 hence thesis by A10, A11, A12, XXREAL_0: 2;

 end;

 hence thesis by A2, COMSEQ_2:def 6;

 end;

 theorem :: COMSEQ_3:40



 Th40: for a,b be Real_Sequence, c be convergent Complex_Sequence st (for n 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

 let a,b be Real_Sequence, c be convergent Complex_Sequence;

 assume

 A1: for n holds ( Re (c . n)) = (a . n) & ( Im (c . n)) = (b . n);



 A2: for p be Real st 0 0 ;

 consider n such that

 A4: for m st n <= m holds |.((c . m) - ( lim c)).| < p by A3, COMSEQ_2:def 6;

 take n;

 let m;

 assume n <= m;

 then

 A5: |.((c . m) - ( lim c)).| < p by A4;

 ( Im (c . m)) = (b . m) & ( Im ((c . m) - ( lim c))) = (( Im (c . m)) - ( Im ( lim c))) by A1, COMPLEX1: 19;

 then |.((b . m) - ( Im ( lim c))).| <= |.((c . m) - ( lim c)).| by Th13;

 hence thesis by A5, XXREAL_0: 2;

 end;



 A6: for p be Real st 0 < p holds ex n st for m st n <= m holds |.((a . m) - ( Re ( lim c))).| < p

 proof

 let p be Real;

 assume

 A7: 0 < p;

 consider n such that

 A8: for m st n <= m holds |.((c . m) - ( lim c)).| < p by A7, COMSEQ_2:def 6;

 take n;

 let m;

 ( Re (c . m)) = (a . m) by A1;

 then ( Re ((c . m) - ( lim c))) = ((a . m) - ( Re ( lim c))) by COMPLEX1: 19;

 then

 A9: |.((a . m) - ( Re ( lim c))).| <= |.((c . m) - ( lim c)).| by Th13;

 assume n <= m;

 then |.((c . m) - ( lim c)).| < p by A8;

 hence thesis by A9, XXREAL_0: 2;

 end;

 a is convergent & b is convergent by A1, Th38;

 hence thesis by A6, A2, SEQ_2:def 7;

 end;

 theorem :: COMSEQ_3:41



 Th41: for c be convergent Complex_Sequence holds ( Re c) is convergent & ( Im c) is convergent & ( lim ( Re c)) = ( Re ( lim c)) & ( lim ( Im c)) = ( Im ( lim c))

 proof

 let c be convergent Complex_Sequence;

 (for n holds (( Re c) . n) = ( Re (c . n))) & for n holds (( Im c) . n) = ( Im (c . n)) by Def5, Def6;

 hence thesis by Th40;

 end;

 registration

 let c be convergent Complex_Sequence;

 cluster ( Re c) -> convergent;

 coherence by Th41;

 cluster ( Im c) -> convergent;

 coherence by Th41;

 end

 theorem :: COMSEQ_3:42



 Th42: for c be 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))

 proof

 let c be Complex_Sequence;

 assume

 A1: ( Re c) is convergent & ( Im c) is convergent;



 A2: (for n holds (( Re c) . n) = ( Re (c . n))) & for n holds (( Im c) . n) = ( Im (c . n)) by Def5, Def6;

 then ( lim c) = (( lim ( Re c)) + (( lim ( Im c)) * )) by A1, Th39;

 hence thesis by A1, A2, Th39, COMPLEX1: 12;

 end;

 theorem :: COMSEQ_3:43



 Th43: ( 0 < |.z.| & |.z.| < 1 & (seq . 0 ) = z & for n holds (seq . (n + 1)) = ((seq . n) * z)) implies seq is convergent & ( lim seq) = 0c

 proof

 assume that

 A1: 0 < |.z.| and

 A2: |.z.| < 1;

 deffunc g( Nat) = ( |.z.| to_power ($1 + 1));

 consider rseq1 such that

 A3: for n holds (rseq1 . n) = g(n) from SEQ_1:sch 1;

 assume that

 A4: (seq . 0 ) = z and

 A5: for n holds (seq . (n + 1)) = ((seq . n) * z);



 A6: for n holds |.(seq . n).| = ( |.z.| to_power (n + 1))

 proof

 defpred P[ Nat] means |.(seq . $1).| = ( |.z.| to_power ($1 + 1));



 A7: for k be Nat st P[k] holds P[(k + 1)]

 proof

 let k be Nat;

 assume

 A8: P[k];

 |.(seq . (k + 1)).| = |.((seq . k) * z).| by A5

 .= (( |.z.| to_power (k + 1)) * |.z.|) by A8, COMPLEX1: 65

 .= (( |.z.| to_power (k + 1)) * ( |.z.| to_power 1)) by POWER: 25

 .= ( |.z.| to_power ((k + 1) + 1)) by A1, POWER: 27;

 hence thesis;

 end;



 A9: P[ 0 ] by A4, POWER: 25;

 for n holds P[n] from NAT_1:sch 2( A9, A7);

 hence thesis;

 end;

 A10:

 now

 let n;

 (( abs ( Re seq)) . n) = |.(( Re seq) . n).| by SEQ_1: 12;

 then

 A11: (( abs ( Re seq)) . n) = |.( Re (seq . n)).| by Def5;

 |.( Re (seq . n)).| <= |.(seq . n).| & |.(seq . n).| = ( |.z.| to_power (n + 1)) by A6, Th13;

 hence (( abs ( Re seq)) . n) <= (rseq1 . n) by A3, A11;

 end;

 A12:

 now

 let n;



 A13: |.(seq . n).| = ( |.z.| to_power (n + 1)) by A6;

 (( abs ( Im seq)) . n) = |.(( Im seq) . n).| & |.( Im (seq . n)).| <= |.(seq . n).| by Th13, SEQ_1: 12;

 then (( abs ( Im seq)) . n) <= ( |.z.| to_power (n + 1)) by A13, Def6;

 hence (( abs ( Im seq)) . n) <= (rseq1 . n) by A3;

 end;

 (C . 0 ) = 0 ;

 then

 A14: ( lim C) = 0 by SEQ_4: 25;



 A15: rseq1 is convergent & ( lim rseq1) = 0 by A1, A2, A3, SERIES_1: 1;

 now

 let n;

 (( abs ( Re seq)) . n) = |.(( Re seq) . n).| by SEQ_1: 12;

 then 0 <= (( abs ( Re seq)) . n) by COMPLEX1: 46;

 hence (C . n) <= (( abs ( Re seq)) . n);

 end;

 then

 A16: ( abs ( Re seq)) is convergent & ( lim ( abs ( Re seq))) = 0 by A14, A15, A10, SEQ_2: 19, SEQ_2: 20;

 then

 A17: ( Re seq) is convergent by SEQ_4: 15;

 now

 let n;

 (( abs ( Im seq)) . n) = |.(( Im seq) . n).| by SEQ_1: 12;

 then 0 <= (( abs ( Im seq)) . n) by COMPLEX1: 46;

 hence (C . n) <= (( abs ( Im seq)) . n);

 end;

 then

 A18: ( abs ( Im seq)) is convergent & ( lim ( abs ( Im seq))) = 0 by A14, A15, A12, SEQ_2: 19, SEQ_2: 20;

 then

 A19: ( Im seq) is convergent by SEQ_4: 15;

 ( lim ( Im seq)) = 0 by A18, SEQ_4: 15;

 then

 A20: ( Im ( lim seq)) = 0 by A17, A19, Th42;

 ( lim ( Re seq)) = 0 by A16, SEQ_4: 15;

 then ( Re ( lim seq)) = 0 by A17, A19, Th42;

 hence thesis by A17, A19, A20, Lm1, Th42, COMPLEX1: 13;

 end;

 theorem :: COMSEQ_3:44



 Th44: |.z.| < 1 & (for n holds (seq . n) = (z |^ (n + 1))) implies seq is convergent & ( lim seq) = 0c

 proof

 assume that

 A1: |.z.| < 1 and

 A2: for n holds (seq . n) = (z |^ (n + 1));

 A3:

 now

 let n;



 thus (seq . (n + 1)) = (z |^ ((n + 1) + 1)) by A2

 .= ((z |^ (n + 1)) * z) by NEWTON: 6

 .= ((seq . n) * z) by A2;

 end;

 A4:

 now

 assume |.z.| = 0 ;

 then

 A5: z = 0c by COMPLEX1: 45;

 A6:

 now

 let n;



 thus (seq . n) = ( 0c |^ (n + 1)) by A2, A5

 .= ((( 0c GeoSeq ) . n) * 0c ) by Def1

 .= 0c ;

 end;

 hence seq is convergent by COMSEQ_2: 9;

 thus thesis by A6, COMSEQ_2: 9, COMSEQ_2: 10;

 end;



 A7: (seq . 0 ) = (z |^ ( 0 + 1)) by A2

 .= z;

 now



 A8: 0 <= |.z.| by COMPLEX1: 46;

 assume |.z.| <> 0 ;

 hence thesis by A1, A7, A3, A8, Th43;

 end;

 hence thesis by A4;

 end;

 theorem :: COMSEQ_3:45

 r > 0 & (ex m st for n st n >= m holds |.(seq . n).| >= r) implies not |.seq.| is convergent or ( lim |.seq.|) <> 0

 proof

 assume that

 A1: r > 0 and

 A2: ex m st for n st n >= m holds |.(seq . n).| >= r;

 consider m such that

 A3: for n st n >= m holds |.(seq . n).| >= r by A2;

 now

 let n such that

 A4: n >= m;

 0 <= ( |.seq.| . n) by Lm3;



 then |.( |.seq.| . n).| = ( |.seq.| . n) by ABSVALUE:def 1

 .= |.(seq . n).| by VALUED_1: 18;

 hence |.( |.seq.| . n).| >= r by A3, A4;

 end;

 hence thesis by A1, SERIES_1: 38;

 end;

 theorem :: COMSEQ_3:46



 Th46: seq is convergent iff for p st 0 < p holds ex n st for m st n <= m holds |.((seq . m) - (seq . n)).| < p

 proof

 A1:

 now

 assume

 A2: for p st 0 < p holds ex n st for m st n <= m holds |.((seq . m) - (seq . n)).| < p;

 for p be Real st 0 < p holds ex n st for m st n <= m holds |.((( Re seq) . m) - (( Re seq) . n)).| < p

 proof

 let p be Real;

 assume

 A3: 0 < p;

 consider n such that

 A4: for m st n <= m holds |.((seq . m) - (seq . n)).| < p by A2, A3;

 take n;

 let m;

 assume n <= m;

 then

 A5: |.((seq . m) - (seq . n)).| < p by A4;

 ( Re ((seq . m) - (seq . n))) = (( Re (seq . m)) - ( Re (seq . n))) by COMPLEX1: 19

 .= ((( Re seq) . m) - ( Re (seq . n))) by Def5

 .= ((( Re seq) . m) - (( Re seq) . n)) by Def5;

 then |.((( Re seq) . m) - (( Re seq) . n)).| <= |.((seq . m) - (seq . n)).| by Th13;

 hence thesis by A5, XXREAL_0: 2;

 end;

 hence

 A6: ( Re seq) is convergent by SEQ_4: 41;

 for p be Real st 0 < p holds ex n st for m st n <= m holds |.((( Im seq) . m) - (( Im seq) . n)).| < p

 proof

 let p be Real;

 assume

 A7: 0 < p;

 consider n such that

 A8: for m st n <= m holds |.((seq . m) - (seq . n)).| < p by A2, A7;

 take n;

 let m;

 assume n <= m;

 then

 A9: |.((seq . m) - (seq . n)).| < p by A8;

 ( Im ((seq . m) - (seq . n))) = (( Im (seq . m)) - ( Im (seq . n))) by COMPLEX1: 19

 .= ((( Im seq) . m) - ( Im (seq . n))) by Def6

 .= ((( Im seq) . m) - (( Im seq) . n)) by Def6;

 then |.((( Im seq) . m) - (( Im seq) . n)).| <= |.((seq . m) - (seq . n)).| by Th13;

 hence thesis by A9, XXREAL_0: 2;

 end;

 hence ( Im seq) is convergent by SEQ_4: 41;

 hence seq is convergent by A6, Th42;

 end;

 now

 assume seq is convergent;

 then

 consider z be Complex such that

 A10: for p be Real st 0 < p holds ex n st for m st n <= m holds |.((seq . m) - z).| < p;

 let p;

 assume 0 < p;

 then

 consider n such that

 A11: for m st n <= m holds |.((seq . m) - z).| < (p / 2) by A10;

 take n;

 let m;

 assume n <= m;

 then

 A12: |.((seq . m) - z).| < (p / 2) by A11;

 |.((seq . n) - z).| < (p / 2) by A11;

 then ( |.((seq . m) - z).| + |.((seq . n) - z).|) < ((p / 2) + (p / 2)) by A12, XREAL_1: 8;

 then

 A13: ( |.((seq . m) - z).| + |.(z - (seq . n)).|) < p by COMPLEX1: 60;

 |.((seq . m) - (seq . n)).| <= ( |.((seq . m) - z).| + |.(z - (seq . n)).|) by COMPLEX1: 63;

 hence |.((seq . m) - (seq . n)).| < p by A13, XXREAL_0: 2;

 end;

 hence thesis by A1;

 end;

 theorem :: COMSEQ_3:47

 seq is convergent implies for p st 0 < p holds ex n st for m,l be Nat st n <= m & n <= l holds |.((seq . m) - (seq . l)).| < p

 proof

 assume

 A1: seq is convergent;

 let p;

 assume 0 < p;

 then

 consider n such that

 A2: for m st n <= m holds |.((seq . m) - (seq . n)).| < (p / 2) by A1, Th46;

 take n;

 let m,l be Nat;

 assume n <= m & n <= l;

 then |.((seq . m) - (seq . n)).| < (p / 2) & |.((seq . l) - (seq . n)).| < (p / 2) by A2;

 then

 A3: ( |.((seq . m) - (seq . n)).| + |.((seq . l) - (seq . n)).|) < ((p / 2) + (p / 2)) by XREAL_1: 8;

 |.(((seq . m) - (seq . n)) - ((seq . l) - (seq . n))).| <= ( |.((seq . m) - (seq . n)).| + |.((seq . l) - (seq . n)).|) by COMPLEX1: 57;

 hence |.((seq . m) - (seq . l)).| < p by A3, XXREAL_0: 2;

 end;

 theorem :: COMSEQ_3:48

 (for n holds |.(seq . n).| <= (rseq . n)) & rseq is convergent & ( lim rseq) = 0 implies seq is convergent & ( lim seq) = 0c

 proof

 assume that

 A1: for n holds |.(seq . n).| <= (rseq . n) and

 A2: rseq is convergent & ( lim rseq) = 0 ;

 A3:

 now

 let n;

 (( abs ( Re seq)) . n) = |.(( Re seq) . n).| by SEQ_1: 12;

 then 0 <= (( abs ( Re seq)) . n) by COMPLEX1: 46;

 hence (C . n) <= (( abs ( Re seq)) . n);

 end;

 (C . 0 ) = 0 ;

 then

 A4: ( lim C) = 0 by SEQ_4: 25;

 now

 let n;

 (( Re seq) . n) = ( Re (seq . n)) by Def5;

 then

 A5: (( abs ( Re seq)) . n) = |.( Re (seq . n)).| by SEQ_1: 12;

 |.( Re (seq . n)).| <= |.(seq . n).| & |.(seq . n).| <= (rseq . n) by A1, Th13;

 hence (( abs ( Re seq)) . n) <= (rseq . n) by A5, XXREAL_0: 2;

 end;

 then

 A6: ( abs ( Re seq)) is convergent & ( lim ( abs ( Re seq))) = 0 by A2, A4, A3, SEQ_2: 19, SEQ_2: 20;

 then

 A7: ( Re seq) is convergent by SEQ_4: 15;

 A8:

 now

 let n;

 (( abs ( Im seq)) . n) = |.(( Im seq) . n).| by SEQ_1: 12;

 then 0 <= (( abs ( Im seq)) . n) by COMPLEX1: 46;

 hence (C . n) <= (( abs ( Im seq)) . n);

 end;

 now

 let n;



 A9: (( Im seq) . n) = ( Im (seq . n)) & (( abs ( Im seq)) . n) = |.(( Im seq) . n).| by Def6, SEQ_1: 12;

 |.( Im (seq . n)).| <= |.(seq . n).| & |.(seq . n).| <= (rseq . n) by A1, Th13;

 hence (( abs ( Im seq)) . n) <= (rseq . n) by A9, XXREAL_0: 2;

 end;

 then

 A10: ( abs ( Im seq)) is convergent & ( lim ( abs ( Im seq))) = 0 by A2, A4, A8, SEQ_2: 19, SEQ_2: 20;

 then

 A11: ( Im seq) is convergent by SEQ_4: 15;

 ( lim ( Im seq)) = 0 by A10, SEQ_4: 15;

 then

 A12: ( Im ( lim seq)) = 0 by A7, A11, Th42;

 ( lim ( Re seq)) = 0 by A6, SEQ_4: 15;

 then ( Re ( lim seq)) = 0 by A7, A11, Th42;

 hence thesis by A7, A11, A12, Lm1, Th42, COMPLEX1: 13;

 end;

 begin

 theorem :: COMSEQ_3:49

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

 proof

 assume seq is subsequence of seq1;

 then

 consider Nseq such that

 A1: seq = (seq1 * Nseq) by VALUED_0:def 17;

 ( Re seq) = (( Re seq1) * Nseq) by A1, Th22;

 hence ( Re seq) is subsequence of ( Re seq1);

 ( Im seq) = (( Im seq1) * Nseq) by A1, Th22;

 hence thesis;

 end;

 theorem :: COMSEQ_3:50

 seq is bounded implies ex seq1 st seq1 is subsequence of seq & seq1 is convergent

 proof

 assume seq is bounded;

 then

 consider r be Real such that

 A1: 0 < r and

 A2: for n holds |.(seq . n).| < r by COMSEQ_2: 8;

 now

 let n;

 |.(( Re seq) . n).| = |.( Re (seq . n)).| & |.( Re (seq . n)).| <= |.(seq . n).| by Def5, Th13;

 hence |.(( Re seq) . n).| < r by A2, XXREAL_0: 2;

 end;

 then ( Re seq) is bounded by A1, SEQ_2: 3;

 then

 consider rseq1 such that

 A3: rseq1 is subsequence of ( Re seq) and

 A4: rseq1 is convergent by SEQ_4: 40;

 consider Nseq such that

 A5: rseq1 = (( Re seq) * Nseq) by A3, VALUED_0:def 17;

 A6:

 now

 let n;

 n in NAT by ORDINAL1:def 12;

 then |.((seq * Nseq) . n).| = |.(seq . (Nseq . n)).| by FUNCT_2: 15;

 hence |.((seq * Nseq) . n).| < r by A2;

 end;

 now

 let n;

 |.(( Im (seq * Nseq)) . n).| = |.( Im ((seq * Nseq) . n)).| & |.( Im ((seq * Nseq) . n)).| <= |.((seq * Nseq) . n).| by Def6, Th13;

 hence |.(( Im (seq * Nseq)) . n).| < r by A6, XXREAL_0: 2;

 end;

 then ( Im (seq * Nseq)) is bounded by A1, SEQ_2: 3;

 then

 consider rseq2 such that

 A7: rseq2 is subsequence of ( Im (seq * Nseq)) and

 A8: rseq2 is convergent by SEQ_4: 40;

 consider Nseq1 such that

 A9: rseq2 = (( Im (seq * Nseq)) * Nseq1) by A7, VALUED_0:def 17;

 ( Re ((seq * Nseq) * Nseq1)) = (( Re (seq * Nseq)) * Nseq1) by Th22

 .= (rseq1 * Nseq1) by A5, Th22;

 then

 A10: ( Re ((seq * Nseq) * Nseq1)) is convergent by A4, SEQ_4: 16;

 (seq * Nseq) is subsequence of seq & ((seq * Nseq) * Nseq1) is subsequence of (seq * Nseq) by VALUED_0:def 17;

 then

 A11: ((seq * Nseq) * Nseq1) is subsequence of seq by VALUED_0: 20;

 ( Im ((seq * Nseq) * Nseq1)) is convergent by A8, A9, Th22;

 hence thesis by A11, A10, Th42;

 end;

 definition

 let seq be Complex_Sequence;

 :: COMSEQ_3:def8

 attr seq is summable means

 : Def8: ( Partial_Sums seq) is convergent;

 end

 set D = ( NAT --> 0c );

 registration

 cluster summable for Complex_Sequence;

 existence

 proof

 take D, 0c ;

 let p be Real such that

 A1: 0 < p;

 take 0 ;

 for n holds (D . n) = 0c ;

 hence thesis by A1, Th24, COMPLEX1: 44;

 end;

 end

 registration

 let seq be summable Complex_Sequence;

 cluster ( Partial_Sums seq) -> convergent;

 coherence by Def8;

 end

 definition

 let seq be Complex_Sequence;

 :: COMSEQ_3:def9

 attr seq is absolutely_summable means

 : Def9: |.seq.| is summable;

 end

 theorem :: COMSEQ_3:51



 Th51: (for n holds (seq . n) = 0c ) implies seq is absolutely_summable

 proof

 assume

 A1: for n holds (seq . n) = 0c ;

 take 0 ;

 let p be Real such that

 A2: 0 < p;

 take 0 ;

 let m;

 |.((( Partial_Sums |.seq.|) . m) - 0 ).| = |.( 0 - 0 ).| by A1, Th25

 .= 0 by ABSVALUE:def 1;

 hence thesis by A2;

 end;

 registration

 cluster absolutely_summable for Complex_Sequence;

 existence

 proof

 take D;

 for n holds (D . n) = 0c ;

 hence thesis by Th51;

 end;

 end

 registration

 let seq be absolutely_summable Complex_Sequence;

 cluster |.seq.| -> summable;

 coherence by Def9;

 end

 theorem :: COMSEQ_3:52



 Th52: seq is summable implies seq is convergent & ( lim seq) = 0c

 proof

 assume

 A1: seq is summable;

 then ( Re ( Partial_Sums seq)) is convergent;

 then ( Partial_Sums ( Re seq)) is convergent by Th26;

 then

 A2: ( Re seq) is summable;

 ( Im ( Partial_Sums seq)) is convergent by A1;

 then ( Partial_Sums ( Im seq)) is convergent by Th26;

 then

 A3: ( Im seq) is summable;

 then ( lim ( Im seq)) = 0 by SERIES_1: 4;

 then

 A4: ( Im ( lim seq)) = 0 by A2, A3, Th42;

 ( lim ( Re seq)) = 0 by A2, SERIES_1: 4;

 then ( Re ( lim seq)) = 0 by A2, A3, Th42;

 hence thesis by A2, A3, A4, Lm1, Th42, COMPLEX1: 13;

 end;

 registration

 cluster summable -> convergent for Complex_Sequence;

 coherence by Th52;

 end

 theorem :: COMSEQ_3:53



 Th53: seq is summable implies ( Re seq) is summable & ( Im seq) is summable & ( Sum seq) = (( Sum ( Re seq)) + (( Sum ( Im seq)) * ))

 proof



 A1: ( lim ( Re ( Partial_Sums seq))) = ( lim ( Partial_Sums ( Re seq))) & ( lim ( Im ( Partial_Sums seq))) = ( lim ( Partial_Sums ( Im seq))) by Th26;

 assume

 A2: seq is summable;

 then ( Re ( Partial_Sums seq)) is convergent;

 then

 A3: ( Partial_Sums ( Re seq)) is convergent by Th26;

 ( Im ( Partial_Sums seq)) is convergent by A2;

 then

 A4: ( Partial_Sums ( Im seq)) is convergent by Th26;

 ( lim ( Re ( Partial_Sums seq))) = ( Re ( lim ( Partial_Sums seq))) & ( lim ( Im ( Partial_Sums seq))) = ( Im ( lim ( Partial_Sums seq))) by A2, Th41;

 hence thesis by A3, A4, A1, COMPLEX1: 13;

 end;

 registration

 let seq be summable Complex_Sequence;

 cluster ( Re seq) -> summable;

 coherence by Th53;

 cluster ( Im seq) -> summable;

 coherence by Th53;

 end

 theorem :: COMSEQ_3:54



 Th54: seq1 is summable & seq2 is summable implies (seq1 + seq2) is summable & ( Sum (seq1 + seq2)) = (( Sum seq1) + ( Sum seq2))

 proof

 assume

 A1: seq1 is summable & seq2 is summable;

 then

 A2: (( Partial_Sums seq1) + ( Partial_Sums seq2)) is convergent;



 A3: (( Partial_Sums seq1) + ( Partial_Sums seq2)) = ( Partial_Sums (seq1 + seq2)) by Th27;

 ( Sum (seq1 + seq2)) = ( lim (( Partial_Sums seq1) + ( Partial_Sums seq2))) by Th27

 .= (( lim ( Partial_Sums seq1)) + ( lim ( Partial_Sums seq2))) by A1, COMSEQ_2: 14;

 hence thesis by A2, A3;

 end;

 theorem :: COMSEQ_3:55



 Th55: seq1 is summable & seq2 is summable implies (seq1 - seq2) is summable & ( Sum (seq1 - seq2)) = (( Sum seq1) - ( Sum seq2))

 proof

 assume

 A1: seq1 is summable & seq2 is summable;

 then

 A2: (( Partial_Sums seq1) - ( Partial_Sums seq2)) is convergent;



 A3: (( Partial_Sums seq1) - ( Partial_Sums seq2)) = ( Partial_Sums (seq1 - seq2)) by Th28;

 ( Sum (seq1 - seq2)) = ( lim (( Partial_Sums seq1) - ( Partial_Sums seq2))) by Th28

 .= (( lim ( Partial_Sums seq1)) - ( lim ( Partial_Sums seq2))) by A1, COMSEQ_2: 26;

 hence thesis by A2, A3;

 end;

 registration

 let seq1,seq2 be summable Complex_Sequence;

 cluster (seq1 + seq2) -> summable;

 coherence by Th54;

 cluster (seq1 - seq2) -> summable;

 coherence by Th55;

 end

 theorem :: COMSEQ_3:56



 Th56: seq is summable implies for z be Complex holds (z (#) seq) is summable & ( Sum (z (#) seq)) = (z * ( Sum seq))

 proof

 assume

 A1: seq is summable;

 let z be Complex;



 A2: ( Partial_Sums (z (#) seq)) = (z (#) ( Partial_Sums seq)) by Th29;

 ( Sum (z (#) seq)) = ( lim (z (#) ( Partial_Sums seq))) by Th29

 .= (z * ( Sum seq)) by A1, COMSEQ_2: 18;

 hence thesis by A1, A2;

 end;

 registration

 let z be Element of COMPLEX , seq be summable Complex_Sequence;

 cluster (z (#) seq) -> summable;

 coherence by Th56;

 end

 theorem :: COMSEQ_3:57



 Th57: ( Re seq) is summable & ( Im seq) is summable implies seq is summable & ( Sum seq) = (( Sum ( Re seq)) + (( Sum ( Im seq)) * ))

 proof

 assume that

 A1: ( Re seq) is summable and

 A2: ( Im seq) is summable;

 ( Partial_Sums ( Im seq)) is convergent by A2;

 then

 A3: ( Im ( Partial_Sums seq)) is convergent by Th26;

 ( Partial_Sums ( Re seq)) is convergent by A1;

 then

 A4: ( Re ( Partial_Sums seq)) is convergent by Th26;

 then

 A5: ( lim ( Im ( Partial_Sums seq))) = ( Im ( lim ( Partial_Sums seq))) by A3, Th42;



 A6: ( lim ( Re ( Partial_Sums seq))) = ( lim ( Partial_Sums ( Re seq))) & ( lim ( Im ( Partial_Sums seq))) = ( lim ( Partial_Sums ( Im seq))) by Th26;

 ( Partial_Sums seq) is convergent & ( lim ( Re ( Partial_Sums seq))) = ( Re ( lim ( Partial_Sums seq))) by A4, A3, Th42;

 hence thesis by A6, A5, COMPLEX1: 13;

 end;

 theorem :: COMSEQ_3:58



 Th58: seq is summable implies for n holds (seq ^\ n) is summable

 proof

 assume

 A1: seq is summable;

 let n;



 A2: ( Re (seq ^\ n)) = (( Re seq) ^\ n) & ( Im (seq ^\ n)) = (( Im seq) ^\ n) by Th23;

 (( Re seq) ^\ n) is summable & (( Im seq) ^\ n) is summable by A1, SERIES_1: 12;

 hence (seq ^\ n) is summable by A2, Th57;

 end;

 registration

 let seq be summable Complex_Sequence, n be Nat;

 cluster (seq ^\ n) -> summable;

 coherence by Th58;

 end

 theorem :: COMSEQ_3:59

 (ex n st (seq ^\ n) is summable) implies seq is summable

 proof

 given n such that

 A1: (seq ^\ n) is summable;

 ( Im (seq ^\ n)) = (( Im seq) ^\ n) by Th23;

 then

 A2: ( Im seq) is summable by A1, SERIES_1: 13;

 ( Re (seq ^\ n)) = (( Re seq) ^\ n) by Th23;

 then ( Re seq) is summable by A1, SERIES_1: 13;

 hence thesis by A2, Th57;

 end;

 theorem :: COMSEQ_3:60

 seq is summable implies for n holds ( Sum seq) = ((( Partial_Sums seq) . n) + ( Sum (seq ^\ (n + 1))))

 proof

 assume

 A1: seq is summable;

 then ( Sum seq) = (( Sum ( Re seq)) + (( Sum ( Im seq)) * )) by Th53;

 then

 A2: ( Re ( Sum seq)) = ( Sum ( Re seq)) & ( Im ( Sum seq)) = ( Sum ( Im seq)) by COMPLEX1: 12;

 let n;



 A3: ( Sum (seq ^\ (n + 1))) = (( Sum ( Re (seq ^\ (n + 1)))) + (( Sum ( Im (seq ^\ (n + 1)))) * )) by A1, Th53;



 A4: ( Sum ( Im seq)) = ((( Partial_Sums ( Im seq)) . n) + ( Sum (( Im seq) ^\ (n + 1)))) by A1, SERIES_1: 15

 .= ((( Im ( Partial_Sums seq)) . n) + ( Sum (( Im seq) ^\ (n + 1)))) by Th26

 .= ((( Im ( Partial_Sums seq)) . n) + ( Sum ( Im (seq ^\ (n + 1))))) by Th23

 .= ((( Im ( Partial_Sums seq)) . n) + ( Im ( Sum (seq ^\ (n + 1))))) by A3, COMPLEX1: 12

 .= (( Im (( Partial_Sums seq) . n)) + ( Im ( Sum (seq ^\ (n + 1))))) by Def6

 .= ( Im ((( Partial_Sums seq) . n) + ( Sum (seq ^\ (n + 1))))) by COMPLEX1: 8;

 ( Sum ( Re seq)) = ((( Partial_Sums ( Re seq)) . n) + ( Sum (( Re seq) ^\ (n + 1)))) by A1, SERIES_1: 15

 .= ((( Re ( Partial_Sums seq)) . n) + ( Sum (( Re seq) ^\ (n + 1)))) by Th26

 .= ((( Re ( Partial_Sums seq)) . n) + ( Sum ( Re (seq ^\ (n + 1))))) by Th23

 .= ((( Re ( Partial_Sums seq)) . n) + ( Re ( Sum (seq ^\ (n + 1))))) by A3, COMPLEX1: 12

 .= (( Re (( Partial_Sums seq) . n)) + ( Re ( Sum (seq ^\ (n + 1))))) by Def5

 .= ( Re ((( Partial_Sums seq) . n) + ( Sum (seq ^\ (n + 1))))) by COMPLEX1: 8;

 hence thesis by A2, A4, COMPLEX1:def 3;

 end;

 theorem :: COMSEQ_3:61



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

 proof

 ( Partial_Sums |.seq.|) is bounded_above iff |.seq.| is summable;

 hence thesis;

 end;

 registration

 let seq be absolutely_summable Complex_Sequence;

 cluster ( Partial_Sums |.seq.|) -> bounded_above;

 coherence by Th61;

 end

 theorem :: COMSEQ_3:62



 Th62: seq is summable iff for p st 0 < p holds ex n st for m st n <= m holds |.((( Partial_Sums seq) . m) - (( Partial_Sums seq) . n)).| < p by Th46;

 theorem :: COMSEQ_3:63



 Th63: seq is absolutely_summable implies seq is summable

 proof

 assume

 A1: seq is absolutely_summable;

 now

 let p;

 assume 0 < p;

 then

 consider n such that

 A2: for m st n <= m holds |.((( Partial_Sums |.seq.|) . m) - (( Partial_Sums |.seq.|) . n)).| < p by A1, SEQ_4: 41;

 take n;

 let m;

 assume n <= m;

 then

 A3: |.((( Partial_Sums |.seq.|) . m) - (( Partial_Sums |.seq.|) . n)).| < p by A2;

 |.((( Partial_Sums seq) . m) - (( Partial_Sums seq) . n)).| <= |.((( Partial_Sums |.seq.|) . m) - (( Partial_Sums |.seq.|) . n)).| by Th31;

 hence |.((( Partial_Sums seq) . m) - (( Partial_Sums seq) . n)).| summable for Complex_Sequence;

 coherence by Th63;

 end

 registration

 cluster absolutely_summable for Complex_Sequence;

 existence

 proof

 set C = the absolutely_summable Complex_Sequence;

 take C;

 thus thesis;

 end;

 end

 theorem :: COMSEQ_3:64



 Th64: |.z.| < 1 implies (z GeoSeq ) is summable & ( Sum (z GeoSeq )) = ( 1r / ( 1r - z))

 proof

 set seq2 = ( NAT --> 1r );

 deffunc f( Nat) = (z |^ ($1 + 1));

 consider seq1 such that

 A1: for n holds (seq1 . n) = f(n) from COMSEQ_1:sch 1;

 assume

 A2: |.z.| < 1;

 then

 A3: ( lim seq1) = 0c by A1, Th44;

 A4:

 now

 let n be Element of NAT ;



 thus (( Partial_Sums (z GeoSeq )) . n) = (( 1r - (z |^ (n + 1))) / ( 1r - z)) by A2, Th36, COMPLEX1: 48

 .= (( 1r - (seq1 . n)) / ( 1r - z)) by A1

 .= (( 1r * ((seq2 . n) - (seq1 . n))) / ( 1r - z)) by COMPLEX1:def 4, FUNCOP_1: 7

 .= (( 1r / ( 1r - z)) * ((seq2 . n) + ( - (seq1 . n)))) by XCMPLX_1: 74

 .= (( 1r / ( 1r - z)) * ((seq2 . n) + (( - seq1) . n))) by VALUED_1: 8

 .= (( 1r / ( 1r - z)) * ((seq2 - seq1) . n)) by VALUED_1: 1

 .= ((( 1r / ( 1r - z)) (#) (seq2 - seq1)) . n) by VALUED_1: 6;

 end;



 A5: for n holds (seq2 . n) = 1r by ORDINAL1:def 12, FUNCOP_1: 7;

 then

 A6: seq2 is convergent by COMSEQ_2: 9;



 A7: seq1 is convergent by A2, A1, Th44;

 then

 A8: (seq2 - seq1) is convergent by A6;

 hence ( Partial_Sums (z GeoSeq )) is convergent by A4, FUNCT_2: 63;

 ( lim (seq2 - seq1)) = (( lim seq2) - ( lim seq1)) by A7, A6, COMSEQ_2: 26

 .= 1r by A3, A5, COMSEQ_2: 10;



 then ( lim (( 1r / ( 1r - z)) (#) (seq2 - seq1))) = (( 1r / ( 1r - z)) * 1r ) by A8, COMSEQ_2: 18

 .= ( 1r / ( 1r - z)) by COMPLEX1:def 4;

 hence thesis by A4, FUNCT_2: 63;

 end;

 theorem :: COMSEQ_3:65

 |.z.| < 1 & (for n holds (seq . (n + 1)) = (z * (seq . n))) implies seq is summable & ( Sum seq) = ((seq . 0 ) / ( 1r - z))

 proof

 assume that

 A1: |.z.| < 1 and

 A2: for n holds (seq . (n + 1)) = (z * (seq . n));

 now

 let n be Element of NAT ;



 thus (( Partial_Sums seq) . n) = ((seq . 0 ) * (( 1r - (z |^ (n + 1))) / ( 1r - z))) by A1, A2, Th37, COMPLEX1: 48

 .= ((seq . 0 ) * (( Partial_Sums (z GeoSeq )) . n)) by A1, Th36, COMPLEX1: 48

 .= (((seq . 0 ) (#) ( Partial_Sums (z GeoSeq ))) . n) by VALUED_1: 6;

 end;

 then

 A3: ( Partial_Sums seq) = ((seq . 0 ) (#) ( Partial_Sums (z GeoSeq )));



 A4: (z GeoSeq ) is summable by A1, Th64;

 hence seq is summable by A3;

 ( Sum seq) = ((seq . 0 ) * ( Sum (z GeoSeq ))) by A3, A4, COMSEQ_2: 18

 .= ((seq . 0 ) * ( 1r / ( 1r - z))) by A1, Th64

 .= (((seq . 0 ) * 1r ) / ( 1r - z)) by XCMPLX_1: 74

 .= ((seq . 0 ) / ( 1r - z)) by COMPLEX1:def 4;

 hence thesis;

 end;

 theorem :: COMSEQ_3:66

 rseq1 is summable & (ex m st for n st m <= n holds |.(seq2 . n).| <= (rseq1 . n)) implies seq2 is absolutely_summable

 proof

 assume that

 A1: rseq1 is summable and

 A2: ex m st for n st m <= n holds |.(seq2 . n).| <= (rseq1 . n);

 consider m such that

 A3: for n st m <= n holds |.(seq2 . n).| <= (rseq1 . n) by A2;

 A4:

 now

 let n;

 |.(seq2 . n).| = ( |.seq2.| . n) by VALUED_1: 18;

 hence 0 <= ( |.seq2.| . n) by COMPLEX1: 46;

 end;

 now

 let n;

 assume m <= n;

 then |.(seq2 . n).| <= (rseq1 . n) by A3;

 hence ( |.seq2.| . n) <= (rseq1 . n) by VALUED_1: 18;

 end;

 hence |.seq2.| is summable by A1, A4, SERIES_1: 19;

 end;

 theorem :: COMSEQ_3:67

 (for n holds 0 <= ( |.seq1.| . n) & ( |.seq1.| . n) <= ( |.seq2.| . n)) & seq2 is absolutely_summable implies seq1 is absolutely_summable & ( Sum |.seq1.|) <= ( Sum |.seq2.|) by SERIES_1: 20;

 theorem :: COMSEQ_3:68

 (for n holds ( |.seq.| . n) > 0 ) & (ex m st for n st n >= m holds (( |.seq.| . (n + 1)) / ( |.seq.| . n)) >= 1) implies not seq is absolutely_summable by SERIES_1: 27;

 theorem :: COMSEQ_3:69

 (for n holds (rseq1 . n) = (n -root ( |.seq.| . n))) & rseq1 is convergent & ( lim rseq1) < 1 implies seq is absolutely_summable

 proof

 assume

 A1: (for n holds (rseq1 . n) = (n -root ( |.seq.| . n))) & rseq1 is convergent & ( lim rseq1) < 1;

 for n holds ( |.seq.| . n) >= 0 by Lm3;

 hence |.seq.| is summable by A1, SERIES_1: 28;

 end;

 theorem :: COMSEQ_3:70

 (for n holds (rseq1 . n) = (n -root ( |.seq.| . n))) & (ex m st for n st m <= n holds (rseq1 . n) >= 1) implies not |.seq.| is summable

 proof

 assume

 A1: (for n holds (rseq1 . n) = (n -root ( |.seq.| . n))) & ex m st for n st m <= n holds (rseq1 . n) >= 1;

 for n holds ( |.seq.| . n) >= 0 by Lm3;

 hence thesis by A1, SERIES_1: 29;

 end;

 theorem :: COMSEQ_3:71

 (for n holds (rseq1 . n) = (n -root ( |.seq.| . n))) & rseq1 is convergent & ( lim rseq1) > 1 implies not seq is absolutely_summable

 proof

 assume

 A1: (for n holds (rseq1 . n) = (n -root ( |.seq.| . n))) & rseq1 is convergent & ( lim rseq1) > 1;

 for n holds ( |.seq.| . n) >= 0 by Lm3;

 hence not |.seq.| is summable by A1, SERIES_1: 30;

 end;

 theorem :: COMSEQ_3:72

 |.seq.| is non-increasing & (for n holds (rseq1 . n) = ((2 to_power n) * ( |.seq.| . (2 to_power n)))) implies (seq is absolutely_summable iff rseq1 is summable)

 proof

 assume |.seq.| is non-increasing & for n holds (rseq1 . n) = ((2 to_power n) * ( |.seq.| . (2 to_power n)));

 then for n holds |.seq.| is non-increasing & ( |.seq.| . n) >= 0 & (rseq1 . n) = ((2 to_power n) * ( |.seq.| . (2 to_power n))) by Lm3;

 then |.seq.| is summable iff rseq1 is summable by SERIES_1: 31;

 hence thesis;

 end;

 theorem :: COMSEQ_3:73

 p > 1 & (for n st n >= 1 holds ( |.seq.| . n) = (1 / (n to_power p))) implies seq is absolutely_summable by SERIES_1: 32;

 theorem :: COMSEQ_3:74

 p <= 1 & (for n st n >= 1 holds ( |.seq.| . n) = (1 / (n to_power p))) implies not seq is absolutely_summable by SERIES_1: 33;

 theorem :: COMSEQ_3:75

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

 proof

 assume that

 A1: for n holds (seq . n) <> 0c & (rseq1 . n) = (( |.seq.| . (n + 1)) / ( |.seq.| . n)) and

 A2: rseq1 is convergent & ( lim rseq1) < 1;

 now

 let n;



 A3: (seq . n) <> 0c & ( |.seq.| . n) = |.(seq . n).| by A1, VALUED_1: 18;

 hence ( |.seq.| . n) <> 0 & (rseq1 . n) = (( |.seq.| . (n + 1)) / ( |.seq.| . n)) by A1, COMPLEX1: 47;

 thus ( |.seq.| . n) <> 0 & (rseq1 . n) = (( |. |.seq.|.| . (n + 1)) / ( |.seq.| . n)) by A1, A3, COMPLEX1: 47;

 thus ( |.seq.| . n) <> 0 & (rseq1 . n) = ((( abs |.seq.|) . (n + 1)) / (( abs |.seq.|) . n)) by A1, A3, COMPLEX1: 47;

 end;

 then |.seq.| is absolutely_summable by A2, SERIES_1: 37;

 hence thesis;

 end;

 theorem :: COMSEQ_3:76

 (for n holds (seq . n) <> 0c ) & (ex m st for n st n >= m holds (( |.seq.| . (n + 1)) / ( |.seq.| . n)) >= 1) implies not seq is absolutely_summable

 proof

 assume that

 A1: for n holds (seq . n) <> 0c and

 A2: ex m st for n st n >= m holds (( |.seq.| . (n + 1)) / ( |.seq.| . n)) >= 1;

 consider m such that

 A3: for n st n >= m holds (( |.seq.| . (n + 1)) / ( |.seq.| . n)) >= 1 by A2;

 A4:

 now

 let n;

 (seq . n) <> 0c by A1;

 then |.(seq . n).| <> 0 by COMPLEX1: 47;

 hence ( |.seq.| . n) <> 0 by VALUED_1: 18;

 end;

 for n st n >= m holds ((( abs |.seq.|) . (n + 1)) / (( abs |.seq.|) . n)) >= 1 by A3;

 hence not |.seq.| is summable by A4, SERIES_1: 39;

 end;