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