:: Sequences in $R^n$
:: by Agnieszka Sakowicz , Jaros{\l}aw Gryko and Adam Grabowski
::
:: Received May 10, 1994
:: Copyright (c) 1994-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, SEQ_1, NAT_1, EUCLID, REAL_1, PRE_TOPC,
FUNCT_1, RELAT_1, VALUED_0, TARSKI, STRUCT_0, SUPINF_2, ARYTM_3, ARYTM_1,
COMPLEX1, VALUED_1, CARD_1, XXREAL_0, XXREAL_2, SEQ_2, ORDINAL2,
XBOOLE_0, PARTFUN1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, RELAT_1, FUNCT_1,
VALUED_1, PARTFUN1, COMPLEX1, REAL_1, PRE_TOPC, XXREAL_0, XCMPLX_0,
XREAL_0, NAT_1, SEQ_1, STRUCT_0, RLVECT_1, VFUNCT_1, EUCLID;
constructors REAL_1, COMPLEX1, MONOID_0, EUCLID, RELSET_1, BINOP_2, VFUNCT_1;
registrations ORDINAL1, RELSET_1, XXREAL_0, XREAL_0, MEMBERED, STRUCT_0,
MONOID_0, EUCLID, XBOOLE_0, VALUED_1, FUNCT_2, NUMBERS, VALUED_0, NAT_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions FUNCT_2;
equalities STRUCT_0, RLVECT_1;
theorems FUNCT_1, FUNCT_2, TARSKI, EUCLID, SEQ_1, NAT_1, XBOOLE_0, NORMSP_1,
XCMPLX_0, XREAL_1, COMPLEX1, XXREAL_0, VFUNCT_1, ORDINAL1, RLVECT_1;
schemes SEQ_1, NAT_1;
begin
definition
let N be Nat;
mode Real_Sequence of N is sequence of TOP-REAL N;
end;
reserve N for Nat;
reserve n,m,n1,n2 for Nat;
reserve q,r,r1,r2 for Real;
reserve x,y for set;
reserve w,w1,w2,g,g1,g2 for Point of TOP-REAL N;
reserve seq,seq1,seq2,seq3,seq9 for Real_Sequence of N;
theorem Th1:
for f being Function holds f is Real_Sequence of N iff (dom f=NAT
& for n holds f.n is Point of TOP-REAL N)
proof
let f be Function;
thus f is Real_Sequence of N implies
(dom f=NAT & for n being Nat holds f.n is Point
of TOP-REAL N)
by NORMSP_1:12,ORDINAL1:def 12;
assume that
A1: dom f=NAT and
A2: for n holds f.n is Point of TOP-REAL N;
for x holds x in NAT implies f.x is Point of TOP-REAL N by A2;
hence thesis by A1,NORMSP_1:12;
end;
definition
let N;
let IT be Real_Sequence of N;
attr IT is non-zero means
rng IT c= NonZero TOP-REAL N;
end;
theorem Th2:
seq is non-zero iff for x st x in NAT holds seq.x<>0.TOP-REAL N
proof
thus seq is non-zero implies for x st x in NAT holds seq.x<>0.TOP-REAL N
proof
assume seq is non-zero;
then
A1: rng seq c= NonZero TOP-REAL N;
let x;
assume x in NAT;
then x in dom seq by Th1;
then seq.x in rng seq by FUNCT_1:def 3;
then not seq.x in {0.TOP-REAL N} by A1,XBOOLE_0:def 5;
hence thesis by TARSKI:def 1;
end;
assume
A2: for x st x in NAT holds seq.x<>0.TOP-REAL N;
now
let y be object;
assume y in rng seq;
then consider x being object such that
A3: x in dom seq and
A4: seq.x=y by FUNCT_1:def 3;
A5: x in NAT by A3,NORMSP_1:12;
then y<>0.TOP-REAL N by A2,A4;
then
A6: not y in {0.TOP-REAL N} by TARSKI:def 1;
y is Point of TOP-REAL N by A4,A5,NORMSP_1:12;
hence y in NonZero TOP-REAL N by A6,XBOOLE_0:def 5;
end;
then rng seq c= NonZero TOP-REAL N by TARSKI:def 3;
hence thesis;
end;
theorem Th3:
seq is non-zero iff for n holds seq.n<>0.TOP-REAL N
proof
thus seq is non-zero implies for n holds seq.n<>0.TOP-REAL N
by ORDINAL1:def 12,Th2;
assume for n holds seq.n<>0.TOP-REAL N;
then for x holds x in NAT implies seq.x<>0.TOP-REAL N;
hence thesis by Th2;
end;
definition
let N be Nat,seq1,seq2 be Real_Sequence of N;
func seq1 + seq2 -> Real_Sequence of N equals
seq1 + seq2;
coherence
proof
A1: dom seq1 = NAT & dom seq2 = NAT by FUNCT_2:def 1;
dom (seq1+seq2) = dom seq1 /\ dom seq2 by VFUNCT_1:def 1;
hence thesis by A1,FUNCT_2:67;
end;
end;
definition
let r be Real;
let N be Nat,seq be Real_Sequence of N;
func r * seq -> Real_Sequence of N equals
r(#)seq;
coherence
proof
A1: dom seq = NAT by FUNCT_2:def 1;
dom (r(#)seq) = dom seq by VFUNCT_1:def 4;
hence thesis by A1,FUNCT_2:67;
end;
end;
definition
let N be Nat,seq be Real_Sequence of N;
func - seq -> Real_Sequence of N equals
- seq;
coherence
proof
A1: dom seq = NAT by FUNCT_2:def 1;
dom (-seq) = dom seq by VFUNCT_1:def 5;
hence thesis by A1,FUNCT_2:67;
end;
end;
definition
let N be Nat,seq1,seq2 be Real_Sequence of N;
func seq1 - seq2 -> Real_Sequence of N equals
seq1 +- seq2;
correctness;
end;
definition
let N be Nat,seq be Real_Sequence of N;
func |.seq.| -> Real_Sequence means
:Def6:
for n being Nat holds it.n = |.seq.n.|;
existence
proof
deffunc U(Nat) = |.seq.$1.|;
thus ex s being Real_Sequence st
for n being Nat holds s.n= U(n) from SEQ_1:sch 1;
end;
uniqueness
proof
let seq8,seq9 be Real_Sequence such that
A1: for n being Nat holds seq8.n=|.seq.n.| and
A2: for n being Nat holds seq9.n=|.seq.n.|;
let n be Element of NAT;
seq9.n=|.seq.n.| by A2;
hence seq8.n=seq9.n by A1;
end;
end;
theorem Th4:
for N,n be Nat,seq1,seq2 be Real_Sequence of N holds
(seq1+seq2).n = seq1.n + seq2.n
proof
let N,n be Nat,seq1,seq2 be Real_Sequence of N;
reconsider m = n as Element of NAT by ORDINAL1:def 12;
A1: dom(seq1+seq2) = NAT by FUNCT_2:def 1;
thus (seq1+seq2).n = (seq1+seq2)/.m
.= seq1/.m + seq2/.m by A1,VFUNCT_1:def 1
.= seq1.n + seq2.n;
end;
theorem Th5:
for N,n be Nat,seq be Real_Sequence of N holds
(r*seq).n = r*seq.n
proof
let N,n be Nat,seq be Real_Sequence of N;
reconsider m = n as Element of NAT by ORDINAL1:def 12;
A1: dom(r*seq) = NAT by FUNCT_2:def 1;
thus (r*seq).n = (r*seq)/.m
.= r*seq/.m by A1,VFUNCT_1:def 4
.= r*seq.n;
end;
theorem Th6:
for N,n be Nat,seq be Real_Sequence of N holds
(-seq).n = -seq.n
proof
let N,n be Nat,seq be Real_Sequence of N;
reconsider m = n as Element of NAT by ORDINAL1:def 12;
A1: dom(-seq) = NAT by FUNCT_2:def 1;
thus (-seq).n = (-seq)/.m
.= -seq/.m by A1,VFUNCT_1:def 5
.= -seq.n;
end;
theorem Th7:
|.r.|*|.w.| = |.r*w.| by EUCLID:11;
theorem
|.r*seq.| = |.r.|(#)|.seq.|
proof
let n be Element of NAT;
thus |.r*seq.|.n=|.(r*seq).n.| by Def6
.=|.r*(seq.n).| by Th5
.=|.r.|*|.seq.n.| by Th7
.=|.r.|*(|.seq.|).n by Def6
.=(|.r.|(#)|.seq.|).n by SEQ_1:9;
end;
theorem
seq1 + seq2 = seq2 + seq1;
theorem Th10:
(seq1 + seq2) + seq3 = seq1 + (seq2 + seq3)
proof
let n be Element of NAT;
thus ((seq1+seq2)+seq3).n = (seq1+seq2).n+ seq3.n by Th4
.= seq1.n+seq2.n+seq3.n by Th4
.=seq1.n+(seq2.n+seq3.n) by RLVECT_1:def 3
.=seq1.n+(seq2+seq3).n by Th4
.=(seq1+(seq2+seq3)).n by Th4;
end;
theorem Th11:
-seq = (-1)*seq
proof
let n be Element of NAT;
thus ((-1)*seq).n=(-1)*seq.n by Th5
.=-seq.n by RLVECT_1:16
.=(-seq).n by Th6;
end;
theorem Th12:
r*(seq1 + seq2) = r*seq1 + r*seq2
proof
let n be Element of NAT;
thus (r*(seq1 + seq2)).n=r*(seq1+seq2).n by Th5
.=r*(seq1.n+seq2.n) by Th4
.=r*seq1.n+r*seq2.n by RLVECT_1:def 5
.=(r*seq1).n+r*seq2.n by Th5
.=(r*seq1).n+(r*seq2).n by Th5
.=((r*seq1)+(r*seq2)).n by Th4;
end;
theorem Th13:
(r*q)*seq = r*(q*seq)
proof
let n be Element of NAT;
thus ((r*q)*seq).n=(r*q)*seq.n by Th5
.=r*(q*seq.n) by RLVECT_1:def 7
.=r*(q*seq).n by Th5
.=(r*(q*seq)).n by Th5;
end;
theorem Th14:
r*(seq1 - seq2) = r*seq1 - r*seq2
proof
thus r*(seq1-seq2)=r*seq1+r*(-seq2) by Th12
.=r*seq1+r*((-1)*seq2) by Th11
.=r*seq1+((-1)*r)*seq2 by Th13
.=r*seq1+(-1)*(r*seq2) by Th13
.=r*seq1-(r*seq2) by Th11;
end;
theorem
seq1 - (seq2 + seq3) = seq1 - seq2 - seq3
proof
thus seq1-(seq2+seq3)=seq1+(-1)*(seq2+seq3) by Th11
.=seq1+((-1)*seq2+(-1)*seq3) by Th12
.=seq1+(-seq2+(-1)*seq3) by Th11
.=seq1+(-seq2+-seq3) by Th11
.=seq1-seq2-seq3 by Th10;
end;
theorem Th16:
1*seq=seq
proof
let n be Element of NAT;
thus (1*seq).n=1*seq.n by Th5
.=seq.n by RLVECT_1:def 8;
end;
theorem Th17:
-(-seq) = seq
proof
thus -(-seq)=(-1)*(-seq) by Th11
.=(-1)*((-1)*seq) by Th11
.=((-1)*(-1))*seq by Th13
.=seq by Th16;
end;
theorem
seq1 - (-seq2) = seq1 + seq2 by Th17;
theorem
seq1 - (seq2 - seq3) = seq1 - seq2 + seq3
proof
thus seq1-(seq2-seq3)=seq1+(-1)*(seq2-seq3) by Th11
.=seq1+((-1)*seq2-((-1)*seq3)) by Th14
.=seq1+(-seq2-((-1)*seq3)) by Th11
.=seq1+(-seq2-(-seq3)) by Th11
.=seq1+(-seq2+seq3) by Th17
.=seq1-seq2+seq3 by Th10;
end;
theorem
seq1 + (seq2 - seq3) = seq1 + seq2 - seq3 by Th10;
theorem Th21:
r <> 0 & seq is non-zero implies r*seq is non-zero
proof
assume that
A1: r<>0 and
A2: seq is non-zero and
A3: not r*seq is non-zero;
consider n1 such that
A4: (r*seq).n1=0.TOP-REAL N by A3,Th3;
A5: seq.n1 <> 0.TOP-REAL N by A2,Th3;
r*seq.n1=0.TOP-REAL N by A4,Th5;
hence contradiction by A1,A5,RLVECT_1:11;
end;
theorem
seq is non-zero implies -seq is non-zero
proof
assume seq is non-zero;
then (-1)*seq is non-zero by Th21;
hence thesis by Th11;
end;
theorem Th23:
|.0.TOP-REAL N.| = 0
proof
thus |.0.TOP-REAL N.| = |.0*N.| by EUCLID:70
.= 0 by EUCLID:7;
end;
theorem Th24:
|.w.| = 0 implies w = 0.TOP-REAL N
proof
reconsider s = w as Element of REAL N by EUCLID:22;
assume |.w.| = 0;
then s = 0*N by EUCLID:8
.= 0.TOP-REAL N by EUCLID:70;
hence thesis;
end;
theorem
|.w.| >= 0;
theorem
|.-w.| = |.w.| by EUCLID:71;
theorem Th27:
|.w1 - w2.| = |.w2 - w1.|
proof
thus |.w1 - w2.| = |.-(w1 - w2).| by EUCLID:71
.= |.w2 - w1.| by RLVECT_1:33;
end;
Lm1: |.w1 - w2.| = 0 implies w1 = w2
proof
assume |.w1 - w2.| = 0;
then w1 - w2 = 0.TOP-REAL N by Th24;
hence thesis by RLVECT_1:21;
end;
Lm2: w1 = w2 implies |.w1 - w2.| = 0
proof
assume w1 = w2;
then |.w1 - w2.| = |.0.TOP-REAL N.| by RLVECT_1:5
.= 0 by Th23;
hence thesis;
end;
theorem
|.w1 - w2.| = 0 iff w1 = w2 by Lm1,Lm2;
theorem Th29:
|.w1 + w2.| <= |.w1.| + |.w2.|
proof
reconsider s1 = w1, s2 = w2 as Element of REAL N by EUCLID:22;
w1 + w2 = s1 + s2;
hence thesis by EUCLID:12;
end;
theorem
|.w1 - w2.| <= |.w1.| + |.w2.|
proof
reconsider s1 = w1, s2 = w2 as Element of REAL N by EUCLID:22;
w1 - w2 = s1 - s2;
hence thesis by EUCLID:13;
end;
theorem
|.w1.| - |.w2.| <= |.w1 + w2.|
proof
reconsider s1 = w1, s2 = w2 as Element of REAL N by EUCLID:22;
w1 + w2 = s1 + s2;
hence thesis by EUCLID:14;
end;
theorem Th32:
|.w1.| - |.w2.| <= |.w1 - w2.|
proof
reconsider s1 = w1, s2 = w2 as Element of REAL N by EUCLID:22;
w1 - w2 = s1 - s2;
hence thesis by EUCLID:15;
end;
theorem
w1 <> w2 implies |.w1 - w2.| > 0
proof
reconsider s1 = w1, s2 = w2 as Element of REAL N by EUCLID:22;
s1 - s2 = w1 - w2;
hence thesis by EUCLID:17;
end;
theorem
|.w1 - w2.| <= |.w1 - w.| + |.w - w2.|
proof
0.TOP-REAL N = w - w by RLVECT_1:5
.= -w + w;
then |.w1 - w2.| = |.w1 + ((-w) + w) - w2.| by RLVECT_1:4
.= |.w1 + (-w) + w - w2.| by RLVECT_1:def 3
.= |.(w1 - w) + w - w2.|
.= |.(w1 - w) + (w - w2).| by RLVECT_1:def 3;
hence thesis by Th29;
end;
definition
let N;
let IT be Real_Sequence of N;
attr IT is bounded means
ex r st for n holds |.IT.n.| < r;
end;
theorem Th35:
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: for n st X[n] holds X[n+1]
proof
let n;
given r1 such that
A2: 0<r1 and
A3: for m st m<=n holds |.seq.m.|<r1;
A4: now
assume
A5: r1<=|.seq.(n+1).|;
take r=|.seq.(n+1).|+1;
thus 0<r;
let m such that
A6: m<=n+1;
A7: now
assume m<=n;
then |.seq.m.|<r1 by A3;
then |.seq.m.|<|.seq.(n+1).| by A5,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 A6,A7,NAT_1:8;
end;
now
assume
A8: |.seq.(n+1).|<=r1;
take r=r1+1;
thus 0<r by A2;
let m such that
A9: m<=n+1;
A10: now
assume m<=n;
then
A11: |.seq.m.|<r1 by A3;
r1+0<r by XREAL_1:8;
hence |.seq.m.|<r by A11,XXREAL_0:2;
end;
now
A12: r1+0<r by XREAL_1:8;
assume m=n+1;
hence |.seq.m.|<r by A8,A12,XXREAL_0:2;
end;
hence |.seq.m.|<r by A9,A10,NAT_1:8;
end;
hence thesis by A4;
end;
A13: X[0]
proof
take r=|.seq.0 .|+1;
thus 0<r;
let m;
assume m<=0;
then 0=m;
then |.seq.m.|+0<r by XREAL_1:8;
hence thesis;
end;
thus for n holds X[n] from NAT_1:sch 2(A13,A1);
end;
definition
let N;
let IT be Real_Sequence of N;
attr IT is convergent means
ex g st for r st 0<r ex n st for m st n<= m holds |.IT.m-g.| < r;
end;
definition
let N,seq;
assume
A1: seq is convergent;
func lim seq -> Point of TOP-REAL N means
:Def9:
for r st 0<r ex n st for m st n<=m holds |.seq.m-it.| < r;
existence by A1;
uniqueness
proof
given g1,g2 such that
A2: for r st 0<r ex n st for m st n<=m holds |.seq.m-g1.|<r and
A3: for r st 0<r ex n st for m st n<=m holds |.seq.m-g2.|<r and
A4: g1<>g2;
A5: now
assume |.g1-g2.|=0;
then 0.TOP-REAL N+g2=g1-g2+g2 by Th24;
then g2=g1-g2+g2 by RLVECT_1:4
.=g1-(g2-g2) by RLVECT_1:29
.=g1-0.TOP-REAL N by RLVECT_1:5
.=g1+ -0.TOP-REAL N
.=g1+(-1)*0.TOP-REAL N by RLVECT_1:16
.=g1+0.TOP-REAL N by RLVECT_1:10
.=g1 by RLVECT_1:4;
hence contradiction by A4;
end;
then consider n1 such that
A6: for m st n1<=m holds |.seq.m-g1.|<|.g1-g2.|/4 by A2,XREAL_1:224;
consider n2 such that
A7: for m st n2<=m holds |.seq.m-g2.|<|.g1-g2.|/4 by A3,A5,XREAL_1:224;
A8: |.seq.(n1+n2)-g2.|<|.g1-g2.|/4 by A7,NAT_1:12;
|.seq.(n1+n2)-g1.|<|.g1-g2.|/4 by A6,NAT_1:12;
then
A9: |.seq.(n1+n2)-g2.|+|.seq.(n1+n2)-g1.|<|.g1-g2.|/4+|.g1-g2.|/4 by A8,
XREAL_1:8;
|.g1-g2.|=|.g1-g2+0.TOP-REAL N.| by RLVECT_1:4
.=|.g1-g2+(-1)*0.TOP-REAL N.| by RLVECT_1:10
.= |.g1-g2+-0.TOP-REAL N.| by RLVECT_1:16
.= |.g1-g2-0.TOP-REAL N.|
.=|.g1-g2-(seq.(n1+n2)-seq.(n1+n2)).| by RLVECT_1:5
.=|.g1-g2-seq.(n1+n2)+seq.(n1+n2).| by RLVECT_1:29
.=|.g1-(seq.(n1+n2)+g2)+seq.(n1+n2).| by RLVECT_1:27
.=|.g1-seq.(n1+n2)-g2+seq.(n1+n2).| by RLVECT_1:27
.=|.g1-seq.(n1+n2)-(g2-seq.(n1+n2)).| by RLVECT_1:29
.=|.g1-seq.(n1+n2)+-(g2-seq.(n1+n2)).|
.=|.g1-seq.(n1+n2)+(seq.(n1+n2)-g2).| by RLVECT_1:33
.=|.-(seq.(n1+n2)-g1)+(seq.(n1+n2)-g2).| by RLVECT_1:33;
then |.g1-g2.|<=|.-(seq.(n1+n2)-g1).|+|.seq.(n1+n2)-g2.| by Th29;
then
A10: |.g1-g2.|<=|.seq.(n1+n2)-g1.|+|.seq.(n1+n2)-g2.| by EUCLID:71;
|.g1-g2.|/2 <|.g1-g2.| by A5,XREAL_1:216;
hence contradiction by A9,A10,XXREAL_0:2;
end;
end;
theorem Th36:
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 r st 0<r ex n st for m st n<=m holds |.seq.m-g1.|<r by A1;
consider g2 such that
A4: for r st 0<r ex n st for m st n<=m holds |.seq9.m-g2.|<r by A2;
take g=g1+g2;
let r;
assume
A5: 0<r;
then consider n1 such that
A6: for m st n1<=m holds |.seq.m-g1.|<r/2 by A3,XREAL_1:215;
consider n2 such that
A7: for m st n2<=m holds |.seq9.m-g2.|<r/2 by A4,A5,XREAL_1:215;
take k=n1+n2;
let m;
assume
A8: k<=m;
n2<=k by NAT_1:12;
then n2<=m by A8,XXREAL_0:2;
then
A9: |.seq9.m-g2.|<r/2 by A7;
A10: |.(seq+seq9).m-g.|=|.seq.m+seq9.m-(g1+g2).| by Th4
.=|.seq.m+(seq9.m-(g1+g2)).| by RLVECT_1:def 3
.=|.seq.m+((-(g1+g2))+seq9.m).|
.=|.seq.m+-(g1+g2)+seq9.m.| by RLVECT_1:def 3
.=|.seq.m-(g1+g2)+seq9.m.|
.=|.seq.m-g1-g2+seq9.m.| by RLVECT_1:27
.=|.seq.m-g1+-g2+seq9.m.|
.=|.seq.m-g1+(seq9.m+-g2).| by RLVECT_1:def 3
.=|.seq.m-g1+(seq9.m-g2).|;
A11: |.seq.m-g1+(seq9.m-g2).|<=|.seq.m-g1.|+|.seq9.m-g2.| by Th29;
n1<=n1+n2 by NAT_1:12;
then n1<=m by A8,XXREAL_0:2;
then |.seq.m-g1.|<r/2 by A6;
then |.seq.m-g1.|+|.seq9.m-g2.|<r/2+r/2 by A9,XREAL_1:8;
hence thesis by A10,A11,XXREAL_0:2;
end;
theorem Th37:
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;
A3: now
let r;
assume 0<r;
then
A4: 0<r/2 by XREAL_1:215;
then consider n1 such that
A5: for m st n1<=m holds |.seq.m-lim (seq).|<r/2 by A1,Def9;
consider n2 such that
A6: for m st n2<=m holds |.seq9.m-lim (seq9).|<r/2 by A2,A4,Def9;
take k=n1+n2;
let m such that
A7: k<=m;
n2<=k by NAT_1:12;
then n2<=m by A7,XXREAL_0:2;
then
A8: |.seq9.m-(lim seq9).|<r/2 by A6;
A9: |.((seq+seq9).m)-((lim seq)+(lim seq9)).| =|.((seq+seq9).m)-(lim seq)
-(lim seq9).| by RLVECT_1:27
.=|.seq.m+seq9.m-(lim seq)-(lim seq9).| by Th4
.=|.seq.m+(seq9.m-(lim seq))-(lim seq9).| by RLVECT_1:def 3
.=|.seq.m+(-(lim seq)+seq9.m)-(lim seq9).|
.=|.seq.m+-(lim seq)+seq9.m-(lim seq9).| by RLVECT_1:def 3
.=|.seq.m-(lim seq)+seq9.m-(lim seq9).|
.=|.seq.m-(lim seq)+(seq9.m-(lim seq9)).| by RLVECT_1:def 3;
A10: |.seq.m-(lim seq)+(seq9.m-(lim seq9)).|<= |.seq.m-(lim seq).|+|.seq9.
m-(lim seq9).| by Th29;
n1<=n1+n2 by NAT_1:12;
then n1<=m by A7,XXREAL_0:2;
then |.seq.m-lim(seq).|<r/2 by A5;
then |.seq.m-(lim seq).|+|.seq9.m-(lim seq9).|<r/2+r/2 by A8,XREAL_1:8;
hence |.((seq+seq9).m)-((lim seq)+(lim seq9)).|<r by A9,A10,XXREAL_0:2;
end;
seq+seq9 is convergent by A1,A2,Th36;
hence thesis by A3,Def9;
end;
theorem Th38:
seq is convergent implies r*seq is convergent
proof
assume seq is convergent;
then consider g1 such that
A1: for q st 0<q ex n st for m st n<=m holds |.seq.m-g1.|<q;
set g=r*g1;
A2: now
A3: 0/|.r.|=0;
assume
A4: r<>0;
then
A5: 0<|.r.| by COMPLEX1:47;
let q;
assume 0<q;
then consider n1 such that
A6: for m st n1<=m holds |.seq.m-g1.|<q/|.r.| by A1,A5,A3,XREAL_1:74;
take k=n1;
let m;
assume k<=m;
then
A7: |.seq.m-g1.|<q/|.r.| by A6;
A8: 0<|.r.| by A4,COMPLEX1:47;
A9: |.r.|*(q/|.r.|)=|.r.|*(|.r.|"*q) by XCMPLX_0:def 9
.=|.r.|*|.r.|"*q
.=1*q by A8,XCMPLX_0:def 7
.=q;
|.((r*seq).m)-g.|=|.r*seq.m-r*g1.| by Th5
.=|.r*(seq.m-g1).| by RLVECT_1:34
.=|.r.|*|.seq.m-g1.| by Th7;
hence |.((r*seq).m)-g.|<q by A5,A7,A9,XREAL_1:68;
end;
now
assume
A10: r=0;
let q such that
A11: 0<q;
reconsider k=0 as Nat;
take k;
let m such that
k<=m;
|.((r*seq).m)-g.|=|.((0 *seq).m)-0.TOP-REAL N.| by A10,RLVECT_1:10
.=|.0.TOP-REAL N-((0 * seq).m).| by Th27
.=|.0.TOP-REAL N+-((0 * seq).m).|
.=|.-((0 * seq).m).| by RLVECT_1:4
.=|.(0 * seq).m.| by EUCLID:71
.=|.0 * seq.m.| by Th5
.=|.0.TOP-REAL N.| by RLVECT_1:10
.=0 by Th23;
hence |.((r*seq).m)-g.|<q by A11;
end;
hence thesis by A2;
end;
theorem Th39:
seq is convergent implies lim(r*seq)=r*(lim seq)
proof
A1: now
assume
A2: r=0;
let q such that
A3: 0<q;
reconsider k=0 as Nat;
take k;
let m such that
k<=m;
r*(lim seq)=0.TOP-REAL N by A2,RLVECT_1:10;
then |.((r*seq).m)-r*(lim seq).|=|.0 * seq.m-0.TOP-REAL N.| by A2,Th5
.=|.0.TOP-REAL N-0 * seq.m.| by Th27
.=|.0.TOP-REAL N+-0 * seq.m.|
.=|.-0 * seq.m.| by RLVECT_1:4
.=|.0 * seq.m.| by EUCLID:71
.=|.0.TOP-REAL N.| by RLVECT_1:10
.=0 by Th23;
hence |.((r*seq).m)-r*(lim seq).|<q by A3;
end;
assume
A4: seq is convergent;
A5: now
A6: 0/|.r.|=0;
assume
A7: r<>0;
then
A8: 0<|.r.| by COMPLEX1:47;
let q;
assume 0<q;
then 0<q/|.r.| by A8,A6,XREAL_1:74;
then consider n1 such that
A9: for m st n1<=m holds |.seq.m-(lim seq).|<q/|.r.| by A4,Def9;
take k=n1;
let m;
assume k<=m;
then
A10: |.seq.m-(lim seq).|<q/|.r.| by A9;
A11: 0<>|.r.| by A7,COMPLEX1:47;
A12: |.r.|*(q/|.r.|)=|.r.|*(|.r.|"*q) by XCMPLX_0:def 9
.=|.r.|*|.r.|"*q
.=1*q by A11,XCMPLX_0:def 7
.=q;
|.((r*seq).m)-r*(lim seq).|=|.r*seq.m-r*(lim seq).| by Th5
.=|.r*(seq.m-(lim seq)).| by RLVECT_1:34
.=|.r.|*|.seq.m-(lim seq).| by Th7;
hence |.((r*seq).m)-r*(lim seq).|<q by A8,A10,A12,XREAL_1:68;
end;
r*seq is convergent by A4,Th38;
hence thesis by A1,A5,Def9;
end;
theorem Th40:
seq is convergent implies - seq is convergent
proof
assume seq is convergent;
then (-1)*seq is convergent by Th38;
hence thesis by Th11;
end;
theorem Th41:
seq is convergent implies lim(-seq)=-(lim seq)
proof
assume seq is convergent;
then lim ((-1)*seq)=(-1)*(lim seq) by Th39
.=-(1*(lim seq)) by RLVECT_1:79
.=-(lim seq) by RLVECT_1:def 8;
hence thesis by Th11;
end;
theorem
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,Th40;
hence thesis by A1,Th36;
end;
theorem
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;
- seq9 is convergent by A2,Th40;
hence lim(seq - seq9)=(lim seq)+(lim(- seq9)) by A1,Th37
.=(lim seq)+-(lim seq9) by A2,Th41
.=(lim seq)-(lim seq9);
end;
theorem
seq is convergent implies seq is bounded
proof
assume seq is convergent;
then consider g such that
A1: for r st 0<r ex n st for m st n<=m holds |.seq.m-g.|<r;
consider n1 such that
A2: for m st n1<=m holds |.seq.m-g.|<1 by A1;
A3: now
take r=|.g.|+1;
thus 0<r;
let m;
A4: |.seq.m.|-|.g.|+|.g.|=|.seq.m.|;
assume n1<=m;
then
A5: |.seq.m-g.|<1 by A2;
|.seq.m.|-|.g.|<=|.seq.m-g.| by Th32;
then |.seq.m.|-|.g.|<1 by A5,XXREAL_0:2;
hence |.seq.m.|<r by A4,XREAL_1:6;
end;
now
consider r2 such that
A6: 0<r2 and
A7: for m st m<=n1 holds |.seq.m.|<r2 by Th35;
consider r1 such that
A8: 0<r1 and
A9: for m st n1<=m holds |.seq.m.|<r1 by A3;
take r=r1+r2;
thus 0<r by A8,A6;
let m;
A10: 0+r2<r by A8,XREAL_1:8;
A11: now
assume m<=n1;
then |.seq.m.|<r2 by A7;
hence |.seq.m.|<r by A10,XXREAL_0:2;
end;
A12: r1+0<r by A6,XREAL_1:8;
now
assume n1<=m;
then |.seq.m.|<r1 by A9;
hence |.seq.m.|<r by A12,XXREAL_0:2;
end;
hence |.seq.m.|<r by A11;
end;
hence thesis;
end;
theorem
seq is convergent implies ((lim seq) <> 0.TOP-REAL N 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.TOP-REAL N;
0 <> |.(lim seq).| by A2,Th24;
then 0<|.(lim seq).|/2 by XREAL_1:215;
then consider n1 such that
A3: for m st n1<=m holds |.seq.m-(lim seq).|<|.(lim seq).|/2 by A1,Def9;
take n=n1;
let m;
assume n<=m;
then
A4: |.seq.m-(lim seq).|<|.(lim seq).|/2 by A3;
|.(lim seq).|-|.seq.m.|<=|.(lim seq)-seq.m.| & |.(lim seq)-seq.m.|=|.seq
.m-( lim seq).| by Th27,Th32;
then
A5: |.(lim seq).|-|.seq.m.|<|.(lim seq).|/2 by A4,XXREAL_0:2;
|.(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 A5,XREAL_1:6;
end;