[STATEMENT]
lemma dirichlet_inverse_cong [cong]:
  assumes "\<And>n. n > 0 \<Longrightarrow> f n = f' n" "i = i'" "n = n'"
  shows   "dirichlet_inverse f i n = dirichlet_inverse f' i' n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dirichlet_inverse f i n = dirichlet_inverse f' i' n'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dirichlet_inverse f i n = dirichlet_inverse f' i' n'
[PROOF STEP]
have "dirichlet_inverse f i n = dirichlet_inverse f' i n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dirichlet_inverse f i n = dirichlet_inverse f' i n
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
0 < ?n \<Longrightarrow> f ?n = f' ?n

goal (1 subgoal):
 1. dirichlet_inverse f i n = dirichlet_inverse f' i n
[PROOF STEP]
proof (induction n rule: dirichlet_inverse_induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. (\<And>n. 0 < n \<Longrightarrow> f n = f' n) \<Longrightarrow> dirichlet_inverse f i 0 = dirichlet_inverse f' i 0
 2. (\<And>n. 0 < n \<Longrightarrow> f n = f' n) \<Longrightarrow> dirichlet_inverse f i (Suc 0) = dirichlet_inverse f' i (Suc 0)
 3. \<And>n. \<lbrakk>1 < n; \<And>k. \<lbrakk>k < n; \<And>n. 0 < n \<Longrightarrow> f n = f' n\<rbrakk> \<Longrightarrow> dirichlet_inverse f i k = dirichlet_inverse f' i k; \<And>n. 0 < n \<Longrightarrow> f n = f' n\<rbrakk> \<Longrightarrow> dirichlet_inverse f i n = dirichlet_inverse f' i n
[PROOF STEP]
case (gt1 n)
[PROOF STATE]
proof (state)
this:
1 < n
\<lbrakk>?k < n; \<And>n. 0 < n \<Longrightarrow> f n = f' n\<rbrakk> \<Longrightarrow> dirichlet_inverse f i ?k = dirichlet_inverse f' i ?k
0 < ?n \<Longrightarrow> f ?n = f' ?n

goal (3 subgoals):
 1. (\<And>n. 0 < n \<Longrightarrow> f n = f' n) \<Longrightarrow> dirichlet_inverse f i 0 = dirichlet_inverse f' i 0
 2. (\<And>n. 0 < n \<Longrightarrow> f n = f' n) \<Longrightarrow> dirichlet_inverse f i (Suc 0) = dirichlet_inverse f' i (Suc 0)
 3. \<And>n. \<lbrakk>1 < n; \<And>k. \<lbrakk>k < n; \<And>n. 0 < n \<Longrightarrow> f n = f' n\<rbrakk> \<Longrightarrow> dirichlet_inverse f i k = dirichlet_inverse f' i k; \<And>n. 0 < n \<Longrightarrow> f n = f' n\<rbrakk> \<Longrightarrow> dirichlet_inverse f i n = dirichlet_inverse f' i n
[PROOF STEP]
have *: "dirichlet_inverse f i k = dirichlet_inverse f' i k" if "k dvd n \<and> k < n" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dirichlet_inverse f i k = dirichlet_inverse f' i k
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
k dvd n \<and> k < n

goal (1 subgoal):
 1. dirichlet_inverse f i k = dirichlet_inverse f' i k
[PROOF STEP]
by (intro gt1) auto
[PROOF STATE]
proof (state)
this:
?k dvd n \<and> ?k < n \<Longrightarrow> dirichlet_inverse f i ?k = dirichlet_inverse f' i ?k

goal (3 subgoals):
 1. (\<And>n. 0 < n \<Longrightarrow> f n = f' n) \<Longrightarrow> dirichlet_inverse f i 0 = dirichlet_inverse f' i 0
 2. (\<And>n. 0 < n \<Longrightarrow> f n = f' n) \<Longrightarrow> dirichlet_inverse f i (Suc 0) = dirichlet_inverse f' i (Suc 0)
 3. \<And>n. \<lbrakk>1 < n; \<And>k. \<lbrakk>k < n; \<And>n. 0 < n \<Longrightarrow> f n = f' n\<rbrakk> \<Longrightarrow> dirichlet_inverse f i k = dirichlet_inverse f' i k; \<And>n. 0 < n \<Longrightarrow> f n = f' n\<rbrakk> \<Longrightarrow> dirichlet_inverse f i n = dirichlet_inverse f' i n
[PROOF STEP]
have *: "(\<Sum>d | d dvd n \<and> d < n. f (n div d) * dirichlet_inverse f i d) =
               (\<Sum>d | d dvd n \<and> d < n. f' (n div d) * dirichlet_inverse f' i d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>d | d dvd n \<and> d < n. f (n div d) * dirichlet_inverse f i d) = (\<Sum>d | d dvd n \<and> d < n. f' (n div d) * dirichlet_inverse f' i d)
[PROOF STEP]
by (intro sum.cong refl) (subst gt1.prems, auto elim: dvdE simp: *)
[PROOF STATE]
proof (state)
this:
(\<Sum>d | d dvd n \<and> d < n. f (n div d) * dirichlet_inverse f i d) = (\<Sum>d | d dvd n \<and> d < n. f' (n div d) * dirichlet_inverse f' i d)

goal (3 subgoals):
 1. (\<And>n. 0 < n \<Longrightarrow> f n = f' n) \<Longrightarrow> dirichlet_inverse f i 0 = dirichlet_inverse f' i 0
 2. (\<And>n. 0 < n \<Longrightarrow> f n = f' n) \<Longrightarrow> dirichlet_inverse f i (Suc 0) = dirichlet_inverse f' i (Suc 0)
 3. \<And>n. \<lbrakk>1 < n; \<And>k. \<lbrakk>k < n; \<And>n. 0 < n \<Longrightarrow> f n = f' n\<rbrakk> \<Longrightarrow> dirichlet_inverse f i k = dirichlet_inverse f' i k; \<And>n. 0 < n \<Longrightarrow> f n = f' n\<rbrakk> \<Longrightarrow> dirichlet_inverse f i n = dirichlet_inverse f' i n
[PROOF STEP]
consider "n = 0" | "n = 1" | "n > 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n = 0 \<Longrightarrow> thesis; n = 1 \<Longrightarrow> thesis; 1 < n \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<lbrakk>n = 0 \<Longrightarrow> ?thesis; n = 1 \<Longrightarrow> ?thesis; 1 < n \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (3 subgoals):
 1. (\<And>n. 0 < n \<Longrightarrow> f n = f' n) \<Longrightarrow> dirichlet_inverse f i 0 = dirichlet_inverse f' i 0
 2. (\<And>n. 0 < n \<Longrightarrow> f n = f' n) \<Longrightarrow> dirichlet_inverse f i (Suc 0) = dirichlet_inverse f' i (Suc 0)
 3. \<And>n. \<lbrakk>1 < n; \<And>k. \<lbrakk>k < n; \<And>n. 0 < n \<Longrightarrow> f n = f' n\<rbrakk> \<Longrightarrow> dirichlet_inverse f i k = dirichlet_inverse f' i k; \<And>n. 0 < n \<Longrightarrow> f n = f' n\<rbrakk> \<Longrightarrow> dirichlet_inverse f i n = dirichlet_inverse f' i n
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>n = 0 \<Longrightarrow> ?thesis; n = 1 \<Longrightarrow> ?thesis; 1 < n \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. dirichlet_inverse f i n = dirichlet_inverse f' i n
[PROOF STEP]
by cases (insert *, simp_all add: dirichlet_inverse_gt_1 * cong: sum.cong)
[PROOF STATE]
proof (state)
this:
dirichlet_inverse f i n = dirichlet_inverse f' i n

goal (2 subgoals):
 1. (\<And>n. 0 < n \<Longrightarrow> f n = f' n) \<Longrightarrow> dirichlet_inverse f i 0 = dirichlet_inverse f' i 0
 2. (\<And>n. 0 < n \<Longrightarrow> f n = f' n) \<Longrightarrow> dirichlet_inverse f i (Suc 0) = dirichlet_inverse f' i (Suc 0)
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
dirichlet_inverse f i n = dirichlet_inverse f' i n

goal (1 subgoal):
 1. dirichlet_inverse f i n = dirichlet_inverse f' i' n'
[PROOF STEP]
with assms(2,3)
[PROOF STATE]
proof (chain)
picking this:
i = i'
n = n'
dirichlet_inverse f i n = dirichlet_inverse f' i n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i = i'
n = n'
dirichlet_inverse f i n = dirichlet_inverse f' i n

goal (1 subgoal):
 1. dirichlet_inverse f i n = dirichlet_inverse f' i' n'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dirichlet_inverse f i n = dirichlet_inverse f' i' n'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dirichlet_inverse_gt_1':
  assumes "n > 1"
  shows   "dirichlet_inverse f i n =
             -i * dirichlet_prod (\<lambda>n. if n = 1 then 0 else f n) (dirichlet_inverse f i) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dirichlet_inverse f i n = - i * dirichlet_prod (\<lambda>n. if n = 1 then 0::'a else f n) (dirichlet_inverse f i) n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dirichlet_inverse f i n = - i * dirichlet_prod (\<lambda>n. if n = 1 then 0::'a else f n) (dirichlet_inverse f i) n
[PROOF STEP]
have "dirichlet_prod (\<lambda>n. if n = 1 then 0 else f n) (dirichlet_inverse f i) n =
          (\<Sum>d | d dvd n. (if n div d = Suc 0 then 0 else f (n div d)) * dirichlet_inverse f i d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dirichlet_prod (\<lambda>n. if n = 1 then 0::'a else f n) (dirichlet_inverse f i) n = (\<Sum>d | d dvd n. (if n div d = Suc 0 then 0::'a else f (n div d)) * dirichlet_inverse f i d)
[PROOF STEP]
by (simp add: dirichlet_prod_altdef1)
[PROOF STATE]
proof (state)
this:
dirichlet_prod (\<lambda>n. if n = 1 then 0::'a else f n) (dirichlet_inverse f i) n = (\<Sum>d | d dvd n. (if n div d = Suc 0 then 0::'a else f (n div d)) * dirichlet_inverse f i d)

goal (1 subgoal):
 1. dirichlet_inverse f i n = - i * dirichlet_prod (\<lambda>n. if n = 1 then 0::'a else f n) (dirichlet_inverse f i) n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dirichlet_prod (\<lambda>n. if n = 1 then 0::'a else f n) (dirichlet_inverse f i) n = (\<Sum>d | d dvd n. (if n div d = Suc 0 then 0::'a else f (n div d)) * dirichlet_inverse f i d)

goal (1 subgoal):
 1. dirichlet_inverse f i n = - i * dirichlet_prod (\<lambda>n. if n = 1 then 0::'a else f n) (dirichlet_inverse f i) n
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
1 < n
[PROOF STEP]
have "\<dots> = (\<Sum>d | d dvd n \<and> d \<noteq> n. f (n div d) * dirichlet_inverse f i d)"
[PROOF STATE]
proof (prove)
using this:
1 < n

goal (1 subgoal):
 1. (\<Sum>d | d dvd n. (if n div d = Suc 0 then 0::'a else f (n div d)) * dirichlet_inverse f i d) = (\<Sum>d | d dvd n \<and> d \<noteq> n. f (n div d) * dirichlet_inverse f i d)
[PROOF STEP]
by (intro sum.mono_neutral_cong_right) (auto elim: dvdE)
[PROOF STATE]
proof (state)
this:
(\<Sum>d | d dvd n. (if n div d = Suc 0 then 0::'a else f (n div d)) * dirichlet_inverse f i d) = (\<Sum>d | d dvd n \<and> d \<noteq> n. f (n div d) * dirichlet_inverse f i d)

goal (1 subgoal):
 1. dirichlet_inverse f i n = - i * dirichlet_prod (\<lambda>n. if n = 1 then 0::'a else f n) (dirichlet_inverse f i) n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>d | d dvd n. (if n div d = Suc 0 then 0::'a else f (n div d)) * dirichlet_inverse f i d) = (\<Sum>d | d dvd n \<and> d \<noteq> n. f (n div d) * dirichlet_inverse f i d)

goal (1 subgoal):
 1. dirichlet_inverse f i n = - i * dirichlet_prod (\<lambda>n. if n = 1 then 0::'a else f n) (dirichlet_inverse f i) n
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
1 < n
[PROOF STEP]
have "{d. d dvd n \<and> d \<noteq> n} = {d. d dvd n \<and> d < n}"
[PROOF STATE]
proof (prove)
using this:
1 < n

goal (1 subgoal):
 1. {d. d dvd n \<and> d \<noteq> n} = {d. d dvd n \<and> d < n}
[PROOF STEP]
by (auto dest: dvd_imp_le)
[PROOF STATE]
proof (state)
this:
{d. d dvd n \<and> d \<noteq> n} = {d. d dvd n \<and> d < n}

goal (1 subgoal):
 1. dirichlet_inverse f i n = - i * dirichlet_prod (\<lambda>n. if n = 1 then 0::'a else f n) (dirichlet_inverse f i) n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{d. d dvd n \<and> d \<noteq> n} = {d. d dvd n \<and> d < n}

goal (1 subgoal):
 1. dirichlet_inverse f i n = - i * dirichlet_prod (\<lambda>n. if n = 1 then 0::'a else f n) (dirichlet_inverse f i) n
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
1 < n
[PROOF STEP]
have "-i * (\<Sum>d\<in>\<dots>. f (n div d) * dirichlet_inverse f i d) =
                          dirichlet_inverse f i n"
[PROOF STATE]
proof (prove)
using this:
1 < n

goal (1 subgoal):
 1. - i * (\<Sum>d | d dvd n \<and> d < n. f (n div d) * dirichlet_inverse f i d) = dirichlet_inverse f i n
[PROOF STEP]
by (simp add: dirichlet_inverse_gt_1)
[PROOF STATE]
proof (state)
this:
- i * (\<Sum>d | d dvd n \<and> d < n. f (n div d) * dirichlet_inverse f i d) = dirichlet_inverse f i n

goal (1 subgoal):
 1. dirichlet_inverse f i n = - i * dirichlet_prod (\<lambda>n. if n = 1 then 0::'a else f n) (dirichlet_inverse f i) n
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
- i * dirichlet_prod (\<lambda>n. if n = 1 then 0::'a else f n) (dirichlet_inverse f i) n = dirichlet_inverse f i n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
- i * dirichlet_prod (\<lambda>n. if n = 1 then 0::'a else f n) (dirichlet_inverse f i) n = dirichlet_inverse f i n

goal (1 subgoal):
 1. dirichlet_inverse f i n = - i * dirichlet_prod (\<lambda>n. if n = 1 then 0::'a else f n) (dirichlet_inverse f i) n
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
dirichlet_inverse f i n = - i * dirichlet_prod (\<lambda>n. if n = 1 then 0::'a else f n) (dirichlet_inverse f i) n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma of_int_dirichlet_prod:
  "of_int (dirichlet_prod f g n) = dirichlet_prod (\<lambda>n. of_int (f n)) (\<lambda>n. of_int (g n)) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int (dirichlet_prod f g n) = dirichlet_prod (\<lambda>n. of_int (f n)) (\<lambda>n. of_int (g n)) n
[PROOF STEP]
by (simp add: dirichlet_prod_def)


[STATEMENT]
lemma of_int_dirichlet_inverse:
  "of_int (dirichlet_inverse f i n) = dirichlet_inverse (\<lambda>n. of_int (f n)) (of_int i) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int (dirichlet_inverse f i n) = dirichlet_inverse (\<lambda>n. of_int (f n)) (of_int i) n
[PROOF STEP]
proof (induction n rule: dirichlet_inverse_induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. of_int (dirichlet_inverse f i 0) = dirichlet_inverse (\<lambda>n. of_int (f n)) (of_int i) 0
 2. of_int (dirichlet_inverse f i (Suc 0)) = dirichlet_inverse (\<lambda>n. of_int (f n)) (of_int i) (Suc 0)
 3. \<And>n. \<lbrakk>1 < n; \<And>k. k < n \<Longrightarrow> of_int (dirichlet_inverse f i k) = dirichlet_inverse (\<lambda>n. of_int (f n)) (of_int i) k\<rbrakk> \<Longrightarrow> of_int (dirichlet_inverse f i n) = dirichlet_inverse (\<lambda>n. of_int (f n)) (of_int i) n
[PROOF STEP]
case (gt1 n)
[PROOF STATE]
proof (state)
this:
1 < n
?k < n \<Longrightarrow> of_int (dirichlet_inverse f i ?k) = dirichlet_inverse (\<lambda>n. of_int (f n)) (of_int i) ?k

goal (3 subgoals):
 1. of_int (dirichlet_inverse f i 0) = dirichlet_inverse (\<lambda>n. of_int (f n)) (of_int i) 0
 2. of_int (dirichlet_inverse f i (Suc 0)) = dirichlet_inverse (\<lambda>n. of_int (f n)) (of_int i) (Suc 0)
 3. \<And>n. \<lbrakk>1 < n; \<And>k. k < n \<Longrightarrow> of_int (dirichlet_inverse f i k) = dirichlet_inverse (\<lambda>n. of_int (f n)) (of_int i) k\<rbrakk> \<Longrightarrow> of_int (dirichlet_inverse f i n) = dirichlet_inverse (\<lambda>n. of_int (f n)) (of_int i) n
[PROOF STEP]
from gt1
[PROOF STATE]
proof (chain)
picking this:
1 < n
?k < n \<Longrightarrow> of_int (dirichlet_inverse f i ?k) = dirichlet_inverse (\<lambda>n. of_int (f n)) (of_int i) ?k
[PROOF STEP]
have "(of_int (dirichlet_inverse f i n) :: 'a) =
    - (of_int i * (\<Sum>d | d dvd n \<and> d < n. of_int (f (n div d) * dirichlet_inverse f i d)))"
     (is "_ = - (_ * ?A)")
[PROOF STATE]
proof (prove)
using this:
1 < n
?k < n \<Longrightarrow> of_int (dirichlet_inverse f i ?k) = dirichlet_inverse (\<lambda>n. of_int (f n)) (of_int i) ?k

goal (1 subgoal):
 1. of_int (dirichlet_inverse f i n) = - (of_int i * (\<Sum>d | d dvd n \<and> d < n. of_int (f (n div d) * dirichlet_inverse f i d)))
[PROOF STEP]
by (simp add: dirichlet_inverse_gt_1 of_int_dirichlet_prod)
[PROOF STATE]
proof (state)
this:
of_int (dirichlet_inverse f i n) = - (of_int i * (\<Sum>d | d dvd n \<and> d < n. of_int (f (n div d) * dirichlet_inverse f i d)))

goal (3 subgoals):
 1. of_int (dirichlet_inverse f i 0) = dirichlet_inverse (\<lambda>n. of_int (f n)) (of_int i) 0
 2. of_int (dirichlet_inverse f i (Suc 0)) = dirichlet_inverse (\<lambda>n. of_int (f n)) (of_int i) (Suc 0)
 3. \<And>n. \<lbrakk>1 < n; \<And>k. k < n \<Longrightarrow> of_int (dirichlet_inverse f i k) = dirichlet_inverse (\<lambda>n. of_int (f n)) (of_int i) k\<rbrakk> \<Longrightarrow> of_int (dirichlet_inverse f i n) = dirichlet_inverse (\<lambda>n. of_int (f n)) (of_int i) n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
of_int (dirichlet_inverse f i n) = - (of_int i * (\<Sum>d | d dvd n \<and> d < n. of_int (f (n div d) * dirichlet_inverse f i d)))

goal (3 subgoals):
 1. of_int (dirichlet_inverse f i 0) = dirichlet_inverse (\<lambda>n. of_int (f n)) (of_int i) 0
 2. of_int (dirichlet_inverse f i (Suc 0)) = dirichlet_inverse (\<lambda>n. of_int (f n)) (of_int i) (Suc 0)
 3. \<And>n. \<lbrakk>1 < n; \<And>k. k < n \<Longrightarrow> of_int (dirichlet_inverse f i k) = dirichlet_inverse (\<lambda>n. of_int (f n)) (of_int i) k\<rbrakk> \<Longrightarrow> of_int (dirichlet_inverse f i n) = dirichlet_inverse (\<lambda>n. of_int (f n)) (of_int i) n
[PROOF STEP]
have "?A = (\<Sum>d | d dvd n \<and> d < n. of_int (f (n div d)) *
                  dirichlet_inverse (\<lambda>n. of_int (f n)) (of_int i) d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>d | d dvd n \<and> d < n. of_int (f (n div d) * dirichlet_inverse f i d)) = (\<Sum>d | d dvd n \<and> d < n. of_int (f (n div d)) * dirichlet_inverse (\<lambda>n. of_int (f n)) (of_int i) d)
[PROOF STEP]
by (intro sum.cong refl) (auto simp: gt1)
[PROOF STATE]
proof (state)
this:
(\<Sum>d | d dvd n \<and> d < n. of_int (f (n div d) * dirichlet_inverse f i d)) = (\<Sum>d | d dvd n \<and> d < n. of_int (f (n div d)) * dirichlet_inverse (\<lambda>n. of_int (f n)) (of_int i) d)

goal (3 subgoals):
 1. of_int (dirichlet_inverse f i 0) = dirichlet_inverse (\<lambda>n. of_int (f n)) (of_int i) 0
 2. of_int (dirichlet_inverse f i (Suc 0)) = dirichlet_inverse (\<lambda>n. of_int (f n)) (of_int i) (Suc 0)
 3. \<And>n. \<lbrakk>1 < n; \<And>k. k < n \<Longrightarrow> of_int (dirichlet_inverse f i k) = dirichlet_inverse (\<lambda>n. of_int (f n)) (of_int i) k\<rbrakk> \<Longrightarrow> of_int (dirichlet_inverse f i n) = dirichlet_inverse (\<lambda>n. of_int (f n)) (of_int i) n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>d | d dvd n \<and> d < n. of_int (f (n div d) * dirichlet_inverse f i d)) = (\<Sum>d | d dvd n \<and> d < n. of_int (f (n div d)) * dirichlet_inverse (\<lambda>n. of_int (f n)) (of_int i) d)

goal (3 subgoals):
 1. of_int (dirichlet_inverse f i 0) = dirichlet_inverse (\<lambda>n. of_int (f n)) (of_int i) 0
 2. of_int (dirichlet_inverse f i (Suc 0)) = dirichlet_inverse (\<lambda>n. of_int (f n)) (of_int i) (Suc 0)
 3. \<And>n. \<lbrakk>1 < n; \<And>k. k < n \<Longrightarrow> of_int (dirichlet_inverse f i k) = dirichlet_inverse (\<lambda>n. of_int (f n)) (of_int i) k\<rbrakk> \<Longrightarrow> of_int (dirichlet_inverse f i n) = dirichlet_inverse (\<lambda>n. of_int (f n)) (of_int i) n
[PROOF STEP]
have "-(of_int i * \<dots>) = dirichlet_inverse (\<lambda>n. of_int (f n)) (of_int i) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - (of_int i * (\<Sum>d | d dvd n \<and> d < n. of_int (f (n div d)) * dirichlet_inverse (\<lambda>n. of_int (f n)) (of_int i) d)) = dirichlet_inverse (\<lambda>n. of_int (f n)) (of_int i) n
[PROOF STEP]
using gt1.hyps
[PROOF STATE]
proof (prove)
using this:
1 < n

goal (1 subgoal):
 1. - (of_int i * (\<Sum>d | d dvd n \<and> d < n. of_int (f (n div d)) * dirichlet_inverse (\<lambda>n. of_int (f n)) (of_int i) d)) = dirichlet_inverse (\<lambda>n. of_int (f n)) (of_int i) n
[PROOF STEP]
by (simp add: dirichlet_inverse_gt_1)
[PROOF STATE]
proof (state)
this:
- (of_int i * (\<Sum>d | d dvd n \<and> d < n. of_int (f (n div d)) * dirichlet_inverse (\<lambda>n. of_int (f n)) (of_int i) d)) = dirichlet_inverse (\<lambda>n. of_int (f n)) (of_int i) n

goal (3 subgoals):
 1. of_int (dirichlet_inverse f i 0) = dirichlet_inverse (\<lambda>n. of_int (f n)) (of_int i) 0
 2. of_int (dirichlet_inverse f i (Suc 0)) = dirichlet_inverse (\<lambda>n. of_int (f n)) (of_int i) (Suc 0)
 3. \<And>n. \<lbrakk>1 < n; \<And>k. k < n \<Longrightarrow> of_int (dirichlet_inverse f i k) = dirichlet_inverse (\<lambda>n. of_int (f n)) (of_int i) k\<rbrakk> \<Longrightarrow> of_int (dirichlet_inverse f i n) = dirichlet_inverse (\<lambda>n. of_int (f n)) (of_int i) n
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
of_int (dirichlet_inverse f i n) = dirichlet_inverse (\<lambda>n. of_int (f n)) (of_int i) n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
of_int (dirichlet_inverse f i n) = dirichlet_inverse (\<lambda>n. of_int (f n)) (of_int i) n

goal (1 subgoal):
 1. of_int (dirichlet_inverse f i n) = dirichlet_inverse (\<lambda>n. of_int (f n)) (of_int i) n
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
of_int (dirichlet_inverse f i n) = dirichlet_inverse (\<lambda>n. of_int (f n)) (of_int i) n

goal (2 subgoals):
 1. of_int (dirichlet_inverse f i 0) = dirichlet_inverse (\<lambda>n. of_int (f n)) (of_int i) 0
 2. of_int (dirichlet_inverse f i (Suc 0)) = dirichlet_inverse (\<lambda>n. of_int (f n)) (of_int i) (Suc 0)
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma dirichlet_inverse_code [code]:
  "dirichlet_inverse f i n = (if n = 0 then 0 else if n = 1 then i else
     -i * fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f (n div d) *
     dirichlet_inverse f i d + acc else acc) 1 (n - 1) 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dirichlet_inverse f i n = (if n = 0 then 0::'a else if n = 1 then i else - i * fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f (n div d) * dirichlet_inverse f i d + acc else acc) 1 (n - 1) (0::'a))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dirichlet_inverse f i n = (if n = 0 then 0::'a else if n = 1 then i else - i * fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f (n div d) * dirichlet_inverse f i d + acc else acc) 1 (n - 1) (0::'a))
[PROOF STEP]
consider "n = 0" | "n = 1" | "n > 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n = 0 \<Longrightarrow> thesis; n = 1 \<Longrightarrow> thesis; 1 < n \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<lbrakk>n = 0 \<Longrightarrow> ?thesis; n = 1 \<Longrightarrow> ?thesis; 1 < n \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. dirichlet_inverse f i n = (if n = 0 then 0::'a else if n = 1 then i else - i * fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f (n div d) * dirichlet_inverse f i d + acc else acc) 1 (n - 1) (0::'a))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>n = 0 \<Longrightarrow> ?thesis; n = 1 \<Longrightarrow> ?thesis; 1 < n \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. dirichlet_inverse f i n = (if n = 0 then 0::'a else if n = 1 then i else - i * fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f (n div d) * dirichlet_inverse f i d + acc else acc) 1 (n - 1) (0::'a))
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. n = 0 \<Longrightarrow> dirichlet_inverse f i n = (if n = 0 then 0::'a else if n = 1 then i else - i * fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f (n div d) * dirichlet_inverse f i d + acc else acc) 1 (n - 1) (0::'a))
 2. n = 1 \<Longrightarrow> dirichlet_inverse f i n = (if n = 0 then 0::'a else if n = 1 then i else - i * fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f (n div d) * dirichlet_inverse f i d + acc else acc) 1 (n - 1) (0::'a))
 3. 1 < n \<Longrightarrow> dirichlet_inverse f i n = (if n = 0 then 0::'a else if n = 1 then i else - i * fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f (n div d) * dirichlet_inverse f i d + acc else acc) 1 (n - 1) (0::'a))
[PROOF STEP]
assume n: "n > 1"
[PROOF STATE]
proof (state)
this:
1 < n

goal (3 subgoals):
 1. n = 0 \<Longrightarrow> dirichlet_inverse f i n = (if n = 0 then 0::'a else if n = 1 then i else - i * fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f (n div d) * dirichlet_inverse f i d + acc else acc) 1 (n - 1) (0::'a))
 2. n = 1 \<Longrightarrow> dirichlet_inverse f i n = (if n = 0 then 0::'a else if n = 1 then i else - i * fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f (n div d) * dirichlet_inverse f i d + acc else acc) 1 (n - 1) (0::'a))
 3. 1 < n \<Longrightarrow> dirichlet_inverse f i n = (if n = 0 then 0::'a else if n = 1 then i else - i * fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f (n div d) * dirichlet_inverse f i d + acc else acc) 1 (n - 1) (0::'a))
[PROOF STEP]
have *: "(\<lambda>d acc. if d dvd n then f (n div d) * dirichlet_inverse f i d + acc else acc) =
               (\<lambda>d acc. (if d dvd n then f (n div d) * dirichlet_inverse f i d else 0) + acc)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>d acc. if d dvd n then f (n div d) * dirichlet_inverse f i d + acc else acc) = (\<lambda>d. (+) (if d dvd n then f (n div d) * dirichlet_inverse f i d else (0::'a)))
[PROOF STEP]
by (simp add: fun_eq_iff)
[PROOF STATE]
proof (state)
this:
(\<lambda>d acc. if d dvd n then f (n div d) * dirichlet_inverse f i d + acc else acc) = (\<lambda>d. (+) (if d dvd n then f (n div d) * dirichlet_inverse f i d else (0::'a)))

goal (3 subgoals):
 1. n = 0 \<Longrightarrow> dirichlet_inverse f i n = (if n = 0 then 0::'a else if n = 1 then i else - i * fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f (n div d) * dirichlet_inverse f i d + acc else acc) 1 (n - 1) (0::'a))
 2. n = 1 \<Longrightarrow> dirichlet_inverse f i n = (if n = 0 then 0::'a else if n = 1 then i else - i * fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f (n div d) * dirichlet_inverse f i d + acc else acc) 1 (n - 1) (0::'a))
 3. 1 < n \<Longrightarrow> dirichlet_inverse f i n = (if n = 0 then 0::'a else if n = 1 then i else - i * fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f (n div d) * dirichlet_inverse f i d + acc else acc) 1 (n - 1) (0::'a))
[PROOF STEP]
have "fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f (n div d) *
            dirichlet_inverse f i d + acc else acc) 1 (n - 1) 0 =
            (\<Sum>d = 1..n - 1. if d dvd n then f (n div d) * dirichlet_inverse f i d else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f (n div d) * dirichlet_inverse f i d + acc else acc) 1 (n - 1) (0::'a) = (\<Sum>d = 1..n - 1. if d dvd n then f (n div d) * dirichlet_inverse f i d else (0::'a))
[PROOF STEP]
by (subst *, subst sum_atLeastAtMost_code [symmetric]) simp
[PROOF STATE]
proof (state)
this:
fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f (n div d) * dirichlet_inverse f i d + acc else acc) 1 (n - 1) (0::'a) = (\<Sum>d = 1..n - 1. if d dvd n then f (n div d) * dirichlet_inverse f i d else (0::'a))

goal (3 subgoals):
 1. n = 0 \<Longrightarrow> dirichlet_inverse f i n = (if n = 0 then 0::'a else if n = 1 then i else - i * fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f (n div d) * dirichlet_inverse f i d + acc else acc) 1 (n - 1) (0::'a))
 2. n = 1 \<Longrightarrow> dirichlet_inverse f i n = (if n = 0 then 0::'a else if n = 1 then i else - i * fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f (n div d) * dirichlet_inverse f i d + acc else acc) 1 (n - 1) (0::'a))
 3. 1 < n \<Longrightarrow> dirichlet_inverse f i n = (if n = 0 then 0::'a else if n = 1 then i else - i * fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f (n div d) * dirichlet_inverse f i d + acc else acc) 1 (n - 1) (0::'a))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f (n div d) * dirichlet_inverse f i d + acc else acc) 1 (n - 1) (0::'a) = (\<Sum>d = 1..n - 1. if d dvd n then f (n div d) * dirichlet_inverse f i d else (0::'a))

goal (3 subgoals):
 1. n = 0 \<Longrightarrow> dirichlet_inverse f i n = (if n = 0 then 0::'a else if n = 1 then i else - i * fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f (n div d) * dirichlet_inverse f i d + acc else acc) 1 (n - 1) (0::'a))
 2. n = 1 \<Longrightarrow> dirichlet_inverse f i n = (if n = 0 then 0::'a else if n = 1 then i else - i * fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f (n div d) * dirichlet_inverse f i d + acc else acc) 1 (n - 1) (0::'a))
 3. 1 < n \<Longrightarrow> dirichlet_inverse f i n = (if n = 0 then 0::'a else if n = 1 then i else - i * fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f (n div d) * dirichlet_inverse f i d + acc else acc) 1 (n - 1) (0::'a))
[PROOF STEP]
from n
[PROOF STATE]
proof (chain)
picking this:
1 < n
[PROOF STEP]
have "\<dots> = (\<Sum>d | d dvd n \<and> d < n. f (n div d) * dirichlet_inverse f i d)"
[PROOF STATE]
proof (prove)
using this:
1 < n

goal (1 subgoal):
 1. (\<Sum>d = 1..n - 1. if d dvd n then f (n div d) * dirichlet_inverse f i d else (0::'a)) = (\<Sum>d | d dvd n \<and> d < n. f (n div d) * dirichlet_inverse f i d)
[PROOF STEP]
by (intro sum.mono_neutral_cong_right; cases n)
         (auto dest: dvd_imp_le elim: dvdE simp: Suc_le_eq intro!: Nat.gr0I)
[PROOF STATE]
proof (state)
this:
(\<Sum>d = 1..n - 1. if d dvd n then f (n div d) * dirichlet_inverse f i d else (0::'a)) = (\<Sum>d | d dvd n \<and> d < n. f (n div d) * dirichlet_inverse f i d)

goal (3 subgoals):
 1. n = 0 \<Longrightarrow> dirichlet_inverse f i n = (if n = 0 then 0::'a else if n = 1 then i else - i * fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f (n div d) * dirichlet_inverse f i d + acc else acc) 1 (n - 1) (0::'a))
 2. n = 1 \<Longrightarrow> dirichlet_inverse f i n = (if n = 0 then 0::'a else if n = 1 then i else - i * fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f (n div d) * dirichlet_inverse f i d + acc else acc) 1 (n - 1) (0::'a))
 3. 1 < n \<Longrightarrow> dirichlet_inverse f i n = (if n = 0 then 0::'a else if n = 1 then i else - i * fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f (n div d) * dirichlet_inverse f i d + acc else acc) 1 (n - 1) (0::'a))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>d = 1..n - 1. if d dvd n then f (n div d) * dirichlet_inverse f i d else (0::'a)) = (\<Sum>d | d dvd n \<and> d < n. f (n div d) * dirichlet_inverse f i d)

goal (3 subgoals):
 1. n = 0 \<Longrightarrow> dirichlet_inverse f i n = (if n = 0 then 0::'a else if n = 1 then i else - i * fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f (n div d) * dirichlet_inverse f i d + acc else acc) 1 (n - 1) (0::'a))
 2. n = 1 \<Longrightarrow> dirichlet_inverse f i n = (if n = 0 then 0::'a else if n = 1 then i else - i * fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f (n div d) * dirichlet_inverse f i d + acc else acc) 1 (n - 1) (0::'a))
 3. 1 < n \<Longrightarrow> dirichlet_inverse f i n = (if n = 0 then 0::'a else if n = 1 then i else - i * fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f (n div d) * dirichlet_inverse f i d + acc else acc) 1 (n - 1) (0::'a))
[PROOF STEP]
from n
[PROOF STATE]
proof (chain)
picking this:
1 < n
[PROOF STEP]
have "-i * \<dots> = dirichlet_inverse f i n"
[PROOF STATE]
proof (prove)
using this:
1 < n

goal (1 subgoal):
 1. - i * (\<Sum>d | d dvd n \<and> d < n. f (n div d) * dirichlet_inverse f i d) = dirichlet_inverse f i n
[PROOF STEP]
by (simp add: dirichlet_inverse_gt_1)
[PROOF STATE]
proof (state)
this:
- i * (\<Sum>d | d dvd n \<and> d < n. f (n div d) * dirichlet_inverse f i d) = dirichlet_inverse f i n

goal (3 subgoals):
 1. n = 0 \<Longrightarrow> dirichlet_inverse f i n = (if n = 0 then 0::'a else if n = 1 then i else - i * fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f (n div d) * dirichlet_inverse f i d + acc else acc) 1 (n - 1) (0::'a))
 2. n = 1 \<Longrightarrow> dirichlet_inverse f i n = (if n = 0 then 0::'a else if n = 1 then i else - i * fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f (n div d) * dirichlet_inverse f i d + acc else acc) 1 (n - 1) (0::'a))
 3. 1 < n \<Longrightarrow> dirichlet_inverse f i n = (if n = 0 then 0::'a else if n = 1 then i else - i * fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f (n div d) * dirichlet_inverse f i d + acc else acc) 1 (n - 1) (0::'a))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
- i * fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f (n div d) * dirichlet_inverse f i d + acc else acc) 1 (n - 1) (0::'a) = dirichlet_inverse f i n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
- i * fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f (n div d) * dirichlet_inverse f i d + acc else acc) 1 (n - 1) (0::'a) = dirichlet_inverse f i n

goal (1 subgoal):
 1. dirichlet_inverse f i n = (if n = 0 then 0::'a else if n = 1 then i else - i * fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f (n div d) * dirichlet_inverse f i d + acc else acc) 1 (n - 1) (0::'a))
[PROOF STEP]
using n
[PROOF STATE]
proof (prove)
using this:
- i * fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f (n div d) * dirichlet_inverse f i d + acc else acc) 1 (n - 1) (0::'a) = dirichlet_inverse f i n
1 < n

goal (1 subgoal):
 1. dirichlet_inverse f i n = (if n = 0 then 0::'a else if n = 1 then i else - i * fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f (n div d) * dirichlet_inverse f i d + acc else acc) 1 (n - 1) (0::'a))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dirichlet_inverse f i n = (if n = 0 then 0::'a else if n = 1 then i else - i * fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f (n div d) * dirichlet_inverse f i d + acc else acc) 1 (n - 1) (0::'a))

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> dirichlet_inverse f i n = (if n = 0 then 0::'a else if n = 1 then i else - i * fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f (n div d) * dirichlet_inverse f i d + acc else acc) 1 (n - 1) (0::'a))
 2. n = 1 \<Longrightarrow> dirichlet_inverse f i n = (if n = 0 then 0::'a else if n = 1 then i else - i * fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f (n div d) * dirichlet_inverse f i d + acc else acc) 1 (n - 1) (0::'a))
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
dirichlet_inverse f i n = (if n = 0 then 0::'a else if n = 1 then i else - i * fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f (n div d) * dirichlet_inverse f i d + acc else acc) 1 (n - 1) (0::'a))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dirichlet_prod_inverse:
  assumes "f 1 * i = 1"
  shows   "dirichlet_prod f (dirichlet_inverse f i) = (\<lambda>n. if n = 1 then 1 else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dirichlet_prod f (dirichlet_inverse f i) = (\<lambda>n. if n = 1 then 1::'a else (0::'a))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
