:: Heron's Formula and Ptolemy's Theorem
::  by Marco Riccardi
::
:: Received January 10, 2008
:: Copyright (c) 2008-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, PRE_TOPC, EUCLID, COMPLEX1, ARYTM_1, CARD_1, SUPINF_2,
      SUBSET_1, VALUED_0, FINSEQ_1, SIN_COS, COMPLEX2, RELAT_1, XXREAL_0,
      ARYTM_3, REAL_1, EUCLID_3, COMPTRIG, FINSEQ_6, XCMPLX_0, MCART_1,
      FUNCT_1, PROB_2, SQUARE_1, RVSUM_1, RLTOPSP1, JGRAPH_6, XBOOLE_0,
      BORSUK_1, XXREAL_1, TOPS_2, STRUCT_0, PARTFUN1, ORDINAL2, TARSKI,
      ZFMISC_1, PROJPL_1, TOPMETR, PCOMPS_1, METRIC_1, SIN_COS6, EUCLID_6,
      PENCIL_1, RLVECT_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1,
      NUMBERS, XREAL_0, XXREAL_0, PARTFUN1, BINOP_1, STRUCT_0, PRE_TOPC,
      SQUARE_1, VALUED_0, FINSEQ_1, FINSEQ_2, RVSUM_1, RLVECT_1, RLTOPSP1,
      EUCLID, SIN_COS, JGRAPH_6, COMPTRIG, COMPLEX2, TOPMETR, RCOMP_1,
      EUCLID_3, TOPS_2, XCMPLX_0, COMPLEX1, REAL_1, METRIC_1, PCOMPS_1,
      SIN_COS6;
 constructors REAL_1, SQUARE_1, BINOP_2, MONOID_0, RCOMP_1, SIN_COS, JGRAPH_6,
      COMPTRIG, COMPLEX2, EUCLID_3, TOPS_2, SIN_COS6, FUNCSDOM, CONVEX1,
      PCOMPS_1, COMPLEX1;
 registrations XBOOLE_0, RELSET_1, XXREAL_0, XREAL_0, MEMBERED, MONOID_0,
      STRUCT_0, EUCLID, XCMPLX_0, TOPMETR, SQUARE_1, FUNCT_2, PRE_TOPC,
      METRIC_1, BORSUK_1, SIN_COS6, VALUED_0, RVSUM_1, RLTOPSP1, SIN_COS,
      ORDINAL1;
 requirements BOOLE, SUBSET, REAL, NUMERALS, ARITHM;


begin :: Law of Cosines and Meister-Gauss Formula

reserve p1,p2,p3,p4,p5,p6,p,pc for Point of TOP-REAL 2;
reserve a,b,c,r,s for Real;

theorem :: EUCLID_6:1
  sin angle(p1,p2,p3) = sin angle(p4,p5,p6) & cos angle(p1,p2,p3) =
  cos angle(p4,p5,p6) implies angle(p1,p2,p3) = angle(p4,p5,p6);

theorem :: EUCLID_6:2
  sin angle(p1,p2,p3) = - sin angle(p3,p2,p1);

theorem :: EUCLID_6:3
  cos angle(p1,p2,p3) = cos angle(p3,p2,p1);

theorem :: EUCLID_6:4
  angle(p1,p4,p2)+angle(p2,p4,p3)=angle(p1,p4,p3) or angle(p1,p4,p2
  )+angle(p2,p4,p3)=angle(p1,p4,p3) + 2*PI;

:: Meister-Gauss formula

definition
  let p1,p2,p3;
