:: Circumcenter, Circumcircle, and Centroid of a Triangle
::  by Roland Coghetto
:: 
:: Received December 30, 2015
:: Copyright (c) 2015-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, NAT_1, SUBSET_1, COMPLEX1, REAL_1, RELAT_1, TARSKI,
      CARD_1, ARYTM_1, ARYTM_3, RVSUM_1, SQUARE_1, XXREAL_0, ZFMISC_1,
      XBOOLE_0, RLTOPSP1, PRE_TOPC, MCART_1, EUCLID, INCSP_1, PROJRED2, AFF_1,
      ANALOAF, EUCLID_3, SYMSP_1, EUCLIDLP, METRIC_1, JGRAPH_6, SIN_COS,
      COMPLEX2, XXREAL_1, PROJPL_1, EUCLID10, EUCLID12, RUSUB_5, GTARSKI1,
      SUPINF_2, PENCIL_1;
 notations INT_1, EUCLIDLP, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XCMPLX_0,
      NUMBERS, XREAL_0, COMPLEX1, ORDINAL1, METRIC_1, STRUCT_0, FINSEQ_2,
      SQUARE_1, RVSUM_1, PRE_TOPC, XXREAL_0, RLVECT_1, RLTOPSP1, EUCLID,
      EUCLID_4, JGRAPH_6, SIN_COS, COMPLEX2, EUCLID_3, EUCLID_6, RCOMP_1,
      EUCLID10, MENELAUS, TOPREAL6, GTARSKI1;
 constructors SQUARE_1, EUCLID_4, EUCLIDLP, COMPLEX1, JGRAPH_6, MONOID_0,
      SIN_COS, EUCLID_3, EUCLID10, INTEGRA1, MENELAUS, TOPREAL6, GTARSKI1,
      COMPLEX2, COMPTRIG;
 registrations INT_1, MONOID_0, SUBSET_1, RELSET_1, XXREAL_0, XREAL_0, EUCLID,
      VALUED_0, SQUARE_1, ORDINAL1, EUCLIDLP, SIN_COS, EUCLID10;
 requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;


begin :: Preliminaries

reserve n for Nat,
        lambda,lambda2,mu,mu2 for Real,
        x1,x2 for Element of REAL n,
        An,Bn,Cn for Point of TOP-REAL n,
        a for Real;

theorem :: EUCLID12:1
  An = (1-lambda) * x1 + lambda * x2 & Bn = (1-mu) * x1 + mu * x2
  implies Bn - An = (mu-lambda)*(x2-x1);

theorem :: EUCLID12:2
  |.a.| = |.1-a.| implies a = 1/2;

 reserve Pn,PAn,PBn for Element of REAL n,
         Ln for Element of line_of_REAL n;

theorem :: EUCLID12:3
  Line(Pn,Pn)={Pn};

theorem :: EUCLID12:4
  An=PAn & Bn=PBn implies Line(An,Bn)=Line(PAn,PBn);

theorem :: EUCLID12:5
  An <> Cn & Cn in LSeg(An,Bn) & An in Ln & Cn in Ln & Ln is being_line
  implies Bn in Ln;

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

theorem :: EUCLID12:6
  Ln is being_line or ex Pn being Element of REAL n st Ln={Pn};

theorem :: EUCLID12:7
  Ln is being_line or Ln is being_point;

theorem :: EUCLID12:8
  Ln is being_line implies not ex Pn being Element of REAL n st Ln={Pn};

theorem :: EUCLID12:9
  Ln is being_line implies not Ln is being_point;

begin :: Between

reserve A,B,C for Point of TOP-REAL 2;

theorem :: EUCLID12:10
  C in LSeg(A,B) implies |.A-B.| = |.A-C.| + |.C-B.|;

theorem :: EUCLID12:11
  |.A-B.| = |.A-C.| + |.C-B.| implies C in LSeg(A,B);

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

theorem :: EUCLID12:13
  for p,q,r be 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;

theorem :: EUCLID12:14
  for p,q,r be 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;

begin :: REAL 2 is a plane

reserve x,y,z,y1,y2 for Element of REAL 2;
reserve L,L1,L2,L3,L4 for Element of line_of_REAL 2;
reserve D,E,F for Point of TOP-REAL 2;
reserve b,c,d,r,s for Real;