[PROOF STEP]
fix n :: nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
[PROOF STEP]
consider "n = 0" | "n = 1" | "n > 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n = 0 \<Longrightarrow> thesis; n = 1 \<Longrightarrow> thesis; 1 < n \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<lbrakk>n = 0 \<Longrightarrow> ?thesis; n = 1 \<Longrightarrow> ?thesis; 1 < n \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<And>n. dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
[PROOF STEP]
thus "dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1 else 0)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>n = 0 \<Longrightarrow> ?thesis; n = 1 \<Longrightarrow> ?thesis; 1 < n \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. n = 0 \<Longrightarrow> dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
 2. n = 1 \<Longrightarrow> dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
 3. 1 < n \<Longrightarrow> dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
[PROOF STEP]
assume n: "n > 1"
[PROOF STATE]
proof (state)
this:
1 < n

goal (3 subgoals):
 1. n = 0 \<Longrightarrow> dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
 2. n = 1 \<Longrightarrow> dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
 3. 1 < n \<Longrightarrow> dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
[PROOF STEP]
have fin: "finite {d. d dvd n \<and> d \<noteq> n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {d. d dvd n \<and> d \<noteq> n}
[PROOF STEP]
by (rule finite_subset[of _ "{d. d dvd n}"]) (insert n, auto)
[PROOF STATE]
proof (state)
this:
finite {d. d dvd n \<and> d \<noteq> n}

