let p be Point of (TOP-REAL 2); ( p `2 >= 0 implies for x, a, b being Real
for r being positive Real st 0 <= a & b <= 1 & (+ (x,r)) . p in ].a,b.[ holds
ex r1 being positive Real st
( r1 <= p `2 & Ball (p,r1) c= (+ (x,r)) " ].a,b.[ ) )
assume A1:
p `2 >= 0
; for x, a, b being Real
for r being positive Real st 0 <= a & b <= 1 & (+ (x,r)) . p in ].a,b.[ holds
ex r1 being positive Real st
( r1 <= p `2 & Ball (p,r1) c= (+ (x,r)) " ].a,b.[ )
let x, a, b be Real; for r being positive Real st 0 <= a & b <= 1 & (+ (x,r)) . p in ].a,b.[ holds
ex r1 being positive Real st
( r1 <= p `2 & Ball (p,r1) c= (+ (x,r)) " ].a,b.[ )
let r be positive Real; ( 0 <= a & b <= 1 & (+ (x,r)) . p in ].a,b.[ implies ex r1 being positive Real st
( r1 <= p `2 & Ball (p,r1) c= (+ (x,r)) " ].a,b.[ ) )
A2:
p = |[(p `1),(p `2)]|
by EUCLID:53;
A3:
Ball (|[x,r]|,r) misses y=0-line
by Th21;
A4:
|[((p `1) - x),(p `2)]| `1 = (p `1) - x
by EUCLID:52;
assume that
A5:
0 <= a
and
A6:
b <= 1
and
A7:
(+ (x,r)) . p in ].a,b.[
; ex r1 being positive Real 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 positive Real by A3, A1, A5, A8, A7, A10, EUCLID:53, XBOOLE_0:3, XXREAL_1:4;
A12:
|[((p `1) - x),p2]| `2 = p2
by EUCLID:52;
A13:
(2 * r) * p2 > 0
;
then
|.(|[x,0]| - p).| ^2 > ((2 * r) * (p `2)) * a
by A11, A8, XREAL_1:79;
then
|.(p - |[x,0]|).| ^2 > ((2 * r) * (p `2)) * a
by TOPRNS_1:27;
then
|.|[((p `1) - x),((p `2) - 0)]|.| ^2 > ((2 * r) * (p `2)) * a
by A2, EUCLID:62;
then
(((p `1) - x) ^2) + (p2 ^2) > ((2 * r) * p2) * a
by A4, A12, JGRAPH_1:29;
then
((((p `1) - x) ^2) + (p2 ^2)) - (((2 * r) * p2) * a) > 0
by XREAL_1:50;
then
(((((p `1) - x) ^2) + (p2 ^2)) - (((2 * r) * p2) * a)) + ((r * a) ^2) > (r * a) ^2
by XREAL_1:29;
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:77;
then
|.(p - |[x,0]|).| ^2 < ((2 * r) * (p `2)) * b
by TOPRNS_1:27;
then
|.|[((p `1) - x),((p `2) - 0)]|.| ^2 < ((2 * r) * (p `2)) * b
by A2, EUCLID:62;
then
(((p `1) - x) ^2) + (p2 ^2) < ((2 * r) * p2) * b
by A4, A12, JGRAPH_1:29;
then
((((p `1) - x) ^2) + (p2 ^2)) - (((2 * r) * p2) * b) < 0
by XREAL_1:49;
then
(((((p `1) - x) ^2) + (p2 ^2)) - (((2 * r) * p2) * b)) + ((r * b) ^2) < (r * b) ^2
by XREAL_1:30;
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:52;
A17:
|[((p `1) - x),(p2 - (r * a))]| `2 = p2 - (r * a)
by EUCLID:52;
|[((p `1) - x),(p2 - (r * a))]| `1 = (p `1) - x
by EUCLID:52;
then
|.|[((p `1) - x),(p2 - (r * a))]|.| ^2 > (r * a) ^2
by A14, A17, JGRAPH_1:29;
then
|.(p - |[x,(r * a)]|).| ^2 > (r * a) ^2
by A2, EUCLID:62;
then A18:
|.(p - |[x,(r * a)]|).| > r * a
by SQUARE_1:48;
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:27;
|[((p `1) - x),(p2 - (r * b))]| `1 = (p `1) - x
by EUCLID:52;
then
|.|[((p `1) - x),(p2 - (r * b))]|.| ^2 < (r * b) ^2
by A15, A16, JGRAPH_1:29;
then A21:
|.(p - |[x,(r * b)]|).| ^2 < (r * b) ^2
by A2, EUCLID:62;
r * b9 >= 0
;
then
|.(p - |[x,(r * b)]|).| < r * b
by A21, SQUARE_1:48;
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:50, XXREAL_0:15;
then reconsider r1 = min (((r * b) - |.(p - |[x,(r * b)]|).|),(|.(p - |[x,(r * a)]|).| - (r * a))) as positive Real ;
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:6;
|.(p - |[(p `1),0]|).| =
|.|[((p `1) - (p `1)),(p2 - 0)]|.|
by A2, EUCLID:62
.=
|.p2.|
by TOPREAL6:23
.=
p2
by ABSVALUE:def 1
;
then A23:
|.(|[x,(r * b)]| - |[(p `1),0]|).| <= |.(|[x,(r * b)]| - p).| + p2
by TOPRNS_1:34;
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:8;
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:27;
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 Th21;
verum
end;
then A25:
Ball (p,r1) c= y>=0-plane
by A2, Th20;
let u be object ; 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:8;
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:34;
then
|.(q - |[x,(r * b)]|).| < r * b
by A28, XXREAL_0:2;
then A29:
(+ (x,r)) . q < b
by A6, Th63;
A30:
|.(p - |[x,(r * a)]|).| <= |.(p - q).| + |.(q - |[x,(r * a)]|).|
by TOPRNS_1:34;
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:12;
|.(p - q).| = |.(q - p).|
by TOPRNS_1:27;
then
|.(q - |[x,(r * a)]|).| >= |.(p - |[x,(r * a)]|).| - |.(q - p).|
by A30, XREAL_1:20;
then A33:
|.(q - |[x,(r * a)]|).| > r * a
by A32, XXREAL_0:2;
q = |[(q `1),(q `2)]|
by EUCLID:53;
then
q `2 >= 0
by A25, A26, Th18;
then
(+ (x,r)) . q > a
by A33, A5, A31, Th64;
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:38; verum