[STATEMENT]
lemma hensels_lemma':
  assumes "f \<in> carrier Zp_x"
  assumes "a \<in> carrier Zp"
  assumes "val_Zp (f\<bullet>a) > 2*val_Zp ((pderiv f)\<bullet>a)"
  shows "\<exists>!\<alpha> \<in> carrier Zp. f\<bullet>\<alpha> = \<zero> \<and> val_Zp (a \<ominus> \<alpha>) > val_Zp ((pderiv f)\<bullet>a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!\<alpha>. \<alpha> \<in> carrier Zp \<and> f \<bullet> \<alpha> = \<zero> \<and> val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> \<alpha>)
[PROOF STEP]
proof(cases "f\<bullet>a = \<zero>")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f \<bullet> a = \<zero> \<Longrightarrow> \<exists>!\<alpha>. \<alpha> \<in> carrier Zp \<and> f \<bullet> \<alpha> = \<zero> \<and> val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> \<alpha>)
 2. f \<bullet> a \<noteq> \<zero> \<Longrightarrow> \<exists>!\<alpha>. \<alpha> \<in> carrier Zp \<and> f \<bullet> \<alpha> = \<zero> \<and> val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> \<alpha>)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
f \<bullet> a = \<zero>

goal (2 subgoals):
 1. f \<bullet> a = \<zero> \<Longrightarrow> \<exists>!\<alpha>. \<alpha> \<in> carrier Zp \<and> f \<bullet> \<alpha> = \<zero> \<and> val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> \<alpha>)
 2. f \<bullet> a \<noteq> \<zero> \<Longrightarrow> \<exists>!\<alpha>. \<alpha> \<in> carrier Zp \<and> f \<bullet> \<alpha> = \<zero> \<and> val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> \<alpha>)
[PROOF STEP]
have T0: "pderiv f \<bullet> a \<noteq> \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pderiv f \<bullet> a \<noteq> \<zero>
[PROOF STEP]
apply(rule ccontr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> pderiv f \<bullet> a \<noteq> \<zero> \<Longrightarrow> False
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
eint 2 * val_Zp (pderiv f \<bullet> a) < val_Zp (f \<bullet> a)

goal (1 subgoal):
 1. \<not> pderiv f \<bullet> a \<noteq> \<zero> \<Longrightarrow> False
[PROOF STEP]
unfolding val_Zp_def
[PROOF STATE]
proof (prove)
using this:
eint 2 * (if pderiv f \<bullet> a = \<zero> then \<infinity> else eint (padic_val p (pderiv f \<bullet> a))) < (if f \<bullet> a = \<zero> then \<infinity> else eint (padic_val p (f \<bullet> a)))

goal (1 subgoal):
 1. \<not> pderiv f \<bullet> a \<noteq> \<zero> \<Longrightarrow> False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
pderiv f \<bullet> a \<noteq> \<zero>

goal (2 subgoals):
 1. f \<bullet> a = \<zero> \<Longrightarrow> \<exists>!\<alpha>. \<alpha> \<in> carrier Zp \<and> f \<bullet> \<alpha> = \<zero> \<and> val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> \<alpha>)
 2. f \<bullet> a \<noteq> \<zero> \<Longrightarrow> \<exists>!\<alpha>. \<alpha> \<in> carrier Zp \<and> f \<bullet> \<alpha> = \<zero> \<and> val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> \<alpha>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pderiv f \<bullet> a \<noteq> \<zero>
[PROOF STEP]
have T1: "a \<in> carrier Zp \<and> f\<bullet>a = \<zero> \<and> val_Zp (a \<ominus> a) > val_Zp ((pderiv f)\<bullet>a)"
[PROOF STATE]
proof (prove)
using this:
pderiv f \<bullet> a \<noteq> \<zero>

goal (1 subgoal):
 1. a \<in> carrier Zp \<and> f \<bullet> a = \<zero> \<and> val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> a)
[PROOF STEP]
using assms True
[PROOF STATE]
proof (prove)
using this:
pderiv f \<bullet> a \<noteq> \<zero>
f \<in> carrier (UP Zp)
a \<in> carrier Zp
eint 2 * val_Zp (pderiv f \<bullet> a) < val_Zp (f \<bullet> a)
f \<bullet> a = \<zero>

goal (1 subgoal):
 1. a \<in> carrier Zp \<and> f \<bullet> a = \<zero> \<and> val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> a)
[PROOF STEP]
by(simp add: val_Zp_def)
[PROOF STATE]
proof (state)
this:
a \<in> carrier Zp \<and> f \<bullet> a = \<zero> \<and> val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> a)

goal (2 subgoals):
 1. f \<bullet> a = \<zero> \<Longrightarrow> \<exists>!\<alpha>. \<alpha> \<in> carrier Zp \<and> f \<bullet> \<alpha> = \<zero> \<and> val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> \<alpha>)
 2. f \<bullet> a \<noteq> \<zero> \<Longrightarrow> \<exists>!\<alpha>. \<alpha> \<in> carrier Zp \<and> f \<bullet> \<alpha> = \<zero> \<and> val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> \<alpha>)
[PROOF STEP]
have T2: "\<And>b. b \<in> carrier Zp \<and> f\<bullet>b = \<zero> \<and> val_Zp (a \<ominus> b) > val_Zp ((pderiv f)\<bullet>a) \<Longrightarrow> a = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b. b \<in> carrier Zp \<and> f \<bullet> b = \<zero> \<and> val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> b) \<Longrightarrow> a = b
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>b. b \<in> carrier Zp \<and> f \<bullet> b = \<zero> \<and> val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> b) \<Longrightarrow> a = b
[PROOF STEP]
fix b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>b. b \<in> carrier Zp \<and> f \<bullet> b = \<zero> \<and> val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> b) \<Longrightarrow> a = b
[PROOF STEP]
assume A: "b \<in> carrier Zp \<and> f\<bullet>b = \<zero> \<and> val_Zp (a \<ominus> b) > val_Zp ((pderiv f)\<bullet>a)"
[PROOF STATE]
proof (state)
this:
b \<in> carrier Zp \<and> f \<bullet> b = \<zero> \<and> val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> b)

goal (1 subgoal):
 1. \<And>b. b \<in> carrier Zp \<and> f \<bullet> b = \<zero> \<and> val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> b) \<Longrightarrow> a = b
[PROOF STEP]
obtain h where h_def: "h = b \<ominus> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>h. h = b \<ominus> a \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
h = b \<ominus> a

goal (1 subgoal):
 1. \<And>b. b \<in> carrier Zp \<and> f \<bullet> b = \<zero> \<and> val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> b) \<Longrightarrow> a = b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
h = b \<ominus> a
[PROOF STEP]
have h_fact: "h \<in> carrier Zp \<and> b = a \<oplus> h"
[PROOF STATE]
proof (prove)
using this:
h = b \<ominus> a

goal (1 subgoal):
 1. h \<in> carrier Zp \<and> b = a \<oplus> h
[PROOF STEP]
by (metis A R.l_neg R.minus_closed R.minus_eq R.r_zero add_assoc add_comm assms(2))
[PROOF STATE]
proof (state)
this:
h \<in> carrier Zp \<and> b = a \<oplus> h

goal (1 subgoal):
 1. \<And>b. b \<in> carrier Zp \<and> f \<bullet> b = \<zero> \<and> val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> b) \<Longrightarrow> a = b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
h \<in> carrier Zp \<and> b = a \<oplus> h
[PROOF STEP]
have 1: "f\<bullet>(a \<oplus> h) = \<zero>"
[PROOF STATE]
proof (prove)
using this:
h \<in> carrier Zp \<and> b = a \<oplus> h

goal (1 subgoal):
 1. f \<bullet> (a \<oplus> h) = \<zero>
[PROOF STEP]
using assms A
[PROOF STATE]
proof (prove)
using this:
h \<in> carrier Zp \<and> b = a \<oplus> h
f \<in> carrier (UP Zp)
a \<in> carrier Zp
eint 2 * val_Zp (pderiv f \<bullet> a) < val_Zp (f \<bullet> a)
b \<in> carrier Zp \<and> f \<bullet> b = \<zero> \<and> val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> b)

goal (1 subgoal):
 1. f \<bullet> (a \<oplus> h) = \<zero>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f \<bullet> (a \<oplus> h) = \<zero>

goal (1 subgoal):
 1. \<And>b. b \<in> carrier Zp \<and> f \<bullet> b = \<zero> \<and> val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> b) \<Longrightarrow> a = b
[PROOF STEP]
obtain c where c_def: "c \<in> carrier Zp \<and> f\<bullet>(a \<oplus> h) = (f \<bullet> a) \<oplus> (deriv f a)\<otimes>h \<oplus> c \<otimes>(h[^](2::nat))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>c. c \<in> carrier Zp \<and> f \<bullet> (a \<oplus> h) = f \<bullet> a \<oplus> deriv f a \<otimes> h \<oplus> c \<otimes> h [^] 2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using taylor_deg_1_eval'[of  f a h _ "f \<bullet> a" "deriv f a" ]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>f \<in> carrier (UP Zp); a \<in> carrier Zp; h \<in> carrier Zp; ?c = shift 2 (taylor a f) \<bullet> h; f \<bullet> a = f \<bullet> a; deriv f a = deriv f a\<rbrakk> \<Longrightarrow> f \<bullet> (a \<oplus> h) = f \<bullet> a \<oplus> deriv f a \<otimes> h \<oplus> ?c \<otimes> h [^] 2

goal (1 subgoal):
 1. (\<And>c. c \<in> carrier Zp \<and> f \<bullet> (a \<oplus> h) = f \<bullet> a \<oplus> deriv f a \<otimes> h \<oplus> c \<otimes> h [^] 2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson taylor_closed assms(1) assms(2) to_fun_closed h_fact shift_closed)
[PROOF STATE]
proof (state)
this:
c \<in> carrier Zp \<and> f \<bullet> (a \<oplus> h) = f \<bullet> a \<oplus> deriv f a \<otimes> h \<oplus> c \<otimes> h [^] 2

goal (1 subgoal):
 1. \<And>b. b \<in> carrier Zp \<and> f \<bullet> b = \<zero> \<and> val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> b) \<Longrightarrow> a = b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c \<in> carrier Zp \<and> f \<bullet> (a \<oplus> h) = f \<bullet> a \<oplus> deriv f a \<otimes> h \<oplus> c \<otimes> h [^] 2
[PROOF STEP]
have  "(f \<bullet> a) \<oplus> (deriv f a)\<otimes>h \<oplus> c \<otimes>(h[^](2::nat)) = \<zero>"
[PROOF STATE]
proof (prove)
using this:
c \<in> carrier Zp \<and> f \<bullet> (a \<oplus> h) = f \<bullet> a \<oplus> deriv f a \<otimes> h \<oplus> c \<otimes> h [^] 2

goal (1 subgoal):
 1. f \<bullet> a \<oplus> deriv f a \<otimes> h \<oplus> c \<otimes> h [^] 2 = \<zero>
[PROOF STEP]
by (simp add: "1")
[PROOF STATE]
proof (state)
this:
f \<bullet> a \<oplus> deriv f a \<otimes> h \<oplus> c \<otimes> h [^] 2 = \<zero>

goal (1 subgoal):
 1. \<And>b. b \<in> carrier Zp \<and> f \<bullet> b = \<zero> \<and> val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> b) \<Longrightarrow> a = b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f \<bullet> a \<oplus> deriv f a \<otimes> h \<oplus> c \<otimes> h [^] 2 = \<zero>
[PROOF STEP]
have 2:  "(deriv f a)\<otimes>h \<oplus> c \<otimes>(h[^](2::nat)) = \<zero>"
[PROOF STATE]
proof (prove)
using this:
f \<bullet> a \<oplus> deriv f a \<otimes> h \<oplus> c \<otimes> h [^] 2 = \<zero>

goal (1 subgoal):
 1. deriv f a \<otimes> h \<oplus> c \<otimes> h [^] 2 = \<zero>
[PROOF STEP]
by (simp add: True assms(1) assms(2) deriv_closed h_fact)
[PROOF STATE]
proof (state)
this:
deriv f a \<otimes> h \<oplus> c \<otimes> h [^] 2 = \<zero>

goal (1 subgoal):
 1. \<And>b. b \<in> carrier Zp \<and> f \<bullet> b = \<zero> \<and> val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> b) \<Longrightarrow> a = b
[PROOF STEP]
hence 3: "((deriv f a) \<oplus> c \<otimes>h)\<otimes>h = \<zero>"
[PROOF STATE]
proof (prove)
using this:
deriv f a \<otimes> h \<oplus> c \<otimes> h [^] 2 = \<zero>

goal (1 subgoal):
 1. (deriv f a \<oplus> c \<otimes> h) \<otimes> h = \<zero>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. deriv f a \<otimes> h \<oplus> c \<otimes> h [^] 2 = \<zero> \<Longrightarrow> (deriv f a \<oplus> c \<otimes> h) \<otimes> h = \<zero>
[PROOF STEP]
have "((deriv f a) \<oplus> c \<otimes>h)\<otimes>h = ((deriv f a)\<otimes>h \<oplus> (c \<otimes>h)\<otimes>h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (deriv f a \<oplus> c \<otimes> h) \<otimes> h = deriv f a \<otimes> h \<oplus> c \<otimes> h \<otimes> h
[PROOF STEP]
by (simp add: R.l_distr assms(1) assms(2) c_def deriv_closed h_fact)
[PROOF STATE]
proof (state)
this:
(deriv f a \<oplus> c \<otimes> h) \<otimes> h = deriv f a \<otimes> h \<oplus> c \<otimes> h \<otimes> h

goal (1 subgoal):
 1. deriv f a \<otimes> h \<oplus> c \<otimes> h [^] 2 = \<zero> \<Longrightarrow> (deriv f a \<oplus> c \<otimes> h) \<otimes> h = \<zero>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(deriv f a \<oplus> c \<otimes> h) \<otimes> h = deriv f a \<otimes> h \<oplus> c \<otimes> h \<otimes> h
[PROOF STEP]
have "((deriv f a) \<oplus> c \<otimes>h)\<otimes>h = (deriv f a)\<otimes>h \<oplus> (c \<otimes>(h\<otimes>h))"
[PROOF STATE]
proof (prove)
using this:
(deriv f a \<oplus> c \<otimes> h) \<otimes> h = deriv f a \<otimes> h \<oplus> c \<otimes> h \<otimes> h

goal (1 subgoal):
 1. (deriv f a \<oplus> c \<otimes> h) \<otimes> h = deriv f a \<otimes> h \<oplus> c \<otimes> (h \<otimes> h)
[PROOF STEP]
by (simp add: mult_assoc)
[PROOF STATE]
proof (state)
this:
(deriv f a \<oplus> c \<otimes> h) \<otimes> h = deriv f a \<otimes> h \<oplus> c \<otimes> (h \<otimes> h)

goal (1 subgoal):
 1. deriv f a \<otimes> h \<oplus> c \<otimes> h [^] 2 = \<zero> \<Longrightarrow> (deriv f a \<oplus> c \<otimes> h) \<otimes> h = \<zero>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(deriv f a \<oplus> c \<otimes> h) \<otimes> h = deriv f a \<otimes> h \<oplus> c \<otimes> (h \<otimes> h)
