Journal of Formalized Mathematics
University of Bialystok
Copyright (c) 2003 Association of Mizar Users

### Subsets of Complex Numbers

by
Andrzej Trybulec

MML identifier: NUMBERS
[ Mizar article, MML identifier index ]

```environ

vocabulary COMPLEX1, FUNCT_2, FUNCT_1, FUNCOP_1, ARYTM_2, BOOLE, ARYTM_3,
ORDINAL2, ARYTM, ORDINAL1, RELAT_1, RAT_1, INT_1, ORDINAL3;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2,
FUNCT_4, ORDINAL1, ORDINAL2, ORDINAL3, ARYTM_3, ARYTM_2;
constructors ARYTM_1, FRAENKEL, FUNCT_4, ORDINAL3;
clusters XBOOLE_0, ARYTM_2, SUBSET_1, ORDINAL2, ARYTM_3, FRAENKEL, FUNCT_2,
FUNCT_4, ORDINAL1, ZFMISC_1;
requirements BOOLE, SUBSET, NUMERALS;

begin

definition
func REAL equals
:: NUMBERS:def 1
REAL+ \/ [:{0},REAL+:] \ {[0,0]};
redefine func omega; synonym NAT;
end;

definition
cluster REAL -> non empty;
end;

definition
func COMPLEX equals
:: NUMBERS:def 2
Funcs({0,one},REAL)
\ { x where x is Element of Funcs({0,one},REAL): x.one = 0}
\/ REAL;
func RAT equals
:: NUMBERS:def 3
RAT+ \/ [:{0},RAT+:] \ {[0,0]};
func INT equals
:: NUMBERS:def 4
NAT \/ [:{0},NAT:] \ {[0,0]};
redefine func NAT -> Subset of REAL;
end;

definition
cluster COMPLEX -> non empty;
cluster RAT -> non empty;
cluster INT -> non empty;
end;

reserve i,j,k for Element of NAT;
reserve a,b for Element of REAL;

theorem :: NUMBERS:1
REAL c< COMPLEX;

reserve r,s,t for Element of RAT+;
reserve i,j,k for Element of omega;

theorem :: NUMBERS:2
RAT c< REAL;

theorem :: NUMBERS:3
RAT c< COMPLEX;

theorem :: NUMBERS:4
INT c< RAT;

theorem :: NUMBERS:5
INT c< REAL;

theorem :: NUMBERS:6
INT c< COMPLEX;

theorem :: NUMBERS:7
NAT c< INT;

theorem :: NUMBERS:8
NAT c< RAT;

theorem :: NUMBERS:9
NAT c< REAL;

theorem :: NUMBERS:10
NAT c< COMPLEX;

begin :: to be canceled

theorem :: NUMBERS:11
REAL c= COMPLEX;

theorem :: NUMBERS:12
RAT c= REAL;

theorem :: NUMBERS:13
RAT c= COMPLEX;

theorem :: NUMBERS:14
INT c= RAT;

theorem :: NUMBERS:15
INT c= REAL;

theorem :: NUMBERS:16
INT c= COMPLEX;

theorem :: NUMBERS:17
NAT c= INT;

theorem :: NUMBERS:18
NAT c= RAT;

theorem :: NUMBERS:19
NAT c= REAL;

theorem :: NUMBERS:20
NAT c= COMPLEX;

theorem :: NUMBERS:21
REAL <> COMPLEX;

theorem :: NUMBERS:22
RAT <> REAL;

theorem :: NUMBERS:23
RAT <> COMPLEX;

theorem :: NUMBERS:24
INT <> RAT;

theorem :: NUMBERS:25
INT <> REAL;

theorem :: NUMBERS:26
INT <> COMPLEX;

theorem :: NUMBERS:27
NAT <> INT;

theorem :: NUMBERS:28
NAT <> RAT;

theorem :: NUMBERS:29
NAT <> REAL;

theorem :: NUMBERS:30
NAT <> COMPLEX;
```