Subset of REAL;
coherence
proof
{r} c= REAL
by XREAL_0:def 1;
hence thesis;
end;
end;
theorem Th5:
for X being real-membered set holds X is non empty bounded_above
implies ex g st (for r st r in X holds r<=g) & for s st 0 convergent for Real_Sequence;
coherence by Th13;
end;
theorem
seq is convergent implies lim abs seq = |.lim seq.|
proof
assume
A1: seq is convergent;
now
let p;
assume 0 convergent for Real_Sequence;
coherence by Th16;
end;
theorem
seq is convergent implies lim (seq^\k)=lim seq by Th17;
theorem Th21:
seq^\k is convergent implies seq is convergent
proof
assume seq^\k is convergent;
then consider g1 such that
A1: for p st 0~~ Real means
:Def1:
(for r st r in X holds r<=it) & for s st 0~~~~ Real means
:Def2:
(for r st r in X holds it<=r) & for s st 0~~~~= r)
& for t st for s st s in X holds s >= t holds r >= t holds r = lower_bound X
proof
let X be non empty real-membered set;
assume that
A1: for s st s in X holds s >= r and
A2: for t st for s st s in X holds s >= t holds r >= t;
A3: for s being Real st 0 < s holds
not for t be Real st t in X holds t >= r+s by A2,XREAL_1:29;
X is bounded_below
proof
take r;
let s be ExtReal;
assume s in X;
hence thesis by A1;
end;
hence thesis by A1,A3,Def2;
end;
Lm2: for X being non empty real-membered set, r st (for s st s in X holds s <=
r) & for t st for s st s in X holds s <= t holds r <= t holds r = upper_bound X
proof
let X be non empty real-membered set, r;
assume that
A1: for s st s in X holds s <= r and
A2: for t st for s st s in X holds s <= t holds r <= t;
A3: now
let s be Real such that
A4: 0 < s;
assume for t be Real st t in X holds r-s >= t;
then r <= r-s by A2;
then r+s <= r by XREAL_1:19;
hence contradiction by A4,XREAL_1:29;
end;
X is bounded_above
proof
take r;
let s be ExtReal;
assume s in X;
hence thesis by A1;
end;
hence thesis by A1,A3,Def1;
end;
registration
let X be non empty bounded_below real-membered set;
identify lower_bound X with inf X;
compatibility
proof
A1: now
let t;
assume for s st s in X holds s >= t;
then for x being ExtReal st x in X holds t <= x;
then t is LowerBound of X by XXREAL_2:def 2;
hence inf X >= t by XXREAL_2:def 4;
end;
for s st s in X holds s >= inf X by XXREAL_2:3;
hence thesis by A1,Lm1;
end;
end;
registration
let X be non empty bounded_above real-membered set;
identify upper_bound X with sup X;
compatibility
proof
A1: now
let t;
assume for s st s in X holds t >= s;
then for x being ExtReal st x in X holds x <= t;
then t is UpperBound of X by XXREAL_2:def 1;
hence t >= sup X by XXREAL_2:def 3;
end;
for s st s in X holds s <= sup X by XXREAL_2:4;
hence thesis by A1,Lm2;
end;
end;
theorem Th9:
lower_bound {r} = r & upper_bound {r} = r by XXREAL_2:11,13;
theorem Th10:
lower_bound {r} = upper_bound {r}
proof
lower_bound {r}=r by XXREAL_2:13;
hence thesis by XXREAL_2:11;
end;
theorem
X is real-bounded non empty implies lower_bound X <= upper_bound X
proof
assume X is real-bounded non empty;
then reconsider X as real-bounded non empty real-membered set;
lower_bound X <= upper_bound X by XXREAL_2:40;
hence thesis;
end;
theorem
X is real-bounded non empty implies ((ex r,p st r in X & p in X & p<>r) iff
lower_bound X < upper_bound X)
proof
assume that
A1: X is real-bounded and
A2: X is non empty;
thus (ex r,p st r in X & p in X & p<>r) implies lower_bound X~~

~~0 implies ex k st (seq ^\k) is non-zero
proof
assume that
A1: seq is convergent and
A2: lim seq<>0;
consider n1 such that
A3: for m st n1<=m holds |.lim seq.|/2<|.seq.m.| by A1,A2,SEQ_2:16;
take k=n1;
now
let n;
(0 qua Nat)+k<=n+k by XREAL_1:7;
then |.lim seq.|/2<|.(seq.(n+k)).| by A3;
then
A4: |.lim seq.|/2<|.((seq ^\k).n).| by NAT_1:def 3;
0<|.lim seq.| by A2,COMPLEX1:47;
then 0/2<|.lim seq.|/2;
hence (seq ^\k).n<>0 by A4,ABSVALUE:2;
end;
hence thesis by SEQ_1:5;
end;
theorem
seq is convergent & lim seq<>0 implies ex seq1 st seq1 is subsequence
of seq & seq1 is non-zero
proof
assume seq is convergent & lim seq <>0;
then consider k such that
A1: seq ^\k is non-zero by Th23;
take seq ^\k;
thus thesis by A1;
end;
reconsider zz=0 as Nat;
theorem Th25:
seq is constant & (r in rng seq or ex n st seq.n=r ) implies lim seq=r
proof
assume
A1: seq is constant;
then consider r1 being Element of REAL such that
A2: rng seq={r1} by FUNCT_2:111;
A3: now
assume that
A4: r in rng seq;
consider r2 being Element of REAL such that
A5: for n being Nat holds seq.n=r2 by A1,VALUED_0:def 18;
A6: r=r1 by A4,A2,TARSKI:def 1;
now
let p such that
A7: 0~~

