let p be Point of (TOP-REAL 2); for x, a being Real
for r being positive Real 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; for r being positive Real st a <= 1 & |.(p - |[x,(r * a)]|).| < r * a holds
(+ (x,r)) . p < a
let r be positive Real; ( 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:52;
A3:
p = |[(p `1),(p `2)]|
by EUCLID:53;
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:52;
assume A6:
|.(p - |[x,(r * a)]|).| < r * a
; (+ (x,r)) . p < a
then reconsider r1 = r * a as positive Real ;
A7:
p in Ball (|[x,r1]|,r1)
by A6, TOPREAL9:7;
|.(p - |[x,(r * a)]|).| ^2 < (r * a) ^2
by A6, SQUARE_1:16;
then
|.|[((p `1) - x),((p `2) - (r * a))]|.| ^2 < (r * a) ^2
by A3, EUCLID:62;
then
(((p `1) - x) ^2) + (((p `2) - (r * a)) ^2) < (r * a) ^2
by A5, A2, JGRAPH_1:29;
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:31;
then A8:
(((p `1) - x) ^2) + ((p `2) ^2) < ((2 * (p `2)) * r) * a
by XREAL_1:48;
A9:
Ball (|[x,r1]|,r1) misses y=0-line
by Th21;
Ball (|[x,r1]|,r1) c= y>=0-plane
by Th20;
then reconsider p2 = p `2 as positive Real by A3, A7, Th18, A9, A4, XBOOLE_0:3;
A10:
|[((p `1) - x),(p2 - 0)]| `1 = (p `1) - x
by EUCLID:52;
A11:
|[((p `1) - x),p2]| `2 = p2
by EUCLID:52;
Ball (|[x,r1]|,r1) c= Ball (|[x,(r * 1)]|,(r * 1))
by A1, Th23, XREAL_1:64;
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:27
.=
(|.|[((p `1) - x),(p2 - 0)]|.| ^2) / ((2 * r) * p2)
by A3, EUCLID:62
.=
((((p `1) - x) ^2) + (p2 ^2)) / ((2 * r) * p2)
by A10, A11, JGRAPH_1:29
;
then A12:
(+ (x,r)) . p < (((2 * p2) * r) * a) / ((2 * r) * p2)
by A8, XREAL_1:74;
a * (((2 * p2) * r) / ((2 * r) * p2)) = a * 1
by XCMPLX_1:60;
hence
(+ (x,r)) . p < a
by A12, XCMPLX_1:74; verum