let p be Prime; :: thesis: for n being Element of NAT st 1 <= n & n * p is square-free holds
Moebius (n * p) = - (Moebius n)
let a be Element of 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)
A3: p in NAT by ORDINAL1:def 12;
a,p are_coprime
proof
assume not a,p are_coprime ; :: 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; :: 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