theorem :: EUCLID12:15
  for OO,Ox,Oy be Element of REAL 2 st
  OO = |[0,0]| & Ox = |[1,0]| & Oy = |[0,1]| holds
  REAL 2 = plane(OO,Ox,Oy);

theorem :: EUCLID12:16
  REAL 2 is Element of plane_of_REAL 2;

theorem :: EUCLID12:17
  |[1,0]| <> |[0,1]| & |[1,0]| <> |[0,0]| & |[0,1]| <> |[0,0]|;

theorem :: EUCLID12:18
  ex x st not x in L;

theorem :: EUCLID12:19
  ex L st L is being_point & L misses L1;

theorem :: EUCLID12:20
  not L1 // L2 implies
   (ex x st L1 = {x} or L2 = {x})
  or
   (L1 is being_line & L2 is being_line & ex x st L1 /\ L2 = {x});

theorem :: EUCLID12:21
  not L1 // L2 implies
         L1 is being_point or L2 is being_point or
         (L1 is being_line & L2 is being_line & L1 /\ L2 is being_point);

theorem :: EUCLID12:22
  L1 /\ L2 is being_point & A in L1 /\ L2 implies L1 /\ L2 = {A};

begin :: The midpoint of a segment

definition
  let A,B be Point of TOP-REAL 2;
  func half_length(A,B) -> Real equals
:: EUCLID12:def 2
1/2 * |.A-B.|;
end;

theorem :: EUCLID12:23
  half_length(A,B) = half_length(B,A);

theorem :: EUCLID12:24
  half_length(A,A) = 0;

theorem :: EUCLID12:25
  |.A - 1/2 *(A+B).| = 1/2 * |.A-B.|;

theorem :: EUCLID12:26
  ex C st C in LSeg(A,B) & |.A-C.| = 1/2 * |.A-B.|;

theorem :: EUCLID12:27
  |.A-B.| = |.A-C.| & B in LSeg(A,D) & C in LSeg(A,D) implies B = C;

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

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

theorem :: EUCLID12:28
  the_midpoint_of_the_segment(A,B) in LSeg(A,B);

theorem :: EUCLID12:29
  the_midpoint_of_the_segment(A,B) = 1/2 * (A+B);

theorem :: EUCLID12:30
  the_midpoint_of_the_segment(A,B) = the_midpoint_of_the_segment(B,A);

theorem :: EUCLID12:31
  the_midpoint_of_the_segment(A,A)=A;

theorem :: EUCLID12:32
  the_midpoint_of_the_segment(A,B) = A implies A=B;

theorem :: EUCLID12:33
  the_midpoint_of_the_segment(A,B) = B implies A=B;

theorem :: EUCLID12:34
  C in LSeg(A,B) & |.A-C.| = |.B-C.| implies half_length(A,B) = |.A-C.|;

theorem :: EUCLID12:35
  C in LSeg(A,B) & |.A-C.| = |.B-C.| implies
  C = the_midpoint_of_the_segment(A,B);

theorem :: EUCLID12:36
  |.A - the_midpoint_of_the_segment(A,B).|
    = |. the_midpoint_of_the_segment(A,B) - B.|;

theorem :: EUCLID12:37
  A<>B & r is positive & r <> 1 & |.A-C.| = r * |.A-B.| implies
  A,B,C are_mutually_distinct;

theorem :: EUCLID12:38
  C in LSeg(A,B) & |.A-C.| = 1/2 * |.A-B.| implies |.B-C.| = 1/2 * |.A-B.|;

begin :: Perpendicularity

theorem :: EUCLID12:39
  L1,L2 are_coplane;

theorem :: EUCLID12:40
  L1 _|_ L2 implies L1 meets L2;

theorem :: EUCLID12:41
  L1 is being_line & L2 is being_line & L1 misses L2 implies L1//L2;

theorem :: EUCLID12:42
  L1 <> L2 & L1 meets L2 implies
  (ex x st L1 = {x} or L2 = {x})
  or
  (L1 is being_line & L2 is being_line & ex x st L1 /\ L2 = {x});

