let p be Point of (TOP-REAL 2); :: thesis: ( p `2 >= 0 implies for x, a being Real
for r being positive Real st 0 < (+ (x,r)) . p & (+ (x,r)) . p < a & a <= 1 holds
p in Ball (|[x,(r * a)]|,(r * a)) )
assume A1: p `2 >= 0 ; :: thesis: for x, a being Real
for r being positive Real st 0 < (+ (x,r)) . p & (+ (x,r)) . p < a & a <= 1 holds
p in Ball (|[x,(r * a)]|,(r * a))
let x, a be Real; :: thesis: for r being positive Real st 0 < (+ (x,r)) . p & (+ (x,r)) . p < a & a <= 1 holds
p in Ball (|[x,(r * a)]|,(r * a))
A2: p = |[(p `1),(p `2)]| by EUCLID:53;
let r be positive Real; :: thesis: ( 0 < (+ (x,r)) . p & (+ (x,r)) . p < a & a <= 1 implies p in Ball (|[x,(r * a)]|,(r * a)) )
set r1 = r * a;
assume that
A3: 0 < (+ (x,r)) . p and
A4: (+ (x,r)) . p < a and
A5: a <= 1 ; :: thesis: p in Ball (|[x,(r * a)]|,(r * a))
A6: ( x <> p `1 implies p <> |[(p `1),0]| ) by A4, A5, Th61;
A7: p <> |[x,0]| by A3, Def5;
assume not p in Ball (|[x,(r * a)]|,(r * a)) ; :: thesis: contradiction
then |.(p - |[x,(r * a)]|).| >= r * a by TOPREAL9:7;
then ( |.(p - |[x,(r * a)]|).| = r * a or ( |.(p - |[x,(r * a)]|).| > r * a & ( a < 1 or a = 1 ) ) ) by A5, XXREAL_0:1;
then ( (+ (x,r)) . p = a or ( a < 1 & (+ (x,r)) . p > a ) or ( a = 1 & not p in Ball (|[x,r]|,r) ) ) by A1, A2, A3, A5, A7, A6, Th62, Th64, TOPREAL9:7;
hence contradiction by A1, A2, A4, A7, A6, Def5; :: thesis: verum