let p1, p2 be Point of (TOP-REAL 2); for a, b, r being Real st p1 in inside_of_circle (a,b,r) & p2 in outside_of_circle (a,b,r) holds
ex p being Point of (TOP-REAL 2) st p in (LSeg (p1,p2)) /\ (circle (a,b,r))
let a, b, r be Real; ( p1 in inside_of_circle (a,b,r) & p2 in outside_of_circle (a,b,r) implies ex p being Point of (TOP-REAL 2) st p in (LSeg (p1,p2)) /\ (circle (a,b,r)) )
set pc1 = p1 - |[a,b]|;
set pc2 = p2 - |[a,b]|;
reconsider r9 = r as Real ;
assume
p1 in inside_of_circle (a,b,r)
; ( not p2 in outside_of_circle (a,b,r) or ex p being Point of (TOP-REAL 2) st p in (LSeg (p1,p2)) /\ (circle (a,b,r)) )
then
p1 in { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| < r }
by JGRAPH_6:def 6;
then A1:
ex p19 being Point of (TOP-REAL 2) st
( p1 = p19 & |.(p19 - |[a,b]|).| < r )
;
assume
p2 in outside_of_circle (a,b,r)
; ex p being Point of (TOP-REAL 2) st p in (LSeg (p1,p2)) /\ (circle (a,b,r))
then
p2 in { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| > r }
by JGRAPH_6:def 8;
then A2:
ex p29 being Point of (TOP-REAL 2) st
( p2 = p29 & |.(p29 - |[a,b]|).| > r )
;
then consider f being Function of I[01],((TOP-REAL 2) | (LSeg ((p1 - |[a,b]|),(p2 - |[a,b]|)))) such that
A3:
for x being Real st x in [.0,1.] holds
f . x = ((1 - x) * (p1 - |[a,b]|)) + (x * (p2 - |[a,b]|))
and
A4:
f is being_homeomorphism
and
A5:
f . 0 = p1 - |[a,b]|
and
A6:
f . 1 = p2 - |[a,b]|
by A1, JORDAN5A:3;
reconsider g = f as Function of I[01],(TOP-REAL 2) by JORDAN6:3;
0 in the carrier of I[01]
by BORSUK_1:40, XXREAL_1:1;
then
0 in dom g
by FUNCT_2:def 1;
then A7:
g /. 0 = p1 - |[a,b]|
by A5, PARTFUN1:def 6;
1 in the carrier of I[01]
by BORSUK_1:40, XXREAL_1:1;
then
1 in dom g
by FUNCT_2:def 1;
then A8:
g /. 1 = p2 - |[a,b]|
by A6, PARTFUN1:def 6;
f is continuous
by A4, TOPS_2:def 5;
then consider s being Point of I[01] such that
A9:
|.(g /. s).| = r9
by A1, A2, A7, A8, JORDAN2C:86, JORDAN6:3;
A10:
s in the carrier of I[01]
;
s in [.0,1.]
by BORSUK_1:40;
then
s in { s9 where s9 is Element of ExtREAL : ( 0 <= s9 & s9 <= 1 ) }
by XXREAL_1:def 1;
then A11:
ex s9 being Element of ExtREAL st
( s = s9 & 0 <= s9 & s9 <= 1 )
;
reconsider s = s as Real ;
set p9 = f . s;
s in dom g
by A10, FUNCT_2:def 1;
then
( rng g c= the carrier of (TOP-REAL 2) & g . s in rng g )
by FUNCT_1:3, RELAT_1:def 19;
then reconsider p9 = f . s as Point of (TOP-REAL 2) ;
set p = p9 + |[a,b]|;
take
p9 + |[a,b]|
; p9 + |[a,b]| in (LSeg (p1,p2)) /\ (circle (a,b,r))
f . s =
((1 - s) * (p1 - |[a,b]|)) + (s * (p2 - |[a,b]|))
by A3, BORSUK_1:40
.=
(((1 - s) * p1) - ((1 - s) * |[a,b]|)) + (s * (p2 - |[a,b]|))
by RLVECT_1:34
.=
(((1 - s) * p1) - ((1 - s) * |[a,b]|)) + ((s * p2) - (s * |[a,b]|))
by RLVECT_1:34
.=
(((1 - s) * p1) + ((- (1 - s)) * |[a,b]|)) + ((s * p2) - (s * |[a,b]|))
by RLVECT_1:79
.=
(((1 - s) * p1) + (((- 1) + s) * |[a,b]|)) + ((s * p2) - (s * |[a,b]|))
.=
(((1 - s) * p1) + (((- 1) * |[a,b]|) + (s * |[a,b]|))) + ((s * p2) - (s * |[a,b]|))
by RLVECT_1:def 6
.=
((((1 - s) * p1) + ((- 1) * |[a,b]|)) + (s * |[a,b]|)) + ((s * p2) + (- (s * |[a,b]|)))
by RLVECT_1:def 3
.=
(((1 - s) * p1) + ((- 1) * |[a,b]|)) + ((s * |[a,b]|) + ((s * p2) + (- (s * |[a,b]|))))
by RLVECT_1:def 3
.=
(((1 - s) * p1) + ((- 1) * |[a,b]|)) + (((s * |[a,b]|) + (- (s * |[a,b]|))) + (s * p2))
by RLVECT_1:def 3
.=
(((1 - s) * p1) + ((- 1) * |[a,b]|)) + (((s * |[a,b]|) + ((- s) * |[a,b]|)) + (s * p2))
by RLVECT_1:79
.=
(((1 - s) * p1) + ((- 1) * |[a,b]|)) + (((s + (- s)) * |[a,b]|) + (s * p2))
by RLVECT_1:def 6
.=
(((1 - s) * p1) + ((- 1) * |[a,b]|)) + ((0. (TOP-REAL 2)) + (s * p2))
by RLVECT_1:10
.=
(((1 - s) * p1) + ((- 1) * |[a,b]|)) + (s * p2)
by RLVECT_1:4
.=
(((1 - s) * p1) + (s * p2)) + ((- 1) * |[a,b]|)
by RLVECT_1:def 3
;
then A12: p9 + |[a,b]| =
((((1 - s) * p1) + (s * p2)) + ((- 1) * |[a,b]|)) + |[a,b]|
.=
((((1 - s) * p1) + (s * p2)) + (- |[a,b]|)) + |[a,b]|
.=
(((1 - s) * p1) + (s * p2)) + ((- |[a,b]|) + |[a,b]|)
by RLVECT_1:def 3
.=
(((1 - s) * p1) + (s * p2)) + (0. (TOP-REAL 2))
by RLVECT_1:5
.=
((1 - s) * p1) + (s * p2)
by RLVECT_1:4
;
r =
|.(p9 + (0. (TOP-REAL 2))).|
by A9, RLVECT_1:4
.=
|.(p9 + (|[a,b]| - |[a,b]|)).|
by RLVECT_1:5
.=
|.((p9 + |[a,b]|) + (- |[a,b]|)).|
by RLVECT_1:def 3
.=
|.((p9 + |[a,b]|) - |[a,b]|).|
;
then
p9 + |[a,b]| in { p99 where p99 is Point of (TOP-REAL 2) : |.(p99 - |[a,b]|).| = r }
;
then A13:
p9 + |[a,b]| in circle (a,b,r)
by JGRAPH_6:def 5;
((1 - s) * p1) + (s * p2) in LSeg (p1,p2)
by A11;
hence
p9 + |[a,b]| in (LSeg (p1,p2)) /\ (circle (a,b,r))
by A12, A13, XBOOLE_0:def 4; verum