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