:: by Roland Coghetto

::

:: Received December 30, 2015

:: Copyright (c) 2015-2021 Association of Mizar Users

Lm1: for n being Nat

for lambda being Real

for x1 being Element of REAL n holds (1 - lambda) * x1 = x1 - (lambda * x1)

proof end;

Lm2: for a being Real holds sin (a - PI) = - (sin a)

proof end;

theorem Th1: :: EUCLID12:1

for n being Nat

for lambda, mu being Real

for x1, x2 being Element of REAL n

for An, Bn being Point of (TOP-REAL n) st An = ((1 - lambda) * x1) + (lambda * x2) & Bn = ((1 - mu) * x1) + (mu * x2) holds

Bn - An = (mu - lambda) * (x2 - x1)

for lambda, mu being Real

for x1, x2 being Element of REAL n

for An, Bn being Point of (TOP-REAL n) st An = ((1 - lambda) * x1) + (lambda * x2) & Bn = ((1 - mu) * x1) + (mu * x2) holds

Bn - An = (mu - lambda) * (x2 - x1)

proof end;

theorem Th4: :: EUCLID12:4

for n being Nat

for An, Bn being Point of (TOP-REAL n)

for PAn, PBn being Element of REAL n st An = PAn & Bn = PBn holds

Line (An,Bn) = Line (PAn,PBn)

for An, Bn being Point of (TOP-REAL n)

for PAn, PBn being Element of REAL n st An = PAn & Bn = PBn holds

Line (An,Bn) = Line (PAn,PBn)

proof end;

theorem Th5: :: EUCLID12:5

for n being Nat

for An, Bn, Cn being Point of (TOP-REAL n)

for Ln being Element of line_of_REAL n st An <> Cn & Cn in LSeg (An,Bn) & An in Ln & Cn in Ln & Ln is being_line holds

Bn in Ln

for An, Bn, Cn being Point of (TOP-REAL n)

for Ln being Element of line_of_REAL n st An <> Cn & Cn in LSeg (An,Bn) & An in Ln & Cn in Ln & Ln is being_line holds

Bn in Ln

proof end;

:: deftheorem defines being_point EUCLID12:def 1 :

for n being Nat

for S being Subset of (REAL n) holds

( S is being_point iff ex Pn being Element of REAL n st S = {Pn} );

for n being Nat

for S being Subset of (REAL n) holds

( S is being_point iff ex Pn being Element of REAL n st S = {Pn} );

theorem Th6: :: EUCLID12:6

for n being Nat

for Ln being Element of line_of_REAL n holds

( Ln is being_line or ex Pn being Element of REAL n st Ln = {Pn} )

for Ln being Element of line_of_REAL n holds

( Ln is being_line or ex Pn being Element of REAL n st Ln = {Pn} )

proof end;

theorem :: EUCLID12:7

for n being Nat

for Ln being Element of line_of_REAL n holds

( Ln is being_line or Ln is being_point ) by Th6;

for Ln being Element of line_of_REAL n holds

( Ln is being_line or Ln is being_point ) by Th6;

theorem Th7: :: EUCLID12:8

for n being Nat

for Ln being Element of line_of_REAL n st Ln is being_line holds

for Pn being Element of REAL n holds not Ln = {Pn}

for Ln being Element of line_of_REAL n st Ln is being_line holds

for Pn being Element of REAL n holds not Ln = {Pn}

proof end;

theorem :: EUCLID12:9

for n being Nat

for Ln being Element of line_of_REAL n st Ln is being_line holds

not Ln is being_point by Th7;

for Ln being Element of line_of_REAL n st Ln is being_line holds

not Ln is being_point by Th7;

theorem Th8: :: EUCLID12:10

for A, B, C being Point of (TOP-REAL 2) st C in LSeg (A,B) holds

|.(A - B).| = |.(A - C).| + |.(C - B).|

|.(A - B).| = |.(A - C).| + |.(C - B).|

proof end;

theorem Th9: :: EUCLID12:11

for A, B, C being Point of (TOP-REAL 2) st |.(A - B).| = |.(A - C).| + |.(C - B).| holds

C in LSeg (A,B)

C in LSeg (A,B)

proof end;

theorem Th10: :: EUCLID12:12

for p, q1, q2 being Point of (TOP-REAL 2) holds

( p in LSeg (q1,q2) iff (dist (q1,p)) + (dist (p,q2)) = dist (q1,q2) )

( p in LSeg (q1,q2) iff (dist (q1,p)) + (dist (p,q2)) = dist (q1,q2) )

proof end;

theorem Th11: :: EUCLID12:13

for A, B, C being Point of (TOP-REAL 2)

for p, q, r being Element of (Euclid 2) st p,q,r are_mutually_distinct & p = A & q = B & r = C holds

( A in LSeg (B,C) iff p is_between q,r )

for p, q, r being Element of (Euclid 2) st p,q,r are_mutually_distinct & p = A & q = B & r = C holds

( A in LSeg (B,C) iff p is_between q,r )

proof end;

theorem :: EUCLID12:14

for A, B, C being Point of (TOP-REAL 2)

for p, q, r being Element of (Euclid 2) st p,q,r are_mutually_distinct & p = A & q = B & r = C holds

