:: Circumcenter, Circumcircle, and Centroid of a Triangle
:: by Roland Coghetto
::
:: 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 () 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 ()
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 ()
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 () 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 () 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 () 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 ()
for p, q, r being Element of () 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 ()
for p, q, r being Element of () 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 = & 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,1]| <> )
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 ()
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 ();
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 () holds half_length (A,B) = (1 / 2) * |.(A - B).|;

theorem :: EUCLID12:23
for A, B being Point of () holds half_length (A,B) = half_length (B,A) by EUCLID_6:43;

theorem :: EUCLID12:24
for A being Point of () holds half_length (A,A) = 0
proof end;

theorem Th18: :: EUCLID12:25
for A, B being Point of () holds |.(A - ((1 / 2) * (A + B))).| = (1 / 2) * |.(A - B).|
proof end;

theorem Th19: :: EUCLID12:26
for A, B being Point of () ex C being Point of () 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 () 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 ();
func the_midpoint_of_the_segment (A,B) -> Point of () means :Def1: :: EUCLID12:def 3
ex C being Point of () st
( C in LSeg (A,B) & it = C & |.(A - C).| = half_length (A,B) );
existence
ex b1, C being Point of () st
( C in LSeg (A,B) & b1 = C & |.(A - C).| = half_length (A,B) )
proof end;
uniqueness
for b1, b2 being Point of () st ex C being Point of () st
( C in LSeg (A,B) & b1 = C & |.(A - C).| = half_length (A,B) ) & ex C being Point of () st
( C in LSeg (A,B) & b2 = C & |.(A - C).| = half_length (A,B) ) holds
b1 = b2
by Th20;
end;

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

theorem Th21: :: EUCLID12:28
for A, B being Point of () holds the_midpoint_of_the_segment (A,B) in LSeg (A,B)
proof end;

theorem Th22: :: EUCLID12:29
for A, B being Point of () holds the_midpoint_of_the_segment (A,B) = (1 / 2) * (A + B)
proof end;

theorem Th23: :: EUCLID12:30
for A, B being Point of () 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 () holds the_midpoint_of_the_segment (A,A) = A
proof end;

theorem Th25: :: EUCLID12:32
for A, B being Point of () st the_midpoint_of_the_segment (A,B) = A holds
A = B
proof end;

theorem Th26: :: EUCLID12:33
for A, B being Point of () 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 () 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 () 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 () holds |.(A - ()).| = |.(() - B).|
proof end;

theorem Th29: :: EUCLID12:37
for A, B, C being Point of ()
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 () 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 ;

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 ;

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 ()
for L1, L2 being Element of line_of_REAL 2
for D being Point of () 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 ()
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 ()
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 ()
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 ()
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 ();
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 = {()} );
existence
ex b1, L1, L2 being Element of line_of_REAL 2 st
( b1 = L2 & L1 = Line (A,B) & L1 _|_ L2 & L1 /\ L2 = {()} )
proof end;
uniqueness
for b1, b2 being Element of line_of_REAL 2 st ex L1, L2 being Element of line_of_REAL 2 st
( b1 = L2 & L1 = Line (A,B) & L1 _|_ L2 & L1 /\ L2 = {()} ) & ex L1, L2 being Element of line_of_REAL 2 st
( b2 = L2 & L1 = Line (A,B) & L1 _|_ L2 & L1 /\ L2 = {()} ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines the_perpendicular_bisector EUCLID12:def 4 :
for A, B being Element of () st A <> B holds
for b3 being Element of line_of_REAL 2 holds
( b3 = the_perpendicular_bisector (A,B) iff ex L1, L2 being Element of line_of_REAL 2 st
( b3 = L2 & L1 = Line (A,B) & L1 _|_ L2 & L1 /\ L2 = {()} ) );

theorem :: EUCLID12:53
for A, B being Point of () st A <> B holds
the_perpendicular_bisector (A,B) is being_line
proof end;

theorem :: EUCLID12:54
for A, B being Point of () 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 ()
for L1, L2 being Element of line_of_REAL 2
for D being Point of () 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 () 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 () 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 () 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 ()
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 () 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 () st A,B,C is_a_triangle holds
() /\ () is being_point
proof end;

theorem Th47: :: EUCLID12:62
for A, B, C being Point of () st A,B,C is_a_triangle holds
ex D being Point of () st
( () /\ () = {D} & () /\ () = {D} & () /\ () = {D} & |.(D - A).| = |.(D - B).| & |.(D - A).| = |.(D - C).| & |.(D - B).| = |.(D - C).| )
proof end;

definition
let A, B, C be Point of ();
assume A1: A,B,C is_a_triangle ;
func the_circumcenter (A,B,C) -> Point of () means :Def3: :: EUCLID12:def 5
( () /\ () = {it} & () /\ () = {it} & () /\ () = {it} );
existence
ex b1 being Point of () st
( () /\ () = {b1} & () /\ () = {b1} & () /\ () = {b1} )
proof end;
uniqueness
for b1, b2 being Point of () st () /\ () = {b1} & () /\ () = {b1} & () /\ () = {b1} & () /\ () = {b2} & () /\ () = {b2} & () /\ () = {b2} holds
b1 = b2
by ZFMISC_1:3;
end;

:: deftheorem Def3 defines the_circumcenter EUCLID12:def 5 :
for A, B, C being Point of () st A,B,C is_a_triangle holds
for b4 being Point of () holds
( b4 = the_circumcenter (A,B,C) iff ( () /\ () = {b4} & () /\ () = {b4} & () /\ () = {b4} ) );

definition
let A, B, C be Point of ();
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 () 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 () 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 ()
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 () st A,B,C is_a_triangle holds
proof end;

theorem Th50: :: EUCLID12:66
for A, B, C being Point of () 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 () 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 ()
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 ()
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) = - ()
proof end;