theorem :: EUCLID12:43
  L1 _|_ L2 implies ex x st L1 /\ L2 = {x};

theorem :: EUCLID12:44
  L1 _|_ L2 implies L1 /\ L2 is being_point;

theorem :: EUCLID12:45
  L1 _|_ L2 implies not L1 // L2;

theorem :: EUCLID12:46
  L1 is being_line & L2 is being_line & L1 // L2 implies not L1 _|_ L2;

theorem :: EUCLID12:47
  L1 is being_line implies ex L2 st x in L2 & L1 _|_ L2;

theorem :: EUCLID12:48
  L1 _|_ L2 & L1 = Line(A,B) & L2 = Line(C,D) implies |(B-A,D-C)| = 0;

theorem :: EUCLID12:49
  L is being_line & A in L & B in L & A <> B implies L = Line(A,B);

theorem :: EUCLID12:50
  L1 _|_ L2 & C in L1 /\ L2 & A in L1 & B in L2  & A<>C & B<>C
  implies angle(A,C,B) = PI/2 or angle(A,C,B) = 3 * PI/2;

theorem :: EUCLID12:51
  L1 _|_ L2 & C in L1 /\ L2 & A in L1 & B in L2 & A <> C & B <> C
  implies A,B,C is_a_triangle;

begin :: The Perpendicular bisector of a segment

theorem :: EUCLID12:52
  A <> B & L1 = Line(A,B) & C in LSeg(A,B) & |.A-C.| = 1/2 * |.A-B.|
  implies ex L2 st C in L2 & L1 _|_ L2;

definition
  let A,B being Element of TOP-REAL 2;
  assume
 A <> B;
  func the_perpendicular_bisector(A,B) -> Element of line_of_REAL 2 means
:: EUCLID12:def 4

  ex L1, L2 be Element of line_of_REAL 2 st it = L2 &
  L1 = Line(A,B) & L1 _|_ L2 & L1 /\ L2 = {the_midpoint_of_the_segment(A,B)};
end;

theorem :: EUCLID12:53
  A <> B implies the_perpendicular_bisector(A,B) is being_line;

theorem :: EUCLID12:54
  A <> B implies
  the_perpendicular_bisector(A,B) = the_perpendicular_bisector(B,A);

theorem :: EUCLID12:55
  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 implies |.D-A.| = |.D-B.|;

theorem :: EUCLID12:56
  A <> B & C in the_perpendicular_bisector(A,B) implies |.C-A.| = |.C-B.|;

theorem :: EUCLID12:57
  C in Line(A,B) & |.A-C.| = |.B-C.| implies C in LSeg(A,B);

theorem :: EUCLID12:58
  A <> B implies
  the_midpoint_of_the_segment(A,B) in the_perpendicular_bisector(A,B);

theorem :: EUCLID12:59
  A<>B & L1 = Line(A,B) & L1 _|_ L2 & the_midpoint_of_the_segment(A,B) in L2
  implies L2 = the_perpendicular_bisector(A,B);

theorem :: EUCLID12:60
  A <> B & |.C-A.| = |.C-B.| implies C in the_perpendicular_bisector(A,B);

begin :: The circumcircle of a triangle

theorem :: EUCLID12:61
  A,B,C is_a_triangle implies
  the_perpendicular_bisector(A,B) /\ the_perpendicular_bisector(B,C)
  is being_point;

theorem :: EUCLID12:62
  A,B,C is_a_triangle implies ex D 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.|;

definition
  let A,B,C being Point of TOP-REAL 2;
  assume
 A,B,C is_a_triangle;
  func the_circumcenter(A,B,C) -> Point of TOP-REAL 2 means
:: 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};
end;

definition
  let A,B,C being Point of TOP-REAL 2;
  assume A,B,C is_a_triangle;
  func the_radius_of_the_circumcircle(A,B,C) -> Real equals
:: EUCLID12:def 6

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

theorem :: EUCLID12:63
  A,B,C is_a_triangle implies ex a,b,r st A in circle(a,b,r) &
  B in circle(a,b,r) & C in circle(a,b,r);

theorem :: EUCLID12:64
  A,B,C is_a_triangle & A in circle(a,b,r) & B in circle(a,b,r) &
  C in circle(a,b,r)
  implies |[a,b]| = the_circumcenter(A,B,C) & r = |.the_circumcenter(A,B,C)-A.|
