environ
vocabularies HIDDEN, ORDINAL1, TARSKI, SUBSET_1, ARYTM_3, XBOOLE_0, CARD_1, ARYTM_2, ZFMISC_1, FUNCT_2, FUNCT_1, FUNCOP_1, RELAT_1, ORDINAL2, ORDINAL3, FINSET_1, NUMBERS;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCT_4, ORDINAL1, ORDINAL2, ORDINAL3, FINSET_1, ARYTM_3, ARYTM_2;
definitions ARYTM_3, XBOOLE_0;
theorems XBOOLE_1, ARYTM_2, ZFMISC_1, ARYTM_3, XBOOLE_0, TARSKI, ORDINAL2, ORDINAL3, ENUMSET1, ORDINAL1, FUNCT_2, FUNCT_4, RELAT_1, FINSET_1, XTUPLE_0;
schemes DOMAIN_1;
registrations XBOOLE_0, ORDINAL1, FUNCT_2, ARYTM_3, ARYTM_2, RELAT_1, ORDINAL2, ORDINAL3, CARD_1;
constructors HIDDEN, FUNCT_4, ORDINAL3, ARYTM_2, FINSET_1, XTUPLE_0;
requirements HIDDEN, BOOLE, SUBSET, NUMERALS;
equalities TARSKI, ARYTM_3, ORDINAL1;
expansions TARSKI, ARYTM_3, XBOOLE_0;
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;
Lm2:
1 = succ 0
;
Lm3:
REAL+ c= REAL
Lm4:
RAT+ c= RAT
Lm5:
NAT c= INT
Lm6:
for x, y, z being set st [x,y] = {z} holds
( z = {x} & x = y )
Lm7:
for a, b being Element of REAL holds not (0,one) --> (a,b) in REAL
Lm8:
RAT c= REAL
Lm9:
for i, j being ordinal Element of RAT+ st i in j holds
i < j
Lm10:
for i, j being ordinal Element of RAT+ st i c= j holds
i <=' j
Lm11: 2 =
succ 1
.=
(succ 0) \/ {1}
.=
(0 \/ {0}) \/ {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
reconsider a9 = 1 as Element of RAT+ by Lm1;
reconsider two = 2 as ordinal Element of RAT+ by Lm1;
Lm13:
one + one = two
Lm14:
for i being Element of RAT+ holds i + i = two *' i
Lm15:
INT c= RAT