let x, y be real number ; :: thesis: for r being real positive number st x <> y holds
(+ x,r) . |[y,0 ]| = 1
let r be real positive number ; :: thesis: ( x <> y implies (+ x,r) . |[y,0 ]| = 1 )
A1: ( |.(x - y).| = x - y or |.(x - y).| = - (x - y) ) by ABSVALUE:1;
A2: |[(x - y),r]| `2 = r by EUCLID:56;
|[(x - y),r]| `1 = x - y by EUCLID:56;
then A3: |.|[(x - y),r]|.| ^2 = (r ^2 ) + ((x - y) ^2 ) by A2, JGRAPH_1:46;
assume A4: x <> y ; :: thesis: (+ x,r) . |[y,0 ]| = 1
then x - y <> 0 ;
then A5: |.(x - y).| > 0 by COMPLEX1:133;
then |.(x - y).| ^2 <> 0 ;
then |.|[(x - y),r]|.| ^2 > r ^2 by A1, A5, A3, XREAL_1:31;
then |.|[(x - y),(r - 0 )]|.| > r by SQUARE_1:77;
then |.(|[x,r]| - |[y,0 ]|).| > r by EUCLID:66;
then |.(|[y,0 ]| - |[x,r]|).| > r by TOPRNS_1:28;
then not |[y,0 ]| in Ball |[x,r]|,r by TOPREAL9:7;
hence (+ x,r) . |[y,0 ]| = 1 by A4, Def5; :: thesis: verum