environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, SUBSET_1, FUNCT_1, CARD_1, XCMPLX_0, INT_2, XXREAL_0, ARYTM_3, FINSEQ_1, RELAT_1, ABIAN, NEWTON, NAT_3, PRE_POLY, NAT_1, UPROOTS, CARD_3, TARSKI, INT_1, FINSET_1, ARYTM_1, PYTHTRIP, ZFMISC_1, SQUARE_1, REAL_1, SETFAM_1, PBOOLE, VALUED_0, FUNCOP_1, MOEBIUS1, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, FINSET_1, ZFMISC_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, XREAL_0, XXREAL_0, NEWTON, SETFAM_1, RELAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, VALUED_0, PBOOLE, SQUARE_1, RVSUM_1, FUNCOP_1, XXREAL_2, NAT_3, DOMAIN_1, ABIAN, UPROOTS, PYTHTRIP, RECDEF_1, PRE_POLY, REAL_1, NAT_1, NAT_D, INT_2;
definitions TARSKI, XBOOLE_0;
theorems XBOOLE_0, NAT_3, NEWTON, INT_2, NAT_2, WSIERP_1, CARD_1, PEPIN, NAT_1, XCMPLX_1, XREAL_1, PYTHTRIP, ABIAN, ORDINAL1, EULER_1, XREAL_0, FINSEQ_1, XBOOLE_1, TARSKI, ZFMISC_1, RVSUM_1, FINSEQ_2, NUMBERS, INT_1, FUNCT_1, PBOOLE, UPROOTS, CARD_4, FUNCOP_1, RELAT_1, FINSOP_1, XXREAL_0, NAT_D, VALUED_0, XXREAL_2, FUNCT_2, PARTFUN1, PRE_POLY, MEASURE6;
schemes FUNCT_2, CLASSES1, PRE_CIRC, SUBSET_1, NAT_1;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, FINSET_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, INT_1, MEMBERED, FINSEQ_1, NEWTON, NAT_3, VALUED_0, XXREAL_2, CARD_1, RELSET_1, PRE_POLY;
constructors HIDDEN, NAT_D, FINSOP_1, WSIERP_1, ABIAN, PEPIN, PYTHTRIP, UPROOTS, NAT_3, RECDEF_1, BINOP_2, XXREAL_2, REAL_1, DOMAIN_1, RELSET_1;
requirements HIDDEN, NUMERALS, SUBSET, ARITHM, REAL, BOOLE;
equalities RVSUM_1, SQUARE_1;
expansions TARSKI, XBOOLE_0;
Lm1:
for X, Y, Z, x being set st X misses Y & x in X /\ Z holds
not x in Y /\ Z
by XBOOLE_1:76, XBOOLE_0:3;
Lm2:
for n being Nat st n <> 1 holds
ex p being Prime st p divides n
Lm3:
for n being non zero Nat
for p being Prime holds not p |^ 2 divides Radical n
Lm4:
for n being non zero Nat holds Radical n is square-free
by Lm3;
Lm5:
for m, n being non zero Element of NAT st m divides n & m is square-free holds
m divides Radical n