let p be Point of (TOP-REAL 2); ( p `2 = 0 implies for x being Real
for r being positive Real st (+ (x,r)) . p = 1 holds
ex r1 being positive Real st (Ball (|[(p `1),r1]|,r1)) \/ {p} c= (+ (x,r)) " {1} )
assume A1:
p `2 = 0
; for x being Real
for r being positive Real st (+ (x,r)) . p = 1 holds
ex r1 being positive Real st (Ball (|[(p `1),r1]|,r1)) \/ {p} c= (+ (x,r)) " {1}
let x be Real; for r being positive Real st (+ (x,r)) . p = 1 holds
ex r1 being positive Real st (Ball (|[(p `1),r1]|,r1)) \/ {p} c= (+ (x,r)) " {1}
let r be positive Real; ( (+ (x,r)) . p = 1 implies ex r1 being positive Real st (Ball (|[(p `1),r1]|,r1)) \/ {p} c= (+ (x,r)) " {1} )
set r1 = (|.(p - |[x,r]|).| - r) / 2;
set f = + (x,r);
A2:
p = |[(p `1),(p `2)]|
by EUCLID:53;
assume A3:
(+ (x,r)) . p = 1
; ex r1 being positive Real st (Ball (|[(p `1),r1]|,r1)) \/ {p} c= (+ (x,r)) " {1}
then
(p `1) - x <> 0
by A2, A1, Def5;
then
((p `1) - x) ^2 > 0
by SQUARE_1:12;
then
(((p `1) - x) ^2) + ((0 - r) ^2) > 0 + ((0 - r) ^2)
by XREAL_1:6;
then
|.|[((p `1) - x),((p `2) - r)]|.| ^2 > r ^2
by A1, Th9;
then
|.(p - |[x,r]|).| ^2 > r ^2
by A2, EUCLID:62;
then
|.(p - |[x,r]|).| > r
by SQUARE_1:15;
then
|.(p - |[x,r]|).| - r > 0
by XREAL_1:50;
then reconsider r1 = (|.(p - |[x,r]|).| - r) / 2 as positive Real ;
take
r1
; (Ball (|[(p `1),r1]|,r1)) \/ {p} c= (+ (x,r)) " {1}
let u be object ; TARSKI:def 3 ( not u in (Ball (|[(p `1),r1]|,r1)) \/ {p} or u in (+ (x,r)) " {1} )
assume A4:
u in (Ball (|[(p `1),r1]|,r1)) \/ {p}
; u in (+ (x,r)) " {1}
then reconsider q = u as Point of (TOP-REAL 2) ;
A5:
Ball (|[(p `1),r1]|,r1) c= y>=0-plane
by Th20;
( u in Ball (|[(p `1),r1]|,r1) or u = p )
by A4, ZFMISC_1:136;
then reconsider z = q as Point of Niemytzki-plane by A5, A1, A2, Lm1, Th18;
A6:
q = |[(q `1),(q `2)]|
by EUCLID:53;
A7:
now ( q in Ball (|[(p `1),r1]|,r1) implies ( not q in Ball (|[x,r]|,r) & q `2 <> 0 ) )assume A8:
q in Ball (
|[(p `1),r1]|,
r1)
;
( not q in Ball (|[x,r]|,r) & q `2 <> 0 )then
|.(q - |[(p `1),r1]|).| < r1
by TOPREAL9:7;
then A9:
|.(q - |[(p `1),r1]|).| + |.(|[(p `1),r1]| - p).| < r1 + |.(|[(p `1),r1]| - p).|
by XREAL_1:6;
A10:
|.r1.| = r1
by ABSVALUE:def 1;
A11:
|.(q - |[(p `1),r1]|).| + |.(|[(p `1),r1]| - p).| >= |.(q - p).|
by TOPRNS_1:34;
A12:
|.(q - p).| + |.(|[x,r]| - q).| >= |.(|[x,r]| - p).|
by TOPRNS_1:34;
A13:
|.|[0,r1]|.| = |.r1.|
by TOPREAL6:23;
|[(p `1),r1]| - p = |[((p `1) - (p `1)),(r1 - 0)]|
by A1, A2, EUCLID:62;
then
r1 + r1 > |.(q - p).|
by A9, A11, A10, A13, XXREAL_0:2;
then
(|.(p - |[x,r]|).| - r) + |.(|[x,r]| - q).| > |.(q - p).| + |.(|[x,r]| - q).|
by XREAL_1:6;
then
|.(|[x,r]| - p).| < (|.(p - |[x,r]|).| - r) + |.(|[x,r]| - q).|
by A12, XXREAL_0:2;
then A14:
|.(|[x,r]| - p).| - (|.(p - |[x,r]|).| - r) < |.(|[x,r]| - q).|
by XREAL_1:19;
|.(p - |[x,r]|).| = |.(|[x,r]| - p).|
by TOPRNS_1:27;
then
|.(q - |[x,r]|).| > r
by A14, TOPRNS_1:27;
hence
not
q in Ball (
|[x,r]|,
r)
by TOPREAL9:7;
q `2 <> 0
(
q `2 = 0 implies (
q in y=0-line &
Ball (
|[(p `1),r1]|,
r1)
misses y=0-line ) )
by A6, Th21;
hence
q `2 <> 0
by A8, XBOOLE_0:3;
verum end;
z in y>=0-plane
by Lm1;
then
q `2 >= 0
by A6, Th18;
then
(+ (x,r)) . z = 1
by A7, A3, A4, A6, Def5, ZFMISC_1:136;
then
(+ (x,r)) . z in {1}
by TARSKI:def 1;
hence
u in (+ (x,r)) " {1}
by FUNCT_2:38; verum