goal (3 subgoals):
 1. n = 0 \<Longrightarrow> dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
 2. n = 1 \<Longrightarrow> dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
 3. 1 < n \<Longrightarrow> dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
[PROOF STEP]
have "dirichlet_prod f (dirichlet_inverse f i) n =
            (\<Sum>d | d dvd n. f (n div d) * dirichlet_inverse f i d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dirichlet_prod f (dirichlet_inverse f i) n = (\<Sum>d | d dvd n. f (n div d) * dirichlet_inverse f i d)
[PROOF STEP]
by (simp add: dirichlet_prod_altdef1)
[PROOF STATE]
proof (state)
this:
dirichlet_prod f (dirichlet_inverse f i) n = (\<Sum>d | d dvd n. f (n div d) * dirichlet_inverse f i d)

goal (3 subgoals):
 1. n = 0 \<Longrightarrow> dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
 2. n = 1 \<Longrightarrow> dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
 3. 1 < n \<Longrightarrow> dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dirichlet_prod f (dirichlet_inverse f i) n = (\<Sum>d | d dvd n. f (n div d) * dirichlet_inverse f i d)

goal (3 subgoals):
 1. n = 0 \<Longrightarrow> dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
 2. n = 1 \<Longrightarrow> dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
 3. 1 < n \<Longrightarrow> dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
[PROOF STEP]
have "{d. d dvd n} = insert n {d. d dvd n \<and> d \<noteq> n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {d. d dvd n} = insert n {d. d dvd n \<and> d \<noteq> n}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{d. d dvd n} = insert n {d. d dvd n \<and> d \<noteq> n}

goal (3 subgoals):
 1. n = 0 \<Longrightarrow> dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
 2. n = 1 \<Longrightarrow> dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
 3. 1 < n \<Longrightarrow> dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{d. d dvd n} = insert n {d. d dvd n \<and> d \<noteq> n}

goal (3 subgoals):
 1. n = 0 \<Longrightarrow> dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
 2. n = 1 \<Longrightarrow> dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
 3. 1 < n \<Longrightarrow> dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
[PROOF STEP]
have "(\<Sum>d\<in>\<dots>. f (n div d) * dirichlet_inverse f i d) =
                 f 1 * dirichlet_inverse f i n +
                 (\<Sum>d | d dvd n \<and> d \<noteq> n. f (n div d) * dirichlet_inverse f i d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>d\<in>insert n {d. d dvd n \<and> d \<noteq> n}. f (n div d) * dirichlet_inverse f i d) = f 1 * dirichlet_inverse f i n + (\<Sum>d | d dvd n \<and> d \<noteq> n. f (n div d) * dirichlet_inverse f i d)
[PROOF STEP]
using fin n
[PROOF STATE]
proof (prove)
using this:
finite {d. d dvd n \<and> d \<noteq> n}
1 < n

goal (1 subgoal):
 1. (\<Sum>d\<in>insert n {d. d dvd n \<and> d \<noteq> n}. f (n div d) * dirichlet_inverse f i d) = f 1 * dirichlet_inverse f i n + (\<Sum>d | d dvd n \<and> d \<noteq> n. f (n div d) * dirichlet_inverse f i d)
[PROOF STEP]
by (subst sum.insert) auto
[PROOF STATE]
proof (state)
this:
(\<Sum>d\<in>insert n {d. d dvd n \<and> d \<noteq> n}. f (n div d) * dirichlet_inverse f i d) = f 1 * dirichlet_inverse f i n + (\<Sum>d | d dvd n \<and> d \<noteq> n. f (n div d) * dirichlet_inverse f i d)

goal (3 subgoals):
 1. n = 0 \<Longrightarrow> dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
 2. n = 1 \<Longrightarrow> dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
 3. 1 < n \<Longrightarrow> dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>d\<in>insert n {d. d dvd n \<and> d \<noteq> n}. f (n div d) * dirichlet_inverse f i d) = f 1 * dirichlet_inverse f i n + (\<Sum>d | d dvd n \<and> d \<noteq> n. f (n div d) * dirichlet_inverse f i d)

