let p1 be Point of (TOP-REAL 2); for a, b, r being Real 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; ( 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)
; ( 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
; 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
; ( 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
( (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
;
contradiction
then
(1 * p1) + p1 = ((2 * |[a,b]|) - p1) + p1
by RLVECT_1:def 8;
then
(1 * p1) + (1 * p1) = ((2 * |[a,b]|) - p1) + p1
by RLVECT_1:def 8;
then
(1 + 1) * p1 = ((2 * |[a,b]|) - p1) + p1
by RLVECT_1:def 6;
then
2
* p1 = (2 * |[a,b]|) - (p1 - p1)
by RLVECT_1:29;
then
2
* p1 = (2 * |[a,b]|) - (0. (TOP-REAL 2))
by RLVECT_1:5;
then
2
* p1 = (2 * |[a,b]|) + (0. (TOP-REAL 2))
by RLVECT_1:12;
then
2
* p1 = 2
* |[a,b]|
by RLVECT_1:4;
then
p1 = |[a,b]|
by RLVECT_1:36;
then
|.(|[a,b]| - |[a,b]|).| = r
by A1, TOPREAL9:43;
hence
contradiction
by A3, Lm1;
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 RLVECT_1:def 3
.=
|.(((2 * |[a,b]|) + ((- 1) * |[a,b]|)) + (- p1)).|
.=
|.(((2 + (- 1)) * |[a,b]|) + (- p1)).|
by RLVECT_1:def 6
.=
|.(|[a,b]| - p1).|
by RLVECT_1:def 8
.=
r
by A2, Lm2
;
hence
(2 * |[a,b]|) - p1 in circle (a,b,r)
by TOPREAL9:43; |[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 RLVECT_1:def 5
.=
(1 / 2) * ((p1 + (- p1)) + (2 * |[a,b]|))
by RLVECT_1:def 3
.=
(1 / 2) * ((0. (TOP-REAL 2)) + (2 * |[a,b]|))
by RLVECT_1:5
.=
(1 / 2) * (2 * |[a,b]|)
by RLVECT_1:4
.=
((1 / 2) * 2) * |[a,b]|
by RLVECT_1:def 7
.=
|[a,b]|
by RLVECT_1:def 8
;
hence
|[a,b]| in LSeg (p1,((2 * |[a,b]|) - p1))
; verum