:: Field Properties of Complex Numbers - Requirements
:: by Library Committee
::
:: Received May 29, 2003
:: Copyright (c) 2003-2016 Association of Mizar Users

environ

vocabularies HIDDEN, XCMPLX_0, ARYTM_3, CARD_1, NUMBERS, SUBSET_1, ARYTM_0, ARYTM_1, RELAT_1;
notations HIDDEN, TARSKI, SUBSET_1, ORDINAL1, NUMBERS, ARYTM_0, XCMPLX_0;
definitions ;
theorems ARYTM_0, XCMPLX_0, NUMBERS;
schemes ;
registrations XCMPLX_0, ORDINAL1;
constructors HIDDEN, FUNCT_4, ARYTM_0, XCMPLX_0, NUMBERS;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE;
equalities ;
expansions ;


0 in NAT
;

then reconsider Z = 0 as Element of REAL by NUMBERS:19;

1 in NAT
;

then reconsider J = 1 as Element of REAL by NUMBERS:19;

theorem Th1: :: ARITHM:1
for x being Complex holds x + 0 = x
proof end;

Lm1: - 0 = 0
proof end;

Lm2: opp Z = 0
proof end;

theorem Th2: :: ARITHM:2
for x being Complex holds x * 0 = 0
proof end;

theorem Th3: :: ARITHM:3
for x being Complex holds 1 * x = x
proof end;

theorem :: ARITHM:4
for x being Complex holds x - 0 = x
proof end;

theorem :: ARITHM:5
for x being Complex holds 0 / x = 0
proof end;

Lm3: 1 " = 1
proof end;

theorem :: ARITHM:6
for x being Complex holds x / 1 = x
proof end;