( A in LSeg (B,C) iff p is_Between q,r )

for p, q, r being Element of (Euclid 2) st p,q,r are_mutually_distinct & p = A & q = B & r = C holds

( A in LSeg (B,C) iff p is_Between q,r )

proof end;

theorem Th12: :: EUCLID12:15

for OO, Ox, Oy being Element of REAL 2 st OO = |[0,0]| & Ox = |[1,0]| & Oy = |[0,1]| holds

REAL 2 = plane (OO,Ox,Oy)

REAL 2 = plane (OO,Ox,Oy)

proof end;

theorem :: EUCLID12:19

for L1 being Element of line_of_REAL 2 ex L being Element of line_of_REAL 2 st

( L is being_point & L misses L1 )

( L is being_point & L misses L1 )

proof end;

theorem Th16: :: EUCLID12:20

for L1, L2 being Element of line_of_REAL 2 holds

( L1 // L2 or ex x being Element of REAL 2 st

( L1 = {x} or L2 = {x} ) or ( L1 is being_line & L2 is being_line & ex x being Element of REAL 2 st L1 /\ L2 = {x} ) )

( L1 // L2 or ex x being Element of REAL 2 st

( L1 = {x} or L2 = {x} ) or ( L1 is being_line & L2 is being_line & ex x being Element of REAL 2 st L1 /\ L2 = {x} ) )

proof end;

theorem :: EUCLID12:21

for L1, L2 being Element of line_of_REAL 2 holds

