:: Angle and Triangle in {E}uclidian Topological Space
::  by Akihiro Kubo and Yatsuka Nakamura
::
:: Received May 29, 2003
:: Copyright (c) 2003-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, XCMPLX_0, REAL_1, PRE_TOPC, EUCLID, COMPLEX1, RELAT_1,
      SUBSET_1, MCART_1, ARYTM_3, ARYTM_1, SUPINF_2, CARD_1, SQUARE_1,
      FINSEQ_1, FUNCT_1, RVSUM_1, CARD_3, ORDINAL4, COMPTRIG, SIN_COS,
      XXREAL_0, XXREAL_1, COMPLEX2, PROB_2, RLTOPSP1, XBOOLE_0, TARSKI,
      STRUCT_0, TOPMETR, EUCLID_3;
 notations TARSKI, XBOOLE_0, SUBSET_1, SQUARE_1, RELAT_1, SIN_COS, FUNCT_1,
      FUNCT_2, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, COMPLEX1, XREAL_0,
      REAL_1, FINSEQ_1, RVSUM_1, STRUCT_0, PRE_TOPC, RLTOPSP1, EUCLID,
      COMPTRIG, COMPLEX2, RLVECT_1, TOPMETR, RCOMP_1;
 constructors REAL_1, SQUARE_1, BINOP_2, RCOMP_1, SIN_COS, COMPTRIG, COMPLEX2,
      MONOID_0, TOPMETR, TOPREAL1, COMPLEX1;
 registrations RELSET_1, NUMBERS, XCMPLX_0, XXREAL_0, STRUCT_0, MONOID_0,
      EUCLID, TOPMETR, VALUED_0, XREAL_0, ORDINAL1, SIN_COS, SQUARE_1;
 requirements BOOLE, SUBSET, REAL, NUMERALS, ARITHM;


begin

reserve z,z1,z2 for Complex;
reserve r,x1,x2 for Real;
reserve p0,p,p1,p2,p3,q for Point of TOP-REAL 2;

definition
  let z be Complex;
  func cpx2euc(z) -> Point of TOP-REAL 2 equals
:: EUCLID_3:def 1
  |[Re z,Im z]|;
end;

definition
  let p be Point of TOP-REAL 2;
  func euc2cpx(p) -> Element of COMPLEX equals
:: EUCLID_3:def 2
  p`1 +p`2 *<i>;
end;

theorem :: EUCLID_3:1
  euc2cpx(cpx2euc(z))=z;

theorem :: EUCLID_3:2
  cpx2euc(euc2cpx(p))=p;

theorem :: EUCLID_3:3
  for z1,z2 st cpx2euc(z1)=cpx2euc(z2) holds z1=z2;

theorem :: EUCLID_3:4
  for p1,p2 st euc2cpx(p1)=euc2cpx(p2) holds p1=p2;

theorem :: EUCLID_3:5
  cpx2euc(x1+x2*<i>)= |[x1,x2]|;

theorem :: EUCLID_3:6
  |[Re (z1+z2),Im (z1+z2)]|=|[Re z1 + Re z2, Im z1 + Im z2]|;

theorem :: EUCLID_3:7
  cpx2euc(z1+z2)=cpx2euc(z1)+cpx2euc(z2);

theorem :: EUCLID_3:8
  (p1+p2)`1+(p1+p2)`2*<i> = p1`1+p2`1+(p1`2+p2`2)*<i>;

theorem :: EUCLID_3:9
  euc2cpx(p1+p2)=euc2cpx(p1)+euc2cpx(p2);

theorem :: EUCLID_3:10
  |[Re (-z),Im (-z)]|=|[-(Re z), -(Im z)]|;

theorem :: EUCLID_3:11
  cpx2euc(-z)= -cpx2euc(z);

theorem :: EUCLID_3:12
  (-p)`1+(-p)`2*<i>= -(p`1)+(-(p`2))*<i>;

theorem :: EUCLID_3:13
  euc2cpx(-p)= -euc2cpx(p);

theorem :: EUCLID_3:14
  cpx2euc(z1-z2)=cpx2euc(z1)-cpx2euc(z2);

theorem :: EUCLID_3:15
  euc2cpx(p1-p2)=euc2cpx(p1)-euc2cpx(p2);

theorem :: EUCLID_3:16
  cpx2euc(0c)= 0.TOP-REAL 2;

theorem :: EUCLID_3:17
  euc2cpx(0.TOP-REAL 2)=0c;

theorem :: EUCLID_3:18
  euc2cpx(p)=0c implies p=0.TOP-REAL 2;

theorem :: EUCLID_3:19
  cpx2euc(r*z)=r*(cpx2euc(z));

theorem :: EUCLID_3:20
  euc2cpx(r*p)= r*euc2cpx(p);

