The abstract of the Mizar article:

The Field of Complex Numbers

by

Anna Justyna Milewska

Received January 18, 2000

MML identifier: COMPLFLD

[ Mizar article, MML identifier index ]

environ

 vocabulary COMPLEX1, ARYTM, VECTSP_1, RLVECT_1, COMPLSP1, BINOP_1, LATTICES,
      FUNCT_1, ARYTM_1, RELAT_1, ARYTM_3, ABSVALUE, COMPLFLD, XCMPLX_0;
 notation TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, ORDINAL1, NUMBERS, ARYTM_0,
      XCMPLX_0, XREAL_0, REAL_1, BINOP_1, ABSVALUE, RLVECT_1, VECTSP_1,
      COMPLSP1, COMPLEX1, FUNCT_1;
 constructors REAL_1, ABSVALUE, VECTSP_1, COMPLSP1, DOMAIN_1, BINOP_1,
      COMPLEX1, MEMBERED, ARYTM_0, ARYTM_3, FUNCT_4;
 clusters VECTSP_1, RELSET_1, XREAL_0, COMPLEX1, MEMBERED;
 requirements NUMERALS, SUBSET, BOOLE, ARITHM;


begin

canceled;

  theorem :: COMPLFLD:2
   for x1,y1,x2,y2 be Element of REAL holds
    [*x1,y1*] + [*x2,y2*] = [*x1 + x2,y1 + y2*];

  definition
   func F_Complex -> strict doubleLoopStr means
:: COMPLFLD:def 1
    the carrier of it = COMPLEX &
    the add of it = addcomplex &
    the mult of it = multcomplex &
    the unity of it = 1r &
    the Zero of it = 0c;
  end;

  definition
   cluster F_Complex -> non empty;
  end;

definition
  cluster -> complex Element of F_Complex;
end;

  definition
   cluster F_Complex -> add-associative right_zeroed right_complementable
         Abelian commutative associative left_unital
         right_unital distributive Field-like non degenerated;
  end;

  theorem :: COMPLFLD:3
   for x1,y1 be Element of F_Complex
   for x2,y2 be Element of COMPLEX st x1 = x2 & y1 = y2 holds
    x1 + y1 = x2 + y2;

  theorem :: COMPLFLD:4
   for x1 be Element of F_Complex
   for x2 be Element of COMPLEX st x1 = x2 holds
    - x1 = - x2;

  theorem :: COMPLFLD:5
   for x1,y1 be Element of F_Complex
   for x2,y2 be Element of COMPLEX st x1 = x2 & y1 = y2 holds
    x1 - y1 = x2 - y2;

  theorem :: COMPLFLD:6
   for x1,y1 be Element of F_Complex
   for x2,y2 be Element of COMPLEX st x1 = x2 & y1 = y2 holds
    x1 * y1 = x2 * y2;

  theorem :: COMPLFLD:7
   for x1 be Element of F_Complex
   for x2 be Element of COMPLEX st x1 = x2 & x1 <> 0.F_Complex holds
    x1" = x2";

  theorem :: COMPLFLD:8
   for x1,y1 be Element of F_Complex
   for x2,y2 be Element of COMPLEX st
    x1 = x2 & y1 = y2 & y1 <> 0.F_Complex holds x1/y1 = x2/y2;

  theorem :: COMPLFLD:9
   0.F_Complex = 0c;

  theorem :: COMPLFLD:10
   1_ F_Complex = 1r;

  theorem :: COMPLFLD:11
     1_ F_Complex + 1_ F_Complex <> 0.F_Complex;

  definition
   let z be Element of F_Complex;
   func z*' -> Element of F_Complex means
:: COMPLFLD:def 2
    ex z' be Element of COMPLEX
    st z = z' & it = z'*';
  end;

  definition
   let z be Element of F_Complex;
   func |.z.| -> real number means
:: COMPLFLD:def 3
    ex z' be Element of COMPLEX st z = z' & it = |.z'.|;
  end;

  definition
   let z be Element of F_Complex;
   redefine func |.z.| -> Element of REAL;
  end;

  theorem :: COMPLFLD:12
   for x1 be Element of F_Complex
   for x2 be Element of COMPLEX st
    x1 = x2 holds x1*' = x2*';

reserve z,z1,z2,z3,z4 for Element of F_Complex;

canceled 16;

  theorem :: COMPLFLD:29
     -z = (-1_ F_Complex) * z;