( L1 // L2 or L1 is being_point or L2 is being_point or ( L1 is being_line & L2 is being_line & L1 /\ L2 is being_point ) ) by Th16;

( L1 // L2 or L1 is being_point or L2 is being_point or ( L1 is being_line & L2 is being_line & L1 /\ L2 is being_point ) ) by Th16;

theorem Th17: :: EUCLID12:22

for A being Point of (TOP-REAL 2)

for L1, L2 being Element of line_of_REAL 2 st L1 /\ L2 is being_point & A in L1 /\ L2 holds

L1 /\ L2 = {A} by TARSKI:def 1;

for L1, L2 being Element of line_of_REAL 2 st L1 /\ L2 is being_point & A in L1 /\ L2 holds

L1 /\ L2 = {A} by TARSKI:def 1;

definition
end;

:: deftheorem defines half_length EUCLID12:def 2 :

for A, B being Point of (TOP-REAL 2) holds half_length (A,B) = (1 / 2) * |.(A - B).|;

for A, B being Point of (TOP-REAL 2) holds half_length (A,B) = (1 / 2) * |.(A - B).|;

theorem :: EUCLID12:23

theorem Th19: :: EUCLID12:26

for A, B being Point of (TOP-REAL 2) ex C being Point of (TOP-REAL 2) st

( C in LSeg (A,B) & |.(A - C).| = (1 / 2) * |.(A - B).| )

( C in LSeg (A,B) & |.(A - C).| = (1 / 2) * |.(A - B).| )

proof end;

theorem Th20: :: EUCLID12:27

for A, B, C, D being Point of (TOP-REAL 2) st |.(A - B).| = |.(A - C).| & B in LSeg (A,D) & C in LSeg (A,D) holds

B = C

B = C

proof end;

definition

let A, B be Point of (TOP-REAL 2);

ex b_{1}, C being Point of (TOP-REAL 2) st

( C in LSeg (A,B) & b_{1} = C & |.(A - C).| = half_length (A,B) )

for b_{1}, b_{2} being Point of (TOP-REAL 2) st ex C being Point of (TOP-REAL 2) st

( C in LSeg (A,B) & b_{1} = C & |.(A - C).| = half_length (A,B) ) & ex C being Point of (TOP-REAL 2) st

( C in LSeg (A,B) & b_{2} = C & |.(A - C).| = half_length (A,B) ) holds

b_{1} = b_{2}
by Th20;

end;
func the_midpoint_of_the_segment (A,B) -> Point of (TOP-REAL 2) means :Def1: :: EUCLID12:def 3

ex C being Point of (TOP-REAL 2) st

( C in LSeg (A,B) & it = C & |.(A - C).| = half_length (A,B) );

existence ex C being Point of (TOP-REAL 2) st

( C in LSeg (A,B) & it = C & |.(A - C).| = half_length (A,B) );

ex b

( C in LSeg (A,B) & b

proof end;

uniqueness for b

( C in LSeg (A,B) & b

( C in LSeg (A,B) & b

b

:: deftheorem Def1 defines the_midpoint_of_the_segment EUCLID12:def 3 :

for A, B, b_{3} being Point of (TOP-REAL 2) holds

( b_{3} = the_midpoint_of_the_segment (A,B) iff ex C being Point of (TOP-REAL 2) st

( C in LSeg (A,B) & b_{3} = C & |.(A - C).| = half_length (A,B) ) );

for A, B, b

( b

( C in LSeg (A,B) & b

theorem Th23: :: EUCLID12:30

for A, B being Point of (TOP-REAL 2) holds the_midpoint_of_the_segment (A,B) = the_midpoint_of_the_segment (B,A)

proof end;

theorem Th27: :: EUCLID12:34

for A, B, C being Point of (TOP-REAL 2) st C in LSeg (A,B) & |.(A - C).| = |.(B - C).| holds

half_length (A,B) = |.(A - C).|

half_length (A,B) = |.(A - C).|

proof end;

theorem Th28: :: EUCLID12:35

for A, B, C being Point of (TOP-REAL 2) st C in LSeg (A,B) & |.(A - C).| = |.(B - C).| holds

C = the_midpoint_of_the_segment (A,B)

C = the_midpoint_of_the_segment (A,B)

proof end;

theorem :: EUCLID12:36

for A, B being Point of (TOP-REAL 2) holds |.(A - (the_midpoint_of_the_segment (A,B))).| = |.((the_midpoint_of_the_segment (A,B)) - B).|

proof end;

theorem Th29: :: EUCLID12:37

for A, B, C being Point of (TOP-REAL 2)

for r being Real st A <> B & r is positive & r <> 1 & |.(A - C).| = r * |.(A - B).| holds

A,B,C are_mutually_distinct

for r being Real st A <> B & r is positive & r <> 1 & |.(A - C).| = r * |.(A - B).| holds

A,B,C are_mutually_distinct

proof end;

theorem Th30: :: EUCLID12:38

for A, B, C being Point of (TOP-REAL 2) st C in LSeg (A,B) & |.(A - C).| = (1 / 2) * |.(A - B).| holds

|.(B - C).| = (1 / 2) * |.(A - B).|

|.(B - C).| = (1 / 2) * |.(A - B).|

proof end;

theorem :: EUCLID12:40

theorem :: EUCLID12:41

for L1, L2 being Element of line_of_REAL 2 st L1 is being_line & L2 is being_line & L1 misses L2 holds

L1 // L2 by Th31, EUCLIDLP:113;

L1 // L2 by Th31, EUCLIDLP:113;

theorem Th32: :: EUCLID12:42

for L1, L2 being Element of line_of_REAL 2 st L1 <> L2 & L1 meets L2 & ( for x being Element of REAL 2 holds

( not L1 = {x} & not L2 = {x} ) ) holds

( L1 is being_line & L2 is being_line & ex x being Element of REAL 2 st L1 /\ L2 = {x} )

( not L1 = {x} & not L2 = {x} ) ) holds

( L1 is being_line & L2 is being_line & ex x being Element of REAL 2 st L1 /\ L2 = {x} )

proof end;

theorem Th33: :: EUCLID12:43

for L1, L2 being Element of line_of_REAL 2 st L1 _|_ L2 holds

ex x being Element of REAL 2 st L1 /\ L2 = {x}

ex x being Element of REAL 2 st L1 /\ L2 = {x}

proof end;

theorem :: EUCLID12:44

theorem :: EUCLID12:46

for L1, L2 being Element of line_of_REAL 2 st L1 is being_line & L2 is being_line & L1 // L2 holds

not L1 _|_ L2 by Th34;

not L1 _|_ L2 by Th34;

theorem Th35: :: EUCLID12:47

for x being Element of REAL 2

for L1 being Element of line_of_REAL 2 st L1 is being_line holds

ex L2 being Element of line_of_REAL 2 st

( x in L2 & L1 _|_ L2 )

for L1 being Element of line_of_REAL 2 st L1 is being_line holds

ex L2 being Element of line_of_REAL 2 st

( x in L2 & L1 _|_ L2 )

proof end;

theorem Th36: :: EUCLID12:48

for A, B, C being Point of (TOP-REAL 2)

for L1, L2 being Element of line_of_REAL 2

for D being Point of (TOP-REAL 2) st L1 _|_ L2 & L1 = Line (A,B) & L2 = Line (C,D) holds

|((B - A),(D - C))| = 0

for L1, L2 being Element of line_of_REAL 2

for D being Point of (TOP-REAL 2) st L1 _|_ L2 & L1 = Line (A,B) & L2 = Line (C,D) holds

|((B - A),(D - C))| = 0

proof end;

theorem Th37: :: EUCLID12:49

for A, B being Point of (TOP-REAL 2)

for L being Element of line_of_REAL 2 st L is being_line & A in L & B in L & A <> B holds

L = Line (A,B)

for L being Element of line_of_REAL 2 st L is being_line & A in L & B in L & A <> B holds

L = Line (A,B)

proof end;

theorem Th38: :: EUCLID12:50

for A, B, C being Point of (TOP-REAL 2)

for L1, L2 being Element of line_of_REAL 2 st L1 _|_ L2 & C in L1 /\ L2 & A in L1 & B in L2 & A <> C & B <> C & not angle (A,C,B) = PI / 2 holds

angle (A,C,B) = (3 * PI) / 2

for L1, L2 being Element of line_of_REAL 2 st L1 _|_ L2 & C in L1 /\ L2 & A in L1 & B in L2 & A <> C & B <> C & not angle (A,C,B) = PI / 2 holds

angle (A,C,B) = (3 * PI) / 2

proof end;

theorem :: EUCLID12:51

for A, B, C being Point of (TOP-REAL 2)

for L1, L2 being Element of line_of_REAL 2 st L1 _|_ L2 & C in L1 /\ L2 & A in L1 & B in L2 & A <> C & B <> C holds

A,B,C is_a_triangle

for L1, L2 being Element of line_of_REAL 2 st L1 _|_ L2 & C in L1 /\ L2 & A in L1 & B in L2 & A <> C & B <> C holds

A,B,C is_a_triangle

proof end;

theorem Th39: :: EUCLID12:52

for A, B, C being Point of (TOP-REAL 2)

for L1 being Element of line_of_REAL 2 st A <> B & L1 = Line (A,B) & C in LSeg (A,B) & |.(A - C).| = (1 / 2) * |.(A - B).| holds

ex L2 being Element of line_of_REAL 2 st

( C in L2 & L1 _|_ L2 )

for L1 being Element of line_of_REAL 2 st A <> B & L1 = Line (A,B) & C in LSeg (A,B) & |.(A - C).| = (1 / 2) * |.(A - B).| holds

ex L2 being Element of line_of_REAL 2 st

( C in L2 & L1 _|_ L2 )

proof end;

definition

let A, B be Element of (TOP-REAL 2);

assume A1: A <> B ;

ex b_{1}, L1, L2 being Element of line_of_REAL 2 st

( b_{1} = L2 & L1 = Line (A,B) & L1 _|_ L2 & L1 /\ L2 = {(the_midpoint_of_the_segment (A,B))} )

for b_{1}, b_{2} being Element of line_of_REAL 2 st ex L1, L2 being Element of line_of_REAL 2 st

( b_{1} = L2 & L1 = Line (A,B) & L1 _|_ L2 & L1 /\ L2 = {(the_midpoint_of_the_segment (A,B))} ) & ex L1, L2 being Element of line_of_REAL 2 st

( b_{2} = L2 & L1 = Line (A,B) & L1 _|_ L2 & L1 /\ L2 = {(the_midpoint_of_the_segment (A,B))} ) holds

b_{1} = b_{2}

end;
assume A1: A <> B ;

func the_perpendicular_bisector (A,B) -> Element of line_of_REAL 2 means :Def2: :: EUCLID12:def 4

ex L1, L2 being Element of line_of_REAL 2 st

( it = L2 & L1 = Line (A,B) & L1 _|_ L2 & L1 /\ L2 = {(the_midpoint_of_the_segment (A,B))} );

existence ex L1, L2 being Element of line_of_REAL 2 st

( it = L2 & L1 = Line (A,B) & L1 _|_ L2 & L1 /\ L2 = {(the_midpoint_of_the_segment (A,B))} );

ex b

( b

proof end;

uniqueness for b

( b

( b

b

proof end;

:: deftheorem Def2 defines the_perpendicular_bisector EUCLID12:def 4 :

for A, B being Element of (TOP-REAL 2) st A <> B holds

for b_{3} being Element of line_of_REAL 2 holds

( b_{3} = the_perpendicular_bisector (A,B) iff ex L1, L2 being Element of line_of_REAL 2 st

( b_{3} = L2 & L1 = Line (A,B) & L1 _|_ L2 & L1 /\ L2 = {(the_midpoint_of_the_segment (A,B))} ) );

for A, B being Element of (TOP-REAL 2) st A <> B holds

for b

( b

( b

theorem :: EUCLID12:54

for A, B being Point of (TOP-REAL 2) st A <> B holds

the_perpendicular_bisector (A,B) = the_perpendicular_bisector (B,A)

the_perpendicular_bisector (A,B) = the_perpendicular_bisector (B,A)

proof end;

theorem Th40: :: EUCLID12:55

for A, B, C being Point of (TOP-REAL 2)

for L1, L2 being Element of line_of_REAL 2

for D being Point of (TOP-REAL 2) st A <> B & L1 = Line (A,B) & C in LSeg (A,B) & |.(A - C).| = (1 / 2) * |.(A - B).| & C in L2 & L1 _|_ L2 & D in L2 holds

|.(D - A).| = |.(D - B).|

for L1, L2 being Element of line_of_REAL 2

for D being Point of (TOP-REAL 2) st A <> B & L1 = Line (A,B) & C in LSeg (A,B) & |.(A - C).| = (1 / 2) * |.(A - B).| & C in L2 & L1 _|_ L2 & D in L2 holds

|.(D - A).| = |.(D - B).|

proof end;

theorem Th41: :: EUCLID12:56

for A, B, C being Point of (TOP-REAL 2) st A <> B & C in the_perpendicular_bisector (A,B) holds

|.(C - A).| = |.(C - B).|

|.(C - A).| = |.(C - B).|

proof end;

theorem Th42: :: EUCLID12:57

for A, B, C being Point of (TOP-REAL 2) st C in Line (A,B) & |.(A - C).| = |.(B - C).| holds

C in LSeg (A,B)

C in LSeg (A,B)

proof end;

theorem Th43: :: EUCLID12:58

for A, B being Point of (TOP-REAL 2) st A <> B holds

the_midpoint_of_the_segment (A,B) in the_perpendicular_bisector (A,B)

the_midpoint_of_the_segment (A,B) in the_perpendicular_bisector (A,B)

proof end;

theorem Th44: :: EUCLID12:59

for A, B being Point of (TOP-REAL 2)

for L1, L2 being Element of line_of_REAL 2 st A <> B & L1 = Line (A,B) & L1 _|_ L2 & the_midpoint_of_the_segment (A,B) in L2 holds

L2 = the_perpendicular_bisector (A,B)

for L1, L2 being Element of line_of_REAL 2 st A <> B & L1 = Line (A,B) & L1 _|_ L2 & the_midpoint_of_the_segment (A,B) in L2 holds

L2 = the_perpendicular_bisector (A,B)

proof end;

theorem Th45: :: EUCLID12:60

for A, B, C being Point of (TOP-REAL 2) st A <> B & |.(C - A).| = |.(C - B).| holds

C in the_perpendicular_bisector (A,B)

C in the_perpendicular_bisector (A,B)

proof end;

theorem Th46: :: EUCLID12:61

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds

(the_perpendicular_bisector (A,B)) /\ (the_perpendicular_bisector (B,C)) is being_point

(the_perpendicular_bisector (A,B)) /\ (the_perpendicular_bisector (B,C)) is being_point

proof end;

theorem Th47: :: EUCLID12:62

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds

ex D being Point of (TOP-REAL 2) st

( (the_perpendicular_bisector (A,B)) /\ (the_perpendicular_bisector (B,C)) = {D} & (the_perpendicular_bisector (B,C)) /\ (the_perpendicular_bisector (C,A)) = {D} & (the_perpendicular_bisector (C,A)) /\ (the_perpendicular_bisector (A,B)) = {D} & |.(D - A).| = |.(D - B).| & |.(D - A).| = |.(D - C).| & |.(D - B).| = |.(D - C).| )

ex D being Point of (TOP-REAL 2) st

( (the_perpendicular_bisector (A,B)) /\ (the_perpendicular_bisector (B,C)) = {D} & (the_perpendicular_bisector (B,C)) /\ (the_perpendicular_bisector (C,A)) = {D} & (the_perpendicular_bisector (C,A)) /\ (the_perpendicular_bisector (A,B)) = {D} & |.(D - A).| = |.(D - B).| & |.(D - A).| = |.(D - C).| & |.(D - B).| = |.(D - C).| )

proof end;

definition

let A, B, C be Point of (TOP-REAL 2);

assume A1: A,B,C is_a_triangle ;

ex b_{1} being Point of (TOP-REAL 2) st

( (the_perpendicular_bisector (A,B)) /\ (the_perpendicular_bisector (B,C)) = {b_{1}} & (the_perpendicular_bisector (B,C)) /\ (the_perpendicular_bisector (C,A)) = {b_{1}} & (the_perpendicular_bisector (C,A)) /\ (the_perpendicular_bisector (A,B)) = {b_{1}} )

for b_{1}, b_{2} being Point of (TOP-REAL 2) st (the_perpendicular_bisector (A,B)) /\ (the_perpendicular_bisector (B,C)) = {b_{1}} & (the_perpendicular_bisector (B,C)) /\ (the_perpendicular_bisector (C,A)) = {b_{1}} & (the_perpendicular_bisector (C,A)) /\ (the_perpendicular_bisector (A,B)) = {b_{1}} & (the_perpendicular_bisector (A,B)) /\ (the_perpendicular_bisector (B,C)) = {b_{2}} & (the_perpendicular_bisector (B,C)) /\ (the_perpendicular_bisector (C,A)) = {b_{2}} & (the_perpendicular_bisector (C,A)) /\ (the_perpendicular_bisector (A,B)) = {b_{2}} holds

b_{1} = b_{2}
by ZFMISC_1:3;

end;
assume A1: A,B,C is_a_triangle ;

func the_circumcenter (A,B,C) -> Point of (TOP-REAL 2) means :Def3: :: EUCLID12:def 5

( (the_perpendicular_bisector (A,B)) /\ (the_perpendicular_bisector (B,C)) = {it} & (the_perpendicular_bisector (B,C)) /\ (the_perpendicular_bisector (C,A)) = {it} & (the_perpendicular_bisector (C,A)) /\ (the_perpendicular_bisector (A,B)) = {it} );

existence ( (the_perpendicular_bisector (A,B)) /\ (the_perpendicular_bisector (B,C)) = {it} & (the_perpendicular_bisector (B,C)) /\ (the_perpendicular_bisector (C,A)) = {it} & (the_perpendicular_bisector (C,A)) /\ (the_perpendicular_bisector (A,B)) = {it} );

ex b

( (the_perpendicular_bisector (A,B)) /\ (the_perpendicular_bisector (B,C)) = {b

proof end;

uniqueness for b

b

:: deftheorem Def3 defines the_circumcenter EUCLID12:def 5 :

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds

for b_{4} being Point of (TOP-REAL 2) holds

( b_{4} = the_circumcenter (A,B,C) iff ( (the_perpendicular_bisector (A,B)) /\ (the_perpendicular_bisector (B,C)) = {b_{4}} & (the_perpendicular_bisector (B,C)) /\ (the_perpendicular_bisector (C,A)) = {b_{4}} & (the_perpendicular_bisector (C,A)) /\ (the_perpendicular_bisector (A,B)) = {b_{4}} ) );

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds

for b

( b

definition

let A, B, C be Point of (TOP-REAL 2);

assume A,B,C is_a_triangle ;

coherence

|.((the_circumcenter (A,B,C)) - A).| is Real;

;

end;
assume A,B,C is_a_triangle ;

func the_radius_of_the_circumcircle (A,B,C) -> Real equals :Def4: :: EUCLID12:def 6

|.((the_circumcenter (A,B,C)) - A).|;

correctness |.((the_circumcenter (A,B,C)) - A).|;

coherence

|.((the_circumcenter (A,B,C)) - A).| is Real;

;

:: deftheorem Def4 defines the_radius_of_the_circumcircle EUCLID12:def 6 :

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds

the_radius_of_the_circumcircle (A,B,C) = |.((the_circumcenter (A,B,C)) - A).|;

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds

the_radius_of_the_circumcircle (A,B,C) = |.((the_circumcenter (A,B,C)) - A).|;

theorem Th48: :: EUCLID12:63

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds

ex a, b, r being Real st

( A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) )

ex a, b, r being Real st

( A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) )

proof end;

theorem Th49: :: EUCLID12:64

for a being Real

for A, B, C being Point of (TOP-REAL 2)

for b, r being Real st A,B,C is_a_triangle & A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) holds

( |[a,b]| = the_circumcenter (A,B,C) & r = |.((the_circumcenter (A,B,C)) - A).| )

for A, B, C being Point of (TOP-REAL 2)

for b, r being Real st A,B,C is_a_triangle & A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) holds

( |[a,b]| = the_circumcenter (A,B,C) & r = |.((the_circumcenter (A,B,C)) - A).| )

proof end;

theorem :: EUCLID12:65

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds

the_radius_of_the_circumcircle (A,B,C) > 0

the_radius_of_the_circumcircle (A,B,C) > 0

proof end;

theorem Th50: :: EUCLID12:66

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds

( |.((the_circumcenter (A,B,C)) - A).| = |.((the_circumcenter (A,B,C)) - B).| & |.((the_circumcenter (A,B,C)) - A).| = |.((the_circumcenter (A,B,C)) - C).| & |.((the_circumcenter (A,B,C)) - B).| = |.((the_circumcenter (A,B,C)) - C).| )

( |.((the_circumcenter (A,B,C)) - A).| = |.((the_circumcenter (A,B,C)) - B).| & |.((the_circumcenter (A,B,C)) - A).| = |.((the_circumcenter (A,B,C)) - C).| & |.((the_circumcenter (A,B,C)) - B).| = |.((the_circumcenter (A,B,C)) - C).| )

proof end;

theorem :: EUCLID12:67

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds

( the_radius_of_the_circumcircle (A,B,C) = |.((the_circumcenter (A,B,C)) - B).| & the_radius_of_the_circumcircle (A,B,C) = |.((the_circumcenter (A,B,C)) - C).| )

( the_radius_of_the_circumcircle (A,B,C) = |.((the_circumcenter (A,B,C)) - B).| & the_radius_of_the_circumcircle (A,B,C) = |.((the_circumcenter (A,B,C)) - C).| )

proof end;

theorem :: EUCLID12:68

for a being Real

for A, B, C being Point of (TOP-REAL 2)

for b, c, d, r, s being Real st A,B,C is_a_triangle & A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) & A in circle (c,d,s) & B in circle (c,d,s) & C in circle (c,d,s) holds

( a = c & b = d & r = s )

for A, B, C being Point of (TOP-REAL 2)

for b, c, d, r, s being Real st A,B,C is_a_triangle & A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) & A in circle (c,d,s) & B in circle (c,d,s) & C in circle (c,d,s) holds

( a = c & b = d & r = s )

proof end;

theorem Th51: :: EUCLID12:70

for a being Real

for A, B, C, D being Point of (TOP-REAL 2)

for b, r being Real st A,B,C is_a_triangle & A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) & A,B,D is_a_triangle & A in circle (a,b,r) & B in circle (a,b,r) & D in circle (a,b,r) & C <> D & not the_diameter_of_the_circumcircle (A,B,C) = the_diameter_of_the_circumcircle (D,B,C) holds

the_diameter_of_the_circumcircle (A,B,C) = - (the_diameter_of_the_circumcircle (D,B,C))

for A, B, C, D being Point of (TOP-REAL 2)

for b, r being Real st A,B,C is_a_triangle & A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) & A,B,D is_a_triangle & A in circle (a,b,r) & B in circle (a,b,r) & D in circle (a,b,r) & C <> D & not the_diameter_of_the_circumcircle (A,B,C) = the_diameter_of_the_circumcircle (D,B,C) holds

the_diameter_of_the_circumcircle (A,B,C) = - (the_diameter_of_the_circumcircle (D,B,C))

proof end;

theorem Th52: :: EUCLID12:71

for a being Real

for A, B, C being Point of (TOP-REAL 2)

for b, r being Real st A,B,C is_a_triangle & A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) & not the_diameter_of_the_circumcircle (A,B,C) = 2 * r holds

the_diameter_of_the_circumcircle (A,B,C) = - (2 * r)

for A, B, C being Point of (TOP-REAL 2)

for b, r being Real st A,B,C is_a_triangle & A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) & not the_diameter_of_the_circumcircle (A,B,C) = 2 * r holds

the_diameter_of_the_circumcircle (A,B,C) = - (2 * r)

proof end;

theorem Th53: :: EUCLID12:72

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle & 0 < angle (C,B,A) & angle (C,B,A) < PI holds

the_diameter_of_the_circumcircle (A,B,C) > 0

the_diameter_of_the_circumcircle (A,B,C) > 0

proof end;

theorem Th54: :: EUCLID12:73

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle & PI < angle (C,B,A) & angle (C,B,A) < 2 * PI holds

the_diameter_of_the_circumcircle (A,B,C) < 0

the_diameter_of_the_circumcircle (A,B,C) < 0

proof end;

theorem Th55: :: EUCLID12:74

for a being Real

for A, B, C being Point of (TOP-REAL 2)

for b, r being Real st A,B,C is_a_triangle & 0 < angle (C,B,A) & angle (C,B,A) < PI & A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) holds

the_diameter_of_the_circumcircle (A,B,C) = 2 * r

for A, B, C being Point of (TOP-REAL 2)

for b, r being Real st A,B,C is_a_triangle & 0 < angle (C,B,A) & angle (C,B,A) < PI & A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) holds

the_diameter_of_the_circumcircle (A,B,C) = 2 * r

proof end;

theorem Th56: :: EUCLID12:75

for a being Real

for A, B, C being Point of (TOP-REAL 2)

for b, r being Real st A,B,C is_a_triangle & PI < angle (C,B,A) & angle (C,B,A) < 2 * PI & A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) holds

the_diameter_of_the_circumcircle (A,B,C) = - (2 * r)

for A, B, C being Point of (TOP-REAL 2)

for b, r being Real st A,B,C is_a_triangle & PI < angle (C,B,A) & angle (C,B,A) < 2 * PI & A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) holds