theorem :: EUCLID_3:21
  |.euc2cpx(p).|=sqrt ((p`1)^2+(p`2)^2);

theorem :: EUCLID_3:22
  for f being FinSequence of REAL st len f=2 holds |.f.| = sqrt ((f.1)^2
  +(f.2)^2);

theorem :: EUCLID_3:23
  for f being FinSequence of REAL, p being Point of TOP-REAL 2 st len f
  = 2 & p = f holds |.p.|=|.f.|;

theorem :: EUCLID_3:24
  |.cpx2euc(z).|=sqrt ((Re z)^2 + (Im z)^2);

theorem :: EUCLID_3:25
  |.euc2cpx(p).|=|.p.|;

definition
  let p;
  func Arg(p) -> Real equals
:: EUCLID_3:def 3
  Arg(euc2cpx(p));
end;

theorem :: EUCLID_3:26
  for z being Element of COMPLEX, p st z=euc2cpx(p) or p=cpx2euc(z)
  holds Arg(z)=Arg(p);

theorem :: EUCLID_3:27
  for x1,x2 being Real,p st x1= |.p.|*cos (Arg p) & x2=|.p.|*sin (Arg p)
  holds p = |[ x1,x2 ]|;

theorem :: EUCLID_3:28
  Arg(0.TOP-REAL 2)=0;

theorem :: EUCLID_3:29
  for p st p<>0.TOP-REAL 2 holds (Arg(p)<PI implies Arg(-p)=Arg(p)+PI)&
  (Arg(p)>=PI implies Arg(-p)=Arg(p)-PI);

theorem :: EUCLID_3:30
  for p st Arg p=0 holds p=|[ |.p.|,0 ]| & p`2=0;

theorem :: EUCLID_3:31
  for p st p<>0.TOP-REAL 2 holds (Arg(p)<PI iff Arg(-p)>=PI);

theorem :: EUCLID_3:32
  for p1,p2 st p1<>p2 or p1-p2<>0.TOP-REAL 2 holds (Arg(p1-p2)<PI iff
  Arg(p2-p1)>=PI);

theorem :: EUCLID_3:33
  for p holds Arg p in ].0,PI.[ iff p`2 > 0;

theorem :: EUCLID_3:34
  for p1,p2 st Arg(p1)<PI & Arg(p2)<PI holds Arg(p1+p2)<PI;

definition
  let p1,p2,p3;
  func angle(p1,p2,p3) -> Real equals
:: EUCLID_3:def 4
  angle(euc2cpx(p1),euc2cpx(p2),euc2cpx(p3));
end;

theorem :: EUCLID_3:35
  for p1,p2,p3 holds angle(p1,p2,p3)=angle(p1-p2,0.TOP-REAL 2,p3-p2);

theorem :: EUCLID_3:36
  for p1,p2,p3 st angle(p1,p2,p3) =0 holds Arg(p1-p2)=Arg(p3-p2) & angle
  (p3,p2,p1)=0;

theorem :: EUCLID_3:37
  for p1,p2,p3 st angle(p1,p2,p3) <>0 holds angle(p3,p2,p1)=2*PI-angle(
  p1,p2,p3);

theorem :: EUCLID_3:38
  for p1,p2,p3 st angle(p3,p2,p1) <>0 holds angle(p3,p2,p1)=2*PI-angle(
  p1,p2,p3);

theorem :: EUCLID_3:39
  for x,y being Element of COMPLEX holds Re (x .|. y) = (Re x)*(Re
  y)+(Im x)*(Im y);

theorem :: EUCLID_3:40
  for x,y being Element of COMPLEX holds Im (x .|. y) = -((Re x)*(
  Im y))+(Im x)*(Re y);

theorem :: EUCLID_3:41
  for p,q holds |(p,q)| = p`1*q`1+p`2*q`2;

theorem :: EUCLID_3:42
  for p1,p2 holds |(p1,p2)| = Re ((euc2cpx(p1)) .|. (euc2cpx(p2)));

theorem :: EUCLID_3:43
  for p1,p2,p3 st p1<>0.TOP-REAL 2 & p2<>0.TOP-REAL 2 holds ( |(p1,p2)|=
  0 iff angle(p1,0.TOP-REAL 2,p2)=PI/2 or angle(p1,0.TOP-REAL 2,p2)=3/2*PI);

theorem :: EUCLID_3:44
  for p1,p2 st p1<>0.TOP-REAL 2 & p2<>0.TOP-REAL 2 holds ( -(p1`1*p2`2)+
p1`2*p2`1= |.p1.|*|.p2.| or -(p1`1*p2`2)+p1`2*p2`1= -(|.p1.|*|.p2.|) iff angle(
  p1,0.TOP-REAL 2,p2)=PI/2 or angle(p1,0.TOP-REAL 2,p2)=3/2*PI);