[PROOF STEP]
have "((deriv f a) \<oplus> c \<otimes>h)\<otimes>h = (deriv f a)\<otimes>h \<oplus> (c \<otimes>(h[^](2::nat)))"
[PROOF STATE]
proof (prove)
using this:
(deriv f a \<oplus> c \<otimes> h) \<otimes> h = deriv f a \<otimes> h \<oplus> c \<otimes> (h \<otimes> h)

goal (1 subgoal):
 1. (deriv f a \<oplus> c \<otimes> h) \<otimes> h = deriv f a \<otimes> h \<oplus> c \<otimes> h [^] 2
[PROOF STEP]
using nat_pow_def[of Zp h "2"]
[PROOF STATE]
proof (prove)
using this:
(deriv f a \<oplus> c \<otimes> h) \<otimes> h = deriv f a \<otimes> h \<oplus> c \<otimes> (h \<otimes> h)
h [^] 2 = rec_nat \<one> (\<lambda>u b. b \<otimes> h) 2

goal (1 subgoal):
 1. (deriv f a \<oplus> c \<otimes> h) \<otimes> h = deriv f a \<otimes> h \<oplus> c \<otimes> h [^] 2
[PROOF STEP]
by (simp add: h_fact)
[PROOF STATE]
proof (state)
this:
(deriv f a \<oplus> c \<otimes> h) \<otimes> h = deriv f a \<otimes> h \<oplus> c \<otimes> h [^] 2

goal (1 subgoal):
 1. deriv f a \<otimes> h \<oplus> c \<otimes> h [^] 2 = \<zero> \<Longrightarrow> (deriv f a \<oplus> c \<otimes> h) \<otimes> h = \<zero>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(deriv f a \<oplus> c \<otimes> h) \<otimes> h = deriv f a \<otimes> h \<oplus> c \<otimes> h [^] 2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(deriv f a \<oplus> c \<otimes> h) \<otimes> h = deriv f a \<otimes> h \<oplus> c \<otimes> h [^] 2

goal (1 subgoal):
 1. (deriv f a \<oplus> c \<otimes> h) \<otimes> h = \<zero>
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
(deriv f a \<oplus> c \<otimes> h) \<otimes> h = deriv f a \<otimes> h \<oplus> c \<otimes> h [^] 2
deriv f a \<otimes> h \<oplus> c \<otimes> h [^] 2 = \<zero>

goal (1 subgoal):
 1. (deriv f a \<oplus> c \<otimes> h) \<otimes> h = \<zero>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(deriv f a \<oplus> c \<otimes> h) \<otimes> h = \<zero>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(deriv f a \<oplus> c \<otimes> h) \<otimes> h = \<zero>

goal (1 subgoal):
 1. \<And>b. b \<in> carrier Zp \<and> f \<bullet> b = \<zero> \<and> val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> b) \<Longrightarrow> a = b
[PROOF STEP]
have "h = \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h = \<zero>
[PROOF STEP]
proof(rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. h \<noteq> \<zero> \<Longrightarrow> False
[PROOF STEP]
assume "h \<noteq> \<zero>"
[PROOF STATE]
proof (state)
this:
h \<noteq> \<zero>

goal (1 subgoal):
 1. h \<noteq> \<zero> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
h \<noteq> \<zero>
[PROOF STEP]
have "(deriv f a) \<oplus> c \<otimes>h = \<zero>"
[PROOF STATE]
proof (prove)
using this:
h \<noteq> \<zero>

goal (1 subgoal):
 1. deriv f a \<oplus> c \<otimes> h = \<zero>
[PROOF STEP]
using 2 3
[PROOF STATE]
proof (prove)
using this:
h \<noteq> \<zero>
deriv f a \<otimes> h \<oplus> c \<otimes> h [^] 2 = \<zero>
(deriv f a \<oplus> c \<otimes> h) \<otimes> h = \<zero>

goal (1 subgoal):
 1. deriv f a \<oplus> c \<otimes> h = \<zero>
[PROOF STEP]
by (meson R.m_closed UP_cring.deriv_closed Zp_x_is_UP_cring assms(1) assms(2) c_def h_fact local.integral sum_closed)
[PROOF STATE]
proof (state)
this:
deriv f a \<oplus> c \<otimes> h = \<zero>

goal (1 subgoal):
 1. h \<noteq> \<zero> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
deriv f a \<oplus> c \<otimes> h = \<zero>
[PROOF STEP]
have "(deriv f a) = \<ominus> c \<otimes>h"
[PROOF STATE]
proof (prove)
using this:
deriv f a \<oplus> c \<otimes> h = \<zero>

goal (1 subgoal):
 1. deriv f a = \<ominus> c \<otimes> h
[PROOF STEP]
using R.l_minus R.minus_equality assms(1) assms(2) c_def deriv_closed h_fact
[PROOF STATE]
proof (prove)
using this:
deriv f a \<oplus> c \<otimes> h = \<zero>
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp\<rbrakk> \<Longrightarrow> \<ominus> ?x \<otimes> ?y = \<ominus> (?x \<otimes> ?y)
\<lbrakk>?y \<oplus> ?x = \<zero>; ?x \<in> carrier Zp; ?y \<in> carrier Zp\<rbrakk> \<Longrightarrow> \<ominus> ?x = ?y
f \<in> carrier (UP Zp)
a \<in> carrier Zp
c \<in> carrier Zp \<and> f \<bullet> (a \<oplus> h) = f \<bullet> a \<oplus> deriv f a \<otimes> h \<oplus> c \<otimes> h [^] 2
\<lbrakk>?f \<in> carrier (UP Zp); ?a \<in> carrier Zp\<rbrakk> \<Longrightarrow> deriv ?f ?a \<in> carrier Zp
h \<in> carrier Zp \<and> b = a \<oplus> h

goal (1 subgoal):
 1. deriv f a = \<ominus> c \<otimes> h
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
deriv f a = \<ominus> c \<otimes> h

goal (1 subgoal):
 1. h \<noteq> \<zero> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
deriv f a = \<ominus> c \<otimes> h
[PROOF STEP]
have "val_Zp (deriv f a) = val_Zp (c \<otimes> h)"
[PROOF STATE]
proof (prove)
using this:
deriv f a = \<ominus> c \<otimes> h

goal (1 subgoal):
 1. val_Zp (deriv f a) = val_Zp (c \<otimes> h)
[PROOF STEP]
by (meson R.m_closed \<open>deriv f a \<oplus> c \<otimes> h = \<zero>\<close> assms(1) assms(2) c_def deriv_closed h_fact val_Zp_not_equal_imp_notequal(3))
[PROOF STATE]
proof (state)
this:
val_Zp (deriv f a) = val_Zp (c \<otimes> h)

goal (1 subgoal):
 1. h \<noteq> \<zero> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
val_Zp (deriv f a) = val_Zp (c \<otimes> h)
[PROOF STEP]
have P: "val_Zp (deriv f a) = val_Zp h +  val_Zp c"
[PROOF STATE]
proof (prove)
using this:
val_Zp (deriv f a) = val_Zp (c \<otimes> h)

goal (1 subgoal):
 1. val_Zp (deriv f a) = val_Zp h + val_Zp c
[PROOF STEP]
by (simp add: c_def h_fact val_Zp_mult)
[PROOF STATE]
proof (state)
this:
val_Zp (deriv f a) = val_Zp h + val_Zp c

goal (1 subgoal):
 1. h \<noteq> \<zero> \<Longrightarrow> False
[PROOF STEP]
have "val_Zp (deriv f a) \<ge> val_Zp h "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp h \<le> val_Zp (deriv f a)
[PROOF STEP]
using P val_pos[of c] c_def
[PROOF STATE]
proof (prove)
using this:
val_Zp (deriv f a) = val_Zp h + val_Zp c
c \<in> carrier Zp \<Longrightarrow> 0 \<le> val_Zp c
c \<in> carrier Zp \<and> f \<bullet> (a \<oplus> h) = f \<bullet> a \<oplus> deriv f a \<otimes> h \<oplus> c \<otimes> h [^] 2

goal (1 subgoal):
 1. val_Zp h \<le> val_Zp (deriv f a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
val_Zp h \<le> val_Zp (deriv f a)

goal (1 subgoal):
 1. h \<noteq> \<zero> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
val_Zp h \<le> val_Zp (deriv f a)
[PROOF STEP]
have "val_Zp (deriv f a) \<ge> val_Zp (b \<ominus> a) "
[PROOF STATE]
proof (prove)
using this:
val_Zp h \<le> val_Zp (deriv f a)

goal (1 subgoal):
 1. val_Zp (b \<ominus> a) \<le> val_Zp (deriv f a)
[PROOF STEP]
using h_def
[PROOF STATE]
proof (prove)
using this:
val_Zp h \<le> val_Zp (deriv f a)
h = b \<ominus> a

goal (1 subgoal):
 1. val_Zp (b \<ominus> a) \<le> val_Zp (deriv f a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
val_Zp (b \<ominus> a) \<le> val_Zp (deriv f a)

goal (1 subgoal):
 1. h \<noteq> \<zero> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
val_Zp (b \<ominus> a) \<le> val_Zp (deriv f a)
[PROOF STEP]
have "val_Zp (deriv f a) > val_Zp ((pderiv f)\<bullet>a)"
[PROOF STATE]
proof (prove)
using this:
val_Zp (b \<ominus> a) \<le> val_Zp (deriv f a)

goal (1 subgoal):
 1. val_Zp (pderiv f \<bullet> a) < val_Zp (deriv f a)
[PROOF STEP]
by (metis (no_types, lifting) A assms(2) h_def h_fact minus_a_inv not_less order_trans val_Zp_of_minus)
[PROOF STATE]
proof (state)
this:
val_Zp (pderiv f \<bullet> a) < val_Zp (deriv f a)

goal (1 subgoal):
 1. h \<noteq> \<zero> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
val_Zp (pderiv f \<bullet> a) < val_Zp (deriv f a)
[PROOF STEP]
have P0:"val_Zp (deriv f a) > val_Zp (deriv f a)"
[PROOF STATE]
proof (prove)
using this:
val_Zp (pderiv f \<bullet> a) < val_Zp (deriv f a)

goal (1 subgoal):
 1. val_Zp (deriv f a) < val_Zp (deriv f a)
[PROOF STEP]
by (metis UP_cring.pderiv_eval_deriv Zp_x_is_UP_cring assms(1) assms(2))
[PROOF STATE]
proof (state)
this:
val_Zp (deriv f a) < val_Zp (deriv f a)

goal (1 subgoal):
 1. h \<noteq> \<zero> \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
val_Zp (deriv f a) < val_Zp (deriv f a)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
h = \<zero>

goal (1 subgoal):
 1. \<And>b. b \<in> carrier Zp \<and> f \<bullet> b = \<zero> \<and> val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> b) \<Longrightarrow> a = b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
h = \<zero>
[PROOF STEP]
show "a = b"
[PROOF STATE]
proof (prove)
using this:
h = \<zero>

goal (1 subgoal):
 1. a = b
[PROOF STEP]
by (simp add: assms(2) h_fact)
[PROOF STATE]
proof (state)
this:
a = b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?b2 \<in> carrier Zp \<and> f \<bullet> ?b2 = \<zero> \<and> val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> ?b2) \<Longrightarrow> a = ?b2

goal (2 subgoals):
 1. f \<bullet> a = \<zero> \<Longrightarrow> \<exists>!\<alpha>. \<alpha> \<in> carrier Zp \<and> f \<bullet> \<alpha> = \<zero> \<and> val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> \<alpha>)
 2. f \<bullet> a \<noteq> \<zero> \<Longrightarrow> \<exists>!\<alpha>. \<alpha> \<in> carrier Zp \<and> f \<bullet> \<alpha> = \<zero> \<and> val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> \<alpha>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!\<alpha>. \<alpha> \<in> carrier Zp \<and> f \<bullet> \<alpha> = \<zero> \<and> val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> \<alpha>)
[PROOF STEP]
using T1 T2
[PROOF STATE]
proof (prove)
using this:
a \<in> carrier Zp \<and> f \<bullet> a = \<zero> \<and> val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> a)
?b2 \<in> carrier Zp \<and> f \<bullet> ?b2 = \<zero> \<and> val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> ?b2) \<Longrightarrow> a = ?b2

goal (1 subgoal):
 1. \<exists>!\<alpha>. \<alpha> \<in> carrier Zp \<and> f \<bullet> \<alpha> = \<zero> \<and> val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> \<alpha>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>!\<alpha>. \<alpha> \<in> carrier Zp \<and> f \<bullet> \<alpha> = \<zero> \<and> val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> \<alpha>)

goal (1 subgoal):
 1. f \<bullet> a \<noteq> \<zero> \<Longrightarrow> \<exists>!\<alpha>. \<alpha> \<in> carrier Zp \<and> f \<bullet> \<alpha> = \<zero> \<and> val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> \<alpha>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f \<bullet> a \<noteq> \<zero> \<Longrightarrow> \<exists>!\<alpha>. \<alpha> \<in> carrier Zp \<and> f \<bullet> \<alpha> = \<zero> \<and> val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> \<alpha>)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
f \<bullet> a \<noteq> \<zero>

goal (1 subgoal):
 1. f \<bullet> a \<noteq> \<zero> \<Longrightarrow> \<exists>!\<alpha>. \<alpha> \<in> carrier Zp \<and> f \<bullet> \<alpha> = \<zero> \<and> val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> \<alpha>)
[PROOF STEP]
have F0: "pderiv f \<bullet> a \<noteq> \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pderiv f \<bullet> a \<noteq> \<zero>
[PROOF STEP]
apply(rule ccontr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> pderiv f \<bullet> a \<noteq> \<zero> \<Longrightarrow> False
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
eint 2 * val_Zp (pderiv f \<bullet> a) < val_Zp (f \<bullet> a)

goal (1 subgoal):
 1. \<not> pderiv f \<bullet> a \<noteq> \<zero> \<Longrightarrow> False
[PROOF STEP]
unfolding val_Zp_def
[PROOF STATE]
proof (prove)
using this:
eint 2 * (if pderiv f \<bullet> a = \<zero> then \<infinity> else eint (padic_val p (pderiv f \<bullet> a))) < (if f \<bullet> a = \<zero> then \<infinity> else eint (padic_val p (f \<bullet> a)))

goal (1 subgoal):
 1. \<not> pderiv f \<bullet> a \<noteq> \<zero> \<Longrightarrow> False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
pderiv f \<bullet> a \<noteq> \<zero>

goal (1 subgoal):
 1. f \<bullet> a \<noteq> \<zero> \<Longrightarrow> \<exists>!\<alpha>. \<alpha> \<in> carrier Zp \<and> f \<bullet> \<alpha> = \<zero> \<and> val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> \<alpha>)