the_diameter_of_the_circumcircle (A,B,C) = - (2 * r)

proof end;

theorem Th57: :: EUCLID12:76

for a being Real

for A, B, C being Point of (TOP-REAL 2)

for b, r being Real st A,B,C is_a_triangle & 0 < angle (C,B,A) & angle (C,B,A) < PI & A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) holds

( |.(A - B).| = (2 * r) * (sin (angle (A,C,B))) & |.(B - C).| = (2 * r) * (sin (angle (B,A,C))) & |.(C - A).| = (2 * r) * (sin (angle (C,B,A))) )

for A, B, C being Point of (TOP-REAL 2)

for b, r being Real st A,B,C is_a_triangle & 0 < angle (C,B,A) & angle (C,B,A) < PI & A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) holds

( |.(A - B).| = (2 * r) * (sin (angle (A,C,B))) & |.(B - C).| = (2 * r) * (sin (angle (B,A,C))) & |.(C - A).| = (2 * r) * (sin (angle (C,B,A))) )

proof end;

theorem Th58: :: EUCLID12:77

for a being Real

for A, B, C being Point of (TOP-REAL 2)

for b, r being Real st A,B,C is_a_triangle & PI < angle (C,B,A) & angle (C,B,A) < 2 * PI & A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) holds

( |.(A - B).| = - ((2 * r) * (sin (angle (A,C,B)))) & |.(B - C).| = - ((2 * r) * (sin (angle (B,A,C)))) & |.(C - A).| = - ((2 * r) * (sin (angle (C,B,A)))) )

