[STATEMENT]
lemma lindemann_weierstrass_integral_bound:
  fixes u :: complex
  assumes "C \<ge> 0" "\<And>t. t \<in> closed_segment 0 u \<Longrightarrow> norm (poly f t) \<le> C"
  shows "norm (I u) \<le> norm u * exp (norm u) * C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod (I u) \<le> cmod u * exp (cmod u) * C
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cmod (I u) \<le> cmod u * exp (cmod u) * C
[PROOF STEP]
have "I u = contour_integral (linepath 0 u) (\<lambda>t. exp (u - t) * poly f t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I u = contour_integral (linepath 0 u) (\<lambda>t. exp (u - t) * poly f t)
[PROOF STEP]
using contour_integral_unique[OF lindemann_weierstrass_integral[of u f]]
[PROOF STATE]
proof (prove)
using this:
contour_integral (linepath 0 u) (\<lambda>t. exp (u - t) * poly f t) = exp u * (\<Sum>j\<le>degree f. poly ((pderiv ^^ j) f) 0) - (\<Sum>j\<le>degree f. poly ((pderiv ^^ j) f) u)

goal (1 subgoal):
 1. I u = contour_integral (linepath 0 u) (\<lambda>t. exp (u - t) * poly f t)
[PROOF STEP]
unfolding I_def
[PROOF STATE]
proof (prove)
using this:
contour_integral (linepath 0 u) (\<lambda>t. exp (u - t) * poly f t) = exp u * (\<Sum>j\<le>degree f. poly ((pderiv ^^ j) f) 0) - (\<Sum>j\<le>degree f. poly ((pderiv ^^ j) f) u)

goal (1 subgoal):
 1. exp u * (\<Sum>j\<le>degree f. poly ((pderiv ^^ j) f) 0) - (\<Sum>j\<le>degree f. poly ((pderiv ^^ j) f) u) = contour_integral (linepath 0 u) (\<lambda>t. exp (u - t) * poly f t)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
I u = contour_integral (linepath 0 u) (\<lambda>t. exp (u - t) * poly f t)

goal (1 subgoal):
 1. cmod (I u) \<le> cmod u * exp (cmod u) * C
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
I u = contour_integral (linepath 0 u) (\<lambda>t. exp (u - t) * poly f t)

goal (1 subgoal):
 1. cmod (I u) \<le> cmod u * exp (cmod u) * C
[PROOF STEP]
have "norm \<dots> \<le> exp (norm u) * C * norm (u - 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod (contour_integral (linepath 0 u) (\<lambda>t. exp (u - t) * poly f t)) \<le> exp (cmod u) * C * cmod (u - 0)
[PROOF STEP]
proof (intro contour_integral_bound_linepath)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. (\<lambda>t. exp (u - t) * poly f t) contour_integrable_on linepath 0 u
 2. 0 \<le> exp (cmod u) * C
 3. \<And>x. x \<in> closed_segment 0 u \<Longrightarrow> cmod (exp (u - x) * poly f x) \<le> exp (cmod u) * C
[PROOF STEP]
fix t
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. (\<lambda>t. exp (u - t) * poly f t) contour_integrable_on linepath 0 u
 2. 0 \<le> exp (cmod u) * C
 3. \<And>x. x \<in> closed_segment 0 u \<Longrightarrow> cmod (exp (u - x) * poly f x) \<le> exp (cmod u) * C
[PROOF STEP]
assume t: "t \<in> closed_segment 0 u"
[PROOF STATE]
proof (state)
this:
t \<in> closed_segment 0 u

goal (3 subgoals):
 1. (\<lambda>t. exp (u - t) * poly f t) contour_integrable_on linepath 0 u
 2. 0 \<le> exp (cmod u) * C
 3. \<And>x. x \<in> closed_segment 0 u \<Longrightarrow> cmod (exp (u - x) * poly f x) \<le> exp (cmod u) * C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t \<in> closed_segment 0 u
[PROOF STEP]
obtain s where s: "s \<in> {0..1}" "t = s *\<^sub>R u"
[PROOF STATE]
proof (prove)
using this:
t \<in> closed_segment 0 u

goal (1 subgoal):
 1. (\<And>s. \<lbrakk>s \<in> {0..1}; t = s *\<^sub>R u\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: closed_segment_def)
[PROOF STATE]
proof (state)
this:
s \<in> {0..1}
t = s *\<^sub>R u

goal (3 subgoals):
 1. (\<lambda>t. exp (u - t) * poly f t) contour_integrable_on linepath 0 u
 2. 0 \<le> exp (cmod u) * C
 3. \<And>x. x \<in> closed_segment 0 u \<Longrightarrow> cmod (exp (u - x) * poly f x) \<le> exp (cmod u) * C
[PROOF STEP]
hence "s * norm u \<le> 1 * norm u"
[PROOF STATE]
proof (prove)
using this:
s \<in> {0..1}
t = s *\<^sub>R u

goal (1 subgoal):
 1. s * cmod u \<le> 1 * cmod u
[PROOF STEP]
by (intro mult_right_mono) simp_all
[PROOF STATE]
proof (state)
this:
s * cmod u \<le> 1 * cmod u

goal (3 subgoals):
 1. (\<lambda>t. exp (u - t) * poly f t) contour_integrable_on linepath 0 u
 2. 0 \<le> exp (cmod u) * C
 3. \<And>x. x \<in> closed_segment 0 u \<Longrightarrow> cmod (exp (u - x) * poly f x) \<le> exp (cmod u) * C
[PROOF STEP]
with s
[PROOF STATE]
proof (chain)
picking this:
s \<in> {0..1}
t = s *\<^sub>R u
s * cmod u \<le> 1 * cmod u
[PROOF STEP]
have norm_t: "norm t \<le> norm u"
[PROOF STATE]
proof (prove)
using this:
s \<in> {0..1}
t = s *\<^sub>R u
s * cmod u \<le> 1 * cmod u

goal (1 subgoal):
 1. cmod t \<le> cmod u
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cmod t \<le> cmod u

goal (3 subgoals):
 1. (\<lambda>t. exp (u - t) * poly f t) contour_integrable_on linepath 0 u
 2. 0 \<le> exp (cmod u) * C
 3. \<And>x. x \<in> closed_segment 0 u \<Longrightarrow> cmod (exp (u - x) * poly f x) \<le> exp (cmod u) * C
[PROOF STEP]
from s
[PROOF STATE]
proof (chain)
picking this:
s \<in> {0..1}
t = s *\<^sub>R u
[PROOF STEP]
have "Re u - Re t = (1 - s) * Re u"
[PROOF STATE]
proof (prove)
using this:
s \<in> {0..1}
t = s *\<^sub>R u

goal (1 subgoal):
 1. Re u - Re t = (1 - s) * Re u
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
Re u - Re t = (1 - s) * Re u

goal (3 subgoals):
 1. (\<lambda>t. exp (u - t) * poly f t) contour_integrable_on linepath 0 u
 2. 0 \<le> exp (cmod u) * C
 3. \<And>x. x \<in> closed_segment 0 u \<Longrightarrow> cmod (exp (u - x) * poly f x) \<le> exp (cmod u) * C
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Re u - Re t = (1 - s) * Re u

goal (3 subgoals):
 1. (\<lambda>t. exp (u - t) * poly f t) contour_integrable_on linepath 0 u
 2. 0 \<le> exp (cmod u) * C
 3. \<And>x. x \<in> closed_segment 0 u \<Longrightarrow> cmod (exp (u - x) * poly f x) \<le> exp (cmod u) * C
[PROOF STEP]
have "\<dots> \<le> norm u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1 - s) * Re u \<le> cmod u
[PROOF STEP]
proof (cases "Re u \<ge> 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 \<le> Re u \<Longrightarrow> (1 - s) * Re u \<le> cmod u
 2. \<not> 0 \<le> Re u \<Longrightarrow> (1 - s) * Re u \<le> cmod u
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
0 \<le> Re u

goal (2 subgoals):
 1. 0 \<le> Re u \<Longrightarrow> (1 - s) * Re u \<le> cmod u
 2. \<not> 0 \<le> Re u \<Longrightarrow> (1 - s) * Re u \<le> cmod u
[PROOF STEP]
with \<open>s \<in> {0..1}\<close>
[PROOF STATE]
proof (chain)
picking this:
s \<in> {0..1}
0 \<le> Re u
[PROOF STEP]
have "(1 - s) * Re u \<le> 1 * Re u"
[PROOF STATE]
proof (prove)
using this:
s \<in> {0..1}
0 \<le> Re u

goal (1 subgoal):
 1. (1 - s) * Re u \<le> 1 * Re u
[PROOF STEP]
by (intro mult_right_mono) simp_all
[PROOF STATE]
proof (state)
this:
(1 - s) * Re u \<le> 1 * Re u

goal (2 subgoals):
 1. 0 \<le> Re u \<Longrightarrow> (1 - s) * Re u \<le> cmod u
 2. \<not> 0 \<le> Re u \<Longrightarrow> (1 - s) * Re u \<le> cmod u
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(1 - s) * Re u \<le> 1 * Re u

goal (2 subgoals):
 1. 0 \<le> Re u \<Longrightarrow> (1 - s) * Re u \<le> cmod u
 2. \<not> 0 \<le> Re u \<Longrightarrow> (1 - s) * Re u \<le> cmod u
[PROOF STEP]
have "Re u \<le> norm u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Re u \<le> cmod u
[PROOF STEP]
by (rule complex_Re_le_cmod)
[PROOF STATE]
proof (state)
this:
Re u \<le> cmod u

goal (2 subgoals):
 1. 0 \<le> Re u \<Longrightarrow> (1 - s) * Re u \<le> cmod u
 2. \<not> 0 \<le> Re u \<Longrightarrow> (1 - s) * Re u \<le> cmod u
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<And>x y. x \<le> y \<Longrightarrow> 1 * x \<le> 1 * y) \<Longrightarrow> (1 - s) * Re u \<le> 1 * cmod u
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<And>x y. x \<le> y \<Longrightarrow> 1 * x \<le> 1 * y) \<Longrightarrow> (1 - s) * Re u \<le> 1 * cmod u

goal (1 subgoal):
 1. (1 - s) * Re u \<le> cmod u
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(1 - s) * Re u \<le> cmod u

goal (1 subgoal):
 1. \<not> 0 \<le> Re u \<Longrightarrow> (1 - s) * Re u \<le> cmod u
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> 0 \<le> Re u \<Longrightarrow> (1 - s) * Re u \<le> cmod u
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> 0 \<le> Re u

goal (1 subgoal):
 1. \<not> 0 \<le> Re u \<Longrightarrow> (1 - s) * Re u \<le> cmod u
[PROOF STEP]
with \<open>s \<in> {0..1}\<close>
[PROOF STATE]
proof (chain)
picking this:
s \<in> {0..1}
\<not> 0 \<le> Re u
[PROOF STEP]
have "(1 - s) * Re u \<le> 0"
[PROOF STATE]
proof (prove)
using this:
s \<in> {0..1}
\<not> 0 \<le> Re u

goal (1 subgoal):
 1. (1 - s) * Re u \<le> 0
[PROOF STEP]
by (intro mult_nonneg_nonpos) simp_all
[PROOF STATE]
proof (state)
this:
(1 - s) * Re u \<le> 0

goal (1 subgoal):
 1. \<not> 0 \<le> Re u \<Longrightarrow> (1 - s) * Re u \<le> cmod u
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(1 - s) * Re u \<le> 0

goal (1 subgoal):
 1. \<not> 0 \<le> Re u \<Longrightarrow> (1 - s) * Re u \<le> cmod u
[PROOF STEP]
have "\<dots> \<le> norm u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> cmod u
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 \<le> cmod u

goal (1 subgoal):
 1. \<not> 0 \<le> Re u \<Longrightarrow> (1 - s) * Re u \<le> cmod u
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(1 - s) * Re u \<le> cmod u
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(1 - s) * Re u \<le> cmod u

goal (1 subgoal):
 1. (1 - s) * Re u \<le> cmod u
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(1 - s) * Re u \<le> cmod u

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(1 - s) * Re u \<le> cmod u

goal (3 subgoals):
 1. (\<lambda>t. exp (u - t) * poly f t) contour_integrable_on linepath 0 u
 2. 0 \<le> exp (cmod u) * C
 3. \<And>x. x \<in> closed_segment 0 u \<Longrightarrow> cmod (exp (u - x) * poly f x) \<le> exp (cmod u) * C
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Re u - Re t \<le> cmod u
[PROOF STEP]
have "exp (Re u - Re t) \<le> exp (norm u)"
[PROOF STATE]
proof (prove)
using this:
Re u - Re t \<le> cmod u

goal (1 subgoal):
 1. exp (Re u - Re t) \<le> exp (cmod u)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
exp (Re u - Re t) \<le> exp (cmod u)

goal (3 subgoals):
 1. (\<lambda>t. exp (u - t) * poly f t) contour_integrable_on linepath 0 u
 2. 0 \<le> exp (cmod u) * C
 3. \<And>x. x \<in> closed_segment 0 u \<Longrightarrow> cmod (exp (u - x) * poly f x) \<le> exp (cmod u) * C
[PROOF STEP]
hence "exp (Re u - Re t) * norm (poly f t) \<le> exp (norm u) * C"
[PROOF STATE]
proof (prove)
using this:
exp (Re u - Re t) \<le> exp (cmod u)

goal (1 subgoal):
 1. exp (Re u - Re t) * cmod (poly f t) \<le> exp (cmod u) * C
[PROOF STEP]
using assms t norm_t
[PROOF STATE]
proof (prove)
using this:
exp (Re u - Re t) \<le> exp (cmod u)
0 \<le> C
?t \<in> closed_segment 0 u \<Longrightarrow> cmod (poly f ?t) \<le> C
t \<in> closed_segment 0 u
cmod t \<le> cmod u

goal (1 subgoal):
 1. exp (Re u - Re t) * cmod (poly f t) \<le> exp (cmod u) * C
[PROOF STEP]
by (intro mult_mono) simp_all
[PROOF STATE]
proof (state)
this:
exp (Re u - Re t) * cmod (poly f t) \<le> exp (cmod u) * C

goal (3 subgoals):
 1. (\<lambda>t. exp (u - t) * poly f t) contour_integrable_on linepath 0 u
 2. 0 \<le> exp (cmod u) * C
 3. \<And>x. x \<in> closed_segment 0 u \<Longrightarrow> cmod (exp (u - x) * poly f x) \<le> exp (cmod u) * C
[PROOF STEP]
thus "norm (exp (u - t) * poly f t) \<le> exp (norm u) * C"
[PROOF STATE]
proof (prove)
using this:
exp (Re u - Re t) * cmod (poly f t) \<le> exp (cmod u) * C

