# Theory Mu

Up to index of Isabelle/HOL/HOL-Complex/NumberTheory

theory Mu = Radical:

```(*  Title:      Mu.thy
Author:     David Gray
*)

header {* Properties of the mu function *}

theory Mu = Radical:;

(**********************************************)
(* Good lemma -- but can we prove it without  *)
(* resorting to using multiplicity stuff???   *)
(**********************************************)

lemma zdvd_zmult_not_zdvd_impl_zdvd: "[| p:zprime; 0 < d; 0 < a; (d::int) dvd a * p ; ~ p dvd d |] ==> d dvd a";
apply (rule_tac  multiplicity_le_imp_zdvd, auto);
apply (case_tac "p = pa", auto);
proof-;
assume "~ p dvd d" and "0 < d";
then have "~ p mem pfactors d";
by (insert mem_pfactors_imp_zdvd [of d p], auto);
then have "multiplicity p d = 0";
by (auto simp add: multiplicity_def not_mem_numoccurs_eq_0);
thus "multiplicity p d <= multiplicity p a";
by auto;
next;
fix pa;
assume "p ~= pa";
assume "p:zprime" and "0 < a";
then have "0 < a * p";
by (insert prems, auto simp add: mult_pos zprime_def);
moreover assume "d dvd a * p";
ultimately have "ALL pq. (multiplicity pq d <= multiplicity pq (a * p))";
by (drule_tac zdvd_imp_multiplicity_le, auto);
then have "multiplicity pa d <= multiplicity pa (a * p)";
by auto;
also have "multiplicity pa (a * p) = multiplicity pa a + multiplicity pa p";
by (insert prems, auto simp add: multiplicity_zmult_distrib zprime_def);
also have "multiplicity pa p = 0";
by (insert prems, auto simp add: multiplicity_def pfactors_zprime);
finally show "multiplicity pa d <= multiplicity pa a" by auto;
qed;

(*********************)
(* The Real thing... *)
(*********************)

consts
mu           :: "int => int";

defs
mu_def:           "mu n ==
(if (n <= 1) then 1
else if (squarefree n) then
(if (even(int(length(pfactors n)))) then 1
else -1)
else 0)";

subsection {* Properties about mu *}

lemma mu_eq_1: "n <= 1 ==> mu (n) = 1";
by (auto simp add: mu_def);

lemma mu_zprime: "p:zprime ==> mu(p) = -1";
by (auto simp add: mu_def squarefree_def pfactors_zprime zprime_def);

lemma mu_squarefree1: "[| 1 <= n; ~squarefree(n) |] ==> mu(n) = 0";
apply (case_tac "~squarefree n");
apply (auto simp add: mu_def);
apply (simp add: squarefree_def);
done;

lemma mu_squarefree2: "[| 1 <= n; mu(n) ~= 0 |] ==> squarefree(n)";
proof-;
assume "1 <= n" and "mu(n) ~= 0";
moreover note mu_squarefree1;
ultimately show ?thesis by auto;
qed;

lemma aux1: "[| p:zprime; 1 < d; squarefree(d * p) |] ==> mu(d * p) = -1 * mu(d)";
apply (subgoal_tac "0 < d"); defer;
apply (force);
apply (subgoal_tac "1 < p"); defer;
apply (simp add: zprime_def);
apply (subgoal_tac "1 < d * p");defer;
apply (insert zmult_eq_1_iff [of d p] zero_less_mult_iff [of d p], force);
apply (subgoal_tac "length (pfactors (d * p)) = length(pfactors d) + 1");defer;
apply (simp add: pfactors_zprime_zmult_length);
apply (frule_tac x = d and y = p in squarefree_distrib1, force, force);
apply (frule_tac x = d and y = p in squarefree_distrib2, force, force);
apply (auto simp add: mu_def);
done;

lemma aux2: "[| p:zprime; 1 = d; squarefree(d * p) |] ==> mu(d * p) = -1 * mu(d)";
apply (auto simp add: mu_def length_pfactors_zprime zprime_def);
done;

lemma squarefree_mu_prop: "[| p:zprime; 1 <= d; squarefree(d * p) |] ==> mu(d * p) = -mu(d)";
apply (case_tac "1 = d");
apply (drule aux2, auto);
apply (subgoal_tac "1 < d");
apply (auto simp add: aux1);
done;

(* Get the parts for the mu property *)

(*******************************************)
(* A useful lemma... move to Finite2??     *)
(*******************************************)

lemma pos_pos_zdvd_finite: "(0::int) < m ==> finite {d. 0 < d & d dvd m}";
proof-;
assume "0 < m";
then have "{d. 0 < d & d dvd m} <= {d. 0 < d & d <= m}";
apply (auto);
apply (drule zdvd_bounds, auto);
done;
moreover have "finite {d. 0 < d & d <= m}";
apply (subgoal_tac "{d. 0 < d & d <= m} = {)0..m}");
apply (erule ssubst, auto);
done;
ultimately show ?thesis by (auto simp add: finite_subset);
qed;

(*********************************************)
(* Don't really know what to do with this... *)
(* It is essential to the proof below though *)
(*********************************************)

lemma zprime_zdvd_existence_rad: "1 < n ==> (hd (pdivisors n)):zprime & (hd (pdivisors n)) dvd (rad n)";
apply (case_tac "pdivisors n");
apply (frule pdivisors_gr_1, force);
apply (insert pdivisors_zprimel [of n]);
apply (subgoal_tac "a mem (pdivisors n)");
done;

(***********************)
(* Key Step Number One *)
(***********************)

lemma squarefree_subsets_prop1: "{d. (0::int) < d & d dvd n} =
{d. 0 < d & d dvd n & squarefree d} Un {d. 0 < d & d dvd n & ~squarefree d}";
by (auto);

lemma squarefree_subsets_prop2: "{d. 0 < d & d dvd n & squarefree d} Int {d. 0 < d & d dvd n & ~squarefree d} = {}";
by (auto);

lemma squarefree_subset1_finite: "(0::int) < n ==> finite {d. 0 < d & d dvd n & squarefree d}";
proof-;
assume "0 < n";
then have "finite {d. 0 < d & d dvd n}";
by (auto simp add: pos_pos_zdvd_finite);
moreover have "{d. 0 < d & d dvd n & squarefree d} <= {d. 0 < d & d dvd n}";
by (auto);
ultimately show ?thesis by (auto simp add: finite_subset);
qed;

lemma squarefree_subset2_finite: "(0::int) < n ==> finite {d. 0 < d & d dvd n & ~squarefree d}";
proof-;
assume "0 < n";
then have "finite {d. 0 < d & d dvd n}";
by (auto simp add: pos_pos_zdvd_finite);
moreover have "{d. 0 < d & d dvd n & ~squarefree d} <= {d. 0 < d & d dvd n}";
by (auto);
ultimately show ?thesis by (auto simp add: finite_subset);
qed;

lemma key_step1: "(0::int) < n ==>
setsum mu {d. 0 < d & d dvd n} =
setsum mu {d. 0 < d & d dvd n & squarefree d} + setsum mu {d. 0 < d & d dvd n & ~ squarefree d}";
proof-;
assume "0 < n";
then have "finite {d. 0 < d & d dvd n & squarefree d}" and
"finite {d. 0 < d & d dvd n & ~ squarefree d}";
by (insert squarefree_subset1_finite [of n] squarefree_subset2_finite [of n], auto);
moreover have "{d. (0::int) < d & d dvd n & squarefree d} Int {d. 0 < d & d dvd n & ~squarefree d} = {}";
by (auto simp add: squarefree_subsets_prop2);
ultimately have "setsum mu ({d. 0 < d & d dvd n & squarefree d} Un {d. 0 < d & d dvd n & ~ squarefree d}) =
setsum mu {d. 0 < d & d dvd n & squarefree d} + setsum mu {d. 0 < d & d dvd n & ~ squarefree d}";
by (rule setsum_Un_disjoint);
also have "{d. 0 < d & d dvd n & squarefree d} Un {d. 0 < d & d dvd n & ~ squarefree d} =
{d. 0 < d & d dvd n}"
by (auto simp add: squarefree_subsets_prop1);
finally show ?thesis .;
qed;

(*********************************)
(* Now go to key step number two *)
(*********************************)

lemma not_squarefree_setsum_prop: "0 < n ==> setsum mu {d. (0::int) < d & d dvd n & ~squarefree d} = 0";
proof-;
assume "0 < n";
then have "ALL x:{d. (0::int) < d & d dvd n & ~squarefree d}. mu x = (%x. 0) x";
by (auto simp add: mu_squarefree1);
moreover have p1: "finite {d. (0::int) < d & d dvd n & ~squarefree d}";
by (insert prems, auto simp add: squarefree_subset2_finite);
ultimately have "setsum mu {d. (0::int) < d & d dvd n & ~squarefree d} =
setsum (%x. 0) {d. (0::int) < d & d dvd n & ~squarefree d}";
by (rule_tac setsum_cong, auto);
also have "... = 0"
by (rule finite_induct, auto simp add: p1);
finally show ?thesis .;
qed;

lemma zdvd_squarefree_eq_zdvd_rad: "0 < n ==> {d. (0::int) < d & d dvd n & squarefree d} =
{d. 0 < d & d dvd rad(n)}";
apply (auto);
apply (rule squarefree_zdvd_imp_zdvd_rad, auto);
apply (subgoal_tac "rad n dvd n");
apply (frule zdvd_trans, auto);
apply (subgoal_tac "0 < rad n");
apply (subgoal_tac "squarefree (rad n)");
apply (frule_tac n = "rad n" in squarefree_zdvd_impl_squarefree);
apply (insert rad_min_gre_1 [of n], auto);
done;

lemma key_step2: "(0::int) < n ==>
setsum mu {d. 0 < d & d dvd n & squarefree d} + setsum mu {d. 0 < d & d dvd n & ~ squarefree d} =
setsum mu {d. 0 < d & d dvd (rad n)}";
proof-;
assume "0 < n";
then have "setsum mu {d. 0 < d & d dvd n & squarefree d} + setsum mu {d. 0 < d & d dvd n & ~ squarefree d} =
setsum mu {d. 0 < d & d dvd (rad n)} + 0";
thus ?thesis by auto;
qed;

(**********************************)
(* Time for Key Step number three *)
(* Note that rad n = m            *)
(**********************************)

lemma zdvd_subsets_prop1: "{d. (0::int) < d & d dvd m} =
{d. 0 < d & d dvd m & p dvd d} Un {d. 0 < d & d dvd m & ~p dvd d}";
by (auto);

lemma zdvd_subsets_prop2: "{d. (0::int) < d & d dvd m & p dvd d} Int {d. 0 < d & d dvd m & ~p dvd d} = {}";
by (auto);

lemma subset1_finite: "(0::int) < m ==> finite {d. 0 < d & d dvd m & p dvd d}";
proof-;
assume "0 < m";
then have "finite {d. 0 < d & d dvd m}";
by (auto simp add: pos_pos_zdvd_finite);
moreover have "{d. 0 < d & d dvd m & p dvd d} <= {d. 0 < d & d dvd m}";
by (auto);
ultimately show ?thesis by (auto simp add: finite_subset);
qed;

lemma subset2_finite: "(0::int) < m ==> finite {d. 0 < d & d dvd m & ~ p dvd d}";
proof-;
assume "0 < m";
then have "finite {d. 0 < d & d dvd m}";
by (auto simp add: pos_pos_zdvd_finite);
moreover have "{d. 0 < d & d dvd m & ~p dvd d} <= {d. 0 < d & d dvd m}";
by (auto);
ultimately show ?thesis by (auto simp add: finite_subset);
qed;

lemma key_step3: "(0::int) < m ==>
setsum mu {d. 0 < d & d dvd m} =
setsum mu {d. 0 < d & d dvd m & p dvd d} + setsum mu {d. 0 < d & d dvd m & ~ p dvd d}";
proof-;
assume "0 < m";
then have "finite {d. 0 < d & d dvd m & p dvd d}" and
"finite {d. 0 < d & d dvd m & ~ p dvd d}";
by (insert subset1_finite [of m p] subset2_finite [of m p], auto);
moreover have "{d. (0::int) < d & d dvd m & p dvd d} Int {d. 0 < d & d dvd m & ~p dvd d} = {}"
by (auto simp add: zdvd_subsets_prop2);
ultimately have "setsum mu ({d. 0 < d & d dvd m & p dvd d} Un {d. 0 < d & d dvd m & ~ p dvd d}) =
setsum mu {d. 0 < d & d dvd m & p dvd d} + setsum mu {d. 0 < d & d dvd m & ~ p dvd d}";
by (rule setsum_Un_disjoint);
also have "{d. 0 < d & d dvd m & p dvd d} Un {d. 0 < d & d dvd m & ~ p dvd d} =
{d. (0::int) < d & d dvd m}"
by (auto simp add: zdvd_subsets_prop1);
finally show ?thesis .;
qed;

(**************************)
(* Show Key Step number 4 *)
(**************************)

lemma aux_inject_prop: "p:zprime ==> inj_on (%x. (x::int) * p)  {d. (0::int) < d & d dvd (m div p)}";
by (auto simp add: inj_on_def, auto simp add: zprime_def);

lemma aux_finite_prop: "[| p:zprime; 0 < m; p dvd m |] ==> finite {d. (0::int) < d & d dvd (m div p)}";
proof-;
assume "p : zprime" and "0 < m" and "p dvd m";
then have "0 < m div p";
proof-;
have "p <= m" by (insert prems zdvd_bounds [of p m], auto);
then have "p div p <= m div p";
by (insert prems, rule zdiv_mono1, auto simp add: zprime_def);
also have "p div p = 1" by (insert prems, auto simp add: zprime_def);
finally show "0 < m div p" by auto;
qed;
thus ?thesis by (auto simp add: pos_pos_zdvd_finite);
qed;

lemma aux_image_prop: "[| p:zprime; p dvd m |] ==>
((%x. (x::int) * p) `  {d. (0::int) < d & d dvd (m div p)}) =
{d. 0 < d & d dvd m & p dvd d }";
apply (auto simp add: image_def)
apply (clarsimp simp add: zprime_def zero_less_mult_iff); defer;
apply (rule_tac x = "x div p" in exI, auto);
proof-;
fix x;
assume "p:zprime" and "p dvd x" and "0 < x";
then have "p <= x" by (insert zdvd_bounds [of p x], auto);
then have "p div p <= x div p";
by (insert prems, rule zdiv_mono1, auto simp add: zprime_def);
also have "p div p = 1" by (insert prems, auto simp add: zprime_def);
finally show "0 < x div p" by auto;
next;
fix x;
assume "p:zprime";
assume "p dvd x" and p1: "x dvd m";
then have p2: "p dvd m" by (rule zdvd_trans);
note p1;
also have "m = p * (m div p)";
by (insert p2 zmod_zdiv_equality [of m p] zdvd_iff_zmod_eq_0 [of p m], auto);
also have "x = p * (x div p)";
by (insert prems zmod_zdiv_equality [of x p] zdvd_iff_zmod_eq_0 [of p x], auto);
finally have "p * (x div p) dvd p * (m div p)".;
thus "(x div p) dvd (m div p)";
apply (rule_tac a = p in ne_0_zdvd_prop);
apply (insert prems, auto simp add: zprime_def);
done;
next;
fix x;
assume "p dvd x";
thus "x = (x div p) * p";
by (insert zmod_zdiv_equality [of x p] zdvd_iff_zmod_eq_0 [of p x], auto);
next;
fix xa;
assume "p dvd m";
then have p1 :"p * (m div p) = m";
by (insert zmod_zdiv_equality [of m p] zdvd_iff_zmod_eq_0 [of p m], auto);
assume "xa dvd m div p";
then have "p * xa dvd p * (m div p)"
by (insert zdvd_refl [of p], auto simp add: zdvd_zmult_mono);
also note p1;
finally show "xa * p dvd m" by (auto simp add: zmult_ac);
qed;