for A, B, C being Point of (TOP-REAL 2)

for b, r being Real st A,B,C is_a_triangle & PI < angle (C,B,A) & angle (C,B,A) < 2 * PI & A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) holds

( |.(A - B).| = - ((2 * r) * (sin (angle (A,C,B)))) & |.(B - C).| = - ((2 * r) * (sin (angle (B,A,C)))) & |.(C - A).| = - ((2 * r) * (sin (angle (C,B,A)))) )

proof end;

:: Extended law of sines

theorem :: EUCLID12:78

for a being Real

for A, B, C being Point of (TOP-REAL 2)

for b, r being Real st A,B,C is_a_triangle & 0 < angle (C,B,A) & angle (C,B,A) < PI & A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) holds

( |.(A - B).| / (sin (angle (A,C,B))) = 2 * r & |.(B - C).| / (sin (angle (B,A,C))) = 2 * r & |.(C - A).| / (sin (angle (C,B,A))) = 2 * r )

for A, B, C being Point of (TOP-REAL 2)

for b, r being Real st A,B,C is_a_triangle & 0 < angle (C,B,A) & angle (C,B,A) < PI & A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) holds

( |.(A - B).| / (sin (angle (A,C,B))) = 2 * r & |.(B - C).| / (sin (angle (B,A,C))) = 2 * r & |.(C - A).| / (sin (angle (C,B,A))) = 2 * r )