::$N Meister-Gauss formula (for triangles
  func the_area_of_polygon3(p1,p2,p3) -> Real equals
:: EUCLID_6:def 1
  ((p1`1*p2`2-p2`1*
  p1`2)+(p2`1*p3`2-p3`1*p2`2)+(p3`1*p1`2-p1`1*p3`2))/2;
end;

definition
  let p1,p2,p3;
  func the_perimeter_of_polygon3(p1,p2,p3) -> Real equals
:: EUCLID_6:def 2
  |.p2-p1.| +
  |.p3-p2.| + |.p1-p3.|;
end;

:: Area

theorem :: EUCLID_6:5
  the_area_of_polygon3(p1,p2,p3) = |.p1-p2.|*|.p3-p2.|*sin angle(p3 ,p2,p1) / 2
;

theorem :: EUCLID_6:6
  p2<>p1 implies |.p3-p2.| * sin angle(p3,p2,p1) = |.p3-p1.| * sin
  angle(p2,p1,p3);

:: Law of Cosines

::$N Law of Cosines
theorem :: EUCLID_6:7
  a = |.p1-p2.| & b = |.p3-p2.| & c = |.p3-p1.| implies c^2 = a^2 +
  b^2 - 2*a*b * cos angle(p1,p2,p3);

begin :: Some elementary facts about Euclidean geometry

theorem :: EUCLID_6:8
  p in LSeg(p1,p2) & p<>p1 & p<>p2 implies angle(p1,p,p2) = PI;

theorem :: EUCLID_6:9
  p in LSeg(p2,p3) & p<>p2 implies angle(p3,p2,p1)=angle(p,p2,p1);

theorem :: EUCLID_6:10
  p in LSeg(p2,p3) & p<>p2 implies angle(p1,p2,p3) = angle(p1,p2,p );

theorem :: EUCLID_6:11
  angle(p1,p,p2) = PI implies p in LSeg(p1,p2);

theorem :: EUCLID_6:12
  p in LSeg(p1,p3) & p in LSeg(p1,p4) & p3<>p4 & p<>p1 implies p3
  in LSeg(p1,p4) or p4 in LSeg(p1,p3);

theorem :: EUCLID_6:13
  p in LSeg(p1,p3) & p<>p1 & p<>p3 implies angle(p1,p,p2)+angle(p2
  ,p,p3)=PI or angle(p1,p,p2)+angle(p2,p,p3)=3*PI;

theorem :: EUCLID_6:14
  p in LSeg(p1,p2) & p<>p1 & p<>p2 & (angle(p3,p,p1)=PI/2 or angle
  (p3,p,p1)=3/2*PI) implies angle(p1,p,p3)=angle(p3,p,p2);

:: Vertical angles

theorem :: EUCLID_6:15
  p in LSeg(p1,p3) & p in LSeg(p2,p4) & p<>p1 & p<>p2 & p<>p3 & p
  <>p4 implies angle(p1,p,p2)=angle(p3,p,p4);

:: The Isosceles Triangle Theorem A

theorem :: EUCLID_6:16
  |.p3-p1.|=|.p2-p3.| & p1<>p2 implies angle(p3,p1,p2)=angle(p1,p2 ,p3);

theorem :: EUCLID_6:17
  for p1,p2,p3,p st p in LSeg(p1,p2) & p<>p2 holds |(p3-p,p2-p1)|
  = 0 iff |(p3-p,p2-p)| = 0;

theorem :: EUCLID_6:18
  |.p1-p3.|=|.p2-p3.| & p in LSeg(p1,p2) & p<>p3 & p<>p1 & (angle(
  p3,p,p1)=PI/2 or angle(p3,p,p1)=3/2*PI) implies angle(p1,p3,p)=angle(p,p3,p2)
;

:: The Isosceles Triangle Theorem B

::$N Isosceles Triangle Theorem
theorem :: EUCLID_6:19
  for p1,p2,p3,p st |.p1-p3.|=|.p2-p3.| & p in LSeg(p1,p2) & p<>p3 holds
(angle(p1,p3,p)=angle(p,p3,p2) implies |.p1-p.| = |.p-p2.|) & (|.p1-p.| = |.p-
p2.| implies |(p3-p,p2-p1)| = 0) & (|(p3-p,p2-p1)| = 0 implies angle(p1,p3,p)=
  angle(p,p3,p2));

definition let V be RealLinearSpace;
::$CD
::  let p1,p2,p3 be Point of V;
::   redefine pred p1,p2,p3 are_collinear means
::   :Def3:
::   p1 in LSeg(p2,p3) or p2 in LSeg(p3, p1) or p3 in LSeg(p1,p2);
::  compatibility by TOPREAL9:67;
end;

notation let V be RealLinearSpace;
  let p1,p2,p3 be Element of V;
  antonym p1,p2,p3 is_a_triangle for p1,p2,p3 are_collinear;
end;

theorem :: EUCLID_6:20
  p1,p2,p3 is_a_triangle iff p1,p2,p3 are_mutually_distinct &
  angle(p1,p2,p3)<>PI & angle(p2,p3,p1)<>PI & angle(p3,p1,p2)<>PI;

theorem :: EUCLID_6:21
  p1,p2,p3 is_a_triangle & p4,p5,p6 is_a_triangle & angle(p1,p2,p3
) = angle(p4,p5,p6) & angle(p3,p1,p2) = angle(p6,p4,p5) implies |.p3-p2.|*|.p4-
p6.| = |.p1-p3.|*|.p6-p5.| & |.p3-p2.|*|.p5-p4.| = |.p2-p1.|*|.p6-p5.| & |.p1-
  p3.|*|.p5-p4.| = |.p2-p1.|*|.p4-p6.|;

theorem :: EUCLID_6:22
  p1,p2,p3 is_a_triangle & p4,p5,p6 is_a_triangle & angle(p1,p2,p3
) = angle(p4,p5,p6) & angle(p3,p1,p2) = angle(p5,p6,p4) implies |.p2-p3.| * |.
p4-p6.| = |.p3-p1.| * |.p5-p4.| & |.p2-p3.| * |.p6-p5.| = |.p1-p2.| * |.p5-p4.|
  & |.p3-p1.| * |.p6-p5.| = |.p1-p2.| * |.p4-p6.|;

theorem :: EUCLID_6:23
  p1,p2,p3 are_mutually_distinct & angle(p1,p2,p3)<=PI implies
  angle(p2,p3,p1)<=PI & angle(p3,p1,p2)<=PI;

theorem :: EUCLID_6:24
  p1,p2,p3 are_mutually_distinct & angle(p1,p2,p3)>PI implies
  angle(p2,p3,p1)>PI & angle(p3,p1,p2)>PI;

theorem :: EUCLID_6:25
  p in LSeg(p1,p2) & p1,p2,p3 is_a_triangle & angle(p1,p3,p2) =
  angle(p,p3,p2) implies p=p1;

theorem :: EUCLID_6:26
  p in LSeg(p1,p2) & not p3 in LSeg(p1,p2) & angle(p1,p3,p2) <= PI
  implies angle(p,p3,p2) <= angle(p1,p3,p2);

theorem :: EUCLID_6:27
  p in LSeg(p1,p2) & not p3 in LSeg(p1,p2) & angle(p1,p3,p2) > PI
  & p<>p2 implies angle(p,p3,p2) >= angle(p1,p3,p2);

theorem :: EUCLID_6:28
  p in LSeg(p1,p2) & not p3 in LSeg(p1,p2) implies ex p4 st p4 in
  LSeg(p1,p2) & angle(p1,p3,p4) = angle(p,p3,p2);

theorem :: EUCLID_6:29
  p1 in inside_of_circle(a,b,r) & p2 in outside_of_circle(a,b,r) implies
  ex p st p in LSeg(p1,p2) /\ circle(a,b,r);

theorem :: EUCLID_6:30
  p1 in circle(a,b,r) & p3 in circle(a,b,r) & p4 in circle(a,b,r)
  & p in LSeg(p1,p3) & p in LSeg(p1,p4) & p3<>p4 implies p=p1;

theorem :: EUCLID_6:31
  p1 in circle(a,b,r) & p2 in circle(a,b,r) & p in circle(a,b,r) &
pc = |[a,b]| & pc in LSeg(p,p2) & p1<>p implies 2*angle(p1,p,p2) = angle(p1,pc,
  p2) or 2*(angle(p1,p,p2) - PI) = angle(p1,pc,p2);

:: opposite point on circle

theorem :: EUCLID_6:32
  p1 in circle(a,b,r) & r>0 implies ex p2 st p1<>p2 & p2 in circle
  (a,b,r) & |[a,b]| in LSeg(p1,p2);

:: The centre angle and the inscribed angle

theorem :: EUCLID_6:33
  p1 in circle(a,b,r) & p2 in circle(a,b,r) & p in circle(a,b,r) &
pc = |[a,b]| & p1<>p & p2<>p implies 2*angle(p1,p,p2) = angle(p1,pc,p2) or 2*(
  angle(p1,p,p2) - PI) = angle(p1,pc,p2);

:: Angles subtended by the same chord

theorem :: EUCLID_6:34
  p1 in circle(a,b,r) & p2 in circle(a,b,r) & p3 in circle(a,b,r)
& p4 in circle(a,b,r) & p1<>p3 & p1<>p4 & p2<>p3 & p2<>p4 implies angle(p1,p3,
p2) = angle(p1,p4,p2) or angle(p1,p3,p2) = angle(p1,p4,p2) - PI or angle(p1,p3,
  p2) = angle(p1,p4,p2) + PI;

theorem :: EUCLID_6:35
  p1 in circle(a,b,r) & p2 in circle(a,b,r) & p3 in circle(a,b,r)
  & p1<>p2 & p2<>p3 implies angle(p1,p2,p3)<>PI;

theorem :: EUCLID_6:36
  p1 in circle(a,b,r) & p2 in circle(a,b,r) & p3 in circle(a,b,r)
  & p4 in circle(a,b,r) & p in LSeg(p1,p3) & p in LSeg(p2,p4) & p1,p2,p3,p4
  are_mutually_distinct implies angle(p1,p4,p2) = angle(p1,p3,p2);

theorem :: EUCLID_6:37
  p1 in circle(a,b,r) & p2 in circle(a,b,r) & p3 in circle(a,b,r)
  & angle(p1,p2,p3) = 0 & p1<>p2 & p2<>p3 implies p1=p3;

:: Intersecting Chords Theorem or
:: Product of Segments of Chords

::$N Intersecting chords theorem
theorem :: EUCLID_6:38
  p1 in circle(a,b,r) & p2 in circle(a,b,r) & p3 in circle(a,b,r) & p4
in circle(a,b,r) & p in LSeg(p1,p3) & p in LSeg(p2,p4) implies |.p1-p.|*|.p-p3
  .| = |.p2-p.|*|.p-p4.|;

begin :: Heron's Formula and Ptolemy's Theorem
:: Heron's formula

::$N Heron's Formula
theorem :: EUCLID_6:39
  a = |.p2-p1.| & b = |.p3-p2.| & c = |.p1-p3.| & s =
the_perimeter_of_polygon3(p1,p2,p3)/2 implies
  |.the_area_of_polygon3(p1,p2,p3).| = sqrt(s*(s-a)*(s-b)*(s-c));

:: Ptolemy's Theorem

::$N Ptolemy's Theorem
theorem :: EUCLID_6:40
  p1 in circle(a,b,r) & p2 in circle(a,b,r) & p3 in circle(a,b,r) & p4
in circle(a,b,r) & p in LSeg(p1,p3) & p in LSeg(p2,p4) implies |.p3-p1.|*|.p4-
  p2.| = |.p2-p1.|*|.p4-p3.| + |.p3-p2.|*|.p4-p1.|;

begin :: Appendix

reserve c1,c2,c3 for Element of COMPLEX;

theorem :: EUCLID_6:41
  (p1-p2)`1 = p1`1 - p2`1 & (p1-p2)`2 = p1`2 - p2`2;

theorem :: EUCLID_6:42
  |.p1-p2.| = 0 iff p1=p2;

theorem :: EUCLID_6:43
  |.p1-p2.| = |.p2-p1.|;

theorem :: EUCLID_6:44
  not angle(p1,p2,p3) = 2*angle(p4,p5,p6)+2*PI;

theorem :: EUCLID_6:45
  not angle(p1,p2,p3) = 2*angle(p4,p5,p6)+4*PI;

theorem :: EUCLID_6:46
  not angle(p1,p2,p3) = 2*angle(p4,p5,p6)-4*PI;

theorem :: EUCLID_6:47
  not angle(p1,p2,p3) = 2*angle(p4,p5,p6)-6*PI;

theorem :: EUCLID_6:48
  c1=euc2cpx(p1-p2) & c2=euc2cpx(p3-p2) implies angle(p1,p2,p3) = angle(
  c1,c2);

theorem :: EUCLID_6:49
  angle(c1,c2) + angle(c2,c3) = angle(c1,c3) or angle(c1,c2) + angle(c2,
  c3) = angle(c1,c3) + 2*PI;

theorem :: EUCLID_6:50
  c1 = euc2cpx(p1-p2) & c2 = euc2cpx(p3-p2) implies Re (c1.|.c2) = (p1`1
- p2`1)*(p3`1 - p2`1)+(p1`2 - p2`2)*(p3`2 - p2`2) & Im (c1.|.c2) = -(p1`1 - p2
`1)*(p3`2 - p2`2)+(p1`2 - p2`2)*(p3`1 - p2`1) & |.c1.| = sqrt((p1`1 - p2`1)^2 +
  (p1`2 - p2`2)^2) & |.p1-p2.|=|.c1.|;

theorem :: EUCLID_6:51
  for n being Element of NAT, q1 being Point of TOP-REAL n for f being
Function of TOP-REAL n,R^1 st (for q being Point of TOP-REAL n holds f.q=|.q-q1
  .|) holds f is continuous;

theorem :: EUCLID_6:52
  for n being Element of NAT, q1 being Point of TOP-REAL n ex f being
Function of TOP-REAL n, R^1 st (for q being Point of TOP-REAL n holds f.q=|.q-
  q1.|) & f is continuous;