let a, b be real number ; :: thesis: ( a <= b implies Closed-Interval-TSpace a,b is compact )
set M = Closed-Interval-MSpace a,b;
assume A1: a <= b ; :: thesis: Closed-Interval-TSpace a,b is compact
reconsider a = a, b = b as Real by XREAL_0:def 1;
set r = b - a;
now
per cases ( b - a = 0 or b - a > 0 ) by A1, XREAL_1:50;
suppose A2: b - a > 0 ; :: thesis: Closed-Interval-TSpace a,b is compact
assume A3: not Closed-Interval-TSpace a,b is compact ; :: thesis: contradiction
TopSpaceMetr (Closed-Interval-MSpace a,b) = Closed-Interval-TSpace a,b by TOPMETR:def 8;
then not Closed-Interval-MSpace a,b is compact by A3, TOPMETR:def 6;
then consider F being Subset-Family of (Closed-Interval-MSpace a,b) such that
A4: F is being_ball-family and
A5: F is Cover of (Closed-Interval-MSpace a,b) and
A6: for G being Subset-Family of (Closed-Interval-MSpace a,b) holds
( not G c= F or not G is Cover of (Closed-Interval-MSpace a,b) or not G is finite ) by TOPMETR:23;
defpred S1[ Element of NAT , Element of REAL , Element of REAL ] means ( ( ( for G being Subset-Family of (Closed-Interval-MSpace a,b) holds
( not G c= F or not [.($2 - ((b - a) / (2 |^ ($1 + 1)))),$2.] c= union G or not G is finite ) ) implies $3 = $2 - ((b - a) / (2 |^ ($1 + 2))) ) & ( ex G being Subset-Family of (Closed-Interval-MSpace a,b) st
( G c= F & [.($2 - ((b - a) / (2 |^ ($1 + 1)))),$2.] c= union G & G is finite ) implies $3 = $2 + ((b - a) / (2 |^ ($1 + 2))) ) );
A7: for n being Element of NAT
for p being Real ex w being Real st S1[n,p,w]
proof
let n be Element of NAT ; :: thesis: for p being Real ex w being Real st S1[n,p,w]
let p be Real; :: thesis: ex w being Real st S1[n,p,w]
now
per cases ( for G being Subset-Family of (Closed-Interval-MSpace a,b) holds
( not G c= F or not [.(p - ((b - a) / (2 |^ (n + 1)))),p.] c= union G or not G is finite ) or ex G being Subset-Family of (Closed-Interval-MSpace a,b) st
( G c= F & [.(p - ((b - a) / (2 |^ (n + 1)))),p.] c= union G & G is finite ) ) ;
suppose A8: for G being Subset-Family of (Closed-Interval-MSpace a,b) holds
( not G c= F or not [.(p - ((b - a) / (2 |^ (n + 1)))),p.] c= union G or not G is finite ) ; :: thesis: ex y being Element of REAL st S1[n,p,y]
take y = p - ((b - a) / (2 |^ (n + 2))); :: thesis: S1[n,p,y]
thus S1[n,p,y] by A8; :: thesis: verum
end;
suppose A9: ex G being Subset-Family of (Closed-Interval-MSpace a,b) st
( G c= F & [.(p - ((b - a) / (2 |^ (n + 1)))),p.] c= union G & G is finite ) ; :: thesis: ex y being Element of REAL st S1[n,p,y]
take y = p + ((b - a) / (2 |^ (n + 2))); :: thesis: S1[n,p,y]
thus S1[n,p,y] by A9; :: thesis: verum
end;
end;
end;
hence ex w being Real st S1[n,p,w] ; :: thesis: verum
end;
consider f being Function of NAT ,REAL such that
A10: f . 0 = (a + b) / 2 and
A11: for n being Element of NAT holds S1[n,f . n,f . (n + 1)] from RECDEF_1:sch 2(A7);
A12: for n being Element of NAT holds
( f . (n + 1) = (f . n) + ((b - a) / (2 |^ (n + 2))) or f . (n + 1) = (f . n) - ((b - a) / (2 |^ (n + 2))) )
proof
let n be Element of NAT ; :: thesis: ( f . (n + 1) = (f . n) + ((b - a) / (2 |^ (n + 2))) or f . (n + 1) = (f . n) - ((b - a) / (2 |^ (n + 2))) )
S1[n,f . n,f . (n + 1)] by A11;
hence ( f . (n + 1) = (f . n) + ((b - a) / (2 |^ (n + 2))) or f . (n + 1) = (f . n) - ((b - a) / (2 |^ (n + 2))) ) ; :: thesis: verum
end;
defpred S2[ Element of NAT ] means ( a <= (f . $1) - ((b - a) / (2 |^ ($1 + 1))) & (f . $1) + ((b - a) / (2 |^ ($1 + 1))) <= b );
A13: (f . 0 ) - ((b - a) / (2 |^ (0 + 1))) = ((a + b) / 2) - ((b - a) / 2) by A10, NEWTON:10
.= a ;
A14: (f . 0 ) + ((b - a) / (2 |^ (0 + 1))) = ((a + b) / 2) + ((b - a) / 2) by A10, NEWTON:10
.= b ;
then A15: S2[ 0 ] by A13;
A16: for k being Element of NAT st S2[k] holds
S2[k + 1]
proof
let k be Element of NAT ; :: thesis: ( S2[k] implies S2[k + 1] )
assume S2[k] ; :: thesis: S2[k + 1]
then A17: ( (f . k) - a >= (b - a) / (2 |^ (k + 1)) & b - (f . k) >= (b - a) / (2 |^ (k + 1)) ) by XREAL_1:13, XREAL_1:21;
A18: ((b - a) / (2 * (2 |^ (k + 1)))) + ((b - a) / (2 * (2 |^ (k + 1)))) = (b - a) / (2 |^ (k + 1)) by XCMPLX_1:119;
A19: ((b - a) / (2 |^ (k + 1))) - ((b - a) / (2 |^ (k + (1 + 1)))) = ((b - a) / (2 |^ (k + 1))) - ((b - a) / (2 |^ ((k + 1) + 1)))
.= ((b - a) / (2 |^ (k + 1))) - ((b - a) / (2 * (2 |^ (k + 1)))) by NEWTON:11
.= (b - a) / (2 |^ ((k + 1) + 1)) by A18, NEWTON:11
.= (b - a) / (2 |^ (k + (1 + 1))) ;
now
per cases ( f . (k + 1) = (f . k) + ((b - a) / (2 |^ (k + 2))) or f . (k + 1) = (f . k) - ((b - a) / (2 |^ (k + 2))) ) by A12;
suppose A20: f . (k + 1) = (f . k) + ((b - a) / (2 |^ (k + 2))) ; :: thesis: ( a <= (f . (k + 1)) - ((b - a) / (2 |^ ((k + 1) + 1))) & (f . (k + 1)) + ((b - a) / (2 |^ ((k + 1) + 1))) <= b )
( 2 |^ (k + 1) > 0 & b - a >= 0 ) by A1, NEWTON:102, XREAL_1:50;
then A21: (b - a) / (2 |^ (k + 1)) >= 0 ;
(f . (k + 1)) - a = ((f . k) - a) + ((b - a) / (2 |^ (k + 2))) by A20;
then (f . (k + 1)) - a >= (b - a) / (2 |^ (k + 2)) by A17, A21, XREAL_1:33;
hence a <= (f . (k + 1)) - ((b - a) / (2 |^ ((k + 1) + 1))) by XREAL_1:13; :: thesis: (f . (k + 1)) + ((b - a) / (2 |^ ((k + 1) + 1))) <= b
b - (f . (k + 1)) = (b - (f . k)) - ((b - a) / (2 |^ (k + 2))) by A20;
then b - (f . (k + 1)) >= (b - a) / (2 |^ (k + 2)) by A17, A19, XREAL_1:11;
hence (f . (k + 1)) + ((b - a) / (2 |^ ((k + 1) + 1))) <= b by XREAL_1:21; :: thesis: verum
end;
suppose A22: f . (k + 1) = (f . k) - ((b - a) / (2 |^ (k + 2))) ; :: thesis: ( a <= (f . (k + 1)) - ((b - a) / (2 |^ ((k + 1) + 1))) & (f . (k + 1)) + ((b - a) / (2 |^ ((k + 1) + 1))) <= b )
( 2 |^ (k + 1) > 0 & b - a >= 0 ) by A1, NEWTON:102, XREAL_1:50;
then A23: (b - a) / (2 |^ (k + 1)) >= 0 ;
(f . (k + 1)) - a = ((f . k) - a) - ((b - a) / (2 |^ (k + 2))) by A22;
then (f . (k + 1)) - a >= (b - a) / (2 |^ (k + 2)) by A17, A19, XREAL_1:11;
hence a <= (f . (k + 1)) - ((b - a) / (2 |^ ((k + 1) + 1))) by XREAL_1:13; :: thesis: (f . (k + 1)) + ((b - a) / (2 |^ ((k + 1) + 1))) <= b
b - (f . (k + 1)) = (b - (f . k)) + ((b - a) / (2 |^ (k + 2))) by A22;
then b - (f . (k + 1)) >= (b - a) / (2 |^ (k + 2)) by A17, A23, XREAL_1:33;
hence (f . (k + 1)) + ((b - a) / (2 |^ ((k + 1) + 1))) <= b by XREAL_1:21; :: thesis: verum
end;
end;
end;
hence S2[k + 1] ; :: thesis: verum
end;
A24: for k being Element of NAT holds S2[k] from NAT_1:sch 1(A15, A16);
A25: rng f c= [.a,b.]
proof
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in [.a,b.] )
assume y in rng f ; :: thesis: y in [.a,b.]
then consider x being set such that
A26: ( x in dom f & y = f . x ) by FUNCT_1:def 5;
reconsider n = x as Element of NAT by A26, FUNCT_2:def 1;
( 2 |^ (n + 1) > 0 & b - a >= 0 ) by A1, NEWTON:102, XREAL_1:50;
then ( (b - a) / (2 |^ (n + 1)) >= 0 & a <= (f . n) - ((b - a) / (2 |^ (n + 1))) & (f . n) + ((b - a) / (2 |^ (n + 1))) <= b ) by A24;
then ( a <= f . n & f . n <= b ) by XREAL_1:42, XREAL_1:53;
then y in { y1 where y1 is Real : ( a <= y1 & y1 <= b ) } by A26;
hence y in [.a,b.] by RCOMP_1:def 1; :: thesis: verum
end;
defpred S3[ Element of NAT ] means for G being Subset-Family of (Closed-Interval-MSpace a,b) holds
( not G c= F or not [.((f . $1) - ((b - a) / (2 |^ ($1 + 1)))),((f . $1) + ((b - a) / (2 |^ ($1 + 1)))).] c= union G or not G is finite );
A27: S3[ 0 ]
proof
given G being Subset-Family of (Closed-Interval-MSpace a,b) such that A28: G c= F and
A29: [.((f . 0 ) - ((b - a) / (2 |^ (0 + 1)))),((f . 0 ) + ((b - a) / (2 |^ (0 + 1)))).] c= union G and
A30: G is finite ; :: thesis: contradiction
the carrier of (Closed-Interval-MSpace a,b) c= union G by A1, A13, A14, A29, TOPMETR:14;
then G is Cover of (Closed-Interval-MSpace a,b) by SETFAM_1:def 12;
hence contradiction by A6, A28, A30; :: thesis: verum
end;
A31: for k being Element of NAT st S3[k] holds
S3[k + 1]
proof
let k be Element of NAT ; :: thesis: ( S3[k] implies S3[k + 1] )
assume A32: S3[k] ; :: thesis: S3[k + 1]
A33: (b - a) / (2 |^ (k + (1 + 1))) = (b - a) / (2 |^ ((k + 1) + 1))
.= (b - a) / ((2 |^ (k + 1)) * 2) by NEWTON:11
.= ((b - a) / (2 |^ (k + 1))) / 2 by XCMPLX_1:79 ;
given G being Subset-Family of (Closed-Interval-MSpace a,b) such that A34: G c= F and
A35: [.((f . (k + 1)) - ((b - a) / (2 |^ ((k + 1) + 1)))),((f . (k + 1)) + ((b - a) / (2 |^ ((k + 1) + 1)))).] c= union G and
A36: G is finite ; :: thesis: contradiction
now
per cases ( ex G being Subset-Family of (Closed-Interval-MSpace a,b) st
( G c= F & [.((f . k) - ((b - a) / (2 |^ (k + 1)))),(f . k).] c= union G & G is finite ) or for G being Subset-Family of (Closed-Interval-MSpace a,b) holds
( not G c= F or not [.((f . k) - ((b - a) / (2 |^ (k + 1)))),(f . k).] c= union G or not G is finite ) ) ;
suppose A37: ex G being Subset-Family of (Closed-Interval-MSpace a,b) st
( G c= F & [.((f . k) - ((b - a) / (2 |^ (k + 1)))),(f . k).] c= union G & G is finite ) ; :: thesis: contradiction
then consider G1 being Subset-Family of (Closed-Interval-MSpace a,b) such that
A38: G1 c= F and
A39: [.((f . k) - ((b - a) / (2 |^ (k + 1)))),(f . k).] c= union G1 and
A40: G1 is finite ;
A41: (f . (k + 1)) - ((b - a) / (2 |^ ((k + 1) + 1))) = ((f . k) + ((b - a) / (2 |^ (k + 2)))) - ((b - a) / (2 |^ (k + (1 + 1)))) by A11, A37
.= f . k ;
A42: (f . (k + 1)) + ((b - a) / (2 |^ ((k + 1) + 1))) = ((f . k) + ((b - a) / (2 |^ (k + 2)))) + ((b - a) / (2 |^ (k + (1 + 1)))) by A11, A37
.= ((f . k) + (((b - a) / (2 |^ (k + 1))) / 2)) + (((b - a) / (2 |^ (k + 1))) / 2) by A33
.= (f . k) + ((b - a) / (2 |^ (k + 1))) ;
reconsider G3 = G1 \/ G as Subset-Family of (Closed-Interval-MSpace a,b) ;
( 2 |^ (k + 1) > 0 & b - a >= 0 ) by A1, NEWTON:102, XREAL_1:50;
then (b - a) / (2 |^ (k + 1)) >= 0 ;
then ( (f . k) - ((b - a) / (2 |^ (k + 1))) <= f . k & f . k <= (f . k) + ((b - a) / (2 |^ (k + 1))) ) by XREAL_1:33, XREAL_1:45;
then [.((f . k) - ((b - a) / (2 |^ (k + 1)))),((f . k) + ((b - a) / (2 |^ (k + 1)))).] = [.((f . k) - ((b - a) / (2 |^ (k + 1)))),(f . k).] \/ [.(f . k),((f . k) + ((b - a) / (2 |^ (k + 1)))).] by XXREAL_1:165;
then [.((f . k) - ((b - a) / (2 |^ (k + 1)))),((f . k) + ((b - a) / (2 |^ (k + 1)))).] c= (union G1) \/ (union G) by A35, A39, A41, A42, XBOOLE_1:13;
then A43: [.((f . k) - ((b - a) / (2 |^ (k + 1)))),((f . k) + ((b - a) / (2 |^ (k + 1)))).] c= union G3 by ZFMISC_1:96;
G3 is finite by A36, A40;
hence contradiction by A32, A34, A38, A43, XBOOLE_1:8; :: thesis: verum
end;
suppose A44: for G being Subset-Family of (Closed-Interval-MSpace a,b) holds
( not G c= F or not [.((f . k) - ((b - a) / (2 |^ (k + 1)))),(f . k).] c= union G or not G is finite ) ; :: thesis: contradiction
then A45: (f . (k + 1)) - ((b - a) / (2 |^ ((k + 1) + 1))) = ((f . k) - ((b - a) / (2 |^ (k + 2)))) - ((b - a) / (2 |^ (k + (1 + 1)))) by A11
.= ((f . k) - (((b - a) / (2 |^ (k + 1))) / 2)) - (((b - a) / (2 |^ (k + 1))) / 2) by A33
.= (f . k) - ((b - a) / (2 |^ (k + 1))) ;
(f . (k + 1)) + ((b - a) / (2 |^ ((k + 1) + 1))) = ((f . k) - ((b - a) / (2 |^ (k + 2)))) + ((b - a) / (2 |^ (k + (1 + 1)))) by A11, A44
.= f . k ;
hence contradiction by A34, A35, A36, A44, A45; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
A46: for k being Element of NAT holds S3[k] from NAT_1:sch 1(A27, A31);
A47: [.a,b.] is compact by RCOMP_1:24;
reconsider f = f as Real_Sequence ;
consider s being Real_Sequence such that
A48: s is subsequence of f and
A49: s is convergent and
A50: lim s in [.a,b.] by A25, A47, RCOMP_1:def 3;
reconsider ls = lim s as Point of (Closed-Interval-MSpace a,b) by A1, A50, TOPMETR:14;
( the carrier of (Closed-Interval-MSpace a,b) c= union F & the carrier of (Closed-Interval-MSpace a,b) = [.a,b.] ) by A1, A5, SETFAM_1:def 12, TOPMETR:14;
then consider Z being set such that
A51: ( lim s in Z & Z in F ) by A50, TARSKI:def 4;
consider p being Point of (Closed-Interval-MSpace a,b), r0 being Real such that
A52: Z = Ball p,r0 by A4, A51, TOPMETR:def 4;
consider r1 being Real such that
A53: ( r1 > 0 & Ball ls,r1 c= Ball p,r0 ) by A51, A52, PCOMPS_1:30;
consider Nseq being V34() sequence of NAT such that
A54: s = f * Nseq by A48, VALUED_0:def 17;
A55: r1 / 2 > 0 by A53, XREAL_1:141;
then consider n being Element of NAT such that
A56: for m being Element of NAT st m >= n holds
abs ((s . m) - (lim s)) < r1 / 2 by A49, SEQ_2:def 7;
A57: for m being Element of NAT
for q being Point of (Closed-Interval-MSpace a,b) st s . m = q & m >= n holds
dist ls,q < r1 / 2
proof
let m be Element of NAT ; :: thesis: for q being Point of (Closed-Interval-MSpace a,b) st s . m = q & m >= n holds
dist ls,q < r1 / 2
let q be Point of (Closed-Interval-MSpace a,b); :: thesis: ( s . m = q & m >= n implies dist ls,q < r1 / 2 )
assume A58: ( s . m = q & m >= n ) ; :: thesis: dist ls,q < r1 / 2
then abs ((s . m) - (lim s)) < r1 / 2 by A56;
then A59: abs (- ((s . m) - (lim s))) < r1 / 2 by COMPLEX1:138;
dist ls,q = the distance of (Closed-Interval-MSpace a,b) . (lim s),(s . m) by A58, METRIC_1:def 1
.= the distance of RealSpace . ls,q by A58, TOPMETR:def 1
.= abs ((lim s) - (s . m)) by A58, METRIC_1:def 13, METRIC_1:def 14 ;
hence dist ls,q < r1 / 2 by A59; :: thesis: verum
end;
A60: for m being Element of NAT st m >= n holds
(f * Nseq) . m in Ball ls,(r1 / 2)
proof
let m be Element of NAT ; :: thesis: ( m >= n implies (f * Nseq) . m in Ball ls,(r1 / 2) )
assume A61: m >= n ; :: thesis: (f * Nseq) . m in Ball ls,(r1 / 2)
A62: dom f = NAT by FUNCT_2:def 1;
s . m = f . (Nseq . m) by A54, FUNCT_2:21;
then s . m in rng f by A62, FUNCT_1:def 5;
then reconsider q = s . m as Point of (Closed-Interval-MSpace a,b) by A1, A25, TOPMETR:14;
dist ls,q < r1 / 2 by A57, A61;
hence (f * Nseq) . m in Ball ls,(r1 / 2) by A54, METRIC_1:12; :: thesis: verum
end;
reconsider Ns = Nseq as Real_Sequence by RELSET_1:17;
not Ns is bounded_above
proof
let r be real number ; :: according to SEQ_2:def 3 :: thesis: ex b1 being Element of NAT st r <= Ns . b1
consider n being Element of NAT such that
A63: n > r by SEQ_4:10;
rng Nseq c= NAT by VALUED_0:def 6;
then n <= Ns . n by Th6;
hence ex b1 being Element of NAT st r <= Ns . b1 by A63, XXREAL_0:2; :: thesis: verum
end;
then 2 to_power Ns is divergent_to+infty by Th9, LIMFUNC1:58;
then A64: ( (2 to_power Ns) " is convergent & lim ((2 to_power Ns) " ) = 0 ) by LIMFUNC1:61;
then A65: lim ((b - a) (#) ((2 to_power Ns) " )) = (b - a) * 0 by SEQ_2:22
.= 0 ;
(b - a) (#) ((2 to_power Ns) " ) is convergent by A64, SEQ_2:21;
then consider i being Element of NAT such that
A66: for m being Element of NAT st i <= m holds
abs ((((b - a) (#) ((2 to_power Ns) " )) . m) - 0 ) < r1 / 2 by A55, A65, SEQ_2:def 7;
set l = (i + 1) + n;
A67: (i + 1) + n = (n + 1) + i ;
[.((s . ((i + 1) + n)) - ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) " ))),((s . ((i + 1) + n)) + ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) " ))).] c= Ball ls,r1
proof
let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in [.((s . ((i + 1) + n)) - ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) " ))),((s . ((i + 1) + n)) + ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) " ))).] or z in Ball ls,r1 )
assume z in [.((s . ((i + 1) + n)) - ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) " ))),((s . ((i + 1) + n)) + ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) " ))).] ; :: thesis: z in Ball ls,r1
then z in { m where m is Real : ( (s . ((i + 1) + n)) - ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) " )) <= m & m <= (s . ((i + 1) + n)) + ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) " )) ) } by RCOMP_1:def 1;
then consider x being Real such that
A68: ( x = z & (s . ((i + 1) + n)) - ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) " )) <= x & x <= (s . ((i + 1) + n)) + ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) " )) ) ;
( (f . (Nseq . ((i + 1) + n))) - ((b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1))) >= a & (f . (Nseq . ((i + 1) + n))) + ((b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1))) <= b & 2 |^ ((Nseq . ((i + 1) + n)) + 1) <> 0 ) by A24, NEWTON:102;
then ( (f . (Nseq . ((i + 1) + n))) - ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) " )) >= a & (f . (Nseq . ((i + 1) + n))) + ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) " )) <= b ) ;
then ( (s . ((i + 1) + n)) - ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) " )) >= a & (s . ((i + 1) + n)) + ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) " )) <= b ) by A54, FUNCT_2:21;
then ( x <= b & x >= a ) by A68, XXREAL_0:2;
then x in { m where m is Real : ( a <= m & m <= b ) } ;
then ( the carrier of (Closed-Interval-MSpace a,b) = [.a,b.] & x in [.a,b.] ) by A1, RCOMP_1:def 1, TOPMETR:14;
then reconsider x' = x as Point of (Closed-Interval-MSpace a,b) ;
( s . ((i + 1) + n) <= ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) " )) + x & x - (s . ((i + 1) + n)) <= (b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) " ) ) by A68, XREAL_1:22;
then ( (s . ((i + 1) + n)) - x <= (b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) " ) & - (x - (s . ((i + 1) + n))) >= - ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) " )) ) by XREAL_1:22, XREAL_1:26;
then A69: abs ((s . ((i + 1) + n)) - x) <= (b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) " ) by ABSVALUE:12;
abs ((lim s) - x) = abs (((lim s) - (s . ((i + 1) + n))) + ((s . ((i + 1) + n)) - x)) ;
then A70: abs ((lim s) - x) <= (abs ((lim s) - (s . ((i + 1) + n)))) + (abs ((s . ((i + 1) + n)) - x)) by COMPLEX1:142;
A71: s . ((i + 1) + n) in Ball ls,(r1 / 2) by A54, A60, NAT_1:11;
then reconsider sl = s . ((i + 1) + n) as Point of (Closed-Interval-MSpace a,b) ;
dist ls,sl < r1 / 2 by A71, METRIC_1:12;
then A72: abs ((lim s) - (s . ((i + 1) + n))) < r1 / 2 by Th1;
abs ((((b - a) (#) ((2 to_power Ns) " )) . ((i + 1) + n)) - 0 ) < r1 / 2 by A66, A67, NAT_1:11;
then abs ((b - a) * (((2 to_power Ns) " ) . ((i + 1) + n))) < r1 / 2 by SEQ_1:13;
then abs ((b - a) * (((2 to_power Ns) . ((i + 1) + n)) " )) < r1 / 2 by VALUED_1:10;
then abs ((b - a) * ((2 to_power (Ns . ((i + 1) + n))) " )) < r1 / 2 by Def1;
then A73: abs ((b - a) * ((2 |^ (Nseq . ((i + 1) + n))) " )) < r1 / 2 by POWER:46;
( b - a >= 0 & 2 |^ ((Nseq . ((i + 1) + n)) + 1) > 0 ) by A1, NEWTON:102, XREAL_1:50;
then ( b - a >= 0 & (2 |^ ((Nseq . ((i + 1) + n)) + 1)) " > 0 ) ;
then (b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) " ) >= 0 ;
then A74: abs ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) " )) = (b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) " ) by ABSVALUE:def 1;
( 2 |^ ((Nseq . ((i + 1) + n)) + 1) = 2 * (2 |^ (Nseq . ((i + 1) + n))) & 2 > 1 & 2 |^ (Nseq . ((i + 1) + n)) > 0 ) by NEWTON:11, NEWTON:102;
then ( 2 |^ ((Nseq . ((i + 1) + n)) + 1) > 2 |^ (Nseq . ((i + 1) + n)) & 2 |^ (Nseq . ((i + 1) + n)) > 0 ) by XREAL_1:157;
then ( 1 / (2 |^ ((Nseq . ((i + 1) + n)) + 1)) < 1 / (2 |^ (Nseq . ((i + 1) + n))) & 2 |^ (Nseq . ((i + 1) + n)) <> 0 & 2 > 0 ) by XREAL_1:90;
then ( 1 / (2 |^ ((Nseq . ((i + 1) + n)) + 1)) < (2 |^ (Nseq . ((i + 1) + n))) " & b - a > 0 & 2 |^ ((Nseq . ((i + 1) + n)) + 1) <> 0 ) by A2, NEWTON:102;
then ( (2 |^ ((Nseq . ((i + 1) + n)) + 1)) " < (2 |^ (Nseq . ((i + 1) + n))) " & b - a > 0 ) ;
then (b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) " ) < (b - a) * ((2 |^ (Nseq . ((i + 1) + n))) " ) by XREAL_1:70;
then abs ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) " )) < abs ((b - a) * ((2 |^ (Nseq . ((i + 1) + n))) " )) by A74, ABSVALUE:12;
then A75: abs ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) " )) < r1 / 2 by A73, XXREAL_0:2;
( b - a >= 0 & 2 |^ ((Nseq . ((i + 1) + n)) + 1) > 0 ) by A1, NEWTON:102, XREAL_1:50;
then ( b - a >= 0 & (2 |^ ((Nseq . ((i + 1) + n)) + 1)) " > 0 ) ;
then (b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) " ) >= 0 ;
then (b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) " ) < r1 / 2 by A75, ABSVALUE:def 1;
then abs ((s . ((i + 1) + n)) - x) < r1 / 2 by A69, XXREAL_0:2;
then (abs ((lim s) - (s . ((i + 1) + n)))) + (abs ((s . ((i + 1) + n)) - x)) < (r1 / 2) + (r1 / 2) by A72, XREAL_1:10;
then abs ((lim s) - x) < (r1 / 2) + (r1 / 2) by A70, XXREAL_0:2;
then dist ls,x' < r1 by Th1;
hence z in Ball ls,r1 by A68, METRIC_1:12; :: thesis: verum
end;
then ( [.((s . ((i + 1) + n)) - ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) " ))),((s . ((i + 1) + n)) + ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) " ))).] c= Ball p,r0 & 2 |^ ((Nseq . ((i + 1) + n)) + 1) <> 0 ) by A53, NEWTON:102, XBOOLE_1:1;
then [.((s . ((i + 1) + n)) - ((b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1)))),((s . ((i + 1) + n)) + ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) " ))).] c= Ball p,r0 ;
then [.((s . ((i + 1) + n)) - ((b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1)))),((s . ((i + 1) + n)) + ((b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1)))).] c= Ball p,r0 ;
then [.((f . (Nseq . ((i + 1) + n))) - ((b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1)))),((s . ((i + 1) + n)) + ((b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1)))).] c= Ball p,r0 by A54, FUNCT_2:21;
then A76: [.((f . (Nseq . ((i + 1) + n))) - ((b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1)))),((f . (Nseq . ((i + 1) + n))) + ((b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1)))).] c= Ball p,r0 by A54, FUNCT_2:21;
set G = {(Ball p,r0)};
{(Ball p,r0)} c= bool the carrier of (Closed-Interval-MSpace a,b)
proof
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in {(Ball p,r0)} or a in bool the carrier of (Closed-Interval-MSpace a,b) )
assume a in {(Ball p,r0)} ; :: thesis: a in bool the carrier of (Closed-Interval-MSpace a,b)
then a = Ball p,r0 by TARSKI:def 1;
hence a in bool the carrier of (Closed-Interval-MSpace a,b) ; :: thesis: verum
end;
then reconsider G = {(Ball p,r0)} as Subset-Family of (Closed-Interval-MSpace a,b) ;
A77: G c= F by A51, A52, ZFMISC_1:37;
[.((f . (Nseq . ((i + 1) + n))) - ((b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1)))),((f . (Nseq . ((i + 1) + n))) + ((b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1)))).] c= union G by A76, ZFMISC_1:31;
hence contradiction by A46, A77; :: thesis: verum
end;
end;
end;
hence Closed-Interval-TSpace a,b is compact ; :: thesis: verum