proof end;

theorem :: EUCLID12:79

for a being Real

for A, B, C being Point of (TOP-REAL 2)

for b, r being Real st A,B,C is_a_triangle & PI < angle (C,B,A) & angle (C,B,A) < 2 * PI & A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) holds

( |.(A - B).| / (sin (angle (A,C,B))) = - (2 * r) & |.(B - C).| / (sin (angle (B,A,C))) = - (2 * r) & |.(C - A).| / (sin (angle (C,B,A))) = - (2 * r) )

for A, B, C being Point of (TOP-REAL 2)

for b, r being Real st A,B,C is_a_triangle & PI < angle (C,B,A) & angle (C,B,A) < 2 * PI & A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) holds

( |.(A - B).| / (sin (angle (A,C,B))) = - (2 * r) & |.(B - C).| / (sin (angle (B,A,C))) = - (2 * r) & |.(C - A).| / (sin (angle (C,B,A))) = - (2 * r) )

proof end;

theorem Th59: :: EUCLID12:80

for A, B, C, D, E, F being Point of (TOP-REAL 2) st A,B,C is_a_triangle & D = ((1 - (1 / 2)) * B) + ((1 / 2) * C) & E = ((1 - (1 / 2)) * C) + ((1 / 2) * A) & F = ((1 - (1 / 2)) * A) + ((1 / 2) * B) holds

