let a, b be non zero Element of NAT ; :: thesis: ( a,b are_coprime implies Moebius (a * b) = (Moebius a) * (Moebius b) )
assume A1: a,b are_coprime ; :: thesis: Moebius (a * b) = (Moebius a) * (Moebius b)
per cases ( ( a is square-free & b is square-free ) or ( a is square-free & b is square-containing ) or ( a is square-containing & b is square-free ) or ( a is square-containing & b is square-containing ) ) ;
suppose A2: ( a is square-free & b is square-free ) ; :: thesis: Moebius (a * b) = (Moebius a) * (Moebius b)
A3: a * b is square-free
proof
assume a * b is square-containing ; :: thesis: contradiction
then consider p being Prime such that
A4: p |^ 2 divides a * b ;
p in NAT by ORDINAL1:def 12;
then ( p |^ 2 divides a or p |^ 2 divides b ) by A1, A4, Th11;
hence contradiction by A2; :: thesis: verum
end;
A5: Moebius a = (- 1) |^ (card (support (ppf a))) by A2, Def3;
card (support (pfexp (a * b))) = (card (support (pfexp a))) + (card (support (pfexp b))) by A1, NAT_3:47;
then card (support (ppf (a * b))) = (card (support (pfexp a))) + (card (support (pfexp b))) by NAT_3:def 9
.= (card (support (pfexp a))) + (card (support (ppf b))) by NAT_3:def 9
.= (card (support (ppf a))) + (card (support (ppf b))) by NAT_3:def 9 ;
then Moebius (a * b) = (- 1) |^ ((card (support (ppf a))) + (card (support (ppf b)))) by A3, Def3
.= ((- 1) |^ (card (support (ppf a)))) * ((- 1) |^ (card (support (ppf b)))) by NEWTON:8 ;
hence Moebius (a * b) = (Moebius a) * (Moebius b) by A2, A5, Def3; :: thesis: verum
end;
suppose A6: ( a is square-free & b is square-containing ) ; :: thesis: Moebius (a * b) = (Moebius a) * (Moebius b)
then consider p being Prime such that
A7: p |^ 2 divides b ;
p |^ 2 divides a * b by A7, NAT_D:9;
then A8: a * b is square-containing ;
Moebius b = 0 by A6, Def3;
hence Moebius (a * b) = (Moebius a) * (Moebius b) by A8, Def3; :: thesis: verum
end;
suppose A9: ( a is square-containing & b is square-free ) ; :: thesis: Moebius (a * b) = (Moebius a) * (Moebius b)
then consider p being Prime such that
A10: p |^ 2 divides a ;
p |^ 2 divides a * b by A10, NAT_D:9;
then A11: a * b is square-containing ;
Moebius a = 0 by A9, Def3;
hence Moebius (a * b) = (Moebius a) * (Moebius b) by A11, Def3; :: thesis: verum
end;
suppose A12: ( a is square-containing & b is square-containing ) ; :: thesis: Moebius (a * b) = (Moebius a) * (Moebius b)
then consider p being Prime such that
A13: p |^ 2 divides a ;
p |^ 2 divides a * b by A13, NAT_D:9;
then A14: a * b is square-containing ;
Moebius a = 0 by A12, Def3;
hence Moebius (a * b) = (Moebius a) * (Moebius b) by A14, Def3; :: thesis: verum
end;
end;