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

begin

Lm1: omega c= ( { [c,d] where c, d is Element of omega : ( c,d are_relative_prime & 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

proof end;

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

proof end;

Lm5: NAT c= INT

proof end;

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} & 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 NAT ;
coherence
0 is Element of NAT by ORDINAL1:def 12;

end;

theorem Th1: :: NUMBERS:1

REAL c< COMPLEX

proof end;

Lm8: RAT c= REAL

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 = succ 1
.= (succ 0) \/ {1} by ORDINAL1:def 1
.= (0 \/ {0}) \/ {1} by ORDINAL1:def 1
.= {0,1} by ENUMSET1:41 ;

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

proof end;

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

proof end;

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

proof end;

theorem Th2: :: NUMBERS:2

RAT c< REAL

proof end;

theorem Th3: :: NUMBERS:3

RAT c< COMPLEX by Th1, Th2, XBOOLE_1:56;

Lm15: INT c= RAT

proof end;

theorem Th4: :: NUMBERS:4

INT c< RAT

proof end;

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

proof end;

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

proof end;

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:13;
cluster RAT -> infinite ;
coherence
not RAT is finite by Th18, FINSET_1:13;
cluster REAL -> infinite ;
coherence
not REAL is finite by Th19, FINSET_1:13;
cluster COMPLEX -> infinite ;
coherence
not COMPLEX is finite by Th20, FINSET_1:13;

end;