Line (A,D), Line (B,E), Line (C,F) are_concurrent

Line (A,D), Line (B,E), Line (C,F) are_concurrent

proof end;

definition

let A, B, C be Point of (TOP-REAL 2);

Line (A,(the_midpoint_of_the_segment (B,C))) is Element of line_of_REAL 2

end;
func median (A,B,C) -> Element of line_of_REAL 2 equals :: EUCLID12:def 7

Line (A,(the_midpoint_of_the_segment (B,C)));

coherence Line (A,(the_midpoint_of_the_segment (B,C)));

Line (A,(the_midpoint_of_the_segment (B,C))) is Element of line_of_REAL 2

proof end;

:: deftheorem defines median EUCLID12:def 7 :

for A, B, C being Point of (TOP-REAL 2) holds median (A,B,C) = Line (A,(the_midpoint_of_the_segment (B,C)));

for A, B, C being Point of (TOP-REAL 2) holds median (A,B,C) = Line (A,(the_midpoint_of_the_segment (B,C)));

theorem :: EUCLID12:84

theorem Th62: :: EUCLID12:86

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds

ex D being Point of (TOP-REAL 2) st

( D in median (A,B,C) & D in median (B,C,A) & D in median (C,A,B) )

ex D being Point of (TOP-REAL 2) st

