environ
vocabularies HIDDEN, NUMBERS, XREAL_0, ORDINAL1, SUBSET_1, INT_1, TARSKI, ARYTM_3, XBOOLE_0, CARD_1, ARYTM_0, RELAT_1, REAL_1, ARYTM_2, ORDINAL2, ARYTM_1, ZFMISC_1, XXREAL_0, NAT_1, RAT_1, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, ORDINAL3, ARYTM_3, ARYTM_2, NUMBERS, ARYTM_0, XCMPLX_0, XREAL_0, REAL_1, NAT_1, INT_1, ARYTM_1, XXREAL_0;
definitions XREAL_0, TARSKI, XBOOLE_0;
theorems INT_1, NAT_1, TARSKI, XREAL_0, XCMPLX_0, XCMPLX_1, XBOOLE_0, NUMBERS, ARYTM_3, ARYTM_0, ARYTM_2, ZFMISC_1, ARYTM_1, XREAL_1, XXREAL_0, XBOOLE_1, ORDINAL1, XTUPLE_0;
schemes NAT_1;
registrations ORDINAL1, ARYTM_3, ARYTM_2, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, ORDINAL3;
constructors HIDDEN, FUNCT_4, ARYTM_1, ARYTM_0, XXREAL_0, REAL_1, NAT_1, INT_1, ORDINAL3;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities XBOOLE_0, XCMPLX_0, ARYTM_3;
expansions TARSKI;
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:
for i1, j1 being Nat holds quotient (i1,j1) = i1 / j1
reconsider 09 = 0 as Element of REAL+ by ARYTM_2:2;
Lm3:
for a being Real
for x9 being Element of REAL+ st x9 = a holds
09 - x9 = - a
Lm4:
for x being object st x in RAT holds
ex m, n being Integer st x = m / n
Lm5:
for x being object
for w being Nat
for m being Integer st x = m / w holds
x in RAT
Lm6:
for x being object
for m, n being Integer st x = m / n holds
x in RAT
theorem
for
a,
b being
Real st
a < b holds
ex
p being
Rational st
(
a < p &
p < b )
Lm7:
1 " = 1
;
:: or of natural denominator and numerator, etc., are all rational numbers.