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;

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;

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

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 )

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;assume
( A = D or C = D or B = D )
; :: thesis: contradiction

end;per cases then
( A = D or C = D or B = D )
;

end;

suppose A11:
A = D
; :: thesis: contradiction

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;

now :: thesis: ( L1 _|_ L3 & A in L3 /\ L1 & C in L3 & B in L1 & A <> C & B <> A )

then A13:
cos (angle (C,A,B)) = 0
by SIN_COS:77, Th38;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

end;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

proof

hence
( A <> C & B <> A )
by A1; :: thesis: verum
assume A12:
A = C
; :: thesis: contradiction

then |.(C - B).| = 0 by A2, EUCLID_6:42;

hence contradiction by A12, A1, EUCLID_6:42; :: thesis: verum

end;then |.(C - B).| = 0 by A2, EUCLID_6:42;

hence contradiction by A12, A1, EUCLID_6:42; :: thesis: verum

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

suppose
C = D
; :: thesis: contradiction

then
C in L1 /\ L3
by A8, TARSKI:def 1;

then A15: C in Line (A,B) by A4, XBOOLE_0:def 4;

A16: |.(A - C).| = |.(C - B).| by A2, EUCLID_6:43

.= |.(B - C).| by EUCLID_6:43 ;

then C in LSeg (A,B) by A15, Th42;

then C = the_midpoint_of_the_segment (A,B) by A16, Th28;

hence contradiction by A3, A1, Th43; :: thesis: verum

end;then A15: C in Line (A,B) by A4, XBOOLE_0:def 4;

A16: |.(A - C).| = |.(C - B).| by A2, EUCLID_6:43

.= |.(B - C).| by EUCLID_6:43 ;

then C in LSeg (A,B) by A15, Th42;

then C = the_midpoint_of_the_segment (A,B) by A16, Th28;

hence contradiction by A3, A1, Th43; :: thesis: verum

suppose A17:
B = D
; :: thesis: contradiction

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;

now :: thesis: ( L1 _|_ L3 & B in L3 /\ L1 & C in L3 & A in L1 & B <> C & B <> A )

then A19:
( angle (C,B,A) = PI / 2 or angle (C,B,A) = PI + (PI / 2) )
by Th38;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

end;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

proof

hence
( B <> C & B <> A )
by A1; :: thesis: verum
assume A18:
B = C
; :: thesis: contradiction

then |.(C - A).| = 0 by A2, EUCLID_6:42;

hence contradiction by A18, A1, EUCLID_6:42; :: thesis: verum

end;then |.(C - A).| = 0 by A2, EUCLID_6:42;

hence contradiction by A18, A1, EUCLID_6:42; :: thesis: verum

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

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).|

then
( D in L1 & |.(A - D).| = |.(B - D).| )
by SQUARE_1:40, A9, A23, XBOOLE_0:def 4;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 - (- |.(B - D).|) <= - 0 ;

then |.(B - D).| = 0 ;

hence contradiction by A10, EUCLID_6:42; :: thesis: verum

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