lemma aux3: "[| p : zprime; 0 < m; p dvd m|] ==>
setsum mu {d. 0 < d & d dvd m & p dvd d} =
setsum (mu ˆ (%x. (x::int) * p)) {d. (0::int) < d & d dvd (m div p)}";
proof-;
assume "p:zprime" and "0 < m" and "p dvd m";
then have "setsum mu ((%x. (x::int) * p) `  {d. (0::int) < d & d dvd (m div p)}) =
setsum (mu ˆ (%x. (x::int) * p)) {d. (0::int) < d & d dvd (m div p)}";
apply (insert prems aux_finite_prop [of p m] aux_inject_prop [of p m]);
apply (rule setsum_reindex, auto);
done;
also have "((%x. (x::int) * p) `  {d. (0::int) < d & d dvd (m div p)}) =
{d. 0 < d & d dvd m & p dvd d }";
by (insert prems, auto simp add: aux_image_prop);
finally show ?thesis .;
qed;

lemma aux4: "[| p:zprime; 0 < m; p dvd m; squarefree m|] ==>
ALL x:{d. (0::int) < d & d dvd (m div p)}.
(mu ˆ (%x. (x::int) * p))x = ((%x. -(x::int)) ˆ mu)x";
apply (auto, rule squarefree_mu_prop, auto);
proof-;
fix x;
assume "x dvd m div p" and "p dvd m";
then have "x * p dvd (m div p) * p";
by (insert zdvd_refl [of p], auto simp add: zdvd_zmult_mono);
also have "(m div p) * p = m";
by (insert prems zmod_zdiv_equality [of m p] zdvd_iff_zmod_eq_0 [of p m], auto);
finally have "x * p dvd m".;
moreover assume "squarefree m" and "0 < m";
ultimately show "squarefree(x * p)"
by (rule_tac squarefree_zdvd_impl_squarefree);
qed;

