let x, y be Real; for r being positive Real st x <> y holds
(+ (x,r)) . |[y,0]| = 1
let r be positive Real; ( 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:52;
|[(x - y),r]| `1 = x - y
by EUCLID:52;
then A3:
|.|[(x - y),r]|.| ^2 = (r ^2) + ((x - y) ^2)
by A2, JGRAPH_1:29;
assume A4:
x <> y
; (+ (x,r)) . |[y,0]| = 1
then
x - y <> 0
;
then A5:
|.(x - y).| > 0
by COMPLEX1:47;
then
|.(x - y).| ^2 <> 0
;
then
|.|[(x - y),r]|.| ^2 > r ^2
by A1, A5, A3, XREAL_1:29;
then
|.|[(x - y),(r - 0)]|.| > r
by SQUARE_1:15;
then
|.(|[x,r]| - |[y,0]|).| > r
by EUCLID:62;
then
|.(|[y,0]| - |[x,r]|).| > r
by TOPRNS_1:27;
then
not |[y,0]| in Ball (|[x,r]|,r)
by TOPREAL9:7;
hence
(+ (x,r)) . |[y,0]| = 1
by A4, Def5; verum