:: Convergent Sequences and the Limit of Sequences
:: by Jaros{\l}aw Kotowicz
::
:: Received July 4, 1989
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, XREAL_0, SEQ_1, VALUED_0, FUNCT_1, ARYTM_1,
ARYTM_3, COMPLEX1, XXREAL_0, CARD_1, RELAT_1, XXREAL_2, NAT_1, ORDINAL2,
TARSKI, REAL_1, VALUED_1, SEQ_2, COMSEQ_1, XCMPLX_0, SQUARE_1;
notations TARSKI, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1,
REAL_1, NAT_1, RELAT_1, FUNCT_1, VALUED_0, VALUED_1, FUNCOP_1, SEQ_1,
XXREAL_0, SQUARE_1, COMSEQ_1, COMSEQ_2;
constructors XXREAL_0, REAL_1, NAT_1, COMPLEX1, PARTFUN1, VALUED_1, RELSET_1,
FUNCOP_1, COMSEQ_2, SQUARE_1, SEQ_1;
registrations ORDINAL1, RELSET_1, XXREAL_0, XREAL_0, MEMBERED, XBOOLE_0,
VALUED_0, VALUED_1, FUNCT_2, NUMBERS, COMSEQ_2, XCMPLX_0, SQUARE_1,
NAT_1, SEQ_1;
requirements REAL, NUMERALS, SUBSET, ARITHM;
definitions COMSEQ_2;
equalities SQUARE_1, COMPLEX1, VALUED_1;
expansions COMSEQ_2;
theorems SEQ_1, ABSVALUE, NAT_1, XREAL_0, XCMPLX_0, XCMPLX_1, XREAL_1,
COMPLEX1, XXREAL_0, VALUED_1, FUNCT_2, VALUED_0, COMSEQ_2, NUMBERS,
SQUARE_1, ORDINAL1;
schemes NAT_1;
begin
reserve n,n1,n2,m for Nat,
r,r1,r2,p,g1,g2,g for Real,
seq,seq9,seq1 for Real_Sequence,
y for set;
theorem Th1:
-g<r & r<g iff |.r.|<g
proof
thus -g<r & r<g implies |.r.|<g
proof
assume that
A1: -g<r and
A2: r<g;
A3: |.r.|<=g by A1,A2,ABSVALUE:5;
now
assume
A4: |.r.|=g;
now
assume r<0;
then g=-r by A4,ABSVALUE:def 1;
hence contradiction by A1;
end;
hence contradiction by A2,A4,ABSVALUE:def 1;
end;
hence thesis by A3,XXREAL_0:1;
end;
assume
A5: |.r.|<g;
then
A6: -g<=r by ABSVALUE:5;
A7: 0<=|.r.| by COMPLEX1:46;
A8: 0<g by A5,COMPLEX1:46;
A9: -g<-0 by A5,A7;
now
assume r=-g;
then |.r.|=--g by A9,ABSVALUE:def 1
.=g;
hence contradiction by A5;
end;
hence -g<r by A6,XXREAL_0:1;
thus thesis by A5,A8,ABSVALUE:def 1;
end;
theorem Th2:
g<>0 & r<>0 implies |.g"-r".|=|.g-r.|/(|.g.|*|.r.|)
proof
assume that
A1: g<>0 and
A2: r<>0;
thus |.g"-r".|=|.1/g-r".| by XCMPLX_1:215
.=|.1/g-1/r.| by XCMPLX_1:215
.=|.(1*r-1*g)/(g*r).| by A1,A2,XCMPLX_1:130
.=|.r-g.|/|.g*r.| by COMPLEX1:67
.=|.-(g-r).|/(|.g.|*|.r.|) by COMPLEX1:65
.=|.g-r.|/(|.g.|*|.r.|) by COMPLEX1:52;
end;
definition
let f be real-valued Function;
attr f is bounded_above means
ex r st for y being object st y in dom f holds f.y<r;
attr f is bounded_below means
ex r st for y being object st y in dom f holds r<f.y;
end;
definition
let seq;
A1: dom seq = NAT by SEQ_1:1;
redefine attr seq is bounded_above means :: redefines bounded_above (SEQ_2, definition)
:Def3:
ex r st for n holds seq.n<r;
compatibility
proof
thus seq is bounded_above implies ex r st for n holds seq.n<r
proof
given r such that
A2: for y being object st y in dom seq holds seq.y<r;
take r;
let n;
n in NAT by ORDINAL1:def 12;
hence thesis by A1,A2;
end;
given r such that
A3: for n holds seq.n<r;
take r;
let y be object;
assume y in dom seq;
hence thesis by A3;
end;
redefine attr seq is bounded_below means :: redefines bounded_below (SEQ_2, definition)
:Def4:
ex r st for n holds r<seq.n;
compatibility
proof
thus seq is bounded_below implies ex r st for n holds r < seq.n
proof
given r such that
A4: for y being object st y in dom seq holds r < seq.y;
take r;
let n;
n in NAT by ORDINAL1:def 12;
hence thesis by A1,A4;
end;
given r such that
A5: for n holds r < seq.n;
take r;
let y be object;
assume y in dom seq;
hence thesis by A5;
end;
end;
registration
cluster bounded -> bounded_above bounded_below for real-valued Function;
coherence
proof
let f be real-valued Function;
given r such that
A1: for y st y in dom f holds |.f.y.| <r;
thus f is bounded_above
proof
take r;
let y be object;
A2: f.y <= |.f.y.| by ABSVALUE:4;
assume y in dom f;
hence thesis by A1,A2,XXREAL_0:2;
end;
take -|.r.|;
let y be object;
A3: -|.f.y.| <= f.y by ABSVALUE:4;
r <= |.r.| by ABSVALUE:4;
then
A4: - |.r.| <= -r by XREAL_1:24;
assume y in dom f;
then |.f.y.| <r by A1;
then -r < -|.f.y.| by XREAL_1:24;
then -|.r.| < -|.f.y.| by A4,XXREAL_0:2;
hence thesis by A3,XXREAL_0:2;
end;
cluster bounded_above bounded_below -> bounded for real-valued Function;
coherence
proof
let f be real-valued Function;
assume f is bounded_above;
then consider r1 such that
A5: for y being object st y in dom f holds f.y<r1;
assume f is bounded_below;
then consider r2 such that
A6: for y being object st y in dom f holds r2<f.y;
take g=|.r1.|+|.r2.|+1;
A7: 0<=|.r1.| by COMPLEX1:46;
let y such that
A8: y in dom f;
r1<=|.r1.| by ABSVALUE:4;
then f.y<|.r1.| by A5,A8,XXREAL_0:2;
then f.y +0<|.r1.|+|.r2.| by COMPLEX1:46,XREAL_1:8;
then
A9: f.y<g by XREAL_1:8;
-|.r2.|<=r2 by ABSVALUE:4;
then -|.r2.|<f.y by A6,A8,XXREAL_0:2;
then -|.r1.|+-|.r2.|<0+f.y by A7,XREAL_1:8;
then
A10: -|.r1.|-|.r2.|+-1<f.y+0 by XREAL_1:8;
-|.r1.|-|.r2.|-1=-g;
hence |.f.y.|<g by A9,A10,Th1;
end;
end;
theorem Th3:
seq is bounded iff ex r st (0<r & for n holds |.seq.n.|<r)
proof
thus seq is bounded implies ex r st (0<r & for n holds |.seq.n.|<r)
proof
assume
A1: seq is bounded;
then consider r1 such that
A2: for n holds seq.n<r1 by Def3;
consider r2 such that
A3: for n holds r2<seq.n by A1,Def4;
take g=|.r1.|+|.r2.|+1;
A4: 0<=|.r1.| by COMPLEX1:46;
0<=|.r2.| by COMPLEX1:46;
hence 0<g by A4;
let n;
r1<=|.r1.| by ABSVALUE:4;
then seq.n<|.r1.| by A2,XXREAL_0:2;
then seq.n +0<|.r1.|+|.r2.| by COMPLEX1:46,XREAL_1:8;
then
A5: seq.n<g by XREAL_1:8;
-|.r2.|<=r2 by ABSVALUE:4;
then -|.r2.|<seq.n by A3,XXREAL_0:2;
then -|.r1.|+-|.r2.|<0+seq.n by A4,XREAL_1:8;
then
A6: -|.r1.|-|.r2.|+-1<seq.n+0 by XREAL_1:8;
-|.r1.|-|.r2.|-1=-g;
hence thesis by A5,A6,Th1;
end;
given r such that 0<r and
A7: for n holds |.seq.n.|<r;
take r;
let y;
assume y in dom seq;
then y is Element of NAT by FUNCT_2:def 1;
hence thesis by A7;
end;
theorem Th4:
for n ex r st (0<r & for m st m<=n holds |.seq.m.|<r)
proof
defpred X[Nat] means ex r1 st 0<r1 & for m st m<=$1 holds |.seq.m.|<r1;
A1: X[0]
proof
reconsider r=|.seq.0.|+1 as Real;
take r;
0+0<|.seq.0.|+1 by COMPLEX1:46,XREAL_1:8;
hence 0<r;
let m;
assume m<=0;
then 0=m;
then |.seq.m.|+0<r by XREAL_1:8;
hence thesis;
end;
A2: for n st X[n] holds X[n+1]
proof
let n;
given r1 such that
A3: 0<r1 and
A4: for m st m<=n holds |.seq.m.|<r1;
A5: now
assume
A6: |.seq.(n+1).|<=r1;
take r=r1+1;
thus 0<r by A3;
let m such that
A7: m<=n+1;
A8: now
assume m<=n;
then
A9: |.seq.m.|<r1 by A4;
r1+0<r by XREAL_1:8;
hence |.seq.m.|<r by A9,XXREAL_0:2;
end;
now
assume
A10: m=n+1;
r1+0<r by XREAL_1:8;
hence |.seq.m.|<r by A6,A10,XXREAL_0:2;
end;
hence |.seq.m.|<r by A7,A8,NAT_1:8;
end;
now
assume
A11: r1<=|.seq.(n+1).|;
take r=|.seq.(n+1).|+1;
0+0<r by COMPLEX1:46,XREAL_1:8;
hence 0<r;
let m such that
A12: m<=n+1;
A13: now
assume m<=n;
then |.seq.m.|<r1 by A4;
then |.seq.m.|<|.seq.(n+1).| by A11,XXREAL_0:2;
then |.seq.m.|+0<r by XREAL_1:8;
hence |.seq.m.|<r;
end;
now
assume m=n+1;
then |.seq.m.|+0<r by XREAL_1:8;
hence |.seq.m.|<r;
end;
hence |.seq.m.|<r by A12,A13,NAT_1:8;
end;
hence thesis by A5;
end;
thus for n holds X[n] from NAT_1:sch 2(A1,A2);
end;
::
:: CONVERGENT REAL SEQUENCES
:: THE LIMIT OF SEQUENCES
::
definition
::$CD
let seq;
redefine attr seq is convergent means :: redefines convergent (COMSEQ_2, definition)
ex g st for p st 0<p ex n st for m st n<=m holds |.seq.m-g.| < p;
compatibility
proof
thus seq is convergent implies
ex g st for p st 0<p ex n st for m st n<=m holds |.seq.m-g.| < p
proof assume seq is convergent;
then consider g being Complex such that
A1: for p be Real st 0<p
ex n st for m st n<=m holds |.seq.m-g.|<p;
A2: Re g+(Im g)*<i> = g by COMPLEX1:13;
now assume
A3: g is not real;
A4: Im g <> 0 by A2,A3;
set p = |.Im g.|;
A5: p > 0 by A4,COMPLEX1:47;
not ex n st for m st n<=m holds |.seq.m-g.|< p
proof let n; take n; thus n<=n;
reconsider sn = seq.n as Element of REAL by XREAL_0:def 1;
A6: Im(sn) = 0 by COMPLEX1:def 2;
A7: Im(seq.n-g) = Im(seq.n)-Im g by COMPLEX1:19;
A8: |.seq.n-g.| = sqrt ((Re(seq.n-g))^2 + (Im g)^2) by A7,A6;
(Re(seq.n-g))^2 >= 0 by XREAL_1:63;
then sqrt((Re(seq.n-g))^2+|.Im g.|^2) >= |.Im g.| by SQUARE_1:58;
hence |.seq.n-g.| >= |.Im g.| by A8,COMPLEX1:75;
end;
hence contradiction by A1,A5;
end;
then reconsider g as Real;
take g;
let p;
reconsider p as Real;
0<p implies ex n st for m st n<=m holds |.seq.m-g.| < p by A1;
hence thesis;
end;
given g such that
A9: for p st 0<p ex n st for m st n<=m holds |.seq.m-g.| < p;
g in REAL by XREAL_0:def 1;
then reconsider g as Element of COMPLEX by NUMBERS:11;
take g;
thus thesis by A9;
end;
end;
definition
let seq;
assume
A1: seq is convergent;
func lim seq -> Real means
:Def6:
for p st 0<p ex n st for m st n<=m holds |.seq.m-it.|<p;
existence by A1;
uniqueness
proof
given g1,g2 such that
A2: for p st 0<p ex n st for m st n<=m holds |.seq.m-g1.|<p and
A3: for p st 0<p ex n st for m st n<=m holds |.seq.m-g2.|<p and
A4: g1<>g2;
A5: now
assume |.g1-g2.|=0;
then 0+g2=g1-g2+g2 by ABSVALUE:2;
hence contradiction by A4;
end;
A6: 0<=|.g1-g2.| by COMPLEX1:46;
then consider n1 such that
A7: for m st n1<=m holds |.seq.m-g1.|<|.g1-g2.|/4 by A2,A5;
consider n2 such that
A8: for m st n2<=m holds |.seq.m-g2.|<|.g1-g2.|/4 by A3,A5,A6;
A9: |.seq.(n1+n2)-g1.|<|.g1-g2.|/4 by A7,NAT_1:12;
|.seq.(n1+n2)-g2.|<|.g1-g2.|/4 by A8,NAT_1:12;
then
A10: |.seq.(n1+n2)-g2.|+|.seq.(n1+n2)-g1.|<|.g1-g2.|/4+|.g1-g2.|/4
by A9,XREAL_1:8;
|.g1-g2.|=|.-(seq.(n1+n2)-g1)+(seq.(n1+n2)-g2).|;
then |.g1-g2.|<=|.-(seq.(n1+n2)-g1).|+|.seq.(n1+n2)-g2.| by COMPLEX1:56;
then
A11: |.g1-g2.|<=|.seq.(n1+n2)-g1.|+|.seq.(n1+n2)-g2.| by COMPLEX1:52;
|.g1-g2.|/2 <|.g1-g2.| by A5,A6,XREAL_1:216;
hence contradiction by A10,A11,XXREAL_0:2;
end;
end;
definition
let f be real-valued Function;
redefine attr f is bounded means :: redefines bounded (COMSEQ_2, definition)
f is bounded_above bounded_below;
compatibility;
end;
registration
cluster constant -> convergent for Real_Sequence;
coherence
proof
let seq be Real_Sequence;
assume seq is constant;
then consider r being Element of REAL such that
A1: for n being Nat holds seq.n=r by VALUED_0:def 18;
take g=r;
let p such that
A2: 0<p;
take n=0;
let m such that
n<=m;
|.(seq.m)-g.|=|.r-g.| by A1
.=0 by ABSVALUE:2;
hence thesis by A2;
end;
end;
theorem Th5:
seq is convergent & seq9 is convergent implies seq + seq9 is convergent
proof
assume that
A1: seq is convergent and
A2: seq9 is convergent;
consider g1 such that
A3: for p st 0<p ex n st for m st n<=m holds |.seq.m-g1.|<p by A1;
consider g2 such that
A4: for p st 0<p ex n st for m st n<=m holds |.seq9.m-g2.|<p by A2;
take g=g1+g2;
let p;
assume
A5: 0<p;
then consider n1 such that
A6: for m st n1<=m holds |.seq.m-g1.|<p/2 by A3;
consider n2 such that
A7: for m st n2<=m holds |.seq9.m-g2.|<p/2 by A4,A5;
take k=n1+n2;
let m such that
A8: k<=m;
n1<=n1+n2 by NAT_1:12;
then n1<=m by A8,XXREAL_0:2;
then
A9: |.seq.m-g1.|<p/2 by A6;
n2<=k by NAT_1:12;
then n2<=m by A8,XXREAL_0:2;
then |.seq9.m-g2.|<p/2 by A7;
then
A10: |.seq.m-g1.|+|.seq9.m-g2.|<p/2+p/2 by A9,XREAL_1:8;
A11: |.(seq+seq9).m-g.|=|.seq.m+seq9.m-(g1+g2).| by SEQ_1:7
.=|.seq.m-g1+(seq9.m-g2).|;
|.seq.m-g1+(seq9.m-g2).|<=|.seq.m-g1.|+|.seq9.m-g2.| by COMPLEX1:56;
hence thesis by A10,A11,XXREAL_0:2;
end;
registration
let seq1,seq2 be convergent Real_Sequence;
cluster seq1 + seq2 -> convergent for Real_Sequence;
coherence by Th5;
end;
theorem Th6:
seq is convergent & seq9 is convergent implies
lim (seq + seq9)=(lim seq)+(lim seq9)
proof
assume that
A1: seq is convergent and
A2: seq9 is convergent;
now
let p;
assume 0<p;
then
A3: 0<p/2;
then consider n1 such that
A4: for m st n1<=m holds |.seq.m-(lim seq).|<p/2 by A1,Def6;
consider n2 such that
A5: for m st n2<=m holds |.seq9.m-(lim seq9).|<p/2 by A2,A3,Def6;
take k=n1+n2;
let m such that
A6: k<=m;
n1<=n1+n2 by NAT_1:12;
then n1<=m by A6,XXREAL_0:2;
then
A7: |.seq.m-(lim seq).|<p/2 by A4;
n2<=k by NAT_1:12;
then n2<=m by A6,XXREAL_0:2;
then |.seq9.m-(lim seq9).|<p/2 by A5;
then
A8: |.seq.m-(lim seq).|+|.seq9.m-(lim seq9).|<p/2+p/2 by A7,XREAL_1:8;
A9: |.((seq+seq9).m)-((lim seq)+(lim seq9)).|
=|.seq.m+seq9.m-((lim seq)+(lim seq9)).| by SEQ_1:7
.=|.seq.m-(lim seq)+(seq9.m-(lim seq9)).|;
|.seq.m-(lim seq)+(seq9.m-(lim seq9)).|<=
|.seq.m-(lim seq).|+|.seq9.m-(lim seq9).| by COMPLEX1:56;
hence |.(seq+seq9).m-((lim seq)+(lim seq9)).|<p by A8,A9,XXREAL_0:2;
end;
hence thesis by A1,A2,Def6;
end;
theorem Th7:
seq is convergent implies r(#)seq is convergent
proof
assume seq is convergent;
then consider g1 such that
A1: for p st 0<p ex n st for m st n<=m holds |.seq.m-g1.|<p;
take g=r*g1;
A2: now
assume
A3: r=0;
let p such that
A4: 0<p;
reconsider k=0 as Nat;
take k;
let m such that k<=m;
|.((r(#)seq).m)-g.|=|.0*seq.m-0.| by A3,SEQ_1:9
.=0 by ABSVALUE:2;
hence |.((r(#)seq).m)-g.|<p by A4;
end;
now
assume
A5: r<>0;
then
A6: 0<|.r.| by COMPLEX1:47;
let p such that
A7: 0<p;
A8: 0<>|.r.| by A5,COMPLEX1:47;
consider n1 such that
A9: for m st n1<=m holds |.seq.m-g1.|<p/|.r.| by A1,A6,A7;
take k=n1;
let m;
assume k<=m;
then
A10: |.seq.m-g1.|<p/|.r.| by A9;
A11: |.((r(#)seq).m)-g.|=|.r*seq.m-r*g1.| by SEQ_1:9
.=|.r*(seq.m-g1).|
.=|.r.|*|.seq.m-g1.| by COMPLEX1:65;
|.r.|*(p/|.r.|)=|.r.|*((|.r.|)"*p) by XCMPLX_0:def 9
.=|.r.|*(|.r.|)"*p
.=1*p by A8,XCMPLX_0:def 7
.=p;
hence |.((r(#)seq).m)-g.|<p by A6,A10,A11,XREAL_1:68;
end;
hence thesis by A2;
end;
registration
let r be Real;
let seq be convergent Real_Sequence;
cluster r(#)seq -> convergent for Real_Sequence;
coherence by Th7;
end;
theorem Th8:
seq is convergent implies lim(r(#)seq)=r*(lim seq)
proof
assume
A1: seq is convergent;
A2: now
assume
A3: r=0;
let p such that
A4: 0<p;
reconsider k=0 as Nat;
take k;
let m such that k<=m;
|.((r(#)seq).m)-r*(lim seq).|=|.0*seq.m-0.| by A3,SEQ_1:9
.=0 by ABSVALUE:2;
hence |.((r(#)seq).m)-r*(lim seq).|<p by A4;
end;
now
assume
A5: r<>0;
then
A6: 0<|.r.| by COMPLEX1:47;
let p such that
A7: 0<p;
A8: 0<>|.r.| by A5,COMPLEX1:47;
0<p/|.r.| by A6,A7;
then consider n1 such that
A9: for m st n1<=m holds |.seq.m-(lim seq).|<p/|.r.| by A1,Def6;
take k=n1;
let m;
assume k<=m;
then
A10: |.seq.m-(lim seq).|<p/|.r.| by A9;
A11: |.((r(#)seq).m)-r*(lim seq).|=|.r*seq.m-r*(lim seq).| by SEQ_1:9
.=|.r*(seq.m-(lim seq)).|
.=|.r.|*|.seq.m-(lim seq).| by COMPLEX1:65;
|.r.|*(p/|.r.|)=|.r.|*((|.r.|)"*p) by XCMPLX_0:def 9
.=|.r.|*(|.r.|)"*p
.=1*p by A8,XCMPLX_0:def 7
.=p;
hence |.((r(#)seq).m)-r*(lim seq).|<p by A6,A10,A11,XREAL_1:68;
end;
hence thesis by A1,A2,Def6;
end;
theorem
seq is convergent implies -seq is convergent;
registration
let seq be convergent Real_Sequence;
cluster -seq -> convergent for Real_Sequence;
coherence;
end;
theorem Th10:
seq is convergent implies lim(-seq) = -(lim seq)
proof
assume seq is convergent;
then lim ((-1)(#)seq)=(-1)*(lim seq) by Th8;
hence thesis;
end;
theorem Th11:
seq is convergent & seq9 is convergent implies seq - seq9 is convergent
proof
assume that
A1: seq is convergent and
A2: seq9 is convergent;
-seq9 is convergent by A2;
hence thesis by A1;
end;
registration
let seq1,seq2 be convergent Real_Sequence;
cluster seq1 - seq2 -> convergent for Real_Sequence;
coherence by Th11;
end;
theorem Th12:
seq is convergent & seq9 is convergent implies
lim(seq - seq9)=(lim seq)-(lim seq9)
proof
assume that
A1: seq is convergent and
A2: seq9 is convergent;
thus lim(seq - seq9)=(lim seq)+(lim(- seq9)) by A1,A2,Th6
.=(lim seq)+-(lim seq9) by A2,Th10
.=(lim seq)-(lim seq9);
end;
theorem Th13:
seq is convergent implies seq is bounded
proof
assume seq is convergent;
then consider g such that
A1: for p st 0<p ex n st for m st n<=m holds |.seq.m-g.|<p;
consider n1 such that
A2: for m st n1<=m holds |.seq.m-g.|<1 by A1;
A3: now
take r=|.g.|+1;
0+0<r by COMPLEX1:46,XREAL_1:8;
hence 0<r;
let m;
assume n1<=m;
then
A4: |.seq.m-g.|<1 by A2;
|.seq.m.|-|.g.|<=|.seq.m-g.| by COMPLEX1:59;
then
A5: |.seq.m.|-|.g.|<1 by A4,XXREAL_0:2;
|.seq.m.|-|.g.|+|.g.|=|.seq.m.|;
hence |.seq.m.|<r by A5,XREAL_1:6;
end;
now consider r1 such that
A6: 0<r1 and
A7: for m st n1<=m holds |.seq.m.|<r1 by A3;
consider r2 such that
A8: 0<r2 and
A9: for m st m<=n1 holds |.seq.m.|<r2 by Th4;
take r=r1+r2;
thus 0<r by A6,A8;
A10: r1+0<r by A8,XREAL_1:8;
A11: 0+r2<r by A6,XREAL_1:8;
let m;
A12: now
assume n1<=m;
then |.seq.m.|<r1 by A7;
hence |.seq.m.|<r by A10,XXREAL_0:2;
end;
now
assume m<=n1;
then |.seq.m.|<r2 by A9;
hence |.seq.m.|<r by A11,XXREAL_0:2;
end;
hence |.seq.m.|<r by A12;
end;
hence thesis by Th3;
end;
registration
cluster convergent -> bounded for Real_Sequence;
coherence by Th13;
end;
theorem Th14:
seq is convergent & seq9 is convergent implies seq (#) seq9 is convergent
proof
assume that
A1: seq is convergent and
A2: seq9 is convergent;
consider g1 such that
A3: for p st 0<p ex n st for m st n<=m holds |.seq.m-g1.|<p by A1;
consider g2 such that
A4: for p st 0<p ex n st for m st n<=m holds |.seq9.m-g2.|<p by A2;
take g=g1*g2;
consider r such that
A5: 0<r and
A6: for n holds |.seq.n.|<r by A1,Th3;
A7: 0<=|.g2.| by COMPLEX1:46;
A8: 0+0<|.g2.|+r by A5,COMPLEX1:46,XREAL_1:8;
let p;
assume
A9: 0<p;
then consider n1 such that
A10: for m st n1<=m holds |.seq.m-g1.|<p/(|.g2.|+r) by A3,A8;
consider n2 such that
A11: for m st n2<=m holds |.seq9.m-g2.|<p/(|.g2.|+r) by A4,A8,A9;
take n=n1+n2;
let m such that
A12: n<=m;
A13: 0<=|.seq.m.| by COMPLEX1:46;
A14: 0<=|.seq9.m-g2.| by COMPLEX1:46;
n2<=n by NAT_1:12;
then n2<=m by A12,XXREAL_0:2;
then
A15: |.seq9.m-g2.|<p/(|.g2.|+r) by A11;
n1<=n1+n2 by NAT_1:12;
then n1<=m by A12,XXREAL_0:2;
then
A16: |.seq.m-g1.|<=p/(|.g2.|+r) by A10;
|.((seq(#)seq9).m)-g.|=|.seq.m*seq9.m-(seq.m*g2-seq.m*g2)-g1*g2.| by
SEQ_1:8
.=|.seq.m*(seq9.m-g2)+(seq.m-g1)*g2.|;
then
A17: |.((seq(#)seq9).m)-g.|<=
|.seq.m*(seq9.m-g2).|+|.(seq.m-g1)*g2.| by COMPLEX1:56;
|.seq.m.|<r by A6;
then |.seq.m.|*|.seq9.m-g2.|<r*(p/(|.g2.|+r)) by A13,A14,A15,XREAL_1:96;
then
A18: |.seq.m*(seq9.m-g2).|<r*(p/(|.g2.|+r)) by COMPLEX1:65;
|.(seq.m-g1)*g2.|=|.g2.|*|.seq.m-g1.| by COMPLEX1:65;
then
A19: |.(seq.m-g1)*g2.|<=|.g2.|*(p/(|.g2.|+r)) by A7,A16,XREAL_1:64;
r*(p/(|.g2.|+r))+|.g2.|*(p/(|.g2.|+r)) =(p/(|.g2.|+r))*(|.g2.|+r)
.=p by A8,XCMPLX_1:87;
then |.seq.m*(seq9.m-g2).|+|.(seq.m-g1)*g2.|<p by A18,A19,XREAL_1:8;
hence thesis by A17,XXREAL_0:2;
end;
registration
let seq1,seq2 be convergent Real_Sequence;
cluster seq1 (#) seq2 -> convergent for Real_Sequence;
coherence by Th14;
end;
theorem Th15:
seq is convergent & seq9 is convergent implies
lim(seq(#)seq9)=(lim seq)*(lim seq9)
proof
assume that
A1: seq is convergent and
A2: seq9 is convergent;
consider r such that
A3: 0<r and
A4: for n holds |.seq.n.|<r by A1,Th3;
A5: 0<=|.lim seq9.| by COMPLEX1:46;
A6: 0+0<|.lim seq9.|+r by A3,COMPLEX1:46,XREAL_1:8;
now
let p;
assume 0<p;
then
A7: 0<p/(|.lim seq9.|+r) by A6;
then consider n1 such that
A8: for m st n1<=m holds |.seq.m-(lim seq).|<p/(|.lim seq9.|+r) by A1,Def6;
consider n2 such that
A9: for m st n2<=m holds |.seq9.m-(lim seq9).|<p/(|.lim seq9.|+r)
by A2,A7,Def6;
take n=n1+n2;
let m such that
A10: n<=m;
A11: 0<=|.seq.m.| by COMPLEX1:46;
A12: 0<=|.seq9.m-(lim seq9).| by COMPLEX1:46;
n2<=n by NAT_1:12;
then n2<=m by A10,XXREAL_0:2;
then
A13: |.seq9.m-(lim seq9).|<p/(|.lim seq9.|+r) by A9;
n1<=n1+n2 by NAT_1:12;
then n1<=m by A10,XXREAL_0:2;
then
A14: |.seq.m-(lim seq).|<=p/(|.lim seq9.|+r) by A8;
|.((seq(#)seq9).m)-(lim seq)*(lim seq9).|
=|.seq.m*seq9.m-(seq.m*(lim seq9)-seq.m*(lim seq9))-
(lim seq)*(lim seq9).| by SEQ_1:8
.=|.seq.m*(seq9.m-(lim seq9))+
(seq.m-(lim seq))*(lim seq9).|;
then
A15: |.((seq(#)seq9).m)-(lim seq)*(lim seq9).|<=
|.seq.m*(seq9.m-(lim seq9)).|+
|.(seq.m-(lim seq))*(lim seq9).| by COMPLEX1:56;
|.seq.m.|<r by A4;
then |.seq.m.|*|.seq9.m-(lim seq9).|<r*(p/(|.lim seq9.|+r))
by A11,A12,A13,XREAL_1:96;
then
A16: |.seq.m*(seq9.m-(lim seq9)).|<r*(p/(|.lim seq9.|+r)) by COMPLEX1:65;
|.(seq.m-(lim seq))*(lim seq9).|
=|.lim seq9.|*|.seq.m-lim seq.| by COMPLEX1:65;
then
A17: |.(seq.m-(lim seq))*(lim seq9).|<=|.lim seq9.|*
(p/(|.lim seq9.|+r)) by A5,A14,XREAL_1:64;
r*(p/(|.lim seq9.|+r))+|.lim seq9.|*(p/(|.lim seq9.|+r))
=(p/(|.lim seq9.|+r))*(|.lim seq9.|+r)
.=p by A6,XCMPLX_1:87;
then |.seq.m*(seq9.m-(lim seq9)).|+|.(seq.m-(lim seq))*
(lim seq9).|<p by A16,A17,XREAL_1:8;
hence |.((seq(#)seq9).m)-(lim seq)*(lim seq9).|<p by A15,XXREAL_0:2;
end;
hence thesis by A1,A2,Def6;
end;
theorem Th16:
seq is convergent implies (lim seq<>0 implies
ex n st for m st n<=m holds |.lim seq.|/2<|.seq.m.|)
proof
assume that
A1: seq is convergent and
A2: lim seq<>0;
0<|.lim seq.| by A2,COMPLEX1:47;
then 0<|.lim seq.|/2;
then consider n1 such that
A3: for m st n1<=m holds |.seq.m-lim seq.|<|.lim seq.|/2 by A1,Def6;
take n=n1;
let m;
assume n<=m;
then
A4: |.seq.m-lim seq.|<|.lim seq.|/2 by A3;
A5: |.lim seq.|-|.seq.m.|<=|.(lim seq)-seq.m.| by COMPLEX1:59;
|.(lim seq)-seq.m.|=|.-(seq.m-(lim seq)).|
.=|.seq.m-lim seq.| by COMPLEX1:52;
then
A6: |.lim seq.|-|.seq.m.|<|.lim seq.|/2 by A4,A5,XXREAL_0:2;
A7: |.lim seq.|/2+(|.seq.m.|-|.lim seq.|/2) = |.seq.m.|;
|.lim seq.|-|.seq.m.|+(|.seq.m.|-|.lim seq.|/2) = |.lim seq.|/2;
hence thesis by A6,A7,XREAL_1:6;
end;
theorem Th17:
seq is convergent & (for n holds 0<=seq.n) implies 0<=lim seq
proof
assume that
A1: seq is convergent and
A2: for n holds 0<=seq.n and
A3: not 0<=(lim seq);
0<-(lim seq) by A3;
then consider n1 such that
A4: for m st n1<=m holds |.seq.m-lim seq.|<-(lim seq) by A1,Def6;
|.seq.n1-lim seq.|<=-(lim seq) by A4;
then seq.n1-(lim seq)<=-(lim seq) by ABSVALUE:5;
then
A5: seq.n1-(lim seq)+(lim seq)<=-(lim seq)+(lim seq) by XREAL_1:6;
now
assume seq.n1=0;
then |.seq.n1-lim seq.|=-(lim seq) by A3,ABSVALUE:def 1;
hence contradiction by A4;
end;
hence contradiction by A2,A5;
end;
theorem
seq is convergent & seq9 is convergent &
(for n holds seq.n<=(seq9.n)) implies (lim seq)<=(lim seq9)
proof
assume that
A1: seq is convergent and
A2: seq9 is convergent and
A3: for n holds seq.n<=(seq9.n);
now
let n;
seq.n<=seq9.n by A3;
then
A4: seq.n-seq.n<=seq9.n-seq.n by XREAL_1:9;
(seq9-seq).n=seq9.n+(-seq).n by SEQ_1:7
.=seq9.n+-seq.n by SEQ_1:10
.=seq9.n-seq.n;
hence 0<=(seq9-seq).n by A4;
end;
then
A5: 0<=lim(seq9-seq) by A1,A2,Th17;
lim (seq9-seq)=(lim seq9)- (lim seq) by A1,A2,Th12;
then 0+(lim seq)<=(lim seq9)-(lim seq)+(lim seq) by A5,XREAL_1:6;
hence thesis;
end;
theorem Th19:
seq is convergent & seq9 is convergent &
(for n holds seq.n<=(seq1.n) & seq1.n<=seq9.n) & (lim seq)=(lim seq9)
implies seq1 is convergent
proof
assume that
A1: seq is convergent and
A2: seq9 is convergent and
A3: for n holds seq.n<=(seq1.n) & seq1.n<=seq9.n and
A4: (lim seq)=(lim seq9);
take lim seq;
let p;
assume
A5: 0<p;
then consider n1 such that
A6: for m st n1<=m holds |.seq.m-lim seq.|<p by A1,Def6;
consider n2 such that
A7: for m st n2<=m holds |.seq9.m-(lim seq).|<p by A2,A4,A5,Def6;
take n=n1+n2;
let m such that
A8: n<=m;
n2<=n by NAT_1:12;
then n2<=m by A8,XXREAL_0:2;
then |.seq9.m-(lim seq).|<p by A7;
then
A9: seq9.m-(lim seq)<p by Th1;
n1<=n1+n2 by NAT_1:12;
then n1<=m by A8,XXREAL_0:2;
then |.seq.m-lim seq.|<p by A6;
then
A10: -p<seq.m-(lim seq) by Th1;
seq.m<=seq1.m by A3;
then seq.m-(lim seq)<=seq1.m-(lim seq) by XREAL_1:9;
then
A11: -p<seq1.m-(lim seq) by A10,XXREAL_0:2;
seq1.m<=seq9.m by A3;
then seq1.m-(lim seq)<=seq9.m-(lim seq) by XREAL_1:9;
then seq1.m-(lim seq)<p by A9,XXREAL_0:2;
hence thesis by A11,Th1;
end;
theorem
seq is convergent & seq9 is convergent &
(for n holds seq.n<=(seq1.n) & seq1.n<=seq9.n) &
lim seq = lim seq9 implies lim seq1 = lim seq
proof
assume that
A1: seq is convergent and
A2: seq9 is convergent and
A3: for n holds seq.n<=(seq1.n) & seq1.n<=seq9.n and
A4: lim seq = lim seq9;
A5: seq1 is convergent by A1,A2,A3,A4,Th19;
now
let p;
assume
A6: 0<p;
then consider n1 such that
A7: for m st n1<=m holds |.seq.m-lim seq.|<p by A1,Def6;
consider n2 such that
A8: for m st n2<=m holds |.seq9.m-lim seq.|<p by A2,A4,A6,Def6;
take n=n1+n2;
let m such that
A9: n<=m;
n2<=n by NAT_1:12;
then n2<=m by A9,XXREAL_0:2;
then |.seq9.m-lim seq.|<p by A8;
then
A10: seq9.m-(lim seq)<p by Th1;
n1<=n1+n2 by NAT_1:12;
then n1<=m by A9,XXREAL_0:2;
then |.seq.m-lim seq.|<p by A7;
then
A11: -p<seq.m-(lim seq) by Th1;
seq.m<=seq1.m by A3;
then seq.m-(lim seq)<=seq1.m-(lim seq) by XREAL_1:9;
then
A12: -p<seq1.m-(lim seq) by A11,XXREAL_0:2;
seq1.m<=seq9.m by A3;
then seq1.m-(lim seq)<=seq9.m-(lim seq) by XREAL_1:9;
then seq1.m-(lim seq)<p by A10,XXREAL_0:2;
hence |.seq1.m-(lim seq).|<p by A12,Th1;
end;
hence thesis by A5,Def6;
end;
theorem Th21:
seq is convergent & lim seq <> 0 & seq is non-zero implies seq" is convergent
proof
assume that
A1: seq is convergent and
A2: lim seq<>0 and
A3: seq is non-zero;
A4: 0<|.lim seq.| by A2,COMPLEX1:47;
A5: 0<>|.lim seq.| by A2,COMPLEX1:47;
consider n1 such that
A6: for m st n1<=m holds |.lim seq.|/2<|.seq.m.| by A1,A2,Th16;
0*0<|.lim seq.|*|.lim seq.| by A4;
then
A7: 0<(|.lim seq.|*|.lim seq.|)/2;
take (lim seq)";
let p;
assume
A8: 0<p;
then 0*0<p*((|.lim seq.|*|.lim seq.|)/2) by A7;
then consider n2 such that
A9: for m st n2<=m holds
|.seq.m-lim seq.|<p*((|.lim seq.|*|.lim seq.|)/2) by A1,Def6;
take n=n1+n2;
let m such that
A10: n<=m;
n2<=n by NAT_1:12;
then n2<=m by A10,XXREAL_0:2;
then
A11: |.seq.m-lim seq.|<p*((|.lim seq.|*|.lim seq.|)/2) by A9;
n1<=n1+n2 by NAT_1:12;
then n1<=m by A10,XXREAL_0:2;
then
A12: |.lim seq.|/2<|.seq.m.| by A6;
A13: seq.m<>0 by A3,SEQ_1:5;
then seq.m*(lim seq)<>0 by A2;
then 0<|.seq.m*(lim seq).| by COMPLEX1:47;
then 0<|.seq.m.|*|.lim seq.| by COMPLEX1:65;
then
A14: |.seq.m-lim seq.|/(|.seq.m.|*|.lim seq.|)<
(p*((|.lim seq.|*|.lim seq.|)/2))/(|.seq.m.|*|.lim seq.|)
by A11,XREAL_1:74;
A15: (p*((|.lim seq.|*|.lim seq.|)/2))/(|.seq.m.|*|.lim seq.|)
=(p*(2"*(|.lim seq.|*|.lim seq.|)))*
(|.seq.m.|*|.lim seq.|)" by XCMPLX_0:def 9
.=p*2"*((|.lim seq.|*|.lim seq.|)*(|.lim seq.|*|.seq.m.|)")
.=p*2"*((|.lim seq.|*|.lim seq.|)*
(|.lim seq.|"*(|.seq.m.|)")) by XCMPLX_1:204
.=p*2"*(|.lim seq.|*(|.lim seq.|*|.lim seq.|")*|.seq.m.|")
.=p*2"*(|.lim seq.|*1*(|.seq.m.|)") by A5,XCMPLX_0:def 7
.=p*(|.lim seq.|/2)*|.seq.m.|"
.=(p*(|.lim seq.|/2))/|.seq.m.| by XCMPLX_0:def 9;
A16: |.(seq").m-(lim seq)".|=|.(seq.m)"-(lim seq)".| by VALUED_1:10
.=|.seq.m-lim seq.|/(|.seq.m.|*|.lim seq.|) by A2,A13,Th2;
A17: 0<|.lim seq.|/2 by A4;
A18: 0<>|.lim seq.|/2 by A2,COMPLEX1:47;
0*0<p*(|.lim seq.|/2) by A8,A17;
then
A19: (p*(|.lim seq.|/2))/|.seq.m.|<
(p*(|.lim seq.|/2))/(|.lim seq.|/2) by A12,A17,XREAL_1:76;
(p*(|.lim seq.|/2))/(|.lim seq.|/2 )
=(p*(|.lim seq.|/2))*(|.lim seq.|/2 )" by XCMPLX_0:def 9
.=p*((|.lim seq.|/2)*(|.lim seq.|/2 )")
.=p*1 by A18,XCMPLX_0:def 7
.=p;
hence thesis by A14,A15,A16,A19,XXREAL_0:2;
end;
theorem Th22:
seq is convergent & lim seq <> 0 & seq is non-zero
implies lim seq"=(lim seq)"
proof
assume that
A1: seq is convergent and
A2: (lim seq)<>0 and
A3: seq is non-zero;
A4: seq" is convergent by A1,A2,A3,Th21;
A5: 0<|.lim seq.| by A2,COMPLEX1:47;
A6: 0<>|.lim seq.| by A2,COMPLEX1:47;
consider n1 such that
A7: for m st n1<=m holds |.lim seq.|/2<|.seq.m.| by A1,A2,Th16;
0*0<|.lim seq.|*|.lim seq.| by A5;
then
A8: 0<(|.lim seq.|*|.lim seq.|)/2;
now
let p;
assume
A9: 0<p;
then 0*0<p*((|.lim seq.|*|.lim seq.|)/2) by A8;
then consider n2 such that
A10: for m st n2<=m holds
|.seq.m-lim seq.|<p*((|.lim seq.|*|.lim seq.|)/2) by A1,Def6;
take n=n1+n2;
let m such that
A11: n<=m;
n2<=n by NAT_1:12;
then n2<=m by A11,XXREAL_0:2;
then
A12: |.seq.m-lim seq.|<p*((|.lim seq.|*|.lim seq.|)/2) by A10;
n1<=n1+n2 by NAT_1:12;
then n1<=m by A11,XXREAL_0:2;
then
A13: |.lim seq.|/2<|.seq.m.| by A7;
A14: seq.m<>0 by A3,SEQ_1:5;
then seq.m*(lim seq)<>0 by A2;
then 0<|.seq.m*(lim seq).| by COMPLEX1:47;
then 0<|.seq.m.|*|.lim seq.| by COMPLEX1:65;
then
A15: |.seq.m-lim seq.|/(|.seq.m.|*|.lim seq.|)<
(p*((|.lim seq.|*|.lim seq.|)/2))/(|.seq.m.|*|.lim seq.|)
by A12,XREAL_1:74;
A16: (p*((|.lim seq.|*|.lim seq.|)/2))/(|.seq.m.|*|.lim seq.|)
=(p*(2"*(|.lim seq.|*|.lim seq.|)))*
(|.seq.m.|*|.lim seq.|)" by XCMPLX_0:def 9
.=p*2"*((|.lim seq.|*|.lim seq.|)*(|.lim seq.|*|.seq.m.|)")
.=p*2"*((|.lim seq.|*|.lim seq.|)*
((|.lim seq.|)"*(|.seq.m.|)")) by XCMPLX_1:204
.=p*2"*(|.lim seq.|*(|.lim seq.|*|.lim seq.|")*|.seq.m.|")
.=p*2"*(|.lim seq.|*1*|.seq.m.|") by A6,XCMPLX_0:def 7
.=p*(|.lim seq.|/2)*|.seq.m.|"
.=(p*(|.lim seq.|/2))/|.seq.m.| by XCMPLX_0:def 9;
A17: |.(seq").m-(lim seq)".|=|.(seq.m)"-(lim seq)".| by VALUED_1:10
.=|.seq.m-lim seq.|/(|.seq.m.|*|.lim seq.|) by A2,A14,Th2;
A18: 0<|.lim seq.|/2 by A5;
A19: 0<>|.lim seq.|/2 by A2,COMPLEX1:47;
0*0<p*(|.lim seq.|/2) by A9,A18;
then
A20: (p*(|.lim seq.|/2))/|.seq.m.|<
(p*(|.lim seq.|/2))/(|.lim seq.|/2) by A13,A18,XREAL_1:76;
(p*(|.lim seq.|/2))/(|.lim seq.|/2 )
=(p*(|.lim seq.|/2))*(|.lim seq.|/2 )" by XCMPLX_0:def 9
.=p*((|.lim seq.|/2)*(|.lim seq.|/2 )")
.=p*1 by A19,XCMPLX_0:def 7
.=p;
hence |.(seq").m-(lim seq)".|<p by A15,A16,A17,A20,XXREAL_0:2;
end;
hence thesis by A4,Def6;
end;
theorem
seq9 is convergent & seq is convergent & lim seq <> 0
& seq is non-zero implies seq9/"seq is convergent
proof
assume that
A1: seq9 is convergent and
A2: seq is convergent and
A3: (lim seq)<>0 and
A4: seq is non-zero;
seq" is convergent by A2,A3,A4,Th21;
hence thesis by A1;
end;
theorem
seq9 is convergent & seq is convergent & lim seq <> 0
& seq is non-zero implies lim(seq9/"seq)=(lim seq9)/(lim seq)
proof
assume that
A1: seq9 is convergent and
A2: seq is convergent and
A3: (lim seq)<>0 and
A4: seq is non-zero;
seq" is convergent by A2,A3,A4,Th21;
then lim (seq9(#)(seq"))=(lim seq9)*(lim seq") by A1,Th15
.=(lim seq9)*(lim seq)" by A2,A3,A4,Th22
.=(lim seq9)/(lim seq) by XCMPLX_0:def 9;
hence thesis;
end;
theorem Th25:
seq is convergent & seq1 is bounded & lim seq=0 implies
seq(#)seq1 is convergent
proof
assume that
A1: seq is convergent and
A2: seq1 is bounded and
A3: lim seq=0;
reconsider g1=0 as Real;
take g=g1;
let p such that
A4: 0<p;
consider r such that
A5: 0<r and
A6: for m holds |.seq1.m.|<r by A2,Th3;
A7: 0<p/r by A4,A5;
then consider n1 such that
A8: for m st n1<=m holds |.seq.m-0.|<p/r by A1,A3,Def6;
take n=n1;
let m such that
A9: n<=m;
|.seq.m.|=|.seq.m-0.|;
then
A10: |.seq.m.|<p/r by A8,A9;
A11: |.((seq(#)seq1).m)-g.|=|.seq.m*seq1.m-0.| by SEQ_1:8
.=|.seq.m.|*|.seq1.m.| by COMPLEX1:65;
now
assume
A12: |.seq1.m.|<>0;
(p/r)*r=p*r"*r by XCMPLX_0:def 9
.=p*(r"*r)
.=p*1 by A5,XCMPLX_0:def 7
.=p;
then
A13: (p/r)*|.seq1.m.|<p by A6,A7,XREAL_1:68;
0<=|.seq1.m.| by COMPLEX1:46;
then |.((seq(#)seq1).m)-g.|<(p/r)*|.seq1.m.| by A10,A11,A12,XREAL_1:68;
hence thesis by A13,XXREAL_0:2;
end;
hence thesis by A4,A11;
end;
theorem
seq is convergent & seq1 is bounded & lim seq=0 implies lim(seq(#)seq1)=0
proof
assume that
A1: seq is convergent and
A2: seq1 is bounded and
A3: lim seq=0;
A4: seq(#)seq1 is convergent by A1,A2,A3,Th25;
now
let p such that
A5: 0<p;
consider r such that
A6: 0<r and
A7: for m holds |.seq1.m.|<r by A2,Th3;
A8: 0<p/r by A5,A6;
then consider n1 such that
A9: for m st n1<=m holds |.seq.m-0.|<p/r by A1,A3,Def6;
take n=n1;
let m;
assume n<=m;
then
A10: |.seq.m-0.|<p/r by A9;
A11: |.((seq(#)seq1).m)-0.|=|.seq.m*seq1.m-0.| by SEQ_1:8
.=|.seq.m.|*|.seq1.m.| by COMPLEX1:65;
now
assume
A12: |.seq1.m.|<>0;
(p/r)*r=p*r"*r by XCMPLX_0:def 9
.=p*(r"*r)
.=p*1 by A6,XCMPLX_0:def 7;
then
A13: (p/r)*|.seq1.m.|<p by A7,A8,XREAL_1:68;
0<=|.seq1.m.| by COMPLEX1:46;
then |.((seq(#)seq1).m)-0.|<(p/r)*|.seq1.m.| by A10,A11,A12,XREAL_1:68;
hence |.((seq(#)seq1).m)-0.|<p by A13,XXREAL_0:2;
end;
hence |.((seq(#)seq1).m)-0.|<p by A5,A11;
end;
hence thesis by A4,Def6;
end;
:: from COMSEQ_2, 2011.07.10, A.T.
reserve g for Complex;
registration
let s be convergent Complex_Sequence;
cluster |.s.| -> convergent for Real_Sequence;
coherence
proof
|.s.| is convergent
proof
consider g such that
A1: for p be Real st 0<p ex n st for m st n<=m holds |.s.m-g.|<p
by COMSEQ_2:def 5;
take |.g.|;
let p be Real;
assume
A2: 0<p;
consider n such that
A3: for m st n<=m holds |.s.m-g.|<p by A1,A2;
take n;
let m;
assume n<=m;
then |.s.m-g.|<p by A3;
then |.|.s.m.|- |.g.|.| + |.s.m-g.| < p+|.s.m-g.| by COMPLEX1:64
,XREAL_1:8;
then
|.|.s.m.|- |.g.|.| + |.s.m-g.|- |.s.m-g.| < p+|.s.m-g.|- |.s.m-g.|
by XREAL_1:9;
hence thesis by VALUED_1:18;
end;
hence thesis;
end;
end;
reserve s,s1,s9 for Complex_Sequence;
theorem Th27:
s is convergent implies lim |.s.| = |.lim s.|
proof
set g = lim s;
assume
A1: s is convergent;
then reconsider s1 = s as convergent Complex_Sequence;
reconsider w = |.s1.| as Real_Sequence;
A2: w is convergent;
reconsider w = |.lim s.| as Real;
now
let p be Real;
assume
A3: 0<p;
consider n such that
A4: for m st n<=m holds |.s.m-g.|<p by A1,A3,COMSEQ_2:def 6;
take n;
let m;
assume n<=m;
then |.s.m-g.|<p by A4;
then |.|.s.m.|- |.g.|.| + |.s.m-g.| < p+|.s.m-g.|
by COMPLEX1:64,XREAL_1:8;
then |.|.s.m.|- |.g.|.| + |.s.m-g.|- |.s.m-g.| < p+|.s.m-g.|- |.s.m-g.|
by XREAL_1:9;
hence |.|.s.|.m - w.| < p by VALUED_1:18;
end;
hence thesis by A2,Def6;
end;
theorem
for s,s9 being convergent Complex_Sequence
holds lim |.(s + s9).| = |.(lim s)+(lim s9).|
proof
let s,s9 be convergent Complex_Sequence;
thus lim |.(s + s9).| = |.lim (s + s9).| by Th27
.= |.(lim s)+(lim s9).| by COMSEQ_2:14;
end;
theorem
for s being convergent Complex_Sequence
holds lim |.(r(#)s).| = |.r.|*|.(lim s).|
proof
let s being convergent Complex_Sequence;
thus lim |.(r(#)s).| = |.lim (r(#)s).| by Th27
.= |.r*(lim s).| by COMSEQ_2:18
.= |.r.|*|.(lim s).| by COMPLEX1:65;
end;
theorem
for s being convergent Complex_Sequence
holds lim |.-s.| = |.lim s.|
proof
let s being convergent Complex_Sequence;
thus lim |.-s.| = |.lim (-s).| by Th27
.= |.-(lim s).| by COMSEQ_2:22
.= |.lim s.| by COMPLEX1:52;
end;
theorem
for s,s9 being convergent Complex_Sequence
holds lim |.s - s9.| = |.(lim s) - (lim s9).|
proof
let s,s9 be convergent Complex_Sequence;
thus lim |.s - s9.| = |.lim (s - s9).| by Th27
.= |.(lim s) - (lim s9).| by COMSEQ_2:26;
end;
theorem
for s,s9 being convergent Complex_Sequence
holds lim |.s(#)s9.| = |.lim s.|*|.lim s9.|
proof
let s,s9 be convergent Complex_Sequence;
thus lim |.s(#)s9.| = |.lim (s(#)s9).| by Th27
.= |.(lim s)*(lim s9).| by COMSEQ_2:30
.= |.lim s.|*|.lim s9.| by COMPLEX1:65;
end;
theorem
s is convergent & (lim s)<>0c & s is non-zero implies lim |.s".| = (|.
lim s.|)"
proof
assume
A1: s is convergent & (lim s)<>0c & s is non-zero;
then s" is convergent by COMSEQ_2:34;
hence lim |.s".| = |.lim s".| by Th27
.= |.(lim s)".| by A1,COMSEQ_2:35
.= (|.lim s.|)" by COMPLEX1:66;
end;
theorem
s9 is convergent & s is convergent & (lim s)<>0c & s is non-zero
implies lim |.(s9/"s).|=|.(lim s9).|/|.(lim s).|
proof
assume
A1: s9 is convergent & s is convergent & (lim s)<>0c & s is non-zero;
then s9/"s is convergent by COMSEQ_2:38;
hence lim |.s9/"s.| = |.lim (s9/"s).| by Th27
.= |.(lim s9)/(lim s).| by A1,COMSEQ_2:39
.= |.(lim s9).|/|.(lim s).| by COMPLEX1:67;
end;
theorem
s is convergent & s1 is bounded & (lim s)=0c implies lim |.s(#)s1.| = 0
proof
assume
A1: s is convergent & s1 is bounded & (lim s)=0c;
then s(#)s1 is convergent by COMSEQ_2:42;
hence lim |.s(#)s1.| = |.(lim (s(#)s1)).| by Th27
.= 0 by A1,COMPLEX1:44,COMSEQ_2:43;
end;