let p be Point of (TOP-REAL 2); :: thesis: ( p `2 >= 0 implies for x being Real
for y being non negative Real
for r being positive Real holds
( (+ (x,y,r)) . p = 0 iff p = |[x,y]| ) )
assume A1: p `2 >= 0 ; :: thesis: for x being Real
for y being non negative Real
for r being positive Real holds
( (+ (x,y,r)) . p = 0 iff p = |[x,y]| )
let x be Real; :: thesis: for y being non negative Real
for r being positive Real holds
( (+ (x,y,r)) . p = 0 iff p = |[x,y]| )
let y be non negative Real; :: thesis: for r being positive Real holds
( (+ (x,y,r)) . p = 0 iff p = |[x,y]| )
let r be positive Real; :: thesis: ( (+ (x,y,r)) . p = 0 iff p = |[x,y]| )
A2: p = |[(p `1),(p `2)]| by EUCLID:53;
hereby :: thesis: ( p = |[x,y]| implies (+ (x,y,r)) . p = 0 )
assume A3: (+ (x,y,r)) . p = 0 ; :: thesis: p = |[x,y]|
then p in Ball (|[x,y]|,r) by A1, A2, Def6;
then 0 = |.(|[x,y]| - p).| / r by A1, A2, A3, Def6;
then 0 * r = |.(|[x,y]| - p).| ;
hence p = |[x,y]| by TOPRNS_1:28; :: thesis: verum
end;
assume A4: p = |[x,y]| ; :: thesis: (+ (x,y,r)) . p = 0
then p in Ball (|[x,y]|,r) by Th13;
hence (+ (x,y,r)) . p = |.(|[x,y]| - p).| / r by A4, Def6
.= 0 / r by A4, TOPRNS_1:28
.= 0 ;
:: thesis: verum