let p be Point of (TOP-REAL 2); ( p `2 >= 0 implies for x, a, b being real number
for r being real positive number st 0 <= a & b <= 1 & (+ x,r) . p in ].a,b.[ holds
ex r1 being real positive number st
( r1 <= p `2 & Ball p,r1 c= (+ x,r) " ].a,b.[ ) )
assume A1:
p `2 >= 0
; for x, a, b being real number
for r being real positive number st 0 <= a & b <= 1 & (+ x,r) . p in ].a,b.[ holds
ex r1 being real positive number st
( r1 <= p `2 & Ball p,r1 c= (+ x,r) " ].a,b.[ )
let x, a, b be real number ; for r being real positive number st 0 <= a & b <= 1 & (+ x,r) . p in ].a,b.[ holds
ex r1 being real positive number st
( r1 <= p `2 & Ball p,r1 c= (+ x,r) " ].a,b.[ )
let r be real positive number ; ( 0 <= a & b <= 1 & (+ x,r) . p in ].a,b.[ implies ex r1 being real positive number st
( r1 <= p `2 & Ball p,r1 c= (+ x,r) " ].a,b.[ ) )
A2:
p = |[(p `1 ),(p `2 )]|
by EUCLID:57;
A3:
Ball |[x,r]|,r misses y=0-line
by Th25;
A4:
|[((p `1 ) - x),(p `2 )]| `1 = (p `1 ) - x
by EUCLID:56;
assume that
A5:
0 <= a
and
A6:
b <= 1
and
A7:
(+ x,r) . p in ].a,b.[
; ex r1 being real positive number st
( r1 <= p `2 & Ball p,r1 c= (+ x,r) " ].a,b.[ )
A8:
(+ x,r) . p > a
by A7, XXREAL_1:4;
A9:
(+ x,r) . p < b
by A7, XXREAL_1:4;
then A10:
( p in Ball |[x,r]|,r or ( p `1 = x & p `2 = 0 & p <> |[x,0 ]| ) )
by A8, A1, A2, A5, A6, Def5;
then A11:
(+ x,r) . p = (|.(|[x,0 ]| - p).| ^2 ) / ((2 * r) * (p `2 ))
by A1, A2, Def5;
( p `2 = 0 implies p in y=0-line )
by A2;
then reconsider p2 = p `2 , b9 = b as real positive number by A3, A1, A5, A8, A7, A10, EUCLID:57, XBOOLE_0:3, XXREAL_1:4;
A12:
|[((p `1 ) - x),p2]| `2 = p2
by EUCLID:56;
A13:
(2 * r) * p2 > 0
;
then
|.(|[x,0 ]| - p).| ^2 > ((2 * r) * (p `2 )) * a
by A11, A8, XREAL_1:81;
then
|.(p - |[x,0 ]|).| ^2 > ((2 * r) * (p `2 )) * a
by TOPRNS_1:28;
then
|.|[((p `1 ) - x),((p `2 ) - 0 )]|.| ^2 > ((2 * r) * (p `2 )) * a
by A2, EUCLID:66;
then
(((p `1 ) - x) ^2 ) + (p2 ^2 ) > ((2 * r) * p2) * a
by A4, A12, JGRAPH_1:46;
then
((((p `1 ) - x) ^2 ) + (p2 ^2 )) - (((2 * r) * p2) * a) > 0
by XREAL_1:52;
then
(((((p `1 ) - x) ^2 ) + (p2 ^2 )) - (((2 * r) * p2) * a)) + ((r * a) ^2 ) > (r * a) ^2
by XREAL_1:31;
then A14:
(((p `1 ) - x) ^2 ) + ((p2 - (r * a)) ^2 ) > (r * a) ^2
;
|.(|[x,0 ]| - p).| ^2 < ((2 * r) * (p `2 )) * b
by A13, A11, A9, XREAL_1:79;
then
|.(p - |[x,0 ]|).| ^2 < ((2 * r) * (p `2 )) * b
by TOPRNS_1:28;
then
|.|[((p `1 ) - x),((p `2 ) - 0 )]|.| ^2 < ((2 * r) * (p `2 )) * b
by A2, EUCLID:66;
then
(((p `1 ) - x) ^2 ) + (p2 ^2 ) < ((2 * r) * p2) * b
by A4, A12, JGRAPH_1:46;
then
((((p `1 ) - x) ^2 ) + (p2 ^2 )) - (((2 * r) * p2) * b) < 0
by XREAL_1:51;
then
(((((p `1 ) - x) ^2 ) + (p2 ^2 )) - (((2 * r) * p2) * b)) + ((r * b) ^2 ) < (r * b) ^2
by XREAL_1:32;
then A15:
(((p `1 ) - x) ^2 ) + ((p2 - (r * b)) ^2 ) < (r * b) ^2
;
A16:
|[((p `1 ) - x),(p2 - (r * b))]| `2 = p2 - (r * b)
by EUCLID:56;
A17:
|[((p `1 ) - x),(p2 - (r * a))]| `2 = p2 - (r * a)
by EUCLID:56;
|[((p `1 ) - x),(p2 - (r * a))]| `1 = (p `1 ) - x
by EUCLID:56;
then
|.|[((p `1 ) - x),(p2 - (r * a))]|.| ^2 > (r * a) ^2
by A14, A17, JGRAPH_1:46;
then
|.(p - |[x,(r * a)]|).| ^2 > (r * a) ^2
by A2, EUCLID:66;
then A18:
|.(p - |[x,(r * a)]|).| > r * a
by SQUARE_1:118;
A19:
((r * b) - |.(p - |[x,(r * b)]|).|) + |.(p - |[x,(r * b)]|).| = r * b
;
set r1 = min ((r * b) - |.(p - |[x,(r * b)]|).|),(|.(p - |[x,(r * a)]|).| - (r * a));
A20:
|.(p - |[x,(r * b)]|).| = |.(|[x,(r * b)]| - p).|
by TOPRNS_1:28;
|[((p `1 ) - x),(p2 - (r * b))]| `1 = (p `1 ) - x
by EUCLID:56;
then
|.|[((p `1 ) - x),(p2 - (r * b))]|.| ^2 < (r * b) ^2
by A15, A16, JGRAPH_1:46;
then A21:
|.(p - |[x,(r * b)]|).| ^2 < (r * b) ^2
by A2, EUCLID:66;
r * b9 >= 0
;
then
|.(p - |[x,(r * b)]|).| < r * b
by A21, SQUARE_1:118;
then
( ( (r * b) - |.(p - |[x,(r * b)]|).| > 0 & min ((r * b) - |.(p - |[x,(r * b)]|).|),(|.(p - |[x,(r * a)]|).| - (r * a)) = (r * b) - |.(p - |[x,(r * b)]|).| ) or ( |.(p - |[x,(r * a)]|).| - (r * a) > 0 & min ((r * b) - |.(p - |[x,(r * b)]|).|),(|.(p - |[x,(r * a)]|).| - (r * a)) = |.(p - |[x,(r * a)]|).| - (r * a) ) )
by A18, XREAL_1:52, XXREAL_0:15;
then reconsider r1 = min ((r * b) - |.(p - |[x,(r * b)]|).|),(|.(p - |[x,(r * a)]|).| - (r * a)) as real positive number ;
take
r1
; ( r1 <= p `2 & Ball p,r1 c= (+ x,r) " ].a,b.[ )
r1 <= (r * b) - |.(p - |[x,(r * b)]|).|
by XXREAL_0:17;
then A22:
|.(|[x,(r * b)]| - p).| + r1 <= r * b
by A20, A19, XREAL_1:8;
|.(p - |[(p `1 ),0 ]|).| =
|.|[((p `1 ) - (p `1 )),(p2 - 0 )]|.|
by A2, EUCLID:66
.=
abs p2
by TOPREAL6:31
.=
p2
by ABSVALUE:def 1
;
then A23:
|.(|[x,(r * b)]| - |[(p `1 ),0 ]|).| <= |.(|[x,(r * b)]| - p).| + p2
by TOPRNS_1:35;
hereby Ball p,r1 c= (+ x,r) " ].a,b.[
assume
r1 > p `2
;
contradictionthen
|.(|[x,(r * b)]| - p).| + p2 < |.(|[x,(r * b)]| - p).| + r1
by XREAL_1:10;
then
|.(|[x,(r * b)]| - |[(p `1 ),0 ]|).| < |.(|[x,(r * b)]| - p).| + r1
by A23, XXREAL_0:2;
then
|.(|[x,(r * b)]| - |[(p `1 ),0 ]|).| < r * b
by A22, XXREAL_0:2;
then
|.(|[(p `1 ),0 ]| - |[x,(r * b)]|).| < r * b
by TOPRNS_1:28;
then A24:
|[(p `1 ),0 ]| in Ball |[x,(r * b)]|,
(r * b)
by TOPREAL9:7;
|[(p `1 ),0 ]| in y=0-line
;
then
Ball |[x,(r * b)]|,
(r * b9) meets y=0-line
by A24, XBOOLE_0:3;
hence
contradiction
by Th25;
verum
end;
then A25:
Ball p,r1 c= y>=0-plane
by A2, Th24;
let u be set ; TARSKI:def 3 ( not u in Ball p,r1 or u in (+ x,r) " ].a,b.[ )
assume A26:
u in Ball p,r1
; u in (+ x,r) " ].a,b.[
then reconsider q = u as Point of (TOP-REAL 2) ;
A27:
|.(q - p).| < r1
by A26, TOPREAL9:7;
then
|.(q - p).| + |.(p - |[x,(r * b)]|).| < r1 + |.(p - |[x,(r * b)]|).|
by XREAL_1:10;
then A28:
|.(q - p).| + |.(p - |[x,(r * b)]|).| < r * b
by A20, A22, XXREAL_0:2;
|.(q - |[x,(r * b)]|).| <= |.(q - p).| + |.(p - |[x,(r * b)]|).|
by TOPRNS_1:35;
then
|.(q - |[x,(r * b)]|).| < r * b
by A28, XXREAL_0:2;
then A29:
(+ x,r) . q < b
by A6, Th67;
A30:
|.(p - |[x,(r * a)]|).| <= |.(p - q).| + |.(q - |[x,(r * a)]|).|
by TOPRNS_1:35;
a < b
by A8, A9, XXREAL_0:2;
then A31:
a < 1
by A6, XXREAL_0:2;
|.(p - |[x,(r * a)]|).| - (r * a) >= r1
by XXREAL_0:17;
then
|.(p - |[x,(r * a)]|).| - (r * a) > |.(q - p).|
by A27, XXREAL_0:2;
then A32:
|.(p - |[x,(r * a)]|).| - |.(q - p).| > r * a
by XREAL_1:14;
|.(p - q).| = |.(q - p).|
by TOPRNS_1:28;
then
|.(q - |[x,(r * a)]|).| >= |.(p - |[x,(r * a)]|).| - |.(q - p).|
by A30, XREAL_1:22;
then A33:
|.(q - |[x,(r * a)]|).| > r * a
by A32, XXREAL_0:2;
q = |[(q `1 ),(q `2 )]|
by EUCLID:57;
then
q `2 >= 0
by A25, A26, Th22;
then
(+ x,r) . q > a
by A33, A5, A31, Th68;
then
(+ x,r) . q in ].a,b.[
by A29, XXREAL_1:4;
hence
u in (+ x,r) " ].a,b.[
by A25, A26, Lm1, FUNCT_2:46; verum