let p be Point of (TOP-REAL 2); :: thesis: ( p `2 = 0 implies for x being Real
for a being non negative Real
for y, r being positive Real st (+ (x,y,r)) . p > a holds
( |.(|[x,y]| - p).| > r * a & ex r1 being positive Real st
( r1 = (|.(|[x,y]| - p).| - (r * a)) / 2 & (Ball (|[(p `1),r1]|,r1)) \/ {p} c= (+ (x,y,r)) " ].a,1.] ) ) )
A1: p = |[(p `1),(p `2)]| by EUCLID:53;
assume A2: p `2 = 0 ; :: thesis: for x being Real
for a being non negative Real
for y, r being positive Real st (+ (x,y,r)) . p > a holds
( |.(|[x,y]| - p).| > r * a & ex r1 being positive Real st
( r1 = (|.(|[x,y]| - p).| - (r * a)) / 2 & (Ball (|[(p `1),r1]|,r1)) \/ {p} c= (+ (x,y,r)) " ].a,1.] ) )
then reconsider p9 = p as Point of Niemytzki-plane by A1, Lm1, Th18;
let x be Real; :: thesis: for a being non negative Real
for y, r being positive Real st (+ (x,y,r)) . p > a holds
( |.(|[x,y]| - p).| > r * a & ex r1 being positive Real st
( r1 = (|.(|[x,y]| - p).| - (r * a)) / 2 & (Ball (|[(p `1),r1]|,r1)) \/ {p} c= (+ (x,y,r)) " ].a,1.] ) )
let a be non negative Real; :: thesis: for y, r being positive Real st (+ (x,y,r)) . p > a holds
( |.(|[x,y]| - p).| > r * a & ex r1 being positive Real st
( r1 = (|.(|[x,y]| - p).| - (r * a)) / 2 & (Ball (|[(p `1),r1]|,r1)) \/ {p} c= (+ (x,y,r)) " ].a,1.] ) )
let y, r be positive Real; :: thesis: ( (+ (x,y,r)) . p > a implies ( |.(|[x,y]| - p).| > r * a & ex r1 being positive Real st
( r1 = (|.(|[x,y]| - p).| - (r * a)) / 2 & (Ball (|[(p `1),r1]|,r1)) \/ {p} c= (+ (x,y,r)) " ].a,1.] ) ) )
set f = + (x,y,r);
p in y>=0-plane by A2, A1;
then (+ (x,y,r)) . p in [.0,1.] by Lm1, BORSUK_1:40, FUNCT_2:5;
then A3: (+ (x,y,r)) . p <= 1 by XXREAL_1:1;
assume A4: (+ (x,y,r)) . p > a ; :: thesis: ( |.(|[x,y]| - p).| > r * a & ex r1 being positive Real st
( r1 = (|.(|[x,y]| - p).| - (r * a)) / 2 & (Ball (|[(p `1),r1]|,r1)) \/ {p} c= (+ (x,y,r)) " ].a,1.] ) )
then A5: a < 1 by A3, XXREAL_0:2;
A6: |.(|[x,y]| - p).| = |.(p - |[x,y]|).| by TOPRNS_1:27;
thus |.(|[x,y]| - p).| > r * a :: thesis: ex r1 being positive Real st
( r1 = (|.(|[x,y]| - p).| - (r * a)) / 2 & (Ball (|[(p `1),r1]|,r1)) \/ {p} c= (+ (x,y,r)) " ].a,1.] )
proof
per cases ( (+ (x,y,r)) . p < 1 or (+ (x,y,r)) . p = 1 ) by A3, XXREAL_0:1;
suppose (+ (x,y,r)) . p < 1 ; :: thesis: |.(|[x,y]| - p).| > r * a
then p in Ball (|[x,y]|,r) by A2, A1, Def6;
then (+ (x,y,r)) . p = |.(|[x,y]| - p).| / r by A2, A1, Def6;
hence |.(|[x,y]| - p).| > r * a by A4, XREAL_1:79; :: thesis: verum
end;
suppose A7: (+ (x,y,r)) . p = 1 ; :: thesis: |.(|[x,y]| - p).| > r * a
now :: thesis: not p in Ball (|[x,y]|,r)
A8: r / r = 1 by XCMPLX_1:60;
assume A9: p in Ball (|[x,y]|,r) ; :: thesis: contradiction
then A10: |.(p - |[x,y]|).| < r by TOPREAL9:7;
1 = |.(|[x,y]| - p).| / r by A9, A2, A1, A7, Def6;
hence contradiction by A10, A8, A6, XREAL_1:74; :: thesis: verum
end;
then A11: |.(p - |[x,y]|).| >= r by TOPREAL9:7;
r * 1 > r * a by A5, XREAL_1:68;
hence |.(|[x,y]| - p).| > r * a by A11, A6, XXREAL_0:2; :: thesis: verum
end;
end;
end;
then reconsider r9 = |.(|[x,y]| - p).| - (r * a) as positive Real by XREAL_1:50;
take r1 = r9 / 2; :: thesis: ( r1 = (|.(|[x,y]| - p).| - (r * a)) / 2 & (Ball (|[(p `1),r1]|,r1)) \/ {p} c= (+ (x,y,r)) " ].a,1.] )
thus r1 = (|.(|[x,y]| - p).| - (r * a)) / 2 ; :: thesis: (Ball (|[(p `1),r1]|,r1)) \/ {p} c= (+ (x,y,r)) " ].a,1.]
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in (Ball (|[(p `1),r1]|,r1)) \/ {p} or u in (+ (x,y,r)) " ].a,1.] )
A12: Ball (|[(p `1),r1]|,r1) c= y>=0-plane by Th20;
assume A13: u in (Ball (|[(p `1),r1]|,r1)) \/ {p} ; :: thesis: u in (+ (x,y,r)) " ].a,1.]
then ( u in Ball (|[(p `1),r1]|,r1) or u = p9 ) by ZFMISC_1:136;
then reconsider z = u as Point of Niemytzki-plane by A12, Def3;
reconsider q = z as Element of (TOP-REAL 2) by A13;
A14: q = |[(q `1),(q `2)]| by EUCLID:53;
then A15: q `2 >= 0 by Lm1, Th18;
then A16: ( not q in Ball (|[x,y]|,r) implies (+ (x,y,r)) . q = 1 ) by A14, Def6;
per cases ( u = p9 or u in Ball (|[(p `1),r1]|,r1) ) by A13, ZFMISC_1:136;
suppose u = p9 ; :: thesis: u in (+ (x,y,r)) " ].a,1.]
then (+ (x,y,r)) . z in ].a,1.] by A4, A3, XXREAL_1:2;
hence u in (+ (x,y,r)) " ].a,1.] by FUNCT_2:38; :: thesis: verum
end;
suppose u in Ball (|[(p `1),r1]|,r1) ; :: thesis: u in (+ (x,y,r)) " ].a,1.]
then |.(q - |[(p `1),r1]|).| < r1 by TOPREAL9:7;
then A17: |.(q - |[(p `1),r1]|).| + |.(|[(p `1),r1]| - p).| < r1 + |.(|[(p `1),r1]| - p).| by XREAL_1:6;
|.(q - p).| <= |.(q - |[(p `1),r1]|).| + |.(|[(p `1),r1]| - p).| by TOPRNS_1:34;
then A18: |.(q - p).| < r1 + |.(|[(p `1),r1]| - p).| by A17, XXREAL_0:2;
reconsider r1 = r1 as Real ;
A19: |.|[0,r1]|.| = |.r1.| by TOPREAL6:23;
A20: |.(|[x,y]| - p).| <= |.(|[x,y]| - q).| + |.(q - p).| by TOPRNS_1:34;
A21: |.r1.| = r1 by ABSVALUE:def 1;
|.(|[(p `1),r1]| - p).| = |.|[((p `1) - (p `1)),(r1 - 0)]|.| by A2, A1, EUCLID:62;
then |.(|[x,y]| - q).| + |.(q - p).| < |.(|[x,y]| - q).| + (r1 + r1) by A18, A19, A21, XREAL_1:6;
then |.(|[x,y]| - p).| < |.(|[x,y]| - q).| + (r1 + r1) by A20, XXREAL_0:2;
then A22: |.(|[x,y]| - p).| - (r1 + r1) < (|.(|[x,y]| - q).| + (r1 + r1)) - (r1 + r1) by XREAL_1:9;
A23: now :: thesis: ( q in Ball (|[x,y]|,r) implies (+ (x,y,r)) . z > a )
assume q in Ball (|[x,y]|,r) ; :: thesis: (+ (x,y,r)) . z > a
then (+ (x,y,r)) . q = |.(|[x,y]| - q).| / r by A14, A15, Def6;
hence (+ (x,y,r)) . z > a by A22, XREAL_1:81; :: thesis: verum
end;
(+ (x,y,r)) . z in [.0,1.] by BORSUK_1:40;
then (+ (x,y,r)) . z <= 1 by XXREAL_1:1;
then (+ (x,y,r)) . z in ].a,1.] by A5, A16, A23, XXREAL_1:2;
hence u in (+ (x,y,r)) " ].a,1.] by FUNCT_2:38; :: thesis: verum
end;
end;