:: Subsets of Complex Numbers
:: by Andrzej Trybulec
::
:: Received November 7, 2003
:: Copyright (c) 2003-2012 Association of Mizar Users


begin

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

notation
synonym  NAT for  omega ;
synonym  0 for  {} ;
end;

Lm2:  1 = succ 0
;

definition
func REAL  ->  set  equals :: NUMBERS:def 1
(REAL+ \/ [:{0},REAL+:]) \ {[0,0]};
coherence
 (REAL+ \/ [:{0},REAL+:]) \ {[0,0]} is set ;
end;

:: deftheorem  defines REAL NUMBERS:def_1_:_
 REAL = (REAL+ \/ [:{0},REAL+:]) \ {[0,0]};

Lm3:  REAL+ c= REAL
proofend;

registration
cluster REAL  ->  non empty ;
coherence
 not REAL is empty by Lm3, XBOOLE_1:3;
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
(RAT+ \/ [:{0},RAT+:]) \ {[0,0]};
coherence
 (RAT+ \/ [:{0},RAT+:]) \ {[0,0]} is set ;
func INT  ->  set  equals :: NUMBERS:def 4
(NAT \/ [:{0},NAT:]) \ {[0,0]};
coherence
 (NAT \/ [:{0},NAT:]) \ {[0,0]} is set ;
:: original:NAT
redefine func NAT  ->  Subset of REAL;
coherence
 NAT is Subset of REAL by Lm3, ARYTM_2:2, XBOOLE_1:1;
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 = (RAT+ \/ [:{0},RAT+:]) \ {[0,0]};

:: deftheorem  defines INT NUMBERS:def_4_:_
 INT = (NAT \/ [:{0},NAT:]) \ {[0,0]};

Lm4:  RAT+ c= RAT
proofend;

Lm5:  NAT c= INT
proofend;

registration
cluster COMPLEX  ->  non empty ;
coherence
 not COMPLEX is empty ;
cluster RAT  ->  non empty ;
coherence
 not RAT is empty by Lm4, XBOOLE_1:3;
cluster INT  ->  non empty ;
coherence
 not INT is empty by Lm5, XBOOLE_1:3;
end;

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

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

definition
:: original:0
redefine func 0  ->  Element of NAT ;
coherence
 0 is Element of NAT by ORDINAL1:def_11;
end;

theorem Th1: :: NUMBERS:1
REAL c< COMPLEX
proofend;

Lm8:  RAT c= REAL
proofend;

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

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

Lm11: 2 = succ 1
.= (succ 0) \/ {1} by ORDINAL1:def_1
.= (0 \/ {0}) \/ {1} by ORDINAL1:def_1
.= {0,1} by ENUMSET1:1 ;

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

 1 in omega
;

then reconsider a9 = 1 as Element of RAT+ by Lm1;

 2 in omega
;

then reconsider two = 2 as ordinal Element of RAT+ by Lm1;

Lm13:  one + one = two
proofend;

Lm14:  for i being Element of RAT+ holds i + i = two *' i
proofend;

theorem Th2: :: NUMBERS:2
RAT c< REAL
proofend;

theorem Th3: :: NUMBERS:3
RAT c< COMPLEX by Th1, Th2, XBOOLE_1:56;

Lm15:  INT c= RAT
proofend;

theorem Th4: :: NUMBERS:4
INT c< RAT
proofend;

theorem Th5: :: NUMBERS:5
INT c< REAL by Th2, Th4, XBOOLE_1:56;

theorem Th6: :: NUMBERS:6
INT c< COMPLEX by Th1, Th5, XBOOLE_1:56;

theorem Th7: :: NUMBERS:7
NAT c< INT
proofend;

theorem Th8: :: NUMBERS:8
NAT c< RAT by Th4, Th7, XBOOLE_1:56;

theorem Th9: :: NUMBERS:9
NAT c< REAL by Th2, Th8, XBOOLE_1:56;

theorem Th10: :: NUMBERS:10
NAT c< COMPLEX by Th1, Th9, XBOOLE_1:56;

begin

theorem :: NUMBERS:11
REAL c= COMPLEX by Th1, XBOOLE_0:def_8;

theorem :: NUMBERS:12
RAT c= REAL by Th2, XBOOLE_0:def_8;

theorem :: NUMBERS:13
RAT c= COMPLEX by Th3, XBOOLE_0:def_8;

theorem :: NUMBERS:14
INT c= RAT by Th4, XBOOLE_0:def_8;

theorem :: NUMBERS:15
INT c= REAL by Th5, XBOOLE_0:def_8;

theorem :: NUMBERS:16
INT c= COMPLEX by Th6, XBOOLE_0:def_8;

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

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

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

theorem Th20: :: NUMBERS:20
NAT c= COMPLEX by Th10, XBOOLE_0:def_8;

theorem :: NUMBERS:21
REAL <> COMPLEX by Th1;

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

theorem :: NUMBERS:23
RAT <> COMPLEX by Th1, Th2;

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

theorem :: NUMBERS:25
INT <> REAL by Th2, Th4;

theorem :: NUMBERS:26
INT <> COMPLEX by Th1, Th2, Th4, XBOOLE_1:56;

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

theorem :: NUMBERS:28
NAT <> RAT by Th4, Th7;

theorem :: NUMBERS:29
NAT <> REAL by Th2, Th4, Th7, XBOOLE_1:56;

theorem :: NUMBERS:30
NAT <> COMPLEX by Th1, Th2, Th8, XBOOLE_1:56;

definition
func ExtREAL  ->  set  equals :: NUMBERS:def 5
REAL \/ {REAL,[0,REAL]};
coherence
 REAL \/ {REAL,[0,REAL]} is set ;
end;

:: deftheorem  defines ExtREAL NUMBERS:def_5_:_
 ExtREAL = REAL \/ {REAL,[0,REAL]};

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

theorem Th31: :: NUMBERS:31
REAL c= ExtREAL by XBOOLE_1:7;

theorem Th32: :: NUMBERS:32
REAL <> ExtREAL
proofend;

theorem :: NUMBERS:33
REAL c< ExtREAL by Th31, Th32, XBOOLE_0:def_8;

registration
cluster INT  ->  infinite ;
coherence
 not INT is finite by Lm5, FINSET_1:1;
cluster RAT  ->  infinite ;
coherence
 not RAT is finite by Th18, FINSET_1:1;
cluster REAL  ->  infinite ;
coherence
 not REAL is finite by Th19, FINSET_1:1;
cluster COMPLEX  ->  infinite ;
coherence
 not COMPLEX is finite by Th20, FINSET_1:1;
end;