:: Circumcenter, Circumcircle, and Centroid of a Triangle
:: 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)

proof end;

theorem Th2: :: EUCLID12:2

for a being Real st |.a.| = |.(1 - a).| holds
a = 1 / 2

proof end;

theorem Th3: :: EUCLID12:3

for n being Nat
for Pn being Element of REAL n holds Line (Pn,Pn) = {Pn}

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)

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

proof end;

definition

let n be Nat;
let S be Subset of (REAL n);

attr S is being_point means :: EUCLID12:def 1
ex Pn being Element of REAL n st S = {Pn};

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} );

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

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;

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}

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;

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

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)

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

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 )

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 )

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)

proof end;

theorem Th13: :: EUCLID12:16

REAL 2 is Element of plane_of_REAL 2

proof end;

theorem Th14: :: EUCLID12:17

( |[1,0]| <> |[0,1]| & |[1,0]| <> |[0,0]| & |[0,1]| <> |[0,0]| )

proof end;

theorem Th15: :: EUCLID12:18

for L being Element of line_of_REAL 2 holds
not for x being Element of REAL 2 holds x in L

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 )

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

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;

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;

definition

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

func half_length (A,B) -> Real equals :: EUCLID12:def 2
(1 / 2) * |.(A - B).|;

correctness
coherence
(1 / 2) * |.(A - B).| is Real;
;

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

theorem :: EUCLID12:23

for A, B being Point of (TOP-REAL 2) holds half_length (A,B) = half_length (B,A) by EUCLID_6:43;

theorem :: EUCLID12:24

for A being Point of (TOP-REAL 2) holds half_length (A,A) = 0

proof end;

theorem Th18: :: EUCLID12:25

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

proof end;

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

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

proof end;

definition

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

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 b₁, C being Point of (TOP-REAL 2) st
( C in LSeg (A,B) & b₁ = C & |.(A - C).| = half_length (A,B) )

proof end;

uniqueness
for b₁, b₂ being Point of (TOP-REAL 2) st ex C being Point of (TOP-REAL 2) st
( C in LSeg (A,B) & b₁ = C & |.(A - C).| = half_length (A,B) ) & ex C being Point of (TOP-REAL 2) st
( C in LSeg (A,B) & b₂ = C & |.(A - C).| = half_length (A,B) ) holds
b₁ = b₂ by Th20;

end;

:: deftheorem Def1 defines the_midpoint_of_the_segment EUCLID12:def 3 :
for A, B, b₃ being Point of (TOP-REAL 2) holds
( b₃ = the_midpoint_of_the_segment (A,B) iff ex C being Point of (TOP-REAL 2) st
( C in LSeg (A,B) & b₃ = C & |.(A - C).| = half_length (A,B) ) );

theorem Th21: :: EUCLID12:28

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

proof end;

theorem Th22: :: EUCLID12:29

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

proof end;

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 Th24: :: EUCLID12:31

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

proof end;

theorem Th25: :: EUCLID12:32

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

proof end;

theorem Th26: :: EUCLID12:33

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

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

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)

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

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

proof end;

theorem Th31: :: EUCLID12:39

for L1, L2 being Element of line_of_REAL 2 holds L1,L2 are_coplane

proof end;

theorem :: EUCLID12:40

for L1, L2 being Element of line_of_REAL 2 st L1 _|_ L2 holds
L1 meets L2 by Th31, EUCLIDLP:109;

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;

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

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}

proof end;

theorem :: EUCLID12:44

for L1, L2 being Element of line_of_REAL 2 st L1 _|_ L2 holds
L1 /\ L2 is being_point by Th33;

theorem Th34: :: EUCLID12:45

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

proof end;

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;

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 )

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

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)

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

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

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 )

proof end;

definition

let A, B be Element of (TOP-REAL 2);
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 b₁, L1, L2 being Element of line_of_REAL 2 st
( b₁ = L2 & L1 = Line (A,B) & L1 _|_ L2 & L1 /\ L2 = {(the_midpoint_of_the_segment (A,B))} )

proof end;

uniqueness
for b₁, b₂ being Element of line_of_REAL 2 st ex L1, L2 being Element of line_of_REAL 2 st
( b₁ = 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₂ = L2 & L1 = Line (A,B) & L1 _|_ L2 & L1 /\ L2 = {(the_midpoint_of_the_segment (A,B))} ) holds
b₁ = b₂