theorem Th52: :: EUCLID12:71
for a being Real
for A, B, C being Point of ()
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 () 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 () 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 ()
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 ()
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 ()
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 ()
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 ()
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 ()
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 () 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 ();
func median (A,B,C) -> Element of line_of_REAL 2 equals :: EUCLID12:def 7
Line (A,());
coherence
Line (A,()) is Element of line_of_REAL 2
proof end;
end;

:: deftheorem defines median EUCLID12:def 7 :
for A, B, C being Point of () holds median (A,B,C) = Line (A,());

theorem Th60: :: EUCLID12:81
for A being Point of () holds median (A,A,A) = {A}
proof end;

theorem :: EUCLID12:82
for A, B being Point of () holds median (A,A,B) = Line (A,B)
proof end;

theorem :: EUCLID12:83
for A, B being Point of () holds median (A,B,A) = Line (A,B)
proof end;

theorem :: EUCLID12:84
for A, B being Point of () holds median (B,A,A) = Line (A,B) by Th24;

theorem Th61: :: EUCLID12:85
for A, B, C being Point of () 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 () st A,B,C is_a_triangle holds
ex D being Point of () 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 () st A,B,C is_a_triangle holds
ex D being Point of () 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 ();
assume A1: A,B,C is_a_triangle ;
func the_centroid_of_the_triangle (A,B,C) -> Point of () 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 b1 being Point of () st
( (median (A,B,C)) /\ (median (B,C,A)) = {b1} & (median (B,C,A)) /\ (median (C,A,B)) = {b1} & (median (C,A,B)) /\ (median (A,B,C)) = {b1} )
by ;
uniqueness
for b1, b2 being Point of () st (median (A,B,C)) /\ (median (B,C,A)) = {b1} & (median (B,C,A)) /\ (median (C,A,B)) = {b1} & (median (C,A,B)) /\ (median (A,B,C)) = {b1} & (median (A,B,C)) /\ (median (B,C,A)) = {b2} & (median (B,C,A)) /\ (median (C,A,B)) = {b2} & (median (C,A,B)) /\ (median (A,B,C)) = {b2} holds
b1 = b2
by ZFMISC_1:3;
end;

:: deftheorem defines the_centroid_of_the_triangle EUCLID12:def 8 :
for A, B, C being Point of () st A,B,C is_a_triangle holds
for b4 being Point of () holds
( b4 = the_centroid_of_the_triangle (A,B,C) iff ( (median (A,B,C)) /\ (median (B,C,A)) = {b4} & (median (B,C,A)) /\ (median (C,A,B)) = {b4} & (median (C,A,B)) /\ (median (A,B,C)) = {b4} ) );