let p1, p2, p3, p be Point of (TOP-REAL 2); :: thesis: ( p in LSeg (p1,p2) & not p3 in LSeg (p1,p2) implies ex p4 being Point of (TOP-REAL 2) st
( p4 in LSeg (p1,p2) & angle (p1,p3,p4) = angle (p,p3,p2) ) )
assume A1: p in LSeg (p1,p2) ; :: thesis: ( p3 in LSeg (p1,p2) or ex p4 being Point of (TOP-REAL 2) st
( p4 in LSeg (p1,p2) & angle (p1,p3,p4) = angle (p,p3,p2) ) )
assume A2: not p3 in LSeg (p1,p2) ; :: thesis: ex p4 being Point of (TOP-REAL 2) st
( p4 in LSeg (p1,p2) & angle (p1,p3,p4) = angle (p,p3,p2) )
per cases ( p1 = p2 or p = p2 or p1 in LSeg (p2,p3) or p = p1 or p2 in LSeg (p1,p3) or ( p1 <> p2 & p <> p1 & p <> p2 & not p1 in LSeg (p2,p3) & not p2 in LSeg (p1,p3) ) ) ;
suppose A3: p1 = p2 ; :: thesis: ex p4 being Point of (TOP-REAL 2) st
( p4 in LSeg (p1,p2) & angle (p1,p3,p4) = angle (p,p3,p2) )
set p4 = p;
take p ; :: thesis: ( p in LSeg (p1,p2) & angle (p1,p3,p) = angle (p,p3,p2) )
thus p in LSeg (p1,p2) by A1; :: thesis: angle (p1,p3,p) = angle (p,p3,p2)
LSeg (p1,p2) = {p1} by A3, RLTOPSP1:70;
then p = p1 by A1, TARSKI:def 1;
hence angle (p1,p3,p) = angle (p,p3,p2) by A3; :: thesis: verum
end;
suppose A4: ( p = p2 or p1 in LSeg (p2,p3) ) ; :: thesis: ex p4 being Point of (TOP-REAL 2) st
( p4 in LSeg (p1,p2) & angle (p1,p3,p4) = angle (p,p3,p2) )
set p4 = p1;
take p1 ; :: thesis: ( p1 in LSeg (p1,p2) & angle (p1,p3,p1) = angle (p,p3,p2) )
thus p1 in LSeg (p1,p2) by RLTOPSP1:68; :: thesis: angle (p1,p3,p1) = angle (p,p3,p2)
per cases ( p = p2 or p1 in LSeg (p2,p3) ) by A4;
suppose A5: p = p2 ; :: thesis: angle (p1,p3,p1) = angle (p,p3,p2)
thus angle (p1,p3,p1) = 0 by COMPLEX2:79
.= angle (p,p3,p2) by A5, COMPLEX2:79 ; :: thesis: verum
end;
suppose A6: p1 in LSeg (p2,p3) ; :: thesis: angle (p1,p3,p1) = angle (p,p3,p2)
p2 in LSeg (p3,p2) by RLTOPSP1:68;
then A7: LSeg (p1,p2) c= LSeg (p3,p2) by A6, TOPREAL1:6;
thus angle (p1,p3,p1) = 0 by COMPLEX2:79
.= angle (p2,p3,p2) by COMPLEX2:79
.= angle (p,p3,p2) by A1, A2, A7, Th9 ; :: thesis: verum
end;
end;
end;
suppose A8: ( p = p1 or p2 in LSeg (p1,p3) ) ; :: thesis: ex p4 being Point of (TOP-REAL 2) st
( p4 in LSeg (p1,p2) & angle (p1,p3,p4) = angle (p,p3,p2) )
set p4 = p2;
take p2 ; :: thesis: ( p2 in LSeg (p1,p2) & angle (p1,p3,p2) = angle (p,p3,p2) )
thus p2 in LSeg (p1,p2) by RLTOPSP1:68; :: thesis: angle (p1,p3,p2) = angle (p,p3,p2)
per cases ( p = p1 or p2 in LSeg (p1,p3) ) by A8;
suppose p = p1 ; :: thesis: angle (p1,p3,p2) = angle (p,p3,p2)
hence angle (p1,p3,p2) = angle (p,p3,p2) ; :: thesis: verum
end;
suppose A9: p2 in LSeg (p1,p3) ; :: thesis: angle (p1,p3,p2) = angle (p,p3,p2)
p1 in LSeg (p1,p3) by RLTOPSP1:68;
then LSeg (p1,p2) c= LSeg (p1,p3) by A9, TOPREAL1:6;
hence angle (p1,p3,p2) = angle (p,p3,p2) by A1, A2, Th9; :: thesis: verum
end;
end;
end;
suppose A10: ( p1 <> p2 & p <> p1 & p <> p2 & not p1 in LSeg (p2,p3) & not p2 in LSeg (p1,p3) ) ; :: thesis: ex p4 being Point of (TOP-REAL 2) st
( p4 in LSeg (p1,p2) & angle (p1,p3,p4) = angle (p,p3,p2) )
p1 in LSeg (p1,p2) by RLTOPSP1:68;
then reconsider q1 = p1 as Point of ((TOP-REAL 2) | (LSeg (p1,p2))) by PRE_TOPC:8;
A11: 1 * (- 2) <= (cos (angle (p,p3,p2))) * (- 2) by SIN_COS6:6, XREAL_1:65;
consider f1 being Function of (TOP-REAL 2),R^1 such that
A12: for q being Point of (TOP-REAL 2) holds f1 . q = |.(q - p1).| and
A13: f1 is continuous by Lm21;
consider f12 being Function of (TOP-REAL 2),R^1 such that
A14: for q being Point of (TOP-REAL 2)
for r1, r2 being Real st f1 . q = r1 & f1 . q = r2 holds
f12 . q = r1 * r2 and
A15: f12 is continuous by A13, JGRAPH_2:25;
consider f3 being Function of (TOP-REAL 2),R^1 such that
A16: for q being Point of (TOP-REAL 2) holds f3 . q = |.(q - p3).| and
A17: f3 is continuous by Lm21;
consider f32 being Function of (TOP-REAL 2),R^1 such that
A18: for q being Point of (TOP-REAL 2)
for r1, r2 being Real st f3 . q = r1 & f3 . q = r2 holds
f32 . q = r1 * r2 and
A19: f32 is continuous by A17, JGRAPH_2:25;
A20: |.(p2 - p1).| ^2 = ((|.(p1 - p3).| ^2) + (|.(p2 - p3).| ^2)) - (((2 * |.(p1 - p3).|) * |.(p2 - p3).|) * (cos (angle (p1,p3,p2)))) by Th7;
A21: p2 <> p3 by A2, RLTOPSP1:68;
then A22: |.(p2 - p3).| <> 0 by Lm1;
p2 in LSeg (p1,p2) by RLTOPSP1:68;
then reconsider q2 = p2 as Point of ((TOP-REAL 2) | (LSeg (p1,p2))) by PRE_TOPC:8;
consider f0 being Function of ((TOP-REAL 2) | (LSeg (p1,p2))),(TOP-REAL 2) such that
A23: for q being Point of ((TOP-REAL 2) | (LSeg (p1,p2))) holds f0 . q = q and
A24: f0 is continuous by JGRAPH_6:6;
set d = (((|.(p2 - p).| ^2) - (|.(p - p3).| ^2)) - (|.(p2 - p3).| ^2)) / (|.(p - p3).| * |.(p2 - p3).|);
consider f2 being Function of (TOP-REAL 2),R^1 such that
A25: for q being Point of (TOP-REAL 2) holds f2 . q = |.(p1 - p3).| and
A26: f2 is continuous by JGRAPH_2:20;
A27: p1 <> p3 by A2, RLTOPSP1:68;
then A28: |.(p1 - p3).| <> 0 by Lm1;
A29: cos (angle (p,p3,p2)) <> 1
proof
A30: ( 0 <= angle (p,p3,p2) & angle (p,p3,p2) < 2 * PI ) by COMPLEX2:70;
assume cos (angle (p,p3,p2)) = 1 ; :: thesis: contradiction
then A31: angle (p,p3,p2) = 0 by A30, COMPTRIG:61;
A32: ( euc2cpx p <> euc2cpx p3 & euc2cpx p <> euc2cpx p2 ) by A1, A2, A10, EUCLID_3:4;
A33: euc2cpx p3 <> euc2cpx p2 by A21, EUCLID_3:4;
per cases ( ( angle (p3,p2,p) = 0 & angle (p2,p,p3) = PI ) or ( angle (p3,p2,p) = PI & angle (p2,p,p3) = 0 ) ) by A31, A32, A33, COMPLEX2:87;
suppose ( angle (p3,p2,p) = 0 & angle (p2,p,p3) = PI ) ; :: thesis: contradiction
then p in LSeg (p2,p3) by Th11;
hence contradiction by A1, A2, A10, A27, Th12; :: thesis: verum
end;
suppose ( angle (p3,p2,p) = PI & angle (p2,p,p3) = 0 ) ; :: thesis: contradiction
then angle (p3,p2,p1) = PI by A1, A10, Th10;
hence contradiction by A10, Th11; :: thesis: verum
end;
end;
end;
A34: for q being Point of ((TOP-REAL 2) | (LSeg (p1,p2))) holds
( q is Point of (TOP-REAL 2) & q in LSeg (p1,p2) )
proof
let q be Point of ((TOP-REAL 2) | (LSeg (p1,p2))); :: thesis: ( q is Point of (TOP-REAL 2) & q in LSeg (p1,p2) )
A35: q in the carrier of ((TOP-REAL 2) | (LSeg (p1,p2))) ;
then q in LSeg (p1,p2) by PRE_TOPC:8;
hence q is Point of (TOP-REAL 2) ; :: thesis: q in LSeg (p1,p2)
thus q in LSeg (p1,p2) by A35, PRE_TOPC:8; :: thesis: verum
end;
consider f6 being Function of (TOP-REAL 2),R^1 such that
A36: for q being Point of (TOP-REAL 2)
for r1, r2 being Real st f2 . q = r1 & f3 . q = r2 holds
f6 . q = r1 * r2 and
A37: f6 is continuous by A26, A17, JGRAPH_2:25;
reconsider f8 = f6 * f0 as continuous Function of ((TOP-REAL 2) | (LSeg (p1,p2))),R^1 by A24, A37;
consider f22 being Function of (TOP-REAL 2),R^1 such that
A38: for q being Point of (TOP-REAL 2)
for r1, r2 being Real st f2 . q = r1 & f2 . q = r2 holds
f22 . q = r1 * r2 and
A39: f22 is continuous by A26, JGRAPH_2:25;
consider f4 being Function of (TOP-REAL 2),R^1 such that
A40: for q being Point of (TOP-REAL 2)
for r1, r2 being Real st f12 . q = r1 & f22 . q = r2 holds
f4 . q = r1 - r2 and
A41: f4 is continuous by A15, A39, JGRAPH_2:21;
consider f5 being Function of (TOP-REAL 2),R^1 such that
A42: for q being Point of (TOP-REAL 2)
for r1, r2 being Real st f4 . q = r1 & f32 . q = r2 holds
f5 . q = r1 - r2 and
A43: f5 is continuous by A19, A41, JGRAPH_2:21;
A44: |.(p - p3).| <> 0 by A1, A2, Lm1;
reconsider f7 = f5 * f0 as continuous Function of ((TOP-REAL 2) | (LSeg (p1,p2))),R^1 by A24, A43;
A45: for q being Point of ((TOP-REAL 2) | (LSeg (p1,p2)))
for q1 being Point of (TOP-REAL 2) st q = q1 holds
f8 . q = |.(p1 - p3).| * |.(q1 - p3).|
proof
let q be Point of ((TOP-REAL 2) | (LSeg (p1,p2))); :: thesis: for q1 being Point of (TOP-REAL 2) st q = q1 holds
f8 . q = |.(p1 - p3).| * |.(q1 - p3).|
let q1 be Point of (TOP-REAL 2); :: thesis: ( q = q1 implies f8 . q = |.(p1 - p3).| * |.(q1 - p3).| )
dom f8 = the carrier of ((TOP-REAL 2) | (LSeg (p1,p2))) by FUNCT_2:def 1;
then A46: f8 . q = f6 . (f0 . q) by FUNCT_1:12
.= f6 . q by A23 ;
assume A47: q = q1 ; :: thesis: f8 . q = |.(p1 - p3).| * |.(q1 - p3).|
then ( f6 . q = (f2 . q) * (f3 . q) & f2 . q = |.(p1 - p3).| ) by A25, A36;
hence f8 . q = |.(p1 - p3).| * |.(q1 - p3).| by A16, A47, A46; :: thesis: verum
end;
for q being Point of ((TOP-REAL 2) | (LSeg (p1,p2))) holds f8 . q <> 0
proof
let q be Point of ((TOP-REAL 2) | (LSeg (p1,p2))); :: thesis: f8 . q <> 0
reconsider q1 = q as Point of (TOP-REAL 2) by A34;
A48: f8 . q = |.(p1 - p3).| * |.(q1 - p3).| by A45;
assume A49: f8 . q = 0 ; :: thesis: contradiction
per cases ( |.(p1 - p3).| = 0 or |.(q1 - p3).| = 0 ) by A48, A49;
suppose |.(p1 - p3).| = 0 ; :: thesis: contradiction
hence contradiction by A27, Lm1; :: thesis: verum
end;
suppose |.(q1 - p3).| = 0 ; :: thesis: contradiction
then q = p3 by Lm1;
hence contradiction by A2, A34; :: thesis: verum
end;
end;
end;
then consider f9 being Function of ((TOP-REAL 2) | (LSeg (p1,p2))),R^1 such that
A50: for q being Point of ((TOP-REAL 2) | (LSeg (p1,p2)))
for r1, r2 being Real st f7 . q = r1 & f8 . q = r2 holds
f9 . q = r1 / r2 and
A51: f9 is continuous by JGRAPH_2:27;
consider f being Function of I[01],((TOP-REAL 2) | (LSeg (p1,p2))) such that
A52: for x being Real st x in [.0,1.] holds
f . x = ((1 - x) * p1) + (x * p2) and
A53: f is being_homeomorphism and
A54: f . 0 = p1 and
A55: f . 1 = p2 by A10, JORDAN5A:3;
f is continuous by A53, TOPS_2:def 5;
then reconsider g = f9 * f as continuous Function of (Closed-Interval-TSpace (0,1)),R^1 by A51, TOPMETR:20;
A56: dom g = [.0,1.] by BORSUK_1:40, FUNCT_2:def 1;
set b = g . 1;
1 in { r where r is Real : ( 0 <= r & r <= 1 ) } ;
then 1 in dom g by A56, RCOMP_1:def 1;
then A57: g . 1 = f9 . p2 by A55, FUNCT_1:12;
|.(p2 - p).| ^2 = ((|.(p - p3).| ^2) + (|.(p2 - p3).| ^2)) - (((2 * |.(p - p3).|) * |.(p2 - p3).|) * (cos (angle (p,p3,p2)))) by Th7;
then A58: (((|.(p2 - p).| ^2) - (|.(p - p3).| ^2)) - (|.(p2 - p3).| ^2)) / (|.(p - p3).| * |.(p2 - p3).|) = ((- 2) * ((|.(p - p3).| * |.(p2 - p3).|) * (cos (angle (p,p3,p2))))) / (|.(p - p3).| * |.(p2 - p3).|)
.= (- 2) * (((|.(p - p3).| * |.(p2 - p3).|) * (cos (angle (p,p3,p2)))) / (|.(p - p3).| * |.(p2 - p3).|)) by XCMPLX_1:74
.= (- 2) * (cos (angle (p,p3,p2))) by A22, A44, XCMPLX_1:89 ;
A59: for q being Point of ((TOP-REAL 2) | (LSeg (p1,p2)))
for q1 being Point of (TOP-REAL 2) st q = q1 holds
f9 . q = (((|.(q1 - p1).| ^2) - (|.(p1 - p3).| ^2)) - (|.(q1 - p3).| ^2)) / (|.(p1 - p3).| * |.(q1 - p3).|)
proof
let q be Point of ((TOP-REAL 2) | (LSeg (p1,p2))); :: thesis: for q1 being Point of (TOP-REAL 2) st q = q1 holds
f9 . q = (((|.(q1 - p1).| ^2) - (|.(p1 - p3).| ^2)) - (|.(q1 - p3).| ^2)) / (|.(p1 - p3).| * |.(q1 - p3).|)
let q1 be Point of (TOP-REAL 2); :: thesis: ( q = q1 implies f9 . q = (((|.(q1 - p1).| ^2) - (|.(p1 - p3).| ^2)) - (|.(q1 - p3).| ^2)) / (|.(p1 - p3).| * |.(q1 - p3).|) )
A60: q is Point of (TOP-REAL 2) by A34;
dom f7 = the carrier of ((TOP-REAL 2) | (LSeg (p1,p2))) by FUNCT_2:def 1;
then A61: f7 . q = f5 . (f0 . q) by FUNCT_1:12
.= f5 . q by A23
.= (f4 . q) - (f32 . q) by A42, A60
.= ((f12 . q) - (f22 . q)) - (f32 . q) by A40, A60
.= ((f12 . q) - (f22 . q)) - ((f3 . q) * (f3 . q)) by A18, A60
.= (((f1 . q) * (f1 . q)) - (f22 . q)) - ((f3 . q) * (f3 . q)) by A14, A60
.= (((f1 . q) * (f1 . q)) - ((f2 . q) * (f2 . q))) - ((f3 . q) * (f3 . q)) by A38, A60 ;
A62: f9 . q = (f7 . q) / (f8 . q) by A50;
assume A63: q = q1 ; :: thesis: f9 . q = (((|.(q1 - p1).| ^2) - (|.(p1 - p3).| ^2)) - (|.(q1 - p3).| ^2)) / (|.(p1 - p3).| * |.(q1 - p3).|)
then A64: f3 . q = |.(q1 - p3).| by A16;
( f1 . q = |.(q1 - p1).| & f2 . q = |.(p1 - p3).| ) by A12, A25, A63;
hence f9 . q = (((|.(q1 - p1).| ^2) - (|.(p1 - p3).| ^2)) - (|.(q1 - p3).| ^2)) / (|.(p1 - p3).| * |.(q1 - p3).|) by A45, A63, A62, A61, A64; :: thesis: verum
end;
then f9 . q2 = (((|.(p2 - p1).| ^2) - (|.(p1 - p3).| ^2)) - (|.(p2 - p3).| ^2)) / (|.(p1 - p3).| * |.(p2 - p3).|) ;
then A65: f9 . q2 = ((- 2) * ((|.(p1 - p3).| * |.(p2 - p3).|) * (cos (angle (p1,p3,p2))))) / (|.(p1 - p3).| * |.(p2 - p3).|) by A20
.= (- 2) * (((|.(p1 - p3).| * |.(p2 - p3).|) * (cos (angle (p1,p3,p2)))) / (|.(p1 - p3).| * |.(p2 - p3).|)) by XCMPLX_1:74
.= (- 2) * (cos (angle (p1,p3,p2))) by A28, A22, XCMPLX_1:89 ;
A66: (((|.(p2 - p).| ^2) - (|.(p - p3).| ^2)) - (|.(p2 - p3).| ^2)) / (|.(p - p3).| * |.(p2 - p3).|) < g . 1
proof
per cases ( angle (p1,p3,p2) <= PI or angle (p1,p3,p2) > PI ) ;
suppose A67: angle (p1,p3,p2) <= PI ; :: thesis: (((|.(p2 - p).| ^2) - (|.(p - p3).| ^2)) - (|.(p2 - p3).| ^2)) / (|.(p - p3).| * |.(p2 - p3).|) < g . 1
A68: [.0,PI.] /\ (dom cos) = [.0,PI.] by SIN_COS:24, XBOOLE_1:28;
0 <= angle (p1,p3,p2) by COMPLEX2:70;
then A69: angle (p1,p3,p2) in [.0,PI.] /\ (dom cos) by A67, A68, XXREAL_1:1;
A70: ( cos . (angle (p1,p3,p2)) = cos (angle (p1,p3,p2)) & cos . (angle (p,p3,p2)) = cos (angle (p,p3,p2)) ) by SIN_COS:def 19;
A71: angle (p,p3,p2) <= angle (p1,p3,p2) by A1, A2, A67, Th26;
then ( 0 <= angle (p,p3,p2) & angle (p,p3,p2) <= PI ) by A67, COMPLEX2:70, XXREAL_0:2;
then A72: angle (p,p3,p2) in [.0,PI.] /\ (dom cos) by A68, XXREAL_1:1;
p1,p2,p3 is_a_triangle by A2, A10, TOPREAL9:67;
then A73: angle (p,p3,p2) < angle (p1,p3,p2) by A1, A10, A71, Th25, XXREAL_0:1;
cos | [.((2 * PI) * 0),(PI + ((2 * PI) * 0)).] is decreasing by SIN_COS6:55;
then cos . (angle (p1,p3,p2)) < cos . (angle (p,p3,p2)) by A73, A72, A69, RFUNCT_2:21;
hence (((|.(p2 - p).| ^2) - (|.(p - p3).| ^2)) - (|.(p2 - p3).| ^2)) / (|.(p - p3).| * |.(p2 - p3).|) < g . 1 by A57, A65, A58, A70, XREAL_1:69; :: thesis: verum
end;
suppose A74: angle (p1,p3,p2) > PI ; :: thesis: (((|.(p2 - p).| ^2) - (|.(p - p3).| ^2)) - (|.(p2 - p3).| ^2)) / (|.(p - p3).| * |.(p2 - p3).|) < g . 1
A75: [.PI,(2 * PI).] /\ (dom cos) = [.PI,(2 * PI).] by SIN_COS:24, XBOOLE_1:28;
A76: angle (p,p3,p2) <= 2 * PI by COMPLEX2:70;
A77: angle (p,p3,p2) >= angle (p1,p3,p2) by A1, A2, A10, A74, Th27;
then PI <= angle (p,p3,p2) by A74, XXREAL_0:2;
then A78: angle (p,p3,p2) in [.PI,(2 * PI).] /\ (dom cos) by A75, A76, XXREAL_1:1;
angle (p1,p3,p2) <= 2 * PI by COMPLEX2:70;
then A79: angle (p1,p3,p2) in [.PI,(2 * PI).] /\ (dom cos) by A74, A75, XXREAL_1:1;
A80: ( cos . (angle (p1,p3,p2)) = cos (angle (p1,p3,p2)) & cos . (angle (p,p3,p2)) = cos (angle (p,p3,p2)) ) by SIN_COS:def 19;
p1,p2,p3 is_a_triangle by A2, A10, TOPREAL9:67;
then A81: angle (p,p3,p2) > angle (p1,p3,p2) by A1, A10, A77, Th25, XXREAL_0:1;
cos | [.(PI + ((2 * PI) * 0)),((2 * PI) + ((2 * PI) * 0)).] is increasing by SIN_COS6:56;
then cos . (angle (p1,p3,p2)) < cos . (angle (p,p3,p2)) by A81, A78, A79, RFUNCT_2:20;
hence (((|.(p2 - p).| ^2) - (|.(p - p3).| ^2)) - (|.(p2 - p3).| ^2)) / (|.(p - p3).| * |.(p2 - p3).|) < g . 1 by A57, A65, A58, A80, XREAL_1:69; :: thesis: verum
end;
end;
end;
set a = g . 0;
0 in { r where r is Real : ( 0 <= r & r <= 1 ) } ;
then 0 in dom g by A56, RCOMP_1:def 1;
then A82: g . 0 = f9 . p1 by A54, FUNCT_1:12;
A83: f9 . q1 = (((|.(p1 - p1).| ^2) - (|.(p1 - p3).| ^2)) - (|.(p1 - p3).| ^2)) / (|.(p1 - p3).| * |.(p1 - p3).|) by A59
.= (((0 ^2) - (|.(p1 - p3).| ^2)) - (|.(p1 - p3).| ^2)) / (|.(p1 - p3).| * |.(p1 - p3).|) by Lm1
.= ((- 2) * (|.(p1 - p3).| ^2)) / (|.(p1 - p3).| * |.(p1 - p3).|)
.= - 2 by A28, XCMPLX_1:89 ;
then g . 0 <> (((|.(p2 - p).| ^2) - (|.(p - p3).| ^2)) - (|.(p2 - p3).| ^2)) / (|.(p - p3).| * |.(p2 - p3).|) by A82, A58, A29;
then g . 0 < (((|.(p2 - p).| ^2) - (|.(p - p3).| ^2)) - (|.(p2 - p3).| ^2)) / (|.(p - p3).| * |.(p2 - p3).|) by A82, A83, A58, A11, XXREAL_0:1;
then consider rc being Real such that
A84: g . rc = (((|.(p2 - p).| ^2) - (|.(p - p3).| ^2)) - (|.(p2 - p3).| ^2)) / (|.(p - p3).| * |.(p2 - p3).|) and
A85: ( 0 < rc & rc < 1 ) by A66, TOPREAL5:6;
rc in { r where r is Real : ( 0 <= r & r <= 1 ) } by A85;
then A86: rc in dom g by A56, RCOMP_1:def 1;
then A87: f . rc = ((1 - rc) * p1) + (rc * p2) by A52, A56;
set p4 = ((1 - rc) * p1) + (rc * p2);
take ((1 - rc) * p1) + (rc * p2) ; :: thesis: ( ((1 - rc) * p1) + (rc * p2) in LSeg (p1,p2) & angle (p1,p3,(((1 - rc) * p1) + (rc * p2))) = angle (p,p3,p2) )
thus A88: ((1 - rc) * p1) + (rc * p2) in LSeg (p1,p2) by A85; :: thesis: angle (p1,p3,(((1 - rc) * p1) + (rc * p2))) = angle (p,p3,p2)
then reconsider q = ((1 - rc) * p1) + (rc * p2) as Point of ((TOP-REAL 2) | (LSeg (p1,p2))) by PRE_TOPC:8;
A89: |.((((1 - rc) * p1) + (rc * p2)) - p3).| <> 0 by A2, A88, Lm1;
set r2 = |.(p1 - p3).| * |.((((1 - rc) * p1) + (rc * p2)) - p3).|;
A90: |.((((1 - rc) * p1) + (rc * p2)) - p1).| ^2 = ((|.(p1 - p3).| ^2) + (|.((((1 - rc) * p1) + (rc * p2)) - p3).| ^2)) - (((2 * |.(p1 - p3).|) * |.((((1 - rc) * p1) + (rc * p2)) - p3).|) * (cos (angle (p1,p3,(((1 - rc) * p1) + (rc * p2)))))) by Th7;
f9 . q = (((|.((((1 - rc) * p1) + (rc * p2)) - p1).| ^2) - (|.(p1 - p3).| ^2)) - (|.((((1 - rc) * p1) + (rc * p2)) - p3).| ^2)) / (|.(p1 - p3).| * |.((((1 - rc) * p1) + (rc * p2)) - p3).|) by A59;
then A91: (((|.(p2 - p).| ^2) - (|.(p - p3).| ^2)) - (|.(p2 - p3).| ^2)) / (|.(p - p3).| * |.(p2 - p3).|) = ((- 2) * ((|.(p1 - p3).| * |.((((1 - rc) * p1) + (rc * p2)) - p3).|) * (cos (angle (p1,p3,(((1 - rc) * p1) + (rc * p2))))))) / (|.(p1 - p3).| * |.((((1 - rc) * p1) + (rc * p2)) - p3).|) by A84, A86, A87, A90, FUNCT_1:12
.= (- 2) * (((|.(p1 - p3).| * |.((((1 - rc) * p1) + (rc * p2)) - p3).|) * (cos (angle (p1,p3,(((1 - rc) * p1) + (rc * p2)))))) / (|.(p1 - p3).| * |.((((1 - rc) * p1) + (rc * p2)) - p3).|)) by XCMPLX_1:74
.= (- 2) * (cos (angle (p1,p3,(((1 - rc) * p1) + (rc * p2))))) by A28, A89, XCMPLX_1:89 ;
A92: p1 <> ((1 - rc) * p1) + (rc * p2)
proof
A93: |.(p1 - p3).| <> 0 by A27, Lm1;
assume A94: p1 = ((1 - rc) * p1) + (rc * p2) ; :: thesis: contradiction
0 = 0 * |.(p1 - p1).|
.= ((2 * |.(p1 - p3).|) * |.(p1 - p3).|) - (((2 * |.(p1 - p3).|) * |.(p1 - p3).|) * (cos (angle (p1,p3,(((1 - rc) * p1) + (rc * p2)))))) by A90, A94, Lm1 ;
hence contradiction by A58, A29, A91, A93, XCMPLX_1:7; :: thesis: verum
end;
A95: p3 <> ((1 - rc) * p1) + (rc * p2) by A2, A85;
per cases ( angle (p,p3,p2) <= PI or angle (p,p3,p2) > PI ) ;
suppose A96: angle (p,p3,p2) <= PI ; :: thesis: angle (p1,p3,(((1 - rc) * p1) + (rc * p2))) = angle (p,p3,p2)
p,p3,p2 are_mutually_distinct by A1, A2, A10, A21, ZFMISC_1:def 5;
then angle (p3,p2,p) <= PI by A96, Th23;
then A97: angle (p3,p2,p1) <= PI by A1, A10, Th10;
p3,p2,p1 are_mutually_distinct by A10, A27, A21, ZFMISC_1:def 5;
then angle (p2,p1,p3) <= PI by A97, Th23;
then A98: angle ((((1 - rc) * p1) + (rc * p2)),p1,p3) <= PI by A88, A92, Th9;
((1 - rc) * p1) + (rc * p2),p1,p3 are_mutually_distinct by A27, A92, A95, ZFMISC_1:def 5;
then angle (p1,p3,(((1 - rc) * p1) + (rc * p2))) <= PI by A98, Th23;
hence angle (p1,p3,(((1 - rc) * p1) + (rc * p2))) = arccos (cos (angle (p1,p3,(((1 - rc) * p1) + (rc * p2))))) by COMPLEX2:70, SIN_COS6:92
.= angle (p,p3,p2) by A58, A91, A96, COMPLEX2:70, SIN_COS6:92 ;
:: thesis: verum
end;
suppose A99: angle (p,p3,p2) > PI ; :: thesis: angle (p1,p3,(((1 - rc) * p1) + (rc * p2))) = angle (p,p3,p2)
p,p3,p2 are_mutually_distinct by A1, A2, A10, A21, ZFMISC_1:def 5;
then angle (p3,p2,p) > PI by A99, Th24;
then A100: angle (p3,p2,p1) > PI by A1, A10, Th10;
p3,p2,p1 are_mutually_distinct by A10, A27, A21, ZFMISC_1:def 5;
then angle (p2,p1,p3) > PI by A100, Th24;
then A101: angle ((((1 - rc) * p1) + (rc * p2)),p1,p3) > PI by A88, A92, Th9;
((1 - rc) * p1) + (rc * p2),p1,p3 are_mutually_distinct by A27, A92, A95, ZFMISC_1:def 5;
then angle (p1,p3,(((1 - rc) * p1) + (rc * p2))) > PI by A101, Th24;
then - (angle (p1,p3,(((1 - rc) * p1) + (rc * p2)))) < - PI by XREAL_1:24;
then A102: (- (angle (p1,p3,(((1 - rc) * p1) + (rc * p2))))) + (2 * PI) < (- PI) + (2 * PI) by XREAL_1:6;
A103: cos ((2 * PI) - (angle (p1,p3,(((1 - rc) * p1) + (rc * p2))))) = cos . ((- (angle (p1,p3,(((1 - rc) * p1) + (rc * p2))))) + ((2 * PI) * 1)) by SIN_COS:def 19
.= cos . (- (angle (p1,p3,(((1 - rc) * p1) + (rc * p2))))) by SIN_COS6:10
.= cos . (angle (p1,p3,(((1 - rc) * p1) + (rc * p2)))) by SIN_COS:30
.= cos (angle (p,p3,p2)) by A58, A91, SIN_COS:def 19
.= cos . (angle (p,p3,p2)) by SIN_COS:def 19
.= cos . (- (angle (p,p3,p2))) by SIN_COS:30
.= cos . ((- (angle (p,p3,p2))) + ((2 * PI) * 1)) by SIN_COS6:10
.= cos ((2 * PI) - (angle (p,p3,p2))) by SIN_COS:def 19 ;
- (angle (p,p3,p2)) < - PI by A99, XREAL_1:24;
then A104: (- (angle (p,p3,p2))) + (2 * PI) < (- PI) + (2 * PI) by XREAL_1:6;
angle (p,p3,p2) < 2 * PI by COMPLEX2:70;
then - (angle (p,p3,p2)) > - (2 * PI) by XREAL_1:24;
then A105: (- (angle (p,p3,p2))) + (2 * PI) > (- (2 * PI)) + (2 * PI) by XREAL_1:6;
angle (p1,p3,(((1 - rc) * p1) + (rc * p2))) < 2 * PI by COMPLEX2:70;
then - (angle (p1,p3,(((1 - rc) * p1) + (rc * p2)))) > - (2 * PI) by XREAL_1:24;
then (- (angle (p1,p3,(((1 - rc) * p1) + (rc * p2))))) + (2 * PI) > (- (2 * PI)) + (2 * PI) by XREAL_1:6;
then (2 * PI) - (angle (p1,p3,(((1 - rc) * p1) + (rc * p2)))) = arccos (cos ((2 * PI) - (angle (p1,p3,(((1 - rc) * p1) + (rc * p2)))))) by A102, SIN_COS6:92
.= (2 * PI) - (angle (p,p3,p2)) by A104, A103, A105, SIN_COS6:92 ;
hence angle (p1,p3,(((1 - rc) * p1) + (rc * p2))) = angle (p,p3,p2) ; :: thesis: verum
end;
end;
end;
end;