[STATEMENT]
lemma multiplicity_Lcm:
  fixes A :: "'a :: {semiring_Gcd, factorial_semiring_gcd} set"
  assumes "finite A" "A \<noteq> {}" "prime p" "0 \<notin> A"
  shows   "multiplicity p (Lcm A) = Max (multiplicity p ` A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicity p (Lcm A) = Max (multiplicity p ` A)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite A
A \<noteq> {}
prime p
(0::'a) \<notin> A

goal (1 subgoal):
 1. multiplicity p (Lcm A) = Max (multiplicity p ` A)
[PROOF STEP]
proof (induction A rule: finite_ne_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>prime p; (0::'a) \<notin> {x}\<rbrakk> \<Longrightarrow> multiplicity p (Lcm {x}) = Max (multiplicity p ` {x})
 2. \<And>x F. \<lbrakk>finite F; F \<noteq> {}; x \<notin> F; \<lbrakk>prime p; (0::'a) \<notin> F\<rbrakk> \<Longrightarrow> multiplicity p (Lcm F) = Max (multiplicity p ` F); prime p; (0::'a) \<notin> insert x F\<rbrakk> \<Longrightarrow> multiplicity p (Lcm (insert x F)) = Max (multiplicity p ` insert x F)
[PROOF STEP]
case (insert x A)
[PROOF STATE]
proof (state)
this:
finite A
A \<noteq> {}
x \<notin> A
\<lbrakk>prime p; (0::'a) \<notin> A\<rbrakk> \<Longrightarrow> multiplicity p (Lcm A) = Max (multiplicity p ` A)
prime p
(0::'a) \<notin> insert x A

goal (2 subgoals):
 1. \<And>x. \<lbrakk>prime p; (0::'a) \<notin> {x}\<rbrakk> \<Longrightarrow> multiplicity p (Lcm {x}) = Max (multiplicity p ` {x})
 2. \<And>x F. \<lbrakk>finite F; F \<noteq> {}; x \<notin> F; \<lbrakk>prime p; (0::'a) \<notin> F\<rbrakk> \<Longrightarrow> multiplicity p (Lcm F) = Max (multiplicity p ` F); prime p; (0::'a) \<notin> insert x F\<rbrakk> \<Longrightarrow> multiplicity p (Lcm (insert x F)) = Max (multiplicity p ` insert x F)
[PROOF STEP]
have "Lcm (insert x A) = lcm x (Lcm A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Lcm (insert x A) = lcm x (Lcm A)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Lcm (insert x A) = lcm x (Lcm A)

goal (2 subgoals):
 1. \<And>x. \<lbrakk>prime p; (0::'a) \<notin> {x}\<rbrakk> \<Longrightarrow> multiplicity p (Lcm {x}) = Max (multiplicity p ` {x})
 2. \<And>x F. \<lbrakk>finite F; F \<noteq> {}; x \<notin> F; \<lbrakk>prime p; (0::'a) \<notin> F\<rbrakk> \<Longrightarrow> multiplicity p (Lcm F) = Max (multiplicity p ` F); prime p; (0::'a) \<notin> insert x F\<rbrakk> \<Longrightarrow> multiplicity p (Lcm (insert x F)) = Max (multiplicity p ` insert x F)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Lcm (insert x A) = lcm x (Lcm A)

goal (2 subgoals):
 1. \<And>x. \<lbrakk>prime p; (0::'a) \<notin> {x}\<rbrakk> \<Longrightarrow> multiplicity p (Lcm {x}) = Max (multiplicity p ` {x})
 2. \<And>x F. \<lbrakk>finite F; F \<noteq> {}; x \<notin> F; \<lbrakk>prime p; (0::'a) \<notin> F\<rbrakk> \<Longrightarrow> multiplicity p (Lcm F) = Max (multiplicity p ` F); prime p; (0::'a) \<notin> insert x F\<rbrakk> \<Longrightarrow> multiplicity p (Lcm (insert x F)) = Max (multiplicity p ` insert x F)
[PROOF STEP]
have "multiplicity p \<dots> = Max (multiplicity p ` insert x A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicity p (lcm x (Lcm A)) = Max (multiplicity p ` insert x A)
[PROOF STEP]
using insert
[PROOF STATE]
proof (prove)
using this:
finite A
A \<noteq> {}
x \<notin> A
\<lbrakk>prime p; (0::'a) \<notin> A\<rbrakk> \<Longrightarrow> multiplicity p (Lcm A) = Max (multiplicity p ` A)
prime p
(0::'a) \<notin> insert x A

goal (1 subgoal):
 1. multiplicity p (lcm x (Lcm A)) = Max (multiplicity p ` insert x A)
[PROOF STEP]
by (subst multiplicity_lcm) (auto simp: Lcm_0_iff)
[PROOF STATE]
proof (state)
this:
multiplicity p (lcm x (Lcm A)) = Max (multiplicity p ` insert x A)

goal (2 subgoals):
 1. \<And>x. \<lbrakk>prime p; (0::'a) \<notin> {x}\<rbrakk> \<Longrightarrow> multiplicity p (Lcm {x}) = Max (multiplicity p ` {x})
 2. \<And>x F. \<lbrakk>finite F; F \<noteq> {}; x \<notin> F; \<lbrakk>prime p; (0::'a) \<notin> F\<rbrakk> \<Longrightarrow> multiplicity p (Lcm F) = Max (multiplicity p ` F); prime p; (0::'a) \<notin> insert x F\<rbrakk> \<Longrightarrow> multiplicity p (Lcm (insert x F)) = Max (multiplicity p ` insert x F)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
multiplicity p (Lcm (insert x A)) = Max (multiplicity p ` insert x A)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
multiplicity p (Lcm (insert x A)) = Max (multiplicity p ` insert x A)

goal (1 subgoal):
 1. multiplicity p (Lcm (insert x A)) = Max (multiplicity p ` insert x A)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
multiplicity p (Lcm (insert x A)) = Max (multiplicity p ` insert x A)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>prime p; (0::'a) \<notin> {x}\<rbrakk> \<Longrightarrow> multiplicity p (Lcm {x}) = Max (multiplicity p ` {x})
[PROOF STEP]
qed auto