let a, b be non zero Element of NAT ; :: thesis: ( a,b are_relative_prime implies Moebius (a * b) = (Moebius a) * (Moebius b) )
assume A1: a,b are_relative_prime ; :: thesis: Moebius (a * b) = (Moebius a) * (Moebius b)

per cases ( ( not a is square-containing & not b is square-containing ) or ( not a is square-containing & b is square-containing ) or ( a is square-containing & not b is square-containing ) or ( a is square-containing & b is square-containing ) ) ;

suppose A2: ( not a is square-containing & not b is square-containing ) ; :: thesis: Moebius (a * b) = (Moebius a) * (Moebius b)

A3: not a * b is square-containing

proof

assume a * b is square-containing ; :: thesis: contradiction
then consider p being Prime such that
A4: p |^ 2 divides a * b by Def1;
p in NAT by ORDINAL1:def 13;
then ( p |^ 2 divides a or p |^ 2 divides b ) by A1, A4, Th11;
hence contradiction by A2, Def1; :: 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:13 ;
hence Moebius (a * b) = (Moebius a) * (Moebius b) by A2, A5, Def3; :: thesis: verum

end;

suppose A6: ( not a is square-containing & b is square-containing ) ; :: thesis: Moebius (a * b) = (Moebius a) * (Moebius b)

then consider p being Prime such that
A7: p |^ 2 divides b by Def1;
p |^ 2 divides a * b by A7, NAT_D:9;
then A8: a * b is square-containing by Def1;
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 & not b is square-containing ) ; :: thesis: Moebius (a * b) = (Moebius a) * (Moebius b)

then consider p being Prime such that
A10: p |^ 2 divides a by Def1;
p |^ 2 divides a * b by A10, NAT_D:9;
then A11: a * b is square-containing by Def1;
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 by Def1;
p |^ 2 divides a * b by A13, NAT_D:9;
then A14: a * b is square-containing by Def1;
Moebius a = 0 by A12, Def3;
hence Moebius (a * b) = (Moebius a) * (Moebius b) by A14, Def3; :: thesis: verum

end;

end;