Theory Mu

(*  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)");
  apply (auto simp add:  mem_pdivisors_dvd_rad zprimel_def);
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 (auto simp add: rad_zdvd);
  apply (subgoal_tac "0 < rad n");
  apply (subgoal_tac "squarefree (rad n)");
  apply (frule_tac n = "rad n" in squarefree_zdvd_impl_squarefree);
  apply (auto simp add: rad_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";
    by (auto simp add: not_squarefree_setsum_prop zdvd_squarefree_eq_zdvd_rad);
  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;