environ
vocabularies HIDDEN, NUMBERS, BINOP_2, SUBSET_1, FUNCT_1, BINOP_1, RELAT_1, ARYTM_1, ALGSTR_0, FUNCT_7, CARD_1, STRUCT_0, XBOOLE_0, INT_1, ARYTM_3, SUPINF_2, VECTSP_1, MESFUNC1, GROUP_1, RLVECT_1, LATTICES, VECTSP_2, COMPLEX1, XXREAL_0, EUCLID, TARSKI, NAT_1, FUNCSDOM, GCD_1, INT_2, XCMPLX_0, NEWTON, INT_3, MEMBERED, FINSET_1, ORDINAL1;
notations HIDDEN, TARSKI, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, COMPLEX1, XTUPLE_0, RELAT_1, FUNCT_1, FUNCT_2, BINOP_1, EUCLID, XCMPLX_0, XXREAL_0, BINOP_2, GR_CY_1, INT_1, FUNCT_7, NEWTON, INT_2, NAT_D, MEMBERED, STRUCT_0, ALGSTR_0, RLVECT_1, GCD_1, GROUP_1, VECTSP_1, VECTSP_2;
definitions RLVECT_1, STRUCT_0, GROUP_1, VECTSP_1, VECTSP_2, ALGSTR_0;
theorems TARSKI, BINOP_1, FUNCT_1, FUNCT_2, VECTSP_1, INT_1, RELAT_1, GCD_1, RLVECT_1, EUCLID, ABSVALUE, GR_CY_1, NAT_1, INT_2, RELSET_1, ORDINAL1, XCMPLX_1, NUMBERS, BINOP_2, GROUP_1, XREAL_1, COMPLEX1, XXREAL_0, NAT_D, NEWTON, CARD_1, XTUPLE_0, SUBSET_1;
schemes NAT_1, BINOP_1, LMOD_7, BINOP_2;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, NEWTON, STRUCT_0, VECTSP_1, GR_CY_1, GCD_1, VALUED_0, MEMBERED, CARD_1;
constructors HIDDEN, REAL_1, NAT_D, BINOP_2, NEWTON, FUNCT_7, GR_CY_1, EUCLID, GCD_1, RELSET_1, XTUPLE_0, BINOP_1;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities STRUCT_0, CARD_1, ALGSTR_0, ORDINAL1;
expansions STRUCT_0, GROUP_1, VECTSP_1;
set M = INT.Ring ;
Lm1:
for a being Integer holds
( a = 0 or absreal . a >= 1 )
Lm2:
for a, b being Element of INT.Ring st b <> 0. INT.Ring holds
for b9 being Integer st b9 = b & 0 <= b9 holds
ex q, r being Element of INT.Ring st
( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) )
Lm4:
for F being non empty almost_left_invertible associative commutative right_zeroed well-unital doubleLoopStr
for f being Function of F,NAT
for a, b being Element of F st b <> 0. F holds
ex q, r being Element of F st
( a = (q * b) + r & ( r = 0. F or f . r < f . b ) )
Lm5:
for a, b being Nat st b <> 0 holds
ex k being Element of NAT st
( k * b <= a & a < (k + 1) * b )
Lm7:
for n being Nat st 1 < n holds
1. (INT.Ring n) = 1
by NAT_1:44, SUBSET_1:def 8;