environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, INT_1, NAT_1, FINSEQ_1, NEWTON, ARYTM_3, ARYTM_1, RELAT_1, CARD_1, FUNCT_1, CARD_3, FUNCOP_1, ORDINAL4, XBOOLE_0, TARSKI, XXREAL_0, FINSEQ_5, SQUARE_1, INT_2, COMPLEX1, ABIAN, FINSEQ_2, FUNCT_7, PARTFUN1, FINSET_1, RFINSEQ, CALCUL_2, REAL_1, ZFMISC_1, INT_5, ORDINAL1;
notations HIDDEN, XREAL_0, GROUP_4, INT_1, RVSUM_1, FINSET_1, ORDINAL1, CARD_1, NAT_D, INT_2, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, NAT_3, ABIAN, GR_CY_1, FINSEQ_5, FINSEQ_2, EULER_2, NEWTON, FINSEQ_7, REAL_1, PEPIN, TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, NUMBERS, XXREAL_0, NAT_1, DOMAIN_1, FINSEQ_1, RFINSEQ, FUNCOP_1, CALCUL_2, ZFMISC_1, CARD_3, WSIERP_1, BINOP_1, RECDEF_1;
definitions FUNCT_1, TARSKI;
theorems FINSEQ_1, FINSEQ_7, RELAT_1, FINSEQ_3, FINSEQ_2, ABSVALUE, FINSEQ_5, EULER_2, SEQ_2, FINSEQ_4, FUNCT_2, XBOOLE_0, NAT_3, NEWTON, INT_2, NAT_2, WSIERP_1, CARD_1, PEPIN, NAT_1, XCMPLX_1, XREAL_1, HEYTING3, ORDINAL1, EULER_1, XBOOLE_1, TARSKI, RVSUM_1, NUMBERS, INT_1, FUNCT_1, FUNCOP_1, XXREAL_0, NAT_D, HILBERT3, SERIES_2, GRAPH_5, HILBERT2, RFINSEQ, ZFMISC_1, CARD_2, XREAL_0, FINSEQ_6, CALCUL_2, NAT_4, PROB_3, TOPREAL7, CARD_3, REAL_3, PRE_FF, INT_4, VALUED_1, PRE_POLY, XTUPLE_0;
schemes NAT_1, FUNCT_2, RECDEF_1, FINSEQ_2, FUNCT_7, FINSEQ_1;
registrations XXREAL_0, MEMBERED, RELAT_1, FINSEQ_1, ORDINAL1, WSIERP_1, NUMBERS, XBOOLE_0, XREAL_0, NAT_1, INT_1, FINSET_1, NAT_3, RVSUM_1, FUNCT_1, CARD_1, NEWTON, SUBSET_1, VALUED_0, VALUED_1, FINSEQ_2, PRE_POLY, RELSET_1;
constructors HIDDEN, ABIAN, WSIERP_1, PEPIN, NAT_3, NAT_D, REALSET1, GR_CY_1, FINSEQ_5, EULER_2, RFINSEQ, GROUP_4, FINSEQ_7, REAL_1, WELLORD2, CALCUL_2, PROB_3, RECDEF_1, BINOP_1, BINOP_2, CLASSES1, NUMBERS;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities INT_1, XCMPLX_0, SQUARE_1, FINSEQ_2, CALCUL_2, CARD_3;
expansions INT_1, FUNCT_1, TARSKI;
Lm1:
for x, y being Integer holds
( ( x divides y implies y mod x = 0 ) & ( x <> 0 & y mod x = 0 implies x divides y ) )
Lm2:
for i being Integer
for p being Prime holds
( i,p are_coprime or p divides i )
Lm3:
for a being Integer
for p being Prime st a gcd p = 1 holds
not p divides a
Lm4:
for fp being FinSequence of NAT holds Sum fp is Element of NAT
;