[PROOF STEP]
obtain \<alpha> where alpha_def:
       "f\<bullet>\<alpha> = \<zero>"  "\<alpha> \<in> carrier Zp"
       "val_Zp (a \<ominus> \<alpha>) > val_Zp ((pderiv f)\<bullet>a)"
       "(val_Zp (a \<ominus> \<alpha>) = val_Zp (divide (f\<bullet>a) ((pderiv f)\<bullet>a)))"
       "val_Zp ((pderiv f)\<bullet>\<alpha>) = val_Zp ((pderiv f)\<bullet>a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<alpha>. \<lbrakk>f \<bullet> \<alpha> = \<zero>; \<alpha> \<in> carrier Zp; val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> \<alpha>); val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (pderiv f \<bullet> a)); val_Zp (pderiv f \<bullet> \<alpha>) = val_Zp (pderiv f \<bullet> a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms hensels_lemma F0 False
[PROOF STATE]
proof (prove)
using this:
f \<in> carrier (UP Zp)
a \<in> carrier Zp
eint 2 * val_Zp (pderiv f \<bullet> a) < val_Zp (f \<bullet> a)
\<lbrakk>?f \<in> carrier (UP Zp); ?a \<in> carrier Zp; pderiv ?f \<bullet> ?a \<noteq> \<zero>; ?f \<bullet> ?a \<noteq> \<zero>; eint 2 * val_Zp (pderiv ?f \<bullet> ?a) < val_Zp (?f \<bullet> ?a); \<And>\<alpha>. \<lbrakk>?f \<bullet> \<alpha> = \<zero>; \<alpha> \<in> carrier Zp; val_Zp (pderiv ?f \<bullet> ?a) < val_Zp (?a \<ominus> \<alpha>); val_Zp (?a \<ominus> \<alpha>) = val_Zp (local.divide (?f \<bullet> ?a) (pderiv ?f \<bullet> ?a)); val_Zp (pderiv ?f \<bullet> \<alpha>) = val_Zp (pderiv ?f \<bullet> ?a)\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
pderiv f \<bullet> a \<noteq> \<zero>
f \<bullet> a \<noteq> \<zero>

goal (1 subgoal):
 1. (\<And>\<alpha>. \<lbrakk>f \<bullet> \<alpha> = \<zero>; \<alpha> \<in> carrier Zp; val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> \<alpha>); val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (pderiv f \<bullet> a)); val_Zp (pderiv f \<bullet> \<alpha>) = val_Zp (pderiv f \<bullet> a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f \<bullet> \<alpha> = \<zero>
\<alpha> \<in> carrier Zp
val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> \<alpha>)
val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (pderiv f \<bullet> a))
val_Zp (pderiv f \<bullet> \<alpha>) = val_Zp (pderiv f \<bullet> a)

goal (1 subgoal):
 1. f \<bullet> a \<noteq> \<zero> \<Longrightarrow> \<exists>!\<alpha>. \<alpha> \<in> carrier Zp \<and> f \<bullet> \<alpha> = \<zero> \<and> val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> \<alpha>)
[PROOF STEP]
have 0: "\<And>x. x \<in> carrier Zp \<and> f \<bullet> x = \<zero> \<and> val_Zp (a \<ominus> x) > val_Zp (pderiv f \<bullet> a) \<and> val_Zp (pderiv f \<bullet> a) \<noteq> val_Zp (a \<ominus> x) \<Longrightarrow> x= \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> carrier Zp \<and> f \<bullet> x = \<zero> \<and> val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> x) \<and> val_Zp (pderiv f \<bullet> a) \<noteq> val_Zp (a \<ominus> x) \<Longrightarrow> x = \<alpha>
[PROOF STEP]
using alpha_def assms hensels_lemma_unique_root[of f a \<alpha>] F0 False
[PROOF STATE]
proof (prove)
using this:
f \<bullet> \<alpha> = \<zero>
\<alpha> \<in> carrier Zp
val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> \<alpha>)
val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (pderiv f \<bullet> a))
val_Zp (pderiv f \<bullet> \<alpha>) = val_Zp (pderiv f \<bullet> a)
f \<in> carrier (UP Zp)
a \<in> carrier Zp
eint 2 * val_Zp (pderiv f \<bullet> a) < val_Zp (f \<bullet> a)
\<lbrakk>f \<in> carrier (UP Zp); a \<in> carrier Zp; pderiv f \<bullet> a \<noteq> \<zero>; f \<bullet> a \<noteq> \<zero>; eint 2 * val_Zp (pderiv f \<bullet> a) < val_Zp (f \<bullet> a); f \<bullet> \<alpha> = \<zero>; \<alpha> \<in> carrier Zp; val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> \<alpha>); f \<bullet> ?\<beta> = \<zero>; ?\<beta> \<in> carrier Zp; val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> ?\<beta>); val_Zp (pderiv f \<bullet> \<alpha>) = val_Zp (pderiv f \<bullet> a)\<rbrakk> \<Longrightarrow> \<alpha> = ?\<beta>
pderiv f \<bullet> a \<noteq> \<zero>
f \<bullet> a \<noteq> \<zero>

goal (1 subgoal):
 1. \<And>x. x \<in> carrier Zp \<and> f \<bullet> x = \<zero> \<and> val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> x) \<and> val_Zp (pderiv f \<bullet> a) \<noteq> val_Zp (a \<ominus> x) \<Longrightarrow> x = \<alpha>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
?x2 \<in> carrier Zp \<and> f \<bullet> ?x2 = \<zero> \<and> val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> ?x2) \<and> val_Zp (pderiv f \<bullet> a) \<noteq> val_Zp (a \<ominus> ?x2) \<Longrightarrow> ?x2 = \<alpha>

goal (1 subgoal):
 1. f \<bullet> a \<noteq> \<zero> \<Longrightarrow> \<exists>!\<alpha>. \<alpha> \<in> carrier Zp \<and> f \<bullet> \<alpha> = \<zero> \<and> val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> \<alpha>)
[PROOF STEP]
have 1: "\<alpha> \<in> carrier Zp \<and> f \<bullet> \<alpha> = \<zero> \<and> val_Zp (a \<ominus> \<alpha>) > val_Zp (pderiv f \<bullet> a) \<and> val_Zp (pderiv f \<bullet> a) \<noteq> val_Zp (a \<ominus> \<alpha>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> \<in> carrier Zp \<and> f \<bullet> \<alpha> = \<zero> \<and> val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> \<alpha>) \<and> val_Zp (pderiv f \<bullet> a) \<noteq> val_Zp (a \<ominus> \<alpha>)
[PROOF STEP]
using alpha_def order_less_le
[PROOF STATE]
proof (prove)
using this:
f \<bullet> \<alpha> = \<zero>
\<alpha> \<in> carrier Zp
val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> \<alpha>)
val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (pderiv f \<bullet> a))
val_Zp (pderiv f \<bullet> \<alpha>) = val_Zp (pderiv f \<bullet> a)
(?x < ?y) = (?x \<le> ?y \<and> ?x \<noteq> ?y)

goal (1 subgoal):
 1. \<alpha> \<in> carrier Zp \<and> f \<bullet> \<alpha> = \<zero> \<and> val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> \<alpha>) \<and> val_Zp (pderiv f \<bullet> a) \<noteq> val_Zp (a \<ominus> \<alpha>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<alpha> \<in> carrier Zp \<and> f \<bullet> \<alpha> = \<zero> \<and> val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> \<alpha>) \<and> val_Zp (pderiv f \<bullet> a) \<noteq> val_Zp (a \<ominus> \<alpha>)

goal (1 subgoal):
 1. f \<bullet> a \<noteq> \<zero> \<Longrightarrow> \<exists>!\<alpha>. \<alpha> \<in> carrier Zp \<and> f \<bullet> \<alpha> = \<zero> \<and> val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> \<alpha>)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<alpha> \<in> carrier Zp \<and> f \<bullet> \<alpha> = \<zero> \<and> val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> \<alpha>) \<and> val_Zp (pderiv f \<bullet> a) \<noteq> val_Zp (a \<ominus> \<alpha>)

goal (1 subgoal):
 1. \<exists>!\<alpha>. \<alpha> \<in> carrier Zp \<and> f \<bullet> \<alpha> = \<zero> \<and> val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> \<alpha>)
[PROOF STEP]
using 0
[PROOF STATE]
proof (prove)
using this:
\<alpha> \<in> carrier Zp \<and> f \<bullet> \<alpha> = \<zero> \<and> val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> \<alpha>) \<and> val_Zp (pderiv f \<bullet> a) \<noteq> val_Zp (a \<ominus> \<alpha>)
?x2 \<in> carrier Zp \<and> f \<bullet> ?x2 = \<zero> \<and> val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> ?x2) \<and> val_Zp (pderiv f \<bullet> a) \<noteq> val_Zp (a \<ominus> ?x2) \<Longrightarrow> ?x2 = \<alpha>

goal (1 subgoal):
 1. \<exists>!\<alpha>. \<alpha> \<in> carrier Zp \<and> f \<bullet> \<alpha> = \<zero> \<and> val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> \<alpha>)