;

theorem :: EUCLID12:65
  A,B,C is_a_triangle implies the_radius_of_the_circumcircle(A,B,C) > 0;

theorem :: EUCLID12:66
  A,B,C is_a_triangle implies
  |.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.|;

theorem :: EUCLID12:67
  A,B,C is_a_triangle implies
  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.|;

theorem :: EUCLID12:68
  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)
  implies a=c & b=d & r=s;

theorem :: EUCLID12:69
  r <> s implies circle(a,b,r) misses circle(a,b,s);

begin :: Extended Law of sines

theorem :: EUCLID12:70
  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 implies
  the_diameter_of_the_circumcircle(A,B,C)
     = the_diameter_of_the_circumcircle(D,B,C) or
  the_diameter_of_the_circumcircle(A,B,C)
     = - the_diameter_of_the_circumcircle(D,B,C);

theorem :: EUCLID12:71
  A,B,C is_a_triangle &
  A in circle(a,b,r) & B in circle(a,b,r) & C in circle(a,b,r)
  implies
    the_diameter_of_the_circumcircle(A,B,C) = 2 * r or
    the_diameter_of_the_circumcircle(A,B,C) = - 2 * r;

theorem :: EUCLID12:72
  A,B,C is_a_triangle & 0 < angle(C,B,A) < PI implies
  the_diameter_of_the_circumcircle(A,B,C) > 0;

theorem :: EUCLID12:73
  A,B,C is_a_triangle & PI < angle(C,B,A) < 2 * PI implies
  the_diameter_of_the_circumcircle(A,B,C) < 0;

theorem :: EUCLID12:74
  A,B,C is_a_triangle & 0 < angle(C,B,A) < PI &
  A in circle(a,b,r) & B in circle(a,b,r) & C in circle(a,b,r) implies
  the_diameter_of_the_circumcircle(A,B,C) = 2 * r;

theorem :: EUCLID12:75
  A,B,C is_a_triangle & PI < angle(C,B,A) < 2 * PI &
  A in circle(a,b,r) & B in circle(a,b,r) & C in circle(a,b,r) implies
  the_diameter_of_the_circumcircle(A,B,C) = - 2 * r;

theorem :: EUCLID12:76
  A,B,C is_a_triangle & 0 < angle(C,B,A) < PI &
  A in circle(a,b,r) & B in circle(a,b,r) & C in circle(a,b,r)
  implies
  |.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);

theorem :: EUCLID12:77
  A,B,C is_a_triangle & PI < angle(C,B,A) < 2 * PI &
  A in circle(a,b,r) & B in circle(a,b,r) & C in circle(a,b,r)
  implies
  |.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);

::$N Extended law of sines
theorem :: EUCLID12:78
  A,B,C is_a_triangle & 0 < angle(C,B,A) < PI &
  A in circle(a,b,r) & B in circle(a,b,r) & C in circle(a,b,r)
  implies
  |.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;

theorem :: EUCLID12:79
  A,B,C is_a_triangle & PI < angle(C,B,A) < 2 * PI &
  A in circle(a,b,r) & B in circle(a,b,r) & C in circle(a,b,r)
  implies
  |.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;

begin :: The centroid of a triangle

theorem :: EUCLID12:80
  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
  implies Line(A,D),Line(B,E),Line(C,F) are_concurrent;

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

theorem :: EUCLID12:81
  median(A,A,A)={A};

theorem :: EUCLID12:82
  median(A,A,B)=Line(A,B);

theorem :: EUCLID12:83
  median(A,B,A)=Line(A,B);

theorem :: EUCLID12:84
  median(B,A,A)=Line(A,B);

theorem :: EUCLID12:85
  A,B,C is_a_triangle implies median(A,B,C) is being_line;

theorem :: EUCLID12:86
  A,B,C is_a_triangle implies ex D st D in median(A,B,C) & D in median(B,C,A) &
  D in median(C,A,B);

theorem :: EUCLID12:87
  A,B,C is_a_triangle implies ex D 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};

definition
  let A,B,C be Point of TOP-REAL 2;
  assume
 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};
end;