let p be Point of (TOP-REAL 2); :: thesis: ( p `2 >= 0 implies for x being real number
for r being real positive number st (+ x,r) . p = 0 holds
p = |[x,0 ]| )
assume A1: p `2 >= 0 ; :: thesis: for x being real number
for r being real positive number st (+ x,r) . p = 0 holds
p = |[x,0 ]|
let x be real number ; :: thesis: for r being real positive number st (+ x,r) . p = 0 holds
p = |[x,0 ]|
let r be real positive number ; :: thesis: ( (+ x,r) . p = 0 implies p = |[x,0 ]| )
assume A2: (+ x,r) . p = 0 ; :: thesis: p = |[x,0 ]|
set p1 = p `1 ;
set p2 = p `2 ;
A3: p = |[(p `1 ),(p `2 )]| by EUCLID:57;
assume A4: p <> |[x,0 ]| ; :: thesis: contradiction
then ( p `1 <> x or p `2 <> 0 ) by EUCLID:57;
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 Th25;
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 real positive number 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 `1 ),p2]|).| ^2 ;
then 0 = |.(|[x,0 ]| - p).| by A3;
hence contradiction by A4, TOPRNS_1:29; :: thesis: verum