[PROOF STEP]
by (metis (no_types, opaque_lifting) R.minus_closed alpha_def(1-3) assms(2) equal_val_Zp val_Zp_ultrametric_eq')
[PROOF STATE]
proof (state)
this:
\<exists>!\<alpha>. \<alpha> \<in> carrier Zp \<and> f \<bullet> \<alpha> = \<zero> \<and> val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> \<alpha>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Zp_square_root_criterion:
  assumes "p \<noteq> 2"
  assumes "a \<in> carrier Zp"
  assumes "b \<in> carrier Zp"
  assumes "val_Zp b \<ge> val_Zp a"
  assumes "a \<noteq> \<zero>"
  assumes "b \<noteq> \<zero>"
  shows "\<exists>y \<in> carrier Zp. a[^](2::nat) \<oplus> \<p>\<otimes>b[^](2::nat) = (y [^]\<^bsub>Zp\<^esub> (2::nat))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>y\<in>carrier Zp. a [^] 2 \<oplus> [p] \<cdot> \<one> \<otimes> b [^] 2 = y [^] 2
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>y\<in>carrier Zp. a [^] 2 \<oplus> [p] \<cdot> \<one> \<otimes> b [^] 2 = y [^] 2
[PROOF STEP]
have bounds: "val_Zp a < \<infinity>" "val_Zp a \<ge> 0" "val_Zp b < \<infinity>" "val_Zp b \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (val_Zp a < \<infinity> &&& 0 \<le> val_Zp a) &&& val_Zp b < \<infinity> &&& 0 \<le> val_Zp b
[PROOF STEP]
using assms(2) assms(3) assms(6) assms(5) val_Zp_def val_pos[of b]  val_pos[of a]
[PROOF STATE]
proof (prove)
using this:
a \<in> carrier Zp
b \<in> carrier Zp
b \<noteq> \<zero>
a \<noteq> \<zero>
val_Zp = (\<lambda>x. if x = \<zero> then \<infinity> else eint (padic_val p x))
b \<in> carrier Zp \<Longrightarrow> 0 \<le> val_Zp b
a \<in> carrier Zp \<Longrightarrow> 0 \<le> val_Zp a

goal (1 subgoal):
 1. (val_Zp a < \<infinity> &&& 0 \<le> val_Zp a) &&& val_Zp b < \<infinity> &&& 0 \<le> val_Zp b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
val_Zp a < \<infinity>
0 \<le> val_Zp a
val_Zp b < \<infinity>
0 \<le> val_Zp b

goal (1 subgoal):
 1. \<exists>y\<in>carrier Zp. a [^] 2 \<oplus> [p] \<cdot> \<one> \<otimes> b [^] 2 = y [^] 2
[PROOF STEP]
obtain f where f_def: "f = monom Zp_x \<one> 2  \<oplus>\<^bsub>Zp_x\<^esub> to_polynomial Zp (\<ominus> (a[^](2::nat)\<oplus> \<p>\<otimes>b[^](2::nat)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f. f = monom (UP Zp) \<one> 2 \<oplus>\<^bsub>UP Zp\<^esub> to_polynomial Zp (\<ominus> (a [^] 2 \<oplus> [p] \<cdot> \<one> \<otimes> b [^] 2)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f = monom (UP Zp) \<one> 2 \<oplus>\<^bsub>UP Zp\<^esub> to_polynomial Zp (\<ominus> (a [^] 2 \<oplus> [p] \<cdot> \<one> \<otimes> b [^] 2))

goal (1 subgoal):
 1. \<exists>y\<in>carrier Zp. a [^] 2 \<oplus> [p] \<cdot> \<one> \<otimes> b [^] 2 = y [^] 2
[PROOF STEP]
have "\<exists> \<alpha>. f\<bullet>\<alpha> = \<zero> \<and> \<alpha> \<in> carrier Zp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<alpha>. f \<bullet> \<alpha> = \<zero> \<and> \<alpha> \<in> carrier Zp
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>\<alpha>. f \<bullet> \<alpha> = \<zero> \<and> \<alpha> \<in> carrier Zp
[PROOF STEP]
have 0: "f \<in> carrier Zp_x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> carrier (UP Zp)
[PROOF STEP]
using f_def
[PROOF STATE]
proof (prove)
using this:
f = monom (UP Zp) \<one> 2 \<oplus>\<^bsub>UP Zp\<^esub> to_polynomial Zp (\<ominus> (a [^] 2 \<oplus> [p] \<cdot> \<one> \<otimes> b [^] 2))

goal (1 subgoal):
 1. f \<in> carrier (UP Zp)
[PROOF STEP]
by (simp add: X_closed assms(2) assms(3) to_poly_closed)
[PROOF STATE]
proof (state)
this:
f \<in> carrier (UP Zp)

goal (1 subgoal):
 1. \<exists>\<alpha>. f \<bullet> \<alpha> = \<zero> \<and> \<alpha> \<in> carrier Zp
[PROOF STEP]
have 1: "(pderiv f)\<bullet>a = [(2::nat)] \<cdot> \<one> \<otimes> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pderiv f \<bullet> a = [2] \<cdot> \<one> \<otimes> a
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pderiv f \<bullet> a = [2] \<cdot> \<one> \<otimes> a
[PROOF STEP]
have "pderiv f = pderiv (monom Zp_x \<one> 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pderiv f = pderiv (monom (UP Zp) \<one> 2)
[PROOF STEP]
using assms f_def pderiv_add[of "monom Zp_x \<one> 2"] to_poly_closed R.nat_pow_closed
              pderiv_deg_0
[PROOF STATE]
proof (prove)
using this:
p \<noteq> 2
a \<in> carrier Zp
b \<in> carrier Zp
val_Zp a \<le> val_Zp b
a \<noteq> \<zero>
b \<noteq> \<zero>
f = monom (UP Zp) \<one> 2 \<oplus>\<^bsub>UP Zp\<^esub> to_polynomial Zp (\<ominus> (a [^] 2 \<oplus> [p] \<cdot> \<one> \<otimes> b [^] 2))
\<lbrakk>monom (UP Zp) \<one> 2 \<in> carrier (UP Zp); ?q \<in> carrier (UP Zp)\<rbrakk> \<Longrightarrow> pderiv (monom (UP Zp) \<one> 2 \<oplus>\<^bsub>UP Zp\<^esub> ?q) = pderiv (monom (UP Zp) \<one> 2) \<oplus>\<^bsub>UP Zp\<^esub> pderiv ?q
?a \<in> carrier Zp \<Longrightarrow> to_polynomial Zp ?a \<in> carrier (UP Zp)
?x \<in> carrier Zp \<Longrightarrow> ?x [^] ?n \<in> carrier Zp
\<lbrakk>?f \<in> carrier (UP Zp); deg Zp ?f = 0\<rbrakk> \<Longrightarrow> pderiv ?f = \<zero>\<^bsub>UP Zp\<^esub>

goal (1 subgoal):
 1. pderiv f = pderiv (monom (UP Zp) \<one> 2)
[PROOF STEP]
unfolding to_polynomial_def
[PROOF STATE]
proof (prove)
using this:
p \<noteq> 2
a \<in> carrier Zp
b \<in> carrier Zp
val_Zp a \<le> val_Zp b
a \<noteq> \<zero>
b \<noteq> \<zero>
f = monom (UP Zp) \<one> 2 \<oplus>\<^bsub>UP Zp\<^esub> monom (UP Zp) (\<ominus> (a [^] 2 \<oplus> [p] \<cdot> \<one> \<otimes> b [^] 2)) 0
\<lbrakk>monom (UP Zp) \<one> 2 \<in> carrier (UP Zp); ?q \<in> carrier (UP Zp)\<rbrakk> \<Longrightarrow> pderiv (monom (UP Zp) \<one> 2 \<oplus>\<^bsub>UP Zp\<^esub> ?q) = pderiv (monom (UP Zp) \<one> 2) \<oplus>\<^bsub>UP Zp\<^esub> pderiv ?q
?a \<in> carrier Zp \<Longrightarrow> monom (UP Zp) ?a 0 \<in> carrier (UP Zp)
?x \<in> carrier Zp \<Longrightarrow> ?x [^] ?n \<in> carrier Zp
\<lbrakk>?f \<in> carrier (UP Zp); deg Zp ?f = 0\<rbrakk> \<Longrightarrow> pderiv ?f = \<zero>\<^bsub>UP Zp\<^esub>

goal (1 subgoal):
 1. pderiv f = pderiv (monom (UP Zp) \<one> 2)
[PROOF STEP]
using P.nat_pow_closed P.r_zero R.add.inv_closed X_closed Zp_int_inc_closed deg_const monom_term_car pderiv_closed sum_closed
[PROOF STATE]
proof (prove)
using this:
p \<noteq> 2
a \<in> carrier Zp
b \<in> carrier Zp
val_Zp a \<le> val_Zp b
a \<noteq> \<zero>
b \<noteq> \<zero>
f = monom (UP Zp) \<one> 2 \<oplus>\<^bsub>UP Zp\<^esub> monom (UP Zp) (\<ominus> (a [^] 2 \<oplus> [p] \<cdot> \<one> \<otimes> b [^] 2)) 0
\<lbrakk>monom (UP Zp) \<one> 2 \<in> carrier (UP Zp); ?q \<in> carrier (UP Zp)\<rbrakk> \<Longrightarrow> pderiv (monom (UP Zp) \<one> 2 \<oplus>\<^bsub>UP Zp\<^esub> ?q) = pderiv (monom (UP Zp) \<one> 2) \<oplus>\<^bsub>UP Zp\<^esub> pderiv ?q
?a \<in> carrier Zp \<Longrightarrow> monom (UP Zp) ?a 0 \<in> carrier (UP Zp)
?x \<in> carrier Zp \<Longrightarrow> ?x [^] ?n \<in> carrier Zp
\<lbrakk>?f \<in> carrier (UP Zp); deg Zp ?f = 0\<rbrakk> \<Longrightarrow> pderiv ?f = \<zero>\<^bsub>UP Zp\<^esub>
?x \<in> carrier (UP Zp) \<Longrightarrow> ?x [^]\<^bsub>UP Zp\<^esub> ?n \<in> carrier (UP Zp)
?x \<in> carrier (UP Zp) \<Longrightarrow> ?x \<oplus>\<^bsub>UP Zp\<^esub> \<zero>\<^bsub>UP Zp\<^esub> = ?x
?x \<in> carrier Zp \<Longrightarrow> \<ominus> ?x \<in> carrier Zp
X_poly Zp \<in> carrier (UP Zp)
[?n] \<cdot> \<one> \<in> carrier Zp
?a \<in> carrier Zp \<Longrightarrow> deg Zp (monom (UP Zp) ?a 0) = 0
\<lbrakk>?c \<in> carrier Zp; ?x \<in> carrier Zp\<rbrakk> \<Longrightarrow> ?c \<otimes> ?x [^] ?n \<in> carrier Zp
?p \<in> carrier (UP Zp) \<Longrightarrow> pderiv ?p \<in> carrier (UP Zp)
\<lbrakk>?f \<in> carrier Zp; ?g \<in> carrier Zp\<rbrakk> \<Longrightarrow> ?f \<oplus> ?g \<in> carrier Zp

goal (1 subgoal):
 1. pderiv f = pderiv (monom (UP Zp) \<one> 2)
[PROOF STEP]
by (metis (no_types, lifting) R.one_closed monom_closed)
[PROOF STATE]
proof (state)
this:
pderiv f = pderiv (monom (UP Zp) \<one> 2)

goal (1 subgoal):
 1. pderiv f \<bullet> a = [2] \<cdot> \<one> \<otimes> a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pderiv f = pderiv (monom (UP Zp) \<one> 2)
[PROOF STEP]
have 20: "pderiv f = monom (Zp_x) ([(2::nat) ] \<cdot> \<one>) (1::nat)"
[PROOF STATE]
proof (prove)
using this:
pderiv f = pderiv (monom (UP Zp) \<one> 2)

goal (1 subgoal):
 1. pderiv f = monom (UP Zp) ([2] \<cdot> \<one>) 1
[PROOF STEP]
using pderiv_monom[of \<one> 2]
[PROOF STATE]
proof (prove)
using this:
pderiv f = pderiv (monom (UP Zp) \<one> 2)
\<one> \<in> carrier Zp \<Longrightarrow> pderiv (monom (UP Zp) \<one> 2) = monom (UP Zp) ([2] \<cdot> \<one>) (2 - 1)

goal (1 subgoal):
 1. pderiv f = monom (UP Zp) ([2] \<cdot> \<one>) 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
pderiv f = monom (UP Zp) ([2] \<cdot> \<one>) 1

goal (1 subgoal):
 1. pderiv f \<bullet> a = [2] \<cdot> \<one> \<otimes> a
[PROOF STEP]
have 21: "[(2::nat)] \<cdot> \<one> \<noteq> \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [2] \<cdot> \<one> \<noteq> \<zero>
[PROOF STEP]
using Zp_char_0'[of 2]
[PROOF STATE]
proof (prove)
using this:
0 < 2 \<Longrightarrow> [2] \<cdot> \<one> \<noteq> \<zero>

goal (1 subgoal):
 1. [2] \<cdot> \<one> \<noteq> \<zero>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[2] \<cdot> \<one> \<noteq> \<zero>

goal (1 subgoal):
 1. pderiv f \<bullet> a = [2] \<cdot> \<one> \<otimes> a
[PROOF STEP]
have 22: "(pderiv f)\<bullet>a = [(2::nat)] \<cdot> \<one> \<otimes> (a[^]((1::nat)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pderiv f \<bullet> a = [2] \<cdot> \<one> \<otimes> a [^] 1
[PROOF STEP]
using 20
[PROOF STATE]
proof (prove)
using this:
pderiv f = monom (UP Zp) ([2] \<cdot> \<one>) 1

goal (1 subgoal):
 1. pderiv f \<bullet> a = [2] \<cdot> \<one> \<otimes> a [^] 1
[PROOF STEP]
by (simp add: Zp_nat_inc_closed assms(2) to_fun_monom)
[PROOF STATE]
proof (state)
this:
pderiv f \<bullet> a = [2] \<cdot> \<one> \<otimes> a [^] 1

goal (1 subgoal):
 1. pderiv f \<bullet> a = [2] \<cdot> \<one> \<otimes> a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pderiv f \<bullet> a = [2] \<cdot> \<one> \<otimes> a [^] 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
pderiv f \<bullet> a = [2] \<cdot> \<one> \<otimes> a [^] 1

goal (1 subgoal):
 1. pderiv f \<bullet> a = [2] \<cdot> \<one> \<otimes> a
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
pderiv f \<bullet> a = [2] \<cdot> \<one> \<otimes> a [^] 1
a \<in> carrier Zp

goal (1 subgoal):
 1. pderiv f \<bullet> a = [2] \<cdot> \<one> \<otimes> a
[PROOF STEP]
by (simp add: cring.cring_simprules(12))
[PROOF STATE]
proof (state)
this:
pderiv f \<bullet> a = [2] \<cdot> \<one> \<otimes> a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
pderiv f \<bullet> a = [2] \<cdot> \<one> \<otimes> a

goal (1 subgoal):
 1. \<exists>\<alpha>. f \<bullet> \<alpha> = \<zero> \<and> \<alpha> \<in> carrier Zp
[PROOF STEP]
have 2: "(pderiv f)\<bullet>a \<noteq> \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pderiv f \<bullet> a \<noteq> \<zero>
[PROOF STEP]
using 1 assms
[PROOF STATE]
proof (prove)
using this:
pderiv f \<bullet> a = [2] \<cdot> \<one> \<otimes> a
p \<noteq> 2
a \<in> carrier Zp
b \<in> carrier Zp
val_Zp a \<le> val_Zp b
a \<noteq> \<zero>
b \<noteq> \<zero>

goal (1 subgoal):
 1. pderiv f \<bullet> a \<noteq> \<zero>
[PROOF STEP]
by (metis Zp_char_0' Zp_nat_inc_closed local.integral zero_less_numeral)
[PROOF STATE]
proof (state)
this:
pderiv f \<bullet> a \<noteq> \<zero>

goal (1 subgoal):
 1. \<exists>\<alpha>. f \<bullet> \<alpha> = \<zero> \<and> \<alpha> \<in> carrier Zp
[PROOF STEP]
have 3: "f\<bullet>a = \<ominus> (\<p>\<otimes>b[^](2::nat))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<bullet> a = \<ominus> ([p] \<cdot> \<one> \<otimes> b [^] 2)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f \<bullet> a = \<ominus> ([p] \<cdot> \<one> \<otimes> b [^] 2)
[PROOF STEP]
have 3: "f\<bullet>a =
    monom (UP Zp) \<one> 2 \<bullet> a \<oplus>
    to_polynomial Zp (\<ominus> (a [^] (2::nat) \<oplus> [p] \<cdot> \<one> \<otimes> b [^] (2::nat)))\<bullet>a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<bullet> a = monom (UP Zp) \<one> 2 \<bullet> a \<oplus> to_polynomial Zp (\<ominus> (a [^] 2 \<oplus> [p] \<cdot> \<one> \<otimes> b [^] 2)) \<bullet> a
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (monom (UP Zp) \<one> 2 \<oplus>\<^bsub>UP Zp\<^esub> to_polynomial Zp (\<ominus> (a [^] 2 \<oplus> [p] \<cdot> \<one> \<otimes> b [^] 2))) \<bullet> a = monom (UP Zp) \<one> 2 \<bullet> a \<oplus> to_polynomial Zp (\<ominus> (a [^] 2 \<oplus> [p] \<cdot> \<one> \<otimes> b [^] 2)) \<bullet> a
[PROOF STEP]
apply(rule to_fun_plus)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. to_polynomial Zp (\<ominus> (a [^] 2 \<oplus> [p] \<cdot> \<one> \<otimes> b [^] 2)) \<in> carrier (UP Zp)
 2. monom (UP Zp) \<one> 2 \<in> carrier (UP Zp)
 3. a \<in> carrier Zp
[PROOF STEP]
apply (simp add: assms(2) assms(3) to_poly_closed)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. monom (UP Zp) \<one> 2 \<in> carrier (UP Zp)
 2. a \<in> carrier Zp
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> carrier Zp
[PROOF STEP]
by (simp add: assms(2))
[PROOF STATE]
proof (state)
this:
f \<bullet> a = monom (UP Zp) \<one> 2 \<bullet> a \<oplus> to_polynomial Zp (\<ominus> (a [^] 2 \<oplus> [p] \<cdot> \<one> \<otimes> b [^] 2)) \<bullet> a

goal (1 subgoal):
 1. f \<bullet> a = \<ominus> ([p] \<cdot> \<one> \<otimes> b [^] 2)
[PROOF STEP]
have 30: "f\<bullet>a = a[^](2::nat)  \<ominus> (a[^](2::nat) \<oplus> \<p>\<otimes>b[^](2::nat))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<bullet> a = a [^] 2 \<ominus> (a [^] 2 \<oplus> [p] \<cdot> \<one> \<otimes> b [^] 2)
[PROOF STEP]
unfolding 3
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monom (UP Zp) \<one> 2 \<bullet> a \<oplus> to_polynomial Zp (\<ominus> (a [^] 2 \<oplus> [p] \<cdot> \<one> \<otimes> b [^] 2)) \<bullet> a = a [^] 2 \<ominus> (a [^] 2 \<oplus> [p] \<cdot> \<one> \<otimes> b [^] 2)
[PROOF STEP]
by (simp add: R.minus_eq assms(2) assms(3) to_fun_monic_monom to_fun_to_poly)
[PROOF STATE]
proof (state)
this:
f \<bullet> a = a [^] 2 \<ominus> (a [^] 2 \<oplus> [p] \<cdot> \<one> \<otimes> b [^] 2)

goal (1 subgoal):
 1. f \<bullet> a = \<ominus> ([p] \<cdot> \<one> \<otimes> b [^] 2)
[PROOF STEP]
have 31: "f\<bullet>a = a[^](2::nat)  \<ominus> a[^](2::nat) \<ominus> (\<p>\<otimes>b[^](2::nat))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<bullet> a = a [^] 2 \<ominus> a [^] 2 \<ominus> [p] \<cdot> \<one> \<otimes> b [^] 2
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f \<bullet> a = a [^] 2 \<ominus> a [^] 2 \<ominus> [p] \<cdot> \<one> \<otimes> b [^] 2
[PROOF STEP]
have 310: "a[^](2::nat) \<in> carrier Zp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a [^] 2 \<in> carrier Zp
[PROOF STEP]
using assms(2) pow_closed
[PROOF STATE]
proof (prove)
using this:
a \<in> carrier Zp
?a \<in> carrier Zp \<Longrightarrow> ?a [^] ?n \<in> carrier Zp

goal (1 subgoal):
 1. a [^] 2 \<in> carrier Zp
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a [^] 2 \<in> carrier Zp

goal (1 subgoal):
 1. f \<bullet> a = a [^] 2 \<ominus> a [^] 2 \<ominus> [p] \<cdot> \<one> \<otimes> b [^] 2
[PROOF STEP]
have 311: "\<p>\<otimes>(b[^](2::nat)) \<in> carrier Zp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [p] \<cdot> \<one> \<otimes> b [^] 2 \<in> carrier Zp
[PROOF STEP]
by (simp add: assms(3) monom_term_car)
[PROOF STATE]
proof (state)
this:
[p] \<cdot> \<one> \<otimes> b [^] 2 \<in> carrier Zp

goal (1 subgoal):
 1. f \<bullet> a = a [^] 2 \<ominus> a [^] 2 \<ominus> [p] \<cdot> \<one> \<otimes> b [^] 2
[PROOF STEP]
have   "\<ominus> (a [^] (2::nat)\<oplus>(\<p> \<otimes> b [^] (2::nat))) = \<ominus> (a [^] (2::nat)) \<oplus> \<ominus> (\<p> \<otimes> (b [^] (2::nat)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<ominus> (a [^] 2 \<oplus> [p] \<cdot> \<one> \<otimes> b [^] 2) = \<ominus> (a [^] 2) \<oplus> \<ominus> ([p] \<cdot> \<one> \<otimes> b [^] 2)
[PROOF STEP]
using 310 311 R.minus_add
[PROOF STATE]
proof (prove)
using this:
a [^] 2 \<in> carrier Zp
[p] \<cdot> \<one> \<otimes> b [^] 2 \<in> carrier Zp
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp\<rbrakk> \<Longrightarrow> \<ominus> (?x \<oplus> ?y) = \<ominus> ?x \<oplus> \<ominus> ?y

goal (1 subgoal):
 1. \<ominus> (a [^] 2 \<oplus> [p] \<cdot> \<one> \<otimes> b [^] 2) = \<ominus> (a [^] 2) \<oplus> \<ominus> ([p] \<cdot> \<one> \<otimes> b [^] 2)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<ominus> (a [^] 2 \<oplus> [p] \<cdot> \<one> \<otimes> b [^] 2) = \<ominus> (a [^] 2) \<oplus> \<ominus> ([p] \<cdot> \<one> \<otimes> b [^] 2)

goal (1 subgoal):
 1. f \<bullet> a = a [^] 2 \<ominus> a [^] 2 \<ominus> [p] \<cdot> \<one> \<otimes> b [^] 2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<ominus> (a [^] 2 \<oplus> [p] \<cdot> \<one> \<otimes> b [^] 2) = \<ominus> (a [^] 2) \<oplus> \<ominus> ([p] \<cdot> \<one> \<otimes> b [^] 2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<ominus> (a [^] 2 \<oplus> [p] \<cdot> \<one> \<otimes> b [^] 2) = \<ominus> (a [^] 2) \<oplus> \<ominus> ([p] \<cdot> \<one> \<otimes> b [^] 2)

goal (1 subgoal):
 1. f \<bullet> a = a [^] 2 \<ominus> a [^] 2 \<ominus> [p] \<cdot> \<one> \<otimes> b [^] 2
[PROOF STEP]
by (simp add: "30" R.minus_eq add_assoc)
[PROOF STATE]
proof (state)
this:
f \<bullet> a = a [^] 2 \<ominus> a [^] 2 \<ominus> [p] \<cdot> \<one> \<otimes> b [^] 2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f \<bullet> a = a [^] 2 \<ominus> a [^] 2 \<ominus> [p] \<cdot> \<one> \<otimes> b [^] 2

goal (1 subgoal):
 1. f \<bullet> a = \<ominus> ([p] \<cdot> \<one> \<otimes> b [^] 2)
[PROOF STEP]
have 32: "f\<bullet>a = (a[^](2::nat)  \<ominus> a[^](2::nat)) \<ominus> (\<p>\<otimes>b[^](2::nat))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<bullet> a = a [^] 2 \<ominus> a [^] 2 \<ominus> [p] \<cdot> \<one> \<otimes> b [^] 2
[PROOF STEP]
using 31
[PROOF STATE]
proof (prove)
using this:
f \<bullet> a = a [^] 2 \<ominus> a [^] 2 \<ominus> [p] \<cdot> \<one> \<otimes> b [^] 2

goal (1 subgoal):
 1. f \<bullet> a = a [^] 2 \<ominus> a [^] 2 \<ominus> [p] \<cdot> \<one> \<otimes> b [^] 2
[PROOF STEP]
unfolding a_minus_def
[PROOF STATE]
proof (prove)
using this:
f \<bullet> a = a [^] 2 \<oplus> \<ominus> (a [^] 2) \<oplus> \<ominus> ([p] \<cdot> \<one> \<otimes> b [^] 2)

goal (1 subgoal):
 1. f \<bullet> a = a [^] 2 \<oplus> \<ominus> (a [^] 2) \<oplus> \<ominus> ([p] \<cdot> \<one> \<otimes> b [^] 2)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f \<bullet> a = a [^] 2 \<ominus> a [^] 2 \<ominus> [p] \<cdot> \<one> \<otimes> b [^] 2

goal (1 subgoal):
 1. f \<bullet> a = \<ominus> ([p] \<cdot> \<one> \<otimes> b [^] 2)
[PROOF STEP]
have 33: "\<p>\<otimes>b[^](2::nat) \<in> carrier Zp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [p] \<cdot> \<one> \<otimes> b [^] 2 \<in> carrier Zp
[PROOF STEP]
by (simp add: Zp_nat_inc_closed assms(3) monom_term_car)
[PROOF STATE]
proof (state)
this:
[p] \<cdot> \<one> \<otimes> b [^] 2 \<in> carrier Zp

goal (1 subgoal):
 1. f \<bullet> a = \<ominus> ([p] \<cdot> \<one> \<otimes> b [^] 2)
[PROOF STEP]
have 34: "a[^](2::nat) \<in> carrier Zp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a [^] 2 \<in> carrier Zp
[PROOF STEP]
using assms(2) pow_closed
[PROOF STATE]
proof (prove)
using this:
a \<in> carrier Zp
?a \<in> carrier Zp \<Longrightarrow> ?a [^] ?n \<in> carrier Zp

goal (1 subgoal):
 1. a [^] 2 \<in> carrier Zp
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a [^] 2 \<in> carrier Zp

goal (1 subgoal):
 1. f \<bullet> a = \<ominus> ([p] \<cdot> \<one> \<otimes> b [^] 2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a [^] 2 \<in> carrier Zp
[PROOF STEP]
have 34: "(a[^](2::nat)  \<ominus> a[^](2::nat)) = \<zero> "
[PROOF STATE]
proof (prove)
using this:
a [^] 2 \<in> carrier Zp

goal (1 subgoal):
 1. a [^] 2 \<ominus> a [^] 2 = \<zero>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a [^] 2 \<ominus> a [^] 2 = \<zero>

goal (1 subgoal):
 1. f \<bullet> a = \<ominus> ([p] \<cdot> \<one> \<otimes> b [^] 2)
[PROOF STEP]
have 35: "f\<bullet>a = \<zero> \<ominus> (\<p>\<otimes>b[^](2::nat))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<bullet> a = \<zero> \<ominus> [p] \<cdot> \<one> \<otimes> b [^] 2
[PROOF STEP]
by (simp add: "32" "34")
[PROOF STATE]
proof (state)
this:
f \<bullet> a = \<zero> \<ominus> [p] \<cdot> \<one> \<otimes> b [^] 2

goal (1 subgoal):
 1. f \<bullet> a = \<ominus> ([p] \<cdot> \<one> \<otimes> b [^] 2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f \<bullet> a = \<zero> \<ominus> [p] \<cdot> \<one> \<otimes> b [^] 2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f \<bullet> a = \<zero> \<ominus> [p] \<cdot> \<one> \<otimes> b [^] 2

goal (1 subgoal):
 1. f \<bullet> a = \<ominus> ([p] \<cdot> \<one> \<otimes> b [^] 2)
[PROOF STEP]
using 33
[PROOF STATE]
proof (prove)
using this:
f \<bullet> a = \<zero> \<ominus> [p] \<cdot> \<one> \<otimes> b [^] 2
[p] \<cdot> \<one> \<otimes> b [^] 2 \<in> carrier Zp

goal (1 subgoal):
 1. f \<bullet> a = \<ominus> ([p] \<cdot> \<one> \<otimes> b [^] 2)
[PROOF STEP]
unfolding a_minus_def
[PROOF STATE]
proof (prove)
using this:
f \<bullet> a = \<zero> \<oplus> \<ominus> ([p] \<cdot> \<one> \<otimes> b [^] 2)
[p] \<cdot> \<one> \<otimes> b [^] 2 \<in> carrier Zp

goal (1 subgoal):
 1. f \<bullet> a = \<ominus> ([p] \<cdot> \<one> \<otimes> b [^] 2)
[PROOF STEP]
by (simp add: cring.cring_simprules(3))
[PROOF STATE]
proof (state)
this:
f \<bullet> a = \<ominus> ([p] \<cdot> \<one> \<otimes> b [^] 2)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f \<bullet> a = \<ominus> ([p] \<cdot> \<one> \<otimes> b [^] 2)

goal (1 subgoal):
 1. \<exists>\<alpha>. f \<bullet> \<alpha> = \<zero> \<and> \<alpha> \<in> carrier Zp
[PROOF STEP]
have 4: "f\<bullet>a \<noteq>\<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<bullet> a \<noteq> \<zero>
[PROOF STEP]
using 3 assms
[PROOF STATE]
proof (prove)
using this:
f \<bullet> a = \<ominus> ([p] \<cdot> \<one> \<otimes> b [^] 2)
p \<noteq> 2
a \<in> carrier Zp
b \<in> carrier Zp
val_Zp a \<le> val_Zp b
a \<noteq> \<zero>
b \<noteq> \<zero>

goal (1 subgoal):
 1. f \<bullet> a \<noteq> \<zero>
[PROOF STEP]
by (metis R.add.inv_eq_1_iff R.m_closed R.nat_pow_closed Zp.integral Zp_int_inc_closed
          mult_zero_r nonzero_pow_nonzero p_natpow_prod_Suc(1) p_pow_nonzero(2))
[PROOF STATE]
proof (state)
this:
f \<bullet> a \<noteq> \<zero>

goal (1 subgoal):
 1. \<exists>\<alpha>. f \<bullet> \<alpha> = \<zero> \<and> \<alpha> \<in> carrier Zp
[PROOF STEP]
have 5: "val_Zp (f\<bullet>a) = 1 + 2*val_Zp b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (f \<bullet> a) = 1 + eint 2 * val_Zp b
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. val_Zp (f \<bullet> a) = 1 + eint 2 * val_Zp b
[PROOF STEP]
have "val_Zp (f\<bullet>a) = val_Zp (\<p>\<otimes>b[^](2::nat))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (f \<bullet> a) = val_Zp ([p] \<cdot> \<one> \<otimes> b [^] 2)
[PROOF STEP]
using 3 Zp_int_inc_closed assms(3) monom_term_car val_Zp_of_minus
[PROOF STATE]
proof (prove)
using this:
f \<bullet> a = \<ominus> ([p] \<cdot> \<one> \<otimes> b [^] 2)
[?n] \<cdot> \<one> \<in> carrier Zp
b \<in> carrier Zp
\<lbrakk>?c \<in> carrier Zp; ?x \<in> carrier Zp\<rbrakk> \<Longrightarrow> ?c \<otimes> ?x [^] ?n \<in> carrier Zp
?a \<in> carrier Zp \<Longrightarrow> val_Zp ?a = val_Zp (\<ominus> ?a)

goal (1 subgoal):
 1. val_Zp (f \<bullet> a) = val_Zp ([p] \<cdot> \<one> \<otimes> b [^] 2)
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
val_Zp (f \<bullet> a) = val_Zp ([p] \<cdot> \<one> \<otimes> b [^] 2)

goal (1 subgoal):
 1. val_Zp (f \<bullet> a) = 1 + eint 2 * val_Zp b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
val_Zp (f \<bullet> a) = val_Zp ([p] \<cdot> \<one> \<otimes> b [^] 2)
[PROOF STEP]
have "val_Zp (\<p>\<otimes>b[^](2::nat)) = 1 + val_Zp (b[^](2::nat))"
[PROOF STATE]
proof (prove)
using this:
val_Zp (f \<bullet> a) = val_Zp ([p] \<cdot> \<one> \<otimes> b [^] 2)

goal (1 subgoal):
 1. val_Zp ([p] \<cdot> \<one> \<otimes> b [^] 2) = 1 + val_Zp (b [^] 2)
[PROOF STEP]
by (simp add: assms(3) val_Zp_mult val_Zp_p)
[PROOF STATE]
proof (state)
this:
val_Zp ([p] \<cdot> \<one> \<otimes> b [^] 2) = 1 + val_Zp (b [^] 2)

goal (1 subgoal):
 1. val_Zp (f \<bullet> a) = 1 + eint 2 * val_Zp b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
val_Zp ([p] \<cdot> \<one> \<otimes> b [^] 2) = 1 + val_Zp (b [^] 2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
val_Zp ([p] \<cdot> \<one> \<otimes> b [^] 2) = 1 + val_Zp (b [^] 2)

goal (1 subgoal):
 1. val_Zp (f \<bullet> a) = 1 + eint 2 * val_Zp b
[PROOF STEP]
using assms(3) assms(6)
[PROOF STATE]
proof (prove)
using this:
val_Zp ([p] \<cdot> \<one> \<otimes> b [^] 2) = 1 + val_Zp (b [^] 2)
b \<in> carrier Zp
b \<noteq> \<zero>

goal (1 subgoal):
 1. val_Zp (f \<bullet> a) = 1 + eint 2 * val_Zp b
[PROOF STEP]
using Zp_def \<open>val_Zp (to_fun f a) = val_Zp ([p] \<cdot> \<one> \<otimes> b [^] 2)\<close> not_nonzero_Zp
          padic_integers_axioms val_Zp_pow'
[PROOF STATE]
proof (prove)
using this:
val_Zp ([p] \<cdot> \<one> \<otimes> b [^] 2) = 1 + val_Zp (b [^] 2)
b \<in> carrier Zp
b \<noteq> \<zero>
Zp \<equiv> padic_int p
val_Zp (f \<bullet> a) = val_Zp ([p] \<cdot> \<one> \<otimes> b [^] 2)
\<lbrakk>?x \<in> carrier Zp; ?x \<notin> nonzero Zp\<rbrakk> \<Longrightarrow> ?x = \<zero>
padic_integers p
?x \<in> nonzero Zp \<Longrightarrow> val_Zp (?x [^] ?n) = eint (int ?n) * val_Zp ?x

goal (1 subgoal):
 1. val_Zp (f \<bullet> a) = 1 + eint 2 * val_Zp b
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
val_Zp (f \<bullet> a) = 1 + eint 2 * val_Zp b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
val_Zp (f \<bullet> a) = 1 + eint 2 * val_Zp b

goal (1 subgoal):
 1. \<exists>\<alpha>. f \<bullet> \<alpha> = \<zero> \<and> \<alpha> \<in> carrier Zp
[PROOF STEP]
have 6: "val_Zp ((pderiv f)\<bullet>a) = val_Zp a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (pderiv f \<bullet> a) = val_Zp a
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. val_Zp (pderiv f \<bullet> a) = val_Zp a
[PROOF STEP]
have 60: "val_Zp ([(2::nat)] \<cdot> \<one> \<otimes> a) = val_Zp ([(2::nat)] \<cdot> \<one>) + val_Zp a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp ([2] \<cdot> \<one> \<otimes> a) = val_Zp ([2] \<cdot> \<one>) + val_Zp a
[PROOF STEP]
by (simp add: Zp_char_0' assms(2) assms(5) val_Zp_mult ord_of_nonzero(2) ord_pos)
[PROOF STATE]
proof (state)
this:
val_Zp ([2] \<cdot> \<one> \<otimes> a) = val_Zp ([2] \<cdot> \<one>) + val_Zp a

goal (1 subgoal):
 1. val_Zp (pderiv f \<bullet> a) = val_Zp a
[PROOF STEP]
have "val_Zp ([(2::nat)] \<cdot> \<one>) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp ([2] \<cdot> \<one>) = 0
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. val_Zp ([2] \<cdot> \<one>) = 0
[PROOF STEP]
have "(2::nat) < p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int 2 < p
[PROOF STEP]
using prime assms prime_ge_2_int
[PROOF STATE]
proof (prove)
using this:
prime p
p \<noteq> 2
a \<in> carrier Zp
b \<in> carrier Zp
val_Zp a \<le> val_Zp b
a \<noteq> \<zero>
b \<noteq> \<zero>
prime ?p \<Longrightarrow> 2 \<le> ?p

goal (1 subgoal):
 1. int 2 < p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
int 2 < p

goal (1 subgoal):
 1. val_Zp ([2] \<cdot> \<one>) = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
int 2 < p
[PROOF STEP]
have "(2::nat) mod p = (2::nat)"
[PROOF STATE]
proof (prove)
using this:
int 2 < p

goal (1 subgoal):
 1. int 2 mod p = int 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
int 2 mod p = int 2

goal (1 subgoal):
 1. val_Zp ([2] \<cdot> \<one>) = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
int 2 mod p = int 2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
int 2 mod p = int 2

goal (1 subgoal):
 1. val_Zp ([2] \<cdot> \<one>) = 0
[PROOF STEP]
by (simp add: val_Zp_p_nat_unit)
[PROOF STATE]
proof (state)
this:
val_Zp ([2] \<cdot> \<one>) = 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
val_Zp ([2] \<cdot> \<one>) = 0

goal (1 subgoal):
 1. val_Zp (pderiv f \<bullet> a) = val_Zp a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
val_Zp ([2] \<cdot> \<one>) = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
val_Zp ([2] \<cdot> \<one>) = 0

goal (1 subgoal):
 1. val_Zp (pderiv f \<bullet> a) = val_Zp a
[PROOF STEP]
by (simp add: "1" "60")
[PROOF STATE]
proof (state)
this:
val_Zp (pderiv f \<bullet> a) = val_Zp a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
val_Zp (pderiv f \<bullet> a) = val_Zp a

goal (1 subgoal):
 1. \<exists>\<alpha>. f \<bullet> \<alpha> = \<zero> \<and> \<alpha> \<in> carrier Zp
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
val_Zp (pderiv f \<bullet> a) = val_Zp a
[PROOF STEP]
have 7: "val_Zp (f\<bullet>a) > 2* val_Zp ((pderiv f)\<bullet>a)"
[PROOF STATE]
proof (prove)
using this:
val_Zp (pderiv f \<bullet> a) = val_Zp a

goal (1 subgoal):
 1. eint 2 * val_Zp (pderiv f \<bullet> a) < val_Zp (f \<bullet> a)
[PROOF STEP]
using bounds 5 assms(4)
[PROOF STATE]
proof (prove)
using this:
val_Zp (pderiv f \<bullet> a) = val_Zp a
val_Zp a < \<infinity>
0 \<le> val_Zp a
val_Zp b < \<infinity>
0 \<le> val_Zp b
val_Zp (f \<bullet> a) = 1 + eint 2 * val_Zp b
val_Zp a \<le> val_Zp b

goal (1 subgoal):
 1. eint 2 * val_Zp (pderiv f \<bullet> a) < val_Zp (f \<bullet> a)
[PROOF STEP]
by (simp add: assms(5) assms(6) one_eint_def val_Zp_def)
[PROOF STATE]
proof (state)
this:
eint 2 * val_Zp (pderiv f \<bullet> a) < val_Zp (f \<bullet> a)

goal (1 subgoal):
 1. \<exists>\<alpha>. f \<bullet> \<alpha> = \<zero> \<and> \<alpha> \<in> carrier Zp
[PROOF STEP]
obtain \<alpha> where
       A0: "f\<bullet>\<alpha> = \<zero>"  "\<alpha> \<in> carrier Zp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<alpha>. \<lbrakk>f \<bullet> \<alpha> = \<zero>; \<alpha> \<in> carrier Zp\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using hensels_lemma[of f a] "0" "2" "4" "7" assms(2)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>f \<in> carrier (UP Zp); a \<in> carrier Zp; pderiv f \<bullet> a \<noteq> \<zero>; f \<bullet> a \<noteq> \<zero>; eint 2 * val_Zp (pderiv f \<bullet> a) < val_Zp (f \<bullet> a); \<And>\<alpha>. \<lbrakk>f \<bullet> \<alpha> = \<zero>; \<alpha> \<in> carrier Zp; val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> \<alpha>); val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (pderiv f \<bullet> a)); val_Zp (pderiv f \<bullet> \<alpha>) = val_Zp (pderiv f \<bullet> a)\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
f \<in> carrier (UP Zp)
pderiv f \<bullet> a \<noteq> \<zero>
f \<bullet> a \<noteq> \<zero>
eint 2 * val_Zp (pderiv f \<bullet> a) < val_Zp (f \<bullet> a)
a \<in> carrier Zp

goal (1 subgoal):
 1. (\<And>\<alpha>. \<lbrakk>f \<bullet> \<alpha> = \<zero>; \<alpha> \<in> carrier Zp\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f \<bullet> \<alpha> = \<zero>
\<alpha> \<in> carrier Zp

goal (1 subgoal):
 1. \<exists>\<alpha>. f \<bullet> \<alpha> = \<zero> \<and> \<alpha> \<in> carrier Zp
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<alpha>. f \<bullet> \<alpha> = \<zero> \<and> \<alpha> \<in> carrier Zp
[PROOF STEP]
using A0
[PROOF STATE]
proof (prove)
using this:
f \<bullet> \<alpha> = \<zero>
\<alpha> \<in> carrier Zp

goal (1 subgoal):
 1. \<exists>\<alpha>. f \<bullet> \<alpha> = \<zero> \<and> \<alpha> \<in> carrier Zp
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>\<alpha>. f \<bullet> \<alpha> = \<zero> \<and> \<alpha> \<in> carrier Zp

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>\<alpha>. f \<bullet> \<alpha> = \<zero> \<and> \<alpha> \<in> carrier Zp

goal (1 subgoal):
 1. \<exists>y\<in>carrier Zp. a [^] 2 \<oplus> [p] \<cdot> \<one> \<otimes> b [^] 2 = y [^] 2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>\<alpha>. f \<bullet> \<alpha> = \<zero> \<and> \<alpha> \<in> carrier Zp
[PROOF STEP]
obtain \<alpha> where \<alpha>_def: "f\<bullet>\<alpha> = \<zero> \<and> \<alpha> \<in> carrier Zp"
[PROOF STATE]
proof (prove)
using this:
\<exists>\<alpha>. f \<bullet> \<alpha> = \<zero> \<and> \<alpha> \<in> carrier Zp

goal (1 subgoal):
 1. (\<And>\<alpha>. f \<bullet> \<alpha> = \<zero> \<and> \<alpha> \<in> carrier Zp \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f \<bullet> \<alpha> = \<zero> \<and> \<alpha> \<in> carrier Zp

goal (1 subgoal):
 1. \<exists>y\<in>carrier Zp. a [^] 2 \<oplus> [p] \<cdot> \<one> \<otimes> b [^] 2 = y [^] 2
[PROOF STEP]
have "f\<bullet>\<alpha> = \<alpha> [^](2::nat)  \<ominus> (a[^](2::nat)\<oplus> \<p>\<otimes>b[^](2::nat))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<bullet> \<alpha> = \<alpha> [^] 2 \<ominus> (a [^] 2 \<oplus> [p] \<cdot> \<one> \<otimes> b [^] 2)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f \<bullet> \<alpha> = \<alpha> [^] 2 \<ominus> (a [^] 2 \<oplus> [p] \<cdot> \<one> \<otimes> b [^] 2)
[PROOF STEP]
have 0: "f\<bullet>\<alpha> =
    monom (UP Zp) \<one> 2 \<bullet> \<alpha> \<oplus>
    to_polynomial Zp (\<ominus> (a [^] (2::nat) \<oplus> [p] \<cdot> \<one> \<otimes> b [^] (2::nat)))\<bullet>\<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<bullet> \<alpha> = monom (UP Zp) \<one> 2 \<bullet> \<alpha> \<oplus> to_polynomial Zp (\<ominus> (a [^] 2 \<oplus> [p] \<cdot> \<one> \<otimes> b [^] 2)) \<bullet> \<alpha>
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (monom (UP Zp) \<one> 2 \<oplus>\<^bsub>UP Zp\<^esub> to_polynomial Zp (\<ominus> (a [^] 2 \<oplus> [p] \<cdot> \<one> \<otimes> b [^] 2))) \<bullet> \<alpha> = monom (UP Zp) \<one> 2 \<bullet> \<alpha> \<oplus> to_polynomial Zp (\<ominus> (a [^] 2 \<oplus> [p] \<cdot> \<one> \<otimes> b [^] 2)) \<bullet> \<alpha>
[PROOF STEP]
apply(rule to_fun_plus)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. to_polynomial Zp (\<ominus> (a [^] 2 \<oplus> [p] \<cdot> \<one> \<otimes> b [^] 2)) \<in> carrier (UP Zp)
 2. monom (UP Zp) \<one> 2 \<in> carrier (UP Zp)
 3. \<alpha> \<in> carrier Zp
[PROOF STEP]
apply (simp add: assms(2) assms(3) to_poly_closed)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. monom (UP Zp) \<one> 2 \<in> carrier (UP Zp)
 2. \<alpha> \<in> carrier Zp
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> \<in> carrier Zp
[PROOF STEP]
by (simp add: \<alpha>_def)
[PROOF STATE]
proof (state)
this:
f \<bullet> \<alpha> = monom (UP Zp) \<one> 2 \<bullet> \<alpha> \<oplus> to_polynomial Zp (\<ominus> (a [^] 2 \<oplus> [p] \<cdot> \<one> \<otimes> b [^] 2)) \<bullet> \<alpha>

goal (1 subgoal):
 1. f \<bullet> \<alpha> = \<alpha> [^] 2 \<ominus> (a [^] 2 \<oplus> [p] \<cdot> \<one> \<otimes> b [^] 2)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
f \<bullet> \<alpha> = monom (UP Zp) \<one> 2 \<bullet> \<alpha> \<oplus> to_polynomial Zp (\<ominus> (a [^] 2 \<oplus> [p] \<cdot> \<one> \<otimes> b [^] 2)) \<bullet> \<alpha>

goal (1 subgoal):
 1. f \<bullet> \<alpha> = \<alpha> [^] 2 \<ominus> (a [^] 2 \<oplus> [p] \<cdot> \<one> \<otimes> b [^] 2)
[PROOF STEP]
by (simp add: R.minus_eq \<alpha>_def assms(2) assms(3) to_fun_monic_monom to_fun_to_poly)
[PROOF STATE]
proof (state)
this:
f \<bullet> \<alpha> = \<alpha> [^] 2 \<ominus> (a [^] 2 \<oplus> [p] \<cdot> \<one> \<otimes> b [^] 2)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f \<bullet> \<alpha> = \<alpha> [^] 2 \<ominus> (a [^] 2 \<oplus> [p] \<cdot> \<one> \<otimes> b [^] 2)

goal (1 subgoal):
 1. \<exists>y\<in>carrier Zp. a [^] 2 \<oplus> [p] \<cdot> \<one> \<otimes> b [^] 2 = y [^] 2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f \<bullet> \<alpha> = \<alpha> [^] 2 \<ominus> (a [^] 2 \<oplus> [p] \<cdot> \<one> \<otimes> b [^] 2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f \<bullet> \<alpha> = \<alpha> [^] 2 \<ominus> (a [^] 2 \<oplus> [p] \<cdot> \<one> \<otimes> b [^] 2)

goal (1 subgoal):
 1. \<exists>y\<in>carrier Zp. a [^] 2 \<oplus> [p] \<cdot> \<one> \<otimes> b [^] 2 = y [^] 2
[PROOF STEP]
by (metis R.r_right_minus_eq Zp_int_inc_closed \<alpha>_def assms(2) assms(3) monom_term_car pow_closed sum_closed)
[PROOF STATE]
proof (state)
this:
\<exists>y\<in>carrier Zp. a [^] 2 \<oplus> [p] \<cdot> \<one> \<otimes> b [^] 2 = y [^] 2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Zp_semialg_eq:
  assumes "a \<in> nonzero Zp"
  shows "\<exists>y \<in> carrier Zp. \<one> \<oplus> (\<p> [^] (3::nat))\<otimes> (a [^] (4::nat)) = (y [^] (2::nat))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>y\<in>carrier Zp. \<one> \<oplus> [p] \<cdot> \<one> [^] 3 \<otimes> a [^] 4 = y [^] 2
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>y\<in>carrier Zp. \<one> \<oplus> [p] \<cdot> \<one> [^] 3 \<otimes> a [^] 4 = y [^] 2
[PROOF STEP]
obtain f where f_def: "f = monom Zp_x \<one> 2 \<oplus>\<^bsub>Zp_x\<^esub> to_poly (\<ominus> (\<one> \<oplus> (\<p> [^] (3::nat))\<otimes> (a [^] (4::nat))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f. f = monom (UP Zp) \<one> 2 \<oplus>\<^bsub>UP Zp\<^esub> to_polynomial Zp (\<ominus> (\<one> \<oplus> [p] \<cdot> \<one> [^] 3 \<otimes> a [^] 4)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f = monom (UP Zp) \<one> 2 \<oplus>\<^bsub>UP Zp\<^esub> to_polynomial Zp (\<ominus> (\<one> \<oplus> [p] \<cdot> \<one> [^] 3 \<otimes> a [^] 4))

goal (1 subgoal):
 1. \<exists>y\<in>carrier Zp. \<one> \<oplus> [p] \<cdot> \<one> [^] 3 \<otimes> a [^] 4 = y [^] 2
[PROOF STEP]
have a_car: "a \<in> carrier Zp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> carrier Zp
[PROOF STEP]
by (simp add: nonzero_memE assms)
[PROOF STATE]
proof (state)
this:
a \<in> carrier Zp

goal (1 subgoal):
 1. \<exists>y\<in>carrier Zp. \<one> \<oplus> [p] \<cdot> \<one> [^] 3 \<otimes> a [^] 4 = y [^] 2
[PROOF STEP]
have "f \<in> carrier Zp_x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> carrier (UP Zp)
[PROOF STEP]
using f_def
[PROOF STATE]
proof (prove)
using this:
f = monom (UP Zp) \<one> 2 \<oplus>\<^bsub>UP Zp\<^esub> to_polynomial Zp (\<ominus> (\<one> \<oplus> [p] \<cdot> \<one> [^] 3 \<otimes> a [^] 4))

goal (1 subgoal):
 1. f \<in> carrier (UP Zp)
[PROOF STEP]
by (simp add: a_car to_poly_closed)
[PROOF STATE]
proof (state)
this:
f \<in> carrier (UP Zp)

goal (1 subgoal):
 1. \<exists>y\<in>carrier Zp. \<one> \<oplus> [p] \<cdot> \<one> [^] 3 \<otimes> a [^] 4 = y [^] 2
[PROOF STEP]
hence 0:"f\<bullet>\<one> = \<one> \<ominus> (\<one> \<oplus> (\<p> [^] (3::nat))\<otimes> (a [^] (4::nat)))"
[PROOF STATE]
proof (prove)
using this:
f \<in> carrier (UP Zp)

goal (1 subgoal):
 1. f \<bullet> \<one> = \<one> \<ominus> (\<one> \<oplus> [p] \<cdot> \<one> [^] 3 \<otimes> a [^] 4)
[PROOF STEP]
using f_def
[PROOF STATE]
proof (prove)
using this:
f \<in> carrier (UP Zp)
f = monom (UP Zp) \<one> 2 \<oplus>\<^bsub>UP Zp\<^esub> to_polynomial Zp (\<ominus> (\<one> \<oplus> [p] \<cdot> \<one> [^] 3 \<otimes> a [^] 4))

goal (1 subgoal):
 1. f \<bullet> \<one> = \<one> \<ominus> (\<one> \<oplus> [p] \<cdot> \<one> [^] 3 \<otimes> a [^] 4)
[PROOF STEP]
by (simp add: R.minus_eq assms nat_pow_nonzero nonzero_mult_in_car p_pow_nonzero' to_fun_monom_plus to_fun_to_poly to_poly_closed)
[PROOF STATE]
proof (state)
this:
f \<bullet> \<one> = \<one> \<ominus> (\<one> \<oplus> [p] \<cdot> \<one> [^] 3 \<otimes> a [^] 4)

goal (1 subgoal):
 1. \<exists>y\<in>carrier Zp. \<one> \<oplus> [p] \<cdot> \<one> [^] 3 \<otimes> a [^] 4 = y [^] 2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f \<bullet> \<one> = \<one> \<ominus> (\<one> \<oplus> [p] \<cdot> \<one> [^] 3 \<otimes> a [^] 4)
[PROOF STEP]
have 1: "f\<bullet>\<one> = \<ominus> (\<p> [^] (3::nat))\<otimes> (a [^] (4::nat))"
[PROOF STATE]
proof (prove)
using this:
f \<bullet> \<one> = \<one> \<ominus> (\<one> \<oplus> [p] \<cdot> \<one> [^] 3 \<otimes> a [^] 4)

goal (1 subgoal):
 1. f \<bullet> \<one> = \<ominus> ([p] \<cdot> \<one> [^] 3) \<otimes> a [^] 4
[PROOF STEP]
unfolding a_minus_def
[PROOF STATE]
proof (prove)
using this:
f \<bullet> \<one> = \<one> \<oplus> \<ominus> (\<one> \<oplus> [p] \<cdot> \<one> [^] 3 \<otimes> a [^] 4)

goal (1 subgoal):
 1. f \<bullet> \<one> = \<ominus> ([p] \<cdot> \<one> [^] 3) \<otimes> a [^] 4
[PROOF STEP]
by (smt R.add.inv_closed R.l_minus R.minus_add R.minus_minus R.nat_pow_closed R.one_closed R.r_neg1 a_car monom_term_car p_pow_nonzero(1))
[PROOF STATE]
proof (state)
this:
f \<bullet> \<one> = \<ominus> ([p] \<cdot> \<one> [^] 3) \<otimes> a [^] 4

goal (1 subgoal):
 1. \<exists>y\<in>carrier Zp. \<one> \<oplus> [p] \<cdot> \<one> [^] 3 \<otimes> a [^] 4 = y [^] 2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f \<bullet> \<one> = \<ominus> ([p] \<cdot> \<one> [^] 3) \<otimes> a [^] 4
[PROOF STEP]
have "val_Zp (f\<bullet>\<one>) = 3 + val_Zp (a [^] (4::nat))"
[PROOF STATE]
proof (prove)
using this:
f \<bullet> \<one> = \<ominus> ([p] \<cdot> \<one> [^] 3) \<otimes> a [^] 4

goal (1 subgoal):
 1. val_Zp (f \<bullet> \<one>) = eint 3 + val_Zp (a [^] 4)
[PROOF STEP]
using  assms val_Zp_mult[of "\<p> [^] (3::nat)" "(a [^] (4::nat))" ]
      val_Zp_p_pow p_pow_nonzero[of "3::nat"] val_Zp_of_minus
[PROOF STATE]
proof (prove)
using this:
f \<bullet> \<one> = \<ominus> ([p] \<cdot> \<one> [^] 3) \<otimes> a [^] 4
a \<in> nonzero Zp
\<lbrakk>[p] \<cdot> \<one> [^] 3 \<in> carrier Zp; a [^] 4 \<in> carrier Zp\<rbrakk> \<Longrightarrow> val_Zp ([p] \<cdot> \<one> [^] 3 \<otimes> a [^] 4) = val_Zp ([p] \<cdot> \<one> [^] 3) + val_Zp (a [^] 4)
val_Zp ([p] \<cdot> \<one> [^] ?n) = eint (int ?n)
[p] \<cdot> \<one> [^] 3 \<in> carrier Zp
[p] \<cdot> \<one> [^] 3 \<noteq> \<zero>
?a \<in> carrier Zp \<Longrightarrow> val_Zp ?a = val_Zp (\<ominus> ?a)

goal (1 subgoal):
 1. val_Zp (f \<bullet> \<one>) = eint 3 + val_Zp (a [^] 4)
[PROOF STEP]
by (metis R.l_minus R.nat_pow_closed a_car monom_term_car of_nat_numeral)
[PROOF STATE]
proof (state)
this:
val_Zp (f \<bullet> \<one>) = eint 3 + val_Zp (a [^] 4)

goal (1 subgoal):
 1. \<exists>y\<in>carrier Zp. \<one> \<oplus> [p] \<cdot> \<one> [^] 3 \<otimes> a [^] 4 = y [^] 2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
val_Zp (f \<bullet> \<one>) = eint 3 + val_Zp (a [^] 4)
[PROOF STEP]
have 2: "val_Zp (f\<bullet>\<one>) = 3 + 4* val_Zp a"
[PROOF STATE]
proof (prove)
using this:
val_Zp (f \<bullet> \<one>) = eint 3 + val_Zp (a [^] 4)

goal (1 subgoal):
 1. val_Zp (f \<bullet> \<one>) = eint 3 + eint 4 * val_Zp a
[PROOF STEP]
using assms val_Zp_pow'
[PROOF STATE]
proof (prove)
using this:
val_Zp (f \<bullet> \<one>) = eint 3 + val_Zp (a [^] 4)
a \<in> nonzero Zp
?x \<in> nonzero Zp \<Longrightarrow> val_Zp (?x [^] ?n) = eint (int ?n) * val_Zp ?x

goal (1 subgoal):
 1. val_Zp (f \<bullet> \<one>) = eint 3 + eint 4 * val_Zp a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
val_Zp (f \<bullet> \<one>) = eint 3 + eint 4 * val_Zp a

goal (1 subgoal):
 1. \<exists>y\<in>carrier Zp. \<one> \<oplus> [p] \<cdot> \<one> [^] 3 \<otimes> a [^] 4 = y [^] 2
[PROOF STEP]
have "pderiv f = pderiv (monom Zp_x \<one> 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pderiv f = pderiv (monom (UP Zp) \<one> 2)
[PROOF STEP]
using assms f_def pderiv_add[of "monom Zp_x \<one> 2"] to_poly_closed R.nat_pow_closed  pderiv_deg_0
[PROOF STATE]
proof (prove)
using this:
a \<in> nonzero Zp
f = monom (UP Zp) \<one> 2 \<oplus>\<^bsub>UP Zp\<^esub> to_polynomial Zp (\<ominus> (\<one> \<oplus> [p] \<cdot> \<one> [^] 3 \<otimes> a [^] 4))
\<lbrakk>monom (UP Zp) \<one> 2 \<in> carrier (UP Zp); ?q \<in> carrier (UP Zp)\<rbrakk> \<Longrightarrow> pderiv (monom (UP Zp) \<one> 2 \<oplus>\<^bsub>UP Zp\<^esub> ?q) = pderiv (monom (UP Zp) \<one> 2) \<oplus>\<^bsub>UP Zp\<^esub> pderiv ?q
?a \<in> carrier Zp \<Longrightarrow> to_polynomial Zp ?a \<in> carrier (UP Zp)
?x \<in> carrier Zp \<Longrightarrow> ?x [^] ?n \<in> carrier Zp
\<lbrakk>?f \<in> carrier (UP Zp); deg Zp ?f = 0\<rbrakk> \<Longrightarrow> pderiv ?f = \<zero>\<^bsub>UP Zp\<^esub>

goal (1 subgoal):
 1. pderiv f = pderiv (monom (UP Zp) \<one> 2)
[PROOF STEP]
unfolding to_polynomial_def
[PROOF STATE]
proof (prove)
using this:
a \<in> nonzero Zp
f = monom (UP Zp) \<one> 2 \<oplus>\<^bsub>UP Zp\<^esub> monom (UP Zp) (\<ominus> (\<one> \<oplus> [p] \<cdot> \<one> [^] 3 \<otimes> a [^] 4)) 0
\<lbrakk>monom (UP Zp) \<one> 2 \<in> carrier (UP Zp); ?q \<in> carrier (UP Zp)\<rbrakk> \<Longrightarrow> pderiv (monom (UP Zp) \<one> 2 \<oplus>\<^bsub>UP Zp\<^esub> ?q) = pderiv (monom (UP Zp) \<one> 2) \<oplus>\<^bsub>UP Zp\<^esub> pderiv ?q
?a \<in> carrier Zp \<Longrightarrow> monom (UP Zp) ?a 0 \<in> carrier (UP Zp)
?x \<in> carrier Zp \<Longrightarrow> ?x [^] ?n \<in> carrier Zp
\<lbrakk>?f \<in> carrier (UP Zp); deg Zp ?f = 0\<rbrakk> \<Longrightarrow> pderiv ?f = \<zero>\<^bsub>UP Zp\<^esub>

goal (1 subgoal):
 1. pderiv f = pderiv (monom (UP Zp) \<one> 2)
[PROOF STEP]
by (metis (no_types, lifting) P.r_zero R.add.inv_closed R.add.m_closed R.one_closed
        UP_zero_closed a_car deg_const deg_nzero_nzero monom_closed monom_term_car p_pow_nonzero(1))
[PROOF STATE]
proof (state)
this:
pderiv f = pderiv (monom (UP Zp) \<one> 2)

goal (1 subgoal):
 1. \<exists>y\<in>carrier Zp. \<one> \<oplus> [p] \<cdot> \<one> [^] 3 \<otimes> a [^] 4 = y [^] 2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pderiv f = pderiv (monom (UP Zp) \<one> 2)
[PROOF STEP]
have 3: "pderiv f = [(2::nat)] \<cdot> \<one> \<odot>\<^bsub>Zp_x\<^esub> X "
[PROOF STATE]
proof (prove)
using this:
pderiv f = pderiv (monom (UP Zp) \<one> 2)

goal (1 subgoal):
 1. pderiv f = [2] \<cdot> \<one> \<odot>\<^bsub>UP Zp\<^esub> X_poly Zp
[PROOF STEP]
by (metis P.nat_pow_eone R.one_closed Suc_1 X_closed diff_Suc_1 monom_rep_X_pow pderiv_monom')
[PROOF STATE]
proof (state)
this:
pderiv f = [2] \<cdot> \<one> \<odot>\<^bsub>UP Zp\<^esub> X_poly Zp

goal (1 subgoal):
 1. \<exists>y\<in>carrier Zp. \<one> \<oplus> [p] \<cdot> \<one> [^] 3 \<otimes> a [^] 4 = y [^] 2
[PROOF STEP]
hence 4: "val_Zp ((pderiv f)\<bullet>\<one>) = val_Zp ([(2::nat)] \<cdot> \<one> )"
[PROOF STATE]
proof (prove)
using this:
pderiv f = [2] \<cdot> \<one> \<odot>\<^bsub>UP Zp\<^esub> X_poly Zp

goal (1 subgoal):
 1. val_Zp (pderiv f \<bullet> \<one>) = val_Zp ([2] \<cdot> \<one>)
[PROOF STEP]
by (metis R.add.nat_pow_eone R.nat_inc_prod R.nat_inc_prod' R.nat_pow_one R.one_closed
        Zp_nat_inc_closed \<open>pderiv f = pderiv (monom Zp_x \<one> 2)\<close> pderiv_monom to_fun_monom)
[PROOF STATE]
proof (state)
this:
val_Zp (pderiv f \<bullet> \<one>) = val_Zp ([2] \<cdot> \<one>)

goal (1 subgoal):
 1. \<exists>y\<in>carrier Zp. \<one> \<oplus> [p] \<cdot> \<one> [^] 3 \<otimes> a [^] 4 = y [^] 2
[PROOF STEP]
have "(2::int) = (int (2::nat))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 = int 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 = int 2

goal (1 subgoal):
 1. \<exists>y\<in>carrier Zp. \<one> \<oplus> [p] \<cdot> \<one> [^] 3 \<otimes> a [^] 4 = y [^] 2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
2 = int 2
[PROOF STEP]
have 5: "[(2::nat)] \<cdot> \<one> = ([(int (2::nat))] \<cdot> \<one> )"
[PROOF STATE]
proof (prove)
using this:
2 = int 2

goal (1 subgoal):
 1. [2] \<cdot> \<one> = [int 2] \<cdot> \<one>
[PROOF STEP]
using add_pow_def int_pow_int
[PROOF STATE]
proof (prove)
using this:
2 = int 2
[?k] \<cdot>\<^bsub>?R\<^esub> ?a = ?a [^]\<^bsub>add_monoid ?R\<^esub> ?k
?x [^]\<^bsub>?G\<^esub> int ?n = ?x [^]\<^bsub>?G\<^esub> ?n

goal (1 subgoal):
 1. [2] \<cdot> \<one> = [int 2] \<cdot> \<one>
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
[2] \<cdot> \<one> = [int 2] \<cdot> \<one>

goal (1 subgoal):
 1. \<exists>y\<in>carrier Zp. \<one> \<oplus> [p] \<cdot> \<one> [^] 3 \<otimes> a [^] 4 = y [^] 2
[PROOF STEP]
have 6: "val_Zp ((pderiv f)\<bullet>\<one>) \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (pderiv f \<bullet> \<one>) \<le> 1
[PROOF STEP]
apply(cases "p = 2")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. p = 2 \<Longrightarrow> val_Zp (pderiv f \<bullet> \<one>) \<le> 1
 2. p \<noteq> 2 \<Longrightarrow> val_Zp (pderiv f \<bullet> \<one>) \<le> 1
[PROOF STEP]
using "4" "5" val_Zp_p
[PROOF STATE]
proof (prove)
using this:
val_Zp (pderiv f \<bullet> \<one>) = val_Zp ([2] \<cdot> \<one>)
[2] \<cdot> \<one> = [int 2] \<cdot> \<one>
val_Zp ([p] \<cdot> \<one>) = 1

goal (2 subgoals):
 1. p = 2 \<Longrightarrow> val_Zp (pderiv f \<bullet> \<one>) \<le> 1
 2. p \<noteq> 2 \<Longrightarrow> val_Zp (pderiv f \<bullet> \<one>) \<le> 1
[PROOF STEP]
apply auto[1]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<noteq> 2 \<Longrightarrow> val_Zp (pderiv f \<bullet> \<one>) \<le> 1
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p \<noteq> 2 \<Longrightarrow> val_Zp (pderiv f \<bullet> \<one>) \<le> 1
[PROOF STEP]
assume "p \<noteq> 2"
[PROOF STATE]
proof (state)
this:
p \<noteq> 2

goal (1 subgoal):
 1. p \<noteq> 2 \<Longrightarrow> val_Zp (pderiv f \<bullet> \<one>) \<le> 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<noteq> 2
[PROOF STEP]
have 60: "coprime 2 p"
[PROOF STATE]
proof (prove)
using this:
p \<noteq> 2

goal (1 subgoal):
 1. coprime 2 p
[PROOF STEP]
using prime prime_int_numeral_eq primes_coprime two_is_prime_nat
[PROOF STATE]
proof (prove)
using this:
p \<noteq> 2
prime p
prime (numeral ?m) = prime (numeral ?m)
\<lbrakk>prime ?p; prime ?q; ?p \<noteq> ?q\<rbrakk> \<Longrightarrow> coprime ?p ?q
prime 2

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

goal (1 subgoal):
 1. p \<noteq> 2 \<Longrightarrow> val_Zp (pderiv f \<bullet> \<one>) \<le> 1
[PROOF STEP]
have 61: "2 < p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 < p
[PROOF STEP]
using 60 prime
[PROOF STATE]
proof (prove)
using this:
coprime 2 p
prime p

goal (1 subgoal):
 1. 2 < p
[PROOF STEP]
by (smt \<open>p \<noteq> 2\<close> prime_gt_1_int)
[PROOF STATE]
proof (state)
this:
2 < p

goal (1 subgoal):
 1. p \<noteq> 2 \<Longrightarrow> val_Zp (pderiv f \<bullet> \<one>) \<le> 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
2 < p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
2 < p

goal (1 subgoal):
 1. val_Zp (pderiv f \<bullet> \<one>) \<le> 1
[PROOF STEP]
by (smt "4" "5" \<open>2 = int 2\<close> mod_pos_pos_trivial nonzero_closed p_nonzero val_Zp_p val_Zp_p_int_unit val_pos)
[PROOF STATE]
proof (state)
this:
val_Zp (pderiv f \<bullet> \<one>) \<le> 1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
val_Zp (pderiv f \<bullet> \<one>) \<le> 1

goal (1 subgoal):
 1. \<exists>y\<in>carrier Zp. \<one> \<oplus> [p] \<cdot> \<one> [^] 3 \<otimes> a [^] 4 = y [^] 2
[PROOF STEP]
have 7: "val_Zp (f\<bullet>\<one>) \<ge> 3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eint 3 \<le> val_Zp (f \<bullet> \<one>)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eint 3 \<le> val_Zp (f \<bullet> \<one>)
[PROOF STEP]
have "eint 4 * val_Zp a \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> eint 4 * val_Zp a
[PROOF STEP]
using 2 val_pos[of a]
[PROOF STATE]
proof (prove)
using this:
val_Zp (f \<bullet> \<one>) = eint 3 + eint 4 * val_Zp a
a \<in> carrier Zp \<Longrightarrow> 0 \<le> val_Zp a

goal (1 subgoal):
 1. 0 \<le> eint 4 * val_Zp a
[PROOF STEP]
by (metis R.nat_pow_closed a_car assms of_nat_numeral val_Zp_pow' val_pos)
[PROOF STATE]
proof (state)
this:
0 \<le> eint 4 * val_Zp a

goal (1 subgoal):
 1. eint 3 \<le> val_Zp (f \<bullet> \<one>)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
0 \<le> eint 4 * val_Zp a

goal (1 subgoal):
 1. eint 3 \<le> val_Zp (f \<bullet> \<one>)
[PROOF STEP]
using "2"
[PROOF STATE]
proof (prove)
using this:
0 \<le> eint 4 * val_Zp a
val_Zp (f \<bullet> \<one>) = eint 3 + eint 4 * val_Zp a

goal (1 subgoal):
 1. eint 3 \<le> val_Zp (f \<bullet> \<one>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eint 3 \<le> val_Zp (f \<bullet> \<one>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eint 3 \<le> val_Zp (f \<bullet> \<one>)

goal (1 subgoal):
 1. \<exists>y\<in>carrier Zp. \<one> \<oplus> [p] \<cdot> \<one> [^] 3 \<otimes> a [^] 4 = y [^] 2
[PROOF STEP]
have "2*val_Zp ((pderiv f)\<bullet>\<one>) \<le> 2*1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eint 2 * val_Zp (pderiv f \<bullet> \<one>) \<le> eint 2 * 1
[PROOF STEP]
using 6 one_eint_def eint_mult_mono'
[PROOF STATE]
proof (prove)
using this:
val_Zp (pderiv f \<bullet> \<one>) \<le> 1
1 = eint 1
\<lbrakk>0 \<le> ?c \<and> ?c \<noteq> \<infinity>; ?n < ?k\<rbrakk> \<Longrightarrow> ?n * ?c \<le> ?k * ?c

goal (1 subgoal):
 1. eint 2 * val_Zp (pderiv f \<bullet> \<one>) \<le> eint 2 * 1
[PROOF STEP]
by (smt \<open>2 = int 2\<close> eint.distinct(2) eint_ile eint_ord_simps(1) eint_ord_simps(2) mult.commute
        ord_Zp_p ord_Zp_p_pow ord_Zp_pow p_nonzero p_pow_nonzero(1) times_eint_simps(1) val_Zp_p val_Zp_pow' val_pos)
[PROOF STATE]
proof (state)
this:
eint 2 * val_Zp (pderiv f \<bullet> \<one>) \<le> eint 2 * 1

goal (1 subgoal):
 1. \<exists>y\<in>carrier Zp. \<one> \<oplus> [p] \<cdot> \<one> [^] 3 \<otimes> a [^] 4 = y [^] 2
[PROOF STEP]
hence 8: "2 * val_Zp ((pderiv f)\<bullet> \<one>) < val_Zp (f\<bullet>\<one>)"
[PROOF STATE]
proof (prove)
using this:
eint 2 * val_Zp (pderiv f \<bullet> \<one>) \<le> eint 2 * 1

goal (1 subgoal):
 1. eint 2 * val_Zp (pderiv f \<bullet> \<one>) < val_Zp (f \<bullet> \<one>)
[PROOF STEP]
using 7 le_less_trans[of "2 * val_Zp ((pderiv f)\<bullet> \<one>)" "2::eint" 3]
            less_le_trans[of "2 * val_Zp ((pderiv f)\<bullet> \<one>)" 3 "val_Zp (f\<bullet>\<one>)"] one_eint_def
[PROOF STATE]
proof (prove)
using this:
eint 2 * val_Zp (pderiv f \<bullet> \<one>) \<le> eint 2 * 1
eint 3 \<le> val_Zp (f \<bullet> \<one>)
\<lbrakk>eint 2 * val_Zp (pderiv f \<bullet> \<one>) \<le> eint 2; eint 2 < eint 3\<rbrakk> \<Longrightarrow> eint 2 * val_Zp (pderiv f \<bullet> \<one>) < eint 3
\<lbrakk>eint 2 * val_Zp (pderiv f \<bullet> \<one>) < eint 3; eint 3 \<le> val_Zp (f \<bullet> \<one>)\<rbrakk> \<Longrightarrow> eint 2 * val_Zp (pderiv f \<bullet> \<one>) < val_Zp (f \<bullet> \<one>)
1 = eint 1

goal (1 subgoal):
 1. eint 2 * val_Zp (pderiv f \<bullet> \<one>) < val_Zp (f \<bullet> \<one>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eint 2 * val_Zp (pderiv f \<bullet> \<one>) < val_Zp (f \<bullet> \<one>)

goal (1 subgoal):
 1. \<exists>y\<in>carrier Zp. \<one> \<oplus> [p] \<cdot> \<one> [^] 3 \<otimes> a [^] 4 = y [^] 2
[PROOF STEP]
obtain \<alpha> where  \<alpha>_def: "f\<bullet>\<alpha> = \<zero>" and  \<alpha>_def' :"\<alpha> \<in> carrier Zp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<alpha>. \<lbrakk>f \<bullet> \<alpha> = \<zero>; \<alpha> \<in> carrier Zp\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using 2 6 7 hensels_lemma' 8 \<open>f \<in> carrier Zp_x\<close>
[PROOF STATE]
proof (prove)
using this:
val_Zp (f \<bullet> \<one>) = eint 3 + eint 4 * val_Zp a
val_Zp (pderiv f \<bullet> \<one>) \<le> 1
eint 3 \<le> val_Zp (f \<bullet> \<one>)
\<lbrakk>?f \<in> carrier (UP Zp); ?a \<in> carrier Zp; eint 2 * val_Zp (pderiv ?f \<bullet> ?a) < val_Zp (?f \<bullet> ?a)\<rbrakk> \<Longrightarrow> \<exists>!\<alpha>. \<alpha> \<in> carrier Zp \<and> ?f \<bullet> \<alpha> = \<zero> \<and> val_Zp (pderiv ?f \<bullet> ?a) < val_Zp (?a \<ominus> \<alpha>)
eint 2 * val_Zp (pderiv f \<bullet> \<one>) < val_Zp (f \<bullet> \<one>)
f \<in> carrier (UP Zp)

goal (1 subgoal):
 1. (\<And>\<alpha>. \<lbrakk>f \<bullet> \<alpha> = \<zero>; \<alpha> \<in> carrier Zp\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f \<bullet> \<alpha> = \<zero>
\<alpha> \<in> carrier Zp

goal (1 subgoal):
 1. \<exists>y\<in>carrier Zp. \<one> \<oplus> [p] \<cdot> \<one> [^] 3 \<otimes> a [^] 4 = y [^] 2
[PROOF STEP]
have 0: "(monom Zp_x \<one> 2) \<bullet> \<alpha> = \<alpha> [^] (2::nat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monom (UP Zp) \<one> 2 \<bullet> \<alpha> = \<alpha> [^] 2
[PROOF STEP]
by (simp add: \<alpha>_def' to_fun_monic_monom)
[PROOF STATE]
proof (state)
this:
monom (UP Zp) \<one> 2 \<bullet> \<alpha> = \<alpha> [^] 2

goal (1 subgoal):
 1. \<exists>y\<in>carrier Zp. \<one> \<oplus> [p] \<cdot> \<one> [^] 3 \<otimes> a [^] 4 = y [^] 2
[PROOF STEP]
have 1: "to_poly (\<ominus> (\<one> \<oplus> (\<p> [^] (3::nat))\<otimes> (a [^] (4::nat)))) \<bullet> \<alpha> =\<ominus>( \<one> \<oplus> (\<p> [^] (3::nat))\<otimes> (a [^] (4::nat)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_polynomial Zp (\<ominus> (\<one> \<oplus> [p] \<cdot> \<one> [^] 3 \<otimes> a [^] 4)) \<bullet> \<alpha> = \<ominus> (\<one> \<oplus> [p] \<cdot> \<one> [^] 3 \<otimes> a [^] 4)
[PROOF STEP]
by (simp add: \<alpha>_def' a_car to_fun_to_poly)
[PROOF STATE]
proof (state)
this:
to_polynomial Zp (\<ominus> (\<one> \<oplus> [p] \<cdot> \<one> [^] 3 \<otimes> a [^] 4)) \<bullet> \<alpha> = \<ominus> (\<one> \<oplus> [p] \<cdot> \<one> [^] 3 \<otimes> a [^] 4)

goal (1 subgoal):
 1. \<exists>y\<in>carrier Zp. \<one> \<oplus> [p] \<cdot> \<one> [^] 3 \<otimes> a [^] 4 = y [^] 2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
to_polynomial Zp (\<ominus> (\<one> \<oplus> [p] \<cdot> \<one> [^] 3 \<otimes> a [^] 4)) \<bullet> \<alpha> = \<ominus> (\<one> \<oplus> [p] \<cdot> \<one> [^] 3 \<otimes> a [^] 4)
[PROOF STEP]
have "\<alpha> [^] (2::nat) \<ominus> (\<one> \<oplus> (\<p> [^] (3::nat))\<otimes> (a [^] (4::nat))) = \<zero>"
[PROOF STATE]
proof (prove)
using this:
to_polynomial Zp (\<ominus> (\<one> \<oplus> [p] \<cdot> \<one> [^] 3 \<otimes> a [^] 4)) \<bullet> \<alpha> = \<ominus> (\<one> \<oplus> [p] \<cdot> \<one> [^] 3 \<otimes> a [^] 4)

goal (1 subgoal):
 1. \<alpha> [^] 2 \<ominus> (\<one> \<oplus> [p] \<cdot> \<one> [^] 3 \<otimes> a [^] 4) = \<zero>
[PROOF STEP]
using \<alpha>_def \<alpha>_def'
[PROOF STATE]
proof (prove)
using this:
to_polynomial Zp (\<ominus> (\<one> \<oplus> [p] \<cdot> \<one> [^] 3 \<otimes> a [^] 4)) \<bullet> \<alpha> = \<ominus> (\<one> \<oplus> [p] \<cdot> \<one> [^] 3 \<otimes> a [^] 4)
f \<bullet> \<alpha> = \<zero>
\<alpha> \<in> carrier Zp

goal (1 subgoal):
 1. \<alpha> [^] 2 \<ominus> (\<one> \<oplus> [p] \<cdot> \<one> [^] 3 \<otimes> a [^] 4) = \<zero>
[PROOF STEP]
by (simp add: R.minus_eq a_car f_def to_fun_monom_plus to_poly_closed)
[PROOF STATE]
proof (state)
this:
\<alpha> [^] 2 \<ominus> (\<one> \<oplus> [p] \<cdot> \<one> [^] 3 \<otimes> a [^] 4) = \<zero>

goal (1 subgoal):
 1. \<exists>y\<in>carrier Zp. \<one> \<oplus> [p] \<cdot> \<one> [^] 3 \<otimes> a [^] 4 = y [^] 2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<alpha> [^] 2 \<ominus> (\<one> \<oplus> [p] \<cdot> \<one> [^] 3 \<otimes> a [^] 4) = \<zero>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<alpha> [^] 2 \<ominus> (\<one> \<oplus> [p] \<cdot> \<one> [^] 3 \<otimes> a [^] 4) = \<zero>

goal (1 subgoal):
 1. \<exists>y\<in>carrier Zp. \<one> \<oplus> [p] \<cdot> \<one> [^] 3 \<otimes> a [^] 4 = y [^] 2
[PROOF STEP]
by (metis R.add.m_closed R.nat_pow_closed R.one_closed R.r_right_minus_eq \<alpha>_def' a_car monom_term_car p_pow_nonzero(1))
[PROOF STATE]
proof (state)
this:
\<exists>y\<in>carrier Zp. \<one> \<oplus> [p] \<cdot> \<one> [^] 3 \<otimes> a [^] 4 = y [^] 2

goal:
No subgoals!
[PROOF STEP]
qed