let p1, p2 be Point of (TOP-REAL 2); :: thesis:
let a, b, r be real number ; :: thesis:
assume p1 in inside_of_circle a,b,r ; :: thesis:
then p1 in { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| < r } by JGRAPH_6:def 6;
then consider p1' being Point of (TOP-REAL 2) such that
A1: ( p1 = p1' & |.(p1' - |[a,b]|).| < r ) ;
assume p2 in outside_of_circle a,b,r ; :: thesis:
then p2 in { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| > r } by JGRAPH_6:def 8;
then consider p2' being Point of (TOP-REAL 2) such that
A2: ( p2 = p2' & |.(p2' - |[a,b]|).| > r ) ;
set pc1 = p1 - |[a,b]|;
set pc2 = p2 - |[a,b]|;
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 & f . 0 = p1 - |[a,b]| & f . 1 = p2 - |[a,b]| ) by A1, A2, JORDAN5A:4;
reconsider g = f as Function of I[01] ,(TOP-REAL 2) by JORDAN6:4;
reconsider r' = r as Real by XREAL_0:def 1;
f is continuous by A4, TOPS_2:def 5;
then A5: g is continuous by JORDAN6:4;
0 in the carrier of I[01] by BORSUK_1:83, XXREAL_1:1;
then 0 in dom g by FUNCT_2:def 1;
then A6: pi g,0 = p1 - |[a,b]| by A4, PARTFUN1:def 8;
1 in the carrier of I[01] by BORSUK_1:83, XXREAL_1:1;
then 1 in dom g by FUNCT_2:def 1;
then pi g,1 = p2 - |[a,b]| by A4, PARTFUN1:def 8;
then consider s being Point of I[01] such that
A7: |.(pi g,s).| = r' by A1, A2, A5, A6, JORDAN2C:94;
A8: s in the carrier of I[01] ;
s in [.0 ,1.] by BORSUK_1:83;
then s in { s' where s' is Element of ExtREAL : ( 0 <= s' & s' <= 1 ) } by XXREAL_1:def 1;
then consider s' being Element of ExtREAL such that
A9: ( s = s' & 0 <= s' & s' <= 1 ) ;
reconsider s = s as Real by A9, XXREAL_0:45;
set p' = f . s;
A10: rng g c= the carrier of (TOP-REAL 2) by RELAT_1:def 19;
s in dom g by A8, FUNCT_2:def 1;
then g . s in rng g by FUNCT_1:12;
then reconsider p' = f . s as Point of (TOP-REAL 2) by A10;
A11: f . s = ((1 - s) * (p1 - |[a,b]|)) + (s * (p2 - |[a,b]|)) by A3, BORSUK_1:83
.= (((1 - s) * p1) - ((1 - s) * |[a,b]|)) + (s * (p2 - |[a,b]|)) by EUCLID:53
.= (((1 - s) * p1) - ((1 - s) * |[a,b]|)) + ((s * p2) - (s * |[a,b]|)) by EUCLID:53
.= (((1 - s) * p1) + ((- (1 - s)) * |[a,b]|)) + ((s * p2) - (s * |[a,b]|)) by EUCLID:44
.= (((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 EUCLID:37
.= ((((1 - s) * p1) + ((- 1) * |[a,b]|)) + (s * |[a,b]|)) + ((s * p2) + (- (s * |[a,b]|))) by EUCLID:30
.= (((1 - s) * p1) + ((- 1) * |[a,b]|)) + ((s * |[a,b]|) + ((s * p2) + (- (s * |[a,b]|)))) by EUCLID:30
.= (((1 - s) * p1) + ((- 1) * |[a,b]|)) + (((s * |[a,b]|) + (- (s * |[a,b]|))) + (s * p2)) by EUCLID:30
.= (((1 - s) * p1) + ((- 1) * |[a,b]|)) + (((s * |[a,b]|) + ((- s) * |[a,b]|)) + (s * p2)) by EUCLID:44
.= (((1 - s) * p1) + ((- 1) * |[a,b]|)) + (((s + (- s)) * |[a,b]|) + (s * p2)) by EUCLID:37
.= (((1 - s) * p1) + ((- 1) * |[a,b]|)) + ((0. (TOP-REAL 2)) + (s * p2)) by EUCLID:33
.= (((1 - s) * p1) + ((- 1) * |[a,b]|)) + (s * p2) by EUCLID:31
.= (((1 - s) * p1) + (s * p2)) + ((- 1) * |[a,b]|) by EUCLID:30 ;
set p = p' + |[a,b]|;
A12: p' + |[a,b]| = ((((1 - s) * p1) + (s * p2)) + ((- 1) * |[a,b]|)) + |[a,b]| by A11
.= ((((1 - s) * p1) + (s * p2)) + (- |[a,b]|)) + |[a,b]| by EUCLID:43
.= (((1 - s) * p1) + (s * p2)) + ((- |[a,b]|) + |[a,b]|) by EUCLID:30
.= (((1 - s) * p1) + (s * p2)) + (0. (TOP-REAL 2)) by EUCLID:40
.= ((1 - s) * p1) + (s * p2) by EUCLID:31 ;
A13: ((1 - s) * p1) + (s * p2) in LSeg p1,p2 by A9;
r = |.(p' + (0. (TOP-REAL 2))).| by A7, EUCLID:31
.= |.(p' + (|[a,b]| - |[a,b]|)).| by EUCLID:46
.= |.((p' + |[a,b]|) + (- |[a,b]|)).| by EUCLID:30
.= |.((p' + |[a,b]|) - |[a,b]|).| ;
then p' + |[a,b]| in { p'' where p'' is Point of (TOP-REAL 2) : |.(p'' - |[a,b]|).| = r } ;
then A14: p' + |[a,b]| in circle a,b,r by JGRAPH_6:def 5;
take p' + |[a,b]| ; :: thesis:
thus p' + |[a,b]| in (LSeg p1,p2) /\ (circle a,b,r) by A12, A13, A14, XBOOLE_0:def 4; :: thesis: