Copyright (c) 1991 Association of Mizar Users
environ
vocabulary ARYTM, PRE_TOPC, METRIC_1, ABSVALUE, ARYTM_1, FUNCT_1, RCOMP_1,
BOOLE, GROUP_1, SEQ_1, ORDINAL2, RELAT_1, POWER, LIMFUNC1, FINSET_1,
COMPTS_1, SETFAM_1, TOPMETR, PCOMPS_1, ARYTM_3, TARSKI, SEQM_3, SEQ_2;
notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
ORDINAL2, REAL_1, NAT_1, RELAT_1, FUNCT_2, METRIC_1, FINSET_1, BINOP_1,
STRUCT_0, PRE_TOPC, TOPS_2, COMPTS_1, PCOMPS_1, ABSVALUE, SEQ_1, SEQ_2,
SEQM_3, LIMFUNC1, POWER, RCOMP_1, NEWTON, TOPMETR;
constructors REAL_1, NAT_1, TOPS_2, COMPTS_1, ABSVALUE, SEQ_2, SEQM_3,
LIMFUNC1, POWER, RCOMP_1, NEWTON, TOPMETR, PARTFUN1, SEQ_4, MEMBERED,
XBOOLE_0;
clusters PRE_TOPC, FINSET_1, XREAL_0, METRIC_1, RELSET_1, SEQ_1, SEQM_3,
ARYTM_3, NEWTON, MEMBERED, ZFMISC_1, XBOOLE_0, ORDINAL2;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, SEQ_2, LIMFUNC1, COMPTS_1;
theorems ABSVALUE, AXIOMS, FINSET_1, FUNCT_1, FUNCT_2, TOPMETR, LIMFUNC1,
METRIC_1, NAT_1, NEWTON, POWER, PCOMPS_1, RCOMP_1, REAL_1, REAL_2, SEQ_1,
SEQ_2, SEQ_4, SEQM_3, SQUARE_1, TARSKI, ZFMISC_1, XREAL_0, SETFAM_1,
ORDINAL2, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1;
schemes RECDEF_1, NAT_1, SEQ_1;
begin
reserve a,b,x,y,z for real number, i,k,n,m for Nat;
reserve p,q,w for Real;
theorem Th1: for A being SubSpace of RealSpace, p,q being Point of A
st x = p & y = q holds dist(p,q) = abs( x - y )
proof
let A be SubSpace of RealSpace, p,q be Point of A;
assume A1: x = p & y = q;
A2: x is Real & y is Real by XREAL_0:def 1;
thus dist(p,q) = (the distance of A).(p,q) by METRIC_1:def 1
.= (real_dist).(x, y) by A1,METRIC_1:def 14,TOPMETR:def 1
.= abs( x - y ) by A2,METRIC_1:def 13;
end;
theorem Th2: x <= y & y <= z implies [. x,y .] \/ [. y,z .] = [. x,z .]
proof
assume A1: x <= y & y <= z;
A2: [. x,y .] \/ [. y,z .] = [. x,y .] \/ {q:y<=q & q<=z} by RCOMP_1:def 1
.= {p: x <= p & p <= y} \/ {q: y <= q & q <= z} by RCOMP_1:def 1;
now let o be set;
A3: now assume A4: o in {p: x <= p & p <= y} \/ {q: y <= q & q <= z};
now per cases by A4,XBOOLE_0:def 2;
suppose o in {p: x <= p & p <= y};
then consider a be Real such that A5: o=a & x <= a & a <= y;
x <= a & a <= z by A1,A5,AXIOMS:22;
hence o in {w: x <= w & w <= z} by A5;
suppose o in {p: y <= p & p <= z};
then consider a be Real such that A6: o=a & y <= a & a <= z;
x <= a & a <= z by A1,A6,AXIOMS:22;
hence o in {w: x <= w & w <= z} by A6;
end;
hence o in {w: x <= w & w <= z};
end;
now assume o in {w: x <= w & w <= z};
then consider r be Real such that A7: o=r & x <= r & r <= z;
x <= r & r <= y & r <= z or x <= r & y <= r & r <= z by A7;
then o in {p: x <= p & p <= y} or o in {q: y <= q & q <= z} by A7;
hence o in {p: x <= p & p <= y} \/ {q: y <= q & q <= z} by XBOOLE_0:def
2;
end;
hence o in {p: x <= p & p <= y} \/ {q: y <= q & q <= z} iff
o in {w: x <= w & w <= z} by A3;
end;
then {p: x <= p & p <= y} \/ {q: y <= q & q <= z} = {w: x <= w & w <= z}
by TARSKI:2;
hence thesis by A2,RCOMP_1:def 1;
end;
theorem Th3: x >= 0 & a + x <= b implies a <= b
proof
assume A1: x >= 0 & a + x <= b;
then a + x - x <= b - x by REAL_1:49;
then a <= b - x & b - x <= b by A1,REAL_2:173,XCMPLX_1:26;
hence thesis by AXIOMS:22;
end;
theorem Th4: x >= 0 & a - x >= b implies a >= b
proof
assume A1: x >= 0 & a - x >= b;
then a - x + x >= b + x by AXIOMS:24;
then a >= b + x & b + x >= b by A1,REAL_2:173,XCMPLX_1:27;
hence thesis by AXIOMS:22;
end;
theorem Th5: x > 0 implies x|^k > 0
proof
defpred P[Nat] means for x st x > 0 holds x|^$1 > 0;
A1: P[0]
proof
let x; x|^0 = 1 by NEWTON:9;
hence thesis;
end;
A2: for k holds P[k] implies P[k+1]
proof
let k such that A3: for x st x > 0 holds x|^k > 0;
let x; assume x > 0;
then x > 0 & x|^k > 0 & x|^(k+1) = x * x|^k by A3,NEWTON:11;
hence thesis by REAL_2:122;
end;
for k holds P[k] from Ind(A1,A2);
hence thesis;
end;
reserve seq for Real_Sequence;
theorem Th6:
seq is increasing & rng seq c= NAT implies n <= seq.n
proof
defpred P[Nat] means $1 <= seq.$1;
assume that A1: seq is increasing and A2: rng seq c= NAT;
0 in NAT;
then 0 in dom seq by FUNCT_2:def 1;
then seq.0 in rng seq by FUNCT_1:def 5;
then seq.0 is natural by A2,ORDINAL2:def 21;
then A3: P[0] by NAT_1:18;
A4: for k st P[k] holds P[k+1]
proof
let k such that A5: k <= seq.k;
k+1 in NAT;
then k+1 in dom seq by FUNCT_2:def 1;
then seq.(k+1) in rng seq by FUNCT_1:def 5;
then reconsider k' = seq.(k+1) as Nat by A2;
seq.k < seq.(k+1) by A1,SEQM_3:def 11;
then k < k' by A5,AXIOMS:22;
hence k+1 <= seq.(k+1) by NAT_1:38;
end;
for n holds P[n] from Ind(A3,A4);
hence thesis;
end;
definition let seq,k;
func k to_power seq -> Real_Sequence means
:Def1: for n holds it.n = k to_power (seq.n);
existence
proof
deffunc F(Nat) = k to_power (seq.$1);
thus ex s being Real_Sequence st for n holds
s.n = F(n) from ExRealSeq;
end;
uniqueness
proof
let s1,s2 be Real_Sequence;
assume that A1: for n holds s1.n = k to_power (seq.n) and
A2: for n holds s2.n = k to_power (seq.n);
now let n; thus s1.n = k to_power (seq.n) by A1 .= s2.n by A2; end;
hence thesis by FUNCT_2:113;
end;
end;
defpred P[Nat] means 2|^$1 >= $1 + 1;
Lm1: P[0] by NEWTON:9;
Lm2: for n st P[n] holds P[n+1]
proof
let n; assume 2|^n >= n+1;
then 2|^n - n >= 1 & 2 >= 0 by REAL_1:84;
then A1: 2*(2|^n - n) >= 2*1 by AXIOMS:25;
2|^(n+1) - (n + 1 + 1) = 2|^(n + 1) - (n + (1+1)) by XCMPLX_1:1
.= 2*2|^n - (n + 2) by NEWTON:11
.= 2*2|^n - (n + n - n + 2) by XCMPLX_1:26
.= 2*2|^n - (2*n - n + 2) by XCMPLX_1:11
.= 2*2|^n - (2*n - n) - 2 by XCMPLX_1:36
.= 2*2|^n - 2*n + n - 2 by XCMPLX_1:37
.= 2*(2|^n - n) + n - 2 by XCMPLX_1:40
.= 2*(2|^n - n) + (n - 2) by XCMPLX_1:29;
then 2|^(n+1) - (n + 1 + 1) >= 2 + (n - 2) by A1,AXIOMS:24;
then 2|^(n+1) - (n + 1 + 1) >= n & n >= 0 by NAT_1:18,XCMPLX_1:27;
then 2|^(n+1) >= 0 + (n + 1 + 1) by REAL_1:84;
hence 2|^(n+1) >= n + 1 + 1;
end;
theorem Th7:
2|^n >= n + 1
proof for n holds P[n] from Ind(Lm1,Lm2); hence thesis; end;
theorem Th8:
2|^n > n
proof
2|^n >= n + 1 & n+1 > n by Th7,NAT_1:38;
hence thesis by AXIOMS:22;
end;
theorem
Th9: seq is divergent_to+infty implies 2 to_power seq is divergent_to+infty
proof
assume A1: seq is divergent_to+infty;
let r be Real;
consider p being Nat such that A2: p > r by SEQ_4:10;
consider n such that A3: for m st n <= m holds p < seq.m by A1,LIMFUNC1:def
4;
take n; let m; assume m >= n;
then p < seq.m & 2 > 1 & 2<>0 by A3;
then 2 to_power p < 2 to_power (seq.m) & 2 to_power p = 2|^p & 2|^p > p
by Th8,POWER:44,48;
then p < 2 to_power (seq.m) by AXIOMS:22;
then r < 2 to_power (seq.m) by A2,AXIOMS:22;
hence r < (2 to_power seq).m by Def1;
end;
theorem Th10:
for T being TopSpace st the carrier of T is finite holds T is compact
proof
let T be TopSpace;
assume A1: the carrier of T is finite;
let F be Subset-Family of T such that
A2: F is_a_cover_of T & F is open;
reconsider F' = F as Subset-Family of T;
take F';
thus F' c= F & F' is_a_cover_of T by A2;
bool(the carrier of T) is finite & F' c= bool(the carrier of T)
by A1,FINSET_1:24;
hence F' is finite by FINSET_1:13;
end;
:: HEINE - BOREL THEOREM
theorem
a <= b implies Closed-Interval-TSpace(a,b) is compact
proof
set M = Closed-Interval-MSpace(a,b);
assume A1: a <= b;
reconsider a, b as Real by XREAL_0:def 1;
set r = b-a;
now per cases by A1,SQUARE_1:12;
suppose r = 0;
then a = b by XCMPLX_1:15;
then [. a,b .] = {a} & {a} is finite & the carrier of
Closed-Interval-TSpace(a,b) = [. a,b .]
by RCOMP_1:14,TOPMETR:25;
hence Closed-Interval-TSpace(a,b) is compact by Th10;
suppose A2: r > 0;
assume A3: not Closed-Interval-TSpace(a,b) is compact;
TopSpaceMetr M = Closed-Interval-TSpace(a,b) by TOPMETR:def 8;
then not M is compact by A3,TOPMETR:def 6;
then consider F being Subset-Family of M such that
A4: F is_ball-family and
A5: F is_a_cover_of M and
A6: not ex G being Subset-Family of M st
(G c= F & G is_a_cover_of M & G is finite) by TOPMETR:23;
defpred P[Element of NAT, Element of REAL, Element of REAL] means
((not ex G being Subset-Family of M st G c= F &
[. $2-(r/2|^($1+1)), $2 .] c= union G & G is finite) implies
$3 = $2 - r/2|^($1+2)) &
(not (not ex G being Subset-Family of M st G c= F &
[. $2-r/2|^($1+1), $2 .] c= union G & G is finite) implies
$3 = $2 + r/2|^($1+2));
A7: for n,p ex w st P[n,p,w]
proof
let n,p;
now per cases;
suppose A8: not ex G being Subset-Family of M st G c= F &
[. p-(r/2|^(n+1)), p .] c= union G & G is finite;
take y = p - r/2|^(n+2);
thus P[n,p,y] by A8;
suppose A9: not not ex G being Subset-Family of M st G c= F &
[. p-(r/2|^(n+1)), p .] c= union G & G is finite;
take y = p + r/2|^(n+2);
thus P[n,p,y] by A9;
end;
hence thesis;
end;
consider f being Function of NAT,REAL such that
A10: f.0 = (a+b)/2 and
A11: for n holds P[n,f.n,f.(n+1)] from RecExD(A7);
A12: for n holds f.(n+1) = f.n + r/2|^(n+2) or f.(n+1) = f.n - r/2|^(n+2)
proof
let n; P[n,f.n,f.(n+1)] by A11;
hence thesis;
end;
defpred Q[Nat] means a <= f.$1 - r/2|^($1+1) & f.$1 + r/2|^($1+1) <= b;
A13: f.0 - r/2|^(0+1) = (a+b)/2 - r/2 by A10,NEWTON:10
.= (a+b-(b-a))/2 by XCMPLX_1:121
.= ((a+b)-b+a)/2 by XCMPLX_1:37
.= (a+a)/2 by XCMPLX_1:26
.= a by XCMPLX_1:65;
A14: f.0 + r/2|^(0+1) = (a+b)/2 + r/2 by A10,NEWTON:10
.= ((b-a)+(a+b))/2 by XCMPLX_1:63
.= (b-a+a+b)/2 by XCMPLX_1:1
.= (b+b)/2 by XCMPLX_1:27
.= b by XCMPLX_1:65;
then A15: Q[0] by A13;
A16: for k st Q[k] holds Q[k+1]
proof
let k; assume Q[k];
then A17: f.k - a >= r/2|^(k+1) & b - f.k >= r/2|^(k+1)
by REAL_1:84,REAL_2:165;
A18: r/(2*(2|^(k+1))) + r/(2*(2|^(k+1))) = r/2|^(k+1)
by XCMPLX_1:119;
A19: r/2|^(k+1) - r/2|^(k+(1+1))
= r/2|^(k+1) - r/2|^((k+1)+1) by XCMPLX_1:1
.= r/2|^(k+1) - r/(2*2|^(k+1)) by NEWTON:11
.= r/(2*2|^(k+1)) by A18,XCMPLX_1:26
.= r/2|^(k+1+1) by NEWTON:11
.= r/2|^(k+(1+1)) by XCMPLX_1:1;
now per cases by A12;
suppose A20: f.(k+1) = f.k + r/2|^(k+2);
2|^(k+1) > 0 & r >= 0 by A1,Th5,SQUARE_1:12;
then A21: r/2|^(k+1) >= 0 by REAL_2:125;
f.(k+1) - a = f.k - a + r/2|^(k+2) by A20,XCMPLX_1:29;
then f.(k+1) - a >= r/2|^(k+2) by A17,A21,REAL_2:173;
then a <= f.(k+1) - r/2|^(k+(1+1)) by REAL_2:165;
hence a <= f.(k+1) - r/2|^(k+1+1) by XCMPLX_1:1;
b - f.(k+1) = b - f.k - r/2|^(k+2) by A20,XCMPLX_1:36;
then b - f.(k+1) >= r/2|^(k+2) by A17,A19,REAL_1:49;
then f.(k+1) + r/2|^(k+(1+1)) <= b by REAL_1:84;
hence f.(k+1) + r/2|^(k+1+1) <= b by XCMPLX_1:1;
suppose A22: f.(k+1) = f.k - r/2|^(k+2);
2|^(k+1) > 0 & r >= 0 by A1,Th5,SQUARE_1:12;
then A23: r/2|^(k+1) >= 0 by REAL_2:125;
f.(k+1) - a = f.k - a - r/2|^(k+2) by A22,XCMPLX_1:21;
then f.(k+1) - a >= r/2|^(k+2) by A17,A19,REAL_1:49;
then a <= f.(k+1) - r/2|^(k+(1+1)) by REAL_2:165;
hence a <= f.(k+1) - r/2|^(k+1+1) by XCMPLX_1:1;
b - f.(k+1) = b - f.k + r/2|^(k+2) by A22,XCMPLX_1:37;
then b - f.(k+1) >= r/2|^(k+2) by A17,A23,REAL_2:173;
then f.(k+1) + r/2|^(k+(1+1)) <= b by REAL_1:84;
hence f.(k+1) + r/2|^(k+1+1) <= b by XCMPLX_1:1;
end;
hence thesis;
end;
A24: for k holds Q[k] from Ind(A15,A16);
A25: rng f c= [. a,b .]
proof
let y be set; assume y in rng f;
then consider x being set such that
A26: x in dom f & y = f.x by FUNCT_1:def 5;
reconsider n = x as Nat by A26,FUNCT_2:def 1;
2|^(n+1) > 0 & r >= 0 by A1,Th5,SQUARE_1:12;
then r/2|^(n+1) >= 0 & a <= f.n - r/2|^(n+1) & f.n + r/2|^(n+1) <= b
by A24,REAL_2:125;
then a <= f.n & f.n <= b by Th3,Th4;
then y in { y1 where y1 is Real: a <= y1 & y1 <= b} by A26;
hence y in [. a,b .] by RCOMP_1:def 1;
end;
defpred R[Nat] means not ex G being Subset-Family of M st
(G c= F & [. f.$1 - r/2|^($1+1), f.$1 + r/2|^($1+1) .] c= union G &
G is finite);
A27: R[0]
proof
given G being Subset-Family of M such that
A28: G c= F and
A29: [. f.0 - r/2|^(0+1), f.0 + r/2|^(0+1) .] c= union G and
A30: G is finite;
the carrier of M c= union G by A1,A13,A14,A29,TOPMETR:14;
then G is_a_cover_of M by TOPMETR:def 5;
hence contradiction by A6,A28,A30;
end;
A31: for k st R[k] holds R[k+1]
proof
let k such that A32: R[k];
A33: r/2|^(k+(1+1)) = r/2|^(k+1+1) by XCMPLX_1:1
.= r/((2|^(k+1))*2) by NEWTON:11
.= r/(2|^(k+1))/2 by XCMPLX_1:79;
given G being Subset-Family of M such that
A34: G c= F and
A35: [. f.(k+1) - r/2|^(k+1+1), f.(k+1) + r/2|^(k+1+1) .] c= union G and
A36: G is finite;
now per cases;
suppose A37: ex G being Subset-Family of M st G c= F &
[. f.k - r/2|^(k+1), f.k .] c= union G & G is finite;
then consider G1 being Subset-Family of M such that
A38: G1 c= F and
A39: [. f.k - r/2|^(k+1), f.k .] c= union G1 and
A40: G1 is finite;
A41: f.(k+1) = f.k + r/2|^(k+2) by A11,A37;
then A42: f.(k+1) - r/2|^(k+1+1)
= f.k + r/2|^(k+2) - r/2|^(k+(1+1)) by XCMPLX_1:1
.= f.k by XCMPLX_1:26;
A43: f.(k+1) + r/2|^(k+1+1)
= f.k + r/2|^(k+2) + r/2|^(k+(1+1)) by A41,XCMPLX_1:1
.= f.k + (r/2|^(k+2) + r/2|^(k+2)) by XCMPLX_1:1
.= f.k + r/2|^(k+1) by A33,XCMPLX_1:66;
reconsider G3 = G1 \/ G as Subset-Family of M;
2|^(k+1) > 0 & r >= 0 by A1,Th5,SQUARE_1:12;
then r/2|^(k+1) >= 0 by REAL_2:125;
then f.k - r/2|^(k+1) <= f.k & f.k <=
f.k + r/2|^(k+1) by REAL_2:173;
then [. f.k - r/2|^(k+1), f.k + r/2|^(k+1).] =
[. f.k - r/2|^(k+1), f.k .] \/ [. f.k, f.k + r/2|^(k+1).] by Th2;
then [. f.k - r/2|^(k+1), f.k + r/2|^(k+1).] c= union G1 \/ union G
by A35,A39,A42,A43,XBOOLE_1:13;
then A44: [. f.k - r/2|^(k+1), f.k + r/2|^(k+1).] c= union G3
by ZFMISC_1:96;
A45: G3 is finite by A36,A40,FINSET_1:14;
G3 c= F by A34,A38,XBOOLE_1:8;
hence contradiction by A32,A44,A45;
suppose A46: not (ex G being Subset-Family of M st G c= F &
[. f.k - r/2|^(k+1), f.k .] c= union G & G is finite);
then A47: f.(k+1) = f.k - r/2|^(k+2) by A11;
then A48: f.(k+1) - r/2|^(k+1+1)
= f.k - r/2|^(k+2) - r/2|^(k+(1+1)) by XCMPLX_1:1
.= f.k - (r/2|^(k+2) + r/2|^(k+(1+1))) by XCMPLX_1:36
.= f.k - r/2|^(k+1) by A33,XCMPLX_1:66;
f.(k+1) + r/2|^(k+1+1)
= f.k - r/2|^(k+2) + r/2|^(k+(1+1)) by A47,XCMPLX_1:1
.= f.k by XCMPLX_1:27;
hence contradiction by A34,A35,A36,A46,A48;
end;
hence thesis;
end;
A49: for k holds R[k] from Ind(A27,A31);
A50: [. a,b .] is compact by RCOMP_1:24;
reconsider f as Real_Sequence;
consider s being Real_Sequence such that
A51: s is_subsequence_of f and
A52: s is convergent and
A53: lim s in [. a,b .] by A25,A50,RCOMP_1:def 3;
reconsider ls = lim s as Point of M by A1,A53,TOPMETR:14;
the carrier of M c= union F & the carrier of M = [. a,b .]
by A1,A5,TOPMETR:14,def 5;
then consider Z being set such that A54: lim s in Z & Z in F by A53,TARSKI
:def 4;
consider p being Point of M, r0 being Real such that
A55: Z = Ball(p,r0) by A4,A54,TOPMETR:def 4;
consider r1 being Real such that
A56: r1 > 0 & Ball(ls,r1) c= Ball(p,r0) by A54,A55,PCOMPS_1:30;
consider Nseq being increasing Seq_of_Nat such that
A57: s = f*Nseq by A51,SEQM_3:def 10;
A58: r1/2 > 0 by A56,REAL_2:127;
then consider n being Nat such that
A59: for m being Nat st m >= n holds abs( s.m - lim s ) < r1/2
by A52,SEQ_2:def 7;
A60: for m being Nat for q being Point of M st s.m = q & m >= n holds
dist(ls, q) < r1/2
proof
let m be Nat, q be Point of M; assume A61: s.m = q & m >= n;
then abs( s.m - lim s ) < r1/2 by A59;
then A62: abs( -(s.m - lim s) ) < r1/2 by ABSVALUE:17;
dist(ls, q)
= (the distance of M).(lim s, s.m) by A61,METRIC_1:def 1
.= (the distance of RealSpace).(ls, q) by A61,TOPMETR:def 1
.= abs( lim s - s.m ) by A61,METRIC_1:def 13,def 14;
hence thesis by A62,XCMPLX_1:143;
end;
A63: for m being Nat st m >= n holds (f*Nseq).m in Ball(ls, r1/2)
proof
let m be Nat such that A64: m >= n;
A65: dom f = NAT by FUNCT_2:def 1;
s.m = f.(Nseq.m) by A57,SEQM_3:31;
then s.m in rng f by A65,FUNCT_1:def 5;
then reconsider q = s.m as Point of M by A1,A25,TOPMETR:14;
dist(ls, q) < r1/2 by A60,A64;
hence (f*Nseq).m in Ball(ls, r1/2) by A57,METRIC_1:12;
end;
not Nseq is bounded_above
proof
let r be real number;
consider n being Nat such that A66: n > r by SEQ_4:10;
rng Nseq c= NAT by SEQM_3:def 8;
then n <= Nseq.n by Th6;
then r <= Nseq.n by A66,AXIOMS:22;
hence thesis;
end;
then Nseq is divergent_to+infty by LIMFUNC1:58;
then 2 to_power Nseq is divergent_to+infty by Th9;
then A67: (2 to_power Nseq)" is convergent & lim (2 to_power Nseq)" = 0
by LIMFUNC1:61;
then A68: lim (r(#)((2 to_power Nseq)")) = r*0 by SEQ_2:22 .= 0;
r(#)((2 to_power Nseq)") is convergent by A67,SEQ_2:21;
then consider i such that
A69: for m st i <= m holds abs( (r(#)((2 to_power Nseq)")).m - 0 ) < r1/2
by A58,A68,SEQ_2:def 7;
set l = i + 1 + n;
l = n + 1 + i by XCMPLX_1:1;
then A70: l >= n & l >= i by NAT_1:29;
[. s.l - r*(2|^(Nseq.l+1))", s.l + r*(2|^(Nseq.l+1))" .] c=
Ball(ls,r1)
proof
let z be set;
assume z in [. s.l - r*(2|^(Nseq.l+1))", s.l + r*(2|^(Nseq.l+1))" .];
then z in
{m where m is Real:
s.l - r*(2|^(Nseq.l+1))" <= m & m <= s.l + r*(2|^(Nseq.l+1))" }
by RCOMP_1:def 1;
then consider x be Real such that
A71: x = z & s.l - r*(2|^(Nseq.l+1))" <= x &
x <= s.l + r*(2|^(Nseq.l+1))";
f.(Nseq.l) - r/(2|^(Nseq.l+1)) >= a &
f.(Nseq.l) + r/(2|^(Nseq.l+1)) <= b & 2|^(Nseq.l+1) <> 0 by A24,Th5;
then f.(Nseq.l) - r*(2|^(Nseq.l+1))" >= a &
f.(Nseq.l) + r*(2|^(Nseq.l+1))" <= b by XCMPLX_0:def 9;
then s.l - r*(2|^(Nseq.l+1))" >= a & s.l + r*(2|^(Nseq.l+1))" <= b
by A57,SEQM_3:31;
then x <= b & x >= a by A71,AXIOMS:22;
then x in {m where m is Real : a <= m & m <= b};
then the carrier of M = [. a,b .] & x in [. a,b .]
by A1,RCOMP_1:def 1,TOPMETR:14;
then reconsider x' = x as Point of M;
s.l <= r*(2|^(Nseq.l+1))" + x & x - s.l <= r*(2|^(Nseq.l+1))"
by A71,REAL_1:86;
then s.l - x <= r*(2|^(Nseq.l+1))" & -(x - s.l) >= -r*(2|^(Nseq.l+1))
"
by REAL_1:50,86;
then s.l - x <= r*(2|^(Nseq.l+1))" & s.l - x >= - r*(2|^(Nseq.l+1))"
by XCMPLX_1:143;
then A72: abs( s.l - x ) <= r*(2|^(Nseq.l+1))" by ABSVALUE:12;
abs( lim s - x ) = abs( (lim s - s.l) + (s.l - x) ) by XCMPLX_1:39;
then A73: abs( lim s - x ) <= abs( lim s - s.l ) + abs( s.l - x )
by ABSVALUE:13;
A74: s.l in Ball(ls, r1/2) by A57,A63,A70;
then reconsider sl = s.l as Point of M;
dist(ls,sl) < r1/2 by A74,METRIC_1:12;
then A75: abs( lim s - s.l ) < r1/2 by Th1;
abs( (r(#)(2 to_power Nseq)").l - 0 ) < r1/2 by A69,A70;
then abs( r*((2 to_power Nseq)").l ) < r1/2 by SEQ_1:13;
then abs( r*((2 to_power Nseq).l)" ) < r1/2 by SEQ_1:def 8;
then abs( r*(2 to_power (Nseq.l))" ) < r1/2 by Def1;
then A76: abs( r*(2|^(Nseq.l))" ) < r1/2 by POWER:48;
r >= 0 & 2|^(Nseq.l+1) > 0 by A1,Th5,SQUARE_1:12;
then r >= 0 & (2|^(Nseq.l+1))" > 0 by REAL_1:72;
then r*(2|^(Nseq.l+1))" >= 0 by REAL_2:121;
then A77: abs( r*(2|^(Nseq.l+1))" ) = r*(2|^(Nseq.l+1))" by ABSVALUE:
def 1;
2|^(Nseq.l+1) = 2*2|^Nseq.l & 2 > 1 & 2|^Nseq.l > 0
by Th5,NEWTON:11;
then 2|^(Nseq.l+1) > 2|^Nseq.l & 2|^Nseq.l > 0 by REAL_2:144;
then 1/(2|^(Nseq.l+1)) < 1/(2|^Nseq.l) & 2|^Nseq.l <> 0 & 2 > 0
by REAL_2:151;
then 1/(2|^(Nseq.l+1)) < (2|^Nseq.l)" & r > 0 & 2|^(Nseq.l+1) <> 0
by A2,Th5,XCMPLX_1:217;
then (2|^(Nseq.l+1))" < (2|^Nseq.l)" & r > 0 by XCMPLX_1:217;
then r*(2|^(Nseq.l+1))" < r*(2|^Nseq.l)" by REAL_1:70;
then abs( r*(2|^(Nseq.l+1))" ) < abs( r*(2|^Nseq.l)" )
by A77,ABSVALUE:12;
then A78: abs( r*(2|^(Nseq.l+1))" ) < r1/2 by A76,AXIOMS:22;
r >= 0 & 2|^(Nseq.l+1) > 0 by A1,Th5,SQUARE_1:12;
then r >= 0 & (2|^(Nseq.l+1))" > 0 by REAL_1:72;
then r*(2|^(Nseq.l+1))" >= 0 by REAL_2:121;
then r*(2|^(Nseq.l+1))" < r1/2 by A78,ABSVALUE:def 1;
then abs( s.l - x ) < r1/2 by A72,AXIOMS:22;
then abs( lim s - s.l ) + abs( s.l - x ) < r1/2 + r1/2
by A75,REAL_1:67;
then abs( lim s - x ) < r1/2 + r1/2 by A73,AXIOMS:22;
then abs( lim s - x ) < r1 by XCMPLX_1:66;
then dist(ls,x') < r1 by Th1;
hence z in Ball(ls,r1) by A71,METRIC_1:12;
end;
then [. s.l - r*(2|^(Nseq.l+1))", s.l + r*(2|^(Nseq.l+1))" .]
c= Ball(p,r0) & 2|^(Nseq.l+1) <> 0 by A56,Th5,XBOOLE_1:1;
then [. s.l - r/2|^(Nseq.l+1), s.l + r*(2|^(Nseq.l+1))" .]
c= Ball(p,r0) by XCMPLX_0:def 9;
then [. s.l - r/2|^(Nseq.l+1), s.l + r/2|^(Nseq.l+1) .]
c= Ball(p,r0) by XCMPLX_0:def 9;
then [. f.(Nseq.l) - r/(2|^(Nseq.l+1)), s.l + r/2|^(Nseq.l+1) .]
c= Ball(p,r0) by A57,SEQM_3:31;
then A79:
[. f.(Nseq.l) - r/(2|^(Nseq.l+1)), f.(Nseq.l) + r/2|^(Nseq.l+1) .]
c= Ball(p,r0) by A57,SEQM_3:31;
set G = {Ball(p,r0)};
G c= bool the carrier of M
proof
let a be set; assume a in G;
then a = Ball(p,r0) by TARSKI:def 1;
hence thesis;
end;
then G is Subset-Family of M by SETFAM_1:def 7;
then reconsider G as Subset-Family of M;
A80: G c= F by A54,A55,ZFMISC_1:37;
[. f.(Nseq.l) - r/2|^(Nseq.l+1), f.(Nseq.l) + r/2|^(Nseq.l+1) .]
c= union G by A79,ZFMISC_1:31;
hence contradiction by A49,A80;
end;
hence thesis;
end;