:: NUMBERS semantic presentation

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

end;

:: deftheorem defines REAL NUMBERS:def 1 :

Lm2: REAL+ c= REAL

proof end;

registration

cluster REAL -> non empty ;
coherence by Lm2, XBOOLE_1:3;

end;

definition

func COMPLEX -> set equals :: NUMBERS:def 2
((Funcs {0,one },REAL ) \ { x where x is Element of Funcs {0,one },REAL : x . one = 0 } ) \/ REAL ;
coherence ;
func RAT -> set equals :: NUMBERS:def 3
(RAT+ \/ [:{0},RAT+ :]) \ {[0,0]};
coherence ;
func INT -> set equals :: NUMBERS:def 4
(NAT \/ [:{0},NAT :]) \ {[0,0]};
coherence ;
:: original: NAT
redefine func NAT -> Subset of REAL ;
coherence by Lm2, ARYTM_2:2, XBOOLE_1:1;

end;

:: deftheorem defines COMPLEX NUMBERS:def 2 :

:: deftheorem defines RAT NUMBERS:def 3 :

:: deftheorem defines INT NUMBERS:def 4 :

Lm3: RAT+ c= RAT

proof end;

Lm4: NAT c= INT

proof end;

registration

cluster COMPLEX -> non empty ;
coherence ;
cluster RAT -> non empty ;
coherence by Lm3, XBOOLE_1:3;
cluster INT -> non empty ;
coherence by Lm4, XBOOLE_1:3;

end;

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

proof end;

Lm6: for a, b being Element of REAL holds not 0,one --> a,b in REAL

proof end;

theorem Th1: :: NUMBERS:1

REAL c< COMPLEX

proof end;

Lm7: RAT c= REAL

proof end;

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

proof end;

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

proof end;

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

Lm11: 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 1' = 1 as Element of RAT+ by ARYTM_3:34;

2 in omega
;

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

Lm12: one + one = two

proof end;