goal (3 subgoals):
 1. n = 0 \<Longrightarrow> dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
 2. n = 1 \<Longrightarrow> dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
 3. 1 < n \<Longrightarrow> dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
[PROOF STEP]
from n
[PROOF STATE]
proof (chain)
picking this:
1 < n
[PROOF STEP]
have "dirichlet_inverse f i n =
      - i * (\<Sum>d | d dvd n \<and> d < n. f (n div d) * dirichlet_inverse f i d)"
[PROOF STATE]
proof (prove)
using this:
1 < n

goal (1 subgoal):
 1. dirichlet_inverse f i n = - i * (\<Sum>d | d dvd n \<and> d < n. f (n div d) * dirichlet_inverse f i d)
[PROOF STEP]
by (subst dirichlet_inverse_gt_1) auto
[PROOF STATE]
proof (state)
this:
dirichlet_inverse f i n = - i * (\<Sum>d | d dvd n \<and> d < n. f (n div d) * dirichlet_inverse f i d)

goal (3 subgoals):
 1. n = 0 \<Longrightarrow> dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
 2. n = 1 \<Longrightarrow> dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
 3. 1 < n \<Longrightarrow> dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dirichlet_inverse f i n = - i * (\<Sum>d | d dvd n \<and> d < n. f (n div d) * dirichlet_inverse f i d)

goal (3 subgoals):
 1. n = 0 \<Longrightarrow> dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
 2. n = 1 \<Longrightarrow> dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
 3. 1 < n \<Longrightarrow> dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
[PROOF STEP]
from n
[PROOF STATE]
proof (chain)
picking this:
1 < n
[PROOF STEP]
have "{d. d dvd n \<and> d < n} = {d. d dvd n \<and> d \<noteq> n}"
[PROOF STATE]
proof (prove)
using this:
1 < n

goal (1 subgoal):
 1. {d. d dvd n \<and> d < n} = {d. d dvd n \<and> d \<noteq> n}
[PROOF STEP]
by (auto dest: dvd_imp_le)
[PROOF STATE]
proof (state)
this:
{d. d dvd n \<and> d < n} = {d. d dvd n \<and> d \<noteq> n}

goal (3 subgoals):
 1. n = 0 \<Longrightarrow> dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
 2. n = 1 \<Longrightarrow> dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
 3. 1 < n \<Longrightarrow> dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{d. d dvd n \<and> d < n} = {d. d dvd n \<and> d \<noteq> n}

goal (3 subgoals):
 1. n = 0 \<Longrightarrow> dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
 2. n = 1 \<Longrightarrow> dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
 3. 1 < n \<Longrightarrow> dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
[PROOF STEP]
have "f 1 * (- i *
                   (\<Sum>d | d dvd n \<and> d \<noteq> n. f (n div d) * dirichlet_inverse f i d)) =
               -(f 1 * i) *
                   (\<Sum>d | d dvd n \<and> d \<noteq> n. f (n div d) * dirichlet_inverse f i d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f 1 * (- i * (\<Sum>d | d dvd n \<and> d \<noteq> n. f (n div d) * dirichlet_inverse f i d)) = - (f 1 * i) * (\<Sum>d | d dvd n \<and> d \<noteq> n. f (n div d) * dirichlet_inverse f i d)
[PROOF STEP]
by (simp add: mult.assoc)
[PROOF STATE]
proof (state)
this:
f 1 * (- i * (\<Sum>d | d dvd n \<and> d \<noteq> n. f (n div d) * dirichlet_inverse f i d)) = - (f 1 * i) * (\<Sum>d | d dvd n \<and> d \<noteq> n. f (n div d) * dirichlet_inverse f i d)

goal (3 subgoals):
 1. n = 0 \<Longrightarrow> dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
 2. n = 1 \<Longrightarrow> dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
 3. 1 < n \<Longrightarrow> dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f 1 * (- i * (\<Sum>d | d dvd n \<and> d \<noteq> n. f (n div d) * dirichlet_inverse f i d)) = - (f 1 * i) * (\<Sum>d | d dvd n \<and> d \<noteq> n. f (n div d) * dirichlet_inverse f i d)

goal (3 subgoals):
 1. n = 0 \<Longrightarrow> dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
 2. n = 1 \<Longrightarrow> dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
 3. 1 < n \<Longrightarrow> dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
[PROOF STEP]
have "f 1 * i = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f 1 * i = (1::'a)
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
f 1 * i = (1::'a)

goal (3 subgoals):
 1. n = 0 \<Longrightarrow> dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
 2. n = 1 \<Longrightarrow> dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
 3. 1 < n \<Longrightarrow> dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dirichlet_prod f (dirichlet_inverse f i) n = - (1::'a) * (\<Sum>d | d dvd n \<and> d \<noteq> n. f (n div d) * dirichlet_inverse f i d) + (\<Sum>d | d dvd n \<and> d \<noteq> n. f (n div d) * dirichlet_inverse f i d)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dirichlet_prod f (dirichlet_inverse f i) n = - (1::'a) * (\<Sum>d | d dvd n \<and> d \<noteq> n. f (n div d) * dirichlet_inverse f i d) + (\<Sum>d | d dvd n \<and> d \<noteq> n. f (n div d) * dirichlet_inverse f i d)

goal (1 subgoal):
 1. dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
[PROOF STEP]
using n
[PROOF STATE]
proof (prove)
using this:
dirichlet_prod f (dirichlet_inverse f i) n = - (1::'a) * (\<Sum>d | d dvd n \<and> d \<noteq> n. f (n div d) * dirichlet_inverse f i d) + (\<Sum>d | d dvd n \<and> d \<noteq> n. f (n div d) * dirichlet_inverse f i d)
1 < n

goal (1 subgoal):
 1. dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
 2. n = 1 \<Longrightarrow> dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))
[PROOF STEP]
qed (insert assms, simp_all add: dirichlet_prod_def)
[PROOF STATE]
proof (state)
this:
dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1::'a else (0::'a))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dirichlet_prod_inverse':
  assumes "f 1 * i = 1"
  shows   "dirichlet_prod (dirichlet_inverse f i) f = (\<lambda>n. if n = 1 then 1 else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dirichlet_prod (dirichlet_inverse f i) f = (\<lambda>n. if n = 1 then 1::'a else (0::'a))
