let X be non empty MetrSpace; :: thesis: for Y being SetSequence of X st X is complete & union (rng Y) = the carrier of X & ( for n being Nat holds (Y . n) ` in Family_open_set X ) holds
ex n0 being Nat ex r being Real ex x0 being Point of X st
( 0 < r & Ball (x0,r) c= Y . n0 )
let Y be SetSequence of X; :: thesis: ( X is complete & union (rng Y) = the carrier of X & ( for n being Nat holds (Y . n) ` in Family_open_set X ) implies ex n0 being Nat ex r being Real ex x0 being Point of X st
( 0 < r & Ball (x0,r) c= Y . n0 ) )
assume that
A1: X is complete and
A2: union (rng Y) = the carrier of X and
A3: for n being Nat holds (Y . n) ` in Family_open_set X ; :: thesis: ex n0 being Nat ex r being Real ex x0 being Point of X st
( 0 < r & Ball (x0,r) c= Y . n0 )
defpred S1[ Nat, Point of X, Real, Point of X, Real] means ( 0 < $3 & $3 < 1 / (2 |^ $1) & (Ball ($2,$3)) /\ (Y . $1) = {} implies ( 0 < $5 & $5 < 1 / (2 |^ ($1 + 1)) & Ball ($4,$5) c= Ball ($2,($3 / 2)) & (Ball ($4,$5)) /\ (Y . ($1 + 1)) = {} ) );
assume A4: for n0 being Nat
for r being Real
for x0 being Point of X holds
( not 0 < r or not Ball (x0,r) c= Y . n0 ) ; :: thesis: contradiction
now :: thesis: not (Y . 0) ` = {}
set x0 = the Point of X;
A5: ( ((Y . 0) `) ` = the carrier of X \ ((Y . 0) `) & Ball ( the Point of X,1) c= the carrier of X ) ;
assume (Y . 0) ` = {} ; :: thesis: contradiction
hence contradiction by A4, A5; :: thesis: verum
end;
then consider z0 being object such that
A6: z0 in (Y . 0) ` by XBOOLE_0:def 1;
reconsider z0 = z0 as Element of X by A6;
(Y . 0) ` in Family_open_set X by A3;
then consider t01 being Real such that
A7: 0 < t01 and
A8: Ball (z0,t01) c= (Y . 0) ` by A6, PCOMPS_1:def 4;
reconsider t0 = min (t01,(1 / 2)) as Element of REAL by XREAL_0:def 1;
t0 <= 1 / 2 by XXREAL_0:17;
then t0 < 1 / 1 by XXREAL_0:2;
then A9: t0 < 1 / (2 |^ 0) by NEWTON:4;
Ball (z0,t0) c= Ball (z0,t01) by PCOMPS_1:1, XXREAL_0:17;
then Ball (z0,t0) c= (Y . 0) ` by A8;
then Ball (z0,t0) misses Y . 0 by SUBSET_1:23;
then A10: (Ball (z0,t0)) /\ (Y . 0) = {} by XBOOLE_0:def 7;
A11: for n being Nat
for x being Point of X
for r being Real ex x1 being Point of X ex r1 being Real st
( 0 < r & r < 1 / (2 |^ n) & (Ball (x,r)) /\ (Y . n) = {} implies ( 0 < r1 & r1 < 1 / (2 |^ (n + 1)) & Ball (x1,r1) c= Ball (x,(r / 2)) & (Ball (x1,r1)) /\ (Y . (n + 1)) = {} ) )
proof
let n be Nat; :: thesis: for x being Point of X
for r being Real ex x1 being Point of X ex r1 being Real st
( 0 < r & r < 1 / (2 |^ n) & (Ball (x,r)) /\ (Y . n) = {} implies ( 0 < r1 & r1 < 1 / (2 |^ (n + 1)) & Ball (x1,r1) c= Ball (x,(r / 2)) & (Ball (x1,r1)) /\ (Y . (n + 1)) = {} ) )
let x be Point of X; :: thesis: for r being Real ex x1 being Point of X ex r1 being Real st
( 0 < r & r < 1 / (2 |^ n) & (Ball (x,r)) /\ (Y . n) = {} implies ( 0 < r1 & r1 < 1 / (2 |^ (n + 1)) & Ball (x1,r1) c= Ball (x,(r / 2)) & (Ball (x1,r1)) /\ (Y . (n + 1)) = {} ) )
let r be Real; :: thesis: ex x1 being Point of X ex r1 being Real st
( 0 < r & r < 1 / (2 |^ n) & (Ball (x,r)) /\ (Y . n) = {} implies ( 0 < r1 & r1 < 1 / (2 |^ (n + 1)) & Ball (x1,r1) c= Ball (x,(r / 2)) & (Ball (x1,r1)) /\ (Y . (n + 1)) = {} ) )
now :: thesis: ( 0 < r & r < 1 / (2 |^ n) & (Ball (x,r)) /\ (Y . n) = {} implies ex x1 being Point of X ex r1 being Real st S1[n,x,r,x1,r1] )
0 < 2 |^ (n + 2) by NEWTON:83;
then A12: 0 < 1 / (2 |^ (n + 2)) by XREAL_1:139;
0 < 2 |^ (n + 1) by NEWTON:83;
then A13: (1 / (2 |^ (n + 1))) / 2 < 1 / (2 |^ (n + 1)) by XREAL_1:139, XREAL_1:216;
2 |^ (n + 2) = 2 |^ ((n + 1) + 1)
.= (2 |^ (n + 1)) * 2 by NEWTON:6 ;
then A14: 1 / (2 |^ (n + 2)) = (1 / (2 |^ (n + 1))) / 2 by XCMPLX_1:78;
assume that
A15: 0 < r and
r < 1 / (2 |^ n) and
(Ball (x,r)) /\ (Y . n) = {} ; :: thesis: ex x1 being Point of X ex r1 being Real st S1[n,x,r,x1,r1]
not Ball (x,(r / 2)) c= Y . (n + 1) by A4, A15, XREAL_1:215;
then Ball (x,(r / 2)) meets (Y . (n + 1)) ` by SUBSET_1:24;
then consider z0 being object such that
A16: z0 in (Ball (x,(r / 2))) /\ ((Y . (n + 1)) `) by XBOOLE_0:4;
reconsider x1 = z0 as Point of X by A16;
A17: (Y . (n + 1)) ` in Family_open_set X by A3;
( Ball (x,(r / 2)) in Family_open_set X & (Y . (n + 1)) ` in Family_open_set X ) by A3, PCOMPS_1:29;
then (Ball (x,(r / 2))) /\ ((Y . (n + 1)) `) in Family_open_set X by PCOMPS_1:31;
then consider t02 being Real such that
A18: 0 < t02 and
A19: Ball (x1,t02) c= (Ball (x,(r / 2))) /\ ((Y . (n + 1)) `) by A16, PCOMPS_1:def 4;
A20: Ball (x1,t02) c= Ball (x,(r / 2)) by A19, XBOOLE_1:18;
x1 in (Y . (n + 1)) ` by A16, XBOOLE_0:def 4;
then consider t01 being Real such that
A21: 0 < t01 and
A22: Ball (x1,t01) c= (Y . (n + 1)) ` by A17, PCOMPS_1:def 4;
reconsider r1 = min ((min (t01,t02)),(1 / (2 |^ (n + 2)))) as Real ;
A23: r1 <= min (t01,t02) by XXREAL_0:17;
min (t01,t02) <= t02 by XXREAL_0:17;
then A24: Ball (x1,r1) c= Ball (x1,t02) by A23, PCOMPS_1:1, XXREAL_0:2;
min (t01,t02) <= t01 by XXREAL_0:17;
then Ball (x1,r1) c= Ball (x1,t01) by A23, PCOMPS_1:1, XXREAL_0:2;
then Ball (x1,r1) c= (Y . (n + 1)) ` by A22;
then A25: Ball (x1,r1) misses Y . (n + 1) by SUBSET_1:23;
take x1 = x1; :: thesis: ex r1 being Real st S1[n,x,r,x1,r1]
take r1 = r1; :: thesis: S1[n,x,r,x1,r1]
A26: r1 <= 1 / (2 |^ (n + 2)) by XXREAL_0:17;
0 < min (t01,t02) by A21, A18, XXREAL_0:15;
hence S1[n,x,r,x1,r1] by A20, A14, A12, A13, A24, A25, A26, XBOOLE_0:def 7, XBOOLE_1:1, XXREAL_0:2, XXREAL_0:15; :: thesis: verum
end;
hence ex x1 being Point of X ex r1 being Real st
( 0 < r & r < 1 / (2 |^ n) & (Ball (x,r)) /\ (Y . n) = {} implies ( 0 < r1 & r1 < 1 / (2 |^ (n + 1)) & Ball (x1,r1) c= Ball (x,(r / 2)) & (Ball (x1,r1)) /\ (Y . (n + 1)) = {} ) ) ; :: thesis: verum
end;
ex x0 being sequence of X ex r0 being Real_Sequence st
( x0 . 0 = z0 & r0 . 0 = t0 & ( for n being Nat st 0 < r0 . n & r0 . n < 1 / (2 |^ n) & (Ball ((x0 . n),(r0 . n))) /\ (Y . n) = {} holds
( 0 < r0 . (n + 1) & r0 . (n + 1) < 1 / (2 |^ (n + 1)) & Ball ((x0 . (n + 1)),(r0 . (n + 1))) c= Ball ((x0 . n),((r0 . n) / 2)) & (Ball ((x0 . (n + 1)),(r0 . (n + 1)))) /\ (Y . (n + 1)) = {} ) ) )
proof
defpred S2[ Nat, Element of [: the carrier of X,REAL:], Element of [: the carrier of X,REAL:]] means ( 0 < $2 `2 & $2 `2 < 1 / (2 |^ $1) & (Ball (($2 `1),($2 `2))) /\ (Y . $1) = {} implies ( 0 < $3 `2 & $3 `2 < 1 / (2 |^ ($1 + 1)) & Ball (($3 `1),($3 `2)) c= Ball (($2 `1),(($2 `2) / 2)) & (Ball (($3 `1),($3 `2))) /\ (Y . ($1 + 1)) = {} ) );
A27: for n being Nat
for u being Element of [: the carrier of X,REAL:] ex v being Element of [: the carrier of X,REAL:] st S2[n,u,v]
proof
let n be Nat; :: thesis: for u being Element of [: the carrier of X,REAL:] ex v being Element of [: the carrier of X,REAL:] st S2[n,u,v]
let u be Element of [: the carrier of X,REAL:]; :: thesis: ex v being Element of [: the carrier of X,REAL:] st S2[n,u,v]
consider v1 being Element of X, v2 being Real such that
A28: S1[n,u `1 ,u `2 ,v1,v2] by A11;
reconsider v2 = v2 as Element of REAL by XREAL_0:def 1;
take [v1,v2] ; :: thesis: S2[n,u,[v1,v2]]
thus S2[n,u,[v1,v2]] by A28; :: thesis: verum
end;
consider f being sequence of [: the carrier of X,REAL:] such that
A29: ( f . 0 = [z0,t0] & ( for n being Nat holds S2[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch 2(A27);
 take pr1 f ; :: thesis: ex r0 being Real_Sequence st
( (pr1 f) . 0 = z0 & r0 . 0 = t0 & ( for n being Nat st 0 < r0 . n & r0 . n < 1 / (2 |^ n) & (Ball (((pr1 f) . n),(r0 . n))) /\ (Y . n) = {} holds
( 0 < r0 . (n + 1) & r0 . (n + 1) < 1 / (2 |^ (n + 1)) & Ball (((pr1 f) . (n + 1)),(r0 . (n + 1))) c= Ball (((pr1 f) . n),((r0 . n) / 2)) & (Ball (((pr1 f) . (n + 1)),(r0 . (n + 1)))) /\ (Y . (n + 1)) = {} ) ) )
take pr2 f ; :: thesis: ( (pr1 f) . 0 = z0 & (pr2 f) . 0 = t0 & ( for n being Nat st 0 < (pr2 f) . n & (pr2 f) . n < 1 / (2 |^ n) & (Ball (((pr1 f) . n),((pr2 f) . n))) /\ (Y . n) = {} holds
( 0 < (pr2 f) . (n + 1) & (pr2 f) . (n + 1) < 1 / (2 |^ (n + 1)) & Ball (((pr1 f) . (n + 1)),((pr2 f) . (n + 1))) c= Ball (((pr1 f) . n),(((pr2 f) . n) / 2)) & (Ball (((pr1 f) . (n + 1)),((pr2 f) . (n + 1)))) /\ (Y . (n + 1)) = {} ) ) )
thus (pr1 f) . 0 = (f . 0) `1 by FUNCT_2:def 5
.= z0 by A29 ; :: thesis: ( (pr2 f) . 0 = t0 & ( for n being Nat st 0 < (pr2 f) . n & (pr2 f) . n < 1 / (2 |^ n) & (Ball (((pr1 f) . n),((pr2 f) . n))) /\ (Y . n) = {} holds
( 0 < (pr2 f) . (n + 1) & (pr2 f) . (n + 1) < 1 / (2 |^ (n + 1)) & Ball (((pr1 f) . (n + 1)),((pr2 f) . (n + 1))) c= Ball (((pr1 f) . n),(((pr2 f) . n) / 2)) & (Ball (((pr1 f) . (n + 1)),((pr2 f) . (n + 1)))) /\ (Y . (n + 1)) = {} ) ) )
thus (pr2 f) . 0 = (f . 0) `2 by FUNCT_2:def 6
.= t0 by A29 ; :: thesis: for n being Nat st 0 < (pr2 f) . n & (pr2 f) . n < 1 / (2 |^ n) & (Ball (((pr1 f) . n),((pr2 f) . n))) /\ (Y . n) = {} holds
( 0 < (pr2 f) . (n + 1) & (pr2 f) . (n + 1) < 1 / (2 |^ (n + 1)) & Ball (((pr1 f) . (n + 1)),((pr2 f) . (n + 1))) c= Ball (((pr1 f) . n),(((pr2 f) . n) / 2)) & (Ball (((pr1 f) . (n + 1)),((pr2 f) . (n + 1)))) /\ (Y . (n + 1)) = {} )
hereby :: thesis: verum
let i be Nat; :: thesis: S1[i,(pr1 f) . i,(pr2 f) . i,(pr1 f) . (i + 1),(pr2 f) . (i + 1)]
A30: i in NAT by ORDINAL1:def 12;
A31: ( (f . (i + 1)) `1 = (pr1 f) . (i + 1) & (f . (i + 1)) `2 = (pr2 f) . (i + 1) ) by FUNCT_2:def 5, FUNCT_2:def 6;
( (f . i) `1 = (pr1 f) . i & (f . i) `2 = (pr2 f) . i ) by FUNCT_2:def 5, FUNCT_2:def 6, A30;
hence S1[i,(pr1 f) . i,(pr2 f) . i,(pr1 f) . (i + 1),(pr2 f) . (i + 1)] by A29, A31; :: thesis: verum
end;
end;
then consider x0 being sequence of X, r0 being Real_Sequence such that
A32: ( x0 . 0 = z0 & r0 . 0 = t0 ) and
A33: for n being Nat st 0 < r0 . n & r0 . n < 1 / (2 |^ n) & (Ball ((x0 . n),(r0 . n))) /\ (Y . n) = {} holds
( 0 < r0 . (n + 1) & r0 . (n + 1) < 1 / (2 |^ (n + 1)) & Ball ((x0 . (n + 1)),(r0 . (n + 1))) c= Ball ((x0 . n),((r0 . n) / 2)) & (Ball ((x0 . (n + 1)),(r0 . (n + 1)))) /\ (Y . (n + 1)) = {} ) ;
0 < 1 / 2 ;
then A34: 0 < t0 by A7, XXREAL_0:15;
A35: for n being Nat holds
( 0 < r0 . n & r0 . n < 1 / (2 |^ n) & Ball ((x0 . (n + 1)),(r0 . (n + 1))) c= Ball ((x0 . n),((r0 . n) / 2)) & (Ball ((x0 . n),(r0 . n))) /\ (Y . n) = {} )
proof
defpred S2[ Nat] means ( 0 < r0 . $1 & r0 . $1 < 1 / (2 |^ $1) & Ball ((x0 . ($1 + 1)),(r0 . ($1 + 1))) c= Ball ((x0 . $1),((r0 . $1) / 2)) & (Ball ((x0 . $1),(r0 . $1))) /\ (Y . $1) = {} );
A36: now :: thesis: for n being Nat st S2[n] holds
S2[n + 1]
let n be Nat; :: thesis: ( S2[n] implies S2[n + 1] )
assume A37: S2[n] ; :: thesis: S2[n + 1]
then A38: (Ball ((x0 . (n + 1)),(r0 . (n + 1)))) /\ (Y . (n + 1)) = {} by A33;
( 0 < r0 . (n + 1) & r0 . (n + 1) < 1 / (2 |^ (n + 1)) ) by A33, A37;
hence S2[n + 1] by A33, A38; :: thesis: verum
end;
A39: S2[ 0 ] by A34, A9, A10, A32, A33;
thus for n being Nat holds S2[n] from NAT_1:sch 2(A39, A36); :: thesis: verum
end;
A40: for m, k being Nat holds dist ((x0 . (m + k)),(x0 . m)) <= (1 / (2 |^ m)) * (1 - (1 / (2 |^ k)))
proof
let m be Nat; :: thesis: for k being Nat holds dist ((x0 . (m + k)),(x0 . m)) <= (1 / (2 |^ m)) * (1 - (1 / (2 |^ k)))
defpred S2[ Nat] means dist ((x0 . (m + $1)),(x0 . m)) <= (1 / (2 |^ m)) * (1 - (1 / (2 |^ $1)));
A41: now :: thesis: for k being Nat st S2[k] holds
S2[k + 1]
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
assume S2[k] ; :: thesis: S2[k + 1]
then A42: (dist ((x0 . ((m + k) + 1)),(x0 . (m + k)))) + (dist ((x0 . (m + k)),(x0 . m))) <= (dist ((x0 . ((m + k) + 1)),(x0 . (m + k)))) + ((1 / (2 |^ m)) * (1 - (1 / (2 |^ k)))) by XREAL_1:6;
( 0 < r0 . ((m + k) + 1) & dist ((x0 . ((m + k) + 1)),(x0 . ((m + k) + 1))) = 0 ) by A35, METRIC_1:1;
then A43: x0 . ((m + k) + 1) in Ball ((x0 . ((m + k) + 1)),(r0 . ((m + k) + 1))) by METRIC_1:11;
r0 . (m + k) < 1 / (2 |^ (m + k)) by A35;
then (r0 . (m + k)) / 2 < (1 / (2 |^ (m + k))) / 2 by XREAL_1:74;
then (r0 . (m + k)) / 2 < 1 / ((2 |^ (m + k)) * 2) by XCMPLX_1:78;
then A44: (r0 . (m + k)) / 2 < 1 / (2 |^ ((m + k) + 1)) by NEWTON:6;
Ball ((x0 . ((m + k) + 1)),(r0 . ((m + k) + 1))) c= Ball ((x0 . (m + k)),((r0 . (m + k)) / 2)) by A35;
then dist ((x0 . ((m + k) + 1)),(x0 . (m + k))) < (r0 . (m + k)) / 2 by A43, METRIC_1:11;
then dist ((x0 . ((m + k) + 1)),(x0 . (m + k))) <= 1 / (2 |^ ((m + k) + 1)) by A44, XXREAL_0:2;
then A45: (dist ((x0 . ((m + k) + 1)),(x0 . (m + k)))) + ((1 / (2 |^ m)) * (1 - (1 / (2 |^ k)))) <= (1 / (2 |^ ((m + k) + 1))) + ((1 / (2 |^ m)) * (1 - (1 / (2 |^ k)))) by XREAL_1:6;
2 |^ (m + (k + 1)) = (2 |^ m) * (2 |^ (k + 1)) by NEWTON:8;
then 1 / (2 |^ ((m + k) + 1)) = (1 / (2 |^ m)) / ((2 |^ (k + 1)) / 1) by XCMPLX_1:78
.= (1 / (2 |^ m)) * (1 / (2 |^ (k + 1))) by XCMPLX_1:79 ;
then A46: (1 / (2 |^ ((m + k) + 1))) + ((1 / (2 |^ m)) * (1 - (1 / (2 |^ k)))) = (1 / (2 |^ m)) * (1 + ((1 / (2 |^ (k + 1))) - (1 / (2 |^ k))))
.= (1 / (2 |^ m)) * (1 + ((1 / ((2 |^ k) * 2)) - (1 / (2 |^ k)))) by NEWTON:6
.= (1 / (2 |^ m)) * (1 + (((1 / (2 |^ k)) / 2) - (1 / (2 |^ k)))) by XCMPLX_1:78
.= (1 / (2 |^ m)) * (1 - ((1 / (2 |^ k)) / 2))
.= (1 / (2 |^ m)) * (1 - (1 / ((2 |^ k) * 2))) by XCMPLX_1:78 ;
dist ((x0 . ((m + k) + 1)),(x0 . m)) <= (dist ((x0 . ((m + k) + 1)),(x0 . (m + k)))) + (dist ((x0 . (m + k)),(x0 . m))) by METRIC_1:4;
then dist ((x0 . (m + (k + 1))),(x0 . m)) <= (dist ((x0 . ((m + k) + 1)),(x0 . (m + k)))) + ((1 / (2 |^ m)) * (1 - (1 / (2 |^ k)))) by A42, XXREAL_0:2;
then dist ((x0 . (m + (k + 1))),(x0 . m)) <= (1 / (2 |^ ((m + k) + 1))) + ((1 / (2 |^ m)) * (1 - (1 / (2 |^ k)))) by A45, XXREAL_0:2;
hence S2[k + 1] by A46, NEWTON:6; :: thesis: verum
end;
2 |^ 0 = 1 by NEWTON:4;
then A47: S2[ 0 ] by METRIC_1:1;
for k being Nat holds S2[k] from NAT_1:sch 2(A47, A41);
 hence for k being Nat holds dist ((x0 . (m + k)),(x0 . m)) <= (1 / (2 |^ m)) * (1 - (1 / (2 |^ k))) ; :: thesis: verum
end;
A48: now :: thesis: for m, k being Nat holds dist ((x0 . (m + k)),(x0 . m)) < 1 / (2 |^ m)
let m be Nat; :: thesis: for k being Nat holds dist ((x0 . (m + k)),(x0 . m)) < 1 / (2 |^ m)
hereby :: thesis: verum
let k be Nat; :: thesis: dist ((x0 . (m + k)),(x0 . m)) < 1 / (2 |^ m)
A49: dist ((x0 . (m + k)),(x0 . m)) <= (1 / (2 |^ m)) * (1 - (1 / (2 |^ k))) by A40;
0 < 2 |^ k by NEWTON:83;
then 0 < 1 / (2 |^ k) by XREAL_1:139;
then A50: 1 - (1 / (2 |^ k)) < 1 - 0 by XREAL_1:10;
0 < 2 |^ m by NEWTON:83;
then 0 < 1 / (2 |^ m) by XREAL_1:139;
then (1 / (2 |^ m)) * (1 - (1 / (2 |^ k))) < (1 / (2 |^ m)) * 1 by A50, XREAL_1:68;
hence dist ((x0 . (m + k)),(x0 . m)) < 1 / (2 |^ m) by A49, XXREAL_0:2; :: thesis: verum
end;
end;
now :: thesis: for r being Real st 0 < r holds
ex p being Nat st
for n, m being Nat st n >= p & m >= p holds
dist ((x0 . n),(x0 . m)) < r
let r be Real; :: thesis: ( 0 < r implies ex p being Nat st
for n, m being Nat st n >= p & m >= p holds
dist ((x0 . n),(x0 . m)) < r )
assume 0 < r ; :: thesis: ex p being Nat st
for n, m being Nat st n >= p & m >= p holds
dist ((x0 . n),(x0 . m)) < r
then consider p1 being Nat such that
A51: 1 / (2 |^ p1) <= r by PREPOWER:92;
reconsider p = p1 + 1 as Nat ;
take p = p; :: thesis: for n, m being Nat st n >= p & m >= p holds
dist ((x0 . n),(x0 . m)) < r
hereby :: thesis: verum
let n, m be Nat; :: thesis: ( n >= p & m >= p implies dist ((x0 . n),(x0 . m)) < r )
assume that
A52: n >= p and
A53: m >= p ; :: thesis: dist ((x0 . n),(x0 . m)) < r
consider k1 being Nat such that
A54: n = p + k1 by A52, NAT_1:10;
reconsider k1 = k1 as Nat ;
n = p + k1 by A54;
then A55: dist ((x0 . n),(x0 . p)) < 1 / (2 |^ p) by A48;
consider k2 being Nat such that
A56: m = p + k2 by A53, NAT_1:10;
reconsider k2 = k2 as Nat ;
A57: 1 / (2 |^ p) = 1 / ((2 |^ p1) * 2) by NEWTON:6
.= (1 / (2 |^ p1)) / 2 by XCMPLX_1:78 ;
m = p + k2 by A56;
then A58: (dist ((x0 . n),(x0 . p))) + (dist ((x0 . p),(x0 . m))) < (1 / (2 |^ p)) + (1 / (2 |^ p)) by A48, A55, XREAL_1:8;
dist ((x0 . n),(x0 . m)) <= (dist ((x0 . n),(x0 . p))) + (dist ((x0 . p),(x0 . m))) by METRIC_1:4;
then dist ((x0 . n),(x0 . m)) < 1 / (2 |^ p1) by A58, A57, XXREAL_0:2;
hence dist ((x0 . n),(x0 . m)) < r by A51, XXREAL_0:2; :: thesis: verum
end;
end;
then x0 is Cauchy by TBSP_1:def 4;
then A59: x0 is convergent by A1, TBSP_1:def 5;
A60: for m, k being Nat holds Ball ((x0 . ((m + 1) + k)),(r0 . ((m + 1) + k))) c= Ball ((x0 . m),((r0 . m) / 2))
proof
let m be Nat; :: thesis: for k being Nat holds Ball ((x0 . ((m + 1) + k)),(r0 . ((m + 1) + k))) c= Ball ((x0 . m),((r0 . m) / 2))
defpred S2[ Nat] means Ball ((x0 . ((m + 1) + $1)),(r0 . ((m + 1) + $1))) c= Ball ((x0 . m),((r0 . m) / 2));
A61: now :: thesis: for k being Nat st S2[k] holds
S2[k + 1]
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
assume A62: S2[k] ; :: thesis: S2[k + 1]
0 < r0 . ((m + 1) + k) by A35;
then (r0 . ((m + 1) + k)) / 2 < r0 . ((m + 1) + k) by XREAL_1:216;
then A63: Ball ((x0 . ((m + 1) + k)),((r0 . ((m + 1) + k)) / 2)) c= Ball ((x0 . ((m + 1) + k)),(r0 . ((m + 1) + k))) by PCOMPS_1:1;
Ball ((x0 . ((m + 1) + (k + 1))),(r0 . ((m + 1) + (k + 1)))) = Ball ((x0 . (((m + 1) + k) + 1)),(r0 . (((m + 1) + k) + 1))) ;
then Ball ((x0 . ((m + 1) + (k + 1))),(r0 . ((m + 1) + (k + 1)))) c= Ball ((x0 . ((m + 1) + k)),((r0 . ((m + 1) + k)) / 2)) by A35;
then Ball ((x0 . ((m + 1) + (k + 1))),(r0 . ((m + 1) + (k + 1)))) c= Ball ((x0 . ((m + 1) + k)),(r0 . ((m + 1) + k))) by A63;
hence S2[k + 1] by A62, XBOOLE_1:1; :: thesis: verum
end;
A64: S2[ 0 ] by A35;
thus for k being Nat holds S2[k] from NAT_1:sch 2(A64, A61); :: thesis: verum
end;
A65: now :: thesis: for m being Nat holds lim x0 in Ball ((x0 . m),(r0 . m))
let m be Nat; :: thesis: lim x0 in Ball ((x0 . m),(r0 . m))
set m1 = m + 1;
0 < r0 . m by A35;
then 0 < (r0 . m) / 2 by XREAL_1:215;
then consider n1 being Nat such that
A66: for l being Nat st n1 <= l holds
dist ((x0 . l),(lim x0)) < (r0 . m) / 2 by A59, TBSP_1:def 3;
reconsider n = max (n1,(m + 1)) as Nat by TARSKI:1;
A67: dist ((x0 . n),(lim x0)) < (r0 . m) / 2 by A66, XXREAL_0:25;
consider k being Nat such that
A68: n = (m + 1) + k by NAT_1:10, XXREAL_0:25;
( dist ((x0 . n),(x0 . n)) = 0 & 0 < r0 . n ) by A35, METRIC_1:1;
then A69: x0 . n in Ball ((x0 . n),(r0 . n)) by METRIC_1:11;
reconsider k = k as Nat ;
n = (m + 1) + k by A68;
then Ball ((x0 . n),(r0 . n)) c= Ball ((x0 . m),((r0 . m) / 2)) by A60;
then dist ((x0 . n),(x0 . m)) < (r0 . m) / 2 by A69, METRIC_1:11;
then A70: (dist ((lim x0),(x0 . n))) + (dist ((x0 . n),(x0 . m))) < ((r0 . m) / 2) + ((r0 . m) / 2) by A67, XREAL_1:8;
dist ((lim x0),(x0 . m)) <= (dist ((lim x0),(x0 . n))) + (dist ((x0 . n),(x0 . m))) by METRIC_1:4;
then dist ((lim x0),(x0 . m)) < ((r0 . m) / 2) + ((r0 . m) / 2) by A70, XXREAL_0:2;
hence lim x0 in Ball ((x0 . m),(r0 . m)) by METRIC_1:11; :: thesis: verum
end;
A71: now :: thesis: for n being Nat holds not lim x0 in Y . n
let n be Nat; :: thesis: not lim x0 in Y . n
thus not lim x0 in Y . n :: thesis: verum
proof
assume A72: lim x0 in Y . n ; :: thesis: contradiction
lim x0 in Ball ((x0 . n),(r0 . n)) by A65;
then lim x0 in (Ball ((x0 . n),(r0 . n))) /\ (Y . n) by A72, XBOOLE_0:def 4;
hence contradiction by A35; :: thesis: verum
end;
end;
not lim x0 in union (rng Y)
proof
assume lim x0 in union (rng Y) ; :: thesis: contradiction
then consider A being set such that
A73: lim x0 in A and
A74: A in rng Y by TARSKI:def 4;
ex k being object st
( k in dom Y & A = Y . k ) by A74, FUNCT_1:def 3;
hence contradiction by A71, A73; :: thesis: verum
end;
hence contradiction by A2; :: thesis: verum