lemma aux5: "[| p : zprime; 0 < m; p dvd m; squarefree m |] ==>
setsum (mu ˆ (%x. (x::int) * p)) {d. (0::int) < d & d dvd (m div p)} =
setsum ((%x. -(x::int)) ˆ mu) {d. (0::int) < d & d dvd (m div p)}";
proof-;
assume "p : zprime" and "0 < m" and "p dvd m" and "squarefree m";
with aux4 have "ALL x:{d. (0::int) < d & d dvd (m div p)}.
(mu ˆ (%x. (x::int) * p))x = ((%x. -(x::int)) ˆ mu)x";
by (auto);
moreover from aux_finite_prop have "finite {d. (0::int) < d & d dvd (m div p)}";
by (insert prems, auto);
ultimately show ?thesis
apply (intro setsum_cong);
apply auto;
done;
qed;

lemma aux6: "[| p:zprime; 0 < m; p dvd m; squarefree m |] ==>
{d. (0::int) < d & d dvd m & ~p dvd d} = {d. 0 < d & d dvd (m div p)}";
apply (auto, rule zdvd_zmult_not_zdvd_impl_zdvd, auto);
proof-;
fix x;
assume "p :zprime" and "0 < m" and "p dvd m";
then have "p <= m" by (insert zdvd_bounds [of p m], auto);
then have "p div p <= m div p";
by (insert prems, rule zdiv_mono1, auto simp add: zprime_def);
also have "p div p = 1" by (insert prems, auto simp add: zprime_def);
finally show "0 < m div p" by auto;
next;
fix x;
assume "p dvd m";
assume "x dvd m";
also have "m = (m div p) * p";
by (insert prems zmod_zdiv_equality [of m p] zdvd_iff_zmod_eq_0 [of p m], auto);
finally show "x dvd m div p * p" .;
next;
fix x;
assume "p dvd m";
assume "x dvd m div p";
then have "x dvd (m div p) * p";
by (auto simp add: zdvd_zmult2);
also have "(m div p) * p = m";
by (insert prems zmod_zdiv_equality [of m p] zdvd_iff_zmod_eq_0 [of p m], auto);
finally show "x dvd m" .;
next;
fix x;
assume "p dvd m" and "p:zprime" and "0 < m";
assume "x dvd m div p" and "p dvd x";
then have "p dvd m div p" by (rule_tac zdvd_trans);
then have "p * p dvd (m div p) * p";
by (insert zdvd_refl [of p], auto simp add: zdvd_zmult_mono);
also have "p * p = p ^ Suc(Suc(0))";
by (auto simp add: power_Suc);
also have "Suc(Suc(0))= 2" by auto;
also have "m div p * p = m";
by (insert prems zmod_zdiv_equality [of m p] zdvd_iff_zmod_eq_0 [of p m], auto);
finally have "p ^ 2 dvd m" .;
then have "2 <= multiplicity p m";
by (insert prems, auto simp add: multiplicity_zpower_zdvd);
moreover assume "squarefree m";
ultimately show "False";
apply (auto simp add: squarefree_prop);
apply (drule_tac x = p in spec, auto);
done;
qed;

