The Mizar article:

Inner Products and Angles of Complex Numbers

by
Wenpai Chang,
Yatsuka Nakamura, and
Piotr Rudnicki

Received May 29, 2003

Copyright (c) 2003 Association of Mizar Users

MML identifier: COMPLEX2
[ MML identifier index ]


environ

 vocabulary RLVECT_1, COMPLEX1, ARYTM_1, SQUARE_1, COMPLFLD, ARYTM, HAHNBAN1,
      FUNCT_1, RCOMP_1, SIN_COS, ARYTM_3, RELAT_1, COMPTRIG, COMPLEX2, PROB_2,
      XCMPLX_0, BOOLE, FINSEQ_6, INT_1, ABSVALUE;
 notation TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, SQUARE_1, NAT_1, RLVECT_1,
      RELAT_1, SEQ_1, RCOMP_1, SIN_COS, HAHNBAN1, COMPTRIG, XREAL_0, ORDINAL1,
      NUMBERS, ARYTM_0, INT_1, XCMPLX_0, REAL_1, COMPLEX1, COMPLFLD, ABSVALUE;
 constructors REAL_1, SQUARE_1, SEQ_1, RFUNCT_2, COMSEQ_3, GROUP_1, RCOMP_1,
      COMPLSP1, SIN_COS, HAHNBAN1, COMPTRIG, COMPLEX1, MEMBERED, ARYTM_0,
      ARYTM_3, FUNCT_4;
 clusters RELSET_1, SIN_COS, INT_1, COMPLEX1, XREAL_0, XCMPLX_0, MEMBERED,
      NUMBERS;
 requirements BOOLE, SUBSET, REAL, NUMERALS, ARITHM;
 theorems AXIOMS, REAL_1, REAL_2, SQUARE_1, JGRAPH_3, COMPLEX1, SIN_COS,
      COMPLFLD, HAHNBAN1, JORDAN6, COMPTRIG, XCMPLX_0, XCMPLX_1, RFUNCT_2,
      SIN_COS2, XREAL_0, XBOOLE_0, JGRAPH_5, INT_1, ABSVALUE, STRUCT_0,
      ARYTM_0;

begin

Lm1:
now let a, b, c be complex number; thus a+b-c = a+b+-c by XCMPLX_0:def 8
  .= a+(b+-c) by XCMPLX_1:1 .= a+(b-c) by XCMPLX_0:def 8; end;

Lm2:
now let a, b, c be complex number; assume a-b = -c; then a - b = -c-0;
  then a--c = b-0 by XCMPLX_1:24; hence a+c = b by XCMPLX_1:151; end;

Lm3:
now let a, b, c be complex number; assume a-b = c; then a-b=c-0;
  then a-c =b-0 by XCMPLX_1:24; hence a-c = b; end;

theorem Th1:
for a, b being Real holds -[*a,b*] = [*-a,-b*]
proof let a, b be Real; Re [*a,b*] = a & Im [*a,b*] = b by COMPLEX1:7;
 hence -[*a,b*] = [*-a,-b*] by COMPLEX1:def 11;
end;

theorem Th2:
for a, b being real number st b > 0
 ex r being real number st r = b*-[\ a/b /]+a & 0 <= r & r < b
proof let a, b be real number such that
A1: b > 0; set ab = [\ a/b /]; set i = -ab;
 take r = b*i+a; thus r = b*i+a;
A2: ab <= a/b & a/b-1 < ab by INT_1:def 4;
   then ab*b <= a/b*b by A1,AXIOMS:25; then ab*b <= a by A1,XCMPLX_1:88;
   then -(ab*b) >= -a by REAL_1:50; then i*b >= -a by XCMPLX_1:175;
   then b*i+a >= a+-a by AXIOMS:24;
 hence 0 <= r by XCMPLX_0:def 6;
    -(a/b-1) > i by A2,REAL_1:50; then (-(a/b-1))*b > i*b by A1,REAL_1:70;
   then (-(a/b)+1)*b > i*b by XCMPLX_1:162;
   then (-(a/b))*b+(1*b) > i*b by XCMPLX_1:8;
   then -(a/b*b)+b > i*b by XCMPLX_1:175; then -a+b > i*b by A1,XCMPLX_1:88;
   then -a+b+a > r by REAL_1:67;
   then a+-a+b > r by XCMPLX_1:1; then 0+b > r by XCMPLX_0:def 6;
  hence r < b;
end;

theorem Th3:
for a, b, c being real number st a > 0 & b >= 0 & c >= 0 & b < a & c < a
for i being Integer st b = c + a*i holds b = c
proof let a, b, c be real number such that
A1: a > 0 and A2: b >= 0 and A3: c >= 0 and A4: b < a and A5: c < a;
   let i be Integer such that
A6: b = c + a*i;
A7: 0+a <= c+a by A3,REAL_1:55;
   per cases;
   suppose i < 0; then i <= -1 by INT_1:21;
    then a*i <= a*(-1) by A1,AXIOMS:25; then a*i <= -a by XCMPLX_1:180;
    then c+a*i <= c+-a by REAL_1:55;
    hence b = c by A2,A5,A6,REAL_2:105;
   suppose i = 0; hence b = c by A6;
   suppose i > 0; then 0+1 <= i by INT_1:20;
    then a*i >= a by A1,REAL_2:146; then c+a*i >= c+a by REAL_1:55;
    hence b = c by A4,A6,A7,AXIOMS:22;
end;

theorem Th4:
for a, b being Real holds sin(a-b) = sin(a)*cos(b)-cos(a)*sin(b) &
                          cos(a-b) = cos(a)*cos(b)+sin(a)*sin(b)
proof let th1, th2 be Real;
  thus sin(th1-th2)=sin(th1+(-th2)) by XCMPLX_0:def 8
        .=sin.(th1+(-th2)) by SIN_COS:def 21
        .=(sin.(th1)) *(cos.(-th2))+(cos.(th1)) * (sin.(-th2)) by SIN_COS:79
        .=(sin.(th1)) *(cos.(th2))+(cos.(th1)) * (sin.(-th2)) by SIN_COS:33
        .=(sin.(th1)) *(cos.(th2))+(cos.(th1)) * -(sin.(th2)) by SIN_COS:33
        .=(sin.(th1)) *(cos.(th2))+-(cos.(th1)) *(sin.(th2)) by XCMPLX_1:175
        .=(sin.(th1)) *(cos.(th2))-(cos.(th1)) *(sin.(th2)) by XCMPLX_0:def 8
  .=(sin(th1)) *(cos.(th2))-(cos.(th1)) * (sin.(th2)) by SIN_COS:def 21
  .=(sin(th1)) *(cos(th2))-(cos.(th1)) * (sin.(th2)) by SIN_COS:def 23
  .=(sin(th1)) *(cos(th2))-(cos(th1)) * (sin.(th2)) by SIN_COS:def 23
  .=(sin(th1)) *(cos(th2))-(cos(th1)) * (sin(th2)) by SIN_COS:def 21;
  thus cos(th1-th2)=cos(th1+(-th2)) by XCMPLX_0:def 8
        .=cos.(th1+(-th2)) by SIN_COS:def 23
        .=(cos.(th1)) *(cos.(-th2))-(sin.(th1)) * (sin.(-th2)) by SIN_COS:79
        .=(cos.(th1)) *(cos.(th2))-(sin.(th1)) * (sin.(-th2)) by SIN_COS:33
        .=(cos.(th1)) *(cos.(th2))-(sin.(th1)) * -(sin.(th2)) by SIN_COS:33
        .=(cos.(th1)) *(cos.(th2))--(sin.(th1)) * (sin.(th2)) by XCMPLX_1:175
        .=(cos.(th1)) *(cos.(th2))+--(sin.(th1)) * (sin.(th2))by XCMPLX_0:def 8
  .=(cos(th1)) *(cos.(th2))+(sin.(th1)) * (sin.(th2)) by SIN_COS:def 23
  .=(cos(th1)) *(cos(th2))+(sin.(th1)) * (sin.(th2)) by SIN_COS:def 23
  .=(cos(th1)) *(cos(th2))+(sin(th1)) * (sin.(th2)) by SIN_COS:def 21
  .=(cos(th1)) *(cos(th2))+(sin(th1)) * (sin(th2)) by SIN_COS:def 21;
  end;

theorem
 for a being Real holds sin.(a-PI) = -sin.a & cos.(a-PI) = -cos.a
   proof let th be Real;
    thus sin.(th- PI) = sin.(th+(-PI)) by XCMPLX_0:def 8
       .= (sin.(th))* (cos.(-PI)) + (cos.(th)) *( sin.(-PI)) by SIN_COS:79
       .= (sin.(th))* (cos.(PI)) + (cos.(th)) *(sin.(-PI)) by SIN_COS:33
       .= (sin.(th))* (cos.(PI)) + (cos.(th)) *(-(sin.(PI))) by SIN_COS:33
       .= -(1)*sin.(th) by SIN_COS:81,XCMPLX_1:175 .= -sin.th;
    thus cos.(th- PI) = cos.(th+(-PI)) by XCMPLX_0:def 8
       .= (cos.(th)) * (cos.(-PI)) - ( sin.(th)) *( sin.(-PI)) by SIN_COS:79
       .= (cos.(th)) * (cos.(PI)) - ( sin.(th)) *( sin.(-PI)) by SIN_COS:33
       .= (cos.(th)) * (cos.(PI)) - ( sin.(th)) *(-(sin.(PI))) by SIN_COS:33
       .= -(1)*cos.(th) by SIN_COS:81,XCMPLX_1:175 .= -cos.th;
   end;

theorem Th6:
for a being Real holds sin(a-PI) = -sin a & cos(a-PI) = -cos a
proof let r be Real;
  thus sin (r-PI) = sin(r)*cos(PI)-cos(r)*sin(PI) by Th4
  .= -sin r by SIN_COS:82,XCMPLX_1:180;
 thus cos (r-PI) = cos(r)*cos(PI)+sin(r)*sin(PI) by Th4
    .= -cos r by SIN_COS:82,XCMPLX_1:180;
end;

