Copyright (c) 1994 Association of Mizar Users
environ
vocabulary FUNCT_1, PRE_TOPC, EUCLID, SEQ_1, RELAT_1, ANPROJ_1, BOOLE,
ARYTM_1, COMPLEX1, FINSEQ_1, ABSVALUE, LATTICES, SEQ_2, ORDINAL2,
ARYTM_3, NORMSP_1;
notation TARSKI, XBOOLE_0, NUMBERS, XREAL_0, RELAT_1, FUNCT_1, REAL_1, NAT_1,
SEQ_1, ABSVALUE, STRUCT_0, NORMSP_1, FINSEQ_1, FINSEQ_2, EUCLID,
PRE_TOPC;
constructors SEQ_1, ABSVALUE, EUCLID, REAL_1, NAT_1, PARTFUN1, NORMSP_1,
MEMBERED, XBOOLE_0;
clusters STRUCT_0, EUCLID, XREAL_0, RELSET_1, SEQ_1, ARYTM_3, MEMBERED,
ZFMISC_1, XBOOLE_0, NUMBERS, ORDINAL2;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
theorems REAL_1, FUNCT_1, FUNCT_2, TARSKI, EUCLID, SEQ_1, NAT_1, AXIOMS,
ABSVALUE, SEQ_2, XBOOLE_0, NORMSP_1, XCMPLX_0, XCMPLX_1;
schemes SEQ_1, NAT_1, ZFREFLE1;
begin
definition let N be Nat;
mode Real_Sequence of N is sequence of TOP-REAL N;
end;
reserve N,n,m,k,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,seq' for Real_Sequence of N;
canceled;
theorem Th2:
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 holds f.n is Point of TOP-REAL N)
by NORMSP_1:17;
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:17;
end;
definition
let N;
let IT be Real_Sequence of N;
attr IT is non-zero means :Def1:
rng IT c= (the carrier of TOP-REAL N) \ {0.REAL N};
end;
theorem
Th3:seq is non-zero iff for x st x in NAT holds seq.x<>0.REAL N
proof
thus seq is non-zero implies for x st x in NAT holds seq.x<>0.REAL N
proof
assume seq is non-zero;
then A1: rng seq c= (the carrier of TOP-REAL N) \ {0.REAL N} by Def1;
let x;
assume x in NAT;
then x in dom seq by Th2;
then seq.x in rng seq by FUNCT_1:def 5;
then not seq.x in {0.REAL N} by A1,XBOOLE_0:def 4;
hence seq.x<>0.REAL N by TARSKI:def 1;
end;
assume A2: for x st x in NAT holds seq.x<>0.REAL N;
now let y;
assume y in rng seq;
then consider x such that
A3: x in dom seq and
A4: seq.x=y by FUNCT_1:def 5;
A5: x in NAT by A3,NORMSP_1:17;
then A6: y is Point of TOP-REAL N by A4,NORMSP_1:17;
y<>0.REAL N by A2,A4,A5;
then not y in {0.REAL N} by TARSKI:def 1;
hence y in (the carrier of TOP-REAL N) \ {0.REAL N} by A6,XBOOLE_0:def 4
;
end;
then rng seq c= (the carrier of TOP-REAL N) \ {0.REAL N} by TARSKI:def 3;
hence thesis by Def1;
end;
theorem
Th4:seq is non-zero iff for n holds seq.n<>0.REAL N
proof
thus seq is non-zero implies for n holds seq.n<>0.REAL N by Th3;
assume for n holds seq.n<>0.REAL N;
then for x holds x in NAT implies seq.x<>0.REAL N;
hence thesis by Th3;
end;
theorem
Th5:for N,seq,seq1 st (for x st x in NAT holds seq.x=seq1.x) holds seq=seq1
proof
let N,seq,seq1 such that
A1: for x st x in NAT holds seq.x=seq1.x;
dom seq= NAT & dom seq1=NAT by NORMSP_1:17;
hence thesis by A1,FUNCT_1:9;
end;
theorem
Th6:for N,seq,seq1 st (for n holds seq.n=seq1.n) holds seq=seq1
proof
let N,seq,seq1;
assume for n holds seq.n=seq1.n;
then for x holds x in NAT implies seq.x=seq1.x;
hence thesis by Th5;
end;
scheme ExTopRealNSeq{N()->Nat, F(Nat)->Point of TOP-REAL N()}:
ex seq being Real_Sequence of N() st for n holds seq.n=F(n)
proof
defpred P[set,set] means ex n st n=$1 & $2=F(n);
A1: now let x;
assume x in NAT;
then consider n such that
A2: n=x;
reconsider r2=F(n) as set;
take y=r2;
thus P[x,y] by A2;
end;
consider f being Function such that
A3: dom f=NAT and
A4: for x st x in NAT holds P[x,f.x] from NonUniqFuncEx(A1);
now let x;
assume x in NAT;
then ex n st
n=x & f.x=F(n) by A4;
hence f.x is Point of TOP-REAL N();
end;
then reconsider f as Real_Sequence of N() by A3,NORMSP_1:17;
take seq=f;
let n;
ex k st k=n & seq.n=F(k) by A4;
hence seq.n=F(n);
end;
definition
let N,seq1,seq2;
func seq1 + seq2 -> Real_Sequence of N means :Def2:
for n holds it.n = seq1.n + seq2.n;
existence
proof
deffunc U(Nat) = seq1.$1 + seq2.$1;
thus ex s being Real_Sequence of N st
for n holds s.n = U(n) from ExTopRealNSeq;
end;
uniqueness
proof
let seq,seq' such that
A1: for n holds seq.n=seq1.n+seq2.n and
A2: for n holds seq'.n=seq1.n+seq2.n;
now let n;
seq.n=seq1.n+seq2.n & seq'.n=seq1.n+seq2.n by A1,A2;
hence seq.n=seq'.n;
end;
hence seq=seq' by Th6;
end;
end;
definition
let r,N,seq;
func r*seq -> Real_Sequence of N means : Def3:
for n holds it.n = r*seq.n;
existence
proof
deffunc U(Nat) = r * seq.$1;
thus ex s being Real_Sequence of N st
for n holds s.n = U(n) from ExTopRealNSeq;
end;
uniqueness
proof
let seq1,seq2 such that
A1: for n holds seq1.n=r*seq.n and
A2: for n holds seq2.n=r*seq.n;
now let n;
seq1.n=r*seq.n & seq2.n=r*seq.n by A1,A2;
hence seq1.n=seq2.n;
end;
hence seq1=seq2 by Th6;
end;
end;
definition
let N,seq;
func - seq -> Real_Sequence of N means :Def4:
for n holds it.n = -seq.n;
existence
proof
take seq1=(-1)*seq;
let n;
thus seq1.n=(-1)*seq.n by Def3
.=-(seq.n) by EUCLID:43;
end;
uniqueness
proof
let seq1,seq2 such that
A1: for n holds seq1.n=-seq.n and
A2: for n holds seq2.n=-seq.n;
now let n;
seq1.n=-seq.n & seq2.n=-seq.n by A1,A2;
hence seq1.n=seq2.n;
end;
hence seq1=seq2 by Th6;
end;
end;
definition
let N,seq1,seq2;
func seq1-seq2 -> Real_Sequence of N equals :Def5:
seq1 +- seq2;
correctness;
end;
definition
let N; let x be Point of TOP-REAL N;
func |.x.|-> Real means :Def6:
ex y be FinSequence of REAL st x=y & it=|.y.|;
existence
proof
reconsider y = x as FinSequence of REAL by EUCLID:27;
take |.y.|;
thus thesis;
end;
uniqueness;
end;
definition
let N,seq;
func |.seq.| -> Real_Sequence means :Def7:
for n holds it.n=|.seq.n.|;
existence
proof deffunc U(Nat) = |.seq.$1.|;
thus ex s being Real_Sequence st
for n holds s.n= U(n) from ExRealSeq;
end;
uniqueness
proof
let seq8,seq9 be Real_Sequence such that
A1: for n holds seq8.n=|.seq.n.| and
A2: for n holds seq9.n=|.seq.n.|;
now let n;
seq9.n=|.seq.n.| by A2;
hence seq8.n=seq9.n by A1;
end;
hence seq8=seq9 by FUNCT_2:113;
end;
end;
canceled;
theorem Th8:
abs(r)*|.w.| = |.r*w.|
proof
reconsider s = w as Element of REAL N by EUCLID:25;
r*w = r*s by EUCLID:def 11;
then |.s.|=|.w.| & |.r*w.| = |.r*s.| by Def6;
hence thesis by EUCLID:14;
end;
theorem
|.r*seq.| = abs(r)(#)|.seq.|
proof
now let n;
thus |.r*seq.|.n=|.(r*seq).n.| by Def7
.=|.r*(seq.n).| by Def3
.=abs(r)*|.seq.n.| by Th8
.=abs(r)*(|.seq.|).n by Def7
.=(abs(r)(#)|.seq.|).n by SEQ_1:13;
end;
hence thesis by FUNCT_2:113;
end;
theorem
seq1 + seq2 = seq2 + seq1
proof
now let n;
thus (seq1+seq2).n = seq2.n + seq1.n by Def2
.= (seq2 + seq1).n by Def2;
end;
hence thesis by Th6;
end;
theorem
Th11:(seq1 + seq2) + seq3 = seq1 + (seq2 + seq3)
proof
now let n;
thus ((seq1+seq2)+seq3).n = (seq1+seq2).n+ seq3.n by Def2
.= seq1.n+seq2.n+seq3.n by Def2
.=seq1.n+(seq2.n+seq3.n) by EUCLID:30
.=seq1.n+(seq2+seq3).n by Def2
.=(seq1+(seq2+seq3)).n by Def2;
end;
hence thesis by Th6;
end;
theorem
Th12:-seq = (-1)*seq
proof
now let n;
thus ((-1)*seq).n=(-1)*seq.n by Def3
.=-seq.n by EUCLID:43
.=(-seq).n by Def4;
end;
hence thesis by Th6;
end;
theorem
Th13: r*(seq1 + seq2) = r*seq1 + r*seq2
proof
now let n;
thus (r*(seq1 + seq2)).n=r*(seq1+seq2).n by Def3
.=r*(seq1.n+seq2.n) by Def2
.=r*seq1.n+r*seq2.n by EUCLID:36
.=(r*seq1).n+r*seq2.n by Def3
.=(r*seq1).n+(r*seq2).n by Def3
.=((r*seq1)+(r*seq2)).n by Def2;
end;
hence thesis by Th6;
end;
theorem
Th14:(r*q)*seq = r*(q*seq)
proof
now let n;
thus ((r*q)*seq).n=(r*q)*seq.n by Def3
.=r*(q*seq.n) by EUCLID:34
.=r*(q*seq).n by Def3
.=(r*(q*seq)).n by Def3;
end;
hence thesis by Th6;
end;
theorem
Th15:r*(seq1 - seq2) = r*seq1 - r*seq2
proof
thus r*(seq1-seq2)=r*(seq1+-seq2) by Def5
.=r*seq1+r*(-seq2) by Th13
.=r*seq1+r*((-1)*seq2) by Th12
.=r*seq1+((-1)*r)*seq2 by Th14
.=r*seq1+(-1)*(r*seq2) by Th14
.=r*seq1+-(r*seq2) by Th12
.=r*seq1-(r*seq2) by Def5;
end;
theorem
seq1 - (seq2 + seq3) = seq1 - seq2 - seq3
proof
thus seq1-(seq2+seq3)=seq1+-(seq2+seq3) by Def5
.=seq1+(-1)*(seq2+seq3) by Th12
.=seq1+((-1)*seq2+(-1)*seq3) by Th13
.=seq1+(-seq2+(-1)*seq3) by Th12
.=seq1+(-seq2+-seq3) by Th12
.=seq1+-seq2+-seq3 by Th11
.=seq1-seq2+-seq3 by Def5
.=seq1-seq2-seq3 by Def5;
end;
theorem
Th17:1*seq=seq
proof
now let n;
thus (1*seq).n=1*seq.n by Def3
.=seq.n by EUCLID:33;
end;
hence thesis by Th6;
end;
theorem
Th18:-(-seq) = seq
proof
thus -(-seq)=(-1)*(-seq) by Th12
.=(-1)*((-1)*seq) by Th12
.=((-1)*(-1))*seq by Th14
.=seq by Th17;
end;
theorem
Th19:seq1 - (-seq2) = seq1 + seq2
proof
thus seq1-(-seq2)=seq1+(-(-seq2)) by Def5
.=seq1+seq2 by Th18;
end;
theorem
seq1 - (seq2 - seq3) = seq1 - seq2 + seq3
proof
thus seq1-(seq2-seq3)=seq1+-(seq2-seq3) by Def5
.=seq1+(-1)*(seq2-seq3) by Th12
.=seq1+((-1)*seq2-((-1)*seq3)) by Th15
.=seq1+(-seq2-((-1)*seq3)) by Th12
.=seq1+(-seq2-(-seq3)) by Th12
.=seq1+(-seq2+seq3) by Th19
.=seq1+-seq2+seq3 by Th11
.=seq1-seq2+seq3 by Def5;
end;
theorem
seq1 + (seq2 - seq3) = seq1 + seq2 - seq3
proof
thus seq1+(seq2-seq3)=seq1+(seq2+-seq3) by Def5
.=seq1+seq2+-seq3 by Th11
.=seq1+seq2-seq3 by Def5;
end;
theorem
Th22: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.REAL N by A3,Th4;
A5: r*seq.n1=0.REAL N by A4,Def3;
seq.n1 <> 0.REAL N by A2,Th4;
hence contradiction by A1,A5,EUCLID:35;
end;
theorem
seq is non-zero implies -seq is non-zero
proof
assume
seq is non-zero;
then (-1)*seq is non-zero by Th22;
hence thesis by Th12;
end;
theorem
Th24:|.0.REAL N.| = 0
proof
0.REAL N = 0*N by EUCLID:def 9;
hence |.0.REAL N.| = |.0*N.| by Def6
.=0 by EUCLID:10;
end;
theorem
Th25:|.w.| = 0 implies w = 0.REAL N
proof
reconsider s = w as Element of REAL N by EUCLID:25;
assume |.w.| = 0;
then |.s.| = 0 by Def6;
then s = 0*N by EUCLID:11
.= 0.REAL N by EUCLID:def 9;
hence thesis;
end;
theorem
Th26:|.w.| >= 0
proof
reconsider s = w as Element of REAL N by EUCLID:25;
|.s.| >= 0 by EUCLID:12;
hence thesis by Def6;
end;
theorem
Th27:|.-w.| = |.w.|
proof
reconsider s = w as Element of REAL N by EUCLID:25;
-s = -w by EUCLID:def 12;
then |.-w.| = |.-s.| by Def6
.=|.s.| by EUCLID:13
.=|.w.| by Def6;
hence thesis;
end;
theorem
Th28:|.w1 - w2.| = |.w2 - w1.|
proof
thus |.w1 - w2.| = |.-(w1 - w2).| by Th27
.= |.w2 - w1.| by EUCLID:48;
end;
Lm1: |.w1 - w2.| = 0 implies w1 = w2
proof
assume |.w1 - w2.| = 0;
then w1 - w2 = 0.REAL N by Th25;
hence w1 = w2 by EUCLID:47;
end;
Lm2: w1 = w2 implies |.w1 - w2.| = 0
proof
assume w1 = w2;
then |.w1 - w2.| = |.0.REAL N.| by EUCLID:46
.= 0 by Th24;
hence thesis;
end;
theorem
|.w1 - w2.| = 0 iff w1 = w2 by Lm1,Lm2;
theorem
Th30:|.w1 + w2.| <= |.w1.| + |.w2.|
proof
reconsider s1 = w1, s2 = w2 as Element of REAL N by EUCLID:25;
w1 + w2 = s1 + s2 by EUCLID:def 10;
then A1: |.w1 + w2.| = |.s1 + s2.| by Def6;
A2: |.s1 + s2.| <= |.s1.| + |.s2.| by EUCLID:15;
|.s1.| = |.w1.| by Def6;
hence |.w1 + w2.| <= |.w1.| + |.w2.| by A1,A2,Def6;
end;
theorem
|.w1 - w2.| <= |.w1.| + |.w2.|
proof
reconsider s1 = w1, s2 = w2 as Element of REAL N by EUCLID:25;
s1 - s2 = w1 - w2 by EUCLID:def 13;
then A1: |.w1 - w2.| = |.s1 - s2.| by Def6;
A2: |.s1 - s2.| <= |.s1.| + |.s2.| by EUCLID:16;
|.s1.| = |.w1.| by Def6;
hence |.w1 - w2.| <= |.w1.| + |.w2.| by A1,A2,Def6;
end;
theorem
|.w1.| - |.w2.| <= |.w1 + w2.|
proof
reconsider s1 = w1, s2 = w2 as Element of REAL N by EUCLID:25;
s1 + s2 = w1 + w2 by EUCLID:def 10;
then A1: |.w1 + w2.| = |.s1 + s2.| by Def6;
A2: |.s1.| - |.s2.| <= |.s1 + s2.| by EUCLID:17;
|.s1.| = |.w1.| by Def6;
hence |.w1.| - |.w2.| <= |.w1 + w2.| by A1,A2,Def6;
end;
theorem
Th33:|.w1.| - |.w2.| <= |.w1 - w2.|
proof
reconsider s1 = w1, s2 = w2 as Element of REAL N by EUCLID:25;
s1 - s2 = w1 - w2 by EUCLID:def 13;
then A1: |.w1 - w2.| = |.s1 - s2.| by Def6;
A2: |.s1.| - |.s2.| <= |.s1 - s2.| by EUCLID:18;
|.s1.| = |.w1.| by Def6;
hence |.w1.| - |.w2.| <= |.w1 - w2.| by A1,A2,Def6;
end;
theorem
w1 <> w2 implies |.w1 - w2.| > 0
proof
reconsider s1 = w1, s2 = w2 as Element of REAL N by EUCLID:25;
A1: s1 - s2 = w1 - w2 by EUCLID:def 13;
assume w1 <> w2;
then |.s1 - s2.| > 0 by EUCLID:20;
hence thesis by A1,Def6;
end;
theorem
|.w1 - w2.| <= |.w1 - w.| + |.w - w2.|
proof
0.REAL N = w - w by EUCLID:46
.= -w + w by EUCLID:45;
then |.w1 - w2.| = |.w1 + ((-w) + w) - w2.| by EUCLID:31
.= |.w1 + (-w) + w - w2.| by EUCLID:30
.= |.(w1 - w) + w - w2.| by EUCLID:45
.= |.(w1 - w) + (w - w2).| by EUCLID:49;
hence thesis by Th30;
end;
theorem
0<=r1 & |.w1.|<|.w2.| & r1<r2 implies |.w1.|*r1<|.w2.|*r2
proof
assume that
A1: 0 <=r1 and
A2: |.w1.|<|.w2.| and
A3: r1<r2;
A4: |.w1.|*r2<|.w2.|*r2 by A1,A2,A3,REAL_1:70;
0 <= |.w1.| by Th26;
then |.w1.|*r1<=|.w1.|*r2 by A3,AXIOMS:25;
hence thesis by A4,AXIOMS:22;
end;
canceled;
theorem
-|.w.|<r & r<|.w.| iff abs(r)<|.w.|
proof
thus -|.w.|<r & r<|.w.| implies abs(r)<|.w.|
proof
assume that
A1: -|.w.|<r and
A2: r<|.w.|;
A3: abs(r)<=|.w.| by A1,A2,ABSVALUE:12;
now assume A4: abs(r)=|.w.|;
now assume r<0;
then -|.w.|=--r by A4,ABSVALUE:def 1;
hence contradiction by A1;
end;
hence contradiction by A2,A4,ABSVALUE:def 1;
end;
hence thesis by A3,REAL_1:def 5;
end;
assume
A5: abs(r)<|.w.|;
then A6: -|.w.|<=r by ABSVALUE:12;
A7: r<=|.w.| by A5,ABSVALUE:12;
A8: 0<=abs(r) by ABSVALUE:5;
A9: 0<|.w.| by A5,ABSVALUE:5;
A10: -|.w.|<0 by A5,A8,REAL_1:26,50;
now assume r=-|.w.|;
then abs(r)=--|.w.| by A10,ABSVALUE:def 1
.=|.w.|;
hence contradiction by A5;
end;
hence -|.w.|<r by A6,REAL_1:def 5;
r <> |.w.| by A5,A9,ABSVALUE:def 1;
hence r<|.w.| by A7,REAL_1:def 5;
end;
definition
let N;
let IT be Real_Sequence of N;
attr IT is bounded means :Def8:
ex r st for n holds |.IT.n.| < r;
end;
theorem
Th39: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 take r=|.seq.0.|+1;
0<=|.seq.0.| by Th26;
then 0+0<|.seq.0.|+1 by REAL_1:67;
hence 0<r;
let m such that
A2: m<=0;
0=m by A2,NAT_1:18;
then |.seq.m.|+0<r by REAL_1:67;
hence |.seq.m.|<r;
end;
A3: for n st X[n] holds X[n+1]
proof let n;
given r1 such that
A4: 0<r1 and
A5: for m st m<=n holds |.seq.m.|<r1;
A6: now assume
A7: |.seq.(n+1).|<=r1;
take r=r1+1;
0+0<r1+1 by A4,REAL_1:67;
hence 0<r;
let m such that A8: m<=n+1;
A9: now assume m<=n;
then A10: |.seq.m.|<r1 by A5;
r1+0<r by REAL_1:67;
hence |.seq.m.|<r by A10,AXIOMS:22;
end;
now assume A11: m=n+1;
r1+0<r by REAL_1:67;
hence |.seq.m.|<r by A7,A11,AXIOMS:22;
end;
hence |.seq.m.|<r by A8,A9,NAT_1:26;
end;
now assume
A12: r1<=|.seq.(n+1).|;
take r=|.seq.(n+1).|+1;
0<=|.seq.(n+1).| by Th26;
then 0+0<r by REAL_1:67;
hence 0<r;
let m such that
A13: m<=n+1;
A14: now assume m<=n;
then |.seq.m.|<r1 by A5;
then |.seq.m.|<|.seq.(n+1).| by A12,AXIOMS:22;
then |.seq.m.|+0<r by REAL_1:67;
hence |.seq.m.|<r;
end;
now assume m=n+1;
then |.seq.m.|+0<r by REAL_1:67;
hence |.seq.m.|<r;
end;
hence |.seq.m.|<r by A13,A14,NAT_1:26;
end;
hence ex r st (0<r & for m st m<=n+1 holds |.seq.m.|<r)
by A6;
end;
thus for n holds X[n] from Ind(A1,A3);
end;
definition
let N;
let IT be Real_Sequence of N;
attr IT is convergent means :Def9:
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 :Def10:
for r st 0<r ex n st for m st n<=m holds |.seq.m-it.| < r;
existence by A1,Def9;
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.REAL N+g2=g1-g2+g2 by Th25;
then g2=g1-g2+g2 by EUCLID:31
.=g1-(g2-g2) by EUCLID:51
.=g1-0.REAL N by EUCLID:46
.=g1+ -0.REAL N by EUCLID:45
.=g1+(-1)*0.REAL N by EUCLID:43
.=g1+0.REAL N by EUCLID:32
.=g1 by EUCLID:31;
hence contradiction by A4;
end;
A6: 0<=|.g1-g2.| by Th26;
then A7: 0<|.g1-g2.|/4 by A5,SEQ_2:3;
then consider n1 such that
A8: for m st n1<=m holds |.seq.m-g1.|<|.g1-g2.|/4 by A2;
consider n2 such that
A9: for m st n2<=m holds |.seq.m-g2.|<|.g1-g2.|/4 by A3,A7;
n1<=n1+n2 by NAT_1:37;
then A10: |.seq.(n1+n2)-g1.|<|.g1-g2.|/4 by A8;
n2<=n1+n2 by NAT_1:37;
then |.seq.(n1+n2)-g2.|<|.g1-g2.|/4 by A9;
then |.seq.(n1+n2)-g2.|+|.seq.(n1+n2)-g1.|<|.g1-g2.|/4+|.g1-g2.|/4
by A10,REAL_1:67;
then A11: |.seq.(n1+n2)-g1.|+|.seq.(n1+n2)-g2.|<|.g1-g2.|/2 by XCMPLX_1:72;
|.g1-g2.|=|.g1-g2+0.REAL N.| by EUCLID:31
.=|.g1-g2+(-1)*0.REAL N.| by EUCLID:32
.= |.g1-g2+-0.REAL N.| by EUCLID:43
.= |.g1-g2-0.REAL N.| by EUCLID:45
.=|.g1-g2-(seq.(n1+n2)-seq.(n1+n2)).| by EUCLID:46
.=|.g1-g2-seq.(n1+n2)+seq.(n1+n2).| by EUCLID:51
.=|.g1-(seq.(n1+n2)+g2)+seq.(n1+n2).| by EUCLID:50
.=|.g1-seq.(n1+n2)-g2+seq.(n1+n2).| by EUCLID:50
.=|.g1-seq.(n1+n2)-(g2-seq.(n1+n2)).| by EUCLID:51
.=|.g1-seq.(n1+n2)+-(g2-seq.(n1+n2)).| by EUCLID:45
.=|.g1-seq.(n1+n2)+(seq.(n1+n2)-g2).| by EUCLID:48
.=|.-(seq.(n1+n2)-g1)+(seq.(n1+n2)-g2).| by EUCLID:48;
then |.g1-g2.|<=|.-(seq.(n1+n2)-g1).|+|.seq.(n1+n2)-g2.| by Th30;
then A12: |.g1-g2.|<=|.seq.(n1+n2)-g1.|+|.seq.(n1+n2)-g2.| by Th27;
|.g1-g2.|/2 <|.g1-g2.| by A5,A6,SEQ_2:4;
hence contradiction by A11,A12,AXIOMS:22;
end;
end;
canceled;
theorem
Th41:seq is convergent & seq' is convergent implies
seq + seq' is convergent
proof
assume that
A1: seq is convergent and
A2: seq' 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,Def9;
consider g2 such that
A4: for r st 0<r ex n st for m st n<=m holds |.seq'.m-g2.|<r
by A2,Def9;
take g=g1+g2;
let r;assume 0<r;
then A5: 0<r/2 by SEQ_2:3;
then consider n1 such that
A6: for m st n1<=m holds |.seq.m-g1.|<r/2 by A3;
consider n2 such that
A7: for m st n2<=m holds |.seq'.m-g2.|<r/2 by A4,A5;
take k=n1+n2;
let m; assume A8: k<=m;
n1<=n1+n2 by NAT_1:37;
then n1<=m by A8,AXIOMS:22;
then A9: |.seq.m-g1.|<r/2 by A6;
n2<=k by NAT_1:37;
then n2<=m by A8,AXIOMS:22;
then |.seq'.m-g2.|<r/2 by A7;
then |.seq.m-g1.|+|.seq'.m-g2.|<r/2+r/2 by A9,REAL_1:67;
then A10: |.seq.m-g1.|+|.seq'.m-g2.|<r by XCMPLX_1:66;
A11:|.(seq+seq').m-g.|=|.seq.m+seq'.m-(g1+g2).| by Def2
.=|.seq.m+(seq'.m-(g1+g2)).| by EUCLID:49
.=|.seq.m+((-(g1+g2))+seq'.m).| by EUCLID:45
.=|.seq.m+-(g1+g2)+seq'.m.| by EUCLID:30
.=|.seq.m-(g1+g2)+seq'.m.| by EUCLID:45
.=|.seq.m-g1-g2+seq'.m.| by EUCLID:50
.=|.seq.m-g1+-g2+seq'.m.| by EUCLID:45
.=|.seq.m-g1+(seq'.m+-g2).| by EUCLID:30
.=|.seq.m-g1+(seq'.m-g2).| by EUCLID:45;
|.seq.m-g1+(seq'.m-g2).|<=|.seq.m-g1.|+|.seq'.m-g2.| by Th30;
hence |.(seq+seq').m -g.|<r by A10,A11,AXIOMS:22;
end;
theorem
Th42:seq is convergent & seq' is convergent implies
lim (seq + seq')=(lim seq)+(lim seq')
proof
assume that
A1: seq is convergent and
A2: seq' is convergent;
A3: seq+seq' is convergent by A1,A2,Th41;
now let r; assume 0<r;
then A4: 0<r/2 by SEQ_2:3;
then consider n1 such that
A5: for m st n1<=m holds |.seq.m-lim (seq).|<r/2 by A1,Def10;
consider n2 such that
A6: for m st n2<=m holds |.seq'.m-lim (seq').|<r/2 by A2,A4,Def10;
take k=n1+n2;
let m such that A7: k<=m;
n1<=n1+n2 by NAT_1:37;
then n1<=m by A7,AXIOMS:22;
then A8: |.seq.m-lim(seq).|<r/2 by A5;
n2<=k by NAT_1:37;
then n2<=m by A7,AXIOMS:22;
then |.seq'.m-(lim seq').|<r/2 by A6;
then |.seq.m-(lim seq).|+|.seq'.m-(lim seq').|<r/2+r/2
by A8,REAL_1:67;
then A9: |.seq.m-(lim seq).|+|.seq'.m-(lim seq').|<r by XCMPLX_1:66;
A10: |.((seq+seq').m)-((lim seq)+(lim seq')).|
=|.((seq+seq').m)-(lim seq)-(lim seq').| by EUCLID:50
.=|.seq.m+seq'.m-(lim seq)-(lim seq').| by Def2
.=|.seq.m+(seq'.m-(lim seq))-(lim seq').| by EUCLID:49
.=|.seq.m+(-(lim seq)+seq'.m)-(lim seq').| by EUCLID:45
.=|.seq.m+-(lim seq)+seq'.m-(lim seq').| by EUCLID:30
.=|.seq.m-(lim seq)+seq'.m-(lim seq').| by EUCLID:45
.=|.seq.m-(lim seq)+(seq'.m-(lim seq')).| by EUCLID:49;
|.seq.m-(lim seq)+(seq'.m-(lim seq')).|<=
|.seq.m-(lim seq).|+|.seq'.m-(lim seq').| by Th30;
hence |.((seq+seq').m)-((lim seq)+(lim seq')).|<r by A9,A10,AXIOMS:22;
end;
hence thesis by A3,Def10;
end;
theorem
Th43: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
by Def9;
set g=r*g1;
A2: now assume
A3: r=0;
let q such that
A4: 0<q;
take k=0;
let m such that k<=m;
|.((r*seq).m)-g.|=|.((0 *seq).m)-0.REAL N.| by A3,EUCLID:33
.=|.0.REAL N-((0 * seq).m).| by Th28
.=|.0.REAL N+-((0 * seq).m).| by EUCLID:45
.=|.-((0 * seq).m).| by EUCLID:31
.=|.(0 * seq).m.| by Th27
.=|.0 * seq.m.| by Def3
.=|.0.REAL N.| by EUCLID:33
.=0 by Th24;
hence |.((r*seq).m)-g.|<q by A4;
end;
now assume
A5: r<>0;
then A6: 0<abs(r) by ABSVALUE:6;
let q such that A7:0<q;
A8: 0<abs(r) by A5,ABSVALUE:6;
0/abs(r)=0;
then 0<q/abs(r) by A6,A7,REAL_1:73;
then consider n1 such that
A9: for m st n1<=m holds |.seq.m-g1.|<q/abs(r) by A1;
take k=n1;
let m;
assume k<=m;
then A10: |.seq.m-g1.|<q/abs(r) by A9;
A11: |.((r*seq).m)-g.|=|.r*seq.m-r*g1.| by Def3
.=|.r*(seq.m-g1).| by EUCLID:53
.=abs(r)*|.seq.m-g1.| by Th8;
abs(r)*(q/abs(r))=abs(r)*(abs(r)"*q) by XCMPLX_0:def 9
.=abs(r)*abs(r)"*q by XCMPLX_1:4
.=1*q by A8,XCMPLX_0:def 7
.=q;
hence |.((r*seq).m)-g.|<q by A6,A10,A11,REAL_1:70;
end;
hence thesis by A2,Def9;
end;
theorem
Th44:seq is convergent implies lim(r*seq)=r*(lim seq)
proof
assume
A1: seq is convergent;
then A2: r*seq is convergent by Th43;
A3: now assume
A4: r=0;
then A5: r*(lim seq)=0.REAL N by EUCLID:33;
let q such that
A6: 0<q;
take k=0;
let m such that k<=m;
|.((r*seq).m)-r*(lim seq).|=|.0 * seq.m-0.REAL N.| by A4,A5,Def3
.=|.0.REAL N-0 * seq.m.| by Th28
.=|.0.REAL N+-0 * seq.m.| by EUCLID:45
.=|.-0 * seq.m.| by EUCLID:31
.=|.0 * seq.m.| by Th27
.=|.0.REAL N.| by EUCLID:33
.=0 by Th24;
hence |.((r*seq).m)-r*(lim seq).|<q by A6;
end;
now assume
A7: r<>0;
then A8: 0<abs(r) by ABSVALUE:6;
let q such that
A9: 0<q;
A10: 0<>abs(r) by A7,ABSVALUE:6;
0/abs(r)=0;
then 0<q/abs(r) by A8,A9,REAL_1:73;
then consider n1 such that
A11: for m st n1<=m holds |.seq.m-(lim seq).|<q/abs(r) by A1,Def10;
take k=n1;
let m; assume k<=m;
then A12: |.seq.m-(lim seq).|<q/abs(r) by A11;
A13: |.((r*seq).m)-r*(lim seq).|=|.r*seq.m-r*(lim seq).| by Def3
.=|.r*(seq.m-(lim seq)).| by EUCLID:53
.=abs(r)*|.seq.m-(lim seq).| by Th8;
abs(r)*(q/abs(r))=abs(r)*(abs(r)"*q) by XCMPLX_0:def 9
.=abs(r)*abs(r)"*q by XCMPLX_1:4
.=1*q by A10,XCMPLX_0:def 7
.=q;
hence |.((r*seq).m)-r*(lim seq).|<q by A8,A12,A13,REAL_1:70;
end;
hence thesis by A2,A3,Def10;
end;
theorem
Th45:seq is convergent implies - seq is convergent
proof
assume seq is convergent;
then (-1)*seq is convergent by Th43;
hence thesis by Th12;
end;
theorem
Th46:seq is convergent implies lim(-seq)=-(lim seq)
proof
assume seq is convergent;
then lim ((-1)*seq)=(-1)*(lim seq) by Th44
.=-(1*(lim seq)) by EUCLID:44
.=-(lim seq) by EUCLID:33;
hence thesis by Th12;
end;
theorem
seq is convergent & seq' is convergent implies
seq - seq' is convergent
proof
assume that
A1: seq is convergent and
A2: seq' is convergent;
-seq' is convergent by A2,Th45;
then seq+-seq' is convergent by A1,Th41;
hence thesis by Def5;
end;
theorem
seq is convergent & seq' is convergent implies
lim(seq - seq')=(lim seq)-(lim seq')
proof
assume that
A1: seq is convergent and
A2: seq' is convergent;
A3: - seq' is convergent by A2,Th45;
thus lim(seq - seq')=lim (seq +(-seq')) by Def5
.=(lim seq)+(lim(- seq')) by A1,A3,Th42
.=(lim seq)+-(lim seq') by A2,Th46
.=(lim seq)-(lim seq') by EUCLID:45;
end;
canceled;
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
by Def9;
consider n1 such that
A2: for m st n1<=m holds |.seq.m-g.|<1 by A1;
A3: now take r=|.g.|+1;
0<=|.g.| by Th26;
then 0+0<r by REAL_1:67;
hence 0<r;
let m; assume n1<=m;
then A4: |.seq.m-g.|<1 by A2;
|.seq.m.|-|.g.|<=|.seq.m-g.| by Th33;
then A5: |.seq.m.|-|.g.|<1 by A4,AXIOMS:22;
|.seq.m.|-|.g.|+|.g.|=|.seq.m.|-(|.g.|-|.g.|) by XCMPLX_1:37
.=|.seq.m.|-(|.g.|+-|.g.|) by XCMPLX_0:def 8
.=|.seq.m.|-0 by XCMPLX_0:def 6
.=|.seq.m.|;
hence |.seq.m.|<r by A5,REAL_1:53;
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 Th39;
take r=r1+r2;
0+0<r by A6,A8,REAL_1:67;
hence 0<r;
A10: r1+0<r by A8,REAL_1:67;
A11: 0+r2<r by A6,REAL_1:67;
let m;
A12: now assume n1<=m;
then |.seq.m.|<r1 by A7;
hence |.seq.m.|<r by A10,AXIOMS:22;
end;
now assume m<=n1;
then |.seq.m.|<r2 by A9;
hence |.seq.m.|<r by A11,AXIOMS:22;
end;
hence |.seq.m.|<r by A12;
end;
hence thesis by Def8;
end;
theorem
seq is convergent implies ((lim seq) <> 0.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.REAL N;
A3: 0<=|.(lim seq).| by Th26;
0 <> |.(lim seq).| by A2,Th25;
then 0<|.(lim seq).|/2 by A3,SEQ_2:3;
then consider n1 such that
A4: for m st n1<=m holds |.seq.m-(lim seq).|<|.(lim seq).|/2 by A1,Def10;
take n=n1;
let m; assume
n<=m;
then A5: |.seq.m-(lim seq).|<|.(lim seq).|/2 by A4;
A6: |.(lim seq).|-|.seq.m.|<=|.(lim seq)-seq.m.| by Th33;
|.(lim seq)-seq.m.|=|.seq.m-(lim seq).| by Th28;
then A7: |.(lim seq).|-|.seq.m.|<|.(lim seq).|/2 by A5,A6,AXIOMS:22;
A8: |.(lim seq).|/2+(|.seq.m.|-|.(lim seq).|/2)
=|.(lim seq).|/2+-(|.(lim seq).|/2-|.seq.m.|) by XCMPLX_1:143
.=|.(lim seq).|/2-(|.(lim seq).|/2-|.seq.m.|) by XCMPLX_0:def 8
.=|.(lim seq).|/2-|.(lim seq).|/2+|.seq.m.| by XCMPLX_1:37
.=0+|.seq.m.| by XCMPLX_1:14
.=|.seq.m.|;
|.(lim seq).|-|.seq.m.|+(|.seq.m.|-|.(lim seq).|/2)
=|.(lim seq).|-|.seq.m.|+|.seq.m.|-|.(lim seq).|/2 by XCMPLX_1:29
.=|.(lim seq).|-(|.seq.m.|-|.seq.m.|)-|.(lim seq).|/2 by XCMPLX_1:37
.=|.(lim seq).|-0-|.(lim seq).|/2 by XCMPLX_1:14
.=|.(lim seq).|/2+|.(lim seq).|/2 -|.(lim seq).|/2 by XCMPLX_1:66
.=|.(lim seq).|/2+(|.(lim seq).|/2 -|.(lim seq).|/2) by XCMPLX_1:29
.=|.(lim seq).|/2+0 by XCMPLX_1:14
.=|.(lim seq).|/2;
hence |.(lim seq).|/2<|.seq.m.| by A7,A8,REAL_1:53;
end;