lemma aux7: "[| p : zprime; 0 < m; p dvd m; squarefree m |] ==>
setsum mu {d. 0 < d & d dvd m & ~p dvd d} =
setsum mu {d. 0 < d & d dvd (m div p)}";
by (auto simp add: aux6);

lemma key_step4: "[| p : zprime; 0 < m; p dvd m; squarefree m |] ==>
setsum mu {d. 0 < d & d dvd m & p dvd d} + setsum mu {d. 0 < d & d dvd m & ~ p dvd d} =
setsum ((%x. -(x::int)) ˆ mu) {d. (0::int) < d & d dvd (m div p)} +
setsum mu {d. 0 < d & d dvd (m div p)}";
proof-;
assume "p : zprime" and "0 < m" and "p dvd m" and "squarefree m";
then have "setsum mu {d. 0 < d & d dvd m & p dvd d} + setsum mu {d. 0 < d & d dvd m & ~ p dvd d} =
setsum (mu ˆ (%x. (x::int) * p)) {d. (0::int) < d & d dvd (m div p)} +
setsum mu {d. 0 < d & d dvd (m div p)}";
by (auto simp add: aux3 aux7);
also have "setsum (mu ˆ (%x. (x::int) * p)) {d. (0::int) < d & d dvd (m div p)} =
setsum ((%x. -(x::int)) ˆ mu) {d. (0::int) < d & d dvd (m div p)}";
by (insert prems, auto simp add: aux5);
finally show ?thesis .;
qed;

