let A be finite Subset of SetPrimes; Product (A -bag) is square-free
set n = Product (A -bag);
reconsider n = Product (A -bag) as non zero Nat by MOEBIUS2:26;
C2:
Product (A -bag) = Product (ppf n)
by NAT_3:61;
ZW:
ppf n = A -bag
by INT_7:15, C2;
for p being Prime holds not p |^ 2 divides n
proof
given p1 being
Prime such that K1:
p1 |^ 2
divides n
;
contradiction
K2:
p1 |-count (p1 |^ 2) <= p1 |-count n
by NAT_3:30, K1;
set m =
p1 |-count n;
W2:
p1 |-count n >= 2
by K2, NAT_3:25, INT_2:def 4;
p1 |^ 1
divides p1 |^ 2
by NEWTON:89;
then V1:
p1 in support (pfexp n)
by NAT_3:37, K1, NAT_D:4;
then W1:
(ppf n) . p1 = p1 |^ (p1 |-count n)
by NAT_3:def 9;
p1 in support (ppf n)
by V1, NAT_3:def 9;
then
p1 = p1 |^ (p1 |-count n)
by W1, BagValue, ZW;
hence
contradiction
by PREPOWER:13, W2, INT_2:def 4;
verum
end;
hence
Product (A -bag) is square-free
by MOEBIUS1:def 1; verum