theorem Th7:
for a, b being real number st a in ].0,PI/2.[ & b in ].0,PI/2.[
 holds a < b iff sin a < sin b
proof let a, b be real number such that
A1: a in ].0,PI/2.[ & b in ].0,PI/2.[;
A2: sin a = sin.a & sin b = sin.b by SIN_COS:def 21;
    a in REAL & b in REAL & dom sin = REAL by SIN_COS:def 20,XREAL_0:def 1;
then A3: a in ].0,PI/2.[ /\ dom sin & b in ].0,PI/2.[ /\ dom sin
   by A1,XBOOLE_0:def 3;
   hence a < b implies sin a < sin b by A1,A2,RFUNCT_2:def 2,SIN_COS2:2;
   assume A4: sin a < sin b; assume a >= b;
   then a > b by A4,REAL_1:def 5;
   hence contradiction by A1,A2,A3,A4,RFUNCT_2:def 2,SIN_COS2:2;
end;

theorem Th8:
for a, b being real number st a in ].PI/2,PI.[ & b in ].PI/2,PI.[
 holds a < b iff sin a > sin b
proof let a, b be real number such that
A1: a in ].PI/2,PI.[ & b in ].PI/2,PI.[;
A2: sin a = sin.a & sin b = sin.b by SIN_COS:def 21;
    a in REAL & b in REAL & dom sin = REAL by SIN_COS:def 20,XREAL_0:def 1;
then A3: a in ].PI/2,PI.[ /\ dom sin & b in ].PI/2,PI.[ /\ dom sin
   by A1,XBOOLE_0:def 3;
   hence a < b implies sin a > sin b by A1,A2,RFUNCT_2:def 3,SIN_COS2:3;
   assume A4: sin a > sin b; assume a >= b; then a > b by A4,REAL_1:def 5;
   hence contradiction by A1,A2,A3,A4,RFUNCT_2:def 3,SIN_COS2:3;
end;

theorem Th9:
for a being Real, i being Integer holds sin a = sin (2*PI*i+a)
proof let r being Real, i being Integer;
A1: sin.r = sin r by SIN_COS:def 21;
A2: sin.(2*PI*i+r) = sin (2*PI*i+r) by SIN_COS:def 21;
A3: sin.(2*PI*(-i)+(2*PI*i+r)) = sin (2*PI*(-i)+(2*PI*i+r)) by SIN_COS:def 21;
 per cases;
 suppose i >= 0; then reconsider iN = i as Nat by INT_1:16;
        sin r = sin (2*PI*iN+r) by A1,A2,SIN_COS2:10;
  hence sin r = sin (2*PI*i+r);
 suppose i < 0; then -i > 0 by REAL_1:66;
   then reconsider iN = -i as Nat by INT_1:16;
 A4: r = 2*PI*0+r .= 2*PI*(-i+i)+r by XCMPLX_0:def 6
   .= 2*PI*iN+2*PI*i+r by XCMPLX_1:8 .= 2*PI*iN+(2*PI*i+r) by XCMPLX_1:1;
    reconsider aa = 2*PI*i+r as Real by XREAL_0:def 1;
    sin (aa) = sin (2*PI*iN+aa) by A2,A3,SIN_COS2:10;
  hence sin r = sin (2*PI*i+r) by A4;
end;

theorem Th10:
for a being Real, i being Integer holds cos a = cos (2*PI*i+a)
proof let r being Real, i being Integer;
A1: cos.r = cos r by SIN_COS:def 23;
A2: cos.(2*PI*i+r) = cos (2*PI*i+r) by SIN_COS:def 23;
A3: cos.(2*PI*(-i)+(2*PI*i+r)) = cos (2*PI*(-i)+(2*PI*i+r)) by SIN_COS:def 23;
 per cases;
 suppose i >= 0; then reconsider iN = i as Nat by INT_1:16;
        cos r = cos (2*PI*iN+r) by A1,A2,SIN_COS2:11;
  hence cos r = cos (2*PI*i+r);
 suppose i < 0; then -i > 0 by REAL_1:66;
   then reconsider iN = -i as Nat by INT_1:16;
 A4: r = 2*PI*0+r .= 2*PI*(-i+i)+r by XCMPLX_0:def 6
   .= 2*PI*iN+2*PI*i+r by XCMPLX_1:8 .= 2*PI*iN+(2*PI*i+r) by XCMPLX_1:1;
    reconsider aa = 2*PI*i+r as Real by XREAL_0:def 1;
    cos (aa) = cos (2*PI*iN+aa) by A2,A3,SIN_COS2:11;
  hence cos r = cos (2*PI*i+r) by A4;
end;

theorem Th11:
for a being Real st sin a = 0 holds cos a <> 0
proof let a be Real; consider r being real number such that
A1: r = 2*PI*-[\ a/(2*PI) /]+a and
A2: 0 <= r & r < 2*PI by Th2,COMPTRIG:21;
A3: sin a = sin r by A1,Th9;
A4: cos a = cos r by A1,Th10; assume sin a = 0 & cos a = 0;
  then (r = 0 or r = PI) & (r = PI/2 or r = 3/2*PI) by A2,A3,A4,COMPTRIG:33,34
;
  hence thesis by COMPTRIG:21;
end;

theorem Th12:
for a, b being Real
 st 0 <= a & a < 2*PI & 0 <= b & b < 2*PI & sin a = sin b & cos a = cos b
  holds a = b
proof let r, s be Real such that
A1: 0 <= r and A2: r < 2*PI and A3: 0 <= s and A4: s < 2*PI and
A5: sin r = sin s and A6: cos r = cos s;
A7: cos(r-s)=(cos r)*(cos s)+(sin r)*(sin s) by Th4 .= 1 by A5,A6,SIN_COS:32;
A8: cos (s-r)=(cos r)*(cos s)+(sin r)*(sin s) by Th4 .= 1 by A5,A6,SIN_COS:32;
A9: sin(r-s)=(sin r)*(cos s)-(cos r)*(sin s) by Th4 .= 0 by A5,A6,XCMPLX_1:14;
A10: sin (s-r)=(sin s)*(cos r)-(cos s)*(sin r) by Th4 .= 0 by A5,A6,XCMPLX_1:14
;
  per cases by REAL_1:def 5;
  suppose r > s; then r > s+0;
  then A11: 0 <= r-s by REAL_1:86; r+0 < 2*PI+s by A2,A3,REAL_1:67;
      then r-s < 2*PI by REAL_1:84; then r-s = 0 or r-s = PI by A9,A11,COMPTRIG
:33;
   hence r = s by A7,SIN_COS:82,XCMPLX_1:15;
  suppose r < s; then s > r+0;
  then A12: 0 <= s-r by REAL_1:86; s+0 < 2*PI+r by A1,A4,REAL_1:67;
      then s-r < 2*PI by REAL_1:84; then s-r = 0 or s-r = PI by A10,A12,
COMPTRIG:33;
   hence r = s by A8,SIN_COS:82,XCMPLX_1:15;
  suppose r = s; hence thesis;
end;

Lm4: the carrier of F_Complex=COMPLEX by COMPLFLD:def 1;

begin :: More on the argument of a complex number
      :: ALL these to be changed (mainly deleted) after the change in COMPTRIG

definition
  cluster F_Complex -> non empty;
  coherence by Lm4,STRUCT_0:def 1;
end;

definition let z be Element of COMPLEX;
 func F_tize(z) -> Element of F_Complex equals :Def1: z;
 correctness by COMPLFLD:def 1;
end;

theorem Th13:
for z being Element of COMPLEX holds Re z = Re F_tize z & Im z = Im F_tize z
proof let z be Element of COMPLEX;
   z=F_tize(z) by Def1; hence thesis by HAHNBAN1:def 3,def 4;
end;

theorem
 for x, y being Element of COMPLEX holds F_tize(x+y) = F_tize(x)+F_tize(y)
proof let z1, z2 be Element of COMPLEX;
A1: F_tize(z1+z2)=z1+z2 by Def1;A2:F_tize(z1)=z1 by Def1; F_tize(z2)=z2 by Def1
;
 hence thesis by A1,A2,COMPLFLD:3;
end;

theorem
for z being Element of COMPLEX holds z = 0c iff F_tize z = 0.F_Complex
 by Def1,COMPLFLD:9;

theorem Th16:
for z being Element of COMPLEX holds |.z.| = |. F_tize z .|
proof let z be Element of COMPLEX; consider z' be Element of COMPLEX such that
A1: F_tize(z) = z' & |.F_tize(z).| = |.z'.| by COMPLFLD:def 3;
 thus |.z.|=|.F_tize(z).| by A1,Def1;
end;

definition let z be Element of COMPLEX;
 func Arg(z) -> Real equals :Def2:
   Arg(F_tize(z));
 correctness;
end;

theorem Th17:
for z being Element of COMPLEX, u being Element of F_Complex
 st z = u holds Arg z = Arg u
proof let z be Element of COMPLEX, z1 be Element of F_Complex;
 assume z=z1; then z1=F_tize(z) by Def1; hence Arg(z)=Arg(z1) by Def2;
end;

theorem Th18:
for z being Element of COMPLEX holds 0 <= Arg z & Arg z < 2*PI
proof let z be Element of COMPLEX;
   0<=Arg(F_tize(z)) & Arg(F_tize(z))<2*PI by COMPTRIG:52;
 hence thesis by Def2;
end;

L0: 0c = [*0,0*] by ARYTM_0:def 7;

theorem Th19:
for z being Element of COMPLEX holds z = [* |.z.|*cos Arg z, |.z.|*sin Arg z *]
proof let a be Element of COMPLEX;
 set Fa = F_tize a;
 per cases;
 suppose a <> 0; then A1: Fa <> 0.F_Complex by Def1,COMPLFLD:9;
A2: Fa = a by Def1;
A3: Arg Fa = Arg a by Def2;
   consider z' being Element of COMPLEX such that
A4: Fa = z' & |.Fa.| = |.z'.| by COMPLFLD:def 3;
 thus a = Fa by Def1
       .= [** |.Fa.|*cos Arg Fa, |.Fa.|*sin Arg Fa **] by A1,COMPTRIG:def 1
       .= [* |.a.|*cos Arg a, |.a.|*sin Arg a *] by A2,A3,A4,HAHNBAN1:def 1;
  suppose a = 0c;
   hence thesis by COMPLEX1:130,L0;
end;

theorem Th20:
Arg 0c = 0
proof thus Arg(0c)=Arg F_tize(0c) by Def2 .=Arg(0.F_Complex) by Def1,COMPLFLD:9
 .=0
            by COMPTRIG:def 1;
end;

theorem Th21:
for z being Element of COMPLEX, r being Real
 st z <> 0 & z = [* |.z.|*cos r, |.z.|*sin r *] & 0 <= r & r < 2*PI
  holds r = Arg z
proof let z be Element of COMPLEX, r being Real such that
A1: z <> 0 and
A2: z = [* |.z.|*cos r, |.z.|*sin r *] and
A3: 0 <= r and
A4: r < 2*PI; set zf = F_tize(z);
A5: z = zf by Def1;
A6: |.z.| = |.zf.| by Th16;
A7: zf <> 0.F_Complex by A1,Def1,COMPLFLD:9;
    zf = [** |.zf.|*cos r, |.zf.|*sin r **] by A2,A5,A6,HAHNBAN1:def 1;
 hence r = Arg zf by A3,A4,A7,COMPTRIG:def 1 .= Arg z by Def2;
end;

theorem Th22:
for z being Element of COMPLEX st z <> 0c
 holds (Arg z < PI implies Arg -z = Arg z +PI) &
       (Arg z >= PI implies Arg -z = Arg z -PI)
proof let z be Element of COMPLEX; assume A1: z <> 0c;
then A2: |.z.| <> 0 by COMPLEX1:131;
A3: -z <> 0c by A1,XCMPLX_1:135;
A4: z = [* |.z.|*cos Arg z, |.z.|*sin Arg z *] by Th19;
A5: -z = [* |.-z.|*cos Arg -z, |.-z.|*sin Arg -z *] by Th19;
A6: -z = [* -|.z.|*cos Arg z, -|.z.|*sin Arg z *] by A4,Th1;
A7: |.z.| = |.-z.| by COMPLEX1:138;
   then |.z.|*cos Arg -z = -|.z.|*cos Arg z by A5,A6,ARYTM_0:12;
   then |.z.|*cos Arg -z = |.z.|*-cos Arg z by XCMPLX_1:175;
   then cos Arg -z = -cos Arg z by A2,XCMPLX_1:5;
then A8: cos Arg -z = cos (Arg z +PI) & cos Arg -z = cos (Arg z -PI)
    by Th6,SIN_COS:84;
    |.z.|*sin Arg -z = -|.z.|*sin Arg z by A5,A6,A7,ARYTM_0:12;
   then |.z.|*sin Arg -z = |.z.|*-sin Arg z by XCMPLX_1:175;
   then sin Arg -z = -sin Arg z by A2,XCMPLX_1:5;
then A9: sin Arg -z = sin (Arg z +PI) & sin Arg -z = sin (Arg z -PI)
    by Th6,SIN_COS:84;
  hereby assume Arg z<PI; then Arg z+PI<PI+PI by REAL_1:67;
   then A10: Arg z +PI < 2*PI by XCMPLX_1:11;
        0 <= Arg z by Th18; then 0+0 <= Arg z +PI by COMPTRIG:21,REAL_1:55;
    hence Arg -z = Arg z +PI by A3,A5,A8,A9,A10,Th21;
  end;
  assume Arg z >= PI; then Arg z -PI >= PI-PI by REAL_1:49;
   then A11: Arg z -PI >= 0 by XCMPLX_1:14;
       Arg z < 2*PI by Th18; then Arg z +0 < 2*PI+PI by COMPTRIG:21,REAL_1:67;
      then Arg z -PI < 2*PI by REAL_1:84;
    hence Arg -z = Arg z -PI by A3,A5,A8,A9,A11,Th21;
end;

theorem Th23:
for r being Real st r >= 0 holds Arg [*r,0*] = 0
proof let r be Real such that
A1: r >= 0; Re [*r,0*] = r & Im [*r,0*] = 0 by COMPLEX1:7;
then A2:  |.[*r,0*].| = abs(r) by COMPLEX1:136 .= r by A1,ABSVALUE:def 1;
    [*r,0*] = [*|.[*r,0*].|*cos Arg [*r,0*], |.[*r,0*].|*sin Arg [*r,0*] *]
     by Th19;
then A3: r =|.[*r,0*].|*cos Arg[*r,0*]&0=|.[*r,0*].|*sin Arg [*r,0*] by ARYTM_0
:12;
   per cases by A1;
   suppose r = 0;
    hence Arg [*r,0*] = 0 by Th20,L0;
   suppose A4: r > 0;
   then A5: cos Arg [*r,0*] = 1 by A2,A3,XCMPLX_1:7;
   A6: sin Arg [*r,0*] = 0 by A2,A3,A4,XCMPLX_1:6;
        0 <= Arg [*r,0*] & Arg [*r,0*] < 2*PI by Th18;
    hence Arg [*r,0*] = 0 by A5,A6,Th12,SIN_COS:34;
end;

theorem Th24:
for z being Element of COMPLEX holds Arg z = 0 iff z = [* |.z.|,0 *]
proof let z be Element of COMPLEX;
 hereby
 assume A1: Arg z=0;
  A2: z=F_tize(z) by Def1;
  A3: Arg(z)=Arg(F_tize(z)) by Def2;
  A4: |.z.|=|.F_tize(z).| by Th16;
   now per cases;
  case z<>0.F_Complex;
    then A5: z=[** |.z.|*cos 0,|.z.|*sin 0 **] by A1,A2,A3,A4,COMPTRIG:def 1;
Im z=Im (F_tize(z)) by Th13;
   hence z=[* |.z.|,0 *] & Im z=0 by A2,A5,HAHNBAN1:15,def 1,SIN_COS:34;
  case z=0.F_Complex;
   hence z=[* |.z.|,0 *] & Im z=0 by COMPLEX1:12,130,L0,COMPLFLD:9;
  end;
 hence z=[* |.z.|,0 *];
 end;
 assume A6: z=[* |.z.|,0 *]; |.z.| >= 0 by COMPLEX1:132;
 hence Arg z = 0 by A6,Th23;
end;

theorem Th25:
for z being Element of COMPLEX st z <> 0c holds Arg(z) < PI iff Arg -z >= PI
proof let z be Element of COMPLEX;
 assume A1: z<>0c;
  thus Arg(z)<PI implies Arg(-z)>=PI
   proof assume A2: Arg(z)<PI;
      Arg(z)>=0 by Th18; then PI+0<=PI+Arg(z) by REAL_1:55;
    hence Arg(-z)>=PI by A1,A2,Th22;
   end;
  thus Arg(-z)>=PI implies Arg(z)<PI
   proof assume Arg(-z)>=PI; then A3: Arg(--z)=Arg(-z)-PI by A1,Th22,REAL_1:26
; 2*PI>Arg(-z) by Th18;
     then PI+PI>Arg(-z) by XCMPLX_1:11; then PI+PI-PI>Arg(-z)-PI by REAL_1:54
;
    hence Arg(z)<PI by A3,XCMPLX_1:26;
   end;
end;

theorem Th26:
for x, y being Element of COMPLEX st x <> y or x-y <> 0c
 holds Arg(x-y) < PI iff Arg(y-x) >= PI
proof let z1,z2 be Element of COMPLEX; assume z1<>z2 or z1-z2<>0c;
  then z1-z2<>0c by XCMPLX_1:15; then (Arg(z1-z2)<PI iff Arg(-(z1-z2))>=PI)
by Th25;
 hence (Arg(z1-z2)<PI iff Arg(z2-z1)>=PI) by XCMPLX_1:143;
end;

theorem Th27:
for z being Element of COMPLEX holds Arg z in ].0,PI.[ iff Im z > 0
proof let z be Element of COMPLEX;
  A1: Arg(z)=Arg(F_tize(z)) by Def2;
 thus Arg z in ].0,PI.[ implies Im z > 0 proof assume Arg z in ].0,PI.[;
  then A2: 0<Arg(z) & Arg(z)<PI by JORDAN6:45;
  A3: Arg(z)<PI/2 or Arg(z)=PI/2 or Arg(z)>PI/2 by REAL_1:def 5;
   now per cases by A2,A3,JORDAN6:45;
  case Arg(z) in ].0,PI/2.[; then Im F_tize(z) >0 by A1,COMPTRIG:59;
   hence Im z>0 by Th13;
  case Arg(z)=PI/2; then Im (F_tize(z))>0 by A1,COMPTRIG:66,SIN_COS:82;
   hence Im z>0 by Th13;
  case Arg(z) in ].PI/2,PI.[; then Im F_tize(z) >0 by A1,COMPTRIG:60;
   hence Im z>0 by Th13;
  end;
  hence Im z>0;
 end;
 A4: ].0,PI/2.[ c= ].0,PI.[ by COMPTRIG:21,JGRAPH_3:9;
 A5: ].PI/2,PI.[ c= ].0,PI.[ by COMPTRIG:21,JGRAPH_3:9;
 thus Im z > 0 implies Arg z in ].0,PI.[
 proof assume Im z >0;
   then A6: Im F_tize(z) >0 by Th13;
    now per cases;
   case Re F_tize(z)>0; then Arg(F_tize(z)) in ].0,PI/2.[ by A6,COMPTRIG:59;
     hence Arg(z) in ].0,PI.[ by A1,A4;
   case Re F_tize(z)=0; then F_tize(z)=[** 0,Im F_tize(z) **] by COMPTRIG:9;
     then Arg(F_tize(z))=PI/2 by A6,COMPTRIG:55;
     hence Arg(z) in ].0,PI.[ by A1,COMPTRIG:21,JORDAN6:45;
   case Re F_tize(z)<0; then Arg(F_tize(z)) in ].PI/2,PI.[ by A6,COMPTRIG:60;
     hence Arg(z) in ].0,PI.[ by A1,A5;
   end;
  hence Arg z in ].0,PI.[;
 end;
end;

theorem
 for z being Element of COMPLEX st Arg z <> 0 holds Arg z < PI iff sin Arg z >
0
proof let z be Element of COMPLEX;
 assume A1: Arg(z)<>0; A2: Arg(z)>=0 by Th18;
  A3: Arg(z)=Arg(F_tize(z)) by Def2;
 thus Arg(z)<PI implies sin (Arg(z))>0
  proof assume Arg(z)<PI; then Arg(z) in ].0,PI.[ by A1,A2,JORDAN6:45;
   then Im (z)>0 by Th27; then Im (F_tize(z))>0 by Th13;
   hence sin (Arg(z))>0 by A3,COMPTRIG:63;
  end;
 A4: ].0,PI/2.[ c= ].0,PI.[ by COMPTRIG:21,JGRAPH_3:9;
 thus sin (Arg(z))>0 implies Arg(z)<PI
 proof assume sin (Arg(z))>0;
   then A5: Im (F_tize(z))>0 by A3,COMPTRIG:66;
    now per cases;
   case Re F_tize(z)>0; then Arg(F_tize(z)) in ].0,PI/2.[ by A5,COMPTRIG:59;
     hence Arg(z)<PI by A3,A4,JORDAN6:45;
   case Re F_tize(z)=0; then F_tize(z)=[** 0,Im F_tize(z) **] by COMPTRIG:9;
    hence Arg(z)<PI by A3,A5,COMPTRIG:21,55;
   case Re F_tize(z)<0; then Arg(F_tize(z)) in ].PI/2,PI.[ by A5,COMPTRIG:60;
    hence Arg(z)<PI by A3,JORDAN6:45;
   end;
  hence Arg(z)<PI;
 end;
end;

theorem
 for x, y being Element of COMPLEX st Arg x < PI & Arg y < PI
 holds Arg(x+y) < PI
proof let z1,z2 be Element of COMPLEX;
 assume A1: Arg(z1)<PI & Arg(z2)<PI;
  A2: Arg(z1+z2)=Arg(F_tize(z1+z2)) by Def2;
  A3: z1+z2=F_tize(z1+z2) by Def1;
   now per cases by Th18;
  case Arg(z1)=0; then A4: z1=[* |.z1.|,0 *] by Th24;
   then A5: z1=[* |.z1.|,0 *] & Im z1=0 by COMPLEX1:7;
    now per cases by Th18;
   case Arg(z2)=0; then A6: z2=[* |.z2.|,0 *] by Th24;
     then A7: z2=[* |.z2.|,0 *] & Im z2=0 by COMPLEX1:7;
     A8: Im (z1+z2)=(Im z1)+(Im z2) by COMPLEX1:19;
     A9: Re z2=|.z2.| by A6,COMPLEX1:7;
      now per cases;
     case A10: z1+z2=0c;
        Arg (z1+z2)=Arg(F_tize(z1+z2)) by Def2 .=Arg(0.F_Complex) by A10,Def1,
COMPLFLD:9
                .=0 by COMPTRIG:def 1;
      hence Arg(z1+z2)<PI by COMPTRIG:21;
     case z1+z2<>0c;
        Re (z1+z2)=Re z1 + Re z2 by COMPLEX1:19 .=|.z1.| + |.z2.| by A4,A9,
COMPLEX1:7;
       then z1+z2 = [* |.z1.| + |.z2.|,0 *] by A5,A7,A8,COMPLEX1:8;
       then A11: z1+z2=[** |.z1.| + |.z2.|,0 **] by HAHNBAN1:def 1;
       A12: 0<= |.z1.| by COMPLEX1:132; 0<= |.z2.| by COMPLEX1:132;
       then 0+0 <= |.z1.| + |.z2.| by A12,REAL_1:55;
      hence Arg(z1+z2)<PI by A2,A3,A11,COMPTRIG:21,53;
     end;
    hence Arg(z1+z2)<PI;
   case Arg(z2)>0; then Arg(z2) in ].0,PI.[ by A1,JORDAN6:45;
     then A13: Im z2>0 by Th27; Im (z1+z2)=(Im z1)+(Im z2) by COMPLEX1:19;
     then Arg(z1+z2) in ].0,PI.[ by A5,A13,Th27;
    hence Arg(z1+z2)<PI by JORDAN6:45;
   end;
   hence Arg(z1+z2)<PI;
  case Arg(z1)>0; then Arg(z1) in ].0,PI.[ by A1,JORDAN6:45;
   then A14: Im z1>0 by Th27;
    now per cases by Th18;
   case Arg(z2)=0; then z2=[* |.z2.|,0 *] by Th24;
     then A15: z2=[* |.z2.|,0 *] & Im z2=0 by COMPLEX1:7;
      Im (z1+z2)=(Im z1)+(Im z2) by COMPLEX1:19;
     then Arg(z1+z2) in ].0,PI.[ by A14,A15,Th27;
    hence Arg(z1+z2)<PI by JORDAN6:45;
   case Arg(z2)>0; then Arg(z2) in ].0,PI.[ by A1,JORDAN6:45;
     then A16: Im z2>0 by Th27; Im (z1+z2)=(Im z1)+(Im z2) by COMPLEX1:19;
     then Im (z1+z2)>0+0 by A14,A16,REAL_1:67; then Arg(z1+z2) in ].0,PI.[ by
Th27;
    hence Arg(z1+z2)<PI by JORDAN6:45;
   end;
   hence Arg(z1+z2)<PI;
  end;
 hence Arg(z1+z2)<PI;
end;

theorem Th30:
for x be Real st x > 0 holds Arg [*0,x*] = PI/2
proof let x be Real such that
A1: x > 0; A2: F_tize [*0,x*] = [*0,x*] by Def1.= [** 0, x **] by HAHNBAN1:def
1;
  thus Arg [*0,x*] = Arg F_tize [*0,x*] by Def2
   .= PI/2 by A1,A2,COMPTRIG:55;
end;

theorem Th31:
for z be Element of COMPLEX holds Arg z in ].0,PI/2.[ iff Re z > 0 & Im z > 0
proof let z be Element of COMPLEX;
A1: F_tize z = z by Def1;
   consider z' being Element of COMPLEX such that
A2: F_tize z = z' & Re F_tize z = Re z' by HAHNBAN1:def 3;
   consider z'' being Element of COMPLEX such that
A3: F_tize z = z'' & Im F_tize z = Im z'' by HAHNBAN1:def 4;
    Arg z = Arg F_tize z by Def2;
  hence Arg z in ].0,PI/2.[ iff Re z > 0 & Im z > 0 by A1,A2,A3,COMPTRIG:59;
end;

theorem Th32:
for z be Element of COMPLEX holds Arg z in ].PI/2,PI.[ iff Re z < 0 & Im z > 0
proof let z be Element of COMPLEX;
A1: F_tize z = z by Def1;
   consider z' being Element of COMPLEX such that
A2: F_tize z = z' & Re F_tize z = Re z' by HAHNBAN1:def 3;
   consider z'' being Element of COMPLEX such that
A3: F_tize z = z'' & Im F_tize z = Im z'' by HAHNBAN1:def 4;
    Arg z = Arg F_tize z by Def2;
  hence Arg z in ].PI/2,PI.[ iff Re z < 0 & Im z > 0 by A1,A2,A3,COMPTRIG:60;
end;

theorem Th33:
for z be Element of COMPLEX st Im z > 0 holds sin Arg z > 0
proof let z be Element of COMPLEX; assume
A1: Im z > 0;
A2: F_tize z = z by Def1; consider z'' being Element of COMPLEX such that
A3: F_tize z = z'' & Im F_tize z = Im z'' by HAHNBAN1:def 4;
    Arg z = Arg F_tize z by Def2;
 hence sin Arg z > 0 by A1,A2,A3,COMPTRIG:63;
end;

theorem Th34:
for z being Element of COMPLEX holds Arg z = 0 iff Re z >= 0 & Im z = 0
proof let z being Element of COMPLEX;
  hereby assume Arg z = 0; then z = [*|.z.|,0*] by Th24;
     then Re z = |.z.| & Im z = 0 by COMPLEX1:7;
   hence Re z >= 0 & Im z = 0 by COMPLEX1:132;
  end;
A1: Arg z = Arg F_tize z by Def2;
 assume A2: Re z >= 0 & Im z = 0; then z = [* Re z, 0 *] by COMPLEX1:8;
  then F_tize z = [*Re z,0*] by Def1.= [** Re z, 0 **] by HAHNBAN1:def 1;
 hence Arg z = 0 by A1,A2,COMPTRIG:53;
end;

theorem Th35:
for z being Element of COMPLEX holds Arg z = PI iff Re z < 0 & Im z=0
proof let z be Element of COMPLEX;
  A1: z=F_tize(z) by Def1;
  A2: Arg(z)=Arg(F_tize(z)) by Def2;
  A3: |.z.|=|.F_tize(z).| by Th16;
 hereby assume A4: Arg z = PI;
  per cases;
  suppose A5: z<>0.F_Complex;
    then z=[** |.z.|*cos PI,|.z.|*sin PI **] by A1,A2,A3,A4,COMPTRIG:def 1;
    then z=[* |.z.|*-1,0 *] by HAHNBAN1:def 1,SIN_COS:82;
    then z=[* -|.z.|,0 *] by XCMPLX_1:180;
    then A6: Re z = -|.z.| & Im z = 0 by COMPLEX1:7; --|.z.| > 0 by A5,COMPLEX1
:133,COMPLFLD:9;
    hence Re z < 0 & Im z = 0 by A6,REAL_1:66;
  suppose z=0.F_Complex;
    hence Re z < 0 & Im z = 0 by A4,Th20,COMPLFLD:9,COMPTRIG:21;
 end;
A7: Arg z = Arg F_tize z by Def2;
 assume A8: Re z < 0 & Im z=0; then z = [* Re z, 0 *] by COMPLEX1:8;
  then F_tize z = [*Re z,0*] by Def1.= [** Re z, 0 **] by HAHNBAN1:def 1;
 hence Arg z = PI by A7,A8,COMPTRIG:54;
end;

theorem Th36:
for z being Element of COMPLEX holds Im z = 0 iff Arg z = 0 or Arg z = PI
proof let z be Element of COMPLEX;
 hereby assume A1: Im z = 0; Re z >= 0 or Re z < 0;
 then A2: Arg [**Re z,0**] = 0 or Arg [**Re z,0**] = PI by COMPTRIG:53,54;
     [**Re z,0**] = [*Re z,0*] by HAHNBAN1:def 1 .= z by A1,COMPLEX1:8;
  hence Arg z = 0 or Arg z = PI by A2,Th17;
 end;
 assume Arg z = 0 or Arg z = PI;
 hence Im z = 0 by Th34,Th35;
end;

theorem Th37:
for z being Element of COMPLEX st Arg z <= PI holds Im z >= 0
proof let z be Element of COMPLEX;
 assume A1: Arg z <= PI;
 per cases by A1,Th18,REAL_1:def 5;
  suppose Arg z = PI or Arg z = 0; hence Im z >= 0 by Th36;
  suppose 0 < Arg z & Arg z < PI; then Arg z in ].0,PI.[ by JORDAN6:45;
  hence Im z >= 0 by Th27;
end;

theorem Th38:
for z being Element of COMPLEX st z <> 0
 holds cos Arg -z = -cos Arg z & sin Arg -z = - sin Arg z
proof let a be Element of COMPLEX; assume
A1: a <> 0;
A2: a = [*|.a.|*cos Arg a, |.a.|*sin Arg a*] by Th19;
 -a = [*|.-a.|*cos Arg -a, |.-a.|*sin Arg -a*] by Th19;
then A3: Re a = |.a.|*cos Arg a & Im a = |.a.|*sin Arg a &
    Re -a = |.-a.|*cos Arg -a & Im -a = |.-a.|*sin Arg -a by A2,COMPLEX1:7;
A4: |.-a.| = |.a.| by COMPLEX1:138;
A5: [*0,0*] = a+-a by L0,XCMPLX_0:def 6
  .= [* |.a.|*cos Arg a + (|.a.|*cos Arg -a),
        |.a.|*sin Arg a + (|.a.|*sin Arg -a)*] by A3,A4,COMPLEX1:def 9;
   then |.a.|*cos Arg a + |.a.|*cos Arg -a = 0 by ARYTM_0:12;
then A6: |.a.|*(cos Arg a + cos Arg -a) = 0 by XCMPLX_1:8;
    |.a.|*sin Arg a + |.a.|*sin Arg -a = 0 by A5,ARYTM_0:12;
then A7: |.a.|*(sin Arg a+sin Arg -a)= 0 by XCMPLX_1:8; |.a.|<>0 by A1,COMPLEX1
:131;
   then cos Arg a +--cos Arg -a = 0 & sin Arg a +--sin Arg -a = 0 by A6,A7,
XCMPLX_1:6;
  hence cos Arg -a = - cos Arg a & sin Arg -a = - sin Arg a by XCMPLX_1:136;
end;

theorem Th39:
for a being Element of COMPLEX st a <> 0
 holds cos Arg a = Re a / |.a.| & sin Arg a = Im a / |.a.|
proof let a be Element of COMPLEX; assume a <> 0;
then A1: |.a.|<>0 by COMPLEX1:131; a = [* |.a.|*cos Arg a,|.a.|*sin Arg a*] by
Th19;
   then Re a = |.a.|*cos Arg a & Im a = |.a.|*sin Arg a by COMPLEX1:7;
 hence cos Arg a = Re a / |.a.| & sin Arg a = Im a / |.a.| by A1,XCMPLX_1:90;
end;

theorem Th40:
for a being Element of COMPLEX, r being Real st r > 0
 holds Arg(a*[*r,0*]) = Arg a
proof let a be Element of COMPLEX, r be Real such that
 A1: r > 0;
 per cases; suppose a = 0; hence Arg(a*[*r,0*]) = Arg a;
 suppose A2: a <> 0; set b = a*[*r,0*];
  A3: Re [*r,0*] = r & Im [*r,0*] = 0 by COMPLEX1:7;
  then A4: Re b = Re a * r - 0*Im a by COMPLEX1:24 .= r*Re a;
  A5: Im b = Re a * 0 + r * Im a by A3,COMPLEX1:24 .= r*Im a;
  A6: |.b.| = |.a.|*|.[*r,0*].| by COMPLEX1:151
          .= |.a.|*abs r by A3,COMPLEX1:136 .= |.a.|*r by A1,ABSVALUE:def 1;
       |.a.| <> 0 by A2,COMPLEX1:131; then A7: |.b.| <> 0 by A1,A6,XCMPLX_1:6;
  A8: cos Arg a = Re a/|.a.| & sin Arg a = Im a/|.a.| by A2,Th39;
  A9: cos Arg b = Re b/|.b.|by A7,Th39,COMPLEX1:130 .=cos Arg a by A1,A4,A6,A8,
XCMPLX_1:92;
  A10: sin Arg b = Im b /|.b.| by A7,Th39,COMPLEX1:130 .=sin Arg a by A1,A5,A6,
A8,XCMPLX_1:92;
      0 <= Arg b & Arg b < 2*PI & 0 <= Arg a & Arg a < 2*PI by Th18;
  hence Arg(a*[*r,0*]) = Arg a by A9,A10,Th12;
end;

theorem Th41:
for a being Element of COMPLEX, r being Real st r < 0
 holds Arg(a*[*r,0*]) = Arg -a
proof let a be Element of COMPLEX, r be Real such that
A1: r < 0;
 per cases; suppose a = 0; hence Arg(a*[*r,0*]) = Arg -a;
 suppose A2: a <> 0; set b = a*[*r,0*];
  A3: Re [*r,0*] = r & Im [*r,0*] = 0 by COMPLEX1:7;
  then A4: Re b = Re a * r - 0*Im a by COMPLEX1:24 .= r*Re a;
  A5: Im b = Re a * 0 + r * Im a by A3,COMPLEX1:24 .= r*Im a;
  A6: |.b.| = |.a.|*|.[*r,0*].| by COMPLEX1:151
          .= |.a.|*abs r by A3,COMPLEX1:136 .= |.a.|*(-r) by A1,ABSVALUE:def 1;
  A7: -r > 0 by A1,REAL_1:66;
      |.a.| <> 0 by A2,COMPLEX1:131; then A8: |.b.| <> 0 by A6,A7,XCMPLX_1:6;
  A9: cos Arg a = Re a/|.a.| & sin Arg a = Im a/|.a.| by A2,Th39;
  A10: cos Arg b = r*Re a/(|.a.|*(-r)) by A4,A6,A8,Th39,COMPLEX1:130
     .= r*Re a/(-|.a.|*r) by XCMPLX_1:175 .= -r*Re a/(|.a.|*r) by XCMPLX_1:189
     .= -cos Arg a by A1,A9,XCMPLX_1:92 .= cos Arg -a by A2,Th38;
  A11: sin Arg b = r*Im a /(|.a.|*(-r)) by A5,A6,A8,Th39,COMPLEX1:130
     .= r*Im a/(-|.a.|*r) by XCMPLX_1:175 .= -r*Im a/(|.a.|*r) by XCMPLX_1:189
     .= -sin Arg a by A1,A9,XCMPLX_1:92 .= sin Arg -a by A2,Th38;
      0 <= Arg b & Arg b < 2*PI & 0 <= Arg -a & Arg -a < 2*PI by Th18;
  hence Arg(a*[*r,0*]) = Arg -a by A10,A11,Th12;
end;

begin :: Inner product

definition ::Inner product of complex numbers
  let x, y be Element of COMPLEX;
  func x .|. y -> Element of COMPLEX equals :Def3:
  x*(y*');
  correctness;
end;

reserve a, b, c, d, x, y, z for Element of COMPLEX;

theorem Th42:
x.|.y = [* (Re x)*(Re y)+(Im x)*(Im y), -(Re x)*(Im y)+(Im x)*(Re y) *]
proof A1: Re [* Re x,Im x *] = Re x & Im [* Re x,Im x *] = Im x &
          Re[* Re y,-Im y *]=Re y & Im [* Re y,-Im y *] = -Im y by COMPLEX1:7;
 thus x.|.y = x*y*' by Def3 .=[* Re x,Im x *]*y*' by COMPLEX1:8
 .=[* Re x,Im x *]*[* Re y,-Im y*] by COMPLEX1:def 15
 .=[*(Re x)*(Re y)-(Im x)*(-Im y),(Re x)*(-Im y)+(Im x)*(Re y)*]
     by A1,COMPLEX1:def 10
 .=[* (Re x)*(Re y)--(Im x)*(Im y),(Re x)*(-Im y)+(Im x)*(Re y) *]
   by XCMPLX_1:175
 .=[* (Re x)*(Re y)+(Im x)*(Im y),(Re x)*(-Im y)+(Im x)*(Re y) *]
   by XCMPLX_1:151
 .=[*(Re x)*(Re y)+(Im x)*(Im y),-((Re x)*(Im y))+(Im x)*(Re y) *]
   by XCMPLX_1:175;
end;

theorem Th43:
z.|.z = [* (Re z)*(Re z)+(Im z)*(Im z),0*] & z.|.z = [* (Re z)^2+(Im z)^2,0*]
proof thus z.|.z
   = [* (Re z)*(Re z)+(Im z)*(Im z),-((Im z)*(Re z))+(Im z)*(Re z) *] by Th42
  .= [* (Re z)*(Re z)+(Im z)*(Im z),0 *] by XCMPLX_0:def 6;
  hence z.|.z = [* (Re z)^2+(Im z)*(Im z),0 *] by SQUARE_1:def 3
         .= [* (Re z)^2+(Im z)^2,0 *] by SQUARE_1:def 3;
end;

theorem Th44:
z.|.z = [* |.z.|^2,0*] & |.z.|^2 = Re (z.|.z)
proof A1: (Re z)^2>=0 by SQUARE_1:72; (Im z)^2>=0 by SQUARE_1:72;
  then A2: (Re z)^2 + (Im z)^2>=0+0 by A1,REAL_1:55;
  A3: |.z.|=sqrt((Re z)^2 + (Im z)^2) by COMPLEX1:def 16;
  thus z.|.z = [* (Re z)^2+(Im z)^2,0*] by Th43 .=[* |.z.|^2,0*] by A2,A3,
SQUARE_1:def 4;
 hence thesis by COMPLEX1:7;
end;

theorem Th45:
|. x.|.y .| = |.x.|*|.y.|
proof thus |.(x.|.y).| = |.(x*(y*')).| by Def3
      .=(|.x.|)*(|.y*'.|) by COMPLEX1:151 .=|.x.|*|.y.| by COMPLEX1:139;
end;

theorem
  x.|.x = 0 implies x = 0
proof assume x.|.x = 0;
 then 0c = [* (Re x)^2+(Im x)^2,0 *]&0c = [*0,0*] by Th43,L0;
 then (Re x)^2+(Im x)^2 = 0 by ARYTM_0:12;
 hence x = 0 by COMPLEX1:13;
end;

theorem Th47:
y.|.x = (x.|.y)*'
proof thus (y.|.x)=(y*x*')*'*' by Def3
    .=((x*')*'*(y*'))*' by COMPLEX1:121
    .=(x.|.y)*' by Def3;
end;

theorem Th48:
(x+y).|.z = x.|.z + y.|.z
proof thus (x + y).|.z =(x+y)*z*' by Def3 .=x*(z*')+y*(z*') by XCMPLX_1:8
  .=(x.|.z)+y*(z*') by Def3 .=(x.|.z)+(y.|.z) by Def3;
end;

theorem Th49:
x.|.(y+z) = x.|.y + x.|.z
proof thus x.|.(y+z) =x*((y+z)*') by Def3 .=x*(y*'+z*') by COMPLEX1:118
  .=x*(y*')+x*(z*') by XCMPLX_1:8 .=(x.|.y)+x*(z*') by Def3
  .=(x.|.y)+(x.|.z) by Def3;
end;

theorem Th50:
(a*x).|.y = a * x.|.y
proof thus (a*x).|.y = a*x*(y*') by Def3 .=a*(x*(y*')) by XCMPLX_1:4
    .= a * x.|.y by Def3;
end;

theorem Th51:
x.|.(a*y) = (a*') * x.|.y
proof thus x.|.(a*y) = x*((a*y)*') by Def3 .=x*((a*')*(y*')) by COMPLEX1:121
     .=(a*')*(x*(y*')) by XCMPLX_1:4 .= (a*') * x.|.y by Def3;
end;

theorem
 (a*x).|.y = x.|.((a*')*y)
proof thus (a*x).|.y =x*a*(y*') by Def3 .=x*((a*'*')*(y*')) by XCMPLX_1:4 .=x*
(((a*')*y)*') by COMPLEX1:121
         .= x.|.((a*')*y) by Def3;
end;

theorem
 (a*x+b*y).|.z = a * x.|.z + b * y.|.z
proof thus (a*x+b*y).|.z = (a*x+b*y)*z*' by Def3
 .= a * x *z*'+b*y*z*' by XCMPLX_1:8 .=a*(x*z*')+b*y*z*' by XCMPLX_1:4
 .=a* x.|.z+b*y*z*' by Def3 .=a* x.|.z+b*(y*z*') by XCMPLX_1:4
 .= a * x.|.z + b * y.|.z by Def3;
end;

theorem
  x.|.(a*y + b*z) = (a*') * x.|.y + (b*') * x.|.z
proof thus x.|.(a*y + b*z) = x.|.(a*y) +x.|.(b*z) by Th49
.=(a*')*x.|.y + x.|.(b*z) by Th51 .=(a*') * x.|.y + (b*') * x.|.z by Th51;
end;

theorem Th55:
(-x).|.y = x.|.(-y)
proof thus (-x).|.y = ((-1r)*x).|.y by COMPLEX1:46
 .= (-(1r*')) * x.|.y by Th50,COMPLEX1:115
 .=((-1r)*')* x.|.y by COMPLEX1:119 .= x.|.((-1r)*y) by Th51
 .=x.|.(-y) by COMPLEX1:46;
end;

theorem Th56:
(-x).|.y = - x.|.y
proof thus (-x).|.y = ((-1r)*x).|.y by COMPLEX1:46
  .= (-1r) * x.|.y by Th50 .=- x.|.y by COMPLEX1:46;
end;

theorem Th57:
- x.|.y = x.|.(-y)
proof thus - x.|.y = (-x).|.y by Th56 .=x.|.(-y) by Th55;end;

theorem
 (-x).|.(-y) = x.|.y
proof (-x).|.(-y) = - x.|.(-y) by Th56 .= - ( - x.|.y ) by Th57;
  hence thesis;
end;

theorem Th59:
(x - y).|.z = x.|.z - y.|.z
proof thus (x - y).|.z =(x-y)*z*' by Def3 .=x*(z*')-y*(z*') by XCMPLX_1:40
  .=(x.|.z)-y*(z*') by Def3 .=(x.|.z)-(y.|.z) by Def3;
end;

theorem Th60:
x.|.(y - z) = x.|.y - x.|.z
proof thus x.|.(y-z) =x*((y-z)*') by Def3 .=x*(y*'-z*') by COMPLEX1:120
  .=x*(y*')-x*(z*') by XCMPLX_1:40 .=(x.|.y)-x*(z*') by Def3
  .=(x.|.y)-(x.|.z) by Def3;
end;

theorem
 0c.|.x = 0c & x.|.0c = 0c
proof thus (0c).|.x =(0c)*(x*') by Def3 .=0c by COMPLEX1:28;
 thus x.|.0c = (x*0c*')*'*' by Def3 .= 0c by COMPLEX1:28,113;
end;

theorem
 (x + y).|.(x + y) = x.|.x + x.|.y + y.|.x + y.|.y
 proof (x + y).|.(x + y) = x.|.(x+y) + y.|.(x+y) by Th48
  .= x.|.x + x.|.y + y.|.(x+y) by Th49
  .= x.|.x + x.|.y + (y.|.x + y.|.y) by Th49
  .= x.|.x + x.|.y + y.|.x + y.|.y by XCMPLX_1:1;
   hence thesis;
 end;

theorem Th63:
(x-y).|.(x-y) = x.|.x - x.|.y - y.|.x + y.|.y
proof (x - y).|.(x - y) =x.|.(x - y) - y.|.(x - y) by Th59
  .=x.|.x - x.|.y - y.|.(x - y) by Th60
  .=x.|.x - x.|.y - (y.|.x - y.|.y) by Th60
  .=x.|.x - x.|.y - y.|.x + y.|.y by XCMPLX_1:37;
   hence thesis;
end;

Lm5:
(|.z.|)^2 = (Re z)^2 + (Im z)^2
proof thus (|.z.|)^2 = |.z.|*|.z.| by SQUARE_1:def 3
 .=|.z*z.| by COMPLEX1:151 .= (Re z)^2 + (Im z)^2 by COMPLEX1:154;
end;

theorem Th64:
Re (x.|.y) = 0 iff Im (x.|.y) = |.x.|*|.y.| or Im (x.|.y) = -|.x.|*|.y.|
proof
 hereby assume A1: Re (x.|.y)=0;
   (|.x.|*|.y.|)^2=(|.(x.|.y).|)^2 by Th45
  .=0+ (Im (x.|.y))^2 by A1,Lm5,SQUARE_1:60 .= (Im (x.|.y))^2;
 hence
    Im (x.|.y)=|.x.|*|.y.| or Im (x.|.y)= - (|.x.|*|.y.|) by JGRAPH_3:1;
 end;
 hereby assume Im (x.|.y)=|.x.|*|.y.| or Im (x.|.y)= - (|.x.|*|.y.|);
  then (Im (x.|.y))^2= (|.x.|*|.y.|)^2 by SQUARE_1:61 .= (|.(x.|.y).|)^2 by
Th45
  .=(Re (x.|.y))^2+(Im (x.|.y))^2 by Lm5;
  then 0= (Re (x.|.y))^2+(Im (x.|.y))^2 - (Im (x.|.y))^2 by XCMPLX_1:14
   .= (Re (x.|.y))^2 by XCMPLX_1:26;
 hence Re (x.|.y)=0 by SQUARE_1:73;
 end;
end;

begin :: Rotation

definition
 let a be Element of COMPLEX, r be Real;
 func Rotate(a, r) -> Element of COMPLEX equals :Def4:
  [* |.a.|*cos (r+Arg a), |.a.|*sin (r+Arg a) *];
  correctness;
end;

reserve r for Real;

theorem Th65:
Rotate(a, 0) = a
proof thus Rotate(a, 0) =
  [* |.a.|*cos (0+Arg a), |.a.|*sin (0+Arg a) *] by Def4 .= a by Th19;
end;

theorem Th66:
Rotate(a, r) = 0c iff a = 0c
proof
A1: Rotate(a, r) = [* |.a.|*cos (r+Arg a), |.a.|*sin (r+Arg a) *] by Def4;
  hereby assume Rotate(a, r) = 0c;
    then A2: |.a.|*cos (r+Arg a) = 0 & |.a.|*sin (r+Arg a) = 0 by A1,ARYTM_0:12
,L0;
   per cases by A2,XCMPLX_1:6;
   suppose |.a.| = 0; hence a = 0c by COMPLEX1:131;
   suppose cos (r+Arg a) = 0 & sin (r+Arg a) = 0; hence a = 0c by Th11;
  end;
  assume a = 0c; hence Rotate(a, r)= 0c by A1,COMPLEX1:130,L0;
end;

theorem Th67:
|.Rotate(a,r).| = |.a.|
proof
A1: |.a.| >= 0 by COMPLEX1:132;
    Rotate(a,r) = [* |.a.|*cos (r+Arg a), |.a.|*sin (r+Arg a) *] by Def4;
   then Re Rotate(a,r) = |.a.|*cos (r+Arg a) & Im Rotate(a,r) = |.a.|*sin (r+
Arg a)
   by COMPLEX1:7;
 hence |.Rotate(a,r).|
  = sqrt((|.a.|*cos (r+Arg a))^2 + (|.a.|*sin (r+Arg a))^2) by COMPLEX1:def 16
 .= sqrt(|.a.|^2*(cos (r+Arg a))^2 + (|.a.|*sin (r+Arg a))^2) by SQUARE_1:68
 .= sqrt(|.a.|^2*(cos (r+Arg a))^2 + |.a.|^2*(sin (r+Arg a))^2) by SQUARE_1:68
 .= sqrt(|.a.|^2*((cos (r+Arg a))^2 + (sin (r+Arg a))^2)) by XCMPLX_1:8
 .= sqrt(|.a.|^2*1) by SIN_COS:32 .= |.a.| by A1,SQUARE_1:89;
end;

theorem Th68:
a <> 0c implies ex i being Integer st Arg(Rotate(a,r)) = 2*PI*i+(r+Arg(a))
proof assume
 a <> 0c;
then A1: Rotate(a, r) <> 0c by Th66;
A2: |.a.| = |.Rotate(a,r).| by Th67;
A3: Rotate(a, r) = [* |.a.|*cos (r+Arg a), |.a.|*sin (r+Arg a) *] by Def4;
    consider AR being real number such that
A4: AR = 2*PI*-[\ (r+Arg a)/(2*PI) /]+(r+Arg a) and
A5: 0 <= AR and
A6: AR < 2*PI by Th2,COMPTRIG:21;
    reconsider ar = AR as Real by XREAL_0:def 1;
A7: cos (r+Arg a) = cos ar by A4,Th10;
A8: sin (r+Arg a) = sin ar by A4,Th9;
  take i = -[\ (r+Arg a)/(2*PI) /]; thus thesis by A1,A2,A3,A4,A5,A6,A7,A8,Th21
;
end;

theorem Th69:
Rotate(a,-Arg a) = [* |.a.|, 0 *]
proof set r = -Arg a;
A1: r+Arg a = 0 by XCMPLX_0:def 6;
   thus Rotate(a,r) = [* |.a.|*cos (r+Arg a), |.a.|*sin (r+Arg a) *] by Def4
     .= [* |.a.|, 0 *] by A1,SIN_COS:34;
end;

theorem Th70:
 Re Rotate(a,r) = (Re a)*(cos r)-(Im a)*(sin r) &
 Im Rotate(a,r) = (Re a)*(sin r)+(Im a)*(cos r)
proof set ra = Rotate(a,r);
 A1: ra = [* |.a.|*cos (r+Arg a), |.a.|*sin (r+Arg a) *] by Def4;
     a = [* |.a.|*cos Arg a, |.a.|*sin Arg a *] by Th19;
 then A2: Re a = |.a.|*cos Arg a & Im a = |.a.|*sin Arg a by COMPLEX1:7;
  thus Re Rotate(a,r)
   = |.a.|*cos (r+Arg a) by A1,COMPLEX1:7
  .= |.a.|*((cos r)*cos(Arg a)-(sin r)*sin(Arg a)) by SIN_COS:80
  .= |.a.|*((cos r)*cos(Arg a))-|.a.|*((sin r)*sin(Arg a)) by XCMPLX_1:40
  .= |.a.|*cos(Arg a)*(cos r)-|.a.|*((sin r)*sin(Arg a)) by XCMPLX_1:4
  .= (Re a)*(cos r)-(Im a)*(sin r) by A2,XCMPLX_1:4;
  thus Im Rotate(a,r)
   = |.a.|*sin(r+Arg a) by A1,COMPLEX1:7
  .= |.a.|*((sin r)*cos(Arg a)+(cos r)*sin(Arg a)) by SIN_COS:80
  .= |.a.|*((sin r)*cos(Arg a))+|.a.|*((cos r)*sin(Arg a)) by XCMPLX_1:8
  .= |.a.|*cos(Arg a)*(sin r)+|.a.|*((cos r)*sin(Arg a)) by XCMPLX_1:4
  .= (Re a)*(sin r)+(Im a)*(cos r) by A2,XCMPLX_1:4;
end;

theorem Th71:
 Rotate(a+b,r) = Rotate(a,r)+Rotate(b,r)
proof set ab = a+b; set rab = Rotate(ab,r),ra = Rotate(a,r), rb = Rotate(b,r);
A1: Re rab = (Re ab)*(cos r)-(Im ab)*(sin r) &
   Im rab = (Re ab)*(sin r)+(Im ab)*(cos r) by Th70;
A2: Re ra = (Re a)*(cos r)-(Im a)*(sin r) &
   Im ra = (Re a)*(sin r)+(Im a)*(cos r) by Th70;
A3: Re rb = (Re b)*(cos r)-(Im b)*(sin r) &
   Im rb = (Re b)*(sin r)+(Im b)*(cos r) by Th70;
A4: Re ab = Re a + Re b & Im ab = Im a + Im b by COMPLEX1:19;
A5: Re (ra+rb) = (Re a)*(cos r)-(Im a)*(sin r)+((Re b)*(cos r)-(Im b)*(sin r))
      by A2,A3,COMPLEX1:19
.= (Re a)*(cos r)-(Im a)*(sin r)+(Re b)*(cos r)-(Im b)*(sin r) by Lm1
.= (Re a)*(cos r)+(Re b)*(cos r)-(Im a)*(sin r)-(Im b)*(sin r) by XCMPLX_1:29
.= (Re a + Re b)*(cos r)-(Im a)*(sin r)-(Im b)*(sin r) by XCMPLX_1:8
.= (Re a + Re b)*(cos r)-((Im a)*(sin r)+(Im b)*(sin r)) by XCMPLX_1:36
.= Re rab by A1,A4,XCMPLX_1:8;
 Im (ra+rb) = (Re a)*(sin r)+(Im a)*(cos r)+((Re b)*(sin r)+(Im b)*(cos r))
      by A2,A3,COMPLEX1:19
.= (Re a)*(sin r)+(Im a)*(cos r)+(Re b)*(sin r)+(Im b)*(cos r) by XCMPLX_1:1
.= (Re a)*(sin r)+(Re b)*(sin r)+(Im a)*(cos r)+(Im b)*(cos r) by XCMPLX_1:1
.= (Re a + Re b)*(sin r)+(Im a)*(cos r)+(Im b)*(cos r) by XCMPLX_1:8
.= (Re a + Re b)*(sin r)+((Im a)*(cos r)+(Im b)*(cos r)) by XCMPLX_1:1
.= Im rab by A1,A4,XCMPLX_1:8;
 hence Rotate(a+b,r) = Rotate(a,r)+Rotate(b,r) by A5,COMPLEX1:9;
end;

theorem Th72:
Rotate(-a,r) = -Rotate(a,r)
proof
 per cases;
 suppose A1: a <> 0c;
A2: -Rotate(a,r) = - [* |.a.|*cos (r+Arg a), |.a.|*sin (r+Arg a) *] by Def4
    .= [* -|.a.|*cos (r+Arg a), -|.a.|*sin (r+Arg a) *] by Th1
    .= [* (-|.a.|)*cos (r+Arg a), -|.a.|*sin (r+Arg a) *] by XCMPLX_1:175
    .= [* (-|.a.|)*cos (r+Arg a), (-|.a.|)*sin (r+Arg a) *] by XCMPLX_1:175
    .= [* |.a.|*-cos (r+Arg a), (-|.a.|)*sin (r+Arg a) *] by XCMPLX_1:176
    .= [* |.a.|*-cos (r+Arg a), |.a.|*-sin (r+Arg a) *] by XCMPLX_1:176;
A3: |.a.| = |.-a.| by COMPLEX1:138;
    cos (r+Arg-a) = -cos(r+Arg a) & sin (r+Arg-a) = -sin(r+Arg a) proof
    per cases;
    suppose Arg a < PI; then Arg -a = PI+Arg a by A1,Th22;
      then r+Arg-a = PI+(r+Arg a) by XCMPLX_1:1;
     hence thesis by SIN_COS:84;
    suppose Arg a >= PI; then Arg -a = (Arg a)-PI by A1,Th22;
      then r+Arg-a = (Arg a)+r-PI by Lm1; hence thesis by Th6;
   end; hence Rotate(-a,r) = -Rotate(a,r) by A2,A3,Def4;
 suppose A4: a = 0c;
   hence Rotate(-a,r) = -0 by Th66 .= -Rotate(a,r) by A4,Th66;
end;

theorem Th73:
Rotate(a-b,r) = Rotate(a,r)-Rotate(b,r)
proof thus Rotate(a-b,r) = Rotate(a+-b,r) by XCMPLX_0:def 8
    .= Rotate(a,r)+Rotate(-b,r) by Th71 .= Rotate(a,r)+-Rotate(b,r) by Th72
    .= Rotate(a,r)-Rotate(b,r) by XCMPLX_0:def 8;
end;

theorem Th74:
Rotate(a, PI) = -a
proof per cases;
 suppose a = 0.F_Complex;
  hence Rotate(a, PI) = -a by Th66,COMPLFLD:9,REAL_1:26;
 suppose a <> 0.F_Complex;
 A1:  a = [* |.a.|*cos Arg a, |.a.|*sin Arg a *] by Th19;
 A2: |.a.|*-cos Arg a = -(|.a.|*cos Arg a) by XCMPLX_1:175 .= - Re a by A1,
COMPLEX1:7;
 A3: |.a.|*-sin Arg a = -(|.a.|*sin Arg a) by XCMPLX_1:175 .= - Im a by A1,
COMPLEX1:7;
 thus Rotate(a, PI)
   = [* |.a.|*cos (PI+Arg a), |.a.|*sin (PI+Arg a) *] by Def4
  .= [* |.a.|*-cos Arg a, |.a.|*sin (PI+Arg a) *] by SIN_COS:84
  .= [* |.a.|*-cos Arg a, |.a.|*-sin Arg a *] by SIN_COS:84
  .= -a by A2,A3,COMPLEX1:def 11;
end;

begin :: Angles

definition
  let a, b be Element of COMPLEX;
  func angle(a,b) -> Real equals :Def5:
             Arg(Rotate(b, -Arg a)) if Arg a = 0 or b <> 0
   otherwise 2*PI - Arg a;
   correctness;
end;

theorem Th75:
r >= 0 implies angle([*r,0*],a) = Arg a
proof assume r >= 0;
then Arg [*r,0*] = 0 by Th23;
 hence angle([*r,0*],a) = Arg(Rotate(a,-0)) by Def5 .= Arg a by Th65;
end;

theorem Th76:
Arg a = Arg b & a <> 0 & b <> 0 implies Arg Rotate(a,r) = Arg Rotate(b,r)
proof assume that
A1: Arg a = Arg b and A2: a <> 0 and A3: b <> 0;
   consider i being Integer such that
A4: Arg(Rotate(a,r)) = 2*PI*i+(r+Arg(a)) by A2,Th68;
   consider j being Integer such that
A5: Arg(Rotate(b,r)) = 2*PI*j+(r+Arg(b)) by A3,Th68;
    Arg(Rotate(a,r))+0 = 2*PI*i+r+Arg(a) by A4,XCMPLX_1:1;
then A6: Arg(Rotate(a,r))-(2*PI*i+r) = Arg(a)-0 by XCMPLX_1:33;
A7: Arg(Rotate(b,r)) = 2*PI*j+r+Arg(b) by A5,XCMPLX_1:1
   .= 2*PI*j+r+(Arg(Rotate(a,r))+-(2*PI*i+r)) by A1,A6,XCMPLX_0:def 8
   .= 2*PI*j+r+-(2*PI*i+r)+Arg(Rotate(a,r)) by XCMPLX_1:1
   .= 2*PI*j+r+(-2*PI*i+-r)+Arg(Rotate(a,r)) by XCMPLX_1:140
   .= 2*PI*j+r+-2*PI*i+-r+Arg(Rotate(a,r)) by XCMPLX_1:1
   .= 2*PI*j+-2*PI*i+r+-r+Arg(Rotate(a,r)) by XCMPLX_1:1
   .= 2*PI*j-2*PI*i+r+-r+Arg(Rotate(a,r)) by XCMPLX_0:def 8
   .= 2*PI*(j-i)+r+-r+Arg(Rotate(a,r)) by XCMPLX_1:40
   .= 2*PI*(j-i)+(r+-r)+Arg(Rotate(a,r)) by XCMPLX_1:1
   .= 2*PI*(j-i)+0+Arg(Rotate(a,r)) by XCMPLX_0:def 6
   .= 2*PI*(j-i)+Arg(Rotate(a,r));
   0 <= Arg Rotate(a,r) & 0 <= Arg Rotate(b,r) &
  Arg Rotate(a,r) < 2*PI & Arg Rotate(b,r) < 2*PI by Th18;
 hence Arg Rotate(a,r) = Arg Rotate(b,r) by A7,Th3;
end;

theorem Th77:
r > 0 implies angle(a,b) = angle(a*[*r,0*],b*[*r,0*])
proof assume that
A1: r > 0;
A2: Arg(b*[*r,0*]) = Arg b by A1,Th40;
A3: Arg(a*[*r,0*]) = Arg a by A1,Th40;
   per cases;
   suppose A4: b <> 0;
        Re [*r,0*] <> 0 by A1,COMPLEX1:7;
   then A5: b*[*r,0*] <> 0 by A4,COMPLEX1:12,XCMPLX_1:6;
    thus angle(a,b) = Arg(Rotate(b,-Arg a)) by A4,Def5
      .= Arg(Rotate(b*[*r,0*],-Arg(a*[*r,0*]))) by A2,A3,A4,A5,Th76
      .= angle(a*[*r,0*],b*[*r,0*]) by A5,Def5;
   suppose A6: b = 0;
    thus thesis proof
    per cases;
    suppose A7: Arg a = 0;
    hence angle(a,b) = Arg(Rotate(b,-Arg a)) by Def5
     .= Arg 0c by A6,Th66 .= Arg(Rotate(b*[*r,0*],-Arg(a*[*r,0*]))) by A6,Th66
     .= angle(a*[*r,0*],b*[*r,0*]) by A3,A7,Def5;
    suppose A8: Arg a <> 0;
    hence angle(a,b) = 2*PI-Arg a by A6,Def5
      .= angle(a*[*r,0*],b*[*r,0*]) by A3,A6,A8,Def5;
    end;
end;

theorem Th78:
a <> 0 & b <> 0 & Arg a = Arg b implies Arg -a = Arg -b
proof assume a <> 0 & b <> 0 & Arg a = Arg b;
  then Arg Rotate(a,PI) = Arg Rotate(b,PI) by Th76;
  then Arg -a = Arg Rotate(b,PI) by Th74;
 hence Arg -a = Arg -b by Th74;
end;

theorem Th79:
a <> 0 & b <> 0 implies angle(a,b) = angle(Rotate(a,r),Rotate(b,r))
proof assume that
A1: a <> 0 and A2: b <> 0;
   consider i being Integer such that
A3: Arg(Rotate(b, -Arg a)) = 2*PI*i+(-(Arg a) + Arg(b)) by A2,Th68;
     Arg(Rotate(b, -Arg a)) = Arg(Rotate(b, -Arg a)) + 0;
then A4: Arg(Rotate(b, -Arg a)) - 2*PI*i = -(Arg a) + Arg(b)-0 by A3,XCMPLX_1:
33;
A5: Rotate(b,r) <> 0 by A2,Th66;
   then consider j being Integer such that
A6: Arg(Rotate(Rotate(b,r), -Arg Rotate(a,r)))
     = 2*PI*j+(-(Arg Rotate(a, r)) + Arg(Rotate(b,r))) by Th68;
   consider k being Integer such that
A7: Arg Rotate(a,r) = 2*PI*k+(r+Arg(a)) by A1,Th68;
   consider l being Integer such that
A8: Arg Rotate(b,r) = 2*PI*l+(r+Arg(b)) by A2,Th68;
A9:   Arg(Rotate(Rotate(b,r), -Arg Rotate(a,r)))
   = 2*PI*j+(-2*PI*k+-(r+Arg(a))+(2*PI*l+(r+Arg(b)))) by A6,A7,A8,XCMPLX_1:140
  .= 2*PI*j+(-2*PI*k+((2*PI*l+(r+Arg(b)))+-(r+Arg(a)))) by XCMPLX_1:1
  .= 2*PI*j+-2*PI*k+((2*PI*l+(r+Arg(b)))+-(r+Arg(a))) by XCMPLX_1:1
  .= 2*PI*j-2*PI*k+((2*PI*l+(r+Arg(b)))+-(r+Arg(a))) by XCMPLX_0:def 8
  .= 2*PI*(j-k)+((2*PI*l+(r+Arg(b)))+-(r+Arg(a))) by XCMPLX_1:40
  .= 2*PI*(j-k)+(2*PI*l+(r+Arg(b)))+-(r+Arg(a)) by XCMPLX_1:1
  .= 2*PI*(j-k)+2*PI*l+(r+Arg(b))+-(r+Arg(a)) by XCMPLX_1:1
  .= 2*PI*(j-k+l)+(r+Arg(b))+-(r+Arg(a)) by XCMPLX_1:8
  .= 2*PI*(j-k+l)+Arg(b)+r+-(r+Arg(a)) by XCMPLX_1:1
  .= 2*PI*(j-k+l)+Arg(b)+r+(-r+-Arg(a)) by XCMPLX_1:140
  .= 2*PI*(j-k+l)+Arg(b)+r+-r+-Arg(a) by XCMPLX_1:1
  .= 2*PI*(j-k+l)+Arg(b)+-Arg(a) by XCMPLX_1:137
  .= 2*PI*(j-k+l)+(-Arg(a)+Arg(b)) by XCMPLX_1:1
  .= 2*PI*(j-k+l)+Arg(Rotate(b, -Arg a)) - 2*PI*i by A4,Lm1
  .= 2*PI*(j-k+l)-2*PI*i+Arg(Rotate(b, -Arg a)) by XCMPLX_1:29
  .= 2*PI*(j-k+l-i)+Arg(Rotate(b, -Arg a)) by XCMPLX_1:40;
A10: 0 <= Arg(Rotate(b, -Arg a)) & Arg(Rotate(b, -Arg a)) < 2*PI &
   0 <= Arg(Rotate(Rotate(b,r), -Arg Rotate(a,r))) &
        Arg(Rotate(Rotate(b,r), -Arg Rotate(a,r))) < 2*PI by Th18;
 thus angle(a,b) = Arg(Rotate(b, -Arg a)) by A2,Def5
   .= Arg(Rotate(Rotate(b,r), -Arg Rotate(a,r))) by A9,A10,Th3
   .= angle(Rotate(a,r),Rotate(b,r)) by A5,Def5;
end;

theorem
 r < 0 & a <> 0 & b <> 0 implies angle(a,b) = angle(a*[*r,0*],b*[*r,0*])
proof assume that
A1: r < 0 and A2: a <> 0 and A3: b <> 0;
   A4: Arg(b*[*r,0*]) = Arg -b by A1,Th41;
   A5: Arg(a*[*r,0*]) = Arg -a by A1,Th41;
   A6: -b <> 0 by A3,XCMPLX_1:135;
       then consider i being Integer such that
   A7: Arg(Rotate(-b, -Arg -a)) = 2*PI*i+(-Arg -a + Arg -b) by Th68;
       set br = b*[*r,0*], ar = a*[*r,0*];
        Re [*r,0*] <> 0 by A1,COMPLEX1:7;
   then A8: br <> 0 by A3,COMPLEX1:12,XCMPLX_1:6; then consider j being Integer
such that
   A9: Arg(Rotate(br,-Arg ar)) = 2*PI*j+(-Arg -a + Arg -b) by A4,A5,Th68;
        Arg(Rotate(-b, -Arg -a))+0 = 2*PI*i+(-Arg -a + Arg -b) by A7;
       then Arg(Rotate(-b,-Arg -a))-2*PI*i=(-Arg -a +Arg -b)-0 by XCMPLX_1:33;
   then A10: Arg(Rotate(br,-Arg ar)) = 2*PI*j+Arg(Rotate(-b,-Arg -a))-2*PI*i
by A9,Lm1
       .= 2*PI*j-2*PI*i+Arg(Rotate(-b,-Arg -a)) by XCMPLX_1:29
       .= 2*PI*(j-i)+Arg(Rotate(-b,-Arg -a)) by XCMPLX_1:40;
   A11: 0 <= Arg(Rotate(br,-Arg ar)) & Arg(Rotate(br,-Arg ar)) < 2*PI &
       0 <= Arg(Rotate(-b,-Arg -a)) & Arg(Rotate(-b,-Arg -a)) < 2*PI
        by Th18;
       thus angle(a,b) = angle(Rotate(a,PI),Rotate(b,PI)) by A2,A3,Th79
         .= angle(-a,Rotate(b,PI)) by Th74 .= angle(-a,-b) by Th74
         .= Arg(Rotate(-b,-Arg -a)) by A6,Def5
         .= Arg(Rotate(br,-Arg ar)) by A10,A11,Th3
         .= angle(a*[*r,0*],b*[*r,0*]) by A8,Def5;
end;

theorem
 a <> 0 & b <> 0 implies angle(a,b) = angle(-a,-b)
proof assume a <> 0 & b <> 0;
 hence angle(a,b) = angle(Rotate(a,PI),Rotate(b,PI)) by Th79
    .= angle(-a,Rotate(b,PI)) by Th74 .= angle(-a,-b) by Th74;
end;

theorem
 b <> 0 & angle(a,b) = 0 implies angle(a,-b) = PI
proof assume that
A1: b <> 0 and
A2: angle(a,b) = 0;
A3: -b <> 0 by A1,XCMPLX_1:135;
A4: Arg(Rotate(b, -Arg a)) = 0 by A1,A2,Def5;
A5: Rotate(b, -Arg a) <> 0 by A1,Th66;
A6: Arg(Rotate(-b, -Arg a)) = Arg(-Rotate(b, -Arg a)) by Th72;
    Arg -Rotate(b, -Arg a) = Arg Rotate(b, -Arg a)+PI by A4,A5,Th22,COMPTRIG:21
.= PI by A4;
  hence angle(a,-b) = PI by A3,A6,Def5;
end;

theorem Th83:
a <> 0 & b <> 0 implies cos angle(a,b) = Re (a.|.b)/(|.a.|*|.b.|) &
                        sin angle(a,b) = - Im (a.|.b)/(|.a.|*|.b.|)
proof assume that
A1: a <> 0 and A2: b <> 0;
A3: |.a.| <> 0 by A1,COMPLEX1:131;
A4: |.b.| <> 0 by A2,COMPLEX1:131;
   set mab = (|.a.|*|.b.|); set mabi = (|.a.|*|.b.|)";
   A5: |.a.| >= 0 & |.b.| >= 0 by COMPLEX1:132;
   then mab > 0*|.a.| by A3,A4,REAL_1:70;
then A6: mabi > 0 by REAL_1:72;
   set ra = Rotate(a,-Arg a), rb = Rotate(b,-Arg a), r = -Arg a;
A7: |.a.|*mabi > 0*mabi by A3,A5,A6,REAL_1:70;
A8: ra = [*|.a.|,0*] by Th69;
 angle(a,b) = angle(ra,rb) by A1,A2,Th79;
then A9: angle(a,b) = angle(ra*[*mabi,0*],rb*[*mabi,0*]) by A6,Th77;
A10: Re ra = |.a.| & Im ra = 0 by A8,COMPLEX1:7;
A11: Re [*mabi,0*] = mabi & Im [*mabi,0*] = 0 by COMPLEX1:7;
    then Re (ra*[*mabi,0*]) = |.a.|*mabi-0*0 &
    Im (ra*[*mabi,0*]) = |.a.|*0+0*mabi by A10,COMPLEX1:24;
    then ra*[*mabi,0*] = [*|.a.|*mabi,0*] by COMPLEX1:8;
then A12: angle(a,b) = Arg(rb*[*mabi,0*]) by A7,A9,Th75;
   set IT = rb*[*mabi,0*];
A13: Re rb = (Re b)*(cos r)-(Im b)*(sin r) &
    Im rb = (Re b)*(sin r)+(Im b)*(cos r) by Th70;
A14: IT = [* |.IT.|*cos Arg IT, |.IT.|*sin Arg IT *] by Th19;
A15: Re IT = Re rb * mabi - (Im rb)*0 by A11,COMPLEX1:24 .= Re rb * mabi;
A16: Im IT = Re rb * 0 + Im rb * mabi by A11,COMPLEX1:24 .= Im rb * mabi;
     a = [* |.a.|*cos Arg a, |.a.|*sin Arg a *] by Th19;
        then Re a = |.a.|*cos Arg a & Im a = |.a.|*sin Arg a by COMPLEX1:7;
then A17:  cos Arg a = (Re a)/|.a.| & sin Arg a = (Im a)/|.a.| by A3,XCMPLX_1:
90;
A18: cos r = cos Arg a by SIN_COS:34;
A19: a.|.b =[* (Re a)*(Re b)+(Im a)*(Im b),-((Re a)*(Im b))+(Im a)*(Re b) *]
    by Th42;
then A20: Re (a.|.b) = (Re a)*(Re b)+(Im a)*(Im b) by COMPLEX1:7;
A21: Re rb = (Re b)*(cos r)-(Im b)*(-sin Arg a) by A13,SIN_COS:34
   .= (Re b)*(cos r)+(-(Im b)*(-sin Arg a)) by XCMPLX_0:def 8
   .= (Re b)*(cos r)+((Im b)*sin Arg a) by XCMPLX_1:178
   .= (Re b)*((Re a)/|.a.|)+(Im b)*((Im a)/|.a.|) by A17,SIN_COS:34
   .= (Re b)*(Re a)/|.a.|+(Im b)*((Im a)/|.a.|) by XCMPLX_1:75
   .= (Re b)*(Re a)/|.a.|+(Im b)*(Im a)/|.a.| by XCMPLX_1:75
   .= Re (a.|.b) / |.a.| by A20,XCMPLX_1:63;
A22: Im rb = (Re b)*(-sin Arg a)+(Im b)*(cos r) by A13,SIN_COS:34
   .= (-(Re b))*((Im a)/|.a.|)+(Im b)*((Re a)/|.a.|) by A17,A18,XCMPLX_1:176
   .= (-(Re b))*(Im a)/|.a.|+(Im b)*((Re a)/|.a.|) by XCMPLX_1:75
   .= (-(Re b))*(Im a)/|.a.|+(Im b)*(Re a)/|.a.| by XCMPLX_1:75
   .= --((-(Re b))*(Im a)+(Im b)*(Re a))/|.a.| by XCMPLX_1:63
   .= -(-((-(Re b))*(Im a)+(Im b)*(Re a)))/|.a.| by XCMPLX_1:188
   .= -(-((Im b)*(Re a))+-((-(Re b))*(Im a)))/|.a.| by XCMPLX_1:140
   .= -(-((Im b)*(Re a))+((--(Re b))*(Im a)))/|.a.| by XCMPLX_1:175
   .= - Im (a.|.b)/|.a.| by A19,COMPLEX1:7;
A23: mabi^2 >= 0 by SQUARE_1:72;
     (Re rb)^2 >= 0 & (Im rb)^2 >= 0 & 0 = 0+0 by SQUARE_1:72;
then A24: (Re rb)^2+(Im rb)^2 >= 0 by REAL_1:55;
A25: |.IT.| = sqrt((Re rb * mabi)^2+(Im rb * mabi)^2) by A15,A16,COMPLEX1:def
16
    .= sqrt((Re rb)^2*mabi^2 + ((Im rb)*mabi)^2) by SQUARE_1:68
    .= sqrt((Re rb)^2*mabi^2 + (Im rb)^2*mabi^2) by SQUARE_1:68
    .= sqrt(mabi^2*((Re rb)^2+(Im rb)^2)) by XCMPLX_1:8
    .= sqrt(mabi^2)*sqrt((Re rb)^2+(Im rb)^2) by A23,A24,SQUARE_1:97
    .= mabi*sqrt((Re rb)^2+(Im rb)^2) by A6,SQUARE_1:89
    .= mabi*|.rb.| by COMPLEX1:def 16 .= mabi*|.b.| by Th67;
then A26: |.IT.| <> 0 by A4,A6,XCMPLX_1:6;
    |.IT.|*cos Arg IT = Re rb * mabi by A14,A15,COMPLEX1:7;
 hence cos angle(a,b) = Re rb * mabi/|.IT.| by A12,A26,XCMPLX_1:90
      .= Re rb *(mabi/|.IT.|) by XCMPLX_1:75
      .= Re (a.|.b) / |.a.|*(mabi/mabi/|.b.|) by A21,A25,XCMPLX_1:79
      .= Re (a.|.b) / |.a.|*(1/|.b.|) by A6,XCMPLX_1:60
      .= Re (a.|.b)*1 / (|.a.|*|.b.|) by XCMPLX_1:77 .= Re (a.|.b)/mab;
    |.IT.|*sin Arg IT = Im rb * mabi by A14,A16,COMPLEX1:7;
 hence sin angle(a,b) = Im rb * mabi/|.IT.| by A12,A26,XCMPLX_1:90
      .= Im rb * (mabi/|.IT.|) by XCMPLX_1:75
      .= (- Im (a.|.b) / |.a.|)*(mabi/mabi/|.b.|) by A22,A25,XCMPLX_1:79
      .= (- Im (a.|.b) / |.a.|)*(1/|.b.|) by A6,XCMPLX_1:60
      .= ((- Im (a.|.b)) / |.a.|)*(1/|.b.|) by XCMPLX_1:188
      .= (- Im (a.|.b))*1/(|.a.|*|.b.|) by XCMPLX_1:77
      .= - Im (a.|.b)/mab by XCMPLX_1:188;
 end;

definition let x, y, z be Element of COMPLEX;
func angle(x,y,z) -> real number equals :Def6:
  Arg(z-y)-Arg(x-y) if Arg(z-y)-Arg(x-y) >= 0
  otherwise 2*PI+(Arg(z-y)-Arg(x-y));
correctness;
end;

theorem Th84:
0 <= angle(x,y,z) & angle(x,y,z) < 2*PI
proof now per cases;
    case A1: Arg(z-y)-Arg(x-y)>=0;
     then A2: angle(x,y,z)=Arg(z-y)-Arg(x-y) by Def6;
     A3: Arg(z-y)<2*PI by Th18;
      Arg(x-y)>=0 by Th18; then Arg(z-y)+0<=Arg(z-y)+Arg(x-y) by REAL_1:55;
     then Arg(z-y)-Arg(x-y)<=Arg(z-y) by REAL_1:86;
     hence 0<=angle(x,y,z) & angle(x,y,z)<2*PI by A1,A2,A3,AXIOMS:22;
    case A4: Arg(z-y)-Arg(x-y)<0;
     then A5: angle(x,y,z)=2*PI+(Arg(z-y)-Arg(x-y)) by Def6;
     A6: Arg(z-y)-Arg(x-y) + 2*PI < 0 + 2*PI by A4,REAL_1:67;
     A7: Arg(x-y)<2*PI by Th18; Arg(z-y)>=0 by Th18;
     then Arg(x-y)+0<=Arg(x-y)+Arg(z-y) by REAL_1:55;
     then Arg(x-y)-Arg(z-y)<=Arg(x-y) by REAL_1:86;
     then (Arg(x-y)-Arg(z-y))<2*PI by A7,AXIOMS:22;
     then 2*PI-(Arg(x-y)-Arg(z-y))>0 by SQUARE_1:11;
     then 2*PI-Arg(x-y)+Arg(z-y)>0 by XCMPLX_1:37;
     then 2*PI+Arg(z-y)-Arg(x-y)>0 by XCMPLX_1:29;
     hence 0<=angle(x,y,z) & angle(x,y,z)<2*PI by A5,A6,XCMPLX_1:29;
    end; hence 0<=angle(x,y,z) & angle(x,y,z)<2*PI;
end;

theorem Th85:
angle(x,y,z)=angle(x-y,0c,z-y)
proof now per cases;
     case A1: Arg((z-y)-0c)-Arg((x-y)-0c)>=0;
      then angle(x-y,0c,z-y)=Arg(z-y)-Arg(x-y) by Def6;
     hence angle(x-y,0c,z-y)=angle(x,y,z) by A1,Def6;
     case A2: Arg((z-y)-0c)-Arg((x-y)-0c)<0;
      then angle(x-y,0c,z-y)=2*PI+(Arg(z-y)-Arg(x-y)) by Def6;
     hence angle(x-y,0c,z-y)=angle(x,y,z) by A2,Def6;
    end; hence angle(x,y,z)=angle(x-y,0c,z-y);
end;

theorem Th86:
angle(a,b,c) = angle(a+d,b+d,c+d)
proof thus angle(a,b,c) = angle(a-b,0c,c-b) by Th85
   .= angle((a+d)-(b+d),0c,c-b) by XCMPLX_1:32
   .= angle((a+d)-(b+d),0c,(c+d)-(b+d)) by XCMPLX_1:32
   .= angle(a+d,b+d,c+d) by Th85;
end;

theorem Th87:
angle(a,b) = angle(a,0c,b)
proof set ab2 = angle(a,b);
A1: 0 = 0c;
A2: 0 <= Arg(Rotate(b,-Arg a)) & Arg(Rotate(b,-Arg a)) < 2*PI &
    0 <= Arg b & Arg b < 2*PI by Th18;
   per cases;
   suppose A3: b <> 0;
   then A4: ab2 = Arg(Rotate(b, -Arg a)) by Def5;
   thus thesis proof
   per cases;
   suppose Arg(b-0c)-Arg(a-0c) >= 0;
   then A5: angle(a,0c,b) = Arg(b-0c)-Arg(a-0c) by Def6
       .= -Arg(a)+Arg(b) by A1,XCMPLX_0:def 8;
       consider i being Integer such that
   A6: Arg(Rotate(b,-Arg a)) = 2*PI*i+(-Arg a + Arg(b)) by A3,Th68;
        0 <= angle(a,0c,b) & angle(a,0c,b) < 2*PI by Th84;
      hence ab2 = angle(a,0c,b) by A2,A4,A5,A6,Th3;
   suppose Arg(b-0c)-Arg(a-0c) < 0;
   then A7: angle(a,0c,b) = 2*PI+(Arg(b)-Arg(a)) by Def6 .= 2*PI+(Arg(b)+-Arg(a
)) by XCMPLX_0:def 8;
      consider i being Integer such that
   A8: Arg(Rotate(b,-Arg a)) = 2*PI*i+(-Arg a + Arg(b)) by A3,Th68;
   A9: 2*PI*i+(-Arg a + Arg(b))
       = 2*PI*i-2*PI*1+2*PI+(-Arg a + Arg(b)) by XCMPLX_1:27
      .= 2*PI*(i-1)+2*PI+(-Arg a + Arg(b)) by XCMPLX_1:40
      .= 2*PI*(i-1)+(2*PI+(-Arg a + Arg(b))) by XCMPLX_1:1;
      0 <= 2*PI+(-Arg a + Arg(b)) & 2*PI+(-Arg a + Arg(b)) < 2*PI by A7,Th84;
    hence thesis by A2,A4,A7,A8,A9,Th3;
   end;
   suppose A10: b = 0;
    thus thesis proof
    per cases;
    suppose A11: Arg a = 0;
    then A12: ab2=Arg(Rotate(b, -Arg a)) by Def5 .= 0 by A10,Th20,Th66;
        Arg(b-0c)-Arg(a-0c) = 0 by A10,A11,Th20;
     hence thesis by A12,Def6;
    suppose A13: Arg a <> 0;
    A14: Arg(b-0c)-Arg(a-0c) = - Arg a by A10,Th20,XCMPLX_1:150; 0 < --Arg a
by A13,Th18;
        then 0 > - Arg a by REAL_1:66; then angle(a,0c,b) = 2*PI+(-Arg a) by
A14,Def6
                                       .= 2*PI-Arg a by XCMPLX_0:def 8;
     hence thesis by A10,A13,Def5;
    end;
end;

theorem Th88:
angle(x,y,z) = 0 implies Arg(x-y) = Arg(z-y) & angle(z,y,x)=0
proof assume A1: angle(x,y,z) =0;
   now per cases;
  case Arg(z-y)-Arg(x-y)>=0; then Arg(z-y)-Arg(x-y)=0 by A1,Def6;
    then A2: Arg(z-y)=0+Arg(x-y) by XCMPLX_1:27 .=Arg(x-y);
    then Arg(x-y)-Arg(z-y)=0 by XCMPLX_1:14;
   hence Arg(x-y)=Arg(z-y) & angle(z,y,x)=0 by A2,Def6;
  case A3: Arg(z-y)-Arg(x-y)<0;
    then angle(x,y,z)=2*PI+(Arg(z-y)-Arg(x-y)) by Def6;
    then 0- (Arg(z-y)-Arg(x-y))=2*PI by A1,XCMPLX_1:26;
    then A4: 0+(Arg(x-y)-Arg(z-y))=2*PI by XCMPLX_1:38; -(Arg(z-y)-Arg(x-y))>0
by A3,REAL_1:66;
    then 0-(Arg(z-y)-Arg(x-y))>0 by XCMPLX_1:150; then 0+(Arg(x-y)-Arg(z-y))>
0
    by XCMPLX_1:38; then angle(z,y,x)=Arg(x-y)-Arg(z-y) by Def6;
   hence contradiction by A4,Th84;
  end; hence Arg(x-y)=Arg(z-y)& angle(z,y,x)=0;
end;

theorem Th89:
a <> 0c & b <> 0c implies (Re (a.|.b) = 0
                      iff angle(a,0c,b) = PI/2 or angle(a,0c,b) = 3/2*PI)
proof assume that
A1: a <> 0c and A2: b <> 0c;
A3: cos angle(a,b) = Re (a.|.b)/(|.a.|*|.b.|) &
   sin angle(a,b) = - Im (a.|.b)/(|.a.|*|.b.|) by A1,A2,Th83;
A4: angle(a,b) = angle(a,0c,b) by Th87;
    |.a.| <> 0 & |.b.| <> 0 by A1,A2,COMPLEX1:131;
then A5: |.a.|*|.b.| <> 0 by XCMPLX_1:6;
A6: 0 <= angle(a,0c,b) & angle(a,0c,b) < 2*PI by Th84;
A7: PI/2 < 2*PI by AXIOMS:22,COMPTRIG:21;
A8: -Im (a.|.b)/(|.a.|*|.b.|) = (-Im (a.|.b))/(|.a.|*|.b.|) by XCMPLX_1:188;
   hereby assume A9: Re (a.|.b) = 0;
     then Im (a.|.b)=|.a.|*|.b.| or Im (a.|.b)= - (|.a.|*|.b.|) by Th64;
     then sin angle(a,b) = 1 or sin angle(a,b) = -1 by A3,A5,A8,XCMPLX_1:60;
    hence angle(a,0c,b) = PI/2 or angle(a,0c,b) = 3/2*PI
           by A3,A4,A6,A7,A9,Th12,COMPTRIG:20,21,SIN_COS:82;
   end; assume angle(a,0c,b) = PI/2 or angle(a,0c,b) = 3/2*PI;
     then 0*(|.a.|*|.b.|) = Re (a.|.b) by A3,A4,A5,COMPTRIG:20,SIN_COS:82,
XCMPLX_1:88;
   hence Re (a.|.b) = 0;
end;

theorem
 a <> 0c & b <> 0c implies (Im(a.|.b) = |.a.|*|.b.| or Im(a.|.b) = -|.a.|*|.b.|
                      iff angle(a,0c,b) = PI/2 or angle(a,0c,b) = 3/2*PI)
proof assume A1: a<>0c & b<>0c;
 hereby assume Im(a.|.b)=|.a.|*|.b.| or Im(a.|.b)=-(|.a.|*|.b.|);
   then Re (a.|.b)=0 by Th64;
   hence angle(a,0c,b)=PI/2 or angle(a,0c,b)=3/2*PI by A1,Th89;
 end;
 hereby assume angle(a,0c,b)=PI/2 or angle(a,0c,b)=3/2*PI;
   then Re (a.|.b)=0 by A1,Th89;
  hence Im(a.|.b)=|.a.|*|.b.| or Im(a.|.b)=-(|.a.|*|.b.|) by Th64;
 end;
end;

Lm6:
for a, b, c being Element of COMPLEX st a <> b & c <> b
 holds Re ((a-b).|.(c-b)) = 0 iff angle(a,b,c) = PI/2 or angle(a,b,c) = 3/2*PI
proof let x, y,z be Element of COMPLEX; assume A1: x<>y & z<>y;
 A2: now assume x-y=0c; then x=0c+y by XCMPLX_1:27;
  hence contradiction by A1,COMPLEX1:22;
 end;
 A3: now assume z-y=0c; then z=0c+y by XCMPLX_1:27;
  hence contradiction by A1,COMPLEX1:22;
 end;
  angle(x,y,z)=angle(x-y,0c,z-y) by Th85;
 hence (Re ((x-y).|.(z-y)) = 0 iff angle(x,y,z)=PI/2 or angle(x,y,z)=3/2*PI)
                          by A2,A3,Th89;
end;

theorem
 x <> y & z <> y & (angle(x,y,z) = PI/2 or angle(x,y,z) = 3/2*PI)
 implies |.x-y.|^2+|.z-y.|^2 = |.x-z.|^2
proof assume
A1:  x<>y & z<>y & (angle(x,y,z)=PI/2 or angle(x,y,z)=3/2*PI);
A2: |.x-y.|^2+|.z-y.|^2
   =Re ((x-y).|.(x-y)) + |.z-y.|^2 by Th44
  .=Re ((x-y).|.(x-y)) + Re ((z-y).|.(z-y)) by Th44
  .=Re ((x-y).|.(x-y)+(z-y).|.(z-y)) by COMPLEX1:19;
  set x3=x-z;
   x3=x-z+y-y by XCMPLX_1:26
       .=x+-z+y-y by XCMPLX_0:def 8 .=x+(-z+y)-y by XCMPLX_1:1
       .=x+(-(z-y))-y by XCMPLX_1:162 .=x+(-(z-y))+(-y) by XCMPLX_0:def 8
       .=x+(-y)+(-(z-y)) by XCMPLX_1:1 .=x-y+(-(z-y)) by XCMPLX_0:def 8
       .=(x-y)-(z-y) by XCMPLX_0:def 8;
  then (x-z).|.(x-z)
   =(x-y).|.(x-y)-(x-y).|.(z-y)-(z-y).|.(x-y) +(z-y).|.(z-y) by Th63;
 then Re((x-z).|.(x-z)) =Re((x-y).|.(x-y)+-(x-y).|.(z-y)-(z-y).|.(x-y)+(z-y)
.|.(z-y))
   by XCMPLX_0:def 8
 .=Re((x-y).|.(x-y)+-(x-y).|.(z-y)+-(z-y).|.(x-y) +(z-y).|.(z-y))
   by XCMPLX_0:def 8
.=Re((x-y).|.(x-y)+(-(x-y).|.(z-y)+-(z-y).|.(x-y))+(z-y).|.(z-y))by XCMPLX_1:1
.=Re((x-y).|.(x-y)+(-((x-y).|.(z-y)+(z-y).|.(x-y)))+(z-y).|.(z-y))
   by XCMPLX_1:140
.=Re((x-y).|.(x-y)+(z-y).|.(z-y)+(-((x-y).|.(z-y)+(z-y).|.(x-y))))
   by XCMPLX_1:1
.=Re((x-y).|.(x-y)+(z-y).|.(z-y)-((x-y).|.(z-y)+(z-y).|.(x-y)))
  by XCMPLX_0:def 8
.=Re((x-y).|.(x-y)+(z-y).|.(z-y))-Re((x-y).|.(z-y)+(z-y).|.(x-y))by COMPLEX1:48
.=Re((x-y).|.(x-y)+(z-y).|.(z-y))-(Re((x-y).|.(z-y))+Re((z-y).|.(x-y)))
   by COMPLEX1:19
.=Re((x-y).|.(x-y)+(z-y).|.(z-y))-(Re((x-y).|.(z-y))+Re(((x-y).|.(z-y))*'))
   by Th47
.=Re((x-y).|.(x-y)+(z-y).|.(z-y))-(Re((x-y).|.(z-y))+Re((x-y).|.(z-y)))
    by COMPLEX1:112
.=Re((x-y).|.(x-y)+(z-y).|.(z-y))-(0+Re((x-y).|.(z-y))) by A1,Lm6
  .=Re((x-y).|.(x-y)+(z-y).|.(z-y)) -0 by A1,Lm6 .=Re((x-y).|.(x-y)+(z-y).|.(z-
y));
   hence |.x-y.|^2+|.z-y.|^2=|.x-z.|^2 by A2,Th44;
end;

theorem Th92:
a <> b & b <> c implies
  angle(a,b,c) = angle(Rotate(a,r), Rotate(b,r), Rotate(c,r))
proof set cb = c-b, ab = a-b;
     set rc = Rotate(c,r), rb = Rotate(b,r), ra = Rotate(a,r);
     set rcb = Rotate(c,r)-Rotate(b,r), rab = Rotate(a,r)-Rotate(b,r);
A1: rcb = Rotate(cb,r) by Th73;
A2: rab = Rotate(ab,r) by Th73;
   assume a <> b & b <> c;
then A3: ab <> 0 & cb <> 0 by XCMPLX_1:15;
    then consider abi being Integer such that
A4: Arg(Rotate(ab,r)) = 2*PI*abi+(r+Arg(ab)) by Th68;
    consider cbi being Integer such that
A5: Arg(Rotate(cb,r)) = 2*PI*cbi+(r+Arg(cb)) by A3,Th68;
A6: 0 <= angle(a,b,c) & angle(a,b,c) < 2*PI by Th84;
A7: 0 <= angle(Rotate(a,r),Rotate(b,r), Rotate(c,r)) &
    angle(Rotate(a,r),Rotate(b,r), Rotate(c,r))< 2*PI by Th84;
A8: Arg(rcb)-Arg(rab)
    = 2*PI*cbi+r+Arg(cb)-(2*PI*abi+(r+Arg(ab))) by A1,A2,A4,A5,XCMPLX_1:1
   .= 2*PI*cbi+r+Arg(cb) - (2*PI*abi+r+Arg(ab)) by XCMPLX_1:1
   .= 2*PI*cbi+r-(2*PI*abi+r+Arg(ab))+Arg(cb) by XCMPLX_1:29
   .= 2*PI*cbi+r-(2*PI*abi+r)-Arg(ab)+Arg(cb) by XCMPLX_1:36
   .= 2*PI*cbi+r-r-2*PI*abi-Arg(ab)+Arg(cb) by XCMPLX_1:36
   .= 2*PI*cbi-2*PI*abi-Arg(ab)+Arg(cb) by XCMPLX_1:26
   .= 2*PI*(cbi-abi)-Arg(ab)+Arg(cb) by XCMPLX_1:40
   .= Arg(cb)-Arg(ab)+2*PI*(cbi-abi) by XCMPLX_1:30;
 per cases;
 suppose Arg(c-b)-Arg(a-b) >= 0;
 then A9: angle(a,b,c) = Arg(c-b)-Arg(a-b) by Def6;
  thus angle(a,b,c) = angle(Rotate(a,r),Rotate(b,r), Rotate(c,r)) proof
  per cases;
  suppose Arg(rcb)-Arg(rab) >= 0;
    then angle(ra,rb,rc) = Arg(rcb)-Arg(rab) by Def6;
   hence thesis by A6,A7,A8,A9,Th3;
  suppose Arg(rcb)-Arg(rab) < 0;
   then angle(ra,rb,rc)
     = Arg(cb)-Arg(ab)+2*PI*(cbi-abi)+2*PI by A8,Def6
    .= Arg(cb)-Arg(ab)+(2*PI*(cbi-abi)+2*PI*1) by XCMPLX_1:1
    .= Arg(cb)-Arg(ab)+2*PI*(cbi-abi+1) by XCMPLX_1:8;
   hence thesis by A6,A7,A9,Th3;
  end;
 suppose Arg(cb)-Arg(ab) < 0;
 then A10: angle(a,b,c) = 2*PI+(Arg(cb)-Arg(ab)) by Def6;
   thus thesis proof
   per cases;
   suppose Arg(rcb)-Arg(rab) >= 0;
    then angle(ra,rb,rc)
     = Arg(cb)-Arg(ab)+2*PI*(cbi-abi+(-1+1)) by A8,Def6
    .= Arg(cb)-Arg(ab)+2*PI*(cbi-abi+-1+1) by XCMPLX_1:1
    .= Arg(cb)-Arg(ab)+(2*PI*(cbi-abi+-1)+2*PI*1) by XCMPLX_1:8
    .= 2*PI+(Arg(cb)-Arg(ab))+2*PI*(cbi-abi+-1) by XCMPLX_1:1;
   hence thesis by A6,A7,A10,Th3;
   suppose Arg(rcb)-Arg(rab) < 0;
   then angle(ra,rb,rc)
     = Arg(cb)-Arg(ab)+2*PI*(cbi-abi)+2*PI by A8,Def6
    .= 2*PI+(Arg(cb)-Arg(ab))+2*PI*(cbi-abi) by XCMPLX_1:1;
   hence thesis by A6,A7,A10,Th3;
 end;
end;

theorem Th93:
angle(a,b,a) = 0
proof Arg(a-b)-Arg(a-b) = 0 by XCMPLX_1:14; hence angle(a,b,a) = 0 by Def6;
end;

Lm7:
angle(x,y,z) <> 0 implies angle(z,y,x)=2*PI-angle(x,y,z)
proof assume A1: angle(x,y,z) <>0;
   now per cases;
  case A2: Arg(x-y)-Arg(z-y)>0;
    then A3: angle(z,y,x)= Arg(x-y)-Arg(z-y) by Def6;
     --(Arg(x-y)-Arg(z-y))>0 by A2; then -(Arg(x-y)-Arg(z-y))<0 by REAL_1:66;
    then -Arg(x-y)+Arg(z-y)<0 by XCMPLX_1:162;
    then Arg(z-y)-Arg(x-y)<0 by XCMPLX_0:def 8;
      then angle(x,y,z)=2*PI+(Arg(z-y)-Arg(x-y)) by Def6
                    .=2*PI -(Arg(x-y)-Arg(z-y)) by XCMPLX_1:38;
      then angle(x,y,z)+angle(z,y,x)=2*PI by A3,XCMPLX_1:27;
   hence angle(z,y,x)=2*PI-angle(x,y,z) by XCMPLX_1:26;
  case A4: Arg(x-y)-Arg(z-y)<=0;
     now assume Arg(x-y)-Arg(z-y)=0; then Arg(x-y)=0+Arg(z-y) by XCMPLX_1:27
      .=Arg(z-y); then Arg(z-y)-Arg(x-y)=0 by XCMPLX_1:14;
     hence contradiction by A1,Def6;
    end;
    then A5: angle(z,y,x)=2*PI+(Arg(x-y)-Arg(z-y)) by A4,Def6
                      .=2*PI -(Arg(z-y)-Arg(x-y)) by XCMPLX_1:38;
     --(Arg(x-y)-Arg(z-y))<=0 by A4; then -(Arg(x-y)-Arg(z-y))>=0 by REAL_1:66
;
    then -Arg(x-y)+Arg(z-y)>=0 by XCMPLX_1:162;
    then Arg(z-y)-Arg(x-y)>=0 by XCMPLX_0:def 8;
      then angle(x,y,z)+angle(z,y,x)
      =(2*PI -(Arg(z-y)-Arg(x-y)))+(Arg(z-y)-Arg(x-y)) by A5,Def6.=2*PI by
XCMPLX_1:27;
   hence angle(z,y,x)=2*PI-angle(x,y,z) by XCMPLX_1:26;
  end; hence angle(z,y,x)=2*PI-angle(x,y,z);
end;

theorem Th94: :: COMPLEX2:47, 48
angle(a,b,c) <> 0 iff angle(a,b,c)+angle(c,b,a) = 2*PI
proof
  hereby assume angle(a,b,c) <> 0;
    then angle(c,b,a) = 2*PI-angle(a,b,c) by Lm7;
   hence angle(a,b,c)+angle(c,b,a) = 2*PI by XCMPLX_1:27;
  end;
  assume angle(a,b,c)+angle(c,b,a) = 2*PI & angle(a,b,c) = 0;
  hence contradiction by Th84;
end;

theorem
 angle(a,b,c) <> 0 implies angle(c,b,a) <> 0
proof assume angle(a,b,c) <> 0;
then A1: angle(a,b,c)+angle(c,b,a) = 2*PI by Th94;
   assume not thesis; hence contradiction by A1,Th84;
end;

theorem
 angle(a,b,c) = PI implies angle(c,b,a) = PI
proof assume A1: angle(a,b,c) = PI; then angle(a,b,c)+angle(c,b,a) = 0+2*PI
  by Th94,COMPTRIG:21; then angle(c,b,a)-0 = 2*PI-PI by A1,XCMPLX_1:33;
 hence angle(c,b,a) = PI+PI-PI by XCMPLX_1:11 .= PI by XCMPLX_1:26;
end;

theorem Th97:
a <> b & a <> c & b <> c
 implies angle(a,b,c) <> 0 or angle(b,c,a) <> 0 or angle(c,a,b) <> 0
proof assume that
A1: a <> b and A2: a <> c and A3: b <> c; assume A4: not thesis;
then A5: Arg(a-c) = Arg (b-c) by Th88;
A6: Arg(b-a) = Arg (c-a) by A4,Th88;
A7: a-b <> 0 & b-a <> 0 & a-c <> 0 & c-a <> 0 & b-c <> 0 & c-b <> 0
    by A1,A2,A3,XCMPLX_1:15;
A8: -(a-b) = b-a & -(b-a) = a-b by XCMPLX_1:143;
A9: -(a-c) = c-a & -(c-a) = a-c by XCMPLX_1:143;
A10: -(c-b) = b-c & -(b-c) = c-b by XCMPLX_1:143;
   A11: Arg(a-b) = Arg (a-c) by A6,A7,A8,A9,Th78;
     Arg(c-b) < PI iff Arg (-(c-b)) >= PI by A7,Th25;
  hence thesis by A4,A5,A10,A11,Th88;
end;

Lm8:
Im a = 0 & Re a > 0 & 0 < Arg(b) & Arg(b) < PI
 implies angle(a,0c,b)+angle(0c,b,a)+angle(b,a,0c) = PI &
         0 < angle(0c,b,a) & 0 < angle(b,a,0c)
proof assume that
A1: Im a = 0 and A2: Re a > 0 and A3: 0 < Arg(b) and A4: Arg(b) < PI;
 a = [*Re a, 0*] by A1,COMPLEX1:8;
then A5: a = [**Re a, 0**] by HAHNBAN1:def 1;
     Arg [**Re a, 0**] = 0 by A2,COMPTRIG:53;
then A6: Arg(a) = 0 by A5,Th17;
then A7: Arg(-a) = Arg(a)+PI by A2,Th22,COMPLEX1:12,COMPTRIG:21 .= PI by A6;
    Arg b in ].0,PI.[ by A3,A4,JORDAN6:45;
then A8: Im b > 0 by Th27;
A9:  Im (a-b) = Im a - Im b by COMPLEX1:48 .= - Im b by A1,XCMPLX_1:150;
     -- Im b = Im b;
then A10:  Im (a-b) < 0 by A8,A9,REAL_1:66;
then A11: Arg(a-b) > PI by Th37; Arg(b-0c)-Arg(a-0c) >= 0 by A3,A6;
then A12: angle(a,0c,b) = Arg(b)-Arg(a) by Def6;
   now let a, b be Element of COMPLEX such that
A13: Im a = 0 and A14: Re a > 0 and A15: 0 < Arg(b) and A16: Arg(b) < PI;
     Arg b in ].0,PI.[ by A15,A16,JORDAN6:45;
then A17: Im b > 0 by Th27;
A18:  Im (b-a) = Im b - Im a by COMPLEX1:48 .= Im b by A13;
A19: Re (b-a) = Re b - Re a by COMPLEX1:48;
    --Re a = Re a; then - Re a < 0 by A14,REAL_1:66;
   then Re b + -Re a < Re b + 0 by REAL_1:67;
then A20: Re (b-a) < Re b by A19,XCMPLX_0:def 8;
   set ba = b-a; set Rb = Re b, Rba = Re ba, Ib = Im b, Iba = Im ba;
   set B = Arg b, BA = Arg ba, mb = |.b.|, mba = |.b-a.|;
    b = [* mb*cos B, mb*sin B *] &
   b = [* Re b, Im b *] by Th19,COMPLEX1:8;
then A21: Re b = mb*cos B & Im b = mb*sin B by ARYTM_0:12;
    b-a = [* mba*cos BA, mba*sin BA *] &
   b-a = [* Re ba, Im ba *] by Th19,COMPLEX1:8;
then A22: Re ba = mba*cos BA & Im ba = mba*sin BA by ARYTM_0:12;
A23: mb = sqrt(Rb^2+Ib^2) by COMPLEX1:def 16;
A24: mba = sqrt(Rba^2+Ib^2) by A18,COMPLEX1:def 16;
    A25: mb >= 0 & mb <> 0 by A17,COMPLEX1:12,133; A26: mba >= 0 & mba <> 0
by A17,A18,COMPLEX1:12,133; Rba^2 >= 0 & Ib^2 >= 0 by SQUARE_1:72;
   then A27: Rba^2 + Ib^2 >= 0+0 by REAL_1:55; Rb^2 >= 0 & Ib^2 >= 0 by
SQUARE_1:72;
   then A28: Rb^2 + Ib^2 >= 0+0 by REAL_1:55;
A29: sin BA > 0 by A17,A18,Th33;
then A30: mba/mb = (sin B)/sin BA by A18,A21,A22,A25,XCMPLX_1:95;
  per cases;
  suppose A31: 0 < Re ba; then Rb > 0 by A20,AXIOMS:22;
    then A32: B in ].0,PI/2.[ by A17,Th31;
    A33: BA in ].0,PI/2.[ by A17,A18,A31,Th31;
     Rb^2 > Rba^2 by A20,A31,SQUARE_1:78;
    then Rb^2 + Ib^2 > Rba^2 + Ib^2 by REAL_1:67;
    then mb > mba by A23,A24,A27,SQUARE_1:95;
    then mba/mb < 1 by A26,REAL_2:142;
    then ((sin B)/sin BA)*sin BA < 1*sin BA by A29,A30,REAL_1:70;
    then sin B < 1*sin BA by A29,XCMPLX_1:88;
    then BA > B by A32,A33,Th7; then BA+-B > B+-B by REAL_1:67;
    then BA-B > B+-B by XCMPLX_0:def 8;
   hence Arg ba - Arg b > 0 by XCMPLX_0:def 6;
  suppose A34: 0 = Rba; then ba = [* 0, Iba *] by COMPLEX1:8;
   then A35: BA = PI/2 by A17,A18,Th30;
         B in ].0,PI/2.[ by A17,A20,A34,Th31; then B < BA by A35,JORDAN6:45;
        then B+-B < BA+-B by REAL_1:67; then 0 < BA+-B by XCMPLX_0:def 6;
   hence Arg ba - Arg(b) > 0 by XCMPLX_0:def 8;
  suppose A36: 0 > Re ba;
   thus Arg ba - Arg(b) > 0 proof
   per cases;
    suppose 0 < Re b; then B in ].0,PI/2.[ by A17,Th31;
    then A37: B < PI/2 by JORDAN6:45;
       BA in ].PI/2,PI.[ by A17,A18,A36,Th32; then BA > PI/2 by JORDAN6:45;
      then BA > B by A37,AXIOMS:22; then B+-B < BA+-B by REAL_1:67;
      then 0 < BA+-B by XCMPLX_0:def 6;
     hence Arg ba - Arg(b) > 0 by XCMPLX_0:def 8;
    suppose 0 = Re b; then b = [* 0, Ib *] by COMPLEX1:8;
      then A38: B = PI/2 by A17,Th30; BA in ].PI/2,PI.[ by A17,A18,A36,Th32;
      then B < BA by A38,JORDAN6:45; then B+-B < BA+-B by REAL_1:67;
      then 0 < BA+-B by XCMPLX_0:def 6;
     hence Arg ba - Arg(b) > 0 by XCMPLX_0:def 8;
    suppose A39: 0 > Re b; then A40: B in ].PI/2,PI.[ by A17,Th32;
     A41: BA in ].PI/2,PI.[ by A17,A18,A36,Th32;
      Rb^2 < Rba^2 by A20,A39,JGRAPH_5:2;
     then Rb^2 + Ib^2 < Rba^2 + Ib^2 by REAL_1:67;
     then mb < mba by A23,A24,A28,SQUARE_1:95;
     then mba/mb > 1 by A25,REAL_2:142;
     then ((sin B)/sin BA)*sin BA > 1*sin BA by A29,A30,REAL_1:70;
     then sin B > 1*sin BA by A29,XCMPLX_1:88;
     then BA > B by A40,A41,Th8; then BA+-B > B+-B by REAL_1:67;
     then BA-B > B+-B by XCMPLX_0:def 8;
    hence Arg ba - Arg b > 0 by XCMPLX_0:def 6;
   end;
end;
then Arg(b-a)-Arg(b) > 0 by A1,A2,A3,A4;
     then Arg(-(a-b))-Arg(b) > 0 by XCMPLX_1:143;
     then Arg(a-b)-PI-Arg(b) > 0 by A10,A11,Th22,COMPLEX1:12;
     then Arg(a-b)-(Arg(b)+PI) > 0 by XCMPLX_1:36;
     then Arg(a-b)-Arg(-b) > 0 by A4,A8,Th22,COMPLEX1:12;
then A42: Arg(a-b)-Arg(0c-b) > 0 by XCMPLX_1:150;
then angle(0c,b,a) = Arg(a-b)-Arg(0c-b) by Def6;
then A43: angle(0c,b,a) = Arg(a-b)-Arg(-b) by XCMPLX_1:150;
      Arg(b-a) <= PI by A10,A11,Th26,COMPLEX1:12; then -Arg(b-a) >= -PI by
REAL_1:50;
     then Arg(-a)+-Arg(b-a) >= -PI+PI by A7,REAL_1:55;
     then Arg(-a)+-Arg(b-a) >= 0-PI+PI by XCMPLX_1:150;
     then Arg(-a)+-Arg(b-a) >= 0 by XCMPLX_1:27;
     then Arg(-a)-Arg(b-a) >= 0 by XCMPLX_0:def 8;
     then Arg(0c-a)-Arg(b-a) >= 0 by XCMPLX_1:150;
     then angle(b,a,0c) = Arg(0c-a)-Arg(b-a) by Def6;
then A44: angle(b,a,0c) = Arg(-a)-Arg(b-a) by XCMPLX_1:150;
A45:  Arg(b)-Arg(-b) = Arg(b)-(Arg(b)+PI) by A4,A8,Th22,COMPLEX1:12
    .= Arg(b)-Arg(b)-PI by XCMPLX_1:36 .= 0-PI by XCMPLX_1:14
    .= -PI by XCMPLX_1:150;
A46:  Arg(a)-Arg(-a) = Arg(a)-(Arg(a)+PI) by A2,A6,Th22,COMPLEX1:12,COMPTRIG:21
    .= Arg(a)-Arg(a)-PI by XCMPLX_1:36 .= 0-PI by XCMPLX_1:14
    .= -PI by XCMPLX_1:150;
A47: Arg(a-b)-Arg(b-a) = Arg(a-b)-Arg(-(a-b)) by XCMPLX_1:143
    .= Arg(a-b)-(Arg(a-b)-PI) by A10,A11,Th22,COMPLEX1:12 .= PI by XCMPLX_1:18;
 thus angle(a,0c,b)+angle(0c,b,a)+angle(b,a,0c)
     = Arg(b)-Arg(a)+Arg(a-b)-Arg(-b)+(Arg(-a)-Arg(b-a)) by A12,A43,A44,Lm1
    .= Arg(b)-Arg(a)-Arg(-b)+Arg(a-b)+(Arg(-a)-Arg(b-a)) by XCMPLX_1:29
    .= Arg(b)-Arg(-b)-Arg(a)+Arg(a-b)+(Arg(-a)-Arg(b-a)) by XCMPLX_1:21
    .= -PI-Arg(a)+Arg(a-b)+Arg(-a)-Arg(b-a) by A45,Lm1
    .= -PI-Arg(a)+Arg(-a)+Arg(a-b)-Arg(b-a) by XCMPLX_1:1
    .= -PI--PI+Arg(a-b)-Arg(b-a) by A46,XCMPLX_1:37
    .= -PI+PI+Arg(a-b)-Arg(b-a) by XCMPLX_1:151
    .= 0+Arg(a-b)-Arg(b-a) by XCMPLX_0:def 6 .= PI by A47;
  thus 0 < angle(0c,b,a) by A42,Def6;
 Arg(a)+PI = Arg(-a) by A46,Lm2;
then A48: Arg(-a)-(Arg(a-b)-PI) = Arg(a)+PI-Arg(a-b)+PI by XCMPLX_1:37
    .= Arg(a)+PI+PI-Arg(a-b) by XCMPLX_1:29
    .= Arg(a)+(PI+PI)-Arg(a-b) by XCMPLX_1:1
    .= Arg(a)+2*PI-Arg(a-b) by XCMPLX_1:11
    .= Arg(a)+(2*PI-Arg(a-b)) by Lm1; 2*PI > 0+Arg(a-b) by Th18;
    then 2*PI-Arg(a-b) > 0 & Arg(a) >= 0 by Th18,REAL_1:86;
    then Arg(a)+(2*PI-Arg(a-b)) > 0+0 by REAL_1:67;
  hence 0 < angle(b,a,0c) by A44,A47,A48,Lm3;
end;

theorem Th98:
a <> b & b <> c & 0 < angle(a,b,c) & angle(a,b,c) < PI
  implies angle(a,b,c)+angle(b,c,a)+angle(c,a,b) = PI &
          0 < angle(b,c,a) & 0 < angle(c,a,b)
proof assume that
A1: a <> b and A2: b <> c and A3: 0 < angle(a,b,c) and A4: angle(a,b,c) < PI;
A5: angle(a+-b,0c,c+-b) = angle(a+-b,b+-b,c+-b) by XCMPLX_0:def 6
   .= angle(a,b,c) by Th86;
   set r = -Arg (a+-b); set A = Rotate(a+-b,r), B = Rotate(c+-b, r);
A6: Rotate(0c,r) = 0c by Th66; a-b <> 0 by A1,XCMPLX_1:15;
then A7: a+-b <> 0c by XCMPLX_0:def 8;
A8: c+-b <> a+-b proof assume c+-b = a+-b; then c = a by XCMPLX_1:2;
      hence contradiction by A3,Th93;
     end; c-b <> 0 by A2,XCMPLX_1:15;
then A9: c+-b <> 0 by XCMPLX_0:def 8;
then A10: angle(a+-b,0c,c+-b) = angle(A,0c,B) by A6,A7,Th92;
A11: A = [* |.a+-b.|, 0 *] by Th69;
then A12: Im A = 0 by COMPLEX1:7;
    now assume a+-b = 0c; then a-b = 0c by XCMPLX_0:def 8;
     hence contradiction by A1,XCMPLX_1:15;
   end; then |.a+-b.| > 0 by COMPLEX1:133;
then A13: Re A > 0 by A11,COMPLEX1:7; then A14: Arg A = 0c by A12,Th34; then
Arg(B-0c)-Arg(A-0c)>= 0 by Th18;
then A15: angle(a,b,c) = Arg B by A5,A10,A14,Def6;
A16: angle(b,c,a) = angle(b+-b,c+-b,a+-b) by Th86
.= angle(0c,c+-b,a+-b) by XCMPLX_0:def 6.=angle(0c,B,A) by A6,A8,A9,Th92;
A17: angle(c,a,b) = angle(c+-b,a+-b,b+-b) by Th86
.= angle(c+-b,a+-b,0c) by XCMPLX_0:def 6.= angle(B,A,0c) by A6,A7,A8,Th92;
  hence angle(a,b,c)+angle(b,c,a)+angle(c,a,b) = PI by A3,A4,A5,A10,A12,A13,A15
,A16,Lm8;
  thus 0 < angle(b,c,a) by A3,A4,A12,A13,A15,A16,Lm8;
  thus 0 < angle(c,a,b) by A3,A4,A12,A13,A15,A17,Lm8;
end;

theorem Th99:
a <> b & b <> c & angle(a,b,c) > PI
  implies angle(a,b,c)+angle(b,c,a)+angle(c,a,b) = 5*PI &
          angle(b,c,a) > PI & angle(c,a,b) > PI
proof assume that
A1: a <> b and A2: b <> c and A3: angle(a,b,c) > PI;
   A4: angle(a,b,c) + angle(c,b,a)= 2*PI+0 by A3,Th94,COMPTRIG:21;
then A5: angle(a,b,c)-0 = 2*PI - angle(c,b,a) by XCMPLX_1:33;
A6: 0 <= angle(c,b,a) by Th84; A7: angle(c,b,a) <> 0 by A4,Th84;
A8: angle(c,b,a) < PI proof assume not thesis;
     then angle(a,b,c) + angle(c,b,a) > PI+PI by A3,REAL_1:67;
     then angle(a,b,c) + angle(c,b,a) > 2*PI by XCMPLX_1:11;
     hence contradiction by A3,Th94,COMPTRIG:21;
    end;
then A9: angle(c,b,a)+angle(b,a,c)+angle(a,c,b) = PI by A1,A2,A6,A7,Th98;
    angle(a,c,b) > 0 by A1,A2,A6,A7,A8,Th98;
   then angle(b,c,a) + angle(a,c,b)= 2*PI+0 by Th94;
then A10: angle(b,c,a)-0 = 2*PI - angle(a,c,b) by XCMPLX_1:33;
    angle(b,a,c) > 0 by A1,A2,A6,A7,A8,Th98;
   then angle(c,a,b)+angle(b,a,c)=2*PI+0 by Th94;
   then angle(c,a,b)-0 =2*PI - angle(b,a,c) by XCMPLX_1:33;
   then angle(a,b,c)+angle(b,c,a)+angle(c,a,b)
 = 2*PI+(2*PI - angle(c,b,a))-angle(a,c,b)+(2*PI - angle(b,a,c)) by A5,A10,Lm1
.= 2*PI+((2*PI - angle(c,b,a))-angle(a,c,b))+(2*PI - angle(b,a,c)) by Lm1
.= 2*PI+(2*PI - (angle(c,b,a)+angle(a,c,b)))+(2*PI - angle(b,a,c))
     by XCMPLX_1:36
.= 2*PI+2*PI - (angle(c,b,a)+angle(a,c,b))+(2*PI - angle(b,a,c)) by Lm1
.= 2*PI+2*PI - (angle(c,b,a)+angle(a,c,b))+2*PI - angle(b,a,c) by Lm1
.= 2*PI+2*PI+2*PI - (angle(c,b,a)+angle(a,c,b)) - angle(b,a,c) by XCMPLX_1:29
.= 2*PI+2*PI+2*PI - (angle(c,b,a)+angle(a,c,b)+angle(b,a,c)) by XCMPLX_1:36
.= 2*PI+2*PI+2*PI - (angle(c,b,a)+angle(b,a,c)+angle(a,c,b)) by XCMPLX_1:1;
  hence
  A11: angle(a,b,c)+angle(b,c,a)+angle(c,a,b)
   = 2*PI+2*PI+(PI+PI)-PI by A9,XCMPLX_1:11 .= 2*PI+2*PI+PI+PI-PI by XCMPLX_1:1
  .= 2*PI+2*PI+PI by XCMPLX_1:26 .= (2+2)*PI+1*PI by XCMPLX_1:8
  .= (2+2+1)*PI by XCMPLX_1:8 .= 5*PI;
A12: 2*PI+PI+2*PI = 2*PI+1*PI+2*PI .= (2+1)*PI+2*PI by XCMPLX_1:8
      .= (3+2)*PI by XCMPLX_1:8 .= 5*PI;
A13: 2*PI+2*PI+PI=(2+2)*PI+1*PI by XCMPLX_1:8.=(4+1)*PI by XCMPLX_1:8 .= 5*PI;
A14: angle(a,b,c) < 2*PI by Th84;
  hereby assume A15: angle(b,c,a) <= PI;
  A16: angle(c,a,b) < 2*PI by Th84;
       angle(a,b,c)+angle(b,c,a) < 2*PI+PI by A14,A15,REAL_1:67;
    hence contradiction by A11,A12,A16,REAL_1:67;
  end;
  assume A17: angle(c,a,b) <= PI; angle(b,c,a) < 2*PI by Th84;
      then angle(a,b,c)+angle(b,c,a) < 2*PI+2*PI by A14,REAL_1:67;
    hence contradiction by A11,A13,A17,REAL_1:67;
end;

Lm9:
Im a = 0 & Re a > 0 & Arg(b) = PI
 implies angle(a,0c,b)+angle(0c,b,a)+angle(b,a,0c) = PI &
         0 = angle(0c,b,a) & 0 = angle(b,a,0c)
proof assume that
A1: Im a = 0 and A2: Re a > 0 and A3: Arg(b) = PI; a = [*Re a, 0*] by A1,
COMPLEX1:8;
then A4: a = [**Re a, 0**] by HAHNBAN1:def 1;
     Arg [**Re a, 0**] = 0 by A2,COMPTRIG:53;
then A5: Arg(a) = 0 by A4,Th17;
then A6: Arg(-a) = Arg(a)+PI by A2,Th22,COMPLEX1:12,COMPTRIG:21 .= PI by A5;
A7: Re b < 0 & Im b = 0 by A3,Th35;
A8:  Im (a-b) = Im a - Im b by COMPLEX1:48 .= - Im b by A1,XCMPLX_1:150;
    A9: Re b +0 < Re a by A2,A7,AXIOMS:22;
then Re a - Re b > 0 by REAL_1:86;
then A10: Re (a-b) > 0 by COMPLEX1:48;
then A11: Arg(a-b) = 0 by A7,A8,Th34;
     --(Re a - Re b) > 0 by A9,REAL_1:86; then -(Re a - Re b) < 0 by REAL_1:66
;
    then Re b+-Re a <0 by XCMPLX_1:162; then Re b - Re a < 0 by XCMPLX_0:def 8;
then A12: Re (b-a) < 0 by COMPLEX1:48;
    A13: Im (b-a) = Im b - Im a by COMPLEX1:48 .= 0 by A1,A3,Th35;
then A14: Arg(b-a) = PI by A12,Th35; Arg(b-0c)-Arg(a-0c) > 0 by A3,A5,COMPTRIG:
21;
then A15: angle(a,0c,b) = Arg(b)-Arg(a) by Def6;
     Arg -b = Arg b -PI by A3,Th20,Th22,COMPTRIG:21;
then A16: Arg b = Arg -b + PI by XCMPLX_1:27;
      Arg (b-a) - Arg b = 0 by A3,A14,XCMPLX_1:14;
     then Arg(-(a-b))-Arg(b) = 0 by XCMPLX_1:143;
     then Arg(a-b)+PI-Arg(b) = 0 by A10,A11,Th22,COMPLEX1:12,COMPTRIG:21;
     then Arg(a-b)+PI-PI-Arg(-b) = 0 by A16,XCMPLX_1:36;
     then Arg(a-b)-Arg(-b) = 0 by XCMPLX_1:26;
then A17: Arg(a-b)-Arg(0c-b) = 0 by XCMPLX_1:150;
then A18: angle(0c,b,a) = Arg(a-b)-Arg(0c-b) by Def6;
then A19: angle(0c,b,a) = Arg(a-b)-Arg(-b) by XCMPLX_1:150;
      -Arg(b-a) = -PI by A12,A13,Th35;
     then Arg(-a)+-Arg(b-a) = 0-PI+PI by A6,XCMPLX_1:150;
     then Arg(-a)+-Arg(b-a) = 0 by XCMPLX_1:27;
     then Arg(-a)-Arg(b-a) = 0 by XCMPLX_0:def 8;
     then Arg(0c-a)-Arg(b-a) = 0 by XCMPLX_1:150;
     then angle(b,a,0c) = Arg(0c-a)-Arg(b-a) by Def6;
then A20: angle(b,a,0c) = Arg(-a)-Arg(b-a) by XCMPLX_1:150;
      Arg -b = Arg b -PI by A3,Th20,Th22,COMPTRIG:21;
     then PI+Arg -b=Arg b by XCMPLX_1:27;
then A21:  Arg(b)-Arg(-b) = PI by XCMPLX_1:26;
A22:  Arg(a)-Arg(-a) = Arg(a)-(Arg(a)+PI) by A2,A5,Th22,COMPLEX1:12,COMPTRIG:21
  .= Arg(a)-Arg(a)-PI by XCMPLX_1:36.=0-PI by XCMPLX_1:14.=-PI by XCMPLX_1:150;
 thus
A23: angle(a,0c,b)+angle(0c,b,a)+angle(b,a,0c)
     = Arg(b)-Arg(a)+Arg(a-b)-Arg(-b)+(Arg(-a)-Arg(b-a)) by A15,A19,A20,Lm1
    .= Arg(b)-Arg(a)-Arg(-b)+Arg(a-b)+(Arg(-a)-Arg(b-a)) by XCMPLX_1:29
    .= Arg(b)-Arg(-b)-Arg(a)+Arg(a-b)+(Arg(-a)-Arg(b-a)) by XCMPLX_1:21
    .= PI-Arg(a)+Arg(a-b)+Arg(-a)-Arg(b-a) by A21,Lm1
    .= PI-Arg(a)+Arg(-a)+Arg(a-b)-Arg(b-a) by XCMPLX_1:1
    .= PI--PI+Arg(a-b)-Arg(b-a) by A22,XCMPLX_1:37
    .= PI+PI+Arg(a-b)-Arg(b-a) by XCMPLX_1:151
    .= PI+PI+(Arg(a-b)-Arg(b-a)) by Lm1 .= PI+PI+-PI by A11,A14,XCMPLX_1:150
    .= PI+(PI+-PI) by XCMPLX_1:1 .= PI+0 by XCMPLX_0:def 6 .= PI;
  thus 0 = angle(0c,b,a) by A17,Def6;
  thus 0 = angle(b,a,0c) by A3,A5,A15,A17,A18,A23,XCMPLX_1:3;
end;

theorem Th100:
a <> b & b <> c & angle(a,b,c) = PI implies angle(b,c,a) = 0 & angle(c,a,b) = 0
proof assume that
A1: a <> b and A2: b <> c and A3: angle(a,b,c) = PI;
A4: angle(a+-b,0c,c+-b) = angle(a+-b,b+-b,c+-b) by XCMPLX_0:def 6
   .= angle(a,b,c) by Th86; set r = -Arg (a+-b);
A5: Rotate(0c,r) = 0c by Th66; set A = Rotate(a+-b,r), B = Rotate(c+-b, r);
     a-b <> 0 by A1,XCMPLX_1:15;
then A6: a+-b <> 0c by XCMPLX_0:def 8;
A7: c+-b <> a+-b proof assume c+-b = a+-b; then c = a by XCMPLX_1:2;
      hence contradiction by A3,Th93,COMPTRIG:21;
     end; c-b <> 0 by A2,XCMPLX_1:15;
then A8: c+-b <> 0 by XCMPLX_0:def 8;
then A9: angle(a+-b,0c,c+-b) = angle(A,0c,B) by A5,A6,Th92;
A10: A = [* |.a+-b.|, 0 *] by Th69;
then A11: Im A = 0 by COMPLEX1:7;
    now assume a+-b = 0c; then a-b = 0c by XCMPLX_0:def 8;
     hence contradiction by A1,XCMPLX_1:15;
   end; then |.a+-b.| > 0 by COMPLEX1:133;
then A12: Re A > 0 by A10,COMPLEX1:7; then A13: Arg A = 0c by A11,Th34;
then Arg(B-0c)-Arg(A-0c)>=0 by Th18;
then A14: angle(a,b,c) = Arg B by A4,A9,A13,Def6;
A15: angle(b,c,a) = angle(b+-b,c+-b,a+-b) by Th86
 .=angle(0c,c+-b,a+-b)by XCMPLX_0:def 6.= angle(0c,B,A) by A5,A7,A8,Th92;
A16: angle(c,a,b) = angle(c+-b,a+-b,b+-b) by Th86
 .=angle(c+-b,a+-b,0c) by XCMPLX_0:def 6.=angle(B,A,0c) by A5,A6,A7,Th92;
  thus angle(b,c,a) = 0 by A3,A11,A12,A14,A15,Lm9;
  thus angle(c,a,b) = 0 by A3,A11,A12,A14,A16,Lm9;
end;

theorem Th101:
a <> b & a <> c & b <> c & angle(a,b,c) = 0
 implies angle(b,c,a) = 0 & angle(c,a,b) = PI or
         angle(b,c,a) = PI & angle(c,a,b) = 0
proof assume that
A1: a <> b & a <> c & b <> c & angle(a,b,c) = 0;
 per cases by A1,Th97;
 suppose A2: angle(b,c,a) <> 0; A3: 0 <= angle(b,c,a) by Th84;
  thus thesis proof
   per cases by REAL_1:def 5;
   suppose angle(b,c,a) < PI; hence thesis by A1,A2,A3,Th98;
   suppose angle(b,c,a) = PI; hence thesis by A1,Th100;
   suppose angle(b,c,a) > PI; hence thesis by A1,Th99,COMPTRIG:21;
  end;
 suppose A4: angle(c,a,b) <> 0; A5: 0 <= angle(c,a,b) by Th84;
  thus thesis proof
   per cases by REAL_1:def 5;
   suppose angle(c,a,b) < PI; hence thesis by A1,A4,A5,Th98;
   suppose angle(c,a,b) = PI; hence thesis by A1,Th100;
   suppose angle(c,a,b) > PI; hence thesis by A1,Th99,COMPTRIG:21;
  end;
end;

Lm10:
a <> b & a <> c & b <> c & angle(a,b,c) = 0
 implies angle(b,c,a)+angle(c,a,b) = PI
proof assume A1: a <> b & a <> c & b <> c & angle(a,b,c) = 0;
  per cases by A1,Th101;
  suppose angle(b,c,a) = 0 & angle(c,a,b) = PI;
    hence angle(b,c,a)+angle(c,a,b) = PI;
  suppose angle(b,c,a) = PI & angle(c,a,b) = 0;
    hence angle(b,c,a)+angle(c,a,b) = PI;
end;

theorem
      angle(a,b,c)+angle(b,c,a)+angle(c,a,b) = PI or
     angle(a,b,c)+angle(b,c,a)+angle(c,a,b) = 5*PI
 iff a <> b & a <> c & b <> c
proof
 hereby assume A1: angle(a,b,c)+angle(b,c,a)+angle(c,a,b) = PI
            or angle(a,b,c)+angle(b,c,a)+angle(c,a,b) = 5*PI;
  per cases by A1;
  suppose A2: angle(a,b,c)+angle(b,c,a)+angle(c,a,b) = PI;
   thus a <> b & a <> c & b <> c proof assume
   A3: not (a <> b & a <> c & b <> c);
   per cases by A3;
   suppose A4: a=b;
   A5: angle(a,c,a) = 0 by Th93;
        not (angle(a,a,c) = 0 & angle(c,a,a) = 0) by A2,A4,Th93,COMPTRIG:21;
     hence contradiction by A2,A4,A5,Th94,COMPTRIG:21;
   suppose A6: a=c;
   A7: angle(a,b,a) = 0 by Th93;
        not (angle(a,a,b) = 0 & angle(b,a,a) = 0) by A2,A6,Th93,COMPTRIG:21;
     hence contradiction by A2,A6,A7,Th94,COMPTRIG:21;
   suppose A8: b=c;
   A9: angle(b,a,b) = 0 by Th93;
        not (angle(a,b,b) = 0 & angle(b,b,a) = 0) by A2,A8,Th93,COMPTRIG:21;
     hence contradiction by A2,A8,A9,Th94,COMPTRIG:21;
   end;
  suppose A10: angle(a,b,c)+angle(b,c,a)+angle(c,a,b) = 5*PI;
      A11: (2+2)*PI < 5*PI by COMPTRIG:21,REAL_1:70;
  then A12: 2*PI+2*PI < 5*PI by XCMPLX_1:8;
   thus a <> b & a <> c & b <> c proof assume
   A13: not (a <> b & a <> c & b <> c);
   per cases by A13;
   suppose a=b;
   then A14: angle(b,c,a) = 0 by Th93;
   A15: angle(c,a,b) < 2*PI by Th84;
        angle(a,b,c)+angle(b,c,a) < 2*PI by A14,Th84;
     hence contradiction by A10,A12,A15,REAL_1:67;
   suppose b=c;
   then A16: angle(c,a,b) = 0 by Th93;
        angle(a,b,c) < 2*PI & angle(b,c,a) < 2*PI by Th84;
       then angle(a,b,c)+angle(b,c,a) < 2*PI+2*PI by REAL_1:67;
     hence contradiction by A10,A11,A16,XCMPLX_1:8;
   suppose a=c;
   then A17: angle(a,b,c) = 0 by Th93;
   A18: angle(c,a,b) < 2*PI by Th84;
        angle(a,b,c)+angle(b,c,a) < 2*PI by A17,Th84;
     hence contradiction by A10,A12,A18,REAL_1:67;
   end;
 end;
  assume A19: a <> b & a <> c & b <> c;
  per cases by REAL_1:def 5;
  suppose angle(a,b,c) = 0;
   hence thesis by A19,Lm10;
  suppose A20: 0 <> angle(a,b,c) & angle(a,b,c) < PI;
    0 <= angle(a,b,c) by Th84;
   hence thesis by A19,A20,Th98;
  suppose A21: 0 <> angle(a,b,c) & angle(a,b,c) = PI;
    then angle(b,c,a) = 0 & angle(c,a,b) = 0 by A19,Th100;
   hence thesis by A21;
  suppose 0 <> angle(a,b,c) & angle(a,b,c) > PI;
   hence thesis by A19,Th99;
 end;


Back to top