### The Mizar article:

### Convergence and the Limit of Complex Sequences. Series

**by****Yasunari Shidama, and****Artur Kornilowicz**

- Received June 25, 1997
Copyright (c) 1997 Association of Mizar Users

- MML identifier: COMSEQ_3
- [ MML identifier index ]

environ vocabulary SEQ_1, COMSEQ_1, COMPLEX1, FUNCT_1, SERIES_1, ABSVALUE, ARYTM, ARYTM_1, SUPINF_2, SEQ_2, ARYTM_3, PROB_1, ORDINAL2, SEQM_3, PREPOWER, SQUARE_1, RLVECT_1, RELAT_1, POWER, LATTICES; notation SUBSET_1, ORDINAL1, NUMBERS, ARYTM_0, XCMPLX_0, XREAL_0, REAL_1, RELAT_1, FUNCT_2, SEQ_1, SEQ_2, NAT_1, SEQM_3, ABSVALUE, SERIES_1, COMPLEX1, COMSEQ_1, COMSEQ_2, SQUARE_1, POWER; constructors SEQ_2, SEQM_3, SERIES_1, SQUARE_1, COMSEQ_1, COMSEQ_2, REAL_1, NAT_1, ABSVALUE, PARTFUN1, COMPLEX1, MEMBERED, ARYTM_0, ARYTM_3, FUNCT_4; clusters XREAL_0, COMSEQ_2, SEQ_1, COMSEQ_1, RELSET_1, SEQM_3, NAT_1, COMPLEX1, MEMBERED, ORDINAL2; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; definitions SEQ_2, COMSEQ_2, SERIES_1; theorems AXIOMS, NAT_1, REAL_1, ABSVALUE, SEQ_1, SEQ_2, SERIES_1, SEQM_3, SEQ_4, POWER, COMPLEX1, COMSEQ_1, COMSEQ_2, SQUARE_1, FUNCT_2, XREAL_0, XCMPLX_0, XCMPLX_1, ARYTM_0; schemes NAT_1, SEQ_1, COMSEQ_1, RECDEF_1; begin :: Preliminaries 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; L0: 0c = [*0,0*] by ARYTM_0:def 7; theorem [*(n+1),0*] <> 0c & [*0,(n+1)*] <> 0c by ARYTM_0:12,L0; theorem Th2: (for n holds rseq.n = 0) implies for m holds (Partial_Sums abs(rseq)).m = 0 proof assume A1: for n holds rseq.n = 0; let m; defpred P[Nat] means abs(rseq).$1 = (Partial_Sums abs(rseq)).$1; A2: P[0] by SERIES_1:def 1; A3: for k st P[k] holds P[k+1] proof let k be Nat such that A4: P[k]; thus abs(rseq).(k+1) = 0 + abs(rseq).(k+1) .= abs(0) + abs(rseq).(k+1) by ABSVALUE:def 1 .= abs(rseq.k) + abs(rseq).(k+1) by A1 .= (Partial_Sums abs(rseq)).k + abs(rseq).(k+1) by A4,SEQ_1:16 .= (Partial_Sums abs(rseq)).(k+1) by SERIES_1:def 1; end; for n holds P[n] from Ind(A2,A3); hence (Partial_Sums abs(rseq)).m = abs(rseq).m .= abs(rseq.m) by SEQ_1:16 .= abs(0) by A1 .= 0 by ABSVALUE:def 1; end; theorem 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 number such that A2: 0<p; take 0; let m be Nat such that 0<=m; abs((Partial_Sums abs(rseq)).m-0) = abs(0-0) by A1,Th2 .= 0 by ABSVALUE:def 1; hence abs((Partial_Sums abs(rseq)).m-0)<p by A2; end; deffunc f(set) = 0; definition cluster absolutely_summable Real_Sequence; existence proof consider C being Real_Sequence such that A1: for n being Nat holds C.n = f(n) from ExRealSeq; take C; thus thesis by A1,Th3; end; end; definition cluster summable -> convergent Real_Sequence; coherence by SERIES_1:7; end; definition cluster absolutely_summable -> summable Real_Sequence; coherence by SERIES_1:40; end; definition cluster absolutely_summable Real_Sequence; existence proof consider R being absolutely_summable Real_Sequence; take R; thus thesis; end; end; theorem rseq is convergent implies (for p st 0<p ex n st for m,l be Nat st n <= m & n <= l holds abs(rseq.m-rseq.l)<p) proof assume A1:rseq is convergent; let p; assume 0<p; then 0<p/2 by SEQ_2:3; then consider n such that A2: for m st n <= m holds abs(rseq.m-rseq.n)<p/2 by A1,SEQ_4:58; take n; now let m,l be Nat; assume A3:n <= m & n <= l; then A4:abs(rseq.m-rseq.n)<p/2 by A2; abs(rseq.l-rseq.n)<p/2 by A2,A3; then abs(rseq.m-rseq.n)+abs(rseq.l-rseq.n) < p/2+p/2 by A4,REAL_1:67; then A5:abs(rseq.m-rseq.n)+abs(rseq.l-rseq.n) < p by XCMPLX_1:66; abs(rseq.m-rseq.l) = abs((rseq.m-rseq.n)-(rseq.l-rseq.n)) by XCMPLX_1:22; then abs(rseq.m-rseq.l) <= abs(rseq.m-rseq.n)+abs(rseq.l-rseq.n) by ABSVALUE:19; hence abs(rseq.m-rseq.l) < p by A5,AXIOMS:22; end; hence for m,l be Nat st n <= m & n <= l holds abs(rseq.m-rseq.l)<p; end; theorem (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; now let n; defpred P[Nat] means Partial_Sums(rseq).(n+$1)-Partial_Sums(rseq).n <= p * $1; Partial_Sums(rseq).(n+0)-Partial_Sums(rseq).n =Partial_Sums(rseq).n+-Partial_Sums(rseq).n by XCMPLX_0:def 8 .=p * 0 by XCMPLX_0:def 6; then A2: P[0]; A3: now let l be Nat such that A4: P[l]; A5: Partial_Sums(rseq).(n+(l+1))-Partial_Sums(rseq).n =Partial_Sums(rseq).((n+l)+1)-Partial_Sums(rseq).n by XCMPLX_1:1 .=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) by XCMPLX_1:29; A6: rseq.(n+l+1) <= p by A1; A7: Partial_Sums(rseq).(n+(l+1))-Partial_Sums(rseq).n <= p * l + rseq.(n+l+1) by A4,A5,AXIOMS:24; A8: p * l + rseq.(n+l+1) <= p * l + p by A6,AXIOMS:24; p * l + p=p * l + p * 1 .=p * (l+1) by XCMPLX_1:8; hence P[l+1] by A7,A8,AXIOMS:22; end; thus for l be Nat holds P[l] from Ind(A2,A3); end; hence thesis; end; theorem (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; Partial_Sums(rseq).(0) =rseq.0 by SERIES_1:def 1; then A2:P[0] by A1; A3: now let n be Nat such that A4: P[n]; A5: Partial_Sums(rseq).(n+1) =Partial_Sums(rseq).(n)+rseq.(n+1) by SERIES_1:def 1; A6: rseq.(n+1) <= p by A1; A7: Partial_Sums(rseq).(n+1) <= p * (n+1) + rseq.(n+1) by A4,A5,AXIOMS:24; A8: p * (n+1)+ rseq.(n+1) <= p * (n+1) + p by A6,AXIOMS:24; p * (n+1) + p=p * (n+1) + p * 1 .=p * ((n+1)+1) by XCMPLX_1:8; hence P[n+1] by A7,A8,AXIOMS:22; end; thus for n be Nat holds P[n] from Ind(A2,A3); end; theorem (for n st n <= m holds rseq1.n <= p * rseq2.n) implies Partial_Sums(rseq1).m <= p * Partial_Sums(rseq2).m proof assume A1: for n st n <= m holds rseq1.n <= p * rseq2.n; defpred P[Nat] means $1 <= m implies Partial_Sums(rseq1).$1 <= p * Partial_Sums(rseq2).$1; A2: P[0] proof assume A3: 0 <= m; A4: Partial_Sums(rseq1).(0) =rseq1.0 by SERIES_1:def 1; p * Partial_Sums(rseq2).(0) =p * rseq2.0 by SERIES_1:def 1; hence thesis by A1,A3,A4; end; A5: now let n be Nat such that A6: P[n]; now assume A7: n + 1 <= m; A8: n < n+1 by REAL_1:69; A9: Partial_Sums(rseq1).(n+1) =Partial_Sums(rseq1).(n)+rseq1.(n+1) by SERIES_1:def 1; A10: rseq1.(n+1) <= p * rseq2.(n+1) by A1,A7; A11: Partial_Sums(rseq1).(n+1) <= p * Partial_Sums(rseq2).(n) + rseq1.(n+1) by A6,A7,A8,A9,AXIOMS:22,24; A12: p * Partial_Sums(rseq2).(n) + rseq1.(n+1) <= p * Partial_Sums(rseq2).(n) + p * rseq2.(n+1) by A10,AXIOMS:24; p * Partial_Sums(rseq2).(n) + p * rseq2.(n+1) =p * (Partial_Sums(rseq2).(n) +rseq2.(n+1)) by XCMPLX_1:8 .=p * Partial_Sums(rseq2).(n+1) by SERIES_1:def 1; hence Partial_Sums(rseq1).(n+1) <= p * Partial_Sums(rseq2).(n+1) by A11,A12,AXIOMS:22; end; hence P[n+1]; end; for n be Nat holds P[n] from Ind(A2,A5); hence Partial_Sums(rseq1).(m) <= p * Partial_Sums(rseq2).(m); end; theorem (for n st n <= m holds rseq1.n <= p * rseq2.n) implies for n st n <= m 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 such that n <= m; 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: P[0] proof assume n+0 <= m; A3: Partial_Sums(rseq1).(n+0)-Partial_Sums(rseq1).(n) =Partial_Sums(rseq1).(n)+-Partial_Sums(rseq1).(n) by XCMPLX_0:def 8 .=0 by XCMPLX_0:def 6; p *( Partial_Sums(rseq2).(n+0)-Partial_Sums(rseq2).(n)) =p * (Partial_Sums(rseq2).(n)+-Partial_Sums(rseq2).(n)) by XCMPLX_0: def 8 .=p * 0 by XCMPLX_0:def 6; hence thesis by A3; end; A4: for l be Nat st P[l] holds P[l+1] proof let l be Nat such that A5: P[l]; assume n + (l+1) <= m; then A6: n+l+1 <= m by XCMPLX_1:1; A7: n+l < (n+l)+1 by REAL_1:69; A8: Partial_Sums(rseq1).(n+(l+1)) =Partial_Sums(rseq1).(n+l+1) by XCMPLX_1:1 .=Partial_Sums(rseq1).(n+l)+rseq1.(n+l+1) by SERIES_1:def 1; rseq1.(n+l+1) <= p * rseq2.(n+l+1) by A1,A6; then Partial_Sums(rseq1).(n+(l+1)) <= Partial_Sums(rseq1).(n+l) + p * rseq2.(n+l+1) by A8,AXIOMS:24; then A9: 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 REAL_1:49; A10: Partial_Sums(rseq1).(n+l) + p * rseq2.(n+l+1) -Partial_Sums(rseq1).n = Partial_Sums(rseq1).(n+l) -Partial_Sums(rseq1).n + p * rseq2.(n+l+1) by XCMPLX_1:29; A11: 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 A5,A6,A7,AXIOMS:22,24; p * (Partial_Sums(rseq2).(n+l)-Partial_Sums(rseq2).n) + p * rseq2.(n+l+1) = p * (Partial_Sums(rseq2).(n+l)-Partial_Sums(rseq2).n + rseq2.(n+l+1)) by XCMPLX_1:8 .= p * (Partial_Sums(rseq2).(n+l)+rseq2.(n+l+1) -Partial_Sums(rseq2).n) by XCMPLX_1:29 .=p * (Partial_Sums(rseq2).((n+l)+1) -Partial_Sums(rseq2).n) by SERIES_1:def 1 .=p * (Partial_Sums(rseq2).(n+(l+1)) -Partial_Sums(rseq2).n) by XCMPLX_1:1; hence thesis by A9,A10,A11,AXIOMS:22; end; thus for l be Nat holds P[l] from Ind(A2,A4); end; theorem (for n holds 0 <= rseq.n) implies (for n, m st n <= m holds abs(Partial_Sums(rseq).m-Partial_Sums(rseq).n) =Partial_Sums(rseq).m-Partial_Sums(rseq).n) & for n holds abs(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:19; A3: now let n,m; assume n <= m; then Partial_Sums(rseq).n <= Partial_Sums(rseq).m by A2,SEQM_3:12; then Partial_Sums(rseq).n-Partial_Sums(rseq).n <= Partial_Sums(rseq).m-Partial_Sums(rseq).n by REAL_1:49; then 0 <= Partial_Sums(rseq).m-Partial_Sums(rseq).n by XCMPLX_1:14; hence abs(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 = rseq.0 by SERIES_1:def 1; A5:0 <= rseq.0 by A1; 0 <= n by NAT_1:18; then Partial_Sums(rseq).0 <= Partial_Sums(rseq).n by A2,SEQM_3:12; hence abs(Partial_Sums(rseq).n)=Partial_Sums(rseq).n by A4,A5,ABSVALUE:def 1; end; hence thesis by A3; end; theorem seq1 is convergent & seq2 is convergent & lim(seq1-seq2)=0c implies lim seq1 = lim seq2 proof assume A1: seq1 is convergent & seq2 is convergent & lim(seq1-seq2)=0c; then lim(seq1-seq2)=lim(seq1)-lim(seq2) by COMSEQ_2:26; hence lim(seq1)=lim(seq2) by A1,XCMPLX_1:15; end; begin :: The Operations on Complex Sequences reserve z for Element of COMPLEX; reserve Nseq,Nseq1 for increasing Seq_of_Nat; Lm1: |.seq.n.|=|.seq.|.n & 0 <= |.seq.|.n proof |.seq.n.|=|.seq.|.n by COMSEQ_1:def 14; hence thesis by COMPLEX1:132; end; definition let z be Element of COMPLEX; func z GeoSeq -> Complex_Sequence means :Def1: it.0 = 1r & for n holds it.(n+1) = it.n * z; existence proof deffunc f(set,Element of COMPLEX) = $2*z; consider f being Function of NAT,COMPLEX such that A1: f.0 = 1r & for n being Nat holds f.(n+1) = f(n,f.n) from LambdaRecExD; take f; thus thesis by A1; end; uniqueness proof let seq1,seq2; assume that A2: seq1.0=1r & for n holds seq1.(n+1)=seq1.n * z and A3: seq2.0=1r & for n holds seq2.(n+1)=seq2.n * z; defpred P[Nat] means seq1.$1 = seq2.$1; A4: P[0] by A2,A3; A5: 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 A2 .= seq2.(k+1) by A3; end; for n holds P[n] from Ind(A4,A5); hence seq1 = seq2 by COMSEQ_1:6; end; end; definition let z be Element of COMPLEX, n be Nat; func z #N n -> Element of COMPLEX equals:Def2: z GeoSeq.n; correctness; end; theorem z #N 0 = 1r proof thus z #N 0 = (z GeoSeq).0 by Def2 .= 1r by Def1; end; definition let c be Complex_Sequence; func Re c -> Real_Sequence means :Def3: for n holds it.n = Re(c.n); existence proof deffunc f(Nat) = Re(c.$1); thus ex f being Real_Sequence st for n holds f.n = f(n) from ExRealSeq; end; uniqueness proof let seq,seq' be Real_Sequence such that A1: for n holds seq.n=Re(c.n) and A2: for n holds seq'.n=Re(c.n); now let n; seq.n=Re(c.n) & seq'.n=Re(c.n) by A1,A2; hence seq.n=seq'.n; end; hence seq=seq' by FUNCT_2:113; end; end; definition let c be Complex_Sequence; func Im c -> Real_Sequence means :Def4: for n holds it.n = Im(c.n); existence proof deffunc f(Nat) = Im(c.$1); thus ex f being Real_Sequence st for n holds f.n = f(n) from ExRealSeq; end; uniqueness proof let seq,seq' be Real_Sequence such that A1: for n holds seq.n=Im(c.n) and A2: for n holds seq'.n=Im(c.n); now let n; seq.n=Im(c.n) & seq'.n=Im(c.n) by A1,A2; hence seq.n=seq'.n; end; hence seq=seq' by FUNCT_2:113; end; end; theorem Th12: |.z.| <= abs Re z + abs Im z proof A1:z = [*Re z, Im z*] by COMPLEX1:8; A2:Re([*Re z,0*])=Re z by COMPLEX1:7; A3:Im([*Re z,0*])=0 by COMPLEX1:7; A4:Re([*0,Im z*])=0 by COMPLEX1:7; A5:Im([*0,Im z*])=Im z by COMPLEX1:7; [*Re z,0*] +[*0,Im z*] =[*Re ([*Re z,0*])+Re([*0,Im z*]), Im ([*Re z,0*])+Im([*0,Im z*])*] by COMPLEX1:def 9 .=[*Re z ,Im z*] by A3,A4,A5,COMPLEX1:7; then A6: |.z.| <= |.[*Re z,0*].| +|.[*0,Im z*].| by A1,COMPLEX1:142; |.[*Re z,0*].| = abs(Re z) by A2,A3,COMPLEX1:136; hence thesis by A4,A5,A6,COMPLEX1:137; end; theorem Th13: abs(Re z) <= |.z.| & abs(Im z) <= |.z.| proof A1:|.z.| = sqrt ((Re z)^2 + (Im z)^2) by COMPLEX1:def 16; A2:0 <= (Re z)^2 by SQUARE_1:72; 0 <= (Im z)^2 by SQUARE_1:72; then 0+(Re z)^2 <= (Im z)^2 + (Re z)^2 by AXIOMS:24; then A3:0 <= (Re z)^2 & (Re z)^2 <= (Re z)^2 + (Im z)^2 by SQUARE_1:72; 0+(Im z)^2 <= (Re z)^2 + (Im z)^2 by A2,AXIOMS:24; then A4:0 <= (Im z)^2 & (Im z)^2 <= (Re z)^2 + (Im z)^2 by SQUARE_1:72; A5:sqrt((Re z)^2) <= sqrt((Re z)^2 + (Im z)^2) by A3,SQUARE_1:94; sqrt((Im z)^2) <= sqrt((Re z)^2 + (Im z)^2) by A4,SQUARE_1:94; hence thesis by A1,A5,SQUARE_1:91; end; theorem Th14: Re seq1=Re seq2 & Im seq1=Im seq2 implies seq1=seq2 proof assume A1: Re seq1=Re seq2 & Im seq1=Im seq2; now let n; A2:Re(seq1.n)=Re seq2.n by A1,Def3 .=Re(seq2.n) by Def3; Im(seq1.n)=Im seq2.n by A1,Def4 .=Im(seq2.n) by Def4; hence seq1.n=seq2.n by A2,COMPLEX1:9; end; hence seq1=seq2 by COMSEQ_1:6; end; theorem Th15: Re seq1 + Re seq2 = Re (seq1+seq2) & Im seq1 + Im seq2 = Im (seq1+seq2) proof now let n; thus (Re seq1+Re seq2).n=Re seq1.n+Re seq2.n by SEQ_1:11 .=Re(seq1.n)+Re seq2.n by Def3 .=Re(seq1.n)+Re(seq2.n) by Def3 .=Re(seq1.n+seq2.n) by COMPLEX1:19 .=Re((seq1+seq2).n) by COMSEQ_1:def 4 .=Re (seq1+seq2).n by Def3; end; hence Re seq1+Re seq2=Re (seq1+seq2) by FUNCT_2:113; now let n; thus (Im seq1+Im seq2).n=Im seq1.n+Im seq2.n by SEQ_1:11 .=Im(seq1.n)+Im seq2.n by Def4 .=Im(seq1.n)+Im(seq2.n) by Def4 .=Im(seq1.n+seq2.n) by COMPLEX1:19 .=Im((seq1+seq2).n) by COMSEQ_1:def 4 .=Im (seq1+seq2).n by Def4; end; hence Im seq1+Im seq2=Im (seq1+seq2) by FUNCT_2:113; end; theorem Th16: -(Re seq) = Re (-seq) & -(Im seq) = Im -seq proof now let n; thus (-Re seq).n= -(Re seq.n) by SEQ_1:14 .=-Re(seq.n) by Def3 .= Re(-(seq.n)) by COMPLEX1:34 .= Re((-seq).n) by COMSEQ_1:def 9 .=Re (-seq).n by Def3; end; hence -Re seq=Re (-seq) by FUNCT_2:113; now let n; thus (-Im seq).n=-Im seq.n by SEQ_1:14 .=-Im(seq.n) by Def4 .= Im(-(seq.n)) by COMPLEX1:34 .= Im((-seq).n) by COMSEQ_1:def 9 .=(Im -seq).n by Def4; end; hence -Im seq=Im -seq by FUNCT_2:113; end; theorem Th17: r*Re(z)=Re([*r,0*]*z) & r*Im(z)=Im([*r,0*]*z) proof set zr=[*r,0*]; A1:Re(zr)=r &Im(zr)=0 by COMPLEX1:7; [*r,0*]*z=[*Re(zr) * Re z - Im(zr) * Im z,Re(zr) * Im z + Re z * Im zr *] by COMPLEX1:def 10 .= [*r * Re z,r * Im z*] by A1; hence thesis by COMPLEX1:7; end; theorem Th18: Re seq1-Re seq2=Re (seq1-seq2) & Im seq1-Im seq2=Im(seq1-seq2) proof now let n; thus (Re seq1-Re seq2).n = (Re seq1+-Re seq2).n by SEQ_1:15 .= Re seq1.n+(-Re seq2).n by SEQ_1:11 .=Re seq1.n+(Re -seq2).n by Th16 .=(Re seq1+Re -seq2).n by SEQ_1:11 .=Re (seq1+(-seq2)).n by Th15 .=Re (seq1-seq2).n by COMSEQ_1:def 10; end; hence Re seq1-Re seq2=Re (seq1-seq2) by FUNCT_2:113; now let n; thus (Im seq1-Im seq2).n = (Im seq1+-Im seq2).n by SEQ_1:15 .= Im seq1.n+(-Im seq2).n by SEQ_1:11 .=Im seq1.n+Im (-seq2).n by Th16 .=(Im seq1+Im -seq2).n by SEQ_1:11 .=Im (seq1+ -seq2).n by Th15 .=Im(seq1-seq2).n by COMSEQ_1:def 10; end; hence Im seq1-Im seq2=Im(seq1-seq2) by FUNCT_2:113; end; theorem r(#)Re seq = Re ([*r,0*] (#) seq) & r(#)Im seq = Im ([*r,0*] (#) seq) proof now let n; thus (r(#)Re seq).n= r*(Re seq.n) by SEQ_1:13 .=r*Re(seq.n) by Def3 .=Re([*r,0*]*(seq.n)) by Th17 .=Re(([*r,0*] (#) seq).n) by COMSEQ_1:def 7 .=Re ([*r,0*] (#) seq).n by Def3; end; hence r(#)Re seq=Re ([*r,0*] (#) seq) by FUNCT_2:113; now let n; thus (r(#)Im seq).n= r*(Im seq.n) by SEQ_1:13 .=r*Im(seq.n) by Def4 .=Im([*r,0*]*(seq.n)) by Th17 .=Im(([*r,0*] (#) seq).n) by COMSEQ_1:def 7 .=Im([*r,0*](#)seq).n by Def4; end; hence r(#)Im seq=Im([*r,0*](#)seq) by FUNCT_2:113; end; theorem 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; thus Re (z (#) seq).n=Re((z (#) seq).n) by Def3 .=Re((z * seq.n )) by COMSEQ_1:def 7 .=Re([*Re(z) * Re(seq.n) - Im(z) * Im(seq.n), Re(z) * Im(seq.n) + Re(seq.n) * Im(z)*]) by COMPLEX1:def 10 .= Re(z) * Re(seq.n) - Im(z) * Im(seq.n) by COMPLEX1:7 .= Re(z) *( Re seq.n) - Im(z) * Im(seq.n) by Def3 .= Re(z) *( Re seq.n) - Im(z) *( Im seq.n) by Def4 .= (Re(z) (#) Re seq).n - Im(z) *( Im seq.n) by SEQ_1:13 .= (Re(z) (#) Re seq).n - (Im(z) (#) Im seq).n by SEQ_1:13 .= (Re(z) (#) Re seq).n + (- (Im(z) (#) Im seq).n) by XCMPLX_0:def 8 .= (Re(z) (#) Re seq).n + (- Im(z) (#) Im seq).n by SEQ_1:14 .= (Re(z) (#) Re seq +(- Im(z) (#) Im seq)).n by SEQ_1:11 .= (Re(z) (#) Re seq - Im(z) (#) Im seq).n by SEQ_1:15; end; hence Re (z (#) seq)=Re(z)(#)Re seq-Im(z)(#)Im seq by FUNCT_2:113; now let n; thus Im(z(#)seq).n =Im((z (#) seq).n) by Def4 .=Im((z * seq.n )) by COMSEQ_1:def 7 .=Im([*Re(z) * Re(seq.n) - Im(z) * Im(seq.n), Re(z) * Im(seq.n) + Re(seq.n) * Im(z)*]) by COMPLEX1:def 10 .= Re(z) * Im(seq.n) + Re(seq.n) * Im(z) by COMPLEX1:7 .= Re(z) * Im(seq.n) + Im(z) * Re seq.n by Def3 .= Re(z) * Im seq.n + Im(z) *( Re seq.n) by Def4 .= (Re(z) (#) Im seq).n + Im(z) *( Re seq.n) by SEQ_1:13 .= (Re(z) (#) Im seq).n + (Im(z) (#) Re seq).n by SEQ_1:13 .= (Re(z) (#) Im seq + Im(z) (#) Re seq).n by SEQ_1:11; end; hence Im(z(#)seq)=Re(z)(#)Im seq+Im(z)(#)Re seq by FUNCT_2:113; end; theorem 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; thus Re (seq1 (#) seq2).n=Re((seq1 (#) seq2).n) by Def3 .=Re((seq1.n * seq2.n )) by COMSEQ_1:def 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:def 10 .= Re(seq1.n) * Re(seq2.n) - Im(seq1.n) * Im(seq2.n) by COMPLEX1:7 .= (Re seq1.n) * Re(seq2.n) - Im(seq1.n) * Im(seq2.n) by Def3 .= (Re seq1.n) *( Re seq2.n) - Im(seq1.n) * Im(seq2.n) by Def3 .= (Re seq1.n) *( Re seq2.n) - Im(seq1.n) *( Im seq2.n) by Def4 .= (Re seq1.n) *( Re seq2.n) - (Im seq1.n)*( Im seq2.n) by Def4 .= (Re seq1 (#) Re seq2).n - (Im seq1.n) *( Im seq2.n) by SEQ_1:12 .= (Re seq1 (#) Re seq2).n - (Im seq1 (#) Im seq2).n by SEQ_1:12 .= (Re seq1 (#)Re seq2).n + (- (Im seq1 (#) Im seq2).n) by XCMPLX_0:def 8 .= (Re seq1 (#) Re seq2).n + (- Im seq1 (#) Im seq2).n by SEQ_1:14 .= (Re seq1 (#) Re seq2 +(- Im seq1 (#) Im seq2)).n by SEQ_1:11 .= (Re seq1 (#) Re seq2 - Im seq1 (#) Im seq2).n by SEQ_1:15; end; hence Re (seq1 (#) seq2)=Re seq1(#)Re seq2-Im seq1(#)Im seq2 by FUNCT_2:113 ; now let n; thus Im (seq1 (#) seq2).n =Im((seq1 (#) seq2).n) by Def4 .=Im((seq1.n * seq2.n )) by COMSEQ_1:def 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:def 10 .= Re(seq1.n) * Im(seq2.n) + Re(seq2.n) * Im(seq1.n) by COMPLEX1:7 .= Re(seq1.n) * Im(seq2.n) + Im(seq1.n) * Re seq2.n by Def3 .= Re seq1.n * Im(seq2.n) + Im(seq1.n) * Re seq2.n by Def3 .= Re seq1.n * Im seq2.n + Im(seq1.n) * Re seq2.n by Def4 .= (Re seq1.n * Im seq2.n) + (Im seq1.n * Re seq2.n) by Def4 .= (Re seq1 (#) Im seq2).n + Im seq1.n *( Re seq2.n) by SEQ_1:12 .= (Re seq1 (#) Im seq2).n + (Im seq1 (#) Re seq2).n by SEQ_1:12 .= (Re seq1 (#) Im seq2 + Im seq1 (#) Re seq2).n by SEQ_1:11; end; hence Im (seq1 (#) seq2)=Re seq1(#)Im seq2+Im seq1(#)Re seq2 by FUNCT_2:113; end; definition let seq be Complex_Sequence, Nseq be increasing Seq_of_Nat; func seq (#) Nseq -> Complex_Sequence means :Def5: for n holds it.n = seq.(Nseq.n); existence proof deffunc f(Nat) = seq.(Nseq.$1); thus ex f being Complex_Sequence st for n holds f.n = f(n) from ExComplexSeq; end; uniqueness proof let seq1,seq2 be Complex_Sequence such that A1: for n holds seq1.n= seq.(Nseq.n) and A2: for n holds seq2.n=seq.(Nseq.n); now let n; seq1.n=seq.(Nseq.n) & seq2.n=seq.(Nseq.n) by A1,A2; hence seq1.n=seq2.n; end; hence seq1=seq2 by COMSEQ_1:6; end; end; theorem Th22: Re (seq(#)Nseq)=(Re seq)*Nseq & Im (seq(#)Nseq)=(Im seq)*Nseq proof now let n; thus (Re (seq(#)Nseq)).n =Re((seq(#)Nseq).n) by Def3 .=Re(seq.(Nseq.n)) by Def5 .=Re seq.(Nseq.n) by Def3 .=(Re seq*Nseq).n by SEQM_3:31; end; hence Re (seq(#)Nseq)=Re seq*Nseq by FUNCT_2:113; now let n; thus Im (seq(#)Nseq).n =Im((seq(#)Nseq).n) by Def4 .=Im(seq.(Nseq.n)) by Def5 .=Im seq.(Nseq.n) by Def4 .=(Im seq*Nseq).n by SEQM_3:31; end; hence Im (seq(#)Nseq)=Im seq*Nseq by FUNCT_2:113; end; definition let seq be Complex_Sequence, k be Nat; func seq ^\ k -> Complex_Sequence means :Def6: for n holds it.n=seq.(n+k); existence proof deffunc f(Nat) = seq.($1+k); thus ex f being Complex_Sequence st for n holds f.n = f(n) from ExComplexSeq; end; uniqueness proof let seq1,seq2; assume that A1:for n holds seq1.n=seq.(n+k) and A2:for n holds seq2.n=seq.(n+k); now let n; seq1.n=seq.(n+k) & seq2.n=seq.(n+k) by A1,A2; hence seq1.n=seq2.n; end; hence seq1=seq2 by COMSEQ_1:6; end; end; theorem Th23: (Re seq)^\k =Re (seq^\k) & (Im seq)^\k =Im (seq^\k) proof now let n; thus (Re seq^\k).n =Re seq.(n+k) by SEQM_3:def 9 .=Re(seq.(n+k)) by Def3 .=Re((seq^\k).n) by Def6 .=Re ((seq)^\k).n by Def3; thus (Im seq^\k).n =Im seq.(n+k) by SEQM_3:def 9 .=Im(seq.(n+k)) by Def4 .=Im((seq^\k).n) by Def6 .=Im ((seq)^\k).n by Def4; end; hence (Re seq)^\k =Re ((seq)^\k) & (Im seq)^\k =Im ((seq)^\k) by FUNCT_2:113; end; definition let seq be Complex_Sequence; func Partial_Sums seq -> Complex_Sequence means :Def7: it.0 = seq.0 & for n holds it.(n+1) = it.n + seq.(n+1); existence proof deffunc f(Nat,Element of COMPLEX) = $2 + seq.($1+1); consider f being Function of NAT,COMPLEX such that A1: f.0 = seq.0 & for n being Nat holds f.(n+1) = f(n,f.n) from LambdaRecExD; take f; thus thesis by A1; end; uniqueness proof let seq1,seq2; assume that A2: seq1.0=seq.0 & for n holds seq1.(n+1)=seq1.n + seq.(n+1) and A3: seq2.0=seq.0 & for n holds seq2.(n+1)=seq2.n + seq.(n+1); defpred P[Nat] means seq1.$1 = seq2.$1; A4: P[0] by A2,A3; A5: 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 + seq.(k+1) by A2 .= seq2.(k+1) by A3; end; for n holds P[n] from Ind(A4,A5); hence seq1 = seq2 by COMSEQ_1:6; end; end; definition let seq be Complex_Sequence; func Sum seq -> Element of COMPLEX equals :Def8: lim Partial_Sums seq; correctness; end; theorem Th24: (for n holds seq.n = 0c) implies for m holds (Partial_Sums seq).m = 0c proof assume A1: for n holds seq.n = 0c; let m; defpred P[Nat] means seq.$1 = (Partial_Sums seq).$1; A2: P[0] by Def7; A3: for k st P[k] holds P[k+1] proof let k be Nat such that A4: P[k]; thus seq.(k+1) = 0c + seq.(k+1) by COMPLEX1:22 .= (Partial_Sums seq).k + seq.(k+1) by A1,A4 .= (Partial_Sums seq).(k+1) by Def7; end; for n holds P[n] from Ind(A2,A3); then seq = Partial_Sums seq by COMSEQ_1:6; hence (Partial_Sums seq).m = 0c by A1; end; theorem Th25: (for n holds seq.n = 0c) implies for m holds (Partial_Sums |.seq.|).m = 0 proof assume A1: for n holds seq.n = 0c; let m; defpred P[Nat] means |.seq.|.$1 = (Partial_Sums |.seq.|).$1; A2: P[0] by SERIES_1:def 1; A3: for k st P[k] holds P[k+1] proof let k be Nat such that A4: P[k]; thus |.seq.|.(k+1) = |.0c.| + |.seq.|.(k+1) by COMPLEX1:130 .= |.seq.k.| + |.seq.|.(k+1) by A1 .= (Partial_Sums |.seq.|).k + |.seq.|.(k+1) by A4, COMSEQ_1:def 14 .= (Partial_Sums |.seq.|).(k+1) by SERIES_1:def 1; end; for n holds P[n] from Ind(A2,A3); hence (Partial_Sums |.seq.|).m = |.seq.|.m .= |.seq.m.| by COMSEQ_1:def 14 .= 0 by A1,COMPLEX1:130; end; theorem 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; A1:P[0] proof thus Partial_Sums(Re seq).0 = Re seq.0 by SERIES_1:def 1 .= Re(seq.0) by Def3 .= Re(Partial_Sums(seq).0) by Def7 .= Re Partial_Sums(seq).0 by Def3; end; A2: 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 Def3 .=Re(Partial_Sums(seq).k) +Re(seq.(k+1)) by Def3 .=Re(Partial_Sums(seq).k + seq.(k+1)) by COMPLEX1:19 .=Re(Partial_Sums(seq).(k+1)) by Def7 .=Re Partial_Sums(seq).(k+1) by Def3; hence thesis; end; A3:for n holds P[n] from Ind(A1,A2); defpred R[Nat] means Partial_Sums(Im seq).$1 = Im Partial_Sums(seq).$1; A4:R[0] proof thus Partial_Sums(Im seq).0 = Im seq.0 by SERIES_1:def 1 .= Im(seq.0) by Def4 .= Im(Partial_Sums(seq).0) by Def7 .= Im Partial_Sums(seq).0 by Def4; end; A5: 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 Def4 .=Im(Partial_Sums(seq).k) +Im(seq.(k+1)) by Def4 .=Im(Partial_Sums(seq).k + seq.(k+1)) by COMPLEX1:19 .=Im(Partial_Sums(seq).(k+1)) by Def7 .=Im Partial_Sums(seq).(k+1) by Def4; hence thesis; end; for n holds R[n] from Ind(A4,A5); hence thesis by A3,FUNCT_2:113; end; theorem Th27: Partial_Sums(seq1)+Partial_Sums(seq2) = Partial_Sums(seq1+seq2) proof A1:Re (Partial_Sums(seq1)+Partial_Sums(seq2)) =Re Partial_Sums(seq1)+Re Partial_Sums(seq2) by Th15 .=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:8 .=Partial_Sums(Re (seq1+seq2)) by Th15 .=Re Partial_Sums(seq1+seq2) by Th26; Im (Partial_Sums(seq1)+Partial_Sums(seq2)) =Im Partial_Sums(seq1)+Im Partial_Sums(seq2) by Th15 .=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:8 .=Partial_Sums(Im (seq1+seq2)) by Th15 .=Im Partial_Sums(seq1+seq2) by Th26; hence thesis by A1,Th14; end; theorem Th28: Partial_Sums(seq1)-Partial_Sums(seq2) = Partial_Sums(seq1-seq2) proof A1: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:9 .=Partial_Sums(Re (seq1-seq2)) by Th18 .=Re Partial_Sums(seq1-seq2) by Th26; 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:9 .=Partial_Sums(Im (seq1-seq2)) by Th18 .=Im Partial_Sums(seq1-seq2) by Th26; hence thesis by A1,Th14; end; theorem Th29: Partial_Sums(z (#) seq) = z (#) Partial_Sums(seq) proof defpred P[Nat] means Partial_Sums(z (#) seq).$1= (z (#) Partial_Sums(seq)).$1; A1:P[0] proof thus Partial_Sums(z(#)seq).0 =(z (#) seq).0 by Def7 .=z * seq.0 by COMSEQ_1:def 7 .=z * Partial_Sums(seq).0 by Def7 .=(z (#) Partial_Sums(seq)).0 by COMSEQ_1:def 7; end; A2:now let n; assume A3: P[n]; thus P[n+1] proof thus Partial_Sums(z (#) seq).(n+1) =Partial_Sums(z (#) seq).n + (z (#) seq).(n+1) by Def7 .=(z * Partial_Sums(seq).n )+ (z (#) seq).(n+1) by A3,COMSEQ_1:def 7 .=(z * Partial_Sums(seq).n )+ (z * seq.(n+1)) by COMSEQ_1:def 7 .= z * ( Partial_Sums(seq).n + seq.(n+1)) by XCMPLX_1:8 .= z * ( Partial_Sums(seq).(n+1)) by Def7 .= (z (#) Partial_Sums(seq)).(n+1) by COMSEQ_1:def 7; end; end; for n holds P[n] from Ind(A1,A2); hence thesis by COMSEQ_1:6; end; theorem |.Partial_Sums(seq).k.| <= Partial_Sums(|.seq.|).k proof defpred P[Nat] means |. Partial_Sums(seq).$1 .| <= Partial_Sums(|.seq.|).$1; Partial_Sums(|.seq.|).0 = (|.seq.|).0 by SERIES_1:def 1 .= |. seq.0 .| by COMSEQ_1:def 14; then A1: P[0] by Def7; A2: now let k such that A3: P[k]; A4: |. Partial_Sums(seq).(k+1) .| =|. Partial_Sums(seq).k + (seq).(k+1) .| by Def7; A5: |. Partial_Sums(seq).k + (seq).(k+1) .| <= |. Partial_Sums(seq).k.| + |. (seq).(k+1) .| by COMPLEX1:142; |. Partial_Sums(seq).k.| + |.(seq).(k+1).| <= Partial_Sums(|.seq.| ).k + |.(seq).(k+1).| by A3,AXIOMS:24; then |. Partial_Sums(seq).(k+1) .| <= Partial_Sums(|.seq.|).k + |.seq.(k+1).| by A4,A5,AXIOMS:22; then |. Partial_Sums(seq).(k+1) .| <= Partial_Sums(|.seq.|).k+|.seq.|.(k+1) by COMSEQ_1:def 14; hence P[k+1] by SERIES_1:def 1; end; for k holds P[k] from Ind(A1,A2); hence thesis; end; theorem Th31: |.Partial_Sums(seq).m- Partial_Sums(seq).n.| <= abs( 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; Partial_Sums(|.seq.|).(n+0)-Partial_Sums(|.seq.|).n =Partial_Sums(|.seq.|).n+-Partial_Sums(|.seq.|).n by XCMPLX_0:def 8 .=0 by XCMPLX_0:def 6; then A2: P[0]; A3: now let k be Nat; assume A4: P[k]; A5: Partial_Sums(|.seq.|).(n+(k+1))- Partial_Sums(|.seq.|).n =Partial_Sums(|.seq.|).((n+k)+1)- Partial_Sums(|.seq.|).n by XCMPLX_1:1 .=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 COMSEQ_1:def 14 .=Partial_Sums(|.seq.|).(n+k)- Partial_Sums(|.seq.|).n +|.seq.(n+k+1).| by XCMPLX_1:29; 0 <= |.seq.(n+k+1).| by COMPLEX1:132; then 0+0 <= Partial_Sums(|.seq.|).(n+k) - Partial_Sums(|.seq.|).n +|.seq.(n+k+1).| by A4,REAL_1:55; hence P[k+1] by A5; end; thus for k be Nat holds P[k] from Ind(A2,A3); end; A6: for n,k be Nat holds abs( Partial_Sums(|.seq.|).(n+k)- Partial_Sums(|.seq.|).n ) = Partial_Sums(|.seq.|).(n+k)- Partial_Sums(|.seq.|).n proof let n,k be Nat; 0 <= Partial_Sums(|.seq.|).(n+k)- Partial_Sums(|.seq.|).n by A1; hence thesis by ABSVALUE:def 1; end; A7: for n for m st n <= m holds |.Partial_Sums(seq).m- Partial_Sums(seq).n.| <= abs( Partial_Sums(|.seq.|).m- Partial_Sums(|.seq.|).n ) proof let n; A8: for k be Nat holds |.Partial_Sums(seq).(n+k)- Partial_Sums(seq).n.| <= abs( Partial_Sums(|.seq.|).(n+k)- Partial_Sums(|.seq.|).n ) proof defpred P[Nat] means |.Partial_Sums(seq).(n+$1)- Partial_Sums(seq).n.| <= abs( Partial_Sums(|.seq.|).(n+$1)- Partial_Sums(|.seq.|).n ); |.Partial_Sums(seq).(n+0)- Partial_Sums(seq).n.| = 0 by COMPLEX1:130,XCMPLX_1:14; then A9:P[0] by ABSVALUE:5; A10: now let k be Nat; assume A11: P[k]; A12: |.Partial_Sums(seq).(n+(k+1))- Partial_Sums(seq).n .| =|.Partial_Sums(seq).((n+k)+1)- Partial_Sums(seq).n .| by XCMPLX_1:1 .=|.(Partial_Sums(seq).(n+k)+seq.(n+k+1))- Partial_Sums(seq).n.| by Def7 .=|.Partial_Sums(seq).(n+k)- Partial_Sums(seq).n+seq.(n+k+1).| by XCMPLX_1:29; A13:|.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:142; A14: |.Partial_Sums(seq).(n+k)- Partial_Sums(seq).n.| +|.seq.(n+k+1).| <= abs( Partial_Sums(|.seq.|).(n+k)- Partial_Sums(|.seq.|).n ) +|.seq.(n+k+1).| by A11,AXIOMS:24; abs( 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 by XCMPLX_1:29 .=Partial_Sums(|.seq.|).(n+k)+|.seq.|.(n+k+1) - Partial_Sums(|.seq.|).n by COMSEQ_1:def 14 .=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 XCMPLX_1:1 .=abs( Partial_Sums(|.seq.|).(n+(k+1))- Partial_Sums(|.seq.|).n ) by A6; hence P[k+1] by A12,A13,A14,AXIOMS:22; end; thus for k be Nat holds P[k] from Ind(A9,A10); end; let m; assume n <= m; then consider k be Nat such that A15:m=n+k by NAT_1:28; thus thesis by A8,A15; end; for n, m holds |.Partial_Sums(seq).m- Partial_Sums(seq).n.| <= abs( Partial_Sums(|.seq.|).m- Partial_Sums(|.seq.|).n ) proof let n,m; m <= n implies |.Partial_Sums(seq).m- Partial_Sums(seq).n.| <= abs( Partial_Sums(|.seq.|).m- Partial_Sums(|.seq.|).n ) proof assume m <= n; then A16:|.Partial_Sums(seq).n- Partial_Sums(seq).m.| <= abs( Partial_Sums(|.seq.|).n- Partial_Sums(|.seq.|).m ) by A7; abs( Partial_Sums(|.seq.|).n- Partial_Sums(|.seq.|).m ) =abs(-( Partial_Sums(|.seq.|).n- Partial_Sums(|.seq.|).m) ) by ABSVALUE:17 .=abs( Partial_Sums(|.seq.|).m- Partial_Sums(|.seq.|).n ) by XCMPLX_1:143; hence thesis by A16,COMPLEX1:146; end; hence thesis by A7; end; hence thesis; end; theorem 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; thus (Partial_Sums(Re seq)^\k).n =Partial_Sums(Re seq).(n+k) by SEQM_3:def 9 .=Re Partial_Sums(seq).(n+k) by Th26 .=Re(Partial_Sums(seq).(n+k)) by Def3 .=Re((Partial_Sums(seq)^\k).n) by Def6 .=(Re (Partial_Sums(seq)^\k)).n by Def3; thus (Partial_Sums(Im seq)^\k).n =Partial_Sums(Im seq).(n+k) by SEQM_3:def 9 .=Im Partial_Sums(seq).(n+k) by Th26 .=Im(Partial_Sums(seq).(n+k)) by Def4 .=Im((Partial_Sums(seq)^\k).n) by Def6 .=Im (Partial_Sums(seq)^\k).n by Def4; end; hence thesis by FUNCT_2:113; end; theorem (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 Def3 .=Re(seq.0) by A1 .=Re seq.0 by Def3; thus Im seq1.n=Im(seq1.n) by Def4 .=Im(seq.0) by A1 .=Im seq.0 by Def4; end; A3: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:14 .=Re (Partial_Sums(seq)^\1)-Re seq1 by Th32 .=Re (Partial_Sums(seq)^\1-seq1) by Th18; 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:14 .=Im (Partial_Sums(seq)^\1)-Im seq1 by Th32 .=Im (Partial_Sums(seq)^\1-seq1) by Th18; hence thesis by A3,Th14; end; theorem Th34: Partial_Sums |.seq.| is non-decreasing proof for n holds 0 <= |.seq.|.n by Lm1; hence thesis by SERIES_1:19; end; definition let seq be Complex_Sequence; cluster Partial_Sums |.seq.| -> non-decreasing; coherence by Th34; end; theorem (for n st n <= m holds seq1.n = seq2.n) implies Partial_Sums(seq1).m =Partial_Sums(seq2).m proof assume A1: for n st n <= m holds seq1.n = seq2.n; defpred P[Nat] means $1 <= m implies Partial_Sums(seq1).$1=Partial_Sums(seq2).$1; A2: P[0] proof assume A3: 0 <= m; thus Partial_Sums(seq1).0=seq1.0 by Def7 .=seq2.0 by A1,A3 .=Partial_Sums(seq2).0 by Def7; end; A4: for k be Nat st P[k] holds P[k+1] proof let k be Nat such that A5: P[k]; assume A6:k+1 <= m; k < k+1 by REAL_1:69; hence Partial_Sums(seq1).(k+1) =Partial_Sums(seq2).k+seq1.(k+1) by A5,A6,Def7,AXIOMS:22 .=Partial_Sums(seq2).k+seq2.(k+1) by A1,A6 .=Partial_Sums(seq2).(k+1) by Def7; end; for k holds P[k] from Ind(A2,A4); hence Partial_Sums(seq1).m=Partial_Sums(seq2).m; end; theorem Th36: 1r <> z implies for n holds Partial_Sums(z GeoSeq).n = (1r - z #N (n+1))/(1r-z) proof now let z; assume 1r <> z; then 0< |.1r-z.| by COMPLEX1:148; then A1: 1r-z <>0c by COMPLEX1:133; defpred P[Nat] means Partial_Sums(z GeoSeq).$1 = (1r - z #N ($1+1))/(1r-z); A2:P[0] proof thus Partial_Sums(z GeoSeq).0 =(z GeoSeq).0 by Def7 .=1r by Def1 .=(1r-z)/(1r-z) by A1,COMPLEX1:86 .=(1r -1r * z )/(1r-z) by COMPLEX1:29 .=(1r-(z GeoSeq).0 * z)/(1r-z) by Def1 .=(1r -(z GeoSeq).(0+1) )/(1r-z) by Def1 .=(1r-z #N (0+1) )/(1r-z) by Def2; end; A3:for n st P[n] holds P[n+1] proof let n; assume A4:P[n]; thus Partial_Sums(z GeoSeq).(n+1) =Partial_Sums(z GeoSeq).n + (z GeoSeq).(n+1) by Def7 .= (1r - z #N (n+1))/(1r-z)+ z #N (n+1) by A4,Def2 .= (1r - z #N (n+1))/(1r-z)+ z #N (n+1) * 1r by COMPLEX1:29 .= (1r - z #N (n+1))/(1r-z)+ z #N (n+1) * ((1r-z)/(1r-z)) by A1,COMPLEX1:86 .= (1r - z #N (n+1))/(1r-z)+ (z #N (n+1) * (1r-z))/(1r-z) by XCMPLX_1:75 .= (1r - z #N (n+1) + (z #N (n+1) * (1r-z)))/(1r-z) by XCMPLX_1:63 .= (1r - z #N (n+1) + (z #N (n+1) * 1r -z #N(n+1) * z ))/(1r-z) by XCMPLX_1:40 .= (1r - z #N (n+1) + (z #N (n+1) -z #N(n+1) * z ))/(1r-z) by COMPLEX1:29 .= (1r - z #N (n+1) + z #N (n+1) -z #N(n+1) * z )/(1r-z) by XCMPLX_1:29 .= (1r - (z #N (n+1) - z #N (n+1)) -z #N(n+1) * z )/(1r-z) by XCMPLX_1:37 .= (1r - 0c -z #N(n+1) * z )/(1r-z) by XCMPLX_1:14 .= (1r - z #N(n+1) * z )/(1r-z) by COMPLEX1:52 .= (1r - (z GeoSeq).(n+1) * z )/(1r-z) by Def2 .= (1r - (z GeoSeq).((n+1)+1) )/(1r-z) by Def1 .= (1r - z #N ((n+1) +1) )/(1r-z) by Def2; end; thus for n holds P[n] from Ind(A2,A3); end; hence thesis; end; theorem 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 (n+1))/(1r-z)) proof assume A1:z <> 1r & for n holds seq.(n+1) = z * seq.n; defpred P[Nat] means seq.$1=seq.0 * (z GeoSeq).$1; A2: P[0] proof thus seq.0 = seq.0 * 1r by COMPLEX1:29 .= seq.0 * (z GeoSeq).0 by Def1; end; A3: now let n; assume A4:P[n]; thus P[n+1] proof thus seq.(n+1)=z * (seq.0 * (z GeoSeq).n) by A1,A4 .=seq.0 * (z * (z GeoSeq).n) by XCMPLX_1:4 .=seq.0 * (z GeoSeq).(n+1) by Def1; end; end; A5: dom seq = NAT by FUNCT_2:def 1; for n holds P[n] from Ind(A2,A3); then A6:Partial_Sums(seq)=Partial_Sums(seq.0 (#) (z GeoSeq)) by A5,COMSEQ_1:def 7 .=seq.0 (#) Partial_Sums(z GeoSeq) by Th29; let n; thus Partial_Sums(seq).n=seq.0 * Partial_Sums(z GeoSeq).n by A6,COMSEQ_1:def 7 .=seq.0 * ( (1r - z #N (n+1))/(1r -z) ) by A1,Th36; end; begin :: Convergence of Complex Sequences theorem Th38: for a, b being Real_Sequence, c being 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 being real number such that A4: for p being real number st 0<p ex n st for m st n<=m holds abs(a.m-a1) < p by A2,SEQ_2:def 6; consider b1 being real number such that A5: for p being real number st 0<p ex n st for m st n<=m holds abs(b.m-b1)<p by A3,SEQ_2:def 6; reconsider a1,b1 as Real by XREAL_0:def 1; take g=[*a1,b1*]; for p st 0<p holds ex n st for m st n <= m holds |.c.m-g.|< p proof let p be Real; assume 0 < p; then A6: 0 < p/2 by SEQ_2:3; then consider n1 such that A7: for m st n1<=m holds abs(a.m-a1)< p/2 by A4; consider n2 such that A8: for m st n2<=m holds abs(b.m-b1)< p/2 by A5,A6; n1 <= (n1+n2) &n2 <= (n1+n2) by NAT_1:29; then consider n such that A9: n1 <= n &n2 <= n; take n; for m st n <= m holds |.c.m-g.|< p proof let m; assume n <= m; then n1 <= m & n2 <= m by A9,AXIOMS:22; then abs(a.m-a1)< p/2 & abs(b.m-b1)< p/2 by A7,A8; then abs(a.m-a1) + abs(b.m-b1)< p/2+ p/2 by REAL_1:67; then A10: abs(a.m-a1) + abs(b.m-b1)< p by XCMPLX_1:66; A11: |.c.m-g.| <= abs(Re(c.m-g)) + abs(Im(c.m-g)) by Th12; A12: Re(c.m)=a.m by A1; Re(g) =a1 by COMPLEX1:7; then A13: Re(c.m-g)=a.m-a1 by A12,COMPLEX1:48; A14: Im(c.m)=b.m by A1; Im(g) =b1 by COMPLEX1:7; then Im(c.m-g)=b.m-b1 by A14,COMPLEX1:48; hence |.c.m-g.|< p by A10,A11,A13,AXIOMS:22; end; hence thesis; end; hence thesis; end; assume c is convergent; then consider z such that A15: for p st 0<p ex n st for m st n <= m holds |.c.m-z.| < p by COMSEQ_2:def 4; thus a is convergent proof reconsider z as Element of COMPLEX; take Re(z); let p be real number; A16: p is Real by XREAL_0:def 1; assume 0<p; then consider n such that A17: for m st n <= m holds |.c.m-z.| < p by A15,A16; take n; let m; assume n <= m; then A18: |.c.m-z.| < p by A17; A19: Re(c.m) =a.m by A1; Re(c.m-z)=Re(c.m)-Re(z) by COMPLEX1:48; then abs(a.m-Re(z)) <= |.c.m-z.| by A19,Th13; hence thesis by A18,AXIOMS:22; end; take Im(z); let p be real number; A20: p is Real by XREAL_0:def 1; assume p>0; then consider n such that A21: for m st n <= m holds |.c.m-z.| < p by A15,A20; take n; let m; assume n <= m; then A22: |.c.m-z.| < p by A21; A23: Im(c.m) =b.m by A1; Im(c.m-z)=Im(c.m)-Im(z) by COMPLEX1:48; then abs(b.m-Im(z) ) <= |.c.m-z.| by A23,Th13; hence thesis by A22,AXIOMS:22; end; theorem Th39: for a, b being convergent Real_Sequence, c being 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; assume A1: for n holds Re(c.n) = a.n & Im(c.n) = b.n; hence A2: c is convergent by Th38; set g=[*lim(a),lim(b)*]; for p st 0<p holds ex n st for m st n<=m holds |.c.m-g.|< p proof let p be Real; assume 0 < p; then A3: 0 < p/2 by SEQ_2:3; then consider n1 such that A4: for m st n1<=m holds abs(a.m-lim(a))< p/2 by SEQ_2:def 7; consider n2 such that A5: for m st n2<=m holds abs(b.m-lim(b))< p/2 by A3,SEQ_2:def 7; n1 <= (n1+n2) &n2 <= (n1+n2) by NAT_1:29; then consider n such that A6: n1 <= n &n2 <= n; take n; let m; assume n <= m; then n1 <= m & n2 <= m by A6,AXIOMS:22; then abs(a.m-lim(a))< p/2 & abs(b.m-lim(b))< p/2 by A4,A5; then abs(a.m-lim(a)) + abs(b.m-lim(b))< p/2+ p/2 by REAL_1:67; then A7: abs(a.m-lim(a)) + abs(b.m-lim(b))< p by XCMPLX_1 :66; A8: |.c.m-g.| <= abs(Re(c.m-g)) + abs(Im(c.m-g)) by Th12; A9: Re(c.m)=a.m by A1; Re(g) =lim(a) by COMPLEX1:7; then A10: Re(c.m-g)=a.m-lim(a) by A9,COMPLEX1:48; A11: Im(c.m)=b.m by A1; Im(g) =lim(b) by COMPLEX1:7; then Im(c.m-g)=b.m-lim(b) by A11,COMPLEX1:48; hence thesis by A7,A8,A10,AXIOMS:22; end; hence thesis by A2,COMSEQ_2:def 5; end; theorem Th40: for a, b being Real_Sequence, c being 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; then A2: a is convergent & b is convergent by Th38; A3: for p being real number st 0<p ex n st for m st n<=m holds abs(a.m-Re(lim(c)))<p proof let p be real number; A4: p is Real by XREAL_0:def 1; assume 0<p; then consider n such that A5: for m st n <= m holds |.c.m-lim(c).| < p by A4,COMSEQ_2:def 5; take n; let m; assume n <= m; then A6: |.c.m-lim(c).| < p by A5; Re(c.m) =a.m by A1; then Re(c.m-lim(c))=a.m-Re(lim(c)) by COMPLEX1:48; then abs(a.m-Re(lim(c)) ) <= |.c.m-lim(c).| by Th13; hence thesis by A6,AXIOMS:22; end; for p being real number st 0<p ex n st for m st n<=m holds abs(b.m-Im(lim(c))) <p proof let p be real number; A7: p is Real by XREAL_0:def 1; assume p>0; then consider n such that A8: for m st n <= m holds |.c.m-lim(c).| < p by A7,COMSEQ_2:def 5; take n; let m; assume n <= m; then A9: |.c.m-lim(c).| < p by A8; A10: Im(c.m) =b.m by A1; Im(c.m-lim(c))=Im(c.m)-Im(lim(c)) by COMPLEX1:48; then abs(b.m-Im(lim(c)) ) <= |.c.m-lim(c).| by A10,Th13; hence thesis by A9,AXIOMS:22; end; hence thesis by A2,A3,SEQ_2:def 7; end; theorem Th41: 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)) proof let c be convergent Complex_Sequence; A1:for n holds Re c.n=Re(c.n) by Def3; for n holds Im c.n=Im(c.n) by Def4; hence thesis by A1,Th40; end; definition let c be convergent Complex_Sequence; cluster Re c -> convergent; coherence by Th41; cluster Im c -> convergent; coherence by Th41; end; theorem Th42: 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) 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) by Def3; for n holds Im c.n=Im(c.n) by Def4; then c is convergent & lim(c)=[*lim(Re c),lim(Im c)*] by A1,A2,Th39; hence thesis by COMPLEX1:7; end; theorem 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 A1: 0 < |.z.| & |.z.| < 1; assume A2: seq.0 = z & for n holds seq.(n+1) = seq.n * z; A3: for n holds |.seq.n.| = |.z.| to_power (n+1) proof defpred P[Nat] means |. seq.$1 .|= |.z.| to_power ($1+1); A4: P[0] by A2,POWER:30; A5: for k st P[k] holds P[k+1] proof let k be Nat; assume A6: P[k]; |.seq.(k+1).| = |.seq.k * z.| by A2 .= |.z.| to_power (k+1) * |.z.| by A6,COMPLEX1:151 .= |.z.| to_power (k+1) * |.z.| to_power (1) by POWER:30 .= |.z.| to_power ((k+1)+1) by A1,POWER:32; hence |.seq.(k+1).| = |.z.| to_power ((k+1)+1); end; for n holds P[n] from Ind(A4,A5); hence thesis; end; consider rseq be Real_Sequence such that A7:for n holds rseq.n=f(n) from ExRealSeq; A8:rseq is constant by A7,SEQM_3:def 6; rseq.0=0 by A7; then A9: rseq is convergent & lim(rseq)=0 by A8,SEQ_4:39,40; deffunc g(Nat) = |.z.| to_power ($1+1); consider rseq1 such that A10: for n holds rseq1.n=g(n) from ExRealSeq; A11: rseq1 is convergent & lim(rseq1)=0 by A1,A10,SERIES_1:1; A12: (for n holds rseq.n <= abs(Re seq).n ) & (for n holds abs(Re seq).n <= rseq1.n) proof A13: now let n; 0 <= abs(Re seq).n proof abs(Re seq).n=abs(Re seq.n) by SEQ_1:16; hence thesis by ABSVALUE:5; end; hence rseq.n <= abs(Re seq).n by A7; end; now let n; abs(Re seq).n = abs(Re seq.n) by SEQ_1:16; then A14: abs(Re seq).n = abs(Re(seq.n)) by Def3; A15: abs(Re(seq.n)) <= |.seq.n.| by Th13; |.seq.n.| = |.z.| to_power (n+1) by A3; hence abs(Re seq).n <= rseq1.n by A10,A14,A15; end; hence thesis by A13; end; A16: (for n holds rseq.n <= abs(Im seq).n ) & (for n holds abs(Im seq).n <= rseq1.n) proof A17: now let n; 0 <= abs(Im seq).n proof abs(Im seq).n=abs(Im seq.n) by SEQ_1:16; hence thesis by ABSVALUE:5; end; hence rseq.n <= abs(Im seq).n by A7; end; now let n; A18: abs(Im seq).n = abs(Im seq.n) by SEQ_1:16; A19: abs(Im(seq.n)) <= |.seq.n.| by Th13; |.seq.n.| = |.z.| to_power (n+1) by A3; then abs(Im seq).n <= |.z.| to_power (n+1) by A18,A19,Def4; hence abs(Im seq).n <= rseq1.n by A10; end; hence thesis by A17; end; A20: abs(Re seq) is convergent by A9,A11,A12,SEQ_2:33; A21: lim(abs(Re seq))=0 by A9,A11,A12,SEQ_2:34; A22:abs(Im seq) is convergent by A9,A11,A16,SEQ_2:33; A23:lim(abs(Im seq))=0 by A9,A11,A16,SEQ_2:34; A24: Re seq is convergent & lim(Re seq)=0 by A20,A21,SEQ_4:28; Im seq is convergent & lim(Im seq)=0 by A22,A23,SEQ_4:28; then seq is convergent & Re lim(seq)=0 &Im lim(seq)=0 by A24,Th42; hence thesis by COMPLEX1:8,L0; end; theorem Th44: |.z.| < 1 & (for n holds seq.n=z #N (n+1)) implies seq is convergent & lim(seq)=0c proof assume A1: |.z.| <1 & (for n holds seq.n=z #N (n+1)); then A2: seq.0= z #N (0+1) .=(z GeoSeq).(0+1) by Def2 .=(z GeoSeq).0 * z by Def1 .=1r * z by Def1 .=z by COMPLEX1:29; A3: now let n; thus seq.(n+1) = z #N ((n+1)+1) by A1 .= (z GeoSeq).((n+1)+1) by Def2 .= (z GeoSeq).(n+1) * z by Def1 .= z #N (n+1) * z by Def2 .= seq.n * z by A1; end; A4: now assume A5: |.z.| <> 0; 0 <= |.z.| by COMPLEX1:132; hence seq is convergent & lim(seq)=0c by A1,A2,A3,A5,Th43; end; now assume |.z.| = 0; then A6: z =0c by COMPLEX1:131; A7: now let n; thus seq.n = 0c #N (n+1) by A1,A6 .=(0c GeoSeq).(n+1) by Def2 .=(0c GeoSeq).n * 0c by Def1 .=0c by COMPLEX1:28; end; hence seq is convergent by COMSEQ_2:9; thus seq is convergent & lim(seq)=0c by A7,COMSEQ_2:9,10; end; hence thesis by A4; end; theorem 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 A1: r>0 & (ex m st for n st n>=m holds |.seq.n.| >= r); then consider m such that A2: for n st n>=m holds |.seq.n.| >= r; now let n such that A3:n>=m; 0 <= |.seq.|.n by Lm1; then abs((|.seq.|).n) =|.seq.|.n by ABSVALUE:def 1 .=|.seq.n.| by COMSEQ_1:def 14; hence abs((|.seq.|).n) >= r by A2,A3; end; hence thesis by A1,SERIES_1:43; end; theorem Th46: seq is convergent iff for p st 0<p ex n st for m st n <= m holds |.seq.m-seq.n.|<p proof A1:now assume seq is convergent; then consider z such that A2:for p st 0<p holds ex n st for m st n <= m holds |.seq.m-z.|<p by COMSEQ_2:def 4; let p; assume 0< p; then 0 <p/2 by SEQ_2:3; then consider n such that A3: for m st n <= m holds |.seq.m-z.|<p/2 by A2; take n; let m; assume n <= m; then A4:|.seq.m-z.|<p/2 by A3; |.seq.n-z.|<p/2 by A3; then |.seq.m-z.| + |.seq.n-z.| <p/2+p/2 by A4,REAL_1:67; then |.seq.m-z.| + |.seq.n-z.| <p by XCMPLX_1:66; then A5:|.seq.m-z.| + |.z-seq.n.| <p by COMPLEX1:146; |.seq.m-seq.n.| <= |.seq.m-z.| + |.z-seq.n.| by COMPLEX1:149; hence |.seq.m-seq.n.|< p by A5,AXIOMS:22; end; now assume A6: for p st 0<p holds ex n st for m st n <= m holds |.seq.m-seq.n.|<p; for p be real number st 0<p holds ex n st for m st n <= m holds abs(Re seq.m-Re seq.n)<p proof let p be real number; A7: p is Real by XREAL_0:def 1; assume 0<p; then consider n such that A8: for m st n <= m holds |.seq.m-seq.n.|<p by A6,A7; take n; let m; assume n <= m; then A9: |.seq.m-seq.n.|<p by A8; Re(seq.m-seq.n)=Re(seq.m)-Re(seq.n) by COMPLEX1:48 .=Re seq.m-Re(seq.n) by Def3 .=Re seq.m-Re seq.n by Def3; then abs(Re seq.m-Re seq.n) <= |.seq.m-seq.n.| by Th13; hence abs(Re seq.m-Re seq.n) < p by A9,AXIOMS:22; end; hence A10: Re seq is convergent by SEQ_4:58; for p be real number st 0<p holds ex n st for m st n <= m holds abs(Im seq.m-Im seq.n)<p proof let p be real number; A11: p is Real by XREAL_0:def 1; assume 0<p; then consider n such that A12: for m st n <= m holds |.seq.m-seq.n.|<p by A6,A11; take n; let m; assume n <= m; then A13: |.seq.m-seq.n.|<p by A12; Im(seq.m-seq.n)=Im(seq.m)-Im(seq.n) by COMPLEX1:48 .=Im seq.m-Im(seq.n) by Def4 .=Im seq.m-Im seq.n by Def4; then abs(Im seq.m-Im seq.n) <= |.seq.m-seq.n.| by Th13; hence abs(Im seq.m-Im seq.n) < p by A13,AXIOMS:22; end; hence Im seq is convergent by SEQ_4:58; hence seq is convergent by A10,Th42; end; hence thesis by A1; end; theorem seq is convergent implies (for p st 0<p 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 0<p/2 by SEQ_2:3; then consider n such that A2: for m st n <= m holds |.seq.m-seq.n.|<p/2 by A1,Th46; take n; now let m,l be Nat; assume A3:n <= m & n <= l; then A4:|.seq.m-seq.n.|<p/2 by A2; |.seq.l-seq.n.|<p/2 by A2,A3; then |.seq.m-seq.n.|+|.seq.l-seq.n.| < p/2+p/2 by A4,REAL_1:67; then A5:|.seq.m-seq.n.|+|.seq.l-seq.n.| < p by XCMPLX_1:66; A6: |.(seq.m-seq.n)-(seq.l-seq.n).| =|.seq.m-seq.n-seq.l+seq.n.| by XCMPLX_1:37 .=|.seq.m+-seq.n-seq.l+seq.n.| by XCMPLX_0:def 8 .=|.seq.m+-seq.n+-seq.l+seq.n.| by XCMPLX_0:def 8 .=|.seq.m+-seq.l+-seq.n+seq.n.| by XCMPLX_1:1 .=|.(seq.m+-seq.l)+(-seq.n+seq.n).| by XCMPLX_1:1 .=|.(seq.m+-seq.l)+0c.| by XCMPLX_0:def 6 .=|.(seq.m+-seq.l).| by COMPLEX1:22 .=|.(seq.m-seq.l).| by XCMPLX_0:def 8; |.(seq.m-seq.n)-(seq.l-seq.n).| <= |.seq.m-seq.n.|+|.seq.l-seq.n.| by COMPLEX1:143; hence |.seq.m-seq.l.| < p by A5,A6,AXIOMS:22; end; hence thesis; end; theorem ((for n holds |. seq.n .| <= rseq.n) & rseq is convergent & lim(rseq)=0) implies seq is convergent & lim(seq)=0c proof assume A1: (for n holds |. seq.n .| <= rseq.n) & rseq is convergent & lim(rseq)=0; ex rseq1 be Real_Sequence st for n holds rseq1.n = f(n) from ExRealSeq; then consider rseq1 be Real_Sequence such that A2:for n holds rseq1.n=0; A3:rseq1 is constant by A2,SEQM_3:def 6; rseq1.0=0 by A2; then A4: rseq1 is convergent & lim(rseq1)=0 by A3,SEQ_4:39,40; A5: (for n holds rseq1.n <= abs(Re(seq)).n ) & (for n holds abs(Re(seq)).n <= rseq.n) proof A6: now let n; 0 <= abs(Re(seq)).n proof abs(Re(seq)).n=abs(Re(seq).n) by SEQ_1:16; hence thesis by ABSVALUE:5; end; hence rseq1.n <= abs(Re(seq)).n by A2; end; now let n; Re(seq).n = Re(seq.n) by Def3; then A7: abs(Re(seq)).n = abs(Re(seq.n)) by SEQ_1:16; A8: abs(Re(seq.n)) <= |.seq.n.| by Th13; |.seq.n.| <= rseq.n by A1; hence abs(Re(seq)).n <= rseq.n by A7,A8,AXIOMS:22; end; hence thesis by A6; end; A9: (for n holds rseq1.n <= abs(Im(seq)).n ) & (for n holds abs(Im(seq)).n <= rseq.n) proof A10: now let n; 0 <= abs(Im(seq)).n proof abs(Im(seq)).n=abs(Im(seq).n) by SEQ_1:16; hence thesis by ABSVALUE:5; end; hence rseq1.n <= abs(Im(seq)).n by A2; end; now let n; A11: Im(seq).n = Im(seq.n) by Def4; A12: abs(Im(seq)).n = abs(Im(seq).n) by SEQ_1:16; A13: abs(Im(seq.n)) <= |.seq.n.| by Th13; |.seq.n.| <= rseq.n by A1; hence abs(Im(seq)).n <= rseq.n by A11,A12,A13,AXIOMS:22; end; hence thesis by A10; end; A14: abs(Re(seq)) is convergent by A1,A4,A5,SEQ_2:33; A15: lim(abs(Re(seq)))=0 by A1,A4,A5,SEQ_2:34; A16:abs(Im(seq)) is convergent by A1,A4,A9,SEQ_2:33; A17:lim(abs(Im(seq)))=0 by A1,A4,A9,SEQ_2:34; A18: Re(seq) is convergent & lim(Re(seq))=0 by A14,A15,SEQ_4:28; Im(seq) is convergent & lim(Im(seq))=0 by A16,A17,SEQ_4:28; then seq is convergent & Re lim(seq)=0 &Im lim(seq)=0 by A18,Th42; hence thesis by COMPLEX1:8,L0; end; begin :: Summable and Absolutely Summable Complex Sequences definition let seq, seq1 be Complex_Sequence; pred seq is_subsequence_of seq1 means :Def9: ex Nseq st seq = seq1(#)Nseq; end; theorem 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 Def9; Re seq=Re seq1* Nseq by A1,Th22; hence Re seq is_subsequence_of Re seq1 by SEQM_3:def 10; Im seq=Im seq1 * Nseq by A1,Th22; hence thesis by SEQM_3:def 10; end; theorem Th50: seq is_subsequence_of seq1 & seq1 is_subsequence_of seq2 implies seq is_subsequence_of seq2 proof assume that A1: seq is_subsequence_of seq1 and A2: seq1 is_subsequence_of seq2; consider Nseq such that A3: seq=seq1(#)Nseq by A1,Def9; consider Nseq1 such that A4: seq1=seq2(#)Nseq1 by A2,Def9; now let n; thus (seq2(#)(Nseq1 * Nseq)).n = seq2.((Nseq1 * Nseq).n) by Def5 .=seq2.(Nseq1.(Nseq.n)) by SEQM_3:31 .=(seq2(#)Nseq1).(Nseq.n) by Def5 .=seq.n by A3,A4,Def5; end; then seq=seq2(#)(Nseq1*Nseq) by COMSEQ_1:6; hence seq is_subsequence_of seq2 by Def9; end; theorem seq is bounded implies ex seq1 st seq1 is_subsequence_of seq & seq1 is convergent proof assume seq is bounded; then consider r being Real such that A1: 0 < r & for n holds |.seq.n.| <r by COMSEQ_2:8; now let n; A2: |.seq.n.| <r by A1; A3:abs (Re seq.n)=abs(Re(seq.n)) by Def3; abs(Re(seq.n)) <= |.seq.n.| by Th13; hence abs(Re seq.n) < r by A2,A3,AXIOMS:22; end; then Re seq is bounded by A1,SEQ_2:15; then consider rseq1 such that A4: rseq1 is_subsequence_of Re seq & rseq1 is convergent by SEQ_4:57; consider Nseq such that A5: rseq1=Re seq*Nseq by A4,SEQM_3:def 10; A6: now let n; |. (seq (#) Nseq).n .|=|. seq.(Nseq.n) .| by Def5; hence |. (seq (#) Nseq).n .| < r by A1; end; now let n; A7: |.(seq(#) Nseq).n.| <r by A6; A8:abs(Im (seq(#)Nseq).n)=abs(Im((seq(#) Nseq).n)) by Def4; abs(Im((seq(#) Nseq).n)) <= |.(seq(#) Nseq).n.| by Th13; hence abs(Im (seq(#)Nseq).n) < r by A7,A8,AXIOMS:22; end; then Im (seq(#)Nseq) is bounded by A1,SEQ_2:15; then consider rseq2 such that A9: rseq2 is_subsequence_of Im (seq(#)Nseq) & rseq2 is convergent by SEQ_4:57; consider Nseq1 such that A10: rseq2=Im (seq(#)Nseq)*Nseq1 by A9,SEQM_3:def 10; A11: seq(#)Nseq is_subsequence_of seq by Def9; (seq(#)Nseq)(#)Nseq1 is_subsequence_of seq(#)Nseq by Def9; then A12: (seq(#)Nseq)(#)Nseq1 is_subsequence_of seq by A11,Th50; A13: Im ((seq(#)Nseq)(#)Nseq1) is convergent by A9,A10,Th22; Re ((seq(#)Nseq)(#)Nseq1)=(Re (seq(#)Nseq))*Nseq1 by Th22 .=rseq1*Nseq1 by A5,Th22; then Re ((seq(#)Nseq)(#) Nseq1) is_subsequence_of rseq1 by SEQM_3:def 10; then Re ((seq(#)Nseq)(#)Nseq1) is convergent by A4,SEQ_4:29; then (seq(#)Nseq)(#)Nseq1 is convergent by A13,Th42; hence thesis by A12; end; definition let seq be Complex_Sequence; attr seq is summable means :Def10: Partial_Sums seq is convergent; end; deffunc z(set) = 0c; definition cluster summable Complex_Sequence; existence proof consider C being Complex_Sequence such that A1: for n holds C.n = z(n) from ExComplexSeq; take C; take 0c; let p be Real such that A2: 0<p; take 0; let m such that 0<=m; thus |.Partial_Sums C.m-0c.|<p by A1,A2,Th24,COMPLEX1:130; end; end; definition let seq be summable Complex_Sequence; cluster Partial_Sums seq -> convergent; coherence by Def10; end; definition let seq; attr seq is absolutely_summable means :Def11: |.seq.| is summable; end; theorem Th52: (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 number such that A2: 0<p; take 0; let m such that 0<=m; abs((Partial_Sums |.seq.|).m-0) = abs(0-0) by A1,Th25 .= 0 by ABSVALUE:def 1; hence abs((Partial_Sums |.seq.|).m-0)<p by A2; end; definition cluster absolutely_summable Complex_Sequence; existence proof consider C being Complex_Sequence such that A1: for n holds C.n = z(n) from ExComplexSeq; take C; thus thesis by A1,Th52; end; end; definition let seq be absolutely_summable Complex_Sequence; cluster |.seq.| -> summable; coherence by Def11; end; theorem Th53: seq is summable implies seq is convergent & lim seq = 0c proof assume seq is summable; then Partial_Sums(seq) is convergent by Def10; then Re Partial_Sums(seq) is convergent &Im Partial_Sums(seq) is convergent by Th41; then Partial_Sums(Re seq) is convergent &Partial_Sums(Im seq) is convergent by Th26; then Re seq is summable & Im seq is summable by SERIES_1:def 2; then Re seq is convergent & lim(Re seq)=0 & Im seq is convergent & lim(Im seq)=0 by SERIES_1:7; then seq is convergent & Re(lim(seq))=0 &Im(lim(seq))=0 by Th42; hence thesis by COMPLEX1:8,L0; end; definition cluster summable -> convergent Complex_Sequence; coherence by Th53; end; theorem Th54: seq is summable implies Re seq is summable & Im seq is summable & Sum(seq)=[*Sum(Re seq),Sum(Im seq)*] proof assume seq is summable; then A1: Partial_Sums(seq) is convergent by Def10; then Re Partial_Sums(seq) is convergent &Im Partial_Sums(seq) is convergent by Th41; then A2: Partial_Sums(Re seq) is convergent &Partial_Sums(Im seq) is convergent by Th26; A3:lim(Re Partial_Sums(seq))=lim(Partial_Sums(Re seq)) & lim(Im Partial_Sums(seq))=lim(Partial_Sums(Im seq)) by Th26; A4:lim(Partial_Sums(Re seq))=Sum(Re seq) & lim(Partial_Sums(Im seq))=Sum(Im seq) by SERIES_1:def 3; lim(Re Partial_Sums(seq))=Re(lim(Partial_Sums(seq))) & lim(Im Partial_Sums(seq))=Im(lim(Partial_Sums(seq))) by A1,Th41; then Re(Sum(seq))=lim(Re Partial_Sums(seq)) & Im(Sum(seq))=lim(Im Partial_Sums(seq)) by Def8; hence thesis by A2,A3,A4,COMPLEX1:8,SERIES_1:def 2; end; definition let seq be summable Complex_Sequence; cluster Re seq -> summable; coherence by Th54; cluster Im seq -> summable; coherence by Th54; end; theorem Th55: seq1 is summable & seq2 is summable implies seq1+seq2 is summable & Sum(seq1+seq2)= Sum(seq1)+Sum(seq2) proof assume seq1 is summable & seq2 is summable; then A1:Partial_Sums(seq1) is convergent & Partial_Sums(seq2) is convergent by Def10; then A2:Partial_Sums(seq1)+Partial_Sums(seq2) is convergent by COMSEQ_2:13; A3:Partial_Sums(seq1)+Partial_Sums(seq2) =Partial_Sums(seq1+seq2) by Th27; Sum(seq1+seq2)=lim(Partial_Sums(seq1+seq2)) by Def8 .=lim(Partial_Sums(seq1)+Partial_Sums(seq2)) by Th27 .=lim(Partial_Sums(seq1))+lim(Partial_Sums(seq2)) by A1,COMSEQ_2:14; then Sum(seq1+seq2)=Sum(seq1)+lim(Partial_Sums(seq2)) by Def8 .= Sum(seq1)+Sum(seq2) by Def8; hence thesis by A2,A3,Def10; end; theorem Th56: seq1 is summable & seq2 is summable implies seq1-seq2 is summable & Sum(seq1-seq2)= Sum(seq1)-Sum(seq2) proof assume seq1 is summable & seq2 is summable; then A1:Partial_Sums(seq1) is convergent & Partial_Sums(seq2) is convergent by Def10; then A2:Partial_Sums(seq1)-Partial_Sums(seq2) is convergent by COMSEQ_2:25; A3:Partial_Sums(seq1)-Partial_Sums(seq2) =Partial_Sums(seq1-seq2) by Th28; Sum(seq1-seq2)=lim(Partial_Sums(seq1-seq2)) by Def8 .=lim(Partial_Sums(seq1)-Partial_Sums(seq2)) by Th28 .=lim(Partial_Sums(seq1))-lim(Partial_Sums(seq2)) by A1,COMSEQ_2:26; then Sum(seq1-seq2)=Sum(seq1)-lim(Partial_Sums(seq2)) by Def8 .= Sum(seq1)-Sum(seq2) by Def8; hence thesis by A2,A3,Def10; end; definition let seq1, seq2 be summable Complex_Sequence; cluster seq1 + seq2 -> summable; coherence by Th55; cluster seq1 - seq2 -> summable; coherence by Th56; end; theorem Th57: seq is summable implies z (#) seq is summable & Sum(z (#) seq)= z * Sum(seq) proof assume seq is summable; then A1:Partial_Sums(seq) is convergent by Def10; then A2:(z (#) Partial_Sums(seq)) is convergent by COMSEQ_2:17; A3:Partial_Sums(z (#) seq)=(z (#) Partial_Sums(seq)) by Th29; Sum(z (#) seq)=lim(Partial_Sums(z (#) seq)) by Def8 .=lim((z (#) Partial_Sums(seq))) by Th29 .=z * lim(Partial_Sums(seq)) by A1,COMSEQ_2:18 .=z * Sum(seq) by Def8; hence z (#) seq is summable & Sum(z (#) seq)= z * Sum(seq) by A2,A3,Def10; end; definition let z be Element of COMPLEX, seq be summable Complex_Sequence; cluster z (#) seq -> summable; coherence by Th57; end; theorem Th58: Re seq is summable & Im seq is summable implies seq is summable & Sum(seq)=[*Sum(Re seq),Sum(Im seq)*] proof assume Re seq is summable & Im seq is summable; then Partial_Sums(Re seq) is convergent &Partial_Sums(Im seq) is convergent by SERIES_1:def 2; then A1: Re Partial_Sums(seq) is convergent &Im Partial_Sums(seq) is convergent by Th26; then A2: Partial_Sums(seq) is convergent by Th42; A3:lim(Re Partial_Sums(seq))=lim(Partial_Sums(Re seq)) & lim(Im Partial_Sums(seq))=lim(Partial_Sums(Im seq)) by Th26; A4:lim(Partial_Sums(Re seq))=Sum(Re seq) & lim(Partial_Sums(Im seq))=Sum(Im seq) by SERIES_1:def 3; lim(Re Partial_Sums(seq))=Re(lim(Partial_Sums(seq))) & lim(Im Partial_Sums(seq))=Im(lim(Partial_Sums(seq))) by A1,Th42; then Re(Sum(seq))=lim(Re Partial_Sums(seq)) & Im(Sum(seq))=lim(Im Partial_Sums(seq)) by Def8; hence thesis by A2,A3,A4,Def10,COMPLEX1:8; end; theorem Th59: seq is summable implies for n holds seq^\n is summable proof assume A1: seq is summable; now let n; Re seq is summable & Im seq is summable by A1,Th54; then A2: Re seq^\n is summable & Im seq^\n is summable by SERIES_1:15; Re (seq^\n)=Re seq^\n & Im(seq^\n)=Im seq^\n by Th23; hence seq^\n is summable by A2,Th58; end; hence thesis; end; definition let seq be summable Complex_Sequence, n be Nat; cluster seq^\n -> summable; coherence by Th59; end; theorem (ex n st seq^\n is summable) implies seq is summable proof given n such that A1:seq^\n is summable; A2: Re (seq^\n) is summable & Im (seq^\n) is summable by A1,Th54; Re (seq^\n)=Re seq^\n & Im (seq^\n)=Im seq^\n by Th23; then Re seq is summable & Im seq is summable by A2,SERIES_1:16; hence thesis by Th58; end; theorem seq is summable implies for n holds Sum(seq) = Partial_Sums(seq).n + Sum(seq^\(n+1)) proof assume A1:seq is summable; then A2:Re(seq) is summable & Im(seq) is summable by Th54; let n; A3:seq^\(n+1) is summable by A1,Th59; Sum(seq)=[* Sum(Re(seq)),Sum(Im(seq))*] by A1,Th54; then A4:Re(Sum(seq))=Sum(Re(seq)) & Im(Sum(seq))=Sum(Im(seq)) by COMPLEX1:7; A5:Sum(seq^\(n+1))=[*Sum(Re(seq^\(n+1))),Sum(Im(seq^\(n+1)))*] by A3,Th54; A6:Sum(Re(seq)) =Partial_Sums(Re(seq)).n + Sum(Re(seq)^\(n+1)) by A2,SERIES_1:18 .=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 A5,COMPLEX1:7 .=Re(Partial_Sums(seq).n) + Re(Sum(seq^\(n+1))) by Def3 .=Re(Partial_Sums(seq).n+ Sum(seq^\(n+1))) by COMPLEX1:19; Sum(Im(seq)) =Partial_Sums(Im(seq)).n + Sum(Im(seq)^\(n+1)) by A2,SERIES_1:18 .=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 A5,COMPLEX1:7 .=Im(Partial_Sums(seq).n) + Im(Sum(seq^\(n+1))) by Def4 .=Im(Partial_Sums(seq).n+ Sum(seq^\(n+1))) by COMPLEX1:19; hence Sum(seq)=Partial_Sums(seq).n+ Sum (seq^\(n+1)) by A4,A6,COMPLEX1:def 5; end; theorem Th62: Partial_Sums |.seq.| is bounded_above iff seq is absolutely_summable proof for n holds 0 <= |.seq.|.n by Lm1; then Partial_Sums(|.seq.|) is bounded_above iff |.seq.| is summable by SERIES_1:20; hence thesis by Def11; end; definition let seq be absolutely_summable Complex_Sequence; cluster Partial_Sums |.seq.| -> bounded_above; coherence by Th62; end; theorem Th63: 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) proof A1:now assume seq is summable; then Partial_Sums(seq) is convergent by Def10; hence 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; end; now assume for p st 0<p holds ex n st for m st n <= m holds |.Partial_Sums(seq).m-Partial_Sums(seq).n.|< p; then Partial_Sums(seq) is convergent by Th46; hence seq is summable by Def10; end; hence thesis by A1; end; theorem Th64: seq is absolutely_summable implies seq is summable proof assume seq is absolutely_summable; then |.seq.| is summable by Def11; then A1: Partial_Sums(|.seq.|) is convergent by SERIES_1:def 2; now let p; assume 0<p; then consider n such that A2: for m st n <= m holds abs(Partial_Sums(|.seq.|).m-Partial_Sums(|.seq.|).n)< p by A1,SEQ_4:58; take n; let m; assume n <= m; then A3: abs(Partial_Sums(|.seq.|).m-Partial_Sums(|.seq.|).n)< p by A2; |.Partial_Sums(seq).m-Partial_Sums(seq).n.| <= abs(Partial_Sums(|.seq.|).m-Partial_Sums(|.seq.|).n) by Th31; hence |.Partial_Sums(seq).m-Partial_Sums(seq).n.| <p by A3,AXIOMS:22; end; hence seq is summable by Th63; end; definition cluster absolutely_summable -> summable Complex_Sequence; coherence by Th64; end; definition cluster absolutely_summable Complex_Sequence; existence proof consider C being absolutely_summable Complex_Sequence; take C; thus thesis; end; end; theorem Th65: |.z.| < 1 implies z GeoSeq is summable & Sum(z GeoSeq) = 1r/(1r-z) proof assume A1: |.z.|<1; 1r-z <>0c proof assume A2: 1r-z = 0c; 0 <= abs(|.1r.|-|.z.|) by ABSVALUE:5; then abs(|.1r.|-|.z.|)=0 by A2,COMPLEX1:130,150; then |.1r.|-|.z.| =0 by ABSVALUE:7; hence contradiction by A1,COMPLEX1:134,XCMPLX_1:15; end; then A3: 1r <> z by XCMPLX_1:14; deffunc f(Nat) = z #N ($1+1); consider seq1 such that A4:for n holds seq1.n=f(n) from ExComplexSeq; A5:seq1 is convergent & lim(seq1)=0c by A1,A4,Th44; deffunc j(set) = 1r; consider seq2 such that A6:for n holds seq2.n=j(n) from ExComplexSeq; A7: seq2 is convergent by A6,COMSEQ_2:9; then A8: seq2-seq1 is convergent by A5,COMSEQ_2:25; A9: lim(seq2-seq1)=lim(seq2)-lim(seq1) by A5,A7,COMSEQ_2:26 .=1r -0c by A5,A6,COMSEQ_2:10 .=1r by COMPLEX1:52; A10:(1r/(1r-z))(#)(seq2-seq1) is convergent by A8,COMSEQ_2:17; A11:lim((1r/(1r-z))(#)(seq2-seq1))=1r/(1r-z) * 1r by A8,A9,COMSEQ_2:18 .=1r/(1r-z) by COMPLEX1:29; A12: now let n; thus Partial_Sums(z GeoSeq).n = (1r - z #N (n+1))/(1r-z) by A3,Th36 .= (1r - seq1.n)/(1r-z) by A4 .= (seq2.n-seq1.n)/(1r-z) by A6 .= 1r * (seq2.n-seq1.n)/(1r-z) by COMPLEX1:29 .= (seq2.n-seq1.n) * (1r/(1r-z)) by XCMPLX_1:75 .= (1r/(1r-z)) * (seq2.n+-seq1.n) by XCMPLX_0:def 8 .= (1r/(1r-z)) * (seq2.n+(-seq1).n) by COMSEQ_1:def 9 .= (1r/(1r-z)) * (seq2+(-seq1)).n by COMSEQ_1:def 4 .= (1r/(1r-z)) * (seq2-seq1).n by COMSEQ_1:def 10 .= ((1r/(1r-z))(#)(seq2-seq1)).n by COMSEQ_1:def 7; end; hence Partial_Sums(z GeoSeq) is convergent by A10,COMSEQ_1:6; lim(Partial_Sums(z GeoSeq) ) =1r/(1r-z) by A11,A12,COMSEQ_1:6; hence Sum(z GeoSeq) = 1r/(1r-z) by Def8; end; theorem |.z.| < 1 & (for n holds seq.(n+1) = z * seq.n) implies seq is summable & Sum(seq) = seq.0/(1r-z) proof assume A1:|.z.|< 1 & (for n holds seq.(n+1) = z * seq.n); 1r-z <>0c proof assume A2: 1r-z = 0c; 0 <= abs(|.1r.|-|.z.|) by ABSVALUE:5; then abs(|.1r.|-|.z.|)=0 by A2,COMPLEX1:130,150; then |.1r.|-|.z.| =0 by ABSVALUE:7; hence contradiction by A1,COMPLEX1:134,XCMPLX_1:15; end; then A3: z <> 1r by XCMPLX_1:14; now let n; thus Partial_Sums(seq).n = seq.0 * ((1r - z #N (n+1))/(1r-z)) by A1,A3,Th37 .=seq.0 * Partial_Sums(z GeoSeq).n by A3,Th36 .=(seq.0 (#) Partial_Sums(z GeoSeq)).n by COMSEQ_1:def 7; end; then A4: Partial_Sums(seq)=(seq.0 (#) Partial_Sums(z GeoSeq)) by COMSEQ_1:6; z GeoSeq is summable & Sum(z GeoSeq) = 1r/(1r-z) by A1,Th65; then A5: Partial_Sums(z GeoSeq) is convergent & Sum(z GeoSeq) = lim(Partial_Sums(z GeoSeq)) by Def8,Def10; then Partial_Sums(seq) is convergent & lim(Partial_Sums(seq)) =seq.0 * lim(Partial_Sums(z GeoSeq)) by A4,COMSEQ_2:17,18; hence seq is summable by Def10; Sum(seq)=lim(Partial_Sums(seq)) by Def8 .=seq.0 * Sum(z GeoSeq) by A4,A5,COMSEQ_2:18 .=seq.0 * (1r/(1r-z)) by A1,Th65 .=seq.0 * 1r/(1r-z) by XCMPLX_1:75 .=seq.0/(1r-z) by COMPLEX1:29; hence thesis; end; theorem rseq1 is summable & (ex m st for n st m<=n holds |.seq2.n.| <= rseq1.n ) implies seq2 is absolutely_summable proof assume A1:rseq1 is summable & (ex m st for n st m<=n holds |.seq2.n.| <= rseq1.n ); then consider m such that A2: for n st m<=n holds |.seq2.n.| <= rseq1.n; A3:now let n; assume m <= n; then |.seq2.n.| <= rseq1.n by A2; hence |.seq2.|.n <= rseq1.n by COMSEQ_1:def 14; end; now let n; |.seq2.n.|=|.seq2.|.n by COMSEQ_1:def 14; hence 0 <= |.seq2.|.n by COMPLEX1:132; end; hence |.seq2.| is summable by A1,A3,SERIES_1:22; end; theorem (for n holds 0 <= |.seq1.|.n & |.seq1.|.n <= |.seq2.|.n) & seq2 is absolutely_summable implies seq1 is absolutely_summable & Sum |.seq1.| <= Sum |.seq2.| proof assume A1: (for n holds 0 <= |.seq1.|.n & |.seq1.|.n <= |.seq2.|.n) & seq2 is absolutely_summable; then |.seq2.| is summable by Def11; hence |.seq1.| is summable & Sum(|.seq1.|)<=Sum(|.seq2.|) by A1,SERIES_1:24; end; theorem (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 proof assume (for n holds |.seq.|.n>0) & (ex m st for n st n>=m holds |.seq.|.(n+1)/ |.seq.|.n >= 1); hence |.seq.| is not summable by SERIES_1:31; end; theorem (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 Lm1; hence |.seq.| is summable by A1,SERIES_1:32; end; theorem (for n holds rseq1.n = n-root (|.seq.|.n)) & (ex m st for n st m<=n holds rseq1.n>= 1) implies |.seq.| is not 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 Lm1; hence |.seq.| is not summable by A1,SERIES_1:33; end; theorem (for n holds rseq1.n = n-root (|.seq.|.n)) & rseq1 is convergent & lim rseq1 > 1 implies seq is not 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 Lm1; hence |.seq.| is not summable by A1,SERIES_1:34; end; theorem |.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 Lm1; then |.seq.| is summable iff rseq1 is summable by SERIES_1:35; hence seq is absolutely_summable iff rseq1 is summable by Def11; end; theorem p>1 & (for n st n>=1 holds |.seq.|.n = 1/n to_power p) implies seq is absolutely_summable proof assume p>1 & (for n st n>=1 holds |.seq.|.n = 1/n to_power p); then |.seq.| is summable by SERIES_1:36; hence thesis by Def11; end; theorem p<=1 & (for n st n>=1 holds |.seq.|.n=1/n to_power p) implies not seq is absolutely_summable proof assume p<=1 & (for n st n>=1 holds |.seq.|.n=1/n to_power p); then not |.seq.| is summable by SERIES_1:37; hence thesis by Def11; end; theorem (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 A1:(for n holds seq.n<>0c & rseq1.n=|.seq.|.(n+1)/|.seq.|.n) & rseq1 is convergent & lim rseq1 < 1; now let n; A2:seq.n<>0c & rseq1.n=|.seq.|.(n+1)/|.seq.|.n by A1; A3:0 <= |.seq.|.n & 0 <= |.seq.|.(n+1) by Lm1; A4: abs((|.seq.|)).n =abs((|.seq.|).n) by SEQ_1:16 .=|.seq.|.n by A3,ABSVALUE:def 1; A5: abs((|.seq.|)).(n+1) =abs((|.seq.|).(n+1)) by SEQ_1:16 .=|.seq.|.(n+1) by A3,ABSVALUE:def 1; A6: |.seq.|.n =|.seq.n.| by COMSEQ_1:def 14; hence |.seq.|.n <>0 & rseq1.n=|.seq.|.(n+1)/|.seq.|.n by A2,COMPLEX1:133; thus (|.seq.|).n <>0 & rseq1.n=abs((|.seq.|)).(n+1)/|.seq.|.n by A2,A5,A6,COMPLEX1:133; thus (|.seq.|).n <>0 & rseq1.n=abs((|.seq.|)).(n+1)/abs((|.seq.|)).n by A2,A4,A5,A6,COMPLEX1:133; end; then |.seq.| is absolutely_summable by A1,SERIES_1:42; then A7:abs(|.seq.|) is summable by SERIES_1:def 5; now let n; A8:0 <= |.seq.|.n by Lm1; thus abs((|.seq.|)).n =abs((|.seq.|).n) by SEQ_1:16 .=|.seq.|.n by A8,ABSVALUE:def 1; end; then abs((|.seq.|)) = |.seq.| by FUNCT_2:113; hence seq is absolutely_summable by A7,Def11; end; theorem (for n holds seq.n<>0c) & (ex m st for n st n>=m holds |.seq.|.(n+1)/|.seq.|.n >= 1) implies seq is not absolutely_summable proof assume A1: (for n holds seq.n<>0c) & (ex m st for n st n>=m holds |.seq.|.(n+1)/|.seq.|.n >= 1); A2:now let n; seq.n<>0c by A1; then |.seq.n.|<>0 by COMPLEX1:133; hence |.seq.|.n <>0 by COMSEQ_1:def 14; end; consider m such that A3:for n st n>=m holds |.seq.|.(n+1)/|.seq.|.n >= 1 by A1; now let n such that A4:n>=m; A5:0 <= |.seq.|.n & 0 <= |.seq.|.(n+1) by Lm1; A6: abs((|.seq.|)).n =abs((|.seq.|).n) by SEQ_1:16 .=|.seq.|.n by A5,ABSVALUE:def 1; abs((|.seq.|)).(n+1) =abs((|.seq.|).(n+1)) by SEQ_1:16 .=|.seq.|.(n+1) by A5,ABSVALUE:def 1; hence abs((|.seq.|)).(n+1)/abs((|.seq.|)).n >= 1 by A3,A4,A6; end; hence |.seq.| is not summable by A2,SERIES_1:44; end;

Back to top