lemma key_step5: "[| p : zprime; 0 < m; p dvd m |] ==>
setsum ((%x. -(x::int)) ˆ mu) {d. (0::int) < d & d dvd (m div p)} +
setsum mu {d. 0 < d & d dvd (m div p)} =
0";
proof-;
assume "p : zprime" and "0 < m" and "p dvd m";
have "setsum ((%x. -(x::int)) ˆ mu) {d. (0::int) < d & d dvd (m div p)} +
setsum mu {d. 0 < d & d dvd (m div p)} =
setsum (%x. ((%x. -(x::int)) ˆ mu)(x) + (mu x)) {d. (0::int) < d & d dvd (m div p)}";
by (auto simp add: setsum_addf [THEN sym]);
also have "setsum (%x. ((%x. -(x::int)) ˆ mu)(x) + (mu x)) {d. (0::int) < d & d dvd (m div p)} = 0";
apply (insert prems aux_finite_prop [of p m]);
apply (auto simp add: setsum_constant);
done;
finally show ?thesis .;
qed;

theorem moebius_prop: "[| 1 <= n |] ==> setsum mu {d. 0 < d & d dvd n} = (if n = 1 then 1 else 0)";
apply (case_tac "n = 1");
apply (auto);
apply (subgoal_tac "{d. (0::int) < d & d dvd 1} = {1}");
apply (simp);
apply (simp add: mu_def);
apply (insert ge_0_zdvd_1);
apply (force);
apply (subgoal_tac "1 < n");
apply (auto);
proof-;
assume "1 < n";
then have p1: "1 < rad n" by (auto simp add: rad_min_gr_1);
have p2: "(hd (pdivisors n)):zprime" and p3: "(hd (pdivisors n)) dvd (rad n)";
by (insert prems, auto simp add: zprime_zdvd_existence_rad);
have p4: "squarefree (rad n)";
by (insert prems, auto simp add: rad_squarefree);
have "setsum mu {d. 0 < d & d dvd n} =
setsum mu {d. 0 < d & d dvd n & squarefree d} + setsum mu {d. 0 < d & d dvd n & ~ squarefree d}";
by (insert prems, auto simp add: key_step1);
also have "... = setsum mu {d. 0 < d & d dvd (rad n)}";
by (insert prems, auto simp add: key_step2);
also have "... = setsum mu {d. 0 < d & d dvd (rad n) & (hd (pdivisors n)) dvd d} +
setsum mu {d. 0 < d & d dvd (rad n) & ~ (hd (pdivisors n)) dvd d}";
apply (subgoal_tac "0 < rad n");
apply (drule_tac p = "(hd (pdivisors n))" in key_step3, force);
apply (insert p1, auto);
done;
also have "... = setsum ((%x. -(x::int)) ˆ mu) {d. (0::int) < d & d dvd ((rad n) div (hd (pdivisors n)))} +
setsum mu {d. 0 < d & d dvd ((rad n) div (hd (pdivisors n)))}";
apply (rule_tac key_step4);
apply (insert p1 p2 p3 p4, auto);
done;
also have "... = 0";
apply (rule_tac key_step5);
apply (insert prems p1 p2 p3, auto);
done;
finally show "setsum mu {d. 0 < d & d dvd n} = 0".;
qed;

