let A, B, C be Point of (TOP-REAL 2); :: thesis: ( A <> B & |.(C - A).| = |.(C - B).| implies C in the_perpendicular_bisector (A,B) )
assume that
A1: A <> B and
A2: |.(C - A).| = |.(C - B).| ; :: thesis: C in the_perpendicular_bisector (A,B)
assume A3: not C in the_perpendicular_bisector (A,B) ; :: thesis: contradiction
consider L1, L2 being Element of line_of_REAL 2 such that
the_perpendicular_bisector (A,B) = L2 and
A4: L1 = Line (A,B) and
A5: L1 _|_ L2 and
L1 /\ L2 = {(the_midpoint_of_the_segment (A,B))} by A1, Def2;
reconsider rA = A, rB = B, rC = C as Element of REAL 2 by EUCLID:22;
L1 is being_line by A5, EUCLIDLP:67;
then consider L3 being Element of line_of_REAL 2 such that
A6: rC in L3 and
A7: L1 _|_ L3 by Th35;
consider x being Element of REAL 2 such that
A8: L1 /\ L3 = {x} by A7, Th33;
reconsider D = x as Point of (TOP-REAL 2) by EUCLID:22;
A9: D in L1 /\ L3 by A8, TARSKI:def 1;
A10: now :: thesis: ( not A = D & not C = D & not B = D )
assume ( A = D or C = D or B = D ) ; :: thesis: contradiction
per cases then ( A = D or C = D or B = D ) ;
suppose A11: A = D ; :: thesis: contradiction
now :: thesis: ( L1 _|_ L3 & A in L3 /\ L1 & C in L3 & B in L1 & A <> C & B <> A )
thus L1 _|_ L3 by A7; :: thesis: ( A in L3 /\ L1 & C in L3 & B in L1 & A <> C & B <> A )
thus A in L3 /\ L1 by A11, A8, TARSKI:def 1; :: thesis: ( C in L3 & B in L1 & A <> C & B <> A )
thus ( C in L3 & B in L1 ) by A6, A4, RLTOPSP1:72; :: thesis: ( A <> C & B <> A )
A <> C hence ( A <> C & B <> A ) by A1; :: thesis: verum
end;
then A13: cos (angle (C,A,B)) = 0 by SIN_COS:77, Th38;
set z1 = |.(B - C).|;
set z2 = |.(C - A).|;
set z3 = |.(B - A).|;
A14: |.(B - C).| ^2 = ((|.(C - A).| ^2) + (|.(B - A).| ^2)) - (((2 * |.(C - A).|) * |.(B - A).|) * (cos (angle (C,A,B)))) by EUCLID_6:7
.= (|.(C - A).| ^2) + (|.(B - A).| ^2) by A13 ;
|.(B - C).| ^2 = (|.(B - C).| ^2) + (|.(B - A).| ^2) by A14, A2, EUCLID_6:43;
then |.(B - A).| = 0 by SQUARE_1:12;
hence contradiction by A1, EUCLID_6:42; :: thesis: verum
end;
suppose A17: B = D ; :: thesis: contradiction
now :: thesis: ( L1 _|_ L3 & B in L3 /\ L1 & C in L3 & A in L1 & B <> C & B <> A )
thus L1 _|_ L3 by A7; :: thesis: ( B in L3 /\ L1 & C in L3 & A in L1 & B <> C & B <> A )
thus B in L3 /\ L1 by A17, A8, TARSKI:def 1; :: thesis: ( C in L3 & A in L1 & B <> C & B <> A )
thus ( C in L3 & A in L1 ) by A6, A4, RLTOPSP1:72; :: thesis: ( B <> C & B <> A )
B <> C hence ( B <> C & B <> A ) by A1; :: thesis: verum
end;
then A19: ( angle (C,B,A) = PI / 2 or angle (C,B,A) = PI + (PI / 2) ) by Th38;
set z1 = |.(A - C).|;
set z2 = |.(C - B).|;
set z3 = |.(A - B).|;
|.(A - C).| ^2 = ((|.(C - B).| ^2) + (|.(A - B).| ^2)) - (((2 * |.(C - B).|) * |.(A - B).|) * (cos (angle (C,B,A)))) by EUCLID_6:7
.= (|.(C - B).| ^2) + (|.(A - B).| ^2) by A19, SIN_COS:77 ;
then |.(A - C).| ^2 = (|.(A - C).| ^2) + (|.(A - B).| ^2) by A2, EUCLID_6:43;
then |.(A - B).| = 0 by SQUARE_1:12;
hence contradiction by A1, EUCLID_6:42; :: thesis: verum
end;
end;
end;
A20: ( L1 _|_ L3 & D in L1 /\ L3 & A in L1 & C in L3 & A <> D & C <> D ) by A7, A8, TARSKI:def 1, A4, RLTOPSP1:72, A6, A10;
A21: ( L1 _|_ L3 & D in L1 /\ L3 & B in L1 & C in L3 & B <> D & C <> D ) by A7, A8, TARSKI:def 1, A4, RLTOPSP1:72, A6, A10;
set a1 = |.(A - D).|;
set b1 = |.(C - D).|;
set c1 = |.(C - A).|;
A22: |.(C - A).| ^2 = ((|.(A - D).| ^2) + (|.(C - D).| ^2)) - (((2 * |.(A - D).|) * |.(C - D).|) * (cos (angle (A,D,C)))) by EUCLID_6:7
.= ((|.(A - D).| ^2) + (|.(C - D).| ^2)) - (((2 * |.(A - D).|) * |.(C - D).|) * 0) by A20, SIN_COS:77, Th38
.= (|.(A - D).| ^2) + (|.(C - D).| ^2) ;
set a2 = |.(B - D).|;
set b2 = |.(C - D).|;
set c2 = |.(C - B).|;
|.(C - B).| ^2 = ((|.(B - D).| ^2) + (|.(C - D).| ^2)) - (((2 * |.(B - D).|) * |.(C - D).|) * (cos (angle (B,D,C)))) by EUCLID_6:7
.= ((|.(B - D).| ^2) + (|.(C - D).| ^2)) - (((2 * |.(B - D).|) * |.(C - D).|) * 0) by A21, Th38, SIN_COS:77
.= (|.(B - D).| ^2) + (|.(C - D).| ^2) ;
then A23: (|.(A - D).| ^2) + (|.(C - D).| ^2) = (|.(B - D).| ^2) + (|.(C - D).| ^2) by A2, A22;
now :: thesis: not |.(A - D).| = - |.(B - D).|
assume |.(A - D).| = - |.(B - D).| ; :: thesis: contradiction
then - (- |.(B - D).|) <= - 0 ;
then |.(B - D).| = 0 ;
hence contradiction by A10, EUCLID_6:42; :: thesis: verum
end;
then ( D in L1 & |.(A - D).| = |.(B - D).| ) by SQUARE_1:40, A9, A23, XBOOLE_0:def 4;
then ( D in LSeg (A,B) & |.(A - D).| = |.(B - D).| ) by A4, Th42;
then ( D = the_midpoint_of_the_segment (A,B) & D in L3 ) by Th28, A9, XBOOLE_0:def 4;
hence contradiction by A3, A6, A1, A4, A7, Th44; :: thesis: verum