let p be Point of (TOP-REAL 2); for x, a being real number
for r being real positive number st a <= 1 & |.(p - |[x,(r * a)]|).| < r * a holds
(+ x,r) . p < a
set p1 = p `1 ;
set p2 = p `2 ;
let x, a be real number ; for r being real positive number st a <= 1 & |.(p - |[x,(r * a)]|).| < r * a holds
(+ x,r) . p < a
let r be real positive number ; ( a <= 1 & |.(p - |[x,(r * a)]|).| < r * a implies (+ x,r) . p < a )
assume A1:
a <= 1
; ( not |.(p - |[x,(r * a)]|).| < r * a or (+ x,r) . p < a )
A2:
|[((p `1 ) - x),((p `2 ) - (r * a))]| `2 = (p `2 ) - (r * a)
by EUCLID:56;
A3:
p = |[(p `1 ),(p `2 )]|
by EUCLID:57;
then A4:
( p `2 = 0 implies p in y=0-line )
;
set r1 = r * a;
set r2 = r * 1;
A5:
|[((p `1 ) - x),((p `2 ) - (r * a))]| `1 = (p `1 ) - x
by EUCLID:56;
assume A6:
|.(p - |[x,(r * a)]|).| < r * a
; (+ x,r) . p < a
then reconsider r1 = r * a as real positive number ;
A7:
p in Ball |[x,r1]|,r1
by A6, TOPREAL9:7;
|.(p - |[x,(r * a)]|).| ^2 < (r * a) ^2
by A6, SQUARE_1:78;
then
|.|[((p `1 ) - x),((p `2 ) - (r * a))]|.| ^2 < (r * a) ^2
by A3, EUCLID:66;
then
(((p `1 ) - x) ^2 ) + (((p `2 ) - (r * a)) ^2 ) < (r * a) ^2
by A5, A2, JGRAPH_1:46;
then
(((((p `1 ) - x) ^2 ) + ((p `2 ) ^2 )) - ((2 * (p `2 )) * (r * a))) + ((r * a) ^2 ) < (r * a) ^2
;
then
((((p `1 ) - x) ^2 ) + ((p `2 ) ^2 )) - (((2 * (p `2 )) * r) * a) < 0
by XREAL_1:33;
then A8:
(((p `1 ) - x) ^2 ) + ((p `2 ) ^2 ) < ((2 * (p `2 )) * r) * a
by XREAL_1:50;
A9:
Ball |[x,r1]|,r1 misses y=0-line
by Th25;
Ball |[x,r1]|,r1 c= y>=0-plane
by Th24;
then reconsider p2 = p `2 as real positive number by A3, A7, Th22, A9, A4, XBOOLE_0:3;
A10:
|[((p `1 ) - x),(p2 - 0 )]| `1 = (p `1 ) - x
by EUCLID:56;
A11:
|[((p `1 ) - x),p2]| `2 = p2
by EUCLID:56;
Ball |[x,r1]|,r1 c= Ball |[x,(r * 1)]|,(r * 1)
by A1, Th27, XREAL_1:66;
then (+ x,r) . p =
(|.(|[x,0 ]| - p).| ^2 ) / ((2 * r) * p2)
by A3, A7, Def5
.=
(|.(p - |[x,0 ]|).| ^2 ) / ((2 * r) * p2)
by TOPRNS_1:28
.=
(|.|[((p `1 ) - x),(p2 - 0 )]|.| ^2 ) / ((2 * r) * p2)
by A3, EUCLID:66
.=
((((p `1 ) - x) ^2 ) + (p2 ^2 )) / ((2 * r) * p2)
by A10, A11, JGRAPH_1:46
;
then A12:
(+ x,r) . p < (((2 * p2) * r) * a) / ((2 * r) * p2)
by A8, XREAL_1:76;
a * (((2 * p2) * r) / ((2 * r) * p2)) = a * 1
by XCMPLX_1:60;
hence
(+ x,r) . p < a
by A12, XCMPLX_1:75; verum