end;
```

lemma zdvd_zmult_not_zdvd_impl_zdvd:

`  [| p ∈ zprime; 0 < d; 0 < a; d dvd a * p; ¬ p dvd d |] ==> d dvd a`

### Properties about mu

lemma mu_eq_1:

`  n ≤ 1 ==> mu n = 1`

lemma mu_zprime:

`  p ∈ zprime ==> mu p = -1`

lemma mu_squarefree1:

`  [| 1 ≤ n; ¬ squarefree n |] ==> mu n = 0`

lemma mu_squarefree2:

`  [| 1 ≤ n; mu n ≠ 0 |] ==> squarefree n`

lemma aux1:

`  [| p ∈ zprime; 1 < d; squarefree (d * p) |] ==> mu (d * p) = -1 * mu d`

lemma aux2:

`  [| p ∈ zprime; 1 = d; squarefree (d * p) |] ==> mu (d * p) = -1 * mu d`

lemma squarefree_mu_prop:

`  [| p ∈ zprime; 1 ≤ d; squarefree (d * p) |] ==> mu (d * p) = - mu d`

lemma pos_pos_zdvd_finite:

`  0 < m ==> finite {d. 0 < d ∧ d dvd m}`

`  1 < n ==> hd (pdivisors n) ∈ zprime ∧ hd (pdivisors n) dvd rad n`

lemma squarefree_subsets_prop1:

```  {d. 0 < d ∧ d dvd n} =
{d. 0 < d ∧ d dvd n ∧ squarefree d} ∪ {d. 0 < d ∧ d dvd n ∧ ¬ squarefree d}```

lemma squarefree_subsets_prop2:

`  {d. 0 < d ∧ d dvd n ∧ squarefree d} ∩ {d. 0 < d ∧ d dvd n ∧ ¬ squarefree d} = {}`

lemma squarefree_subset1_finite:

`  0 < n ==> finite {d. 0 < d ∧ d dvd n ∧ squarefree d}`

lemma squarefree_subset2_finite:

`  0 < n ==> finite {d. 0 < d ∧ d dvd n ∧ ¬ squarefree d}`

lemma key_step1:

```  0 < n
==> setsum mu {d. 0 < d ∧ d dvd n} =
setsum mu {d. 0 < d ∧ d dvd n ∧ squarefree d} +
setsum mu {d. 0 < d ∧ d dvd n ∧ ¬ squarefree d}```

lemma not_squarefree_setsum_prop:

`  0 < n ==> setsum mu {d. 0 < d ∧ d dvd n ∧ ¬ squarefree d} = 0`

`  0 < n ==> {d. 0 < d ∧ d dvd n ∧ squarefree d} = {d. 0 < d ∧ d dvd rad n}`

lemma key_step2:

```  0 < n
==> setsum mu {d. 0 < d ∧ d dvd n ∧ squarefree d} +
setsum mu {d. 0 < d ∧ d dvd n ∧ ¬ squarefree d} =
setsum mu {d. 0 < d ∧ d dvd rad n}```

lemma zdvd_subsets_prop1:

```  {d. 0 < d ∧ d dvd m} =
{d. 0 < d ∧ d dvd m ∧ p dvd d} ∪ {d. 0 < d ∧ d dvd m ∧ ¬ p dvd d}```

lemma zdvd_subsets_prop2:

`  {d. 0 < d ∧ d dvd m ∧ p dvd d} ∩ {d. 0 < d ∧ d dvd m ∧ ¬ p dvd d} = {}`

lemma subset1_finite:

`  0 < m ==> finite {d. 0 < d ∧ d dvd m ∧ p dvd d}`

lemma subset2_finite:

`  0 < m ==> finite {d. 0 < d ∧ d dvd m ∧ ¬ p dvd d}`

lemma key_step3:

```  0 < m
==> setsum mu {d. 0 < d ∧ d dvd m} =
setsum mu {d. 0 < d ∧ d dvd m ∧ p dvd d} +
setsum mu {d. 0 < d ∧ d dvd m ∧ ¬ p dvd d}```

lemma aux_inject_prop:

`  p ∈ zprime ==> inj_on (%x. x * p) {d. 0 < d ∧ d dvd m div p}`

lemma aux_finite_prop:

`  [| p ∈ zprime; 0 < m; p dvd m |] ==> finite {d. 0 < d ∧ d dvd m div p}`

lemma aux_image_prop:

```  [| p ∈ zprime; p dvd m |]
==> (%x. x * p) ` {d. 0 < d ∧ d dvd m div p} = {d. 0 < d ∧ d dvd m ∧ p dvd d}```

