:: NUMBERS semantic presentation

E1: one = succ 0 by ORDINAL2:def 4
.= 1 ;

notation
synonym NAT for omega ;
end;

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

:: deftheorem Def1 defines REAL NUMBERS:def 1 :
REAL = (REAL+ \/ [:{0},REAL+ :]) \ {[0,0]};

Lemma2: REAL+ c= REAL
proof end;

registration
cluster REAL -> non empty ;
coherence
not REAL is empty by Lemma2, XBOOLE_1:3;
end;

definition
func COMPLEX -> set equals :: NUMBERS:def 2
((Funcs {0,one },REAL ) \ { b1 where B is Element of Funcs {0,one },REAL : b1 . one = 0 } ) \/ REAL ;
coherence
((Funcs {0,one },REAL ) \ { b1 where B is Element of Funcs {0,one },REAL : b1 . one = 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 ;
redefine func NAT as NAT -> Subset of REAL ;
coherence
NAT is Subset of REAL by Lemma2, ARYTM_2:2, XBOOLE_1:1;
end;

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

:: deftheorem Def3 defines RAT NUMBERS:def 3 :
RAT = (RAT+ \/ [:{0},RAT+ :]) \ {[0,0]};

:: deftheorem Def4 defines INT NUMBERS:def 4 :
INT = (NAT \/ [:{0},NAT :]) \ {[0,0]};

Lemma3: RAT+ c= RAT
proof end;

Lemma4: 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 Lemma3, XBOOLE_1:3;
cluster INT -> non empty ;
coherence
not INT is empty by Lemma4, XBOOLE_1:3;
end;

Lemma5: for b1, b2, b3 being set st [b1,b2] = {b3} holds
( b3 = {b1} & b1 = b2 )
proof end;

Lemma6: for b1, b2 being Element of REAL holds not 0,one --> b1,b2 in REAL
proof end;

theorem Th1: :: NUMBERS:1
REAL c< COMPLEX
proof end;

Lemma8: RAT c= REAL
proof end;

Lemma9: for b1, b2 being ordinal Element of RAT+ st b1 in b2 holds
b1 < b2
proof end;

Lemma10: for b1, b2 being ordinal Element of RAT+ st b1 c= b2 holds
b1 <=' b2
proof end;

E11: 2 = succ 1
.= (succ 0) \/ {1} by ORDINAL1:def 1
.= (0 \/ {0}) \/ {1} by ORDINAL1:def 1
.= {0,1} by ENUMSET1:41 ;

Lemma12: for b1, b2 being natural Ordinal st b1 *^ b1 = 2 *^ b2 holds
ex b3 being natural Ordinal st b1 = 2 *^ b3
proof end;

1 in omega
;

then reconsider c1 = 1 as Element of RAT+ by ARYTM_3:34;

2 in omega
;

then reconsider c2 = 2 as ordinal Element of RAT+ by ARYTM_3:34;

Lemma13: one + one = c2
proof end;

Lemma14: for b1 being Element of RAT+ holds b1 + b1 = c2 *' b1
proof end;

theorem Th2: :: NUMBERS:2
RAT c< REAL
proof end;

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

Lemma17: 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;

theorem Th11: :: NUMBERS:11
REAL c= COMPLEX by Th1, XBOOLE_0:def 8;

theorem Th12: :: NUMBERS:12
RAT c= REAL by Th2, XBOOLE_0:def 8;

theorem Th13: :: NUMBERS:13
RAT c= COMPLEX by Th3, XBOOLE_0:def 8;

theorem Th14: :: NUMBERS:14
INT c= RAT by Th4, XBOOLE_0:def 8;

theorem Th15: :: NUMBERS:15
INT c= REAL by Th5, XBOOLE_0:def 8;

theorem Th16: :: NUMBERS:16
INT c= COMPLEX by Th6, XBOOLE_0:def 8;

theorem Th17: :: NUMBERS:17
NAT c= INT by Th7, XBOOLE_0:def 8;

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 Th21: :: NUMBERS:21
REAL <> COMPLEX by Th1;

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

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

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

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

theorem Th26: :: NUMBERS:26
INT <> COMPLEX by Th1, Th5;

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

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

theorem Th29: :: NUMBERS:29
NAT <> REAL by Th2, Th8;

theorem Th30: :: NUMBERS:30
NAT <> COMPLEX by Th1, Th9;