let p be Point of (TOP-REAL 2); :: thesis: ( p `2 >= 0 implies for x being Real
for r being positive Real st (+ (x,r)) . p = 0 holds
p = |[x,0]| )
assume A1: p `2 >= 0 ; :: thesis: for x being Real
for r being positive Real st (+ (x,r)) . p = 0 holds
p = |[x,0]|
set p1 = p `1 ;
set p2 = p `2 ;
let x be Real; :: thesis: for r being positive Real st (+ (x,r)) . p = 0 holds
p = |[x,0]|
let r be positive Real; :: thesis: ( (+ (x,r)) . p = 0 implies p = |[x,0]| )
assume A2: (+ (x,r)) . p = 0 ; :: thesis: p = |[x,0]|
A3: p = |[(p `1),(p `2)]| by EUCLID:53;
assume A4: p <> |[x,0]| ; :: thesis: contradiction
then ( p `1 <> x or p `2 <> 0 ) by EUCLID:53;
then A5: |[(p `1),(p `2)]| in Ball (|[x,r]|,r) by A1, A2, A3, Def5;
Ball (|[x,r]|,r) misses y=0-line by Th21;
then not |[(p `1),(p `2)]| in y=0-line by A5, XBOOLE_0:3;
then p `2 <> 0 ;
then reconsider p2 = p `2 as positive Real by A1;
0 / ((2 * r) * p2) = (|.(|[x,0]| - |[(p `1),p2]|).| ^2) / ((2 * r) * p2) by A2, A3, A5, Def5;
then 0 = |.(|[x,0]| - p).| by A3;
hence contradiction by A4, TOPRNS_1:28; :: thesis: verum