[PROOF STEP]
using dirichlet_prod_inverse[of f] assms
[PROOF STATE]
proof (prove)
using this:
f 1 * ?i = (1::'a) \<Longrightarrow> dirichlet_prod f (dirichlet_inverse f ?i) = (\<lambda>n. if n = 1 then 1::'a else (0::'a))
f 1 * i = (1::'a)

goal (1 subgoal):
 1. dirichlet_prod (dirichlet_inverse f i) f = (\<lambda>n. if n = 1 then 1::'a else (0::'a))
[PROOF STEP]
by (simp add: dirichlet_prod_commutes)


[STATEMENT]
lemma dirichlet_inverse_noninvertible:
  assumes "f (Suc 0) = (0 :: 'a :: {comm_ring_1})" "i = 0"
  shows   "dirichlet_inverse f i n = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dirichlet_inverse f i n = (0::'a)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f (Suc 0) = (0::'a)
i = (0::'a)

goal (1 subgoal):
 1. dirichlet_inverse f i n = (0::'a)
[PROOF STEP]
by (induction f i n rule: dirichlet_inverse.induct) (auto simp: dirichlet_inverse.simps)


[STATEMENT]
lemma multiplicative_dirichlet_prod:
  assumes "multiplicative_function f"
  assumes "multiplicative_function g"
  shows   "multiplicative_function (dirichlet_prod f g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicative_function (dirichlet_prod f g)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. multiplicative_function (dirichlet_prod f g)
[PROOF STEP]
interpret f: multiplicative_function f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicative_function f
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. multiplicative_function (dirichlet_prod f g)
[PROOF STEP]
interpret g: multiplicative_function g
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicative_function g
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. multiplicative_function (dirichlet_prod f g)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicative_function (dirichlet_prod f g)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. dirichlet_prod f g 0 = (0::'a)
 2. dirichlet_prod f g 1 = (1::'a)
 3. \<And>a b. \<lbrakk>1 < a; 1 < b; coprime a b\<rbrakk> \<Longrightarrow> dirichlet_prod f g (a * b) = dirichlet_prod f g a * dirichlet_prod f g b
[PROOF STEP]
fix a b :: nat
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. dirichlet_prod f g 0 = (0::'a)
 2. dirichlet_prod f g 1 = (1::'a)
 3. \<And>a b. \<lbrakk>1 < a; 1 < b; coprime a b\<rbrakk> \<Longrightarrow> dirichlet_prod f g (a * b) = dirichlet_prod f g a * dirichlet_prod f g b
[PROOF STEP]
assume "a > 1" "b > 1" and coprime: "coprime a b"
[PROOF STATE]
proof (state)
this:
1 < a
1 < b
coprime a b

goal (3 subgoals):
 1. dirichlet_prod f g 0 = (0::'a)
 2. dirichlet_prod f g 1 = (1::'a)
 3. \<And>a b. \<lbrakk>1 < a; 1 < b; coprime a b\<rbrakk> \<Longrightarrow> dirichlet_prod f g (a * b) = dirichlet_prod f g a * dirichlet_prod f g b
[PROOF STEP]
hence "dirichlet_prod f g (a * b) =
             (\<Sum>r | r dvd a. \<Sum>s | s dvd b. f (r * s) * g (a * b div (r * s)))"
[PROOF STATE]
proof (prove)
using this:
1 < a
1 < b
coprime a b

goal (1 subgoal):
 1. dirichlet_prod f g (a * b) = (\<Sum>r | r dvd a. \<Sum>s | s dvd b. f (r * s) * g (a * b div (r * s)))
[PROOF STEP]
by (simp add: dirichlet_prod_def sum_divisors_coprime_mult)
[PROOF STATE]
proof (state)
this:
dirichlet_prod f g (a * b) = (\<Sum>r | r dvd a. \<Sum>s | s dvd b. f (r * s) * g (a * b div (r * s)))

goal (3 subgoals):
 1. dirichlet_prod f g 0 = (0::'a)
 2. dirichlet_prod f g 1 = (1::'a)
 3. \<And>a b. \<lbrakk>1 < a; 1 < b; coprime a b\<rbrakk> \<Longrightarrow> dirichlet_prod f g (a * b) = dirichlet_prod f g a * dirichlet_prod f g b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dirichlet_prod f g (a * b) = (\<Sum>r | r dvd a. \<Sum>s | s dvd b. f (r * s) * g (a * b div (r * s)))

goal (3 subgoals):
 1. dirichlet_prod f g 0 = (0::'a)
 2. dirichlet_prod f g 1 = (1::'a)
 3. \<And>a b. \<lbrakk>1 < a; 1 < b; coprime a b\<rbrakk> \<Longrightarrow> dirichlet_prod f g (a * b) = dirichlet_prod f g a * dirichlet_prod f g b
[PROOF STEP]
have "\<dots> = (\<Sum>r | r dvd a. \<Sum>s | s dvd b. f r * f s * g (a div r) * g (b div s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>r | r dvd a. \<Sum>s | s dvd b. f (r * s) * g (a * b div (r * s))) = (\<Sum>r | r dvd a. \<Sum>s | s dvd b. f r * f s * g (a div r) * g (b div s))
[PROOF STEP]
using \<open>coprime a b\<close>
[PROOF STATE]
proof (prove)
using this:
coprime a b

goal (1 subgoal):
 1. (\<Sum>r | r dvd a. \<Sum>s | s dvd b. f (r * s) * g (a * b div (r * s))) = (\<Sum>r | r dvd a. \<Sum>s | s dvd b. f r * f s * g (a div r) * g (b div s))
[PROOF STEP]
proof (rule sum_coprime_dvd_cong)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r s. \<lbrakk>coprime r s; r dvd a; s dvd b\<rbrakk> \<Longrightarrow> f (r * s) * g (a * b div (r * s)) = f r * f s * g (a div r) * g (b div s)
[PROOF STEP]
fix r s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r s. \<lbrakk>coprime r s; r dvd a; s dvd b\<rbrakk> \<Longrightarrow> f (r * s) * g (a * b div (r * s)) = f r * f s * g (a div r) * g (b div s)
[PROOF STEP]
assume "coprime r s" and "r dvd a" and "s dvd b"
[PROOF STATE]
proof (state)
this:
coprime r s
r dvd a
s dvd b

goal (1 subgoal):
 1. \<And>r s. \<lbrakk>coprime r s; r dvd a; s dvd b\<rbrakk> \<Longrightarrow> f (r * s) * g (a * b div (r * s)) = f r * f s * g (a div r) * g (b div s)
[PROOF STEP]
with \<open>a > 1\<close> \<open>b > 1\<close>
[PROOF STATE]
proof (chain)
picking this:
1 < a
1 < b
coprime r s
r dvd a
s dvd b
[PROOF STEP]
have "r > 0" "s > 0"
[PROOF STATE]
proof (prove)
using this:
1 < a
1 < b
coprime r s
r dvd a
s dvd b

goal (1 subgoal):
 1. 0 < r &&& 0 < s
[PROOF STEP]
by (auto intro: ccontr)
[PROOF STATE]
proof (state)
this:
0 < r
0 < s

goal (1 subgoal):
 1. \<And>r s. \<lbrakk>coprime r s; r dvd a; s dvd b\<rbrakk> \<Longrightarrow> f (r * s) * g (a * b div (r * s)) = f r * f s * g (a div r) * g (b div s)
[PROOF STEP]
from \<open>coprime r s\<close>
[PROOF STATE]
proof (chain)
picking this:
coprime r s
[PROOF STEP]
have "f (r * s) = f r * f s"
[PROOF STATE]
proof (prove)
using this:
coprime r s

goal (1 subgoal):
 1. f (r * s) = f r * f s
[PROOF STEP]
by (rule f.mult_coprime)
[PROOF STATE]
proof (state)
this:
f (r * s) = f r * f s

goal (1 subgoal):
 1. \<And>r s. \<lbrakk>coprime r s; r dvd a; s dvd b\<rbrakk> \<Longrightarrow> f (r * s) * g (a * b div (r * s)) = f r * f s * g (a div r) * g (b div s)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f (r * s) = f r * f s

goal (1 subgoal):
 1. \<And>r s. \<lbrakk>coprime r s; r dvd a; s dvd b\<rbrakk> \<Longrightarrow> f (r * s) * g (a * b div (r * s)) = f r * f s * g (a div r) * g (b div s)
[PROOF STEP]
from \<open>coprime a b\<close>
[PROOF STATE]
proof (chain)
picking this:
coprime a b
[PROOF STEP]
have \<open>coprime (a div r) (b div s)\<close>
[PROOF STATE]
proof (prove)
using this:
coprime a b

goal (1 subgoal):
 1. coprime (a div r) (b div s)
[PROOF STEP]
using \<open>r > 0\<close> \<open>s > 0\<close> \<open>r dvd a\<close> \<open>s dvd b\<close> dvd_div_iff_mult [of r a] dvd_div_iff_mult [of s b]
[PROOF STATE]
proof (prove)
using this:
coprime a b
0 < r
0 < s
r dvd a
s dvd b
\<lbrakk>r \<noteq> 0; r dvd a\<rbrakk> \<Longrightarrow> (?a dvd a div r) = (?a * r dvd a)
\<lbrakk>s \<noteq> 0; s dvd b\<rbrakk> \<Longrightarrow> (?a dvd b div s) = (?a * s dvd b)

goal (1 subgoal):
 1. coprime (a div r) (b div s)
[PROOF STEP]
by (auto dest: coprime_imp_coprime dvd_mult_left)
[PROOF STATE]
proof (state)
this:
coprime (a div r) (b div s)

goal (1 subgoal):
 1. \<And>r s. \<lbrakk>coprime r s; r dvd a; s dvd b\<rbrakk> \<Longrightarrow> f (r * s) * g (a * b div (r * s)) = f r * f s * g (a div r) * g (b div s)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
coprime (a div r) (b div s)
[PROOF STEP]
have "g (a div r * (b div s)) = g (a div r) * g (b div s)"
[PROOF STATE]
proof (prove)
using this:
coprime (a div r) (b div s)

goal (1 subgoal):
 1. g (a div r * (b div s)) = g (a div r) * g (b div s)
[PROOF STEP]
by (rule g.mult_coprime)
[PROOF STATE]
proof (state)
this:
g (a div r * (b div s)) = g (a div r) * g (b div s)

goal (1 subgoal):
 1. \<And>r s. \<lbrakk>coprime r s; r dvd a; s dvd b\<rbrakk> \<Longrightarrow> f (r * s) * g (a * b div (r * s)) = f r * f s * g (a div r) * g (b div s)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f (r * s) = f r * f s
g (a div r * (b div s)) = g (a div r) * g (b div s)
[PROOF STEP]
show "f (r * s) * g (a * b div (r * s)) = f r * f s * g (a div r) * g (b div s)"
[PROOF STATE]
proof (prove)
using this:
f (r * s) = f r * f s
g (a div r * (b div s)) = g (a div r) * g (b div s)

goal (1 subgoal):
 1. f (r * s) * g (a * b div (r * s)) = f r * f s * g (a div r) * g (b div s)
[PROOF STEP]
using \<open>r dvd a\<close> \<open>s dvd b\<close>
[PROOF STATE]
proof (prove)
using this:
f (r * s) = f r * f s
g (a div r * (b div s)) = g (a div r) * g (b div s)
r dvd a
s dvd b

goal (1 subgoal):
 1. f (r * s) * g (a * b div (r * s)) = f r * f s * g (a div r) * g (b div s)
[PROOF STEP]
by (simp add: div_mult_div_if_dvd ac_simps)
[PROOF STATE]
proof (state)
this:
f (r * s) * g (a * b div (r * s)) = f r * f s * g (a div r) * g (b div s)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>r | r dvd a. \<Sum>s | s dvd b. f (r * s) * g (a * b div (r * s))) = (\<Sum>r | r dvd a. \<Sum>s | s dvd b. f r * f s * g (a div r) * g (b div s))

goal (3 subgoals):
 1. dirichlet_prod f g 0 = (0::'a)
 2. dirichlet_prod f g 1 = (1::'a)
 3. \<And>a b. \<lbrakk>1 < a; 1 < b; coprime a b\<rbrakk> \<Longrightarrow> dirichlet_prod f g (a * b) = dirichlet_prod f g a * dirichlet_prod f g b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>r | r dvd a. \<Sum>s | s dvd b. f (r * s) * g (a * b div (r * s))) = (\<Sum>r | r dvd a. \<Sum>s | s dvd b. f r * f s * g (a div r) * g (b div s))

goal (3 subgoals):
 1. dirichlet_prod f g 0 = (0::'a)
 2. dirichlet_prod f g 1 = (1::'a)
 3. \<And>a b. \<lbrakk>1 < a; 1 < b; coprime a b\<rbrakk> \<Longrightarrow> dirichlet_prod f g (a * b) = dirichlet_prod f g a * dirichlet_prod f g b
[PROOF STEP]
have "\<dots> = dirichlet_prod f g a * dirichlet_prod f g b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>r | r dvd a. \<Sum>s | s dvd b. f r * f s * g (a div r) * g (b div s)) = dirichlet_prod f g a * dirichlet_prod f g b
[PROOF STEP]
unfolding dirichlet_prod_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>r | r dvd a. \<Sum>s | s dvd b. f r * f s * g (a div r) * g (b div s)) = (\<Sum>d | d dvd a. f d * g (a div d)) * (\<Sum>d | d dvd b. f d * g (b div d))
[PROOF STEP]
by (simp add: sum_product mult_ac)
[PROOF STATE]
proof (state)
this:
(\<Sum>r | r dvd a. \<Sum>s | s dvd b. f r * f s * g (a div r) * g (b div s)) = dirichlet_prod f g a * dirichlet_prod f g b

goal (3 subgoals):
 1. dirichlet_prod f g 0 = (0::'a)
 2. dirichlet_prod f g 1 = (1::'a)
 3. \<And>a b. \<lbrakk>1 < a; 1 < b; coprime a b\<rbrakk> \<Longrightarrow> dirichlet_prod f g (a * b) = dirichlet_prod f g a * dirichlet_prod f g b
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dirichlet_prod f g (a * b) = dirichlet_prod f g a * dirichlet_prod f g b
[PROOF STEP]
show "dirichlet_prod f g (a * b) = \<dots>"
[PROOF STATE]
proof (prove)
using this:
dirichlet_prod f g (a * b) = dirichlet_prod f g a * dirichlet_prod f g b

goal (1 subgoal):
 1. dirichlet_prod f g (a * b) = dirichlet_prod f g a * dirichlet_prod f g b
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
dirichlet_prod f g (a * b) = dirichlet_prod f g a * dirichlet_prod f g b

goal (2 subgoals):
 1. dirichlet_prod f g 0 = (0::'a)
 2. dirichlet_prod f g 1 = (1::'a)
[PROOF STEP]
qed simp_all
[PROOF STATE]
proof (state)
this:
multiplicative_function (dirichlet_prod f g)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma multiplicative_dirichlet_prodD1:
  fixes f g :: "nat \<Rightarrow> 'a :: comm_semiring_1_cancel"
  assumes "multiplicative_function (dirichlet_prod f g)"
  assumes "multiplicative_function f"
  assumes [simp]: "g 0 = 0"
  shows   "multiplicative_function g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicative_function g
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. multiplicative_function g
[PROOF STEP]
interpret f: multiplicative_function f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicative_function f
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. multiplicative_function g
[PROOF STEP]
interpret fg: multiplicative_function "dirichlet_prod f g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicative_function (dirichlet_prod f g)
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. multiplicative_function g
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicative_function g
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. g 0 = (0::'a)
 2. g 1 = (1::'a)
 3. \<And>a b. \<lbrakk>1 < a; 1 < b; coprime a b\<rbrakk> \<Longrightarrow> g (a * b) = g a * g b
[PROOF STEP]
have "dirichlet_prod f g (Suc 0) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dirichlet_prod f g (Suc 0) = (1::'a)
[PROOF STEP]
by (rule fg.Suc_0)
[PROOF STATE]
proof (state)
this:
dirichlet_prod f g (Suc 0) = (1::'a)

goal (3 subgoals):
 1. g 0 = (0::'a)
 2. g 1 = (1::'a)
 3. \<And>a b. \<lbrakk>1 < a; 1 < b; coprime a b\<rbrakk> \<Longrightarrow> g (a * b) = g a * g b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dirichlet_prod f g (Suc 0) = (1::'a)

goal (3 subgoals):
 1. g 0 = (0::'a)
 2. g 1 = (1::'a)
 3. \<And>a b. \<lbrakk>1 < a; 1 < b; coprime a b\<rbrakk> \<Longrightarrow> g (a * b) = g a * g b
[PROOF STEP]
have "dirichlet_prod f g (Suc 0) = g 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dirichlet_prod f g (Suc 0) = g 1
[PROOF STEP]
by (subst dirichlet_prod_Suc_0) simp
[PROOF STATE]
proof (state)
this:
dirichlet_prod f g (Suc 0) = g 1

goal (3 subgoals):
 1. g 0 = (0::'a)
 2. g 1 = (1::'a)
 3. \<And>a b. \<lbrakk>1 < a; 1 < b; coprime a b\<rbrakk> \<Longrightarrow> g (a * b) = g a * g b
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
g 1 = (1::'a)
[PROOF STEP]
show "g 1 = 1"
[PROOF STATE]
proof (prove)
using this:
g 1 = (1::'a)

goal (1 subgoal):
 1. g 1 = (1::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
g 1 = (1::'a)

goal (2 subgoals):
 1. g 0 = (0::'a)
 2. \<And>a b. \<lbrakk>1 < a; 1 < b; coprime a b\<rbrakk> \<Longrightarrow> g (a * b) = g a * g b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. g 0 = (0::'a)
 2. \<And>a b. \<lbrakk>1 < a; 1 < b; coprime a b\<rbrakk> \<Longrightarrow> g (a * b) = g a * g b
[PROOF STEP]
fix a b :: nat
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. g 0 = (0::'a)
 2. \<And>a b. \<lbrakk>1 < a; 1 < b; coprime a b\<rbrakk> \<Longrightarrow> g (a * b) = g a * g b
[PROOF STEP]
assume ab: "a > 1" "b > 1" "coprime a b"
[PROOF STATE]
proof (state)
this:
1 < a
1 < b
coprime a b

goal (2 subgoals):
 1. g 0 = (0::'a)
 2. \<And>a b. \<lbrakk>1 < a; 1 < b; coprime a b\<rbrakk> \<Longrightarrow> g (a * b) = g a * g b
[PROOF STEP]
hence "a > 0" "b > 0" "coprime a b"
[PROOF STATE]
proof (prove)
using this:
1 < a
1 < b
coprime a b

goal (1 subgoal):
 1. 0 < a &&& 0 < b &&& coprime a b
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
0 < a
0 < b
coprime a b

goal (2 subgoals):
 1. g 0 = (0::'a)
 2. \<And>a b. \<lbrakk>1 < a; 1 < b; coprime a b\<rbrakk> \<Longrightarrow> g (a * b) = g a * g b
[PROOF STEP]
thus "g (a * b) = g a * g b"
[PROOF STATE]
proof (prove)
using this:
0 < a
0 < b
coprime a b

goal (1 subgoal):
 1. g (a * b) = g a * g b
[PROOF STEP]
proof (induction "a * b" arbitrary: a b rule: less_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<And>aa ba. \<lbrakk>aa * ba < a * b; 0 < aa; 0 < ba; coprime aa ba\<rbrakk> \<Longrightarrow> g (aa * ba) = g aa * g ba; 0 < a; 0 < b; coprime a b\<rbrakk> \<Longrightarrow> g (a * b) = g a * g b
[PROOF STEP]
case (less a b)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?a * ?b < a * b; 0 < ?a; 0 < ?b; coprime ?a ?b\<rbrakk> \<Longrightarrow> g (?a * ?b) = g ?a * g ?b
0 < a
0 < b
coprime a b

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<And>aa ba. \<lbrakk>aa * ba < a * b; 0 < aa; 0 < ba; coprime aa ba\<rbrakk> \<Longrightarrow> g (aa * ba) = g aa * g ba; 0 < a; 0 < b; coprime a b\<rbrakk> \<Longrightarrow> g (a * b) = g a * g b
[PROOF STEP]
have "dirichlet_prod f g (a * b) + g a * g b =
              (\<Sum>r | r dvd a * b. f r * g (a * b div r)) + g a * g b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dirichlet_prod f g (a * b) + g a * g b = (\<Sum>r | r dvd a * b. f r * g (a * b div r)) + g a * g b
[PROOF STEP]
by (simp add: dirichlet_prod_def)
[PROOF STATE]
proof (state)
this:
dirichlet_prod f g (a * b) + g a * g b = (\<Sum>r | r dvd a * b. f r * g (a * b div r)) + g a * g b

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<And>aa ba. \<lbrakk>aa * ba < a * b; 0 < aa; 0 < ba; coprime aa ba\<rbrakk> \<Longrightarrow> g (aa * ba) = g aa * g ba; 0 < a; 0 < b; coprime a b\<rbrakk> \<Longrightarrow> g (a * b) = g a * g b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dirichlet_prod f g (a * b) + g a * g b = (\<Sum>r | r dvd a * b. f r * g (a * b div r)) + g a * g b

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<And>aa ba. \<lbrakk>aa * ba < a * b; 0 < aa; 0 < ba; coprime aa ba\<rbrakk> \<Longrightarrow> g (aa * ba) = g aa * g ba; 0 < a; 0 < b; coprime a b\<rbrakk> \<Longrightarrow> g (a * b) = g a * g b
[PROOF STEP]
have "{r. r dvd a * b} = insert 1 {r. r dvd a * b \<and> r \<noteq> 1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {r. r dvd a * b} = insert 1 {r. r dvd a * b \<and> r \<noteq> 1}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{r. r dvd a * b} = insert 1 {r. r dvd a * b \<and> r \<noteq> 1}

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<And>aa ba. \<lbrakk>aa * ba < a * b; 0 < aa; 0 < ba; coprime aa ba\<rbrakk> \<Longrightarrow> g (aa * ba) = g aa * g ba; 0 < a; 0 < b; coprime a b\<rbrakk> \<Longrightarrow> g (a * b) = g a * g b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{r. r dvd a * b} = insert 1 {r. r dvd a * b \<and> r \<noteq> 1}

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<And>aa ba. \<lbrakk>aa * ba < a * b; 0 < aa; 0 < ba; coprime aa ba\<rbrakk> \<Longrightarrow> g (aa * ba) = g aa * g ba; 0 < a; 0 < b; coprime a b\<rbrakk> \<Longrightarrow> g (a * b) = g a * g b
[PROOF STEP]
have "(\<Sum>r\<in>\<dots>. f r * g (a * b div r)) + g a * g b =
                   g (a * b) + ((\<Sum>r | r dvd a * b \<and> r \<noteq> 1. f r * g (a * b div r)) + g a * g b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>r\<in>insert 1 {r. r dvd a * b \<and> r \<noteq> 1}. f r * g (a * b div r)) + g a * g b = g (a * b) + ((\<Sum>r | r dvd a * b \<and> r \<noteq> 1. f r * g (a * b div r)) + g a * g b)
[PROOF STEP]
using less.prems
[PROOF STATE]
proof (prove)
using this:
0 < a
0 < b
coprime a b

goal (1 subgoal):
 1. (\<Sum>r\<in>insert 1 {r. r dvd a * b \<and> r \<noteq> 1}. f r * g (a * b div r)) + g a * g b = g (a * b) + ((\<Sum>r | r dvd a * b \<and> r \<noteq> 1. f r * g (a * b div r)) + g a * g b)
[PROOF STEP]
by (subst sum.insert) (auto intro!: finite_subset[OF _ finite_divisors_nat'] simp: add_ac)
[PROOF STATE]
proof (state)
this:
(\<Sum>r\<in>insert 1 {r. r dvd a * b \<and> r \<noteq> 1}. f r * g (a * b div r)) + g a * g b = g (a * b) + ((\<Sum>r | r dvd a * b \<and> r \<noteq> 1. f r * g (a * b div r)) + g a * g b)

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<And>aa ba. \<lbrakk>aa * ba < a * b; 0 < aa; 0 < ba; coprime aa ba\<rbrakk> \<Longrightarrow> g (aa * ba) = g aa * g ba; 0 < a; 0 < b; coprime a b\<rbrakk> \<Longrightarrow> g (a * b) = g a * g b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>r\<in>insert 1 {r. r dvd a * b \<and> r \<noteq> 1}. f r * g (a * b div r)) + g a * g b = g (a * b) + ((\<Sum>r | r dvd a * b \<and> r \<noteq> 1. f r * g (a * b div r)) + g a * g b)

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<And>aa ba. \<lbrakk>aa * ba < a * b; 0 < aa; 0 < ba; coprime aa ba\<rbrakk> \<Longrightarrow> g (aa * ba) = g aa * g ba; 0 < a; 0 < b; coprime a b\<rbrakk> \<Longrightarrow> g (a * b) = g a * g b
[PROOF STEP]
have "(\<Sum>r | r dvd a * b \<and> r \<noteq> 1. f r * g (a * b div r)) =
                     (\<Sum>r | r dvd a * b. if r = 1 then 0 else f r * g (a * b div r))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>r | r dvd a * b \<and> r \<noteq> 1. f r * g (a * b div r)) = (\<Sum>r | r dvd a * b. if r = 1 then 0::'a else f r * g (a * b div r))
[PROOF STEP]
using less.prems
[PROOF STATE]
proof (prove)
using this:
0 < a
0 < b
coprime a b

goal (1 subgoal):
 1. (\<Sum>r | r dvd a * b \<and> r \<noteq> 1. f r * g (a * b div r)) = (\<Sum>r | r dvd a * b. if r = 1 then 0::'a else f r * g (a * b div r))
[PROOF STEP]
by (intro sum.mono_neutral_cong_left) (auto intro: finite_divisors_nat')
[PROOF STATE]
proof (state)
this:
(\<Sum>r | r dvd a * b \<and> r \<noteq> 1. f r * g (a * b div r)) = (\<Sum>r | r dvd a * b. if r = 1 then 0::'a else f r * g (a * b div r))

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<And>aa ba. \<lbrakk>aa * ba < a * b; 0 < aa; 0 < ba; coprime aa ba\<rbrakk> \<Longrightarrow> g (aa * ba) = g aa * g ba; 0 < a; 0 < b; coprime a b\<rbrakk> \<Longrightarrow> g (a * b) = g a * g b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>r | r dvd a * b \<and> r \<noteq> 1. f r * g (a * b div r)) = (\<Sum>r | r dvd a * b. if r = 1 then 0::'a else f r * g (a * b div r))

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<And>aa ba. \<lbrakk>aa * ba < a * b; 0 < aa; 0 < ba; coprime aa ba\<rbrakk> \<Longrightarrow> g (aa * ba) = g aa * g ba; 0 < a; 0 < b; coprime a b\<rbrakk> \<Longrightarrow> g (a * b) = g a * g b
[PROOF STEP]
have "\<dots> = (\<Sum>r | r dvd a. \<Sum>d | d dvd b.
                          if r * d = 1 then 0 else f (r * d) * g (a * b div (r * d)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>r | r dvd a * b. if r = 1 then 0::'a else f r * g (a * b div r)) = (\<Sum>r | r dvd a. \<Sum>d | d dvd b. if r * d = 1 then 0::'a else f (r * d) * g (a * b div (r * d)))
[PROOF STEP]
using \<open>coprime a b\<close>
[PROOF STATE]
proof (prove)
using this:
coprime a b

goal (1 subgoal):
 1. (\<Sum>r | r dvd a * b. if r = 1 then 0::'a else f r * g (a * b div r)) = (\<Sum>r | r dvd a. \<Sum>d | d dvd b. if r * d = 1 then 0::'a else f (r * d) * g (a * b div (r * d)))
[PROOF STEP]
by (rule sum_divisors_coprime_mult)
[PROOF STATE]
proof (state)
this:
(\<Sum>r | r dvd a * b. if r = 1 then 0::'a else f r * g (a * b div r)) = (\<Sum>r | r dvd a. \<Sum>d | d dvd b. if r * d = 1 then 0::'a else f (r * d) * g (a * b div (r * d)))

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<And>aa ba. \<lbrakk>aa * ba < a * b; 0 < aa; 0 < ba; coprime aa ba\<rbrakk> \<Longrightarrow> g (aa * ba) = g aa * g ba; 0 < a; 0 < b; coprime a b\<rbrakk> \<Longrightarrow> g (a * b) = g a * g b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>r | r dvd a * b. if r = 1 then 0::'a else f r * g (a * b div r)) = (\<Sum>r | r dvd a. \<Sum>d | d dvd b. if r * d = 1 then 0::'a else f (r * d) * g (a * b div (r * d)))

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<And>aa ba. \<lbrakk>aa * ba < a * b; 0 < aa; 0 < ba; coprime aa ba\<rbrakk> \<Longrightarrow> g (aa * ba) = g aa * g ba; 0 < a; 0 < b; coprime a b\<rbrakk> \<Longrightarrow> g (a * b) = g a * g b
[PROOF STEP]
have "\<dots> = (\<Sum>r | r dvd a. \<Sum>d | d dvd b.
                          if r * d = 1 then 0 else f (r * d) * g ((a div r) * (b div d)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>r | r dvd a. \<Sum>d | d dvd b. if r * d = 1 then 0::'a else f (r * d) * g (a * b div (r * d))) = (\<Sum>r | r dvd a. \<Sum>d | d dvd b. if r * d = 1 then 0::'a else f (r * d) * g (a div r * (b div d)))
[PROOF STEP]
by (intro sum.cong refl) (auto elim!: dvdE)
[PROOF STATE]
proof (state)
this:
(\<Sum>r | r dvd a. \<Sum>d | d dvd b. if r * d = 1 then 0::'a else f (r * d) * g (a * b div (r * d))) = (\<Sum>r | r dvd a. \<Sum>d | d dvd b. if r * d = 1 then 0::'a else f (r * d) * g (a div r * (b div d)))

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<And>aa ba. \<lbrakk>aa * ba < a * b; 0 < aa; 0 < ba; coprime aa ba\<rbrakk> \<Longrightarrow> g (aa * ba) = g aa * g ba; 0 < a; 0 < b; coprime a b\<rbrakk> \<Longrightarrow> g (a * b) = g a * g b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>r | r dvd a. \<Sum>d | d dvd b. if r * d = 1 then 0::'a else f (r * d) * g (a * b div (r * d))) = (\<Sum>r | r dvd a. \<Sum>d | d dvd b. if r * d = 1 then 0::'a else f (r * d) * g (a div r * (b div d)))

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<And>aa ba. \<lbrakk>aa * ba < a * b; 0 < aa; 0 < ba; coprime aa ba\<rbrakk> \<Longrightarrow> g (aa * ba) = g aa * g ba; 0 < a; 0 < b; coprime a b\<rbrakk> \<Longrightarrow> g (a * b) = g a * g b
[PROOF STEP]
have "\<dots> = (\<Sum>r | r dvd a. \<Sum>d | d dvd b.
                          if r * d = 1 then 0 else f r * f d * g (a div r) * g (b div d))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>r | r dvd a. \<Sum>d | d dvd b. if r * d = 1 then 0::'a else f (r * d) * g (a div r * (b div d))) = (\<Sum>r | r dvd a. \<Sum>d | d dvd b. if r * d = 1 then 0::'a else f r * f d * g (a div r) * g (b div d))
[PROOF STEP]
using \<open>coprime a b\<close>
[PROOF STATE]
proof (prove)
using this:
coprime a b

goal (1 subgoal):
 1. (\<Sum>r | r dvd a. \<Sum>d | d dvd b. if r * d = 1 then 0::'a else f (r * d) * g (a div r * (b div d))) = (\<Sum>r | r dvd a. \<Sum>d | d dvd b. if r * d = 1 then 0::'a else f r * f d * g (a div r) * g (b div d))
[PROOF STEP]
proof (rule sum_coprime_dvd_cong)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r d. \<lbrakk>coprime r d; r dvd a; d dvd b\<rbrakk> \<Longrightarrow> (if r * d = 1 then 0::'a else f (r * d) * g (a div r * (b div d))) = (if r * d = 1 then 0::'a else f r * f d * g (a div r) * g (b div d))
[PROOF STEP]
fix r s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r d. \<lbrakk>coprime r d; r dvd a; d dvd b\<rbrakk> \<Longrightarrow> (if r * d = 1 then 0::'a else f (r * d) * g (a div r * (b div d))) = (if r * d = 1 then 0::'a else f r * f d * g (a div r) * g (b div d))
[PROOF STEP]
assume "coprime r s" and "r dvd a" and "s dvd b"
[PROOF STATE]
proof (state)
this:
coprime r s
r dvd a
s dvd b

goal (1 subgoal):
 1. \<And>r d. \<lbrakk>coprime r d; r dvd a; d dvd b\<rbrakk> \<Longrightarrow> (if r * d = 1 then 0::'a else f (r * d) * g (a div r * (b div d))) = (if r * d = 1 then 0::'a else f r * f d * g (a div r) * g (b div d))
[PROOF STEP]
with \<open>a > 0\<close> \<open>b > 0\<close>
[PROOF STATE]
proof (chain)
picking this:
0 < a
0 < b
coprime r s
r dvd a
s dvd b
[PROOF STEP]
have "r > 0" "s > 0"
[PROOF STATE]
proof (prove)
using this:
0 < a
0 < b
coprime r s
r dvd a
s dvd b

goal (1 subgoal):
 1. 0 < r &&& 0 < s
[PROOF STEP]
by (auto intro: ccontr)
[PROOF STATE]
proof (state)
this:
0 < r
0 < s

goal (1 subgoal):
 1. \<And>r d. \<lbrakk>coprime r d; r dvd a; d dvd b\<rbrakk> \<Longrightarrow> (if r * d = 1 then 0::'a else f (r * d) * g (a div r * (b div d))) = (if r * d = 1 then 0::'a else f r * f d * g (a div r) * g (b div d))
[PROOF STEP]
from \<open>coprime r s\<close>
[PROOF STATE]
proof (chain)
picking this:
coprime r s
[PROOF STEP]
have f: "f (r * s) = f r * f s"
[PROOF STATE]
proof (prove)
using this:
coprime r s

goal (1 subgoal):
 1. f (r * s) = f r * f s
[PROOF STEP]
by (rule f.mult_coprime)
[PROOF STATE]
proof (state)
this:
f (r * s) = f r * f s

goal (1 subgoal):
 1. \<And>r d. \<lbrakk>coprime r d; r dvd a; d dvd b\<rbrakk> \<Longrightarrow> (if r * d = 1 then 0::'a else f (r * d) * g (a div r * (b div d))) = (if r * d = 1 then 0::'a else f r * f d * g (a div r) * g (b div d))
[PROOF STEP]
show "(if r * s = 1 then 0 else f (r * s) * g (a div r * (b div s))) =
          (if r * s = 1 then 0 else f r * f s * g (a div r) * g (b div s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if r * s = 1 then 0::'a else f (r * s) * g (a div r * (b div s))) = (if r * s = 1 then 0::'a else f r * f s * g (a div r) * g (b div s))
[PROOF STEP]
proof (cases "r * s = 1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. r * s = 1 \<Longrightarrow> (if r * s = 1 then 0::'a else f (r * s) * g (a div r * (b div s))) = (if r * s = 1 then 0::'a else f r * f s * g (a div r) * g (b div s))
 2. r * s \<noteq> 1 \<Longrightarrow> (if r * s = 1 then 0::'a else f (r * s) * g (a div r * (b div s))) = (if r * s = 1 then 0::'a else f r * f s * g (a div r) * g (b div s))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
r * s = 1

goal (2 subgoals):
 1. r * s = 1 \<Longrightarrow> (if r * s = 1 then 0::'a else f (r * s) * g (a div r * (b div s))) = (if r * s = 1 then 0::'a else f r * f s * g (a div r) * g (b div s))
 2. r * s \<noteq> 1 \<Longrightarrow> (if r * s = 1 then 0::'a else f (r * s) * g (a div r * (b div s))) = (if r * s = 1 then 0::'a else f r * f s * g (a div r) * g (b div s))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r * s = 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
r * s = 1

goal (1 subgoal):
 1. (if r * s = 1 then 0::'a else f (r * s) * g (a div r * (b div s))) = (if r * s = 1 then 0::'a else f r * f s * g (a div r) * g (b div s))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(if r * s = 1 then 0::'a else f (r * s) * g (a div r * (b div s))) = (if r * s = 1 then 0::'a else f r * f s * g (a div r) * g (b div s))

goal (1 subgoal):
 1. r * s \<noteq> 1 \<Longrightarrow> (if r * s = 1 then 0::'a else f (r * s) * g (a div r * (b div s))) = (if r * s = 1 then 0::'a else f r * f s * g (a div r) * g (b div s))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r * s \<noteq> 1 \<Longrightarrow> (if r * s = 1 then 0::'a else f (r * s) * g (a div r * (b div s))) = (if r * s = 1 then 0::'a else f r * f s * g (a div r) * g (b div s))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
r * s \<noteq> 1

goal (1 subgoal):
 1. r * s \<noteq> 1 \<Longrightarrow> (if r * s = 1 then 0::'a else f (r * s) * g (a div r * (b div s))) = (if r * s = 1 then 0::'a else f r * f s * g (a div r) * g (b div s))
[PROOF STEP]
with \<open>r dvd a\<close> \<open>s dvd b\<close> less.prems
[PROOF STATE]
proof (chain)
picking this:
r dvd a
s dvd b
0 < a
0 < b
coprime a b
r * s \<noteq> 1
[PROOF STEP]
have "(a div r) * (b div s) \<noteq> a * b"
[PROOF STATE]
proof (prove)
using this:
r dvd a
s dvd b
0 < a
0 < b
coprime a b
r * s \<noteq> 1

goal (1 subgoal):
 1. a div r * (b div s) \<noteq> a * b
[PROOF STEP]
by (intro notI) (auto elim!: dvdE)
[PROOF STATE]
proof (state)
this:
a div r * (b div s) \<noteq> a * b

goal (1 subgoal):
 1. r * s \<noteq> 1 \<Longrightarrow> (if r * s = 1 then 0::'a else f (r * s) * g (a div r * (b div s))) = (if r * s = 1 then 0::'a else f r * f s * g (a div r) * g (b div s))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
a div r * (b div s) \<noteq> a * b

goal (1 subgoal):
 1. r * s \<noteq> 1 \<Longrightarrow> (if r * s = 1 then 0::'a else f (r * s) * g (a div r * (b div s))) = (if r * s = 1 then 0::'a else f r * f s * g (a div r) * g (b div s))
[PROOF STEP]
from \<open>r dvd a\<close> \<open>s dvd b\<close> less.prems
[PROOF STATE]
proof (chain)
picking this:
r dvd a
s dvd b
0 < a
0 < b
coprime a b
[PROOF STEP]
have "(a div r) * (b div s) \<le> a * b"
[PROOF STATE]
proof (prove)
using this:
r dvd a
s dvd b
0 < a
0 < b
coprime a b

goal (1 subgoal):
 1. a div r * (b div s) \<le> a * b
[PROOF STEP]
by (intro dvd_imp_le mult_dvd_mono Nat.gr0I) (auto elim!: dvdE)
[PROOF STATE]
proof (state)
this:
a div r * (b div s) \<le> a * b

goal (1 subgoal):
 1. r * s \<noteq> 1 \<Longrightarrow> (if r * s = 1 then 0::'a else f (r * s) * g (a div r * (b div s))) = (if r * s = 1 then 0::'a else f r * f s * g (a div r) * g (b div s))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
a div r * (b div s) \<noteq> a * b
a div r * (b div s) \<le> a * b
[PROOF STEP]
have "(a div r) * (b div s) < a * b"
[PROOF STATE]
proof (prove)
using this:
a div r * (b div s) \<noteq> a * b
a div r * (b div s) \<le> a * b

goal (1 subgoal):
 1. a div r * (b div s) < a * b
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
a div r * (b div s) < a * b

goal (1 subgoal):
 1. r * s \<noteq> 1 \<Longrightarrow> (if r * s = 1 then 0::'a else f (r * s) * g (a div r * (b div s))) = (if r * s = 1 then 0::'a else f r * f s * g (a div r) * g (b div s))
[PROOF STEP]
with \<open>r dvd a\<close> \<open>s dvd b\<close> less.prems
[PROOF STATE]
proof (chain)
picking this:
r dvd a
s dvd b
0 < a
0 < b
coprime a b
a div r * (b div s) < a * b
[PROOF STEP]
have g: "g ((a div r) * (b div s)) = g (a div r) * g (b div s)"
[PROOF STATE]
proof (prove)
using this:
r dvd a
s dvd b
0 < a
0 < b
coprime a b
a div r * (b div s) < a * b

goal (1 subgoal):
 1. g (a div r * (b div s)) = g (a div r) * g (b div s)
[PROOF STEP]
by (auto intro: less coprime_divisors [OF _ _ \<open>coprime a b\<close>] elim!: dvdE)
[PROOF STATE]
proof (state)
this:
g (a div r * (b div s)) = g (a div r) * g (b div s)

goal (1 subgoal):
 1. r * s \<noteq> 1 \<Longrightarrow> (if r * s = 1 then 0::'a else f (r * s) * g (a div r * (b div s))) = (if r * s = 1 then 0::'a else f r * f s * g (a div r) * g (b div s))
[PROOF STEP]
from False
[PROOF STATE]
proof (chain)
picking this:
r * s \<noteq> 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
r * s \<noteq> 1

goal (1 subgoal):
 1. (if r * s = 1 then 0::'a else f (r * s) * g (a div r * (b div s))) = (if r * s = 1 then 0::'a else f r * f s * g (a div r) * g (b div s))
[PROOF STEP]
by (auto simp: less f g ac_simps)
[PROOF STATE]
proof (state)
this:
(if r * s = 1 then 0::'a else f (r * s) * g (a div r * (b div s))) = (if r * s = 1 then 0::'a else f r * f s * g (a div r) * g (b div s))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(if r * s = 1 then 0::'a else f (r * s) * g (a div r * (b div s))) = (if r * s = 1 then 0::'a else f r * f s * g (a div r) * g (b div s))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>r | r dvd a. \<Sum>d | d dvd b. if r * d = 1 then 0::'a else f (r * d) * g (a div r * (b div d))) = (\<Sum>r | r dvd a. \<Sum>d | d dvd b. if r * d = 1 then 0::'a else f r * f d * g (a div r) * g (b div d))

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<And>aa ba. \<lbrakk>aa * ba < a * b; 0 < aa; 0 < ba; coprime aa ba\<rbrakk> \<Longrightarrow> g (aa * ba) = g aa * g ba; 0 < a; 0 < b; coprime a b\<rbrakk> \<Longrightarrow> g (a * b) = g a * g b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>r | r dvd a. \<Sum>d | d dvd b. if r * d = 1 then 0::'a else f (r * d) * g (a div r * (b div d))) = (\<Sum>r | r dvd a. \<Sum>d | d dvd b. if r * d = 1 then 0::'a else f r * f d * g (a div r) * g (b div d))

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<And>aa ba. \<lbrakk>aa * ba < a * b; 0 < aa; 0 < ba; coprime aa ba\<rbrakk> \<Longrightarrow> g (aa * ba) = g aa * g ba; 0 < a; 0 < b; coprime a b\<rbrakk> \<Longrightarrow> g (a * b) = g a * g b
[PROOF STEP]
have "\<dots> = (\<Sum>(r,d)\<in>{r. r dvd a}\<times>{d. d dvd b}.
                        if r * d = 1 then 0 else f r * f d * g (a div r) * g (b div d))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>r | r dvd a. \<Sum>d | d dvd b. if r * d = 1 then 0::'a else f r * f d * g (a div r) * g (b div d)) = (\<Sum>(r, d)\<in>{r. r dvd a} \<times> {d. d dvd b}. if r * d = 1 then 0::'a else f r * f d * g (a div r) * g (b div d))
[PROOF STEP]
by (simp add: sum.cartesian_product)
[PROOF STATE]
proof (state)
this:
(\<Sum>r | r dvd a. \<Sum>d | d dvd b. if r * d = 1 then 0::'a else f r * f d * g (a div r) * g (b div d)) = (\<Sum>(r, d)\<in>{r. r dvd a} \<times> {d. d dvd b}. if r * d = 1 then 0::'a else f r * f d * g (a div r) * g (b div d))

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<And>aa ba. \<lbrakk>aa * ba < a * b; 0 < aa; 0 < ba; coprime aa ba\<rbrakk> \<Longrightarrow> g (aa * ba) = g aa * g ba; 0 < a; 0 < b; coprime a b\<rbrakk> \<Longrightarrow> g (a * b) = g a * g b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>r | r dvd a. \<Sum>d | d dvd b. if r * d = 1 then 0::'a else f r * f d * g (a div r) * g (b div d)) = (\<Sum>(r, d)\<in>{r. r dvd a} \<times> {d. d dvd b}. if r * d = 1 then 0::'a else f r * f d * g (a div r) * g (b div d))

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<And>aa ba. \<lbrakk>aa * ba < a * b; 0 < aa; 0 < ba; coprime aa ba\<rbrakk> \<Longrightarrow> g (aa * ba) = g aa * g ba; 0 < a; 0 < b; coprime a b\<rbrakk> \<Longrightarrow> g (a * b) = g a * g b
[PROOF STEP]
have "\<dots> = (\<Sum>(r1,r2) \<in> {r1. r1 dvd a} \<times> {r2. r2 dvd b} - {(1,1)}.
                         (f r1 * f r2) * g (a div r1) * g (b div r2))" (is "_ = sum ?f ?A")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>(r, d)\<in>{r. r dvd a} \<times> {d. d dvd b}. if r * d = 1 then 0::'a else f r * f d * g (a div r) * g (b div d)) = (\<Sum>(r1, r2)\<in>{r1. r1 dvd a} \<times> {r2. r2 dvd b} - {(1, 1)}. f r1 * f r2 * g (a div r1) * g (b div r2))
[PROOF STEP]
using less.prems
[PROOF STATE]
proof (prove)
using this:
0 < a
0 < b
coprime a b

goal (1 subgoal):
 1. (\<Sum>(r, d)\<in>{r. r dvd a} \<times> {d. d dvd b}. if r * d = 1 then 0::'a else f r * f d * g (a div r) * g (b div d)) = (\<Sum>(r1, r2)\<in>{r1. r1 dvd a} \<times> {r2. r2 dvd b} - {(1, 1)}. f r1 * f r2 * g (a div r1) * g (b div r2))
[PROOF STEP]
by (intro sum.mono_neutral_cong_right) (auto split: if_splits)
[PROOF STATE]
proof (state)
this:
(\<Sum>(r, d)\<in>{r. r dvd a} \<times> {d. d dvd b}. if r * d = 1 then 0::'a else f r * f d * g (a div r) * g (b div d)) = (\<Sum>(r1, r2)\<in>{r1. r1 dvd a} \<times> {r2. r2 dvd b} - {(1, 1)}. f r1 * f r2 * g (a div r1) * g (b div r2))

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<And>aa ba. \<lbrakk>aa * ba < a * b; 0 < aa; 0 < ba; coprime aa ba\<rbrakk> \<Longrightarrow> g (aa * ba) = g aa * g ba; 0 < a; 0 < b; coprime a b\<rbrakk> \<Longrightarrow> g (a * b) = g a * g b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>(r, d)\<in>{r. r dvd a} \<times> {d. d dvd b}. if r * d = 1 then 0::'a else f r * f d * g (a div r) * g (b div d)) = (\<Sum>(r1, r2)\<in>{r1. r1 dvd a} \<times> {r2. r2 dvd b} - {(1, 1)}. f r1 * f r2 * g (a div r1) * g (b div r2))

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<And>aa ba. \<lbrakk>aa * ba < a * b; 0 < aa; 0 < ba; coprime aa ba\<rbrakk> \<Longrightarrow> g (aa * ba) = g aa * g ba; 0 < a; 0 < b; coprime a b\<rbrakk> \<Longrightarrow> g (a * b) = g a * g b
[PROOF STEP]
have "\<dots> + g a * g b = ?f (1, 1) + sum ?f ?A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>(r1, r2)\<in>{r1. r1 dvd a} \<times> {r2. r2 dvd b} - {(1, 1)}. f r1 * f r2 * g (a div r1) * g (b div r2)) + g a * g b = (case (1, 1) of (r1, r2) \<Rightarrow> f r1 * f r2 * g (a div r1) * g (b div r2)) + (\<Sum>(r1, r2)\<in>{r1. r1 dvd a} \<times> {r2. r2 dvd b} - {(1, 1)}. f r1 * f r2 * g (a div r1) * g (b div r2))
[PROOF STEP]
by (simp add: add_ac)
[PROOF STATE]
proof (state)
this:
(\<Sum>(r1, r2)\<in>{r1. r1 dvd a} \<times> {r2. r2 dvd b} - {(1, 1)}. f r1 * f r2 * g (a div r1) * g (b div r2)) + g a * g b = (case (1, 1) of (r1, r2) \<Rightarrow> f r1 * f r2 * g (a div r1) * g (b div r2)) + (\<Sum>(r1, r2)\<in>{r1. r1 dvd a} \<times> {r2. r2 dvd b} - {(1, 1)}. f r1 * f r2 * g (a div r1) * g (b div r2))

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<And>aa ba. \<lbrakk>aa * ba < a * b; 0 < aa; 0 < ba; coprime aa ba\<rbrakk> \<Longrightarrow> g (aa * ba) = g aa * g ba; 0 < a; 0 < b; coprime a b\<rbrakk> \<Longrightarrow> g (a * b) = g a * g b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>(r1, r2)\<in>{r1. r1 dvd a} \<times> {r2. r2 dvd b} - {(1, 1)}. f r1 * f r2 * g (a div r1) * g (b div r2)) + g a * g b = (case (1, 1) of (r1, r2) \<Rightarrow> f r1 * f r2 * g (a div r1) * g (b div r2)) + (\<Sum>(r1, r2)\<in>{r1. r1 dvd a} \<times> {r2. r2 dvd b} - {(1, 1)}. f r1 * f r2 * g (a div r1) * g (b div r2))

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<And>aa ba. \<lbrakk>aa * ba < a * b; 0 < aa; 0 < ba; coprime aa ba\<rbrakk> \<Longrightarrow> g (aa * ba) = g aa * g ba; 0 < a; 0 < b; coprime a b\<rbrakk> \<Longrightarrow> g (a * b) = g a * g b
[PROOF STEP]
have "\<dots> = sum ?f ({r1. r1 dvd a} \<times> {r2. r2 dvd b})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case (1, 1) of (r1, r2) \<Rightarrow> f r1 * f r2 * g (a div r1) * g (b div r2)) + (\<Sum>(r1, r2)\<in>{r1. r1 dvd a} \<times> {r2. r2 dvd b} - {(1, 1)}. f r1 * f r2 * g (a div r1) * g (b div r2)) = (\<Sum>(r1, r2)\<in>{r1. r1 dvd a} \<times> {r2. r2 dvd b}. f r1 * f r2 * g (a div r1) * g (b div r2))
[PROOF STEP]
using less.prems
[PROOF STATE]
proof (prove)
using this:
0 < a
0 < b
coprime a b

goal (1 subgoal):
 1. (case (1, 1) of (r1, r2) \<Rightarrow> f r1 * f r2 * g (a div r1) * g (b div r2)) + (\<Sum>(r1, r2)\<in>{r1. r1 dvd a} \<times> {r2. r2 dvd b} - {(1, 1)}. f r1 * f r2 * g (a div r1) * g (b div r2)) = (\<Sum>(r1, r2)\<in>{r1. r1 dvd a} \<times> {r2. r2 dvd b}. f r1 * f r2 * g (a div r1) * g (b div r2))
[PROOF STEP]
by (intro sum.remove [symmetric]) auto
[PROOF STATE]
proof (state)
this:
(case (1, 1) of (r1, r2) \<Rightarrow> f r1 * f r2 * g (a div r1) * g (b div r2)) + (\<Sum>(r1, r2)\<in>{r1. r1 dvd a} \<times> {r2. r2 dvd b} - {(1, 1)}. f r1 * f r2 * g (a div r1) * g (b div r2)) = (\<Sum>(r1, r2)\<in>{r1. r1 dvd a} \<times> {r2. r2 dvd b}. f r1 * f r2 * g (a div r1) * g (b div r2))

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<And>aa ba. \<lbrakk>aa * ba < a * b; 0 < aa; 0 < ba; coprime aa ba\<rbrakk> \<Longrightarrow> g (aa * ba) = g aa * g ba; 0 < a; 0 < b; coprime a b\<rbrakk> \<Longrightarrow> g (a * b) = g a * g b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(case (1, 1) of (r1, r2) \<Rightarrow> f r1 * f r2 * g (a div r1) * g (b div r2)) + (\<Sum>(r1, r2)\<in>{r1. r1 dvd a} \<times> {r2. r2 dvd b} - {(1, 1)}. f r1 * f r2 * g (a div r1) * g (b div r2)) = (\<Sum>(r1, r2)\<in>{r1. r1 dvd a} \<times> {r2. r2 dvd b}. f r1 * f r2 * g (a div r1) * g (b div r2))

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<And>aa ba. \<lbrakk>aa * ba < a * b; 0 < aa; 0 < ba; coprime aa ba\<rbrakk> \<Longrightarrow> g (aa * ba) = g aa * g ba; 0 < a; 0 < b; coprime a b\<rbrakk> \<Longrightarrow> g (a * b) = g a * g b
[PROOF STEP]
have "\<dots> = dirichlet_prod f g a * dirichlet_prod f g b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>(r1, r2)\<in>{r1. r1 dvd a} \<times> {r2. r2 dvd b}. f r1 * f r2 * g (a div r1) * g (b div r2)) = dirichlet_prod f g a * dirichlet_prod f g b
[PROOF STEP]
by (simp add: sum.cartesian_product sum_product dirichlet_prod_def mult_ac)
[PROOF STATE]
proof (state)
this:
(\<Sum>(r1, r2)\<in>{r1. r1 dvd a} \<times> {r2. r2 dvd b}. f r1 * f r2 * g (a div r1) * g (b div r2)) = dirichlet_prod f g a * dirichlet_prod f g b

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<And>aa ba. \<lbrakk>aa * ba < a * b; 0 < aa; 0 < ba; coprime aa ba\<rbrakk> \<Longrightarrow> g (aa * ba) = g aa * g ba; 0 < a; 0 < b; coprime a b\<rbrakk> \<Longrightarrow> g (a * b) = g a * g b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>(r1, r2)\<in>{r1. r1 dvd a} \<times> {r2. r2 dvd b}. f r1 * f r2 * g (a div r1) * g (b div r2)) = dirichlet_prod f g a * dirichlet_prod f g b

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<And>aa ba. \<lbrakk>aa * ba < a * b; 0 < aa; 0 < ba; coprime aa ba\<rbrakk> \<Longrightarrow> g (aa * ba) = g aa * g ba; 0 < a; 0 < b; coprime a b\<rbrakk> \<Longrightarrow> g (a * b) = g a * g b
[PROOF STEP]
have "g (a * b) + dirichlet_prod f g a * dirichlet_prod f g b =
                   dirichlet_prod f g (a * b) + g (a * b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g (a * b) + dirichlet_prod f g a * dirichlet_prod f g b = dirichlet_prod f g (a * b) + g (a * b)
[PROOF STEP]
using less.prems
[PROOF STATE]
proof (prove)
using this:
0 < a
0 < b
coprime a b

goal (1 subgoal):
 1. g (a * b) + dirichlet_prod f g a * dirichlet_prod f g b = dirichlet_prod f g (a * b) + g (a * b)
[PROOF STEP]
by (simp add: fg.mult_coprime add_ac)
[PROOF STATE]
proof (state)
this:
g (a * b) + dirichlet_prod f g a * dirichlet_prod f g b = dirichlet_prod f g (a * b) + g (a * b)

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<And>aa ba. \<lbrakk>aa * ba < a * b; 0 < aa; 0 < ba; coprime aa ba\<rbrakk> \<Longrightarrow> g (aa * ba) = g aa * g ba; 0 < a; 0 < b; coprime a b\<rbrakk> \<Longrightarrow> g (a * b) = g a * g b
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dirichlet_prod f g (a * b) + g a * g b = dirichlet_prod f g (a * b) + g (a * b)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
dirichlet_prod f g (a * b) + g a * g b = dirichlet_prod f g (a * b) + g (a * b)

goal (1 subgoal):
 1. g (a * b) = g a * g b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
g (a * b) = g a * g b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
g (a * b) = g a * g b

goal (1 subgoal):
 1. g 0 = (0::'a)
[PROOF STEP]
qed simp_all
[PROOF STATE]
proof (state)
this:
multiplicative_function g

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma multiplicative_dirichlet_prodD2:
  fixes f g :: "nat \<Rightarrow> 'a :: comm_semiring_1_cancel"
  assumes "multiplicative_function (dirichlet_prod f g)"
  assumes "multiplicative_function g"
  assumes [simp]: "f 0 = 0"
  shows   "multiplicative_function f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicative_function f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. multiplicative_function f
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
multiplicative_function (dirichlet_prod f g)
[PROOF STEP]
have "multiplicative_function (dirichlet_prod g f)"
[PROOF STATE]
proof (prove)
using this:
multiplicative_function (dirichlet_prod f g)

goal (1 subgoal):
 1. multiplicative_function (dirichlet_prod g f)
[PROOF STEP]
by (simp add: dirichlet_prod_commutes)
[PROOF STATE]
proof (state)
this:
multiplicative_function (dirichlet_prod g f)

goal (1 subgoal):
 1. multiplicative_function f
[PROOF STEP]
from multiplicative_dirichlet_prodD1[OF this assms(2)]
[PROOF STATE]
proof (chain)
picking this:
f 0 = (0::'a) \<Longrightarrow> multiplicative_function f
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f 0 = (0::'a) \<Longrightarrow> multiplicative_function f

goal (1 subgoal):
 1. multiplicative_function f
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
multiplicative_function f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma multiplicative_dirichlet_inverse:
  assumes "multiplicative_function f"
  shows   "multiplicative_function (dirichlet_inverse f 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicative_function (dirichlet_inverse f (1::'a))
[PROOF STEP]
proof (rule multiplicative_dirichlet_prodD1[OF _ assms])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. multiplicative_function (dirichlet_prod f (dirichlet_inverse f (1::'a)))
 2. dirichlet_inverse f (1::'a) 0 = (0::'a)
[PROOF STEP]
interpret multiplicative_function f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicative_function f
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. multiplicative_function (dirichlet_prod f (dirichlet_inverse f (1::'a)))
 2. dirichlet_inverse f (1::'a) 0 = (0::'a)
[PROOF STEP]
have "multiplicative_function (\<lambda>n. if n = 1 then 1 else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicative_function (\<lambda>n. if n = 1 then 1::'b else (0::'b))
[PROOF STEP]
by standard simp_all
[PROOF STATE]
proof (state)
this:
multiplicative_function (\<lambda>n. if n = 1 then 1::?'b1 else (0::?'b1))

goal (2 subgoals):
 1. multiplicative_function (dirichlet_prod f (dirichlet_inverse f (1::'a)))
 2. dirichlet_inverse f (1::'a) 0 = (0::'a)
[PROOF STEP]
thus "multiplicative_function (dirichlet_prod f (dirichlet_inverse f 1))"
[PROOF STATE]
proof (prove)
using this:
multiplicative_function (\<lambda>n. if n = 1 then 1::?'b1 else (0::?'b1))

goal (1 subgoal):
 1. multiplicative_function (dirichlet_prod f (dirichlet_inverse f (1::'a)))
[PROOF STEP]
by (subst dirichlet_prod_inverse) simp_all
[PROOF STATE]
proof (state)
this:
multiplicative_function (dirichlet_prod f (dirichlet_inverse f (1::'a)))

goal (1 subgoal):
 1. dirichlet_inverse f (1::'a) 0 = (0::'a)
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma dirichlet_prod_prime_power:
  assumes "prime p"
  shows   "dirichlet_prod f g (p ^ k) = (\<Sum>i\<le>k. f (p ^ i) * g (p ^ (k - i)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dirichlet_prod f g (p ^ k) = (\<Sum>i\<le>k. f (p ^ i) * g (p ^ (k - i)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dirichlet_prod f g (p ^ k) = (\<Sum>i\<le>k. f (p ^ i) * g (p ^ (k - i)))
[PROOF STEP]
have "dirichlet_prod f g (p ^ k) = (\<Sum>i\<le>k. f (p ^ i) * g (p ^ k div p ^ i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dirichlet_prod f g (p ^ k) = (\<Sum>i\<le>k. f (p ^ i) * g (p ^ k div p ^ i))
[PROOF STEP]
unfolding dirichlet_prod_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>d | d dvd p ^ k. f d * g (p ^ k div d)) = (\<Sum>i\<le>k. f (p ^ i) * g (p ^ k div p ^ i))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
prime p

goal (1 subgoal):
 1. (\<Sum>d | d dvd p ^ k. f d * g (p ^ k div d)) = (\<Sum>i\<le>k. f (p ^ i) * g (p ^ k div p ^ i))
[PROOF STEP]
by (intro sum.reindex_bij_betw [symmetric] bij_betw_prime_power_divisors)
[PROOF STATE]
proof (state)
this:
dirichlet_prod f g (p ^ k) = (\<Sum>i\<le>k. f (p ^ i) * g (p ^ k div p ^ i))

goal (1 subgoal):
 1. dirichlet_prod f g (p ^ k) = (\<Sum>i\<le>k. f (p ^ i) * g (p ^ (k - i)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dirichlet_prod f g (p ^ k) = (\<Sum>i\<le>k. f (p ^ i) * g (p ^ k div p ^ i))

goal (1 subgoal):
 1. dirichlet_prod f g (p ^ k) = (\<Sum>i\<le>k. f (p ^ i) * g (p ^ (k - i)))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
prime p
[PROOF STEP]
have "\<dots> = (\<Sum>i\<le>k. f (p ^ i) * g (p ^ (k - i)))"
[PROOF STATE]
proof (prove)
using this:
prime p

goal (1 subgoal):
 1. (\<Sum>i\<le>k. f (p ^ i) * g (p ^ k div p ^ i)) = (\<Sum>i\<le>k. f (p ^ i) * g (p ^ (k - i)))
[PROOF STEP]
by (intro sum.cong refl) (auto simp: power_diff')
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<le>k. f (p ^ i) * g (p ^ k div p ^ i)) = (\<Sum>i\<le>k. f (p ^ i) * g (p ^ (k - i)))

goal (1 subgoal):
 1. dirichlet_prod f g (p ^ k) = (\<Sum>i\<le>k. f (p ^ i) * g (p ^ (k - i)))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dirichlet_prod f g (p ^ k) = (\<Sum>i\<le>k. f (p ^ i) * g (p ^ (k - i)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dirichlet_prod f g (p ^ k) = (\<Sum>i\<le>k. f (p ^ i) * g (p ^ (k - i)))

goal (1 subgoal):
 1. dirichlet_prod f g (p ^ k) = (\<Sum>i\<le>k. f (p ^ i) * g (p ^ (k - i)))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
dirichlet_prod f g (p ^ k) = (\<Sum>i\<le>k. f (p ^ i) * g (p ^ (k - i)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dirichlet_prod_prime:
  assumes "prime p"
  shows   "dirichlet_prod f g p  = f 1 * g p + f p * g 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dirichlet_prod f g p = f 1 * g p + f p * g 1
[PROOF STEP]
using dirichlet_prod_prime_power[of p f g 1] assms
[PROOF STATE]
proof (prove)
using this:
prime p \<Longrightarrow> dirichlet_prod f g (p ^ 1) = (\<Sum>i\<le>1. f (p ^ i) * g (p ^ (1 - i)))
prime p

goal (1 subgoal):
 1. dirichlet_prod f g p = f 1 * g p + f p * g 1
[PROOF STEP]
by simp