goal (1 subgoal):
 1. cmod (exp (u - t) * poly f t) \<le> exp (cmod u) * C
[PROOF STEP]
by (simp add: norm_mult exp_diff norm_divide field_simps)
[PROOF STATE]
proof (state)
this:
cmod (exp (u - t) * poly f t) \<le> exp (cmod u) * C

goal (2 subgoals):
 1. (\<lambda>t. exp (u - t) * poly f t) contour_integrable_on linepath 0 u
 2. 0 \<le> exp (cmod u) * C
[PROOF STEP]
qed (auto simp: intro!: mult_nonneg_nonneg contour_integrable_continuous_linepath
                          continuous_intros assms)
[PROOF STATE]
proof (state)
this:
cmod (contour_integral (linepath 0 u) (\<lambda>t. exp (u - t) * poly f t)) \<le> exp (cmod u) * C * cmod (u - 0)

goal (1 subgoal):
 1. cmod (I u) \<le> cmod u * exp (cmod u) * C
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
cmod (I u) \<le> exp (cmod u) * C * cmod (u - 0)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cmod (I u) \<le> exp (cmod u) * C * cmod (u - 0)

goal (1 subgoal):
 1. cmod (I u) \<le> cmod u * exp (cmod u) * C
[PROOF STEP]
by (simp add: mult_ac)
[PROOF STATE]
proof (state)
this:
cmod (I u) \<le> cmod u * exp (cmod u) * C

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma poly_higher_pderiv_aux1:
  fixes c :: "'a :: idom"
  assumes "k < n"
  shows   "poly ((pderiv ^^ k) ([:-c, 1:] ^ n * p)) c = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly ((pderiv ^^ k) ([:- c, 1::'a:] ^ n * p)) c = (0::'a)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
k < n