( D in median (A,B,C) & D in median (B,C,A) & D in median (C,A,B) )

proof end;

theorem Th63: :: EUCLID12:87

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds

ex D being Point of (TOP-REAL 2) st

( (median (A,B,C)) /\ (median (B,C,A)) = {D} & (median (B,C,A)) /\ (median (C,A,B)) = {D} & (median (C,A,B)) /\ (median (A,B,C)) = {D} )

ex D being Point of (TOP-REAL 2) st

( (median (A,B,C)) /\ (median (B,C,A)) = {D} & (median (B,C,A)) /\ (median (C,A,B)) = {D} & (median (C,A,B)) /\ (median (A,B,C)) = {D} )

proof end;

definition

let A, B, C be Point of (TOP-REAL 2);

assume A1: A,B,C is_a_triangle ;

ex b_{1} being Point of (TOP-REAL 2) st

( (median (A,B,C)) /\ (median (B,C,A)) = {b_{1}} & (median (B,C,A)) /\ (median (C,A,B)) = {b_{1}} & (median (C,A,B)) /\ (median (A,B,C)) = {b_{1}} )
by A1, Th63;

uniqueness

for b_{1}, b_{2} being Point of (TOP-REAL 2) st (median (A,B,C)) /\ (median (B,C,A)) = {b_{1}} & (median (B,C,A)) /\ (median (C,A,B)) = {b_{1}} & (median (C,A,B)) /\ (median (A,B,C)) = {b_{1}} & (median (A,B,C)) /\ (median (B,C,A)) = {b_{2}} & (median (B,C,A)) /\ (median (C,A,B)) = {b_{2}} & (median (C,A,B)) /\ (median (A,B,C)) = {b_{2}} holds

b_{1} = b_{2}
by ZFMISC_1:3;

end;
assume A1: A,B,C is_a_triangle ;

func the_centroid_of_the_triangle (A,B,C) -> Point of (TOP-REAL 2) means :: EUCLID12:def 8

( (median (A,B,C)) /\ (median (B,C,A)) = {it} & (median (B,C,A)) /\ (median (C,A,B)) = {it} & (median (C,A,B)) /\ (median (A,B,C)) = {it} );

existence ( (median (A,B,C)) /\ (median (B,C,A)) = {it} & (median (B,C,A)) /\ (median (C,A,B)) = {it} & (median (C,A,B)) /\ (median (A,B,C)) = {it} );

ex b

( (median (A,B,C)) /\ (median (B,C,A)) = {b

uniqueness

for b

b

:: deftheorem defines the_centroid_of_the_triangle EUCLID12:def 8 :

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds

for b_{4} being Point of (TOP-REAL 2) holds

( b_{4} = the_centroid_of_the_triangle (A,B,C) iff ( (median (A,B,C)) /\ (median (B,C,A)) = {b_{4}} & (median (B,C,A)) /\ (median (C,A,B)) = {b_{4}} & (median (C,A,B)) /\ (median (A,B,C)) = {b_{4}} ) );

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds

for b

( b