let p, q be Point of (TOP-REAL 2); :: thesis: for e being Point of (Euclid 2)
for r being Real st e = q & p in Ball (e,r) holds
( (q `2) - r < p `2 & p `2 < (q `2) + r )
let e be Point of (Euclid 2); :: thesis: for r being Real st e = q & p in Ball (e,r) holds
( (q `2) - r < p `2 & p `2 < (q `2) + r )
let r be Real; :: thesis: ( e = q & p in Ball (e,r) implies ( (q `2) - r < p `2 & p `2 < (q `2) + r ) )
assume that
A1: e = q and
A2: p in Ball (e,r) ; :: thesis: ( (q `2) - r < p `2 & p `2 < (q `2) + r )
reconsider f = p as Point of (Euclid 2) by TOPREAL3:8;
A3: dist (e,f) < r by A2, METRIC_1:11;
A4: dist (e,f) = (Pitag_dist 2) . (e,f) by METRIC_1:def 1
.= sqrt ((((q `1) - (p `1)) ^2) + (((q `2) - (p `2)) ^2)) by A1, TOPREAL3:7 ;
A5: r > 0 by A2, TBSP_1:12;
assume A6: ( not (q `2) - r < p `2 or not p `2 < (q `2) + r ) ; :: thesis: contradiction
per cases ( (q `2) - r >= p `2 or p `2 >= (q `2) + r ) by A6;
suppose A7: (q `2) - r >= p `2 ; :: thesis: contradiction
((q `1) - (p `1)) ^2 >= 0 by XREAL_1:63;
then A8: (((q `1) - (p `1)) ^2) + (((q `2) - (p `2)) ^2) >= (((q `2) - (p `2)) ^2) + 0 by XREAL_1:6;
(q `2) - (p `2) >= r by A7, XREAL_1:11;
then ((q `2) - (p `2)) ^2 >= r ^2 by A5, SQUARE_1:15;
then (((q `1) - (p `1)) ^2) + (((q `2) - (p `2)) ^2) >= r ^2 by A8, XXREAL_0:2;
then sqrt ((((q `1) - (p `1)) ^2) + (((q `2) - (p `2)) ^2)) >= sqrt (r ^2) by A5, SQUARE_1:26;
hence contradiction by A3, A4, A5, SQUARE_1:22; :: thesis: verum
end;
suppose A9: p `2 >= (q `2) + r ; :: thesis: contradiction
((q `1) - (p `1)) ^2 >= 0 by XREAL_1:63;
then A10: (((q `1) - (p `1)) ^2) + (((q `2) - (p `2)) ^2) >= (((q `2) - (p `2)) ^2) + 0 by XREAL_1:6;
(p `2) - (q `2) >= r by A9, XREAL_1:19;
then (- ((q `2) - (p `2))) ^2 >= r ^2 by A5, SQUARE_1:15;
then (((q `1) - (p `1)) ^2) + (((q `2) - (p `2)) ^2) >= r ^2 by A10, XXREAL_0:2;
then sqrt ((((q `1) - (p `1)) ^2) + (((q `2) - (p `2)) ^2)) >= sqrt (r ^2) by A5, SQUARE_1:26;
hence contradiction by A3, A4, A5, SQUARE_1:22; :: thesis: verum
end;
end;