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;
Lm2:
for i1, j1 being Element of NAT holds quotient i1,j1 = i1 / j1
0 in omega
;
then reconsider 0' = 0 as Element of REAL+ by ARYTM_2:2;
Lm3:
for a being real number
for x' being Element of REAL+ st x' = a holds
0' - x' = - a
Lm4:
for x being set st x in RAT holds
ex m, n being Integer st x = m / n
Lm5:
for x being set
for l being Element of NAT
for m being Integer st x = m / l holds
x in RAT
Lm6:
for x being set
for m, n being Integer st x = m / n holds
x in RAT
:: deftheorem Def1 defines RAT RAT_1:def 1 :
for
b1 being
set holds
(
b1 = RAT iff for
x being
set holds
(
x in b1 iff ex
m,
n being
Integer st
x = m / n ) );
:: deftheorem Def2 defines rational RAT_1:def 2 :
theorem Th1:
theorem
canceled;
theorem Th3:
theorem
canceled;
theorem
canceled;
theorem Th6:
theorem Th7:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th16:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th21:
theorem
theorem
canceled;
theorem Th24:
theorem Th25:
:: deftheorem Def3 defines denominator RAT_1:def 3 :
:: deftheorem defines numerator RAT_1:def 4 :
theorem
canceled;
theorem Th27:
theorem
canceled;
theorem Th29:
theorem Th30:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th34:
theorem
canceled;
theorem Th36:
theorem Th37:
theorem
theorem
canceled;
theorem Th40:
theorem Th41:
theorem
theorem
canceled;
theorem
theorem
Lm7:
1 " = 1
;
theorem
theorem Th47:
theorem Th48:
theorem
theorem Th50:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th60:
theorem
theorem Th62:
theorem Th63:
theorem Th64:
theorem Th65:
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th72:
theorem
theorem
canceled;
theorem
canceled;
theorem
theorem Th77:
theorem
canceled;
theorem
canceled;
theorem Th80:
theorem
theorem
canceled;
theorem
canceled;
theorem
theorem
canceled;
theorem
theorem Th87:
theorem Th88:
theorem