let p be Prime; :: thesis: for n being Element of NAT st 1 <= n & not n * p is square-containing holds
Moebius (n * p) = - (Moebius n)
let a be Element of NAT ; :: thesis: ( 1 <= a & not a * p is square-containing implies Moebius (a * p) = - (Moebius a) )
assume that
A1: 1 <= a and
A2: not a * p is square-containing ; :: thesis: Moebius (a * p) = - (Moebius a)
A3: p in NAT by ORDINAL1:def 12;
a,p are_relative_prime

proof

assume not a,p are_relative_prime ; :: thesis: contradiction
then consider q being prime Nat 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 A3, A4, INT_2:def 4, PYTHTRIP:7;
then p |^ 2 divides a * p by WSIERP_1:1;
hence contradiction by A2, Def1; :: thesis: verum

end;

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