0 implies for seq1 st seq1 is subsequence of seq & seq1 is non-zero holds lim (seq1")=(lim seq)" proof assume that A1: seq is convergent and A2: lim seq<>0; let seq1 such that A3: seq1 is subsequence of seq and A4: seq1 is non-zero; lim seq1=lim seq by A1,A3,Th17; hence thesis by A1,A2,A3,A4,Th16,SEQ_2:22; end; ::$CT 3 LmTh28: (for n holds seq.n = 1/(n+r)) implies for p st 0

~~ (1/p)-r by Th3;
take n;
let m such that
A2: n <= m;
B0: seq.m = 1/(m+r) by A0;
(1/p)-r < m by A3,A2,XXREAL_0:2;
then
A4: (1/p)-r+r < m+r by XREAL_1:8;
then p" " > (m+r)" by A1,XREAL_1:88;
then
B1: 1/(m+r) < p;
B2: -p < -0 by A1;
0 <= m+r by A1,A4;
then -p < 1/(m+r) by B2;
hence thesis by B0,B1,SEQ_2:1;
end;
Th28:
(for n holds seq.n = 1/(n+r)) implies seq is convergent
proof
assume
A0: for n holds seq.n = 1/(n+r);
take 0;
let p;
assume 0~~

0 by A3;
then k1>=1+(0 qua Nat) by NAT_1:13;
then k1<=k1*k1 by XREAL_1:151;
then
A6: k1+r<=k1*k1+r by XREAL_1:6;
take n=k1;
let m such that
A7: n<=m;
n*n<=m*m by A7,XREAL_1:66;
then
A8: n*n+r<=m*m+r by XREAL_1:6;
p"+(0 qua Nat)~~ convergent for Real_Sequence;
coherence
proof
let seq be Real_Sequence;
assume that
A1: seq is monotone and
A2: seq is bounded;
A3: seq is non-increasing implies thesis by A2;
seq is non-decreasing implies thesis by A2;
hence thesis by A1,A3,SEQM_3:def 5;
end;
end;
theorem Th36:
seq is monotone & seq is bounded implies seq is convergent;
theorem
seq is bounded_above & seq is non-decreasing implies for n holds seq.n
<=lim seq
proof
assume that
A1: seq is bounded_above and
A2: seq is non-decreasing;
let m;
set seq1 = NAT --> seq.m;
deffunc U(Nat) = seq.($1+m);
consider seq2 such that
A3: for n holds seq2.n=U(n) from SEQ_1:sch 1;
A4: now
let n;
n in NAT by ORDINAL1:def 12;
then seq1.n=seq.m & seq2.n=seq.(m+n) by A3,FUNCOP_1:7;
hence seq1.n<=seq2.n by A2,SEQM_3:5;
end;
seq1.0=seq.m by FUNCOP_1:7;
then
A5: lim seq1=seq.m by Th25;
for n being Nat holds seq2.n=U(n) by A3;
then
A6: seq2=seq^\m by NAT_1:def 3;
then lim seq2=lim seq by A1,A2,Th17;
hence thesis by A1,A2,A5,A6,A4,SEQ_2:18;
end;
theorem
seq is bounded_below & seq is non-increasing implies for n holds lim
seq <= seq.n
proof
assume that
A1: seq is bounded_below and
A2: seq is non-increasing;
let m;
set seq1 = NAT --> seq.m;
deffunc U(Nat) = seq.($1+m);
consider seq2 such that
A3: for n holds seq2.n=U(n) from SEQ_1:sch 1;
A4: now
let n;
n in NAT by ORDINAL1:def 12;
then seq1.n=seq.m & seq2.n=seq.(m+n) by A3,FUNCOP_1:7;
hence seq2.n<=seq1.n by A2,SEQM_3:7;
end;
seq1.0=seq.m by FUNCOP_1:7;
then
A5: lim seq1=seq.m by Th25;
for n being Nat holds seq2.n=U(n) by A3;
then
A6: seq2=seq^\m by NAT_1:def 3;
then lim seq2=lim seq by A1,A2,Th17;
hence thesis by A1,A2,A5,A6,A4,SEQ_2:18;
end;
theorem Th39:
for seq ex Nseq st seq*Nseq is monotone
proof
let seq;
defpred X[Nat] means for m st $1~~~~len v1;
then m~~