lemma aux3:

```  [| p ∈ zprime; 0 < m; p dvd m |]
==> setsum mu {d. 0 < d ∧ d dvd m ∧ p dvd d} =
setsum (mu ˆ (%x. x * p)) {d. 0 < d ∧ d dvd m div p}```

lemma aux4:

```  [| p ∈ zprime; 0 < m; p dvd m; squarefree m |]
==> ∀x∈{d. 0 < d ∧ d dvd m div p}. (mu ˆ (%x. x * p)) x = (uminus ˆ mu) x```

lemma aux5:

```  [| p ∈ zprime; 0 < m; p dvd m; squarefree m |]
==> setsum (mu ˆ (%x. x * p)) {d. 0 < d ∧ d dvd m div p} =
setsum (uminus ˆ mu) {d. 0 < d ∧ d dvd m div p}```

lemma aux6:

```  [| p ∈ zprime; 0 < m; p dvd m; squarefree m |]
==> {d. 0 < d ∧ d dvd m ∧ ¬ p dvd d} = {d. 0 < d ∧ d dvd m div p}```

lemma aux7:

```  [| p ∈ zprime; 0 < m; p dvd m; squarefree m |]
==> setsum mu {d. 0 < d ∧ d dvd m ∧ ¬ p dvd d} =
setsum mu {d. 0 < d ∧ d dvd m div p}```

lemma key_step4:

```  [| p ∈ zprime; 0 < m; p dvd m; squarefree m |]
==> setsum mu {d. 0 < d ∧ d dvd m ∧ p dvd d} +
setsum mu {d. 0 < d ∧ d dvd m ∧ ¬ p dvd d} =
setsum (uminus ˆ mu) {d. 0 < d ∧ d dvd m div p} +
setsum mu {d. 0 < d ∧ d dvd m div p}```

lemma key_step5:

```  [| p ∈ zprime; 0 < m; p dvd m |]
==> setsum (uminus ˆ mu) {d. 0 < d ∧ d dvd m div p} +
setsum mu {d. 0 < d ∧ d dvd m div p} =
0```

theorem moebius_prop:

`  1 ≤ n ==> setsum mu {d. 0 < d ∧ d dvd n} = (if n = 1 then 1 else 0)`