let a, b be Real; :: 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 ;
set r = b - a;
now :: thesis: Closed-Interval-TSpace (a,b) is compact
per cases ( b - a = 0 or b - a > 0 ) by A1, XREAL_1:48;
suppose A2: b - a > 0 ; :: thesis: Closed-Interval-TSpace (a,b) is compact
A3: TopSpaceMetr (Closed-Interval-MSpace (a,b)) = Closed-Interval-TSpace (a,b) by TOPMETR:def 7;
assume not Closed-Interval-TSpace (a,b) is compact ; :: thesis: contradiction
then not Closed-Interval-MSpace (a,b) is compact by A3, TOPMETR:def 5;
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:16;
defpred S1[ 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 Nat
for p being Element of REAL ex w being Element of REAL st S1[n,p,w]
proof
let n be Nat; :: thesis: for p being Element of REAL ex w being Element of REAL st S1[n,p,w]
let p be Element of REAL ; :: thesis: ex w being Element of REAL st S1[n,p,w]
now :: thesis: ex y being Element of REAL st S1[n,p,y]
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]
reconsider y = p - ((b - a) / (2 |^ (n + 2))) as Element of REAL by XREAL_0:def 1;
take y = y; :: 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]
reconsider y = p + ((b - a) / (2 |^ (n + 2))) as Element of REAL by XREAL_0:def 1;
take y = y; :: thesis: S1[n,p,y]
thus S1[n,p,y] by A9; :: thesis: verum
end;
end;
end;
hence ex w being Element of REAL st S1[n,p,w] ; :: thesis: verum
end;
consider f being sequence of REAL such that
A10: f . 0 = In (((a + b) / 2),REAL) and
A11: for n being Nat holds S1[n,f . n,f . (n + 1)] from RECDEF_1:sch 2(A7);
defpred S2[ 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 );
A12: (f . 0) + ((b - a) / (2 |^ (0 + 1))) = ((a + b) / 2) + ((b - a) / 2) by A10
.= b ;
defpred S3[ Nat] means ( a <= (f . $1) - ((b - a) / (2 |^ ($1 + 1))) & (f . $1) + ((b - a) / (2 |^ ($1 + 1))) <= b );
A13: for n being 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 Nat; :: thesis: ( f . (n + 1) = (f . n) + ((b - a) / (2 |^ (n + 2))) or f . (n + 1) = (f . n) - ((b - a) / (2 |^ (n + 2))) )
reconsider n = n as Element of NAT by ORDINAL1:def 12;
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;
A14: for k being Nat st S3[k] holds
S3[k + 1]
proof
let k be Nat; :: thesis: ( S3[k] implies S3[k + 1] )
A15: ((b - a) / (2 * (2 |^ (k + 1)))) + ((b - a) / (2 * (2 |^ (k + 1)))) = (b - a) / (2 |^ (k + 1)) by XCMPLX_1:118;
A16: ((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:6
.= (b - a) / (2 |^ ((k + 1) + 1)) by A15, NEWTON:6
.= (b - a) / (2 |^ (k + (1 + 1))) ;
assume A17: S3[k] ; :: thesis: S3[k + 1]
then A18: b - (f . k) >= (b - a) / (2 |^ (k + 1)) by XREAL_1:19;
A19: (f . k) - a >= (b - a) / (2 |^ (k + 1)) by A17, XREAL_1:11;
now :: thesis: ( a <= (f . (k + 1)) - ((b - a) / (2 |^ ((k + 1) + 1))) & (f . (k + 1)) + ((b - a) / (2 |^ ((k + 1) + 1))) <= b )
per cases ( f . (k + 1) = (f . k) + ((b - a) / (2 |^ (k + 2))) or f . (k + 1) = (f . k) - ((b - a) / (2 |^ (k + 2))) ) by A13;
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:83, XREAL_1:48;
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 A19, A21, XREAL_1:31;
hence a <= (f . (k + 1)) - ((b - a) / (2 |^ ((k + 1) + 1))) by XREAL_1:11; :: 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 A18, A16, XREAL_1:9;
hence (f . (k + 1)) + ((b - a) / (2 |^ ((k + 1) + 1))) <= b by XREAL_1:19; :: 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 )
then (f . (k + 1)) - a = ((f . k) - a) - ((b - a) / (2 |^ (k + 2))) ;
then (f . (k + 1)) - a >= (b - a) / (2 |^ (k + 2)) by A19, A16, XREAL_1:9;
hence a <= (f . (k + 1)) - ((b - a) / (2 |^ ((k + 1) + 1))) by XREAL_1:11; :: thesis: (f . (k + 1)) + ((b - a) / (2 |^ ((k + 1) + 1))) <= b
( 2 |^ (k + 1) > 0 & b - a >= 0 ) by A1, NEWTON:83, XREAL_1:48;
then A23: (b - a) / (2 |^ (k + 1)) >= 0 ;
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 A18, A23, XREAL_1:31;
hence (f . (k + 1)) + ((b - a) / (2 |^ ((k + 1) + 1))) <= b by XREAL_1:19; :: thesis: verum
end;
end;
end;
hence S3[k + 1] ; :: thesis: verum
end;
A24: (f . 0) - ((b - a) / (2 |^ (0 + 1))) = ((a + b) / 2) - ((b - a) / 2) by A10
.= a ;
then A25: S3[ 0 ] by A12;
A26: for k being Nat holds S3[k] from NAT_1:sch 2(A25, A14);
A27: rng f c= [.a,b.]
proof
let y be object ; :: 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 object such that
A28: x in dom f and
A29: y = f . x by FUNCT_1:def 3;
reconsider n = x as Element of NAT by A28, FUNCT_2:def 1;
A30: ( 2 |^ (n + 1) > 0 & b - a >= 0 ) by A1, NEWTON:83, XREAL_1:48;
(f . n) + ((b - a) / (2 |^ (n + 1))) <= b by A26;
then A31: f . n <= b by A30, XREAL_1:40;
a <= (f . n) - ((b - a) / (2 |^ (n + 1))) by A26;
then a <= f . n by A30, XREAL_1:51;
then y in { y1 where y1 is Real : ( a <= y1 & y1 <= b ) } by A29, A31;
hence y in [.a,b.] by RCOMP_1:def 1; :: thesis: verum
end;
A32: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
assume A33: S2[k] ; :: thesis: S2[k + 1]
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
A37: (b - a) / (2 |^ (k + (1 + 1))) = (b - a) / (2 |^ ((k + 1) + 1))
.= (b - a) / ((2 |^ (k + 1)) * 2) by NEWTON:6
.= ((b - a) / (2 |^ (k + 1))) / 2 by XCMPLX_1:78 ;
now :: thesis: contradiction
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 A38: 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
( 2 |^ (k + 1) > 0 & b - a >= 0 ) by A1, NEWTON:83, XREAL_1:48;
then ( (f . k) - ((b - a) / (2 |^ (k + 1))) <= f . k & f . k <= (f . k) + ((b - a) / (2 |^ (k + 1))) ) by XREAL_1:31, XREAL_1:43;
then A39: [.((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;
A40: (f . (k + 1)) - ((b - a) / (2 |^ ((k + 1) + 1))) = ((f . k) + ((b - a) / (2 |^ (k + 2)))) - ((b - a) / (2 |^ (k + (1 + 1)))) by A11, A38
.= f . k ;
consider G1 being Subset-Family of (Closed-Interval-MSpace (a,b)) such that
A41: G1 c= F and
A42: [.((f . k) - ((b - a) / (2 |^ (k + 1)))),(f . k).] c= union G1 and
A43: G1 is finite by A38;
reconsider G3 = G1 \/ G as Subset-Family of (Closed-Interval-MSpace (a,b)) ;
(f . (k + 1)) + ((b - a) / (2 |^ ((k + 1) + 1))) = ((f . k) + ((b - a) / (2 |^ (k + 2)))) + ((b - a) / (2 |^ (k + (1 + 1)))) by A11, A38
.= ((f . k) + (((b - a) / (2 |^ (k + 1))) / 2)) + (((b - a) / (2 |^ (k + 1))) / 2) by A37
.= (f . k) + ((b - a) / (2 |^ (k + 1))) ;
then [.((f . k) - ((b - a) / (2 |^ (k + 1)))),((f . k) + ((b - a) / (2 |^ (k + 1)))).] c= (union G1) \/ (union G) by A35, A42, A40, A39, XBOOLE_1:13;
then [.((f . k) - ((b - a) / (2 |^ (k + 1)))),((f . k) + ((b - a) / (2 |^ (k + 1)))).] c= union G3 by ZFMISC_1:78;
hence contradiction by A33, A34, A36, A41, 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 ;
(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) - (((b - a) / (2 |^ (k + 1))) / 2)) - (((b - a) / (2 |^ (k + 1))) / 2) by A37
.= (f . k) - ((b - a) / (2 |^ (k + 1))) ;
hence contradiction by A34, A35, A36, A44, A45; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
A46: the carrier of (Closed-Interval-MSpace (a,b)) = [.a,b.] by A1, TOPMETR:10;
A47: S2[ 0 ]
proof
given G being Subset-Family of (Closed-Interval-MSpace (a,b)) such that A48: G c= F and
A49: [.((f . 0) - ((b - a) / (2 |^ (0 + 1)))),((f . 0) + ((b - a) / (2 |^ (0 + 1)))).] c= union G and
A50: G is finite ; :: thesis: contradiction
the carrier of (Closed-Interval-MSpace (a,b)) c= union G by A1, A24, A12, A49, TOPMETR:10;
then G is Cover of (Closed-Interval-MSpace (a,b)) by SETFAM_1:def 11;
hence contradiction by A6, A48, A50; :: thesis: verum
end;
reconsider f = f as Real_Sequence ;
[.a,b.] is compact by RCOMP_1:6;
then 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 A27, RCOMP_1:def 3;
reconsider ls = lim s as Point of (Closed-Interval-MSpace (a,b)) by A1, A53, TOPMETR:10;
consider Nseq being increasing sequence of NAT such that
A54: s = f * Nseq by A51, VALUED_0:def 17;
the carrier of (Closed-Interval-MSpace (a,b)) c= union F by A5, SETFAM_1:def 11;
then consider Z being set such that
A55: lim s in Z and
A56: Z in F by A53, A46, TARSKI:def 4;
consider p being Point of (Closed-Interval-MSpace (a,b)), r0 being Real such that
A57: Z = Ball (p,r0) by A4, A56, TOPMETR:def 4;
set G = {(Ball (p,r0))};
{(Ball (p,r0))} c= bool the carrier of (Closed-Interval-MSpace (a,b))
proof
let a be object ; :: 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)) ;
A58: G c= F by A56, A57, ZFMISC_1:31;
reconsider Ns = Nseq as Real_Sequence by RELSET_1:7, NUMBERS:19;
not Ns is bounded_above
proof
let r be Real; :: according to SEQ_2:def 3 :: thesis: ex b1 being set st r <= Ns . b1
consider n being Nat such that
A59: n > r by SEQ_4:3;
rng Nseq c= NAT by VALUED_0:def 6;
then n <= Ns . n by Th2;
hence ex b1 being set st r <= Ns . b1 by A59, XXREAL_0:2; :: thesis: verum
end;
then A60: 2 to_power Ns is divergent_to+infty by Th3, LIMFUNC1:31;
then A61: (2 to_power Ns) " is convergent by LIMFUNC1:34;
consider r1 being Real such that
A62: r1 > 0 and
A63: Ball (ls,r1) c= Ball (p,r0) by A55, A57, PCOMPS_1:27;
A64: r1 / 2 > 0 by A62, XREAL_1:139;
then consider n being Nat such that
A65: for m being Nat st m >= n holds
|.((s . m) - (lim s)).| < r1 / 2 by A52, SEQ_2:def 7;
A66: 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 that
A67: s . m = q and
A68: m >= n ; :: thesis: dist (ls,q) < r1 / 2
|.((s . m) - (lim s)).| < r1 / 2 by A65, A68;
then A69: |.(- ((s . m) - (lim s))).| < r1 / 2 by COMPLEX1:52;
dist (ls,q) = the distance of (Closed-Interval-MSpace (a,b)) . ((lim s),(s . m)) by A67, METRIC_1:def 1
.= the distance of RealSpace . (ls,q) by A67, TOPMETR:def 1
.= |.((lim s) - (s . m)).| by A67, METRIC_1:def 12, METRIC_1:def 13 ;
hence dist (ls,q) < r1 / 2 by A69; :: thesis: verum
end;
A70: 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 A71: m >= n ; :: thesis: (f * Nseq) . m in Ball (ls,(r1 / 2))
( dom f = NAT & s . m = f . (Nseq . m) ) by A54, FUNCT_2:15, FUNCT_2:def 1;
then s . m in rng f by FUNCT_1:def 3;
then reconsider q = s . m as Point of (Closed-Interval-MSpace (a,b)) by A1, A27, TOPMETR:10;
dist (ls,q) < r1 / 2 by A66, A71;
hence (f * Nseq) . m in Ball (ls,(r1 / 2)) by A54, METRIC_1:11; :: thesis: verum
end;
lim ((2 to_power Ns) ") = 0 by A60, LIMFUNC1:34;
then A72: lim ((b - a) (#) ((2 to_power Ns) ")) = (b - a) * 0 by A61, SEQ_2:8
.= 0 ;
(b - a) (#) ((2 to_power Ns) ") is convergent by A61, SEQ_2:7;
then consider i being Nat such that
A73: for m being Nat st i <= m holds
|.((((b - a) (#) ((2 to_power Ns) ")) . m) - 0).| < r1 / 2 by A64, A72, SEQ_2:def 7;
reconsider l = (i + 1) + n as Element of NAT by ORDINAL1:def 12;
A74: l = (n + 1) + i ;
[.((s . l) - ((b - a) * ((2 |^ ((Nseq . l) + 1)) "))),((s . l) + ((b - a) * ((2 |^ ((Nseq . l) + 1)) "))).] c= Ball (ls,r1)
proof
|.((((b - a) (#) ((2 to_power Ns) ")) . l) - 0).| < r1 / 2 by A73, A74, NAT_1:11;
then |.((b - a) * (((2 to_power Ns) ") . l)).| < r1 / 2 by SEQ_1:9;
then |.((b - a) * (((2 to_power Ns) . l) ")).| < r1 / 2 by VALUED_1:10;
then |.((b - a) * ((2 to_power (Ns . l)) ")).| < r1 / 2 by Def1;
then A75: |.((b - a) * ((2 |^ (Nseq . l)) ")).| < r1 / 2 by POWER:41;
( 2 |^ ((Nseq . l) + 1) = 2 * (2 |^ (Nseq . l)) & 2 |^ (Nseq . l) > 0 ) by NEWTON:6, NEWTON:83;
then 1 / (2 |^ ((Nseq . l) + 1)) < (2 |^ (Nseq . l)) " by XREAL_1:88, XREAL_1:155;
then A76: (b - a) * ((2 |^ ((Nseq . l) + 1)) ") < (b - a) * ((2 |^ (Nseq . l)) ") by A2, XREAL_1:68;
( 2 |^ ((Nseq . l) + 1) > 0 & b - a >= 0 ) by A1, NEWTON:83, XREAL_1:48;
then |.((b - a) * ((2 |^ ((Nseq . l) + 1)) ")).| = (b - a) * ((2 |^ ((Nseq . l) + 1)) ") by ABSVALUE:def 1;
then |.((b - a) * ((2 |^ ((Nseq . l) + 1)) ")).| < |.((b - a) * ((2 |^ (Nseq . l)) ")).| by A76, ABSVALUE:5;
then A77: |.((b - a) * ((2 |^ ((Nseq . l) + 1)) ")).| < r1 / 2 by A75, XXREAL_0:2;
( 2 |^ ((Nseq . l) + 1) > 0 & b - a >= 0 ) by A1, NEWTON:83, XREAL_1:48;
then A78: (b - a) * ((2 |^ ((Nseq . l) + 1)) ") < r1 / 2 by A77, ABSVALUE:def 1;
A79: s . l in Ball (ls,(r1 / 2)) by A54, A70, NAT_1:11;
then reconsider sl = s . l as Point of (Closed-Interval-MSpace (a,b)) ;
dist (ls,sl) < r1 / 2 by A79, METRIC_1:11;
then A80: |.((lim s) - (s . l)).| < r1 / 2 by Th1;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in [.((s . l) - ((b - a) * ((2 |^ ((Nseq . l) + 1)) "))),((s . l) + ((b - a) * ((2 |^ ((Nseq . l) + 1)) "))).] or z in Ball (ls,r1) )
A81: the carrier of (Closed-Interval-MSpace (a,b)) = [.a,b.] by A1, TOPMETR:10;
assume z in [.((s . l) - ((b - a) * ((2 |^ ((Nseq . l) + 1)) "))),((s . l) + ((b - a) * ((2 |^ ((Nseq . l) + 1)) "))).] ; :: thesis: z in Ball (ls,r1)
then z in { m where m is Real : ( (s . l) - ((b - a) * ((2 |^ ((Nseq . l) + 1)) ")) <= m & m <= (s . l) + ((b - a) * ((2 |^ ((Nseq . l) + 1)) ")) ) } by RCOMP_1:def 1;
then consider x being Real such that
A82: x = z and
A83: (s . l) - ((b - a) * ((2 |^ ((Nseq . l) + 1)) ")) <= x and
A84: x <= (s . l) + ((b - a) * ((2 |^ ((Nseq . l) + 1)) ")) ;
(f . (Nseq . l)) - ((b - a) / (2 |^ ((Nseq . l) + 1))) >= a by A26;
then (s . l) - ((b - a) * ((2 |^ ((Nseq . l) + 1)) ")) >= a by A54, FUNCT_2:15;
then A85: x >= a by A83, XXREAL_0:2;
(f . (Nseq . l)) + ((b - a) / (2 |^ ((Nseq . l) + 1))) <= b by A26;
then (s . l) + ((b - a) * ((2 |^ ((Nseq . l) + 1)) ")) <= b by A54, FUNCT_2:15;
then x <= b by A84, XXREAL_0:2;
then x in { m where m is Real : ( a <= m & m <= b ) } by A85;
then reconsider x9 = x as Point of (Closed-Interval-MSpace (a,b)) by A81, RCOMP_1:def 1;
|.((lim s) - x).| = |.(((lim s) - (s . l)) + ((s . l) - x)).| ;
then A86: |.((lim s) - x).| <= |.((lim s) - (s . l)).| + |.((s . l) - x).| by COMPLEX1:56;
x - (s . l) <= (b - a) * ((2 |^ ((Nseq . l) + 1)) ") by A84, XREAL_1:20;
then A87: - (x - (s . l)) >= - ((b - a) * ((2 |^ ((Nseq . l) + 1)) ")) by XREAL_1:24;
s . l <= ((b - a) * ((2 |^ ((Nseq . l) + 1)) ")) + x by A83, XREAL_1:20;
then (s . l) - x <= (b - a) * ((2 |^ ((Nseq . l) + 1)) ") by XREAL_1:20;
then |.((s . l) - x).| <= (b - a) * ((2 |^ ((Nseq . l) + 1)) ") by A87, ABSVALUE:5;
then |.((s . l) - x).| < r1 / 2 by A78, XXREAL_0:2;
then |.((lim s) - (s . l)).| + |.((s . l) - x).| < (r1 / 2) + (r1 / 2) by A80, XREAL_1:8;
then |.((lim s) - x).| < (r1 / 2) + (r1 / 2) by A86, XXREAL_0:2;
then dist (ls,x9) < r1 by Th1;
hence z in Ball (ls,r1) by A82, METRIC_1:11; :: thesis: verum
end;
then [.((s . l) - ((b - a) / (2 |^ ((Nseq . l) + 1)))),((s . l) + ((b - a) * ((2 |^ ((Nseq . l) + 1)) "))).] c= Ball (p,r0) by A63;
then [.((f . (Nseq . l)) - ((b - a) / (2 |^ ((Nseq . l) + 1)))),((s . l) + ((b - a) / (2 |^ ((Nseq . l) + 1)))).] c= Ball (p,r0) by A54, FUNCT_2:15;
then A88: [.((f . (Nseq . l)) - ((b - a) / (2 |^ ((Nseq . l) + 1)))),((f . (Nseq . l)) + ((b - a) / (2 |^ ((Nseq . l) + 1)))).] c= union {(Ball (p,r0))} by A54, FUNCT_2:15;
for k being Nat holds S2[k] from NAT_1:sch 2(A47, A32);
hence contradiction by A58, A88; :: thesis: verum
end;
end;
end;
hence Closed-Interval-TSpace (a,b) is compact ; :: thesis: verum