let p be Point of (TOP-REAL 2); ( p `2 >= 0 implies for x, a being Real
for r being positive Real st 0 <= a & a < 1 & |.(p - |[x,(r * a)]|).| > r * a holds
(+ (x,r)) . p > a )
assume A1:
p `2 >= 0
; for x, a being Real
for r being positive Real st 0 <= a & a < 1 & |.(p - |[x,(r * a)]|).| > r * a holds
(+ (x,r)) . p > a
set p1 = p `1 ;
set p2 = p `2 ;
reconsider p2 = p `2 as non negative Real by A1;
let x, a be Real; for r being positive Real st 0 <= a & a < 1 & |.(p - |[x,(r * a)]|).| > r * a holds
(+ (x,r)) . p > a
let r be positive Real; ( 0 <= a & a < 1 & |.(p - |[x,(r * a)]|).| > r * a implies (+ (x,r)) . p > a )
assume that
A2:
0 <= a
and
A3:
a < 1
; ( not |.(p - |[x,(r * a)]|).| > r * a or (+ (x,r)) . p > a )
reconsider a9 = a as non negative Real by A2;
reconsider ra = r * a as Real ;
assume A4:
|.(p - |[x,(r * a)]|).| > r * a
; (+ (x,r)) . p > a
|.(|[x,0]| - |[x,(r * a)]|).| =
|.(|[x,(r * a)]| - |[x,0]|).|
by TOPRNS_1:27
.=
|.|[(x - x),(ra - 0)]|.|
by EUCLID:62
.=
|.ra.|
by TOPREAL6:23
.=
r * a9
by ABSVALUE:def 1
;
then A5:
( p `1 <> x or p2 <> 0 )
by A4, EUCLID:53;
A6:
p = |[(p `1),(p `2)]|
by EUCLID:53;
then reconsider z = p as Element of Niemytzki-plane by A1, Lm1, Th18;
A7:
(+ (x,r)) . z in the carrier of I[01]
;
per cases
( a = 0 or (+ (x,r)) . p = 1 or ( a > 0 & (+ (x,r)) . z <> 1 ) )
by A2;
suppose A9:
(
a > 0 &
(+ (x,r)) . z <> 1 )
;
(+ (x,r)) . p > aA10:
|[((p `1) - x),(p2 - 0)]| `1 = (p `1) - x
by EUCLID:52;
A11:
|[((p `1) - x),p2]| `2 = p2
by EUCLID:52;
not
p2 is
negative
;
then A12:
p in Ball (
|[x,r]|,
r)
by A6, A5, A9, Def5;
then A13:
(+ (x,r)) . p =
(|.(|[x,0]| - p).| ^2) / ((2 * r) * p2)
by A6, Def5
.=
(|.(p - |[x,0]|).| ^2) / ((2 * r) * p2)
by TOPRNS_1:27
.=
(|.|[((p `1) - x),(p2 - 0)]|.| ^2) / ((2 * r) * p2)
by A6, EUCLID:62
.=
((((p `1) - x) ^2) + (p2 ^2)) / ((2 * r) * p2)
by A10, A11, JGRAPH_1:29
;
|.(p - |[x,(r * a)]|).| ^2 > (r * a) ^2
by A2, A4, SQUARE_1:16;
then A14:
|.|[((p `1) - x),(p2 - (r * a))]|.| ^2 > (r * a) ^2
by A6, EUCLID:62;
A15:
|[((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) ^2) + ((p2 - (r * a)) ^2) > (r * a) ^2
by A14, A15, JGRAPH_1:29;
then
(((((p `1) - x) ^2) + (p2 ^2)) - ((2 * p2) * (r * a))) + ((r * a) ^2) > (r * a) ^2
;
then
((((p `1) - x) ^2) + (p2 ^2)) - (((2 * p2) * r) * a) > 0
by XREAL_1:32;
then A16:
(((p `1) - x) ^2) + (p2 ^2) > ((2 * p2) * r) * a
by XREAL_1:47;
A17:
(
p2 = 0 implies
p in y=0-line )
by A6;
Ball (
|[x,r]|,
r)
misses y=0-line
by Th21;
then reconsider p2 =
p2 as
positive Real by A12, A17, XBOOLE_0:3;
A18:
a * (((2 * p2) * r) / ((2 * r) * p2)) = a * 1
by XCMPLX_1:60;
(+ (x,r)) . p > (((2 * p2) * r) * a) / ((2 * r) * p2)
by A13, A16, XREAL_1:74;
hence
(+ (x,r)) . p > a
by A18, XCMPLX_1:74;
verum end;