The abstract of the Mizar article:

Field Properties of Complex Numbers --- Requirements

by

Library Committee

Received May 29, 2003

MML identifier: ARITHM

[ Mizar article, MML identifier index ]

environ

 vocabulary ARYTM, ARYTM_1, RELAT_1, ARYTM_3, ORDINAL1, ORDINAL2, COMPLEX1,
      OPPCAT_1, XCMPLX_0;
 notation SUBSET_1, ORDINAL1, ORDINAL2, NUMBERS, ARYTM_0, XCMPLX_0;
 constructors ARYTM_0, ARYTM_1, XCMPLX_0, FUNCT_4, ARYTM_3, XBOOLE_0;
 clusters ARYTM_2, NUMBERS, XCMPLX_0, ARYTM_3, ZFMISC_1, XBOOLE_0;
 requirements NUMERALS, SUBSET, BOOLE;


begin
:: This file contains statements which are obvious for Mizar checker if
:: "requirements ARITHM" is included in the environment description
:: of an article. "requirements NUMERALS" is also required.
:: They are published for testing purposes only.
:: Users should use appropriate requirements instead of referencing
:: to these theorems.
:: Some of these items need also other requirements for proper work.

 reserve x for complex number;

theorem :: ARITHM:1
  x + 0 = x;

theorem :: ARITHM:2
  x * 0 = 0;

theorem :: ARITHM:3
  1 * x = x;

theorem :: ARITHM:4
   x - 0 = x;

theorem :: ARITHM:5
   0 / x = 0;

theorem :: ARITHM:6
   x / 1 = x;