Volume 2, 1990

University of Bialystok

Copyright (c) 1990 Association of Mizar Users

**Czeslaw Bylinski**- Warsaw University, Bialystok
- Supported by RPBP.III-24.C1.

- We define the set $\Bbb C$ of complex numbers as the set of all ordered pairs $z =\langle a,b\rangle$ where $a$ and $b$ are real numbers and where addition and multiplication are defined. We define the real and imaginary parts of $z$ and denote this by $a = \Re(z)$, $b = \Im(z)$. These definitions satisfy all the axioms for a field. $0_{\Bbb C} = 0+0i$ and $1_{\Bbb C} = 1+0i$ are identities for addition and multiplication respectively, and there are multiplicative inverses for each non zero element in $\Bbb C$. The difference and division of complex numbers are also defined. We do not interpret the set of all real numbers $\Bbb R$ as a subset of $\Bbb C$. From here on we do not abandon the ordered pair notation for complex numbers. For example: $i^2 = (0+1i)^2 = -1+0i \neq -1$. We conclude this article by introducing two operations on $\Bbb C$ which are not field operations. We define the absolute value of $z$ denoted by $|z|$ and the conjugate of $z$ denoted by $z^\ast$.

Contents (PDF format)

- [1]
Grzegorz Bancerek.
The ordinal numbers.
*Journal of Formalized Mathematics*, 1, 1989. - [2]
Czeslaw Bylinski.
Functions and their basic properties.
*Journal of Formalized Mathematics*, 1, 1989. - [3]
Czeslaw Bylinski.
Functions from a set to a set.
*Journal of Formalized Mathematics*, 1, 1989. - [4]
Czeslaw Bylinski.
The modification of a function by a function and the iteration of the composition of a function.
*Journal of Formalized Mathematics*, 2, 1990. - [5]
Library Committee.
Introduction to arithmetic.
*Journal of Formalized Mathematics*, Addenda, 2003. - [6]
Krzysztof Hryniewiecki.
Basic properties of real numbers.
*Journal of Formalized Mathematics*, 1, 1989. - [7]
Jan Popiolek.
Some properties of functions modul and signum.
*Journal of Formalized Mathematics*, 1, 1989. - [8]
Andrzej Trybulec.
Tarski Grothendieck set theory.
*Journal of Formalized Mathematics*, Axiomatics, 1989. - [9]
Andrzej Trybulec.
Subsets of real numbers.
*Journal of Formalized Mathematics*, Addenda, 2003. - [10]
Andrzej Trybulec and Czeslaw Bylinski.
Some properties of real numbers operations: min, max, square, and square root.
*Journal of Formalized Mathematics*, 1, 1989. - [11]
Zinaida Trybulec.
Properties of subsets.
*Journal of Formalized Mathematics*, 1, 1989. - [12]
Edmund Woronowicz.
Relations and their basic properties.
*Journal of Formalized Mathematics*, 1, 1989.

[ Download a postscript version, MML identifier index, Mizar home page]