:: Subsets of Complex Numbers
:: by Andrzej Trybulec
::
:: Copyright (c) 2003-2021 Association of Mizar Users

Lm1: omega c= ( { [c,d] where c, d is Element of omega : ( c,d are_coprime & d <> {} ) } \ { [k,1] where k is Element of omega : verum } ) \/ omega
by XBOOLE_1:7;

notation
synonym NAT for omega ;
end;

Lm2:
;

definition
func REAL -> set equals :: NUMBERS:def 1
() \ ;
coherence
() \ is set
;
end;

:: deftheorem defines REAL NUMBERS:def 1 :

Lm3:
proof end;

registration
cluster REAL -> non empty ;
coherence
not REAL is empty
by ;
end;

definition
func COMPLEX -> set equals :: NUMBERS:def 2
((Funcs ({0,1},REAL)) \ { x where x is Element of Funcs ({0,1},REAL) : x . 1 = 0 } ) \/ REAL;
coherence
((Funcs ({0,1},REAL)) \ { x where x is Element of Funcs ({0,1},REAL) : x . 1 = 0 } ) \/ REAL is set
;
func RAT -> set equals :: NUMBERS:def 3
() \ ;
coherence
() \ is set
;
func INT -> set equals :: NUMBERS:def 4
() \ ;
coherence
() \ is set
;
end;

:: deftheorem defines COMPLEX NUMBERS:def 2 :
COMPLEX = ((Funcs ({0,1},REAL)) \ { x where x is Element of Funcs ({0,1},REAL) : x . 1 = 0 } ) \/ REAL;

:: deftheorem defines RAT NUMBERS:def 3 :
RAT = () \ ;

:: deftheorem defines INT NUMBERS:def 4 :
INT = () \ ;

Lm4:
proof end;

Lm5:
proof end;

registration
cluster COMPLEX -> non empty ;
coherence
not COMPLEX is empty
;
cluster RAT -> non empty ;
coherence
not RAT is empty
by ;
cluster INT -> non empty ;
coherence
not INT is empty
by ;
end;

Lm6: for x, y, z being set st [x,y] = {z} holds
( z = {x} & x = y )

proof end;

Lm7: for a, b being Element of REAL holds not (0,one) --> (a,b) in REAL
proof end;

definition
:: original: 0
redefine func 0 -> Element of omega ;
coherence
0 is Element of omega
by ORDINAL1:def 11;
end;

theorem Th1: :: NUMBERS:1
proof end;

Lm8:
proof end;

Lm9: for i, j being ordinal Element of RAT+ st i in j holds
i < j

proof end;

Lm10: for i, j being ordinal Element of RAT+ st i c= j holds
i <=' j

proof end;

Lm11: 2 = {0,1}
proof end;

Lm12: for i, k being natural Ordinal st i *^ i = 2 *^ k holds
ex k being natural Ordinal st i = 2 *^ k

proof end;

Lm13:
proof end;

Lm14: for two, i being Element of RAT+ st two = 2 holds
i + i = two *' i

proof end;

theorem Th2: :: NUMBERS:2
proof end;

theorem Th3: :: NUMBERS:3

Lm15:
proof end;

theorem Th4: :: NUMBERS:4
proof end;

theorem Th5: :: NUMBERS:5
INT c< REAL by ;

theorem Th6: :: NUMBERS:6

theorem Th7: :: NUMBERS:7
proof end;

theorem Th8: :: NUMBERS:8
NAT c< RAT by ;

theorem Th9: :: NUMBERS:9
NAT c< REAL by ;

theorem Th10: :: NUMBERS:10

theorem :: NUMBERS:11

theorem :: NUMBERS:12
RAT c= REAL by Th2;

theorem :: NUMBERS:13

theorem :: NUMBERS:14
INT c= RAT by Th4;

theorem :: NUMBERS:15
INT c= REAL by Th5;

theorem :: NUMBERS:16

theorem :: NUMBERS:17
NAT c= INT by Lm5;

theorem Th18: :: NUMBERS:18
NAT c= RAT by Th8;

theorem Th19: :: NUMBERS:19
NAT c= REAL by Th9;

theorem Th20: :: NUMBERS:20

theorem :: NUMBERS:21

theorem :: NUMBERS:22
RAT <> REAL by Th2;

theorem :: NUMBERS:23
RAT <> COMPLEX by ;

theorem :: NUMBERS:24
INT <> RAT by Th4;

theorem :: NUMBERS:25
INT <> REAL by ;

theorem :: NUMBERS:26
INT <> COMPLEX by ;

theorem :: NUMBERS:27
NAT <> INT by Th7;

theorem :: NUMBERS:28
NAT <> RAT by ;

theorem :: NUMBERS:29
NAT <> REAL by ;

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

definition
coherence ;
end;

:: deftheorem defines ExtREAL NUMBERS:def 5 :

registration
cluster ExtREAL -> non empty ;
coherence
not ExtREAL is empty
;
end;

theorem Th31: :: NUMBERS:31

theorem Th32: :: NUMBERS:32
proof end;

theorem :: NUMBERS:33

registration
coherence
not INT is finite
by ;
coherence
not RAT is finite
by ;
coherence
not REAL is finite
by ;
coherence
not COMPLEX is finite
by ;
end;