proof end;

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₃ being Element of line_of_REAL 2 holds
( b₃ = the_perpendicular_bisector (A,B) iff ex L1, L2 being Element of line_of_REAL 2 st
( b₃ = L2 & L1 = Line (A,B) & L1 _|_ L2 & L1 /\ L2 = {(the_midpoint_of_the_segment (A,B))} ) );

theorem :: EUCLID12:53

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

proof end;

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)

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

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

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)

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)

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)

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)

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

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

proof end;

definition

let A, B, C be Point of (TOP-REAL 2);
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
ex b₁ being Point of (TOP-REAL 2) st
( (the_perpendicular_bisector (A,B)) /\ (the_perpendicular_bisector (B,C)) = {b₁} & (the_perpendicular_bisector (B,C)) /\ (the_perpendicular_bisector (C,A)) = {b₁} & (the_perpendicular_bisector (C,A)) /\ (the_perpendicular_bisector (A,B)) = {b₁} )

proof end;

uniqueness
for b₁, b₂ being Point of (TOP-REAL 2) st (the_perpendicular_bisector (A,B)) /\ (the_perpendicular_bisector (B,C)) = {b₁} & (the_perpendicular_bisector (B,C)) /\ (the_perpendicular_bisector (C,A)) = {b₁} & (the_perpendicular_bisector (C,A)) /\ (the_perpendicular_bisector (A,B)) = {b₁} & (the_perpendicular_bisector (A,B)) /\ (the_perpendicular_bisector (B,C)) = {b₂} & (the_perpendicular_bisector (B,C)) /\ (the_perpendicular_bisector (C,A)) = {b₂} & (the_perpendicular_bisector (C,A)) /\ (the_perpendicular_bisector (A,B)) = {b₂} holds
b₁ = b₂ by ZFMISC_1:3;

end;

:: 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₄ being Point of (TOP-REAL 2) holds
( b₄ = the_circumcenter (A,B,C) iff ( (the_perpendicular_bisector (A,B)) /\ (the_perpendicular_bisector (B,C)) = {b₄} & (the_perpendicular_bisector (B,C)) /\ (the_perpendicular_bisector (C,A)) = {b₄} & (the_perpendicular_bisector (C,A)) /\ (the_perpendicular_bisector (A,B)) = {b₄} ) );

definition

let A, B, C be Point of (TOP-REAL 2);
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
coherence
|.((the_circumcenter (A,B,C)) - A).| is Real;
;

end;

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

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

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

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

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

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

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 )

proof end;

theorem :: EUCLID12:69

for a, b, r, s being Real st r <> s holds
circle (a,b,r) misses circle (a,b,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))

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)

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

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

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

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)

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

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

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 )

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

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

proof end;

definition

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

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))) is Element of line_of_REAL 2

proof end;

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

theorem Th60: :: EUCLID12:81

for A being Point of (TOP-REAL 2) holds median (A,A,A) = {A}

proof end;

theorem :: EUCLID12:82

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

proof end;

theorem :: EUCLID12:83

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

proof end;

theorem :: EUCLID12:84

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

theorem Th61: :: EUCLID12:85

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

proof end;

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

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

proof end;

definition

let A, B, C be Point of (TOP-REAL 2);
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
ex b₁ being Point of (TOP-REAL 2) st
( (median (A,B,C)) /\ (median (B,C,A)) = {b₁} & (median (B,C,A)) /\ (median (C,A,B)) = {b₁} & (median (C,A,B)) /\ (median (A,B,C)) = {b₁} ) by A1, Th63;
uniqueness
for b₁, b₂ being Point of (TOP-REAL 2) st (median (A,B,C)) /\ (median (B,C,A)) = {b₁} & (median (B,C,A)) /\ (median (C,A,B)) = {b₁} & (median (C,A,B)) /\ (median (A,B,C)) = {b₁} & (median (A,B,C)) /\ (median (B,C,A)) = {b₂} & (median (B,C,A)) /\ (median (C,A,B)) = {b₂} & (median (C,A,B)) /\ (median (A,B,C)) = {b₂} holds
b₁ = b₂ by ZFMISC_1:3;

end;

:: 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₄ being Point of (TOP-REAL 2) holds
( b₄ = the_centroid_of_the_triangle (A,B,C) iff ( (median (A,B,C)) /\ (median (B,C,A)) = {b₄} & (median (B,C,A)) /\ (median (C,A,B)) = {b₄} & (median (C,A,B)) /\ (median (A,B,C)) = {b₄} ) );