goal (1 subgoal):
 1. poly ((pderiv ^^ k) ([:- c, 1::'a:] ^ n * p)) c = (0::'a)
[PROOF STEP]
proof (induction k arbitrary: n p)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n p. 0 < n \<Longrightarrow> poly ((pderiv ^^ 0) ([:- c, 1::'a:] ^ n * p)) c = (0::'a)
 2. \<And>k n p. \<lbrakk>\<And>n p. k < n \<Longrightarrow> poly ((pderiv ^^ k) ([:- c, 1::'a:] ^ n * p)) c = (0::'a); Suc k < n\<rbrakk> \<Longrightarrow> poly ((pderiv ^^ Suc k) ([:- c, 1::'a:] ^ n * p)) c = (0::'a)
[PROOF STEP]
case (Suc k n p)
[PROOF STATE]
proof (state)
this:
k < ?n \<Longrightarrow> poly ((pderiv ^^ k) ([:- c, 1::'a:] ^ ?n * ?p)) c = (0::'a)
Suc k < n

goal (2 subgoals):
 1. \<And>n p. 0 < n \<Longrightarrow> poly ((pderiv ^^ 0) ([:- c, 1::'a:] ^ n * p)) c = (0::'a)
 2. \<And>k n p. \<lbrakk>\<And>n p. k < n \<Longrightarrow> poly ((pderiv ^^ k) ([:- c, 1::'a:] ^ n * p)) c = (0::'a); Suc k < n\<rbrakk> \<Longrightarrow> poly ((pderiv ^^ Suc k) ([:- c, 1::'a:] ^ n * p)) c = (0::'a)
[PROOF STEP]
from Suc.prems
[PROOF STATE]
proof (chain)
picking this:
Suc k < n
[PROOF STEP]
obtain n' where n: "n = Suc n'"
[PROOF STATE]
proof (prove)
using this:
Suc k < n

goal (1 subgoal):
 1. (\<And>n'. n = Suc n' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases n) auto
[PROOF STATE]
proof (state)
this:
n = Suc n'

goal (2 subgoals):
 1. \<And>n p. 0 < n \<Longrightarrow> poly ((pderiv ^^ 0) ([:- c, 1::'a:] ^ n * p)) c = (0::'a)
 2. \<And>k n p. \<lbrakk>\<And>n p. k < n \<Longrightarrow> poly ((pderiv ^^ k) ([:- c, 1::'a:] ^ n * p)) c = (0::'a); Suc k < n\<rbrakk> \<Longrightarrow> poly ((pderiv ^^ Suc k) ([:- c, 1::'a:] ^ n * p)) c = (0::'a)
[PROOF STEP]
from Suc.prems n
[PROOF STATE]
proof (chain)
picking this:
Suc k < n
n = Suc n'
[PROOF STEP]
have "k < n'"
[PROOF STATE]
proof (prove)
using this:
Suc k < n
n = Suc n'

goal (1 subgoal):
 1. k < n'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
k < n'

goal (2 subgoals):
 1. \<And>n p. 0 < n \<Longrightarrow> poly ((pderiv ^^ 0) ([:- c, 1::'a:] ^ n * p)) c = (0::'a)
 2. \<And>k n p. \<lbrakk>\<And>n p. k < n \<Longrightarrow> poly ((pderiv ^^ k) ([:- c, 1::'a:] ^ n * p)) c = (0::'a); Suc k < n\<rbrakk> \<Longrightarrow> poly ((pderiv ^^ Suc k) ([:- c, 1::'a:] ^ n * p)) c = (0::'a)
[PROOF STEP]
have "(pderiv ^^ Suc k) ([:- c, 1:] ^ n * p) =
          (pderiv ^^ k) ([:- c, 1:] ^ n * pderiv p + [:- c, 1:] ^ n' * smult (of_nat n) p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (pderiv ^^ Suc k) ([:- c, 1::'a:] ^ n * p) = (pderiv ^^ k) ([:- c, 1::'a:] ^ n * pderiv p + [:- c, 1::'a:] ^ n' * Polynomial.smult (of_nat n) p)
[PROOF STEP]
by (simp only: funpow_Suc_right o_def pderiv_mult n pderiv_power_Suc,
        simp only: n [symmetric]) (simp add: pderiv_pCons mult_ac)
[PROOF STATE]
proof (state)
this:
(pderiv ^^ Suc k) ([:- c, 1::'a:] ^ n * p) = (pderiv ^^ k) ([:- c, 1::'a:] ^ n * pderiv p + [:- c, 1::'a:] ^ n' * Polynomial.smult (of_nat n) p)

goal (2 subgoals):
 1. \<And>n p. 0 < n \<Longrightarrow> poly ((pderiv ^^ 0) ([:- c, 1::'a:] ^ n * p)) c = (0::'a)
 2. \<And>k n p. \<lbrakk>\<And>n p. k < n \<Longrightarrow> poly ((pderiv ^^ k) ([:- c, 1::'a:] ^ n * p)) c = (0::'a); Suc k < n\<rbrakk> \<Longrightarrow> poly ((pderiv ^^ Suc k) ([:- c, 1::'a:] ^ n * p)) c = (0::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(pderiv ^^ Suc k) ([:- c, 1::'a:] ^ n * p) = (pderiv ^^ k) ([:- c, 1::'a:] ^ n * pderiv p + [:- c, 1::'a:] ^ n' * Polynomial.smult (of_nat n) p)

goal (2 subgoals):
 1. \<And>n p. 0 < n \<Longrightarrow> poly ((pderiv ^^ 0) ([:- c, 1::'a:] ^ n * p)) c = (0::'a)
 2. \<And>k n p. \<lbrakk>\<And>n p. k < n \<Longrightarrow> poly ((pderiv ^^ k) ([:- c, 1::'a:] ^ n * p)) c = (0::'a); Suc k < n\<rbrakk> \<Longrightarrow> poly ((pderiv ^^ Suc k) ([:- c, 1::'a:] ^ n * p)) c = (0::'a)
[PROOF STEP]
from Suc.prems \<open>k < n'\<close>
[PROOF STATE]
proof (chain)
picking this:
Suc k < n
k < n'
[PROOF STEP]
have "poly \<dots> c = 0"
[PROOF STATE]
proof (prove)
using this:
Suc k < n
k < n'

goal (1 subgoal):
 1. poly ((pderiv ^^ k) ([:- c, 1::'a:] ^ n * pderiv p + [:- c, 1::'a:] ^ n' * Polynomial.smult (of_nat n) p)) c = (0::'a)
[PROOF STEP]
by (simp add: higher_pderiv_add Suc.IH del: mult_smult_right)
[PROOF STATE]
proof (state)
this:
poly ((pderiv ^^ k) ([:- c, 1::'a:] ^ n * pderiv p + [:- c, 1::'a:] ^ n' * Polynomial.smult (of_nat n) p)) c = (0::'a)

goal (2 subgoals):
 1. \<And>n p. 0 < n \<Longrightarrow> poly ((pderiv ^^ 0) ([:- c, 1::'a:] ^ n * p)) c = (0::'a)
 2. \<And>k n p. \<lbrakk>\<And>n p. k < n \<Longrightarrow> poly ((pderiv ^^ k) ([:- c, 1::'a:] ^ n * p)) c = (0::'a); Suc k < n\<rbrakk> \<Longrightarrow> poly ((pderiv ^^ Suc k) ([:- c, 1::'a:] ^ n * p)) c = (0::'a)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
poly ((pderiv ^^ Suc k) ([:- c, 1::'a:] ^ n * p)) c = (0::'a)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
poly ((pderiv ^^ Suc k) ([:- c, 1::'a:] ^ n * p)) c = (0::'a)

goal (1 subgoal):
 1. poly ((pderiv ^^ Suc k) ([:- c, 1::'a:] ^ n * p)) c = (0::'a)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
poly ((pderiv ^^ Suc k) ([:- c, 1::'a:] ^ n * p)) c = (0::'a)

goal (1 subgoal):
 1. \<And>n p. 0 < n \<Longrightarrow> poly ((pderiv ^^ 0) ([:- c, 1::'a:] ^ n * p)) c = (0::'a)
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma poly_higher_pderiv_aux1':
  fixes c :: "'a :: idom"
  assumes "k < n" "[:-c, 1:] ^ n dvd p"
  shows   "poly ((pderiv ^^ k) p) c = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly ((pderiv ^^ k) p) c = (0::'a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. poly ((pderiv ^^ k) p) c = (0::'a)
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
[:- c, 1::'a:] ^ n dvd p
[PROOF STEP]
obtain q where "p = [:-c, 1:] ^ n * q"
[PROOF STATE]
proof (prove)
using this:
[:- c, 1::'a:] ^ n dvd p

goal (1 subgoal):
 1. (\<And>q. p = [:- c, 1::'a:] ^ n * q \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (elim dvdE)
[PROOF STATE]
proof (state)
this:
p = [:- c, 1::'a:] ^ n * q

goal (1 subgoal):
 1. poly ((pderiv ^^ k) p) c = (0::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
p = [:- c, 1::'a:] ^ n * q

goal (1 subgoal):
 1. poly ((pderiv ^^ k) p) c = (0::'a)
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
k < n
[PROOF STEP]
have "poly ((pderiv ^^ k) \<dots>) c = 0"
[PROOF STATE]
proof (prove)
using this:
k < n

goal (1 subgoal):
 1. poly ((pderiv ^^ k) ([:- c, 1::'a:] ^ n * q)) c = (0::'a)
[PROOF STEP]
by (rule poly_higher_pderiv_aux1)
[PROOF STATE]
proof (state)
this:
poly ((pderiv ^^ k) ([:- c, 1::'a:] ^ n * q)) c = (0::'a)

goal (1 subgoal):
 1. poly ((pderiv ^^ k) p) c = (0::'a)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
poly ((pderiv ^^ k) p) c = (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
poly ((pderiv ^^ k) p) c = (0::'a)

goal (1 subgoal):
 1. poly ((pderiv ^^ k) p) c = (0::'a)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
poly ((pderiv ^^ k) p) c = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma poly_higher_pderiv_aux2:
  fixes c :: "'a :: {idom, semiring_char_0}"
  shows   "poly ((pderiv ^^ n) ([:-c, 1:] ^ n * p)) c = fact n * poly p c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly ((pderiv ^^ n) ([:- c, 1::'a:] ^ n * p)) c = fact n * poly p c
[PROOF STEP]
proof (induction n arbitrary: p)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>p. poly ((pderiv ^^ 0) ([:- c, 1::'a:] ^ 0 * p)) c = fact 0 * poly p c
 2. \<And>n p. (\<And>p. poly ((pderiv ^^ n) ([:- c, 1::'a:] ^ n * p)) c = fact n * poly p c) \<Longrightarrow> poly ((pderiv ^^ Suc n) ([:- c, 1::'a:] ^ Suc n * p)) c = fact (Suc n) * poly p c
[PROOF STEP]
case (Suc n p)
[PROOF STATE]
proof (state)
this:
poly ((pderiv ^^ n) ([:- c, 1::'a:] ^ n * ?p)) c = fact n * poly ?p c

goal (2 subgoals):
 1. \<And>p. poly ((pderiv ^^ 0) ([:- c, 1::'a:] ^ 0 * p)) c = fact 0 * poly p c
 2. \<And>n p. (\<And>p. poly ((pderiv ^^ n) ([:- c, 1::'a:] ^ n * p)) c = fact n * poly p c) \<Longrightarrow> poly ((pderiv ^^ Suc n) ([:- c, 1::'a:] ^ Suc n * p)) c = fact (Suc n) * poly p c
[PROOF STEP]
have "(pderiv ^^ Suc n) ([:- c, 1:] ^ Suc n * p) =
          (pderiv ^^ n) ([:- c, 1:] ^ Suc n * pderiv p) +
            (pderiv ^^ n) ([:- c, 1:] ^ n * smult (1 + of_nat n) p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (pderiv ^^ Suc n) ([:- c, 1::'a:] ^ Suc n * p) = (pderiv ^^ n) ([:- c, 1::'a:] ^ Suc n * pderiv p) + (pderiv ^^ n) ([:- c, 1::'a:] ^ n * Polynomial.smult ((1::'a) + of_nat n) p)
[PROOF STEP]
by (simp del: funpow.simps power_Suc add: funpow_Suc_right pderiv_mult
          pderiv_power_Suc higher_pderiv_add pderiv_pCons mult_ac)
[PROOF STATE]
proof (state)
this:
(pderiv ^^ Suc n) ([:- c, 1::'a:] ^ Suc n * p) = (pderiv ^^ n) ([:- c, 1::'a:] ^ Suc n * pderiv p) + (pderiv ^^ n) ([:- c, 1::'a:] ^ n * Polynomial.smult ((1::'a) + of_nat n) p)

goal (2 subgoals):
 1. \<And>p. poly ((pderiv ^^ 0) ([:- c, 1::'a:] ^ 0 * p)) c = fact 0 * poly p c
 2. \<And>n p. (\<And>p. poly ((pderiv ^^ n) ([:- c, 1::'a:] ^ n * p)) c = fact n * poly p c) \<Longrightarrow> poly ((pderiv ^^ Suc n) ([:- c, 1::'a:] ^ Suc n * p)) c = fact (Suc n) * poly p c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(pderiv ^^ Suc n) ([:- c, 1::'a:] ^ Suc n * p) = (pderiv ^^ n) ([:- c, 1::'a:] ^ Suc n * pderiv p) + (pderiv ^^ n) ([:- c, 1::'a:] ^ n * Polynomial.smult ((1::'a) + of_nat n) p)

goal (2 subgoals):
 1. \<And>p. poly ((pderiv ^^ 0) ([:- c, 1::'a:] ^ 0 * p)) c = fact 0 * poly p c
 2. \<And>n p. (\<And>p. poly ((pderiv ^^ n) ([:- c, 1::'a:] ^ n * p)) c = fact n * poly p c) \<Longrightarrow> poly ((pderiv ^^ Suc n) ([:- c, 1::'a:] ^ Suc n * p)) c = fact (Suc n) * poly p c
[PROOF STEP]
have "[:- c, 1:] ^ Suc n * pderiv p = [:- c, 1:] ^ n * ([:-c, 1:] * pderiv p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [:- c, 1::'a:] ^ Suc n * pderiv p = [:- c, 1::'a:] ^ n * ([:- c, 1::'a:] * pderiv p)
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
[:- c, 1::'a:] ^ Suc n * pderiv p = [:- c, 1::'a:] ^ n * ([:- c, 1::'a:] * pderiv p)

goal (2 subgoals):
 1. \<And>p. poly ((pderiv ^^ 0) ([:- c, 1::'a:] ^ 0 * p)) c = fact 0 * poly p c
 2. \<And>n p. (\<And>p. poly ((pderiv ^^ n) ([:- c, 1::'a:] ^ n * p)) c = fact n * poly p c) \<Longrightarrow> poly ((pderiv ^^ Suc n) ([:- c, 1::'a:] ^ Suc n * p)) c = fact (Suc n) * poly p c
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(pderiv ^^ Suc n) ([:- c, 1::'a:] ^ Suc n * p) = (pderiv ^^ n) ([:- c, 1::'a:] ^ n * ([:- c, 1::'a:] * pderiv p)) + (pderiv ^^ n) ([:- c, 1::'a:] ^ n * Polynomial.smult ((1::'a) + of_nat n) p)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(pderiv ^^ Suc n) ([:- c, 1::'a:] ^ Suc n * p) = (pderiv ^^ n) ([:- c, 1::'a:] ^ n * ([:- c, 1::'a:] * pderiv p)) + (pderiv ^^ n) ([:- c, 1::'a:] ^ n * Polynomial.smult ((1::'a) + of_nat n) p)

goal (1 subgoal):
 1. poly ((pderiv ^^ Suc n) ([:- c, 1::'a:] ^ Suc n * p)) c = fact (Suc n) * poly p c
[PROOF STEP]
by (simp add: Suc.IH del: mult_smult_right power_Suc)
[PROOF STATE]
proof (state)
this:
poly ((pderiv ^^ Suc n) ([:- c, 1::'a:] ^ Suc n * p)) c = fact (Suc n) * poly p c

goal (1 subgoal):
 1. \<And>p. poly ((pderiv ^^ 0) ([:- c, 1::'a:] ^ 0 * p)) c = fact 0 * poly p c
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma poly_higher_pderiv_aux3:
  fixes c :: "'a :: {idom,semiring_char_0}"
  assumes "k \<ge> n"
  shows   "\<exists>q. poly ((pderiv ^^ k) ([:-c, 1:] ^ n * p)) c = fact n * poly q c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>q. poly ((pderiv ^^ k) ([:- c, 1::'a:] ^ n * p)) c = fact n * poly q c
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
n \<le> k

goal (1 subgoal):
 1. \<exists>q. poly ((pderiv ^^ k) ([:- c, 1::'a:] ^ n * p)) c = fact n * poly q c
[PROOF STEP]
proof (induction k arbitrary: n p)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n p. n \<le> 0 \<Longrightarrow> \<exists>q. poly ((pderiv ^^ 0) ([:- c, 1::'a:] ^ n * p)) c = fact n * poly q c
 2. \<And>k n p. \<lbrakk>\<And>n p. n \<le> k \<Longrightarrow> \<exists>q. poly ((pderiv ^^ k) ([:- c, 1::'a:] ^ n * p)) c = fact n * poly q c; n \<le> Suc k\<rbrakk> \<Longrightarrow> \<exists>q. poly ((pderiv ^^ Suc k) ([:- c, 1::'a:] ^ n * p)) c = fact n * poly q c
[PROOF STEP]
case (Suc k n p)
[PROOF STATE]
proof (state)
this:
?n \<le> k \<Longrightarrow> \<exists>q. poly ((pderiv ^^ k) ([:- c, 1::'a:] ^ ?n * ?p)) c = fact ?n * poly q c
n \<le> Suc k

goal (2 subgoals):
 1. \<And>n p. n \<le> 0 \<Longrightarrow> \<exists>q. poly ((pderiv ^^ 0) ([:- c, 1::'a:] ^ n * p)) c = fact n * poly q c
 2. \<And>k n p. \<lbrakk>\<And>n p. n \<le> k \<Longrightarrow> \<exists>q. poly ((pderiv ^^ k) ([:- c, 1::'a:] ^ n * p)) c = fact n * poly q c; n \<le> Suc k\<rbrakk> \<Longrightarrow> \<exists>q. poly ((pderiv ^^ Suc k) ([:- c, 1::'a:] ^ n * p)) c = fact n * poly q c
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>q. poly ((pderiv ^^ Suc k) ([:- c, 1::'a:] ^ n * p)) c = fact n * poly q c
[PROOF STEP]
proof (cases n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>q. poly ((pderiv ^^ Suc k) ([:- c, 1::'a:] ^ n * p)) c = fact n * poly q c
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>q. poly ((pderiv ^^ Suc k) ([:- c, 1::'a:] ^ n * p)) c = fact n * poly q c
[PROOF STEP]
fix n'
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>q. poly ((pderiv ^^ Suc k) ([:- c, 1::'a:] ^ n * p)) c = fact n * poly q c
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>q. poly ((pderiv ^^ Suc k) ([:- c, 1::'a:] ^ n * p)) c = fact n * poly q c
[PROOF STEP]
assume n: "n = Suc n'"
[PROOF STATE]
proof (state)
this:
n = Suc n'

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>q. poly ((pderiv ^^ Suc k) ([:- c, 1::'a:] ^ n * p)) c = fact n * poly q c
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>q. poly ((pderiv ^^ Suc k) ([:- c, 1::'a:] ^ n * p)) c = fact n * poly q c
[PROOF STEP]
have "poly ((pderiv ^^ Suc k) ([:-c, 1:] ^ n * p)) c =
            poly ((pderiv ^^ k) ([:- c, 1:] ^ n * pderiv p)) c +
              of_nat n * poly ((pderiv ^^ k) ([:-c, 1:] ^ n' * p)) c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly ((pderiv ^^ Suc k) ([:- c, 1::'a:] ^ n * p)) c = poly ((pderiv ^^ k) ([:- c, 1::'a:] ^ n * pderiv p)) c + of_nat n * poly ((pderiv ^^ k) ([:- c, 1::'a:] ^ n' * p)) c
[PROOF STEP]
by (simp del: funpow.simps power_Suc add: funpow_Suc_right pderiv_power_Suc
            pderiv_mult n pderiv_pCons higher_pderiv_add mult_ac higher_pderiv_smult)
[PROOF STATE]
proof (state)
this:
poly ((pderiv ^^ Suc k) ([:- c, 1::'a:] ^ n * p)) c = poly ((pderiv ^^ k) ([:- c, 1::'a:] ^ n * pderiv p)) c + of_nat n * poly ((pderiv ^^ k) ([:- c, 1::'a:] ^ n' * p)) c

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>q. poly ((pderiv ^^ Suc k) ([:- c, 1::'a:] ^ n * p)) c = fact n * poly q c
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>q. poly ((pderiv ^^ Suc k) ([:- c, 1::'a:] ^ n * p)) c = fact n * poly q c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
poly ((pderiv ^^ Suc k) ([:- c, 1::'a:] ^ n * p)) c = poly ((pderiv ^^ k) ([:- c, 1::'a:] ^ n * pderiv p)) c + of_nat n * poly ((pderiv ^^ k) ([:- c, 1::'a:] ^ n' * p)) c

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>q. poly ((pderiv ^^ Suc k) ([:- c, 1::'a:] ^ n * p)) c = fact n * poly q c
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>q. poly ((pderiv ^^ Suc k) ([:- c, 1::'a:] ^ n * p)) c = fact n * poly q c
[PROOF STEP]
have "\<exists>q1. poly ((pderiv ^^ k) ([:-c, 1:] ^ n * pderiv p)) c = fact n * poly q1 c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>q1. poly ((pderiv ^^ k) ([:- c, 1::'a:] ^ n * pderiv p)) c = fact n * poly q1 c
[PROOF STEP]
using Suc.prems Suc.IH[of n "pderiv p"]
[PROOF STATE]
proof (prove)
using this:
n \<le> Suc k
n \<le> k \<Longrightarrow> \<exists>q. poly ((pderiv ^^ k) ([:- c, 1::'a:] ^ n * pderiv p)) c = fact n * poly q c

goal (1 subgoal):
 1. \<exists>q1. poly ((pderiv ^^ k) ([:- c, 1::'a:] ^ n * pderiv p)) c = fact n * poly q1 c
[PROOF STEP]
by (cases "n' = k") (auto simp: n poly_higher_pderiv_aux1 simp del: power_Suc of_nat_Suc
                                intro: exI[of _ "0::'a poly"])
[PROOF STATE]
proof (state)
this:
\<exists>q1. poly ((pderiv ^^ k) ([:- c, 1::'a:] ^ n * pderiv p)) c = fact n * poly q1 c

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>q. poly ((pderiv ^^ Suc k) ([:- c, 1::'a:] ^ n * p)) c = fact n * poly q c
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>q. poly ((pderiv ^^ Suc k) ([:- c, 1::'a:] ^ n * p)) c = fact n * poly q c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>q1. poly ((pderiv ^^ k) ([:- c, 1::'a:] ^ n * pderiv p)) c = fact n * poly q1 c
[PROOF STEP]
obtain q1
      where "poly ((pderiv ^^ k) ([:-c, 1:] ^ n * pderiv p)) c = fact n * poly q1 c"
[PROOF STATE]
proof (prove)
using this:
\<exists>q1. poly ((pderiv ^^ k) ([:- c, 1::'a:] ^ n * pderiv p)) c = fact n * poly q1 c

goal (1 subgoal):
 1. (\<And>q1. poly ((pderiv ^^ k) ([:- c, 1::'a:] ^ n * pderiv p)) c = fact n * poly q1 c \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
poly ((pderiv ^^ k) ([:- c, 1::'a:] ^ n * pderiv p)) c = fact n * poly q1 c

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>q. poly ((pderiv ^^ Suc k) ([:- c, 1::'a:] ^ n * p)) c = fact n * poly q c
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>q. poly ((pderiv ^^ Suc k) ([:- c, 1::'a:] ^ n * p)) c = fact n * poly q c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
poly ((pderiv ^^ k) ([:- c, 1::'a:] ^ n * pderiv p)) c = fact n * poly q1 c

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>q. poly ((pderiv ^^ Suc k) ([:- c, 1::'a:] ^ n * p)) c = fact n * poly q c
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>q. poly ((pderiv ^^ Suc k) ([:- c, 1::'a:] ^ n * p)) c = fact n * poly q c
[PROOF STEP]
from Suc.IH[of n' p] Suc.prems
[PROOF STATE]
proof (chain)
picking this:
n' \<le> k \<Longrightarrow> \<exists>q. poly ((pderiv ^^ k) ([:- c, 1::'a:] ^ n' * p)) c = fact n' * poly q c
n \<le> Suc k
[PROOF STEP]
obtain q2
      where "poly ((pderiv ^^ k) ([:-c, 1:] ^ n' * p)) c = fact n' * poly q2 c"
[PROOF STATE]
proof (prove)
using this:
n' \<le> k \<Longrightarrow> \<exists>q. poly ((pderiv ^^ k) ([:- c, 1::'a:] ^ n' * p)) c = fact n' * poly q c
n \<le> Suc k

goal (1 subgoal):
 1. (\<And>q2. poly ((pderiv ^^ k) ([:- c, 1::'a:] ^ n' * p)) c = fact n' * poly q2 c \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: n)
[PROOF STATE]
proof (state)
this:
poly ((pderiv ^^ k) ([:- c, 1::'a:] ^ n' * p)) c = fact n' * poly q2 c

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>q. poly ((pderiv ^^ Suc k) ([:- c, 1::'a:] ^ n * p)) c = fact n * poly q c
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>q. poly ((pderiv ^^ Suc k) ([:- c, 1::'a:] ^ n * p)) c = fact n * poly q c
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
poly ((pderiv ^^ Suc k) ([:- c, 1::'a:] ^ n * p)) c = fact n * poly q1 c + of_nat n * (fact n' * poly q2 c)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
poly ((pderiv ^^ Suc k) ([:- c, 1::'a:] ^ n * p)) c = fact n * poly q1 c + of_nat n * (fact n' * poly q2 c)

goal (1 subgoal):
 1. \<exists>q. poly ((pderiv ^^ Suc k) ([:- c, 1::'a:] ^ n * p)) c = fact n * poly q c
[PROOF STEP]
by (auto intro!: exI[of _ "q1 + q2"] simp: n algebra_simps)
[PROOF STATE]
proof (state)
this:
\<exists>q. poly ((pderiv ^^ Suc k) ([:- c, 1::'a:] ^ n * p)) c = fact n * poly q c

goal (1 subgoal):
 1. n = 0 \<Longrightarrow> \<exists>q. poly ((pderiv ^^ Suc k) ([:- c, 1::'a:] ^ n * p)) c = fact n * poly q c
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
\<exists>q. poly ((pderiv ^^ Suc k) ([:- c, 1::'a:] ^ n * p)) c = fact n * poly q c

goal (1 subgoal):
 1. \<And>n p. n \<le> 0 \<Longrightarrow> \<exists>q. poly ((pderiv ^^ 0) ([:- c, 1::'a:] ^ n * p)) c = fact n * poly q c
[PROOF STEP]
qed auto


[STATEMENT]
lemma poly_higher_pderiv_aux3':
  fixes c :: "'a :: {idom, semiring_char_0}"
  assumes "k \<ge> n" "[:-c, 1:] ^ n dvd p"
  shows   "fact n dvd poly ((pderiv ^^ k) p) c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fact n dvd poly ((pderiv ^^ k) p) c
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fact n dvd poly ((pderiv ^^ k) p) c
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
[:- c, 1::'a:] ^ n dvd p
[PROOF STEP]
obtain q where "p = [:-c, 1:] ^ n * q"
[PROOF STATE]
proof (prove)
using this:
[:- c, 1::'a:] ^ n dvd p

goal (1 subgoal):
 1. (\<And>q. p = [:- c, 1::'a:] ^ n * q \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (elim dvdE)
[PROOF STATE]
proof (state)
this:
p = [:- c, 1::'a:] ^ n * q

goal (1 subgoal):
 1. fact n dvd poly ((pderiv ^^ k) p) c
[PROOF STEP]
with poly_higher_pderiv_aux3[OF assms(1), of c q]
[PROOF STATE]
proof (chain)
picking this:
\<exists>qa. poly ((pderiv ^^ k) ([:- c, 1::'a:] ^ n * q)) c = fact n * poly qa c
p = [:- c, 1::'a:] ^ n * q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>qa. poly ((pderiv ^^ k) ([:- c, 1::'a:] ^ n * q)) c = fact n * poly qa c
p = [:- c, 1::'a:] ^ n * q

goal (1 subgoal):
 1. fact n dvd poly ((pderiv ^^ k) p) c
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fact n dvd poly ((pderiv ^^ k) p) c

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma e_transcendental_aux_bound:
  obtains C where "C \<ge> 0"
    "\<And>x. x \<in> closed_segment 0 (of_nat n) \<Longrightarrow>
        norm (\<Prod>k\<in>{1..n}. (x - of_nat k :: complex)) \<le> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>C. \<lbrakk>0 \<le> C; \<And>x. x \<in> closed_segment 0 (of_nat n) \<Longrightarrow> cmod (\<Prod>k = 1..n. x - of_nat k) \<le> C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>C. \<lbrakk>0 \<le> C; \<And>x. x \<in> closed_segment 0 (of_nat n) \<Longrightarrow> cmod (\<Prod>k = 1..n. x - of_nat k) \<le> C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
let ?f = "\<lambda>x. (\<Prod>k\<in>{1..n}. (x - of_nat k))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>C. \<lbrakk>0 \<le> C; \<And>x. x \<in> closed_segment 0 (of_nat n) \<Longrightarrow> cmod (\<Prod>k = 1..n. x - of_nat k) \<le> C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define C where "C = max 0 (Sup (cmod ` ?f ` closed_segment 0 (of_nat n)))"
[PROOF STATE]
proof (state)
this:
C = max 0 (Sup (cmod ` (\<lambda>x. \<Prod>k = 1..n. x - of_nat k) ` closed_segment 0 (of_nat n)))

goal (1 subgoal):
 1. (\<And>C. \<lbrakk>0 \<le> C; \<And>x. x \<in> closed_segment 0 (of_nat n) \<Longrightarrow> cmod (\<Prod>k = 1..n. x - of_nat k) \<le> C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "C \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> C
[PROOF STEP]
by (simp add: C_def)
[PROOF STATE]
proof (state)
this:
0 \<le> C

goal (1 subgoal):
 1. (\<And>C. \<lbrakk>0 \<le> C; \<And>x. x \<in> closed_segment 0 (of_nat n) \<Longrightarrow> cmod (\<Prod>k = 1..n. x - of_nat k) \<le> C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 \<le> C

goal (1 subgoal):
 1. (\<And>C. \<lbrakk>0 \<le> C; \<And>x. x \<in> closed_segment 0 (of_nat n) \<Longrightarrow> cmod (\<Prod>k = 1..n. x - of_nat k) \<le> C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
0 \<le> C

goal (1 subgoal):
 1. (\<And>C. \<lbrakk>0 \<le> C; \<And>x. x \<in> closed_segment 0 (of_nat n) \<Longrightarrow> cmod (\<Prod>k = 1..n. x - of_nat k) \<le> C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
fix x :: complex
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>C. \<lbrakk>0 \<le> C; \<And>x. x \<in> closed_segment 0 (of_nat n) \<Longrightarrow> cmod (\<Prod>k = 1..n. x - of_nat k) \<le> C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
assume "x \<in> closed_segment 0 (of_nat n)"
[PROOF STATE]
proof (state)
this:
x \<in> closed_segment 0 (of_nat n)

goal (1 subgoal):
 1. (\<And>C. \<lbrakk>0 \<le> C; \<And>x. x \<in> closed_segment 0 (of_nat n) \<Longrightarrow> cmod (\<Prod>k = 1..n. x - of_nat k) \<le> C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence "cmod (?f x) \<le> Sup ((cmod \<circ> ?f) ` closed_segment 0 (of_nat n))"
[PROOF STATE]
proof (prove)
using this:
x \<in> closed_segment 0 (of_nat n)

goal (1 subgoal):
 1. cmod (\<Prod>k = 1..n. x - of_nat k) \<le> Sup ((cmod \<circ> (\<lambda>x. \<Prod>k = 1..n. x - of_nat k)) ` closed_segment 0 (of_nat n))
[PROOF STEP]
by (intro cSup_upper bounded_imp_bdd_above compact_imp_bounded compact_continuous_image)
         (auto intro!: continuous_intros)
[PROOF STATE]
proof (state)
this:
cmod (\<Prod>k = 1..n. x - of_nat k) \<le> Sup ((cmod \<circ> (\<lambda>x. \<Prod>k = 1..n. x - of_nat k)) ` closed_segment 0 (of_nat n))

goal (1 subgoal):
 1. (\<And>C. \<lbrakk>0 \<le> C; \<And>x. x \<in> closed_segment 0 (of_nat n) \<Longrightarrow> cmod (\<Prod>k = 1..n. x - of_nat k) \<le> C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cmod (\<Prod>k = 1..n. x - of_nat k) \<le> Sup ((cmod \<circ> (\<lambda>x. \<Prod>k = 1..n. x - of_nat k)) ` closed_segment 0 (of_nat n))

goal (1 subgoal):
 1. (\<And>C. \<lbrakk>0 \<le> C; \<And>x. x \<in> closed_segment 0 (of_nat n) \<Longrightarrow> cmod (\<Prod>k = 1..n. x - of_nat k) \<le> C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "\<dots> \<le> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sup ((cmod \<circ> (\<lambda>x. \<Prod>k = 1..n. x - of_nat k)) ` closed_segment 0 (of_nat n)) \<le> C
[PROOF STEP]
by (simp add: C_def image_comp)
[PROOF STATE]
proof (state)
this:
Sup ((cmod \<circ> (\<lambda>x. \<Prod>k = 1..n. x - of_nat k)) ` closed_segment 0 (of_nat n)) \<le> C

goal (1 subgoal):
 1. (\<And>C. \<lbrakk>0 \<le> C; \<And>x. x \<in> closed_segment 0 (of_nat n) \<Longrightarrow> cmod (\<Prod>k = 1..n. x - of_nat k) \<le> C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
cmod (\<Prod>k = 1..n. x - of_nat k) \<le> C
[PROOF STEP]
have "cmod (?f x) \<le> C"
[PROOF STATE]
proof (prove)
using this:
cmod (\<Prod>k = 1..n. x - of_nat k) \<le> C

goal (1 subgoal):
 1. cmod (\<Prod>k = 1..n. x - of_nat k) \<le> C
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
cmod (\<Prod>k = 1..n. x - of_nat k) \<le> C

goal (1 subgoal):
 1. (\<And>C. \<lbrakk>0 \<le> C; \<And>x. x \<in> closed_segment 0 (of_nat n) \<Longrightarrow> cmod (\<Prod>k = 1..n. x - of_nat k) \<le> C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?x3 \<in> closed_segment 0 (of_nat n) \<Longrightarrow> cmod (\<Prod>k = 1..n. ?x3 - of_nat k) \<le> C

goal (1 subgoal):
 1. (\<And>C. \<lbrakk>0 \<le> C; \<And>x. x \<in> closed_segment 0 (of_nat n) \<Longrightarrow> cmod (\<Prod>k = 1..n. x - of_nat k) \<le> C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
0 \<le> C
?x3 \<in> closed_segment 0 (of_nat n) \<Longrightarrow> cmod (\<Prod>k = 1..n. ?x3 - of_nat k) \<le> C
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 \<le> C
?x3 \<in> closed_segment 0 (of_nat n) \<Longrightarrow> cmod (\<Prod>k = 1..n. ?x3 - of_nat k) \<le> C

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (rule that)
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem e_transcendental_complex: "\<not> algebraic (exp 1 :: complex)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> algebraic (exp 1)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. algebraic (exp 1) \<Longrightarrow> False
[PROOF STEP]
assume "algebraic (exp 1 :: complex)"
[PROOF STATE]
proof (state)
this:
algebraic (exp 1)

goal (1 subgoal):
 1. algebraic (exp 1) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
algebraic (exp 1)
[PROOF STEP]
obtain q :: "int poly"
    where q: "q \<noteq> 0" "coeff q 0 \<noteq> 0" "poly (of_int_poly q) (exp 1 :: complex) = 0"
[PROOF STATE]
proof (prove)
using this:
algebraic (exp 1)

goal (1 subgoal):
 1. (\<And>q. \<lbrakk>q \<noteq> 0; poly.coeff q 0 \<noteq> 0; poly (of_int_poly q) (exp 1) = 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (elim algebraicE'_nonzero) simp_all
[PROOF STATE]
proof (state)
this:
q \<noteq> 0
poly.coeff q 0 \<noteq> 0
poly (of_int_poly q) (exp 1) = 0

goal (1 subgoal):
 1. algebraic (exp 1) \<Longrightarrow> False
[PROOF STEP]
define n :: nat where "n = degree q"
[PROOF STATE]
proof (state)
this:
n = degree q

goal (1 subgoal):
 1. algebraic (exp 1) \<Longrightarrow> False
[PROOF STEP]
from q
[PROOF STATE]
proof (chain)
picking this:
q \<noteq> 0
poly.coeff q 0 \<noteq> 0
poly (of_int_poly q) (exp 1) = 0
[PROOF STEP]
have [simp]: "n \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
q \<noteq> 0
poly.coeff q 0 \<noteq> 0
poly (of_int_poly q) (exp 1) = 0

goal (1 subgoal):
 1. n \<noteq> 0
[PROOF STEP]
by (intro notI) (auto simp: n_def elim!: degree_eq_zeroE)
[PROOF STATE]
proof (state)
this:
n \<noteq> 0

goal (1 subgoal):
 1. algebraic (exp 1) \<Longrightarrow> False
[PROOF STEP]
define qmax where "qmax = Max (insert 0 (abs ` set (coeffs q)))"
[PROOF STATE]
proof (state)
this:
qmax = Max (insert 0 (abs ` set (coeffs q)))

goal (1 subgoal):
 1. algebraic (exp 1) \<Longrightarrow> False
[PROOF STEP]
have qmax_nonneg [simp]: "qmax \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> qmax
[PROOF STEP]
by (simp add: qmax_def)
[PROOF STATE]
proof (state)
this:
0 \<le> qmax

goal (1 subgoal):
 1. algebraic (exp 1) \<Longrightarrow> False
[PROOF STEP]
have qmax: "\<bar>coeff q k\<bar> \<le> qmax" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>poly.coeff q k\<bar> \<le> qmax
[PROOF STEP]
by (cases "k \<le> degree q")
       (auto simp: qmax_def coeff_eq_0 coeffs_def simp del: upt_Suc intro: Max.coboundedI)
[PROOF STATE]
proof (state)
this:
\<bar>poly.coeff q ?k\<bar> \<le> qmax

goal (1 subgoal):
 1. algebraic (exp 1) \<Longrightarrow> False
[PROOF STEP]
obtain C where C: "C \<ge> 0"
    "\<And>x. x \<in> closed_segment 0 (of_nat n) \<Longrightarrow> norm (\<Prod>k\<in>{1..n}. (x - of_nat k :: complex)) \<le> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>C. \<lbrakk>0 \<le> C; \<And>x. x \<in> closed_segment 0 (of_nat n) \<Longrightarrow> cmod (\<Prod>k = 1..n. x - of_nat k) \<le> C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (erule e_transcendental_aux_bound)
[PROOF STATE]
proof (state)
this:
0 \<le> C
?x \<in> closed_segment 0 (of_nat n) \<Longrightarrow> cmod (\<Prod>k = 1..n. ?x - of_nat k) \<le> C

goal (1 subgoal):
 1. algebraic (exp 1) \<Longrightarrow> False
[PROOF STEP]
define E where "E = (1 + real n) * real_of_int qmax * real n * exp (real n) / real n"
[PROOF STATE]
proof (state)
this:
E = (1 + real n) * real_of_int qmax * real n * exp (real n) / real n

goal (1 subgoal):
 1. algebraic (exp 1) \<Longrightarrow> False
[PROOF STEP]
define F where "F = real n * C"
[PROOF STATE]
proof (state)
this:
F = real n * C

goal (1 subgoal):
 1. algebraic (exp 1) \<Longrightarrow> False
[PROOF STEP]
have ineq: "fact (p - 1) \<le> E * F ^ p" if p: "prime p" "p > n" "p > abs (coeff q 0)" for p
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fact (p - 1) \<le> E * F ^ p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fact (p - 1) \<le> E * F ^ p
[PROOF STEP]
from p(1)
[PROOF STATE]
proof (chain)
picking this:
prime p
[PROOF STEP]
have p_pos: "p > 0"
[PROOF STATE]
proof (prove)
using this:
prime p

goal (1 subgoal):
 1. 0 < p
[PROOF STEP]
by (simp add: prime_gt_0_nat)
[PROOF STATE]
proof (state)
this:
0 < p

goal (1 subgoal):
 1. fact (p - 1) \<le> E * F ^ p
[PROOF STEP]
define f :: "int poly"
      where "f = monom 1 (p - 1) * (\<Prod>k\<in>{1..n}. [:-of_nat k, 1:] ^ p)"
[PROOF STATE]
proof (state)
this:
f = Polynomial.monom 1 (p - 1) * (\<Prod>k = 1..n. [:- int k, 1:] ^ p)

goal (1 subgoal):
 1. fact (p - 1) \<le> E * F ^ p
[PROOF STEP]
have poly_f: "poly (of_int_poly f) x = x ^ (p - 1) * (\<Prod>k\<in>{1..n}. (x - of_nat k)) ^ p"
      for x :: complex
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly (of_int_poly f) x = x ^ (p - 1) * (\<Prod>k = 1..n. x - of_nat k) ^ p
[PROOF STEP]
by (simp add: f_def poly_prod poly_monom prod_power_distrib)
[PROOF STATE]
proof (state)
this:
poly (of_int_poly f) ?x = ?x ^ (p - 1) * (\<Prod>k = 1..n. ?x - of_nat k) ^ p

goal (1 subgoal):
 1. fact (p - 1) \<le> E * F ^ p
[PROOF STEP]
define m :: nat where "m = degree f"
[PROOF STATE]
proof (state)
this:
m = degree f

goal (1 subgoal):
 1. fact (p - 1) \<le> E * F ^ p
[PROOF STEP]
from p_pos
[PROOF STATE]
proof (chain)
picking this:
0 < p
[PROOF STEP]
have m: "m = (n + 1) * p - 1"
[PROOF STATE]
proof (prove)
using this:
0 < p

goal (1 subgoal):
 1. m = (n + 1) * p - 1
[PROOF STEP]
by (simp add: m_def f_def degree_mult_eq degree_monom_eq degree_prod_sum_eq degree_linear_power)
[PROOF STATE]
proof (state)
this:
m = (n + 1) * p - 1

goal (1 subgoal):
 1. fact (p - 1) \<le> E * F ^ p
[PROOF STEP]
define M :: int where "M = (- 1) ^ (n * p) * fact n ^ p"
[PROOF STATE]
proof (state)
this:
M = (- 1) ^ (n * p) * fact n ^ p

goal (1 subgoal):
 1. fact (p - 1) \<le> E * F ^ p
[PROOF STEP]
with p
[PROOF STATE]
proof (chain)
picking this:
prime p
n < p
\<bar>poly.coeff q 0\<bar> < int p
M = (- 1) ^ (n * p) * fact n ^ p
[PROOF STEP]
have p_not_dvd_M: "\<not>int p dvd M"
[PROOF STATE]
proof (prove)
using this:
prime p
n < p
\<bar>poly.coeff q 0\<bar> < int p
M = (- 1) ^ (n * p) * fact n ^ p

goal (1 subgoal):
 1. \<not> int p dvd M
[PROOF STEP]
by (auto simp: M_def prime_elem_int_not_dvd_neg1_power prime_dvd_power_iff
            prime_gt_0_nat prime_dvd_fact_iff_int prime_dvd_mult_iff)
[PROOF STATE]
proof (state)
this:
\<not> int p dvd M

goal (1 subgoal):
 1. fact (p - 1) \<le> E * F ^ p
[PROOF STEP]
interpret lindemann_weierstrass_aux "of_int_poly f"
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fact (p - 1) \<le> E * F ^ p
[PROOF STEP]
define J :: complex where "J = (\<Sum>k\<le>n. of_int (coeff q k) * I (of_nat k))"
[PROOF STATE]
proof (state)
this:
J = (\<Sum>k\<le>n. of_int (poly.coeff q k) * I (of_nat k))

goal (1 subgoal):
 1. fact (p - 1) \<le> E * F ^ p
[PROOF STEP]
define idxs where "idxs = ({..n}\<times>{..m}) - {(0, p - 1)}"
[PROOF STATE]
proof (state)
this:
idxs = {..n} \<times> {..m} - {(0, p - 1)}

goal (1 subgoal):
 1. fact (p - 1) \<le> E * F ^ p
[PROOF STEP]
hence "J = (\<Sum>k\<le>n. of_int (coeff q k) * exp 1 ^ k) * (\<Sum>n\<le>m. of_int (poly ((pderiv ^^ n) f) 0)) -
                 of_int (\<Sum>k\<le>n. \<Sum>n\<le>m. coeff q k * poly ((pderiv ^^ n) f) (int k))"
[PROOF STATE]
proof (prove)
using this:
idxs = {..n} \<times> {..m} - {(0, p - 1)}

goal (1 subgoal):
 1. J = (\<Sum>k\<le>n. of_int (poly.coeff q k) * exp 1 ^ k) * (\<Sum>n\<le>m. of_int (poly ((pderiv ^^ n) f) 0)) - of_int (\<Sum>k\<le>n. \<Sum>n\<le>m. poly.coeff q k * poly ((pderiv ^^ n) f) (int k))
[PROOF STEP]
by (simp add: J_def I_def algebra_simps sum_subtractf sum_distrib_left m_def
                    exp_of_nat_mult [symmetric])
[PROOF STATE]
proof (state)
this:
J = (\<Sum>k\<le>n. of_int (poly.coeff q k) * exp 1 ^ k) * (\<Sum>n\<le>m. of_int (poly ((pderiv ^^ n) f) 0)) - of_int (\<Sum>k\<le>n. \<Sum>n\<le>m. poly.coeff q k * poly ((pderiv ^^ n) f) (int k))

goal (1 subgoal):
 1. fact (p - 1) \<le> E * F ^ p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
J = (\<Sum>k\<le>n. of_int (poly.coeff q k) * exp 1 ^ k) * (\<Sum>n\<le>m. of_int (poly ((pderiv ^^ n) f) 0)) - of_int (\<Sum>k\<le>n. \<Sum>n\<le>m. poly.coeff q k * poly ((pderiv ^^ n) f) (int k))

goal (1 subgoal):
 1. fact (p - 1) \<le> E * F ^ p
[PROOF STEP]
have "(\<Sum>k\<le>n. of_int (coeff q k) * exp 1 ^ k) = poly (of_int_poly q) (exp 1 :: complex)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>k\<le>n. of_int (poly.coeff q k) * exp 1 ^ k) = poly (of_int_poly q) (exp 1)
[PROOF STEP]
by (simp add: poly_altdef n_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>k\<le>n. of_int (poly.coeff q k) * exp 1 ^ k) = poly (of_int_poly q) (exp 1)

goal (1 subgoal):
 1. fact (p - 1) \<le> E * F ^ p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>k\<le>n. of_int (poly.coeff q k) * exp 1 ^ k) = poly (of_int_poly q) (exp 1)

goal (1 subgoal):
 1. fact (p - 1) \<le> E * F ^ p
[PROOF STEP]
have "\<dots> = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly (of_int_poly q) (exp 1) = 0
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
poly (of_int_poly q) (exp 1) = 0

goal (1 subgoal):
 1. fact (p - 1) \<le> E * F ^ p
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
J = 0 * (\<Sum>n\<le>m. of_int (poly ((pderiv ^^ n) f) 0)) - of_int (\<Sum>k\<le>n. \<Sum>n\<le>m. poly.coeff q k * poly ((pderiv ^^ n) f) (int k))
[PROOF STEP]
have "J = of_int (-(\<Sum>(k,n)\<in>{..n}\<times>{..m}. coeff q k * poly ((pderiv ^^ n) f) (int k)))"
[PROOF STATE]
proof (prove)
using this:
J = 0 * (\<Sum>n\<le>m. of_int (poly ((pderiv ^^ n) f) 0)) - of_int (\<Sum>k\<le>n. \<Sum>n\<le>m. poly.coeff q k * poly ((pderiv ^^ n) f) (int k))

goal (1 subgoal):
 1. J = of_int (- (\<Sum>(k, n)\<in>{..n} \<times> {..m}. poly.coeff q k * poly ((pderiv ^^ n) f) (int k)))
[PROOF STEP]
by (simp add: sum.cartesian_product)
[PROOF STATE]
proof (state)
this:
J = of_int (- (\<Sum>(k, n)\<in>{..n} \<times> {..m}. poly.coeff q k * poly ((pderiv ^^ n) f) (int k)))

goal (1 subgoal):
 1. fact (p - 1) \<le> E * F ^ p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
J = of_int (- (\<Sum>(k, n)\<in>{..n} \<times> {..m}. poly.coeff q k * poly ((pderiv ^^ n) f) (int k)))

goal (1 subgoal):
 1. fact (p - 1) \<le> E * F ^ p
[PROOF STEP]
have "{..n}\<times>{..m} = insert (0, p - 1) idxs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {..n} \<times> {..m} = insert (0, p - 1) idxs
[PROOF STEP]
by (auto simp: m idxs_def)
[PROOF STATE]
proof (state)
this:
{..n} \<times> {..m} = insert (0, p - 1) idxs

goal (1 subgoal):
 1. fact (p - 1) \<le> E * F ^ p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{..n} \<times> {..m} = insert (0, p - 1) idxs

goal (1 subgoal):
 1. fact (p - 1) \<le> E * F ^ p
[PROOF STEP]
have "-(\<Sum>(k,n)\<in>\<dots>. coeff q k * poly ((pderiv ^^ n) f) (int k)) =
       - (coeff q 0 * poly ((pderiv ^^ (p - 1)) f) 0) -
         (\<Sum>(k, n)\<in>idxs. coeff q k * poly ((pderiv ^^ n) f) (of_nat k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - (\<Sum>(k, n)\<in>insert (0, p - 1) idxs. poly.coeff q k * poly ((pderiv ^^ n) f) (int k)) = - (poly.coeff q 0 * poly ((pderiv ^^ (p - 1)) f) 0) - (\<Sum>(k, n)\<in>idxs. poly.coeff q k * poly ((pderiv ^^ n) f) (int k))
[PROOF STEP]
by (subst sum.insert) (simp_all add: idxs_def)
[PROOF STATE]
proof (state)
this:
- (\<Sum>(k, n)\<in>insert (0, p - 1) idxs. poly.coeff q k * poly ((pderiv ^^ n) f) (int k)) = - (poly.coeff q 0 * poly ((pderiv ^^ (p - 1)) f) 0) - (\<Sum>(k, n)\<in>idxs. poly.coeff q k * poly ((pderiv ^^ n) f) (int k))

goal (1 subgoal):
 1. fact (p - 1) \<le> E * F ^ p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
- (\<Sum>(k, n)\<in>insert (0, p - 1) idxs. poly.coeff q k * poly ((pderiv ^^ n) f) (int k)) = - (poly.coeff q 0 * poly ((pderiv ^^ (p - 1)) f) 0) - (\<Sum>(k, n)\<in>idxs. poly.coeff q k * poly ((pderiv ^^ n) f) (int k))

goal (1 subgoal):
 1. fact (p - 1) \<le> E * F ^ p
[PROOF STEP]
have "coeff q 0 * poly ((pderiv ^^ (p - 1)) f) 0 = coeff q 0 * M * fact (p - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly.coeff q 0 * poly ((pderiv ^^ (p - 1)) f) 0 = poly.coeff q 0 * M * fact (p - 1)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. poly.coeff q 0 * poly ((pderiv ^^ (p - 1)) f) 0 = poly.coeff q 0 * M * fact (p - 1)
[PROOF STEP]
have "f = [:-0, 1:] ^ (p - 1) * (\<Prod>k = 1..n. [:- of_nat k, 1:] ^ p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f = [:- 0, 1:] ^ (p - 1) * (\<Prod>k = 1..n. [:- int k, 1:] ^ p)
[PROOF STEP]
by (simp add: f_def monom_altdef)
[PROOF STATE]
proof (state)
this:
f = [:- 0, 1:] ^ (p - 1) * (\<Prod>k = 1..n. [:- int k, 1:] ^ p)

goal (1 subgoal):
 1. poly.coeff q 0 * poly ((pderiv ^^ (p - 1)) f) 0 = poly.coeff q 0 * M * fact (p - 1)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f = [:- 0, 1:] ^ (p - 1) * (\<Prod>k = 1..n. [:- int k, 1:] ^ p)

goal (1 subgoal):
 1. poly.coeff q 0 * poly ((pderiv ^^ (p - 1)) f) 0 = poly.coeff q 0 * M * fact (p - 1)
[PROOF STEP]
have "poly ((pderiv ^^ (p - 1)) \<dots>) 0 =
                   fact (p - 1) * poly (\<Prod>k = 1..n. [:- of_nat k, 1:] ^ p) 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly ((pderiv ^^ (p - 1)) ([:- 0, 1:] ^ (p - 1) * (\<Prod>k = 1..n. [:- int k, 1:] ^ p))) 0 = fact (p - 1) * poly (\<Prod>k = 1..n. [:- int k, 1:] ^ p) 0
[PROOF STEP]
by (rule poly_higher_pderiv_aux2)
[PROOF STATE]
proof (state)
this:
poly ((pderiv ^^ (p - 1)) ([:- 0, 1:] ^ (p - 1) * (\<Prod>k = 1..n. [:- int k, 1:] ^ p))) 0 = fact (p - 1) * poly (\<Prod>k = 1..n. [:- int k, 1:] ^ p) 0

goal (1 subgoal):
 1. poly.coeff q 0 * poly ((pderiv ^^ (p - 1)) f) 0 = poly.coeff q 0 * M * fact (p - 1)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
poly ((pderiv ^^ (p - 1)) ([:- 0, 1:] ^ (p - 1) * (\<Prod>k = 1..n. [:- int k, 1:] ^ p))) 0 = fact (p - 1) * poly (\<Prod>k = 1..n. [:- int k, 1:] ^ p) 0

goal (1 subgoal):
 1. poly.coeff q 0 * poly ((pderiv ^^ (p - 1)) f) 0 = poly.coeff q 0 * M * fact (p - 1)
[PROOF STEP]
have "poly (\<Prod>k = 1..n. [:- of_nat k :: int, 1:] ^ p) 0 = (-1)^(n*p) * fact n ^ p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly (\<Prod>k = 1..n. [:- int k, 1:] ^ p) 0 = (- 1) ^ (n * p) * fact n ^ p
[PROOF STEP]
by (induction n) (simp_all add: prod.nat_ivl_Suc' power_mult_distrib mult_ac
                            power_minus' power_add del: of_nat_Suc)
[PROOF STATE]
proof (state)
this:
poly (\<Prod>k = 1..n. [:- int k, 1:] ^ p) 0 = (- 1) ^ (n * p) * fact n ^ p

goal (1 subgoal):
 1. poly.coeff q 0 * poly ((pderiv ^^ (p - 1)) f) 0 = poly.coeff q 0 * M * fact (p - 1)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
poly ((pderiv ^^ (p - 1)) f) 0 = fact (p - 1) * ((- 1) ^ (n * p) * fact n ^ p)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
poly ((pderiv ^^ (p - 1)) f) 0 = fact (p - 1) * ((- 1) ^ (n * p) * fact n ^ p)

goal (1 subgoal):
 1. poly.coeff q 0 * poly ((pderiv ^^ (p - 1)) f) 0 = poly.coeff q 0 * M * fact (p - 1)
[PROOF STEP]
by (simp add: mult_ac M_def)
[PROOF STATE]
proof (state)
this:
poly.coeff q 0 * poly ((pderiv ^^ (p - 1)) f) 0 = poly.coeff q 0 * M * fact (p - 1)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
poly.coeff q 0 * poly ((pderiv ^^ (p - 1)) f) 0 = poly.coeff q 0 * M * fact (p - 1)

goal (1 subgoal):
 1. fact (p - 1) \<le> E * F ^ p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
poly.coeff q 0 * poly ((pderiv ^^ (p - 1)) f) 0 = poly.coeff q 0 * M * fact (p - 1)

goal (1 subgoal):
 1. fact (p - 1) \<le> E * F ^ p
[PROOF STEP]
obtain N where "(\<Sum>(k, n)\<in>idxs. coeff q k * poly ((pderiv ^^ n) f) (int k)) = fact p * N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>N. (\<Sum>(k, n)\<in>idxs. poly.coeff q k * poly ((pderiv ^^ n) f) (int k)) = fact p * N \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>N. (\<Sum>(k, n)\<in>idxs. poly.coeff q k * poly ((pderiv ^^ n) f) (int k)) = fact p * N \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "\<forall>(k, n)\<in>idxs. fact p dvd poly ((pderiv ^^ n) f) (of_nat k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(k, n)\<in>idxs. fact p dvd poly ((pderiv ^^ n) f) (int k)
[PROOF STEP]
proof clarify
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> idxs \<Longrightarrow> fact p dvd poly ((pderiv ^^ b) f) (int a)
[PROOF STEP]
fix k j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> idxs \<Longrightarrow> fact p dvd poly ((pderiv ^^ b) f) (int a)
[PROOF STEP]
assume idxs: "(k, j) \<in> idxs"
[PROOF STATE]
proof (state)
this:
(k, j) \<in> idxs

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> idxs \<Longrightarrow> fact p dvd poly ((pderiv ^^ b) f) (int a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(k, j) \<in> idxs
[PROOF STEP]
consider "k = 0" "j < p - 1" | "k = 0" "j > p - 1" | "k \<noteq> 0" "j < p" | "k \<noteq> 0" "j \<ge> p"
[PROOF STATE]
proof (prove)
using this:
(k, j) \<in> idxs

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>k = 0; j < p - 1\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>k = 0; p - 1 < j\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>k \<noteq> 0; j < p\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>k \<noteq> 0; p \<le> j\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (fastforce simp: idxs_def)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<lbrakk>k = 0; j < p - 1\<rbrakk> \<Longrightarrow> ?thesis; \<lbrakk>k = 0; p - 1 < j\<rbrakk> \<Longrightarrow> ?thesis; \<lbrakk>k \<noteq> 0; j < p\<rbrakk> \<Longrightarrow> ?thesis; \<lbrakk>k \<noteq> 0; p \<le> j\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> idxs \<Longrightarrow> fact p dvd poly ((pderiv ^^ b) f) (int a)
[PROOF STEP]
thus "fact p dvd poly ((pderiv ^^ j) f) (of_nat k)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<lbrakk>k = 0; j < p - 1\<rbrakk> \<Longrightarrow> ?thesis; \<lbrakk>k = 0; p - 1 < j\<rbrakk> \<Longrightarrow> ?thesis; \<lbrakk>k \<noteq> 0; j < p\<rbrakk> \<Longrightarrow> ?thesis; \<lbrakk>k \<noteq> 0; p \<le> j\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. fact p dvd poly ((pderiv ^^ j) f) (int k)
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<lbrakk>k = 0; j < p - 1\<rbrakk> \<Longrightarrow> fact p dvd poly ((pderiv ^^ j) f) (int k)
 2. \<lbrakk>k = 0; p - 1 < j\<rbrakk> \<Longrightarrow> fact p dvd poly ((pderiv ^^ j) f) (int k)
 3. \<lbrakk>k \<noteq> 0; j < p\<rbrakk> \<Longrightarrow> fact p dvd poly ((pderiv ^^ j) f) (int k)
 4. \<lbrakk>k \<noteq> 0; p \<le> j\<rbrakk> \<Longrightarrow> fact p dvd poly ((pderiv ^^ j) f) (int k)
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
k = 0
j < p - 1

goal (4 subgoals):
 1. \<lbrakk>k = 0; j < p - 1\<rbrakk> \<Longrightarrow> fact p dvd poly ((pderiv ^^ j) f) (int k)
 2. \<lbrakk>k = 0; p - 1 < j\<rbrakk> \<Longrightarrow> fact p dvd poly ((pderiv ^^ j) f) (int k)
 3. \<lbrakk>k \<noteq> 0; j < p\<rbrakk> \<Longrightarrow> fact p dvd poly ((pderiv ^^ j) f) (int k)
 4. \<lbrakk>k \<noteq> 0; p \<le> j\<rbrakk> \<Longrightarrow> fact p dvd poly ((pderiv ^^ j) f) (int k)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
k = 0
j < p - 1

goal (1 subgoal):
 1. fact p dvd poly ((pderiv ^^ j) f) (int k)
[PROOF STEP]
by (simp add: f_def poly_higher_pderiv_aux1' monom_altdef)
[PROOF STATE]
proof (state)
this:
fact p dvd poly ((pderiv ^^ j) f) (int k)

goal (3 subgoals):
 1. \<lbrakk>k = 0; p - 1 < j\<rbrakk> \<Longrightarrow> fact p dvd poly ((pderiv ^^ j) f) (int k)
 2. \<lbrakk>k \<noteq> 0; j < p\<rbrakk> \<Longrightarrow> fact p dvd poly ((pderiv ^^ j) f) (int k)
 3. \<lbrakk>k \<noteq> 0; p \<le> j\<rbrakk> \<Longrightarrow> fact p dvd poly ((pderiv ^^ j) f) (int k)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrakk>k = 0; p - 1 < j\<rbrakk> \<Longrightarrow> fact p dvd poly ((pderiv ^^ j) f) (int k)
 2. \<lbrakk>k \<noteq> 0; j < p\<rbrakk> \<Longrightarrow> fact p dvd poly ((pderiv ^^ j) f) (int k)
 3. \<lbrakk>k \<noteq> 0; p \<le> j\<rbrakk> \<Longrightarrow> fact p dvd poly ((pderiv ^^ j) f) (int k)
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
k = 0
p - 1 < j

goal (3 subgoals):
 1. \<lbrakk>k = 0; p - 1 < j\<rbrakk> \<Longrightarrow> fact p dvd poly ((pderiv ^^ j) f) (int k)
 2. \<lbrakk>k \<noteq> 0; j < p\<rbrakk> \<Longrightarrow> fact p dvd poly ((pderiv ^^ j) f) (int k)
 3. \<lbrakk>k \<noteq> 0; p \<le> j\<rbrakk> \<Longrightarrow> fact p dvd poly ((pderiv ^^ j) f) (int k)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
k = 0
p - 1 < j

goal (1 subgoal):
 1. fact p dvd poly ((pderiv ^^ j) f) (int k)
[PROOF STEP]
by (simp add: f_def poly_higher_pderiv_aux3' monom_altdef fact_dvd_poly_higher_pderiv_aux')
[PROOF STATE]
proof (state)
this:
fact p dvd poly ((pderiv ^^ j) f) (int k)

goal (2 subgoals):
 1. \<lbrakk>k \<noteq> 0; j < p\<rbrakk> \<Longrightarrow> fact p dvd poly ((pderiv ^^ j) f) (int k)
 2. \<lbrakk>k \<noteq> 0; p \<le> j\<rbrakk> \<Longrightarrow> fact p dvd poly ((pderiv ^^ j) f) (int k)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>k \<noteq> 0; j < p\<rbrakk> \<Longrightarrow> fact p dvd poly ((pderiv ^^ j) f) (int k)
 2. \<lbrakk>k \<noteq> 0; p \<le> j\<rbrakk> \<Longrightarrow> fact p dvd poly ((pderiv ^^ j) f) (int k)
[PROOF STEP]
case 3
[PROOF STATE]
proof (state)
this:
k \<noteq> 0
j < p

goal (2 subgoals):
 1. \<lbrakk>k \<noteq> 0; j < p\<rbrakk> \<Longrightarrow> fact p dvd poly ((pderiv ^^ j) f) (int k)
 2. \<lbrakk>k \<noteq> 0; p \<le> j\<rbrakk> \<Longrightarrow> fact p dvd poly ((pderiv ^^ j) f) (int k)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
k \<noteq> 0
j < p

goal (1 subgoal):
 1. fact p dvd poly ((pderiv ^^ j) f) (int k)
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
using this:
k \<noteq> 0
j < p

goal (1 subgoal):
 1. fact p dvd poly ((pderiv ^^ j) (Polynomial.monom 1 (p - 1) * (\<Prod>k = 1..n. [:- int k, 1:] ^ p))) (int k)
[PROOF STEP]
by (subst poly_higher_pderiv_aux1'[of _ p])
               (insert idxs, auto simp: idxs_def intro!: dvd_mult)
[PROOF STATE]
proof (state)
this:
fact p dvd poly ((pderiv ^^ j) f) (int k)

goal (1 subgoal):
 1. \<lbrakk>k \<noteq> 0; p \<le> j\<rbrakk> \<Longrightarrow> fact p dvd poly ((pderiv ^^ j) f) (int k)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>k \<noteq> 0; p \<le> j\<rbrakk> \<Longrightarrow> fact p dvd poly ((pderiv ^^ j) f) (int k)
[PROOF STEP]
case 4
[PROOF STATE]
proof (state)
this:
k \<noteq> 0
p \<le> j

goal (1 subgoal):
 1. \<lbrakk>k \<noteq> 0; p \<le> j\<rbrakk> \<Longrightarrow> fact p dvd poly ((pderiv ^^ j) f) (int k)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
k \<noteq> 0
p \<le> j

goal (1 subgoal):
 1. fact p dvd poly ((pderiv ^^ j) f) (int k)
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
using this:
k \<noteq> 0
p \<le> j

goal (1 subgoal):
 1. fact p dvd poly ((pderiv ^^ j) (Polynomial.monom 1 (p - 1) * (\<Prod>k = 1..n. [:- int k, 1:] ^ p))) (int k)
[PROOF STEP]
by (intro poly_higher_pderiv_aux3') (insert idxs, auto intro!: dvd_mult simp: idxs_def)
[PROOF STATE]
proof (state)
this:
fact p dvd poly ((pderiv ^^ j) f) (int k)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
fact p dvd poly ((pderiv ^^ j) f) (int k)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>(k, n)\<in>idxs. fact p dvd poly ((pderiv ^^ n) f) (int k)

goal (1 subgoal):
 1. (\<And>N. (\<Sum>(k, n)\<in>idxs. poly.coeff q k * poly ((pderiv ^^ n) f) (int k)) = fact p * N \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence "fact p dvd (\<Sum>(k, n)\<in>idxs. coeff q k * poly ((pderiv ^^ n) f) (int k))"
[PROOF STATE]
proof (prove)
using this:
\<forall>(k, n)\<in>idxs. fact p dvd poly ((pderiv ^^ n) f) (int k)

goal (1 subgoal):
 1. fact p dvd (\<Sum>(k, n)\<in>idxs. poly.coeff q k * poly ((pderiv ^^ n) f) (int k))
[PROOF STEP]
by (auto intro!: dvd_sum dvd_mult simp del: of_int_fact)
[PROOF STATE]
proof (state)
this:
fact p dvd (\<Sum>(k, n)\<in>idxs. poly.coeff q k * poly ((pderiv ^^ n) f) (int k))

goal (1 subgoal):
 1. (\<And>N. (\<Sum>(k, n)\<in>idxs. poly.coeff q k * poly ((pderiv ^^ n) f) (int k)) = fact p * N \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with that
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>(k, n)\<in>idxs. poly.coeff q k * poly ((pderiv ^^ n) f) (int k)) = fact p * ?N \<Longrightarrow> thesis
fact p dvd (\<Sum>(k, n)\<in>idxs. poly.coeff q k * poly ((pderiv ^^ n) f) (int k))
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>(k, n)\<in>idxs. poly.coeff q k * poly ((pderiv ^^ n) f) (int k)) = fact p * ?N \<Longrightarrow> thesis
fact p dvd (\<Sum>(k, n)\<in>idxs. poly.coeff q k * poly ((pderiv ^^ n) f) (int k))

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>(k, n)\<in>idxs. poly.coeff q k * poly ((pderiv ^^ n) f) (int k)) = fact p * N

goal (1 subgoal):
 1. fact (p - 1) \<le> E * F ^ p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>(k, n)\<in>idxs. poly.coeff q k * poly ((pderiv ^^ n) f) (int k)) = fact p * N

goal (1 subgoal):
 1. fact (p - 1) \<le> E * F ^ p
[PROOF STEP]
from p
[PROOF STATE]
proof (chain)
picking this:
prime p
n < p
\<bar>poly.coeff q 0\<bar> < int p
[PROOF STEP]
have "- (coeff q 0 * M * fact (p - 1)) - fact p * N =
                        - fact (p - 1) * (coeff q 0 * M + p * N)"
[PROOF STATE]
proof (prove)
using this:
prime p
n < p
\<bar>poly.coeff q 0\<bar> < int p

goal (1 subgoal):
 1. - (poly.coeff q 0 * M * fact (p - 1)) - fact p * N = - fact (p - 1) * (poly.coeff q 0 * M + int p * N)
[PROOF STEP]
by (subst fact_reduce[of p]) (simp_all add: algebra_simps)
[PROOF STATE]
proof (state)
this:
- (poly.coeff q 0 * M * fact (p - 1)) - fact p * N = - fact (p - 1) * (poly.coeff q 0 * M + int p * N)

goal (1 subgoal):
 1. fact (p - 1) \<le> E * F ^ p
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
J = of_int (- fact (p - 1) * (poly.coeff q 0 * M + int p * N))
[PROOF STEP]
have J: "J = -of_int (fact (p - 1) * (coeff q 0 * M + p * N))"
[PROOF STATE]
proof (prove)
using this:
J = of_int (- fact (p - 1) * (poly.coeff q 0 * M + int p * N))

goal (1 subgoal):
 1. J = - of_int (fact (p - 1) * (poly.coeff q 0 * M + int p * N))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
J = - of_int (fact (p - 1) * (poly.coeff q 0 * M + int p * N))

goal (1 subgoal):
 1. fact (p - 1) \<le> E * F ^ p
[PROOF STEP]
from p q(2)
[PROOF STATE]
proof (chain)
picking this:
prime p
n < p
\<bar>poly.coeff q 0\<bar> < int p
poly.coeff q 0 \<noteq> 0
[PROOF STEP]
have "\<not>p dvd coeff q 0 * M + p * N"
[PROOF STATE]
proof (prove)
using this:
prime p
n < p
\<bar>poly.coeff q 0\<bar> < int p
poly.coeff q 0 \<noteq> 0

goal (1 subgoal):
 1. \<not> int p dvd poly.coeff q 0 * M + int p * N
[PROOF STEP]
by (auto simp: dvd_add_left_iff p_not_dvd_M prime_dvd_fact_iff_int prime_dvd_mult_iff
               dest: dvd_imp_le_int)
[PROOF STATE]
proof (state)
this:
\<not> int p dvd poly.coeff q 0 * M + int p * N

goal (1 subgoal):
 1. fact (p - 1) \<le> E * F ^ p
[PROOF STEP]
hence "coeff q 0 * M + p * N \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
\<not> int p dvd poly.coeff q 0 * M + int p * N

goal (1 subgoal):
 1. poly.coeff q 0 * M + int p * N \<noteq> 0
[PROOF STEP]
by (intro notI) simp_all
[PROOF STATE]
proof (state)
this:
poly.coeff q 0 * M + int p * N \<noteq> 0

goal (1 subgoal):
 1. fact (p - 1) \<le> E * F ^ p
[PROOF STEP]
hence "abs (coeff q 0 * M + p * N) \<ge> 1"
[PROOF STATE]
proof (prove)
using this:
poly.coeff q 0 * M + int p * N \<noteq> 0

goal (1 subgoal):
 1. 1 \<le> \<bar>poly.coeff q 0 * M + int p * N\<bar>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1 \<le> \<bar>poly.coeff q 0 * M + int p * N\<bar>

goal (1 subgoal):
 1. fact (p - 1) \<le> E * F ^ p
[PROOF STEP]
hence "norm (of_int (coeff q 0 * M + p * N) :: complex) \<ge> 1"
[PROOF STATE]
proof (prove)
using this:
1 \<le> \<bar>poly.coeff q 0 * M + int p * N\<bar>

goal (1 subgoal):
 1. 1 \<le> cmod (of_int (poly.coeff q 0 * M + int p * N))
[PROOF STEP]
by (simp only: norm_of_int)
[PROOF STATE]
proof (state)
this:
1 \<le> cmod (of_int (poly.coeff q 0 * M + int p * N))

goal (1 subgoal):
 1. fact (p - 1) \<le> E * F ^ p
[PROOF STEP]
hence "fact (p - 1) * \<dots> \<ge> fact (p - 1) * 1"
[PROOF STATE]
proof (prove)
using this:
1 \<le> cmod (of_int (poly.coeff q 0 * M + int p * N))

goal (1 subgoal):
 1. fact (p - 1) * 1 \<le> fact (p - 1) * cmod (of_int (poly.coeff q 0 * M + int p * N))
[PROOF STEP]
by (intro mult_left_mono) simp_all
[PROOF STATE]
proof (state)
this:
fact (p - 1) * 1 \<le> fact (p - 1) * cmod (of_int (poly.coeff q 0 * M + int p * N))

goal (1 subgoal):
 1. fact (p - 1) \<le> E * F ^ p
[PROOF STEP]
hence J_lower: "norm J \<ge> fact (p - 1)"
[PROOF STATE]
proof (prove)
using this:
fact (p - 1) * 1 \<le> fact (p - 1) * cmod (of_int (poly.coeff q 0 * M + int p * N))

goal (1 subgoal):
 1. fact (p - 1) \<le> cmod J
[PROOF STEP]
unfolding J norm_minus_cancel of_int_mult of_int_fact
[PROOF STATE]
proof (prove)
using this:
fact (p - 1) * 1 \<le> fact (p - 1) * cmod (of_int (poly.coeff q 0 * M + int p * N))

goal (1 subgoal):
 1. fact (p - 1) \<le> cmod (fact (p - 1) * of_int (poly.coeff q 0 * M + int p * N))
[PROOF STEP]
by (simp add: norm_mult)
[PROOF STATE]
proof (state)
this:
fact (p - 1) \<le> cmod J

goal (1 subgoal):
 1. fact (p - 1) \<le> E * F ^ p
[PROOF STEP]
have "norm J \<le> (\<Sum>k\<le>n. norm (of_int (coeff q k) * I (of_nat k)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod J \<le> (\<Sum>k\<le>n. cmod (of_int (poly.coeff q k) * I (of_nat k)))
[PROOF STEP]
unfolding J_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod (\<Sum>k\<le>n. of_int (poly.coeff q k) * I (of_nat k)) \<le> (\<Sum>k\<le>n. cmod (of_int (poly.coeff q k) * I (of_nat k)))
[PROOF STEP]
by (rule norm_sum)
[PROOF STATE]
proof (state)
this:
cmod J \<le> (\<Sum>k\<le>n. cmod (of_int (poly.coeff q k) * I (of_nat k)))

goal (1 subgoal):
 1. fact (p - 1) \<le> E * F ^ p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cmod J \<le> (\<Sum>k\<le>n. cmod (of_int (poly.coeff q k) * I (of_nat k)))

goal (1 subgoal):
 1. fact (p - 1) \<le> E * F ^ p
[PROOF STEP]
have "\<dots> \<le> (\<Sum>k\<le>n. of_int qmax * (real n * exp (real n) * real n ^ (p - 1) * C ^ p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>k\<le>n. cmod (of_int (poly.coeff q k) * I (of_nat k))) \<le> (\<Sum>k\<le>n. real_of_int qmax * (real n * exp (real n) * real n ^ (p - 1) * C ^ p))
[PROOF STEP]
proof (intro sum_mono)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. k \<in> {..n} \<Longrightarrow> cmod (of_int (poly.coeff q k) * I (of_nat k)) \<le> real_of_int qmax * (real n * exp (real n) * real n ^ (p - 1) * C ^ p)
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. k \<in> {..n} \<Longrightarrow> cmod (of_int (poly.coeff q k) * I (of_nat k)) \<le> real_of_int qmax * (real n * exp (real n) * real n ^ (p - 1) * C ^ p)
[PROOF STEP]
assume k: "k \<in> {..n}"
[PROOF STATE]
proof (state)
this:
k \<in> {..n}

goal (1 subgoal):
 1. \<And>k. k \<in> {..n} \<Longrightarrow> cmod (of_int (poly.coeff q k) * I (of_nat k)) \<le> real_of_int qmax * (real n * exp (real n) * real n ^ (p - 1) * C ^ p)
[PROOF STEP]
have "n > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n
[PROOF STEP]
by (rule ccontr) simp
[PROOF STATE]
proof (state)
this:
0 < n

goal (1 subgoal):
 1. \<And>k. k \<in> {..n} \<Longrightarrow> cmod (of_int (poly.coeff q k) * I (of_nat k)) \<le> real_of_int qmax * (real n * exp (real n) * real n ^ (p - 1) * C ^ p)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
0 < n

goal (1 subgoal):
 1. \<And>k. k \<in> {..n} \<Longrightarrow> cmod (of_int (poly.coeff q k) * I (of_nat k)) \<le> real_of_int qmax * (real n * exp (real n) * real n ^ (p - 1) * C ^ p)
[PROOF STEP]
fix x :: complex
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. k \<in> {..n} \<Longrightarrow> cmod (of_int (poly.coeff q k) * I (of_nat k)) \<le> real_of_int qmax * (real n * exp (real n) * real n ^ (p - 1) * C ^ p)
[PROOF STEP]
assume x: "x \<in> closed_segment 0 (of_nat k)"
[PROOF STATE]
proof (state)
this:
x \<in> closed_segment 0 (of_nat k)

goal (1 subgoal):
 1. \<And>k. k \<in> {..n} \<Longrightarrow> cmod (of_int (poly.coeff q k) * I (of_nat k)) \<le> real_of_int qmax * (real n * exp (real n) * real n ^ (p - 1) * C ^ p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> closed_segment 0 (of_nat k)
[PROOF STEP]
obtain t where t: "t \<ge> 0" "t \<le> 1" "x = of_real t * of_nat k"
[PROOF STATE]
proof (prove)
using this:
x \<in> closed_segment 0 (of_nat k)

goal (1 subgoal):
 1. (\<And>t. \<lbrakk>0 \<le> t; t \<le> 1; x = complex_of_real t * of_nat k\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: closed_segment_def scaleR_conv_of_real)
[PROOF STATE]
proof (state)
this:
0 \<le> t
t \<le> 1
x = complex_of_real t * of_nat k

goal (1 subgoal):
 1. \<And>k. k \<in> {..n} \<Longrightarrow> cmod (of_int (poly.coeff q k) * I (of_nat k)) \<le> real_of_int qmax * (real n * exp (real n) * real n ^ (p - 1) * C ^ p)
[PROOF STEP]
hence "norm x = t * real k"
[PROOF STATE]
proof (prove)
using this:
0 \<le> t
t \<le> 1
x = complex_of_real t * of_nat k

goal (1 subgoal):
 1. cmod x = t * real k
[PROOF STEP]
by (simp add: norm_mult)
[PROOF STATE]
proof (state)
this:
cmod x = t * real k

goal (1 subgoal):
 1. \<And>k. k \<in> {..n} \<Longrightarrow> cmod (of_int (poly.coeff q k) * I (of_nat k)) \<le> real_of_int qmax * (real n * exp (real n) * real n ^ (p - 1) * C ^ p)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cmod x = t * real k

goal (1 subgoal):
 1. \<And>k. k \<in> {..n} \<Longrightarrow> cmod (of_int (poly.coeff q k) * I (of_nat k)) \<le> real_of_int qmax * (real n * exp (real n) * real n ^ (p - 1) * C ^ p)
[PROOF STEP]
from \<open>t \<le> 1\<close> k
[PROOF STATE]
proof (chain)
picking this:
t \<le> 1
k \<in> {..n}
[PROOF STEP]
have *: "\<dots> \<le> 1 * real n"
[PROOF STATE]
proof (prove)
using this:
t \<le> 1
k \<in> {..n}

goal (1 subgoal):
 1. t * real k \<le> 1 * real n
[PROOF STEP]
by (intro mult_mono) simp_all
[PROOF STATE]
proof (state)
this:
t * real k \<le> 1 * real n

goal (1 subgoal):
 1. \<And>k. k \<in> {..n} \<Longrightarrow> cmod (of_int (poly.coeff q k) * I (of_nat k)) \<le> real_of_int qmax * (real n * exp (real n) * real n ^ (p - 1) * C ^ p)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
cmod x \<le> 1 * real n
[PROOF STEP]
have x': "norm x \<le> real n"
[PROOF STATE]
proof (prove)
using this:
cmod x \<le> 1 * real n

goal (1 subgoal):
 1. cmod x \<le> real n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cmod x \<le> real n

goal (1 subgoal):
 1. \<And>k. k \<in> {..n} \<Longrightarrow> cmod (of_int (poly.coeff q k) * I (of_nat k)) \<le> real_of_int qmax * (real n * exp (real n) * real n ^ (p - 1) * C ^ p)
[PROOF STEP]
from t \<open>n > 0\<close> *
[PROOF STATE]
proof (chain)
picking this:
0 \<le> t
t \<le> 1
x = complex_of_real t * of_nat k
0 < n
t * real k \<le> 1 * real n
[PROOF STEP]
have x'': "x \<in> closed_segment 0 (of_nat n)"
[PROOF STATE]
proof (prove)
using this:
0 \<le> t
t \<le> 1
x = complex_of_real t * of_nat k
0 < n
t * real k \<le> 1 * real n

goal (1 subgoal):
 1. x \<in> closed_segment 0 (of_nat n)
[PROOF STEP]
by (auto simp: closed_segment_def scaleR_conv_of_real field_simps
                   intro!: exI[of _ "t * real k / real n"] )
[PROOF STATE]
proof (state)
this:
x \<in> closed_segment 0 (of_nat n)

goal (1 subgoal):
 1. \<And>k. k \<in> {..n} \<Longrightarrow> cmod (of_int (poly.coeff q k) * I (of_nat k)) \<le> real_of_int qmax * (real n * exp (real n) * real n ^ (p - 1) * C ^ p)
[PROOF STEP]
have "norm (poly (of_int_poly f) x) =
                norm x ^ (p - 1) * cmod (\<Prod>i = 1..n. x - i) ^ p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod (poly (of_int_poly f) x) = cmod x ^ (p - 1) * cmod (\<Prod>i = 1..n. x - of_nat i) ^ p
[PROOF STEP]
by (simp add: poly_f norm_mult norm_power)
[PROOF STATE]
proof (state)
this:
cmod (poly (of_int_poly f) x) = cmod x ^ (p - 1) * cmod (\<Prod>i = 1..n. x - of_nat i) ^ p

goal (1 subgoal):
 1. \<And>k. k \<in> {..n} \<Longrightarrow> cmod (of_int (poly.coeff q k) * I (of_nat k)) \<le> real_of_int qmax * (real n * exp (real n) * real n ^ (p - 1) * C ^ p)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cmod (poly (of_int_poly f) x) = cmod x ^ (p - 1) * cmod (\<Prod>i = 1..n. x - of_nat i) ^ p

goal (1 subgoal):
 1. \<And>k. k \<in> {..n} \<Longrightarrow> cmod (of_int (poly.coeff q k) * I (of_nat k)) \<le> real_of_int qmax * (real n * exp (real n) * real n ^ (p - 1) * C ^ p)
[PROOF STEP]
from x x' x''
[PROOF STATE]
proof (chain)
picking this:
x \<in> closed_segment 0 (of_nat k)
cmod x \<le> real n
x \<in> closed_segment 0 (of_nat n)
[PROOF STEP]
have "\<dots> \<le> of_nat n ^ (p - 1) * C ^ p"
[PROOF STATE]
proof (prove)
using this:
x \<in> closed_segment 0 (of_nat k)
cmod x \<le> real n
x \<in> closed_segment 0 (of_nat n)

goal (1 subgoal):
 1. cmod x ^ (p - 1) * cmod (\<Prod>i = 1..n. x - of_nat i) ^ p \<le> real n ^ (p - 1) * C ^ p
[PROOF STEP]
by (intro mult_mono C power_mono) simp_all
[PROOF STATE]
proof (state)
this:
cmod x ^ (p - 1) * cmod (\<Prod>i = 1..n. x - of_nat i) ^ p \<le> real n ^ (p - 1) * C ^ p

goal (1 subgoal):
 1. \<And>k. k \<in> {..n} \<Longrightarrow> cmod (of_int (poly.coeff q k) * I (of_nat k)) \<le> real_of_int qmax * (real n * exp (real n) * real n ^ (p - 1) * C ^ p)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
cmod (poly (of_int_poly f) x) \<le> real n ^ (p - 1) * C ^ p
[PROOF STEP]
have "norm (poly (of_int_poly f) x) \<le> real n ^ (p - 1) * C ^ p"
[PROOF STATE]
proof (prove)
using this:
cmod (poly (of_int_poly f) x) \<le> real n ^ (p - 1) * C ^ p

goal (1 subgoal):
 1. cmod (poly (of_int_poly f) x) \<le> real n ^ (p - 1) * C ^ p
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
cmod (poly (of_int_poly f) x) \<le> real n ^ (p - 1) * C ^ p

goal (1 subgoal):
 1. \<And>k. k \<in> {..n} \<Longrightarrow> cmod (of_int (poly.coeff q k) * I (of_nat k)) \<le> real_of_int qmax * (real n * exp (real n) * real n ^ (p - 1) * C ^ p)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?x2 \<in> closed_segment 0 (of_nat k) \<Longrightarrow> cmod (poly (of_int_poly f) ?x2) \<le> real n ^ (p - 1) * C ^ p

goal (1 subgoal):
 1. \<And>k. k \<in> {..n} \<Longrightarrow> cmod (of_int (poly.coeff q k) * I (of_nat k)) \<le> real_of_int qmax * (real n * exp (real n) * real n ^ (p - 1) * C ^ p)
[PROOF STEP]
note A = this
[PROOF STATE]
proof (state)
this:
?x2 \<in> closed_segment 0 (of_nat k) \<Longrightarrow> cmod (poly (of_int_poly f) ?x2) \<le> real n ^ (p - 1) * C ^ p

goal (1 subgoal):
 1. \<And>k. k \<in> {..n} \<Longrightarrow> cmod (of_int (poly.coeff q k) * I (of_nat k)) \<le> real_of_int qmax * (real n * exp (real n) * real n ^ (p - 1) * C ^ p)
[PROOF STEP]
have "norm (I (of_nat k)) \<le>
                      cmod (of_nat k) * exp (cmod (of_nat k)) * (of_nat n ^ (p - 1) * C ^ p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod (I (of_nat k)) \<le> cmod (of_nat k) * exp (cmod (of_nat k)) * (real n ^ (p - 1) * C ^ p)
[PROOF STEP]
by (intro lindemann_weierstrass_integral_bound[OF _ A]
              C mult_nonneg_nonneg zero_le_power) auto
[PROOF STATE]
proof (state)
this:
cmod (I (of_nat k)) \<le> cmod (of_nat k) * exp (cmod (of_nat k)) * (real n ^ (p - 1) * C ^ p)

goal (1 subgoal):
 1. \<And>k. k \<in> {..n} \<Longrightarrow> cmod (of_int (poly.coeff q k) * I (of_nat k)) \<le> real_of_int qmax * (real n * exp (real n) * real n ^ (p - 1) * C ^ p)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cmod (I (of_nat k)) \<le> cmod (of_nat k) * exp (cmod (of_nat k)) * (real n ^ (p - 1) * C ^ p)

goal (1 subgoal):
 1. \<And>k. k \<in> {..n} \<Longrightarrow> cmod (of_int (poly.coeff q k) * I (of_nat k)) \<le> real_of_int qmax * (real n * exp (real n) * real n ^ (p - 1) * C ^ p)
[PROOF STEP]
have "\<dots> \<le> cmod (of_nat n) * exp (cmod (of_nat n)) * (of_nat n ^ (p - 1) * C ^ p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod (of_nat k) * exp (cmod (of_nat k)) * (real n ^ (p - 1) * C ^ p) \<le> cmod (of_nat n) * exp (cmod (of_nat n)) * (real n ^ (p - 1) * C ^ p)
[PROOF STEP]
using k
[PROOF STATE]
proof (prove)
using this:
k \<in> {..n}

goal (1 subgoal):
 1. cmod (of_nat k) * exp (cmod (of_nat k)) * (real n ^ (p - 1) * C ^ p) \<le> cmod (of_nat n) * exp (cmod (of_nat n)) * (real n ^ (p - 1) * C ^ p)
[PROOF STEP]
by (intro mult_mono zero_le_power mult_nonneg_nonneg C) simp_all
[PROOF STATE]
proof (state)
this:
cmod (of_nat k) * exp (cmod (of_nat k)) * (real n ^ (p - 1) * C ^ p) \<le> cmod (of_nat n) * exp (cmod (of_nat n)) * (real n ^ (p - 1) * C ^ p)

goal (1 subgoal):
 1. \<And>k. k \<in> {..n} \<Longrightarrow> cmod (of_int (poly.coeff q k) * I (of_nat k)) \<le> real_of_int qmax * (real n * exp (real n) * real n ^ (p - 1) * C ^ p)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
cmod (I (of_nat k)) \<le> cmod (of_nat n) * exp (cmod (of_nat n)) * (real n ^ (p - 1) * C ^ p)
[PROOF STEP]
show "cmod (of_int (coeff q k) * I (of_nat k)) \<le>
                      of_int qmax * (real n * exp (real n) * real n ^ (p - 1) * C ^ p)"
[PROOF STATE]
proof (prove)
using this:
cmod (I (of_nat k)) \<le> cmod (of_nat n) * exp (cmod (of_nat n)) * (real n ^ (p - 1) * C ^ p)

goal (1 subgoal):
 1. cmod (of_int (poly.coeff q k) * I (of_nat k)) \<le> real_of_int qmax * (real n * exp (real n) * real n ^ (p - 1) * C ^ p)
[PROOF STEP]
unfolding norm_mult
[PROOF STATE]
proof (prove)
using this:
cmod (I (of_nat k)) \<le> cmod (of_nat n) * exp (cmod (of_nat n)) * (real n ^ (p - 1) * C ^ p)

goal (1 subgoal):
 1. cmod (of_int (poly.coeff q k)) * cmod (I (of_nat k)) \<le> real_of_int qmax * (real n * exp (real n) * real n ^ (p - 1) * C ^ p)
[PROOF STEP]
by (intro mult_mono) (simp_all add: qmax of_int_abs [symmetric] del: of_int_abs)
[PROOF STATE]
proof (state)
this:
cmod (of_int (poly.coeff q k) * I (of_nat k)) \<le> real_of_int qmax * (real n * exp (real n) * real n ^ (p - 1) * C ^ p)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>k\<le>n. cmod (of_int (poly.coeff q k) * I (of_nat k))) \<le> (\<Sum>k\<le>n. real_of_int qmax * (real n * exp (real n) * real n ^ (p - 1) * C ^ p))

goal (1 subgoal):
 1. fact (p - 1) \<le> E * F ^ p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>k\<le>n. cmod (of_int (poly.coeff q k) * I (of_nat k))) \<le> (\<Sum>k\<le>n. real_of_int qmax * (real n * exp (real n) * real n ^ (p - 1) * C ^ p))

goal (1 subgoal):
 1. fact (p - 1) \<le> E * F ^ p
[PROOF STEP]
have "\<dots> = E * F ^ p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>k\<le>n. real_of_int qmax * (real n * exp (real n) * real n ^ (p - 1) * C ^ p)) = E * F ^ p
[PROOF STEP]
using p_pos
[PROOF STATE]
proof (prove)
using this:
0 < p

goal (1 subgoal):
 1. (\<Sum>k\<le>n. real_of_int qmax * (real n * exp (real n) * real n ^ (p - 1) * C ^ p)) = E * F ^ p
[PROOF STEP]
by (simp add: power_diff power_mult_distrib E_def F_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>k\<le>n. real_of_int qmax * (real n * exp (real n) * real n ^ (p - 1) * C ^ p)) = E * F ^ p

goal (1 subgoal):
 1. fact (p - 1) \<le> E * F ^ p
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
cmod J \<le> E * F ^ p
[PROOF STEP]
show "fact (p - 1) \<le> E * F ^ p"
[PROOF STATE]
proof (prove)
using this:
cmod J \<le> E * F ^ p

goal (1 subgoal):
 1. fact (p - 1) \<le> E * F ^ p
[PROOF STEP]
using J_lower
[PROOF STATE]
proof (prove)
using this:
cmod J \<le> E * F ^ p
fact (p - 1) \<le> cmod J

goal (1 subgoal):
 1. fact (p - 1) \<le> E * F ^ p
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
fact (p - 1) \<le> E * F ^ p

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>prime ?p; n < ?p; \<bar>poly.coeff q 0\<bar> < int ?p\<rbrakk> \<Longrightarrow> fact (?p - 1) \<le> E * F ^ ?p

goal (1 subgoal):
 1. algebraic (exp 1) \<Longrightarrow> False
[PROOF STEP]
have "(\<lambda>n. E * F * F ^ (n - 1) / fact (n - 1)) \<longlonglongrightarrow> 0" (is ?P)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. E * F * F ^ (n - 1) / fact (n - 1)) \<longlonglongrightarrow> 0
[PROOF STEP]
by (intro filterlim_compose[OF power_over_fact_tendsto_0' filterlim_minus_nat_at_top])
[PROOF STATE]
proof (state)
this:
(\<lambda>n. E * F * F ^ (n - 1) / fact (n - 1)) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. algebraic (exp 1) \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<lambda>n. E * F * F ^ (n - 1) / fact (n - 1)) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. algebraic (exp 1) \<Longrightarrow> False
[PROOF STEP]
have "?P \<longleftrightarrow> (\<lambda>n. E * F ^ n / fact (n - 1)) \<longlonglongrightarrow> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. E * F * F ^ (n - 1) / fact (n - 1)) \<longlonglongrightarrow> 0 = (\<lambda>n. E * F ^ n / fact (n - 1)) \<longlonglongrightarrow> 0
[PROOF STEP]
by (intro filterlim_cong refl eventually_mono[OF eventually_gt_at_top[of "0::nat"]])
       (auto simp: power_Suc [symmetric] simp del: power_Suc)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. E * F * F ^ (n - 1) / fact (n - 1)) \<longlonglongrightarrow> 0 = (\<lambda>n. E * F ^ n / fact (n - 1)) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. algebraic (exp 1) \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. E * F ^ n / fact (n - 1)) \<longlonglongrightarrow> 0
[PROOF STEP]
have "eventually (\<lambda>n. E * F ^ n / fact (n - 1) < 1) at_top"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. E * F ^ n / fact (n - 1)) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. E * F ^ n / fact (n - 1) < 1
[PROOF STEP]
by (rule order_tendstoD) simp_all
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F n in sequentially. E * F ^ n / fact (n - 1) < 1

goal (1 subgoal):
 1. algebraic (exp 1) \<Longrightarrow> False
[PROOF STEP]
hence "eventually (\<lambda>n. E * F ^ n < fact (n - 1)) at_top"
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F n in sequentially. E * F ^ n / fact (n - 1) < 1

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. E * F ^ n < fact (n - 1)
[PROOF STEP]
by eventually_elim simp
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F n in sequentially. E * F ^ n < fact (n - 1)

goal (1 subgoal):
 1. algebraic (exp 1) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F n in sequentially. E * F ^ n < fact (n - 1)
[PROOF STEP]
obtain P where P: "\<And>n. n \<ge> P \<Longrightarrow> E * F ^ n < fact (n - 1)"
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F n in sequentially. E * F ^ n < fact (n - 1)

goal (1 subgoal):
 1. (\<And>P. (\<And>n. P \<le> n \<Longrightarrow> E * F ^ n < fact (n - 1)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: eventually_at_top_linorder)
[PROOF STATE]
proof (state)
this:
P \<le> ?n \<Longrightarrow> E * F ^ ?n < fact (?n - 1)

goal (1 subgoal):
 1. algebraic (exp 1) \<Longrightarrow> False
[PROOF STEP]
have "\<exists>p. prime p \<and> p > Max {nat (abs (coeff q 0)), n, P}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>p. prime p \<and> Max {nat \<bar>poly.coeff q 0\<bar>, n, P} < p
[PROOF STEP]
by (rule bigger_prime)
[PROOF STATE]
proof (state)
this:
\<exists>p. prime p \<and> Max {nat \<bar>poly.coeff q 0\<bar>, n, P} < p

goal (1 subgoal):
 1. algebraic (exp 1) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. prime p \<and> Max {nat \<bar>poly.coeff q 0\<bar>, n, P} < p
[PROOF STEP]
obtain p where "prime p" "p > Max {nat (abs (coeff q 0)), n, P}"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. prime p \<and> Max {nat \<bar>poly.coeff q 0\<bar>, n, P} < p

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>prime p; Max {nat \<bar>poly.coeff q 0\<bar>, n, P} < p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
prime p
Max {nat \<bar>poly.coeff q 0\<bar>, n, P} < p

goal (1 subgoal):
 1. algebraic (exp 1) \<Longrightarrow> False
[PROOF STEP]
hence "int p > abs (coeff q 0)" "p > n" "p \<ge> P"
[PROOF STATE]
proof (prove)
using this:
prime p
Max {nat \<bar>poly.coeff q 0\<bar>, n, P} < p

goal (1 subgoal):
 1. \<bar>poly.coeff q 0\<bar> < int p &&& n < p &&& P \<le> p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<bar>poly.coeff q 0\<bar> < int p
n < p
P \<le> p

goal (1 subgoal):
 1. algebraic (exp 1) \<Longrightarrow> False
[PROOF STEP]
with ineq[of p] \<open>prime p\<close>
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>prime p; n < p; \<bar>poly.coeff q 0\<bar> < int p\<rbrakk> \<Longrightarrow> fact (p - 1) \<le> E * F ^ p
prime p
\<bar>poly.coeff q 0\<bar> < int p
n < p
P \<le> p
[PROOF STEP]
have "fact (p - 1) \<le> E * F ^ p"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>prime p; n < p; \<bar>poly.coeff q 0\<bar> < int p\<rbrakk> \<Longrightarrow> fact (p - 1) \<le> E * F ^ p
prime p
\<bar>poly.coeff q 0\<bar> < int p
n < p
P \<le> p

goal (1 subgoal):
 1. fact (p - 1) \<le> E * F ^ p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fact (p - 1) \<le> E * F ^ p

goal (1 subgoal):
 1. algebraic (exp 1) \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
fact (p - 1) \<le> E * F ^ p

goal (1 subgoal):
 1. algebraic (exp 1) \<Longrightarrow> False
[PROOF STEP]
from \<open>p \<ge> P\<close>
[PROOF STATE]
proof (chain)
picking this:
P \<le> p
[PROOF STEP]
have "fact (p - 1) > E * F ^ p"
[PROOF STATE]
proof (prove)
using this:
P \<le> p

goal (1 subgoal):
 1. E * F ^ p < fact (p - 1)
[PROOF STEP]
by (rule P)
[PROOF STATE]
proof (state)
this:
E * F ^ p < fact (p - 1)

goal (1 subgoal):
 1. algebraic (exp 1) \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
fact (p - 1) \<le> E * F ^ p
E * F ^ p < fact (p - 1)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
fact (p - 1) \<le> E * F ^ p
E * F ^ p < fact (p - 1)

goal (1 subgoal):
 1. False
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma card_less_if_surj_not_inj:
  "\<lbrakk> finite A; f ` A = B; \<not> inj_on f A \<rbrakk> \<Longrightarrow> card B < card A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; f ` A = B; \<not> inj_on f A\<rbrakk> \<Longrightarrow> card B < card A
[PROOF STEP]
by (metis card_image_le inj_on_iff_eq_card order_le_neq_trans)