let p be Prime; :: thesis: for n being Nat st 1 <= n & n * p is square-free holds
Moebius (n * p) = - (Moebius n)
let a be Nat; :: thesis: ( 1 <= a & a * p is square-free implies Moebius (a * p) = - (Moebius a) )
assume that
A1: 1 <= a and
A2: a * p is square-free ; :: thesis: Moebius (a * p) = - (Moebius a)
a,p are_coprime

proof

assume not a,p are_coprime ; :: thesis: contradiction
then consider q being Prime such that
A4: q divides a and
A5: q divides p by PYTHTRIP:def 2;
( q = 1 or q = p ) by A5, INT_2:def 4;
then p * p divides a * p by A4, INT_2:def 4, PYTHTRIP:7;
then p |^ 2 divides a * p by WSIERP_1:1;
hence contradiction by A2; :: thesis: verum

end;

then Moebius (a * p) = (Moebius a) * (Moebius p) by A1, Th35
.= (Moebius a) * (- 1) by Th34 ;
hence Moebius (a * p) = - (Moebius a) ; :: thesis: verum