let p be Point of (TOP-REAL 2); for x being Real
for a, r being positive Real st a <= 1 & |.(p - |[x,(r * a)]|).| = r * a & p `2 <> 0 holds
(+ (x,r)) . p = a
set p1 = p `1 ;
set p2 = p `2 ;
let x be Real; for a, r being positive Real st a <= 1 & |.(p - |[x,(r * a)]|).| = r * a & p `2 <> 0 holds
(+ (x,r)) . p = a
let a, r be positive Real; ( a <= 1 & |.(p - |[x,(r * a)]|).| = r * a & p `2 <> 0 implies (+ (x,r)) . p = a )
assume A1:
a <= 1
; ( not |.(p - |[x,(r * a)]|).| = r * a or not p `2 <> 0 or (+ (x,r)) . p = a )
A2:
|[((p `1) - x),((p `2) - (r * a))]| `1 = (p `1) - x
by EUCLID:52;
A3:
|[((p `1) - x),((p `2) - (r * a))]| `2 = (p `2) - (r * a)
by EUCLID:52;
assume that
A4:
|.(p - |[x,(r * a)]|).| = r * a
and
A5:
p `2 <> 0
; (+ (x,r)) . p = a
A6:
p = |[(p `1),(p `2)]|
by EUCLID:53;
then
|.|[((p `1) - x),((p `2) - (r * a))]|.| ^2 = (r * a) ^2
by A4, EUCLID:62;
then A7:
(((p `1) - x) ^2) + (((p `2) - (r * a)) ^2) = (r * a) ^2
by A2, A3, JGRAPH_1:29;
then A8:
(((p `1) - x) ^2) + ((p `2) ^2) = ((2 * (p `2)) * r) * a
;
((p `1) - x) ^2 >= 0
by XREAL_1:63;
then reconsider p2 = p `2 as positive Real by A5, A8;
A9:
|[((p `1) - x),(p2 - 0)]| `1 = (p `1) - x
by EUCLID:52;
A10:
|[((p `1) - x),p2]| `2 = p2
by EUCLID:52;
per cases
( a < 1 or a = 1 )
by A1, XXREAL_0:1;
suppose
a < 1
;
(+ (x,r)) . p = athen
r * a < r
by XREAL_1:157;
then reconsider s =
r - (r * a) as
positive Real by XREAL_1:50;
|.(p - |[x,r]|).| ^2 =
|.|[((p `1) - x),(p2 - r)]|.| ^2
by A6, EUCLID:62
.=
(((p `1) - x) ^2) + ((p2 - r) ^2)
by Th9
.=
((((p `1) - x) ^2) + ((p2 - (a * r)) ^2)) + (((r - (a * r)) ^2) + ((2 * (r - (a * r))) * ((a * r) - p2)))
.=
(|.|[((p `1) - x),(p2 - (a * r))]|.| ^2) + (((r - (a * r)) ^2) + ((2 * (r - (a * r))) * ((a * r) - p2)))
by Th9
.=
((a * r) ^2) + (((((r * r) - (r * p2)) + ((r * a) * r)) - (r * p2)) - (((((a * r) * r) - ((a * r) * p2)) + ((a * r) ^2)) - ((a * r) * p2)))
by A6, A4, EUCLID:62
.=
(r ^2) - (((1 + 1) * p2) * s)
;
then
|.(p - |[x,r]|).| ^2 < r ^2
by XREAL_1:44;
then
|.(p - |[x,r]|).| < r
by SQUARE_1:15;
then
p in Ball (
|[x,r]|,
r)
by TOPREAL9:7;
then (+ (x,r)) . p =
(|.(|[x,0]| - p).| ^2) / ((2 * r) * p2)
by A6, Def5
.=
(|.(p - |[x,0]|).| ^2) / ((2 * r) * p2)
by TOPRNS_1:27
.=
(|.|[((p `1) - x),(p2 - 0)]|.| ^2) / ((2 * r) * p2)
by A6, EUCLID:62
.=
((((p `1) - x) ^2) + (p2 ^2)) / ((2 * r) * p2)
by A9, A10, JGRAPH_1:29
;
then A11:
(+ (x,r)) . p = (((2 * p2) * r) * a) / ((2 * r) * p2)
by A7;
a * (((2 * p2) * r) / ((2 * r) * p2)) = a * 1
by XCMPLX_1:60;
hence
(+ (x,r)) . p = a
by A11, XCMPLX_1:74;
verum end;