theorem :: EUCLID_3:45
  for p1,p2,p3 st p1<>p2 & p3<>p2 holds ( |( p1-p2,p3-p2 )| = 0 iff
  angle(p1,p2,p3)=PI/2 or angle(p1,p2,p3)=3/2*PI);

::$N Pythagorean Theorem
theorem :: EUCLID_3:46
  for p1,p2,p3 st p1<>p2 & p3<>p2 & (angle(p1,p2,p3)=PI/2 or angle(p1,p2
  ,p3)=3/2*PI) holds |.p1-p2.|^2+|.p3-p2.|^2=|.p1-p3.|^2;

theorem :: EUCLID_3:47 :: Sum of inner angles of triangle
  for p1,p2,p3 st p2<>p1 & p1<>p3 & p3<>p2 & angle(p2,p1,p3)<PI holds
  angle(p2,p1,p3)+angle(p1,p3,p2)+angle(p3,p2,p1)=PI;

definition
  let n be Element of NAT,p1,p2,p3 be Point of TOP-REAL n;
  func Triangle(p1,p2,p3) -> Subset of TOP-REAL n equals
:: EUCLID_3:def 5
  LSeg(p1,p2) \/ LSeg(p2,p3) \/ LSeg(p3,p1);
end;

definition
  let n be Element of NAT,p1,p2,p3 be Point of TOP-REAL n;
  func closed_inside_of_triangle(p1,p2,p3) -> Subset of TOP-REAL n equals
:: EUCLID_3:def 6
  {p where p is Point of TOP-REAL n:
   ex a1,a2,a3 being Real st 0<=a1 & 0<=a2 & 0<=a3
  & a1+a2+a3=1 & p=a1*p1+a2*p2+a3*p3};
end;

definition
  let n be Element of NAT,p1,p2,p3 be Point of TOP-REAL n;
  func inside_of_triangle(p1,p2,p3) -> Subset of TOP-REAL n equals
:: EUCLID_3:def 7
  closed_inside_of_triangle(p1,p2,p3) \ Triangle(p1,p2,p3);
end;

definition
  let n be Element of NAT,p1,p2,p3 be Point of TOP-REAL n;
  func outside_of_triangle(p1,p2,p3) -> Subset of TOP-REAL n equals
:: EUCLID_3:def 8
  {p where p
is Point of TOP-REAL n:
   ex a1,a2,a3 being Real st (0>a1 or 0>a2 or 0>a3) & a1+
  a2+a3=1 & p=a1*p1+a2*p2+a3*p3};
end;

definition
  let n be Element of NAT,p1,p2,p3 be Point of TOP-REAL n;
  func plane(p1,p2,p3) -> Subset of TOP-REAL n equals
:: EUCLID_3:def 9
  outside_of_triangle(p1,
  p2,p3) \/ closed_inside_of_triangle(p1,p2,p3);
end;

theorem :: EUCLID_3:48
  for n being Element of NAT,p1,p2,p3,p being Point of TOP-REAL n
st p in plane(p1,p2,p3)
ex a1,a2,a3 being Real st a1+a2+a3=1 & p=a1*p1+a2
  *p2+a3*p3;

theorem :: EUCLID_3:49
  for n being Element of NAT,p1,p2,p3 being Point of TOP-REAL n holds
  Triangle(p1,p2,p3) c= closed_inside_of_triangle(p1,p2,p3);

definition
  let n be Element of NAT,q1,q2 be Point of TOP-REAL n;
  pred q1,q2 are_lindependent2 means
:: EUCLID_3:def 10

  for a1,a2 being Real st a1*q1+a2* q2=0.TOP-REAL n holds a1=0 & a2=0;
end;

notation
  let n be Element of NAT,q1,q2 be Point of TOP-REAL n;
  antonym q1,q2 are_ldependent2 for q1,q2 are_lindependent2;
end;

theorem :: EUCLID_3:50
  for n being Element of NAT,q1,q2 being Point of TOP-REAL n st q1
  ,q2 are_lindependent2 holds q1<>q2 & q1<>0.TOP-REAL n & q2<>0.TOP-REAL n;

theorem :: EUCLID_3:51
  for n being Element of NAT, p1,p2,p3,p0 being Point of TOP-REAL
  n st p2-p1,p3-p1 are_lindependent2 & p0 in plane(p1,p2,p3)
 ex a1,a2,a3 being Real
   st p0=a1*p1+a2*p2+a3*p3 & a1+a2+a3=1 &
for b1,b2,b3 being Real st p0
  =b1*p1+b2*p2+b3*p3 & b1+b2+b3=1 holds b1=a1 & b2=a2 & b3=a3;

