:: Field Properties of Complex Numbers - Requirements :: by Library Committee :: :: Received May 29, 2003 :: Copyright (c) 2003-2012 Association of Mizar Users begin theorem Th1: :: ARITHM:1 for x being complex number holds x + 0 = x proofend; Lm1: - 0 = 0 proofend; Lm2: opp 0 = 0 proofend; theorem Th2: :: ARITHM:2 for x being complex number holds x * 0 = 0 proofend; theorem Th3: :: ARITHM:3 for x being complex number holds 1 * x = x proofend; theorem :: ARITHM:4 for x being complex number holds x - 0 = x proofend; theorem :: ARITHM:5 for x being complex number holds 0 / x = 0 proofend; Lm3: 1 " = 1 proofend; theorem :: ARITHM:6 for x being complex number holds x / 1 = x proofend;