The Mizar abstract of EUCLID

Journal of Formalized Mathematics
Volume 15, 2003
University of Bialystok
Copyright (c) 2003 Association of Mizar Users
The abstract of the Mizar article:: Angle and Triangle in Euclidian Topological Space
by
Akihiro Kubo, and
Yatsuka Nakamura
Received May 29, 2003
MML identifier: EUCLID_3
[ Mizar article, MML identifier index ]
environ

 vocabulary RLVECT_1, COMPLEX1, ARYTM_1, SQUARE_1, FUNCT_1, RCOMP_1, SIN_COS,
      ARYTM_3, PRE_TOPC, BOOLE, RELAT_1, COMPTRIG, PROB_2, MCART_1, RVSUM_1,
      FINSEQ_1, EUCLID, COMPLEX2, EUCLID_2, TOPREAL1, TOPMETR, EUCLID_3;
 notation TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, SQUARE_1, NAT_1, RELAT_1,
      FUNCT_1, SEQ_1, SIN_COS, FUNCT_2, ARYTM_0, NUMBERS, XREAL_0, REAL_1,
      COMPLEX1, PRE_TOPC, TOPRNS_1, EUCLID, FINSEQ_1, RVSUM_1, COMPLEX2,
      EUCLID_2, TOPREAL1, TOPMETR, RCOMP_1;
 constructors REAL_1, SQUARE_1, SEQ_1, SIN_COS, TOPRNS_1, COMPLEX1, COMPLEX2,
      EUCLID_2, TOPREAL1, TOPMETR, RCOMP_1, MEMBERED, ARYTM_0;
 clusters STRUCT_0, RELSET_1, EUCLID, TOPMETR, ARYTM_3, XREAL_0, MEMBERED,
      NUMBERS;
 requirements BOOLE, SUBSET, REAL, NUMERALS, ARITHM;


begin

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

definition let z be Element of 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 *];
end;

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

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

theorem :: EUCLID_3:3
for p ex z st p = cpx2euc(z);

theorem :: EUCLID_3:4
for z ex p st z=euc2cpx(p);

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

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

theorem :: EUCLID_3:7
(cpx2euc(z))`1=Re z & (cpx2euc(z))`2=Im z;

theorem :: EUCLID_3:8
Re euc2cpx(p)=p`1 & Im euc2cpx(p)=p`2;

theorem :: EUCLID_3:9
cpx2euc([* x1,x2 *])= |[x1,x2]|;

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

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

theorem :: EUCLID_3:12
[* (p1+p2)`1,(p1+p2)`2 *] = [* p1`1+p2`1,p1`2+p2`2 *];

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

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

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

theorem :: EUCLID_3:16
[* (-p)`1,(-p)`2 *]=[* -(p`1),-(p`2) *];

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

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

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

theorem :: EUCLID_3:20
cpx2euc(0c)= 0.REAL 2;

theorem :: EUCLID_3:21
euc2cpx(0.REAL 2)=0c;

theorem :: EUCLID_3:22
euc2cpx(p)=0c implies p=0.REAL 2;

theorem :: EUCLID_3:23
cpx2euc(([* r,0 *])*z)=r*(cpx2euc(z));

theorem :: EUCLID_3:24
[* r,0 *]*[* r1,r2 *] = [* r*r1,r*r2 *];

theorem :: EUCLID_3:25
euc2cpx(r*p)=([* r,0 *])*euc2cpx(p);

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

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

theorem :: EUCLID_3:28
    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:29
  |.cpx2euc(z).|=sqrt ((Re z)^2 + (Im z)^2);

theorem :: EUCLID_3:30
|.cpx2euc(z).|=|.z.|;

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

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

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

theorem :: EUCLID_3:33
for p holds 0<=Arg(p) & Arg(p)<2*PI;

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

theorem :: EUCLID_3:35
Arg(0.REAL 2)=0;

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

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

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

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

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

theorem :: EUCLID_3:41
for p st Arg(p)<>0 holds Arg(p)<PI iff sin (Arg(p))>0;

theorem :: EUCLID_3:42
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:43
for p1,p2,p3 holds 0<=angle(p1,p2,p3) & angle(p1,p2,p3)<2*PI;

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

theorem :: EUCLID_3:45
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:46
for p1,p2,p3 st angle(p1,p2,p3) <>0 holds
   angle(p3,p2,p1)=2*PI-angle(p1,p2,p3);

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

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

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

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

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

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

theorem :: EUCLID_3:53
for p1,p2 st p1<>0.REAL 2 & p2<>0.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.REAL 2,p2)=PI/2 or angle(p1,0.REAL 2,p2)=3/2*PI);

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

theorem :: EUCLID_3:55
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:56 :: Sum of inner angles of triangle
    for p1,p2,p3 st p2<>p1 & p1<>p3 & p3<>p2 &
  angle(p2,p1,p3)<PI & angle(p1,p3,p2)<PI & angle(p3,p2,p1)<PI holds
  angle(p2,p1,p3)+angle(p1,p3,p2)+angle(p3,p2,p1)=PI;

definition let n be 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 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 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 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 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:57
for n being Nat,p1,p2,p3,p being Point of TOP-REAL n st
 p in plane(p1,p2,p3) holds
 ex a1,a2,a3 being Real st a1+a2+a3=1 & p=a1*p1+a2*p2+a3*p3;

theorem :: EUCLID_3:58
for n being 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 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.REAL n holds a1=0 & a2=0;
  antonym q1,q2 are_ldependent2;
end;

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

theorem :: EUCLID_3:60
for n being Nat,p1,p2,p3,p0 being Point of TOP-REAL n st
p2-p1,p3-p1 are_lindependent2 & p0 in plane(p1,p2,p3)
holds (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:61
for n being 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:62
for n being 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:63
for p1,p2,p3 st p2-p1,p3-p1 are_lindependent2 holds
  plane(p1,p2,p3)=REAL 2;

definition let n be 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 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 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) -> map 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) -> map 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) -> map 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:64
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:65
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:66
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:67
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:68
for p1,p2,p3 st p2-p1,p3-p1 are_lindependent2 holds
 inside_of_triangle(p1,p2,p3) is non empty;
The abstract of the Mizar article:

Angle and Triangle in Euclidian Topological Space