theorem :: EUCLID_3:52
  for n being Element of NAT, p1,p2,p3,p0 being Point of TOP-REAL
n st (ex a1,a2,a3 being Real
 st p0=a1*p1+a2*p2+a3*p3 & a1+a2+a3=1) holds p0 in
  plane(p1,p2,p3);

theorem :: EUCLID_3:53
  for n being Element of NAT,p1,p2,p3 being Point of TOP-REAL n holds
plane(p1,p2,p3)={p where p is Point of TOP-REAL n:
  ex a1,a2,a3 being Real st a1
  +a2+a3=1 & p=a1*p1+a2*p2+a3*p3};

theorem :: EUCLID_3:54
  for p1,p2,p3 st p2-p1,p3-p1 are_lindependent2 holds plane(p1,p2, p3)=REAL 2;

definition
  let n be Element of NAT,p1,p2,p3,p be Point of TOP-REAL n;
  assume
 p2-p1,p3-p1 are_lindependent2 & p in plane(p1,p2,p3);
  func tricord1(p1,p2,p3,p) -> Real means
:: EUCLID_3:def 11

  ex a2,a3 being Real st it+a2 +a3=1 & p=it*p1+a2*p2+a3*p3;
end;

definition
  let n be Element of NAT,p1,p2,p3,p be Point of TOP-REAL n;
  assume
 p2-p1,p3-p1 are_lindependent2 & p in plane(p1,p2,p3);
  func tricord2(p1,p2,p3,p) -> Real means
:: EUCLID_3:def 12

  ex a1,a3 being Real st a1+it +a3=1 & p=a1*p1+it*p2+a3*p3;
end;

definition
  let n be Element of NAT,p1,p2,p3,p be Point of TOP-REAL n;
  assume
 p2-p1,p3-p1 are_lindependent2 & p in plane(p1,p2,p3);
  func tricord3(p1,p2,p3,p) -> Real means
:: EUCLID_3:def 13

  ex a1,a2 being Real st a1+a2 +it=1 & p=a1*p1+a2*p2+it*p3;
end;

definition
  let p1,p2,p3;
  func trcmap1(p1,p2,p3) -> Function of TOP-REAL 2,R^1 means
:: EUCLID_3:def 14
  for p holds it.p= tricord1(p1,p2,p3,p);
end;

definition
  let p1,p2,p3;
  func trcmap2(p1,p2,p3) -> Function of TOP-REAL 2,R^1 means
:: EUCLID_3:def 15
  for p holds it.p= tricord2(p1,p2,p3,p);
end;

definition
  let p1,p2,p3;
  func trcmap3(p1,p2,p3) -> Function of TOP-REAL 2,R^1 means
:: EUCLID_3:def 16
  for p holds it.p= tricord3(p1,p2,p3,p);
end;

theorem :: EUCLID_3:55
  for p1,p2,p3,p st p2-p1,p3-p1 are_lindependent2 holds p in
outside_of_triangle(p1,p2,p3) iff tricord1(p1,p2,p3,p)<0 or tricord2(p1,p2,p3,p
  )<0 or tricord3(p1,p2,p3,p)<0;

theorem :: EUCLID_3:56
  for p1,p2,p3,p st p2-p1,p3-p1 are_lindependent2 holds p in
  Triangle(p1,p2,p3) iff tricord1(p1,p2,p3,p)>=0 & tricord2(p1,p2,p3,p)>=0 &
tricord3(p1,p2,p3,p)>=0 & (tricord1(p1,p2,p3,p)=0 or tricord2(p1,p2,p3,p)=0 or
 tricord3(p1,p2,p3,p)=0);

theorem :: EUCLID_3:57
  for p1,p2,p3,p st p2-p1,p3-p1 are_lindependent2 holds p in Triangle(p1
,p2,p3) iff tricord1(p1,p2,p3,p)=0 & tricord2(p1,p2,p3,p)>=0 & tricord3(p1,p2,
p3,p)>=0 or tricord1(p1,p2,p3,p)>=0 & tricord2(p1,p2,p3,p)=0 & tricord3(p1,p2,
p3,p)>=0 or tricord1(p1,p2,p3,p)>=0 & tricord2(p1,p2,p3,p)>=0 & tricord3(p1,p2,
  p3,p)=0;

theorem :: EUCLID_3:58
  for p1,p2,p3,p st p2-p1,p3-p1 are_lindependent2 holds p in
inside_of_triangle(p1,p2,p3) iff tricord1(p1,p2,p3,p)>0 & tricord2(p1,p2,p3,p)>
  0 & tricord3(p1,p2,p3,p)>0;

theorem :: EUCLID_3:59
  for p1,p2,p3 st p2-p1,p3-p1 are_lindependent2 holds inside_of_triangle
  (p1,p2,p3) is non empty;