:: Field Properties of Complex Numbers  Requirements
:: by Library Committee
::
:: Received May 29, 2003
:: Copyright (c) 20032021 Association of Mizar Users
theorem
Th1
:
:: ARITHM:1
for
x
being
Complex
holds
x
+
0
=
x
proof
end;
Lm1
:

0
=
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;