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 & (Ball (p,(|.(|[x,y]| - p).| - (r * a)))) /\ y>=0-plane c= (+ (x,y,r)) " ].a,1.] ) )
assume A1: 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 & (Ball (p,(|.(|[x,y]| - p).| - (r * a)))) /\ y>=0-plane c= (+ (x,y,r)) " ].a,1.] )
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 & (Ball (p,(|.(|[x,y]| - p).| - (r * a)))) /\ y>=0-plane 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 & (Ball (p,(|.(|[x,y]| - p).| - (r * a)))) /\ y>=0-plane c= (+ (x,y,r)) " ].a,1.] )
let y, r be positive Real; :: thesis: ( (+ (x,y,r)) . p > a implies ( |.(|[x,y]| - p).| > r * a & (Ball (p,(|.(|[x,y]| - p).| - (r * a)))) /\ y>=0-plane c= (+ (x,y,r)) " ].a,1.] ) )
set f = + (x,y,r);
A2: p = |[(p `1),(p `2)]| by EUCLID:53;
then p in y>=0-plane by 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 & (Ball (p,(|.(|[x,y]| - p).| - (r * a)))) /\ y>=0-plane 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: (Ball (p,(|.(|[x,y]| - p).| - (r * a)))) /\ y>=0-plane 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 A1, A2, Def6;
then (+ (x,y,r)) . p = |.(|[x,y]| - p).| / r by A1, A2, 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, A1, A2, 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 r1 = |.(|[x,y]| - p).| - (r * a) as positive Real by XREAL_1:50;
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in (Ball (p,(|.(|[x,y]| - p).| - (r * a)))) /\ y>=0-plane or u in (+ (x,y,r)) " ].a,1.] )
assume A12: u in (Ball (p,(|.(|[x,y]| - p).| - (r * a)))) /\ y>=0-plane ; :: thesis: u in (+ (x,y,r)) " ].a,1.]
then reconsider z = u as Point of Niemytzki-plane by Lm1, XBOOLE_0:def 4;
reconsider q = z as Element of (TOP-REAL 2) by A12;
u in Ball (p,(|.(|[x,y]| - p).| - (r * a))) by A12, XBOOLE_0:def 4;
then |.(q - p).| < r1 by TOPREAL9:7;
then A13: |.(|[x,y]| - q).| + |.(q - p).| < |.(|[x,y]| - q).| + r1 by XREAL_1:6;
A14: q = |[(q `1),(q `2)]| by EUCLID:53;
then A15: q `2 >= 0 by Lm1, Th18;
|.(|[x,y]| - p).| <= |.(|[x,y]| - q).| + |.(q - p).| by TOPRNS_1:34;
then |.(|[x,y]| - p).| < |.(|[x,y]| - q).| + r1 by A13, XXREAL_0:2;
then A16: |.(|[x,y]| - p).| - r1 < (|.(|[x,y]| - q).| + r1) - r1 by XREAL_1:9;
A17: 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 A16, XREAL_1:81; :: thesis: verum
end;
(+ (x,y,r)) . z in [.0,1.] by BORSUK_1:40;
then A18: (+ (x,y,r)) . z <= 1 by XXREAL_1:1;
( not q in Ball (|[x,y]|,r) implies (+ (x,y,r)) . q = 1 ) by A15, A14, Def6;
then (+ (x,y,r)) . z in ].a,1.] by A18, A5, A17, XXREAL_1:2;
hence u in (+ (x,y,r)) " ].a,1.] by FUNCT_2:38; :: thesis: verum