let p1 be Point of (TOP-REAL 2); :: thesis: for a, b, r being real number st p1 in circle a,b,r & r > 0 holds
ex p2 being Point of (TOP-REAL 2) st
( p1 <> p2 & p2 in circle a,b,r & |[a,b]| in LSeg p1,p2 )
let a, b, r be real number ; :: thesis: ( p1 in circle a,b,r & r > 0 implies ex p2 being Point of (TOP-REAL 2) st
( p1 <> p2 & p2 in circle a,b,r & |[a,b]| in LSeg p1,p2 ) )
set pc = |[a,b]|;
set p2 = (2 * |[a,b]|) - p1;
assume A1:
p1 in circle a,b,r
; :: thesis: ( not r > 0 or ex p2 being Point of (TOP-REAL 2) st
( p1 <> p2 & p2 in circle a,b,r & |[a,b]| in LSeg p1,p2 ) )
then A2:
|.(p1 - |[a,b]|).| = r
by TOPREAL9:43;
assume A3:
r > 0
; :: thesis: ex p2 being Point of (TOP-REAL 2) st
( p1 <> p2 & p2 in circle a,b,r & |[a,b]| in LSeg p1,p2 )
take
(2 * |[a,b]|) - p1
; :: thesis: ( p1 <> (2 * |[a,b]|) - p1 & (2 * |[a,b]|) - p1 in circle a,b,r & |[a,b]| in LSeg p1,((2 * |[a,b]|) - p1) )
thus
p1 <> (2 * |[a,b]|) - p1
:: thesis: ( (2 * |[a,b]|) - p1 in circle a,b,r & |[a,b]| in LSeg p1,((2 * |[a,b]|) - p1) )proof
assume
p1 = (2 * |[a,b]|) - p1
;
:: thesis: contradiction
then
(1 * p1) + p1 = ((2 * |[a,b]|) - p1) + p1
by EUCLID:33;
then
(1 * p1) + (1 * p1) = ((2 * |[a,b]|) - p1) + p1
by EUCLID:33;
then
(1 + 1) * p1 = ((2 * |[a,b]|) - p1) + p1
by EUCLID:37;
then
2
* p1 = (2 * |[a,b]|) - (p1 - p1)
by EUCLID:51;
then
2
* p1 = (2 * |[a,b]|) - (0. (TOP-REAL 2))
by EUCLID:46;
then
2
* p1 = (2 * |[a,b]|) + (0. (TOP-REAL 2))
by RLVECT_1:25;
then
2
* p1 = 2
* |[a,b]|
by EUCLID:31;
then
p1 = |[a,b]|
by EUCLID:38;
then
|.(|[a,b]| - |[a,b]|).| = r
by A1, TOPREAL9:43;
hence
contradiction
by A3, Lm1;
:: thesis: verum
end;
|.(((2 * |[a,b]|) - p1) - |[a,b]|).| =
|.(((2 * |[a,b]|) - p1) - |[a,b]|).|
.=
|.(((2 * |[a,b]|) + (- p1)) - |[a,b]|).|
.=
|.(((2 * |[a,b]|) + (- |[a,b]|)) + (- p1)).|
by EUCLID:30
.=
|.(((2 * |[a,b]|) + ((- 1) * |[a,b]|)) + (- p1)).|
by EUCLID:43
.=
|.(((2 + (- 1)) * |[a,b]|) + (- p1)).|
by EUCLID:37
.=
|.(|[a,b]| - p1).|
by EUCLID:33
.=
r
by A2, Lm2
;
hence
(2 * |[a,b]|) - p1 in circle a,b,r
by TOPREAL9:43; :: thesis: |[a,b]| in LSeg p1,((2 * |[a,b]|) - p1)
((1 - (1 / 2)) * p1) + ((1 / 2) * ((2 * |[a,b]|) - p1)) =
(1 / 2) * (p1 + ((2 * |[a,b]|) - p1))
by EUCLID:36
.=
(1 / 2) * ((p1 + (- p1)) + (2 * |[a,b]|))
by EUCLID:30
.=
(1 / 2) * ((0. (TOP-REAL 2)) + (2 * |[a,b]|))
by EUCLID:40
.=
(1 / 2) * (2 * |[a,b]|)
by EUCLID:31
.=
((1 / 2) * 2) * |[a,b]|
by EUCLID:34
.=
|[a,b]|
by EUCLID:33
;
hence
|[a,b]| in LSeg p1,((2 * |[a,b]|) - p1)
; :: thesis: verum