environ
vocabularies HIDDEN, ORDINAL2, FINSEQ_1, ARYTM_3, ARYTM_1, RELAT_1, FUNCT_1, FINSEQ_2, INT_1, SQUARE_1, SEQ_1, REALSET1, SERIES_1, SEQ_2, NAT_LAT, FINSET_1, CARD_1, MOEBIUS1, LATTICES, PRE_POLY, XXREAL_2, MSAFREE, MOEBIUS2, NEWTON, XXREAL_0, XBOOLE_0, INT_2, TARSKI, PARTFUN3, NAT_1, BINOP_1, EQREL_1, PBOOLE, NAT_3, CARD_3, FUNCT_2, VALUED_0, UPROOTS, QUOFIELD, MEMBERED, INT_7, STRUCT_0, XCMPLX_0, COMPLEX1, ORDINAL1, SUBSET_1, ZFMISC_1, NUMBERS, REAL_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, CARD_1, XXREAL_0, XCMPLX_0, MEMBERED, ENUMSET1, ZFMISC_1, FINSET_1, MCART_1, SQUARE_1, COMPLEX1, ABSVALUE, INT_1, INT_2, NAT_1, XREAL_0, REAL_1, RELAT_1, FUNCT_1, FUNCT_2, VALUED_0, VALUED_1, FINSEQ_1, REALSET1, FUNCOP_1, CARD_2, PARTFUN3, PRE_POLY, PBOOLE, NAT_D, SEQ_1, SEQ_2, FINSEQ_2, FINSEQ_4, RVSUM_1, STRUCT_0, BINOP_1, LATTICES, NAT_LAT, BINARITH, NEWTON, SERIES_1, SEQM_3, COMSEQ_2, INT_7, WSIERP_1, NAT_3, POLYNOM1, PEPIN, MOEBIUS1, PARTFUN1;
definitions SERIES_1, FUNCOP_1, SEQM_3, CARD_1, ORDINAL1, RVSUM_1, FINSEQ_2, VALUED_0, TARSKI, PARTFUN3, XBOOLE_0, MOEBIUS1;
theorems FINSEQ_2, RVSUM_1, XCMPLX_1, ORDINAL1, SQUARE_1, NAT_1, NEWTON, XREAL_1, FINSEQ_1, RELAT_1, XREAL_0, SEQ_2, SERIES_1, FUNCT_2, SEQ_4, FUNCOP_1, SEQM_3, XXREAL_0, CARD_1, CARD_2, INT_2, PEPIN, FUNCT_1, ABSVALUE, RINFSUP1, PBOOLE, TARSKI, NAT_3, MOEBIUS1, NAT_D, INT_1, XBOOLE_1, XBOOLE_0, PARTFUN1, PARTFUN3, WSIERP_1, ENUMSET1, LATTICES, NAT_2, INT_6, INT_4, NAT_LAT, BINOP_1, VALUED_0, ZFMISC_1, PRE_POLY, INT_7, NAT_4, SUBSET_1, CARD_FIN, PREPOWER;
schemes NAT_1, SEQ_1, FUNCT_2, FUNCT_1, SUBSET_1, NUMPOLY1;
registrations RELSET_1, FINSEQ_2, INT_1, XREAL_0, NAT_1, MEMBERED, ORDINAL2, FINSEQ_1, FINSET_1, RVSUM_1, XXREAL_0, FUNCT_1, REALSET1, NAT_2, FUNCOP_1, NEWTON, SEQ_1, SEQM_3, XCMPLX_0, NUMBERS, MATRIX13, MOEBIUS1, SQUARE_1, ORDINAL1, PARTFUN3, FRAENKEL, CARD_1, STRUCT_0, PRE_POLY, NAT_3, UPROOTS, LATTICES, NAT_LAT, BINOP_1, CAYLDICK, LATTICE2, XBOOLE_0, VALUED_0, XXREAL_2, FUNCT_2, REAL_1, SUBSET_1, VALUED_1, SEQ_4;
constructors HIDDEN, PARTFUN1, WELLORD2, SQUARE_1, NAT_1, BINOP_2, FINSEQOP, SEQ_1, VALUED_1, SIN_COS, POLYNOM2, UPROOTS, INT_7, SERIES_3, COMSEQ_2, ZFMISC_1, CARD_1, CARD_2, MCART_1, MOEBIUS1, ABSVALUE, COMPLEX1, FINSEQ_4, FINSOP_1, SETWOP_2, RVSUM_1, INT_2, NEWTON, BINARITH, BAGORDER, ENUMSET1, LATTICES, NAT_LAT, STRUCT_0, BINOP_1, REALSET1, SERIES_1, ORDINAL1, XXREAL_0, POWER, SEQ_2, REAL_1, PARTFUN3, PEPIN, PBOOLE, NAT_3, POLYNOM1, POLYEQ_3, RELSET_1, WSIERP_1, RSSPACE, ASYMPT_1, FUNCOP_1, SEQM_3, FUNCT_7, NAT_D, RECDEF_1, NUMBERS, XCMPLX_0, XREAL_0, FUNCT_2;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities ORDINAL1, FUNCOP_1, FINSEQ_2, SERIES_1, SQUARE_1, BINOP_1, LATTICES, REALSET1;
expansions TARSKI, INT_2, LATTICES, NAT_D, SEQ_2;
lem6:
2 divides 2 * 3
;
lem8:
2 divides 2 * 4
;
lem9:
3 divides 3 * 3
;
lem10:
2 divides 2 * 5
;
lem12:
2 divides 2 * 6
;
LmX:
for p being Prime holds card (FreeGen p) c= 2 |^ p
SquareBool0:
for n being non zero square-free Nat holds Divisors_Lattice n is Boolean