canceled 5;

  theorem :: COMPLFLD:35
     z1 - -z2 = z1 + z2;

canceled 5;

  theorem :: COMPLFLD:41
     z1 = z1 + z - z;

  theorem :: COMPLFLD:42
     z1 = z1 - z + z;

canceled 4;

  theorem :: COMPLFLD:47
     z1 <> 0.F_Complex & z2 <> 0.F_Complex &
   z1" = z2" implies z1 = z2;

  theorem :: COMPLFLD:48
     z2 <> 0.F_Complex &
    (z1 * z2 = the unity of F_Complex or z2 * z1 = the unity of F_Complex)
    implies z1 = z2";

  theorem :: COMPLFLD:49
     z2 <> 0.F_Complex & (z1 * z2 = z3 or z2 * z1 = z3) implies
    z1 = z3 * z2" & z1 = z2" * z3;

  theorem :: COMPLFLD:50
     (the unity of F_Complex)" = the unity of F_Complex;

  theorem :: COMPLFLD:51
     z1 <> 0.F_Complex & z2 <> 0.F_Complex implies
    (z1 * z2)" = z1" * z2";

canceled;

  theorem :: COMPLFLD:53
     z <> 0.F_Complex implies (-z)" = -(z");

canceled;

  theorem :: COMPLFLD:55
     z1 <> 0.F_Complex & z2 <> 0.F_Complex implies
    z1" + z2" = (z1 + z2) * (z1 * z2)";

  theorem :: COMPLFLD:56
     z1 <> 0.F_Complex & z2 <> 0.F_Complex implies
    z1" - z2" = (z2 - z1) * (z1 * z2)";

canceled;

  theorem :: COMPLFLD:58
     z <> 0.F_Complex implies z" = (the unity of F_Complex) / z;

  theorem :: COMPLFLD:59
     z / (the unity of F_Complex) = z;

  theorem :: COMPLFLD:60
     z <> 0.F_Complex implies z / z = the unity of F_Complex;

  theorem :: COMPLFLD:61
     z <> 0.F_Complex implies (0.F_Complex) / z = 0.F_Complex;

  theorem :: COMPLFLD:62
   z2 <> 0.F_Complex & z1 / z2 = 0.F_Complex implies
    z1 = 0.F_Complex;

  theorem :: COMPLFLD:63
     z2 <> 0.F_Complex & z4 <> 0.F_Complex implies
    (z1 / z2) * (z3 / z4) = (z1 * z3) / (z2 * z4);

  theorem :: COMPLFLD:64
     z2 <> 0.F_Complex implies z * (z1 / z2) = (z * z1) / z2;

  theorem :: COMPLFLD:65
     z2 <> 0.F_Complex & z1 / z2 = the unity of F_Complex implies
    z1 = z2;

  theorem :: COMPLFLD:66
     z <> 0.F_Complex implies z1 = (z1 * z) / z;

  theorem :: COMPLFLD:67
     z1 <> 0.F_Complex & z2 <> 0.F_Complex implies
    (z1 / z2)" = z2 / z1;

  theorem :: COMPLFLD:68
     z1 <> 0.F_Complex & z2 <> 0.F_Complex implies
    (z1" / z2") = z2 / z1;

  theorem :: COMPLFLD:69
     z2 <> 0.F_Complex implies z1 / z2" = z1 * z2;

  theorem :: COMPLFLD:70
     z1 <> 0.F_Complex & z2 <> 0.F_Complex implies
    z1" / z2 = (z1 * z2)";

  theorem :: COMPLFLD:71
     z1 <> 0.F_Complex & z2 <> 0.F_Complex implies
    z1"* (z / z2) = z / (z1 * z2);

  theorem :: COMPLFLD:72
     z <> 0.F_Complex & z2 <> 0.F_Complex implies
    (z1 / z2) = (z1 * z) / (z2 * z) & (z1 / z2) = (z * z1) / (z * z2);

  theorem :: COMPLFLD:73
     z2 <> 0.F_Complex & z3 <> 0.F_Complex implies
    z1 / (z2 * z3) = z1 / z2 / z3;

  theorem :: COMPLFLD:74
     z2 <> 0.F_Complex & z3 <> 0.F_Complex implies
    (z1 * z3) / z2 = z1 / (z2 / z3);

  theorem :: COMPLFLD:75
     z2 <> 0.F_Complex & z3 <> 0.F_Complex &
    z4 <> 0.F_Complex implies
    (z1 / z2) / (z3 / z4) = (z1 * z4) / (z2 * z3);

  theorem :: COMPLFLD:76
     z2 <> 0.F_Complex & z4 <> 0.F_Complex implies
    z1 / z2 + z3 / z4 = (z1 * z4 + z3 * z2) / (z2 * z4);

  theorem :: COMPLFLD:77
     z <> 0.F_Complex implies z1 / z + z2 / z = (z1 + z2) / z;

  theorem :: COMPLFLD:78
     z2 <> 0.F_Complex implies -(z1 / z2) = (-z1) / z2 &
    -(z1 / z2) = z1 / (-z2);

  theorem :: COMPLFLD:79
     z2 <> 0.F_Complex implies z1 / z2 = (-z1) / (-z2);

  theorem :: COMPLFLD:80
     z2 <> 0.F_Complex & z4 <> 0.F_Complex implies
    z1 / z2 - z3 / z4 = (z1 * z4 - z3 * z2) / (z2 * z4);

  theorem :: COMPLFLD:81
     z <> 0.F_Complex implies z1 / z - z2 / z = (z1 - z2) / z;

  theorem :: COMPLFLD:82
     z2 <> 0.F_Complex & (z1 * z2 = z3 or z2 * z1 = z3) implies
    z1 = z3 / z2;

  theorem :: COMPLFLD:83
     (the Zero of F_Complex)*' = the Zero of F_Complex;

  theorem :: COMPLFLD:84
   z*' = the Zero of F_Complex implies z = the Zero of F_Complex;

  theorem :: COMPLFLD:85
     (the unity of F_Complex)*' = the unity of F_Complex;

  theorem :: COMPLFLD:86
     z*'*' = z;

  theorem :: COMPLFLD:87
     (z1 + z2)*' = z1*' + z2*';

  theorem :: COMPLFLD:88
     (-z)*' = -(z*');

  theorem :: COMPLFLD:89
     (z1 - z2)*' = z1*' - z2*';

  theorem :: COMPLFLD:90
     (z1 * z2)*' = z1*' * z2*';

  theorem :: COMPLFLD:91
     z <> the Zero of F_Complex implies z"*' = z*'";

  theorem :: COMPLFLD:92
     z2 <> the Zero of F_Complex implies (z1 / z2)*' = (z1*') / (z2*');

  theorem :: COMPLFLD:93
     |.the Zero of F_Complex.| = 0;

  theorem :: COMPLFLD:94
     |.z.| = 0 implies z = 0.F_Complex;

  theorem :: COMPLFLD:95
     0 <= |.z.|;

  theorem :: COMPLFLD:96
     z <> 0.F_Complex iff 0 < |.z.|;

  theorem :: COMPLFLD:97
     |.the unity of F_Complex.| = 1;

  theorem :: COMPLFLD:98
     |.-z.| = |.z.|;

  theorem :: COMPLFLD:99
     |.z*'.| = |.z.|;

  theorem :: COMPLFLD:100
     |.z1 + z2.| <= |.z1.| + |.z2.|;

  theorem :: COMPLFLD:101
     |.z1 - z2.| <= |.z1.| + |.z2.|;

  theorem :: COMPLFLD:102
     |.z1.| - |.z2.| <= |.z1 + z2.|;

  theorem :: COMPLFLD:103
     |.z1.| - |.z2.| <= |.z1 - z2.|;

  theorem :: COMPLFLD:104
     |.z1 - z2.| = |.z2 - z1.|;

  theorem :: COMPLFLD:105
     |.z1 - z2.| = 0 iff z1 = z2;

  theorem :: COMPLFLD:106
     z1 <> z2 iff 0 < |.z1 - z2.|;

  theorem :: COMPLFLD:107
     |.z1 - z2.| <= |.z1 - z.| + |.z - z2.|;

  theorem :: COMPLFLD:108
     abs(|.z1.| - |.z2.|) <= |.z1 - z2.|;

  theorem :: COMPLFLD:109
     |.z1*z2.| = |.z1.|*|.z2.|;

  theorem :: COMPLFLD:110
     z <> the Zero of F_Complex implies |.z".| = |.z.|";

  theorem :: COMPLFLD:111
     z2 <> the Zero of F_Complex implies |.z1.| / |.z2.| = |.z1 / z2.|;

  theorem :: COMPLFLD:112
     |.z * z.| = |.z * z*'.|;