[STATEMENT]
lemma gauss_int_norm_eq_prime_squareD:
  assumes "prime p" and "[p = 3] (mod 4)" and "gauss_int_norm z = p ^ 2"
  shows   "normalize z = of_nat p" and "prime_elem z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. normalize z = of_nat p &&& prime_elem z
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. normalize z = of_nat p
 2. prime_elem z
[PROOF STEP]
have "\<exists>q::gauss_int. q dvd z \<and> prime q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>q. q dvd z \<and> prime q
[PROOF STEP]
by (rule prime_divisor_exists) (use assms in \<open>auto simp: is_unit_gauss_int_iff'\<close>)
[PROOF STATE]
proof (state)
this:
\<exists>q. q dvd z \<and> prime q

goal (2 subgoals):
 1. normalize z = of_nat p
 2. prime_elem z
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>q. q dvd z \<and> prime q
[PROOF STEP]
obtain q :: gauss_int where q: "q dvd z" "prime q"
[PROOF STATE]
proof (prove)
using this:
\<exists>q. q dvd z \<and> prime q

goal (1 subgoal):
 1. (\<And>q. \<lbrakk>q dvd z; prime q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
q dvd z
prime q

goal (2 subgoals):
 1. normalize z = of_nat p
 2. prime_elem z
[PROOF STEP]
have "gauss_int_norm q dvd gauss_int_norm z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gauss_int_norm q dvd gauss_int_norm z
[PROOF STEP]
by (rule gauss_int_norm_dvd_mono) fact
[PROOF STATE]
proof (state)
this:
gauss_int_norm q dvd gauss_int_norm z

goal (2 subgoals):
 1. normalize z = of_nat p
 2. prime_elem z
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
gauss_int_norm q dvd gauss_int_norm z

goal (2 subgoals):
 1. normalize z = of_nat p
 2. prime_elem z
[PROOF STEP]
have "\<dots> = p ^ 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gauss_int_norm z = p\<^sup>2
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
gauss_int_norm z = p\<^sup>2

goal (2 subgoals):
 1. normalize z = of_nat p
 2. prime_elem z
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
gauss_int_norm q dvd p\<^sup>2
[PROOF STEP]
obtain i where i: "i \<le> 2" "gauss_int_norm q = p ^ i"
[PROOF STATE]
proof (prove)
using this:
gauss_int_norm q dvd p\<^sup>2

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>i \<le> 2; gauss_int_norm q = p ^ i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (subst (asm) divides_primepow_nat) (use assms q in auto)
[PROOF STATE]
proof (state)
this:
i \<le> 2
gauss_int_norm q = p ^ i

goal (2 subgoals):
 1. normalize z = of_nat p
 2. prime_elem z
[PROOF STEP]
from i assms q
[PROOF STATE]
proof (chain)
picking this:
i \<le> 2
gauss_int_norm q = p ^ i
prime p
[p = 3] (mod 4)
gauss_int_norm z = p\<^sup>2
q dvd z
prime q
[PROOF STEP]
have "i \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
i \<le> 2
gauss_int_norm q = p ^ i
prime p
[p = 3] (mod 4)
gauss_int_norm z = p\<^sup>2
q dvd z
prime q

goal (1 subgoal):
 1. i \<noteq> 0
[PROOF STEP]
by (auto intro!: Nat.gr0I simp: gauss_int_norm_eq_Suc_0_iff)
[PROOF STATE]
proof (state)
this:
i \<noteq> 0

goal (2 subgoals):
 1. normalize z = of_nat p
 2. prime_elem z
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i \<noteq> 0

goal (2 subgoals):
 1. normalize z = of_nat p
 2. prime_elem z
[PROOF STEP]
from i assms q
[PROOF STATE]
proof (chain)
picking this:
i \<le> 2
gauss_int_norm q = p ^ i
prime p
[p = 3] (mod 4)
gauss_int_norm z = p\<^sup>2
q dvd z
prime q
[PROOF STEP]
have "i \<noteq> 1"
[PROOF STATE]
proof (prove)
using this:
i \<le> 2
gauss_int_norm q = p ^ i
prime p
[p = 3] (mod 4)
gauss_int_norm z = p\<^sup>2
q dvd z
prime q

goal (1 subgoal):
 1. i \<noteq> 1
[PROOF STEP]
using gauss_int_norm_not_3_mod_4[of q]
[PROOF STATE]
proof (prove)
using this:
i \<le> 2
gauss_int_norm q = p ^ i
prime p
[p = 3] (mod 4)
gauss_int_norm z = p\<^sup>2
q dvd z
prime q
[gauss_int_norm q \<noteq> 3] (mod 4)

goal (1 subgoal):
 1. i \<noteq> 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i \<noteq> 1

goal (2 subgoals):
 1. normalize z = of_nat p
 2. prime_elem z
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
i \<noteq> 0
i \<noteq> 1
[PROOF STEP]
have "i = 2"
[PROOF STATE]
proof (prove)
using this:
i \<noteq> 0
i \<noteq> 1

goal (1 subgoal):
 1. i = 2
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
i \<noteq> 0
i \<noteq> 1
i \<le> 2
gauss_int_norm q = p ^ i

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

goal (2 subgoals):
 1. normalize z = of_nat p
 2. prime_elem z
[PROOF STEP]
with i
[PROOF STATE]
proof (chain)
picking this:
i \<le> 2
gauss_int_norm q = p ^ i
i = 2
[PROOF STEP]
have "gauss_int_norm q = p ^ 2"
[PROOF STATE]
proof (prove)
using this:
i \<le> 2
gauss_int_norm q = p ^ i
i = 2

goal (1 subgoal):
 1. gauss_int_norm q = p\<^sup>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
gauss_int_norm q = p\<^sup>2

goal (2 subgoals):
 1. normalize z = of_nat p
 2. prime_elem z
[PROOF STEP]
hence [simp]: "q = of_nat p"
[PROOF STATE]
proof (prove)
using this:
gauss_int_norm q = p\<^sup>2

goal (1 subgoal):
 1. q = of_nat p
[PROOF STEP]
using prime_gauss_int_norm_squareD[of q p] q
[PROOF STATE]
proof (prove)
using this:
gauss_int_norm q = p\<^sup>2
\<lbrakk>prime q; gauss_int_norm q = p\<^sup>2\<rbrakk> \<Longrightarrow> prime p \<and> q = of_nat p
q dvd z
prime q

goal (1 subgoal):
 1. q = of_nat p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
q = of_nat p

goal (2 subgoals):
 1. normalize z = of_nat p
 2. prime_elem z
[PROOF STEP]
have "normalize (of_nat p) = normalize z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. normalize (of_nat p) = normalize z
[PROOF STEP]
using q assms
[PROOF STATE]
proof (prove)
using this:
q dvd z
prime q
prime p
[p = 3] (mod 4)
gauss_int_norm z = p\<^sup>2

goal (1 subgoal):
 1. normalize (of_nat p) = normalize z
[PROOF STEP]
by (intro gauss_int_dvd_same_norm_imp_associated) auto
[PROOF STATE]
proof (state)
this:
normalize (of_nat p) = normalize z

goal (2 subgoals):
 1. normalize z = of_nat p
 2. prime_elem z
[PROOF STEP]
thus *: "normalize z = of_nat p"
[PROOF STATE]
proof (prove)
using this:
normalize (of_nat p) = normalize z

goal (1 subgoal):
 1. normalize z = of_nat p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
normalize z = of_nat p

goal (1 subgoal):
 1. prime_elem z
[PROOF STEP]
have "prime (normalize z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime (normalize z)
[PROOF STEP]
using prime_gauss_int_of_nat[of p] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>prime p; [p = 3] (mod 4)\<rbrakk> \<Longrightarrow> prime (of_nat p)
prime p
[p = 3] (mod 4)
gauss_int_norm z = p\<^sup>2

goal (1 subgoal):
 1. prime (normalize z)
[PROOF STEP]
by (subst *) auto
[PROOF STATE]
proof (state)
this:
prime (normalize z)

goal (1 subgoal):
 1. prime_elem z
[PROOF STEP]
thus "prime_elem z"
[PROOF STATE]
proof (prove)
using this:
prime (normalize z)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prime_elem_gauss_int_iff:
  fixes z :: gauss_int
  defines "n \<equiv> gauss_int_norm z"
  shows   "prime_elem z \<longleftrightarrow> prime n \<or> (\<exists>p. n = p ^ 2 \<and> prime p \<and> [p = 3] (mod 4))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime_elem z = (prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4)))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. prime_elem z \<Longrightarrow> prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))
 2. prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4)) \<Longrightarrow> prime_elem z
[PROOF STEP]
assume "prime n \<or> (\<exists>p. n = p ^ 2 \<and> prime p \<and> [p = 3] (mod 4))"
[PROOF STATE]
proof (state)
this:
prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))

goal (2 subgoals):
 1. prime_elem z \<Longrightarrow> prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))
 2. prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4)) \<Longrightarrow> prime_elem z
[PROOF STEP]
thus "prime_elem z"
[PROOF STATE]
proof (prove)
using this:
prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))

goal (1 subgoal):
 1. prime_elem z
[PROOF STEP]
by (auto intro: gauss_int_norm_eq_prime_squareD(2)
                    prime_gauss_int_norm_imp_prime_elem simp: n_def)
[PROOF STATE]
proof (state)
this:
prime_elem z

goal (1 subgoal):
 1. prime_elem z \<Longrightarrow> prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prime_elem z \<Longrightarrow> prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))
[PROOF STEP]
assume "prime_elem z"
[PROOF STATE]
proof (state)
this:
prime_elem z

goal (1 subgoal):
 1. prime_elem z \<Longrightarrow> prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))
[PROOF STEP]
hence "prime (normalize z)"
[PROOF STATE]
proof (prove)
using this:
prime_elem z

goal (1 subgoal):
 1. prime (normalize z)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
prime (normalize z)

goal (1 subgoal):
 1. prime_elem z \<Longrightarrow> prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))
[PROOF STEP]
thus "prime n \<or> (\<exists>p. n = p ^ 2 \<and> prime p \<and> [p = 3] (mod 4))"
[PROOF STATE]
proof (prove)
using this:
prime (normalize z)

goal (1 subgoal):
 1. prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))
[PROOF STEP]
proof (cases rule: gauss_int_prime_classification)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. normalize z = 1 + \<i>\<^sub>\<int> \<Longrightarrow> prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))
 2. \<And>p. \<lbrakk>normalize z = of_nat p; prime p; [p = 3] (mod 4)\<rbrakk> \<Longrightarrow> prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))
 3. \<lbrakk>prime (gauss_int_norm (normalize z)); [gauss_int_norm (normalize z) = 1] (mod 4); 0 < ReZ (normalize z); 0 < ImZ (normalize z); ReZ (normalize z) \<noteq> ImZ (normalize z)\<rbrakk> \<Longrightarrow> prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))
[PROOF STEP]
case one_plus_i
[PROOF STATE]
proof (state)
this:
normalize z = 1 + \<i>\<^sub>\<int>

goal (3 subgoals):
 1. normalize z = 1 + \<i>\<^sub>\<int> \<Longrightarrow> prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))
 2. \<And>p. \<lbrakk>normalize z = of_nat p; prime p; [p = 3] (mod 4)\<rbrakk> \<Longrightarrow> prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))
 3. \<lbrakk>prime (gauss_int_norm (normalize z)); [gauss_int_norm (normalize z) = 1] (mod 4); 0 < ReZ (normalize z); 0 < ImZ (normalize z); ReZ (normalize z) \<noteq> ImZ (normalize z)\<rbrakk> \<Longrightarrow> prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))
[PROOF STEP]
have "n = gauss_int_norm (normalize z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n = gauss_int_norm (normalize z)
[PROOF STEP]
by (simp add: n_def)
[PROOF STATE]
proof (state)
this:
n = gauss_int_norm (normalize z)

goal (3 subgoals):
 1. normalize z = 1 + \<i>\<^sub>\<int> \<Longrightarrow> prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))
 2. \<And>p. \<lbrakk>normalize z = of_nat p; prime p; [p = 3] (mod 4)\<rbrakk> \<Longrightarrow> prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))
 3. \<lbrakk>prime (gauss_int_norm (normalize z)); [gauss_int_norm (normalize z) = 1] (mod 4); 0 < ReZ (normalize z); 0 < ImZ (normalize z); ReZ (normalize z) \<noteq> ImZ (normalize z)\<rbrakk> \<Longrightarrow> prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
n = gauss_int_norm (normalize z)

goal (3 subgoals):
 1. normalize z = 1 + \<i>\<^sub>\<int> \<Longrightarrow> prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))
 2. \<And>p. \<lbrakk>normalize z = of_nat p; prime p; [p = 3] (mod 4)\<rbrakk> \<Longrightarrow> prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))
 3. \<lbrakk>prime (gauss_int_norm (normalize z)); [gauss_int_norm (normalize z) = 1] (mod 4); 0 < ReZ (normalize z); 0 < ImZ (normalize z); ReZ (normalize z) \<noteq> ImZ (normalize z)\<rbrakk> \<Longrightarrow> prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))
[PROOF STEP]
have "normalize z = 1 + \<i>\<^sub>\<int>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. normalize z = 1 + \<i>\<^sub>\<int>
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
normalize z = 1 + \<i>\<^sub>\<int>

goal (3 subgoals):
 1. normalize z = 1 + \<i>\<^sub>\<int> \<Longrightarrow> prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))
 2. \<And>p. \<lbrakk>normalize z = of_nat p; prime p; [p = 3] (mod 4)\<rbrakk> \<Longrightarrow> prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))
 3. \<lbrakk>prime (gauss_int_norm (normalize z)); [gauss_int_norm (normalize z) = 1] (mod 4); 0 < ReZ (normalize z); 0 < ImZ (normalize z); ReZ (normalize z) \<noteq> ImZ (normalize z)\<rbrakk> \<Longrightarrow> prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
normalize z = 1 + \<i>\<^sub>\<int>

goal (3 subgoals):
 1. normalize z = 1 + \<i>\<^sub>\<int> \<Longrightarrow> prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))
 2. \<And>p. \<lbrakk>normalize z = of_nat p; prime p; [p = 3] (mod 4)\<rbrakk> \<Longrightarrow> prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))
 3. \<lbrakk>prime (gauss_int_norm (normalize z)); [gauss_int_norm (normalize z) = 1] (mod 4); 0 < ReZ (normalize z); 0 < ImZ (normalize z); ReZ (normalize z) \<noteq> ImZ (normalize z)\<rbrakk> \<Longrightarrow> prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))
[PROOF STEP]
have "gauss_int_norm \<dots> = 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gauss_int_norm (1 + \<i>\<^sub>\<int>) = 2
[PROOF STEP]
by (simp add: gauss_int_norm_def)
[PROOF STATE]
proof (state)
this:
gauss_int_norm (1 + \<i>\<^sub>\<int>) = 2

goal (3 subgoals):
 1. normalize z = 1 + \<i>\<^sub>\<int> \<Longrightarrow> prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))
 2. \<And>p. \<lbrakk>normalize z = of_nat p; prime p; [p = 3] (mod 4)\<rbrakk> \<Longrightarrow> prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))
 3. \<lbrakk>prime (gauss_int_norm (normalize z)); [gauss_int_norm (normalize z) = 1] (mod 4); 0 < ReZ (normalize z); 0 < ImZ (normalize z); ReZ (normalize z) \<noteq> ImZ (normalize z)\<rbrakk> \<Longrightarrow> prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
n = 2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n = 2

goal (1 subgoal):
 1. prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))

goal (2 subgoals):
 1. \<And>p. \<lbrakk>normalize z = of_nat p; prime p; [p = 3] (mod 4)\<rbrakk> \<Longrightarrow> prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))
 2. \<lbrakk>prime (gauss_int_norm (normalize z)); [gauss_int_norm (normalize z) = 1] (mod 4); 0 < ReZ (normalize z); 0 < ImZ (normalize z); ReZ (normalize z) \<noteq> ImZ (normalize z)\<rbrakk> \<Longrightarrow> prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>p. \<lbrakk>normalize z = of_nat p; prime p; [p = 3] (mod 4)\<rbrakk> \<Longrightarrow> prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))
 2. \<lbrakk>prime (gauss_int_norm (normalize z)); [gauss_int_norm (normalize z) = 1] (mod 4); 0 < ReZ (normalize z); 0 < ImZ (normalize z); ReZ (normalize z) \<noteq> ImZ (normalize z)\<rbrakk> \<Longrightarrow> prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))
[PROOF STEP]
case (cong_3_mod_4 p)
[PROOF STATE]
proof (state)
this:
normalize z = of_nat p
prime p
[p = 3] (mod 4)

goal (2 subgoals):
 1. \<And>p. \<lbrakk>normalize z = of_nat p; prime p; [p = 3] (mod 4)\<rbrakk> \<Longrightarrow> prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))
 2. \<lbrakk>prime (gauss_int_norm (normalize z)); [gauss_int_norm (normalize z) = 1] (mod 4); 0 < ReZ (normalize z); 0 < ImZ (normalize z); ReZ (normalize z) \<noteq> ImZ (normalize z)\<rbrakk> \<Longrightarrow> prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))
[PROOF STEP]
have "n = gauss_int_norm (normalize z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n = gauss_int_norm (normalize z)
[PROOF STEP]
by (simp add: n_def)
[PROOF STATE]
proof (state)
this:
n = gauss_int_norm (normalize z)

goal (2 subgoals):
 1. \<And>p. \<lbrakk>normalize z = of_nat p; prime p; [p = 3] (mod 4)\<rbrakk> \<Longrightarrow> prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))
 2. \<lbrakk>prime (gauss_int_norm (normalize z)); [gauss_int_norm (normalize z) = 1] (mod 4); 0 < ReZ (normalize z); 0 < ImZ (normalize z); ReZ (normalize z) \<noteq> ImZ (normalize z)\<rbrakk> \<Longrightarrow> prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
n = gauss_int_norm (normalize z)

goal (2 subgoals):
 1. \<And>p. \<lbrakk>normalize z = of_nat p; prime p; [p = 3] (mod 4)\<rbrakk> \<Longrightarrow> prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))
 2. \<lbrakk>prime (gauss_int_norm (normalize z)); [gauss_int_norm (normalize z) = 1] (mod 4); 0 < ReZ (normalize z); 0 < ImZ (normalize z); ReZ (normalize z) \<noteq> ImZ (normalize z)\<rbrakk> \<Longrightarrow> prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))
[PROOF STEP]
have "normalize z = of_nat p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. normalize z = of_nat p
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
normalize z = of_nat p

goal (2 subgoals):
 1. \<And>p. \<lbrakk>normalize z = of_nat p; prime p; [p = 3] (mod 4)\<rbrakk> \<Longrightarrow> prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))
 2. \<lbrakk>prime (gauss_int_norm (normalize z)); [gauss_int_norm (normalize z) = 1] (mod 4); 0 < ReZ (normalize z); 0 < ImZ (normalize z); ReZ (normalize z) \<noteq> ImZ (normalize z)\<rbrakk> \<Longrightarrow> prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
normalize z = of_nat p

goal (2 subgoals):
 1. \<And>p. \<lbrakk>normalize z = of_nat p; prime p; [p = 3] (mod 4)\<rbrakk> \<Longrightarrow> prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))
 2. \<lbrakk>prime (gauss_int_norm (normalize z)); [gauss_int_norm (normalize z) = 1] (mod 4); 0 < ReZ (normalize z); 0 < ImZ (normalize z); ReZ (normalize z) \<noteq> ImZ (normalize z)\<rbrakk> \<Longrightarrow> prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))
[PROOF STEP]
have "gauss_int_norm \<dots> = p ^ 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gauss_int_norm (of_nat p) = p\<^sup>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
gauss_int_norm (of_nat p) = p\<^sup>2

goal (2 subgoals):
 1. \<And>p. \<lbrakk>normalize z = of_nat p; prime p; [p = 3] (mod 4)\<rbrakk> \<Longrightarrow> prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))
 2. \<lbrakk>prime (gauss_int_norm (normalize z)); [gauss_int_norm (normalize z) = 1] (mod 4); 0 < ReZ (normalize z); 0 < ImZ (normalize z); ReZ (normalize z) \<noteq> ImZ (normalize z)\<rbrakk> \<Longrightarrow> prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
n = p\<^sup>2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n = p\<^sup>2

goal (1 subgoal):
 1. prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))
[PROOF STEP]
using cong_3_mod_4
[PROOF STATE]
proof (prove)
using this:
n = p\<^sup>2
normalize z = of_nat p
prime p
[p = 3] (mod 4)

goal (1 subgoal):
 1. prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))

goal (1 subgoal):
 1. \<lbrakk>prime (gauss_int_norm (normalize z)); [gauss_int_norm (normalize z) = 1] (mod 4); 0 < ReZ (normalize z); 0 < ImZ (normalize z); ReZ (normalize z) \<noteq> ImZ (normalize z)\<rbrakk> \<Longrightarrow> prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>prime (gauss_int_norm (normalize z)); [gauss_int_norm (normalize z) = 1] (mod 4); 0 < ReZ (normalize z); 0 < ImZ (normalize z); ReZ (normalize z) \<noteq> ImZ (normalize z)\<rbrakk> \<Longrightarrow> prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))
[PROOF STEP]
case cong_1_mod_4
[PROOF STATE]
proof (state)
this:
prime (gauss_int_norm (normalize z))
[gauss_int_norm (normalize z) = 1] (mod 4)
0 < ReZ (normalize z)
0 < ImZ (normalize z)
ReZ (normalize z) \<noteq> ImZ (normalize z)

goal (1 subgoal):
 1. \<lbrakk>prime (gauss_int_norm (normalize z)); [gauss_int_norm (normalize z) = 1] (mod 4); 0 < ReZ (normalize z); 0 < ImZ (normalize z); ReZ (normalize z) \<noteq> ImZ (normalize z)\<rbrakk> \<Longrightarrow> prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
prime (gauss_int_norm (normalize z))
[gauss_int_norm (normalize z) = 1] (mod 4)
0 < ReZ (normalize z)
0 < ImZ (normalize z)
ReZ (normalize z) \<noteq> ImZ (normalize z)

goal (1 subgoal):
 1. prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))
[PROOF STEP]
by (simp add: n_def)
[PROOF STATE]
proof (state)
this:
prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
prime n \<or> (\<exists>p. n = p\<^sup>2 \<and> prime p \<and> [p = 3] (mod 4))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma multiplicity_prime_1_plus_i_aux: "multiplicity (1 + \<i>\<^sub>\<int>) (of_nat c) = 2 * multiplicity 2 c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicity (1 + \<i>\<^sub>\<int>) (of_nat c) = 2 * multiplicity 2 c
[PROOF STEP]
proof (cases "c = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. c = 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) (of_nat c) = 2 * multiplicity 2 c
 2. c \<noteq> 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) (of_nat c) = 2 * multiplicity 2 c
[PROOF STEP]
case [simp]: False
[PROOF STATE]
proof (state)
this:
c \<noteq> 0

goal (2 subgoals):
 1. c = 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) (of_nat c) = 2 * multiplicity 2 c
 2. c \<noteq> 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) (of_nat c) = 2 * multiplicity 2 c
[PROOF STEP]
have "2 * multiplicity 2 c = multiplicity 2 (c ^ 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * multiplicity 2 c = multiplicity 2 (c\<^sup>2)
[PROOF STEP]
by (simp add: prime_elem_multiplicity_power_distrib)
[PROOF STATE]
proof (state)
this:
2 * multiplicity 2 c = multiplicity 2 (c\<^sup>2)

goal (2 subgoals):
 1. c = 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) (of_nat c) = 2 * multiplicity 2 c
 2. c \<noteq> 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) (of_nat c) = 2 * multiplicity 2 c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
2 * multiplicity 2 c = multiplicity 2 (c\<^sup>2)

goal (2 subgoals):
 1. c = 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) (of_nat c) = 2 * multiplicity 2 c
 2. c \<noteq> 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) (of_nat c) = 2 * multiplicity 2 c
[PROOF STEP]
have "multiplicity 2 (c ^ 2) = multiplicity (of_nat 2) (of_nat c ^ 2 :: gauss_int)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicity 2 (c\<^sup>2) = multiplicity (of_nat 2) ((of_nat c)\<^sup>2)
[PROOF STEP]
by (simp flip: multiplicity_gauss_int_of_nat)
[PROOF STATE]
proof (state)
this:
multiplicity 2 (c\<^sup>2) = multiplicity (of_nat 2) ((of_nat c)\<^sup>2)

goal (2 subgoals):
 1. c = 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) (of_nat c) = 2 * multiplicity 2 c
 2. c \<noteq> 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) (of_nat c) = 2 * multiplicity 2 c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
multiplicity 2 (c\<^sup>2) = multiplicity (of_nat 2) ((of_nat c)\<^sup>2)

goal (2 subgoals):
 1. c = 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) (of_nat c) = 2 * multiplicity 2 c
 2. c \<noteq> 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) (of_nat c) = 2 * multiplicity 2 c
[PROOF STEP]
have "of_nat 2 = (-\<i>\<^sub>\<int>) * (1 + \<i>\<^sub>\<int>) ^ 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_nat 2 = - \<i>\<^sub>\<int> * (1 + \<i>\<^sub>\<int>)\<^sup>2
[PROOF STEP]
by (simp add: algebra_simps power2_eq_square)
[PROOF STATE]
proof (state)
this:
of_nat 2 = - \<i>\<^sub>\<int> * (1 + \<i>\<^sub>\<int>)\<^sup>2

goal (2 subgoals):
 1. c = 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) (of_nat c) = 2 * multiplicity 2 c
 2. c \<noteq> 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) (of_nat c) = 2 * multiplicity 2 c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
of_nat 2 = - \<i>\<^sub>\<int> * (1 + \<i>\<^sub>\<int>)\<^sup>2

goal (2 subgoals):
 1. c = 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) (of_nat c) = 2 * multiplicity 2 c
 2. c \<noteq> 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) (of_nat c) = 2 * multiplicity 2 c
[PROOF STEP]
have "multiplicity \<dots> (of_nat c ^ 2) = multiplicity ((1 + \<i>\<^sub>\<int>) ^ 2) (of_nat c ^ 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicity (- \<i>\<^sub>\<int> * (1 + \<i>\<^sub>\<int>)\<^sup>2) ((of_nat c)\<^sup>2) = multiplicity ((1 + \<i>\<^sub>\<int>)\<^sup>2) ((of_nat c)\<^sup>2)
[PROOF STEP]
by (subst multiplicity_times_unit_left) auto
[PROOF STATE]
proof (state)
this:
multiplicity (- \<i>\<^sub>\<int> * (1 + \<i>\<^sub>\<int>)\<^sup>2) ((of_nat c)\<^sup>2) = multiplicity ((1 + \<i>\<^sub>\<int>)\<^sup>2) ((of_nat c)\<^sup>2)

goal (2 subgoals):
 1. c = 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) (of_nat c) = 2 * multiplicity 2 c
 2. c \<noteq> 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) (of_nat c) = 2 * multiplicity 2 c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
multiplicity (- \<i>\<^sub>\<int> * (1 + \<i>\<^sub>\<int>)\<^sup>2) ((of_nat c)\<^sup>2) = multiplicity ((1 + \<i>\<^sub>\<int>)\<^sup>2) ((of_nat c)\<^sup>2)

goal (2 subgoals):
 1. c = 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) (of_nat c) = 2 * multiplicity 2 c
 2. c \<noteq> 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) (of_nat c) = 2 * multiplicity 2 c
[PROOF STEP]
have "\<dots> = multiplicity (1 + \<i>\<^sub>\<int>) (of_nat c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicity ((1 + \<i>\<^sub>\<int>)\<^sup>2) ((of_nat c)\<^sup>2) = multiplicity (1 + \<i>\<^sub>\<int>) (of_nat c)
[PROOF STEP]
by (subst multiplicity_power_power) auto
[PROOF STATE]
proof (state)
this:
multiplicity ((1 + \<i>\<^sub>\<int>)\<^sup>2) ((of_nat c)\<^sup>2) = multiplicity (1 + \<i>\<^sub>\<int>) (of_nat c)

goal (2 subgoals):
 1. c = 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) (of_nat c) = 2 * multiplicity 2 c
 2. c \<noteq> 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) (of_nat c) = 2 * multiplicity 2 c
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
2 * multiplicity 2 c = multiplicity (1 + \<i>\<^sub>\<int>) (of_nat c)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
2 * multiplicity 2 c = multiplicity (1 + \<i>\<^sub>\<int>) (of_nat c)

goal (1 subgoal):
 1. multiplicity (1 + \<i>\<^sub>\<int>) (of_nat c) = 2 * multiplicity 2 c
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
multiplicity (1 + \<i>\<^sub>\<int>) (of_nat c) = 2 * multiplicity 2 c

goal (1 subgoal):
 1. c = 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) (of_nat c) = 2 * multiplicity 2 c
[PROOF STEP]
qed auto


[STATEMENT]
lemma multiplicity_prime_cong_3_mod_4:
  assumes "prime (of_nat q :: gauss_int)"
  shows   "multiplicity q (gauss_int_norm z) = 2 * multiplicity (of_nat q) z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicity q (gauss_int_norm z) = 2 * multiplicity (of_nat q) z
[PROOF STEP]
proof (cases "z = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. z = 0 \<Longrightarrow> multiplicity q (gauss_int_norm z) = 2 * multiplicity (of_nat q) z
 2. z \<noteq> 0 \<Longrightarrow> multiplicity q (gauss_int_norm z) = 2 * multiplicity (of_nat q) z
[PROOF STEP]
case [simp]: False
[PROOF STATE]
proof (state)
this:
z \<noteq> 0

goal (2 subgoals):
 1. z = 0 \<Longrightarrow> multiplicity q (gauss_int_norm z) = 2 * multiplicity (of_nat q) z
 2. z \<noteq> 0 \<Longrightarrow> multiplicity q (gauss_int_norm z) = 2 * multiplicity (of_nat q) z
[PROOF STEP]
have "multiplicity q (gauss_int_norm z) =
          multiplicity (of_nat q) (of_nat (gauss_int_norm z) :: gauss_int)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicity q (gauss_int_norm z) = multiplicity (of_nat q) (of_nat (gauss_int_norm z))
[PROOF STEP]
by (simp add: multiplicity_gauss_int_of_nat)
[PROOF STATE]
proof (state)
this:
multiplicity q (gauss_int_norm z) = multiplicity (of_nat q) (of_nat (gauss_int_norm z))

goal (2 subgoals):
 1. z = 0 \<Longrightarrow> multiplicity q (gauss_int_norm z) = 2 * multiplicity (of_nat q) z
 2. z \<noteq> 0 \<Longrightarrow> multiplicity q (gauss_int_norm z) = 2 * multiplicity (of_nat q) z
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
multiplicity q (gauss_int_norm z) = multiplicity (of_nat q) (of_nat (gauss_int_norm z))

goal (2 subgoals):
 1. z = 0 \<Longrightarrow> multiplicity q (gauss_int_norm z) = 2 * multiplicity (of_nat q) z
 2. z \<noteq> 0 \<Longrightarrow> multiplicity q (gauss_int_norm z) = 2 * multiplicity (of_nat q) z
[PROOF STEP]
have "\<dots> = multiplicity (of_nat q) (z * gauss_cnj z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicity (of_nat q) (of_nat (gauss_int_norm z)) = multiplicity (of_nat q) (z * gauss_cnj z)
[PROOF STEP]
by (simp add: self_mult_gauss_cnj)
[PROOF STATE]
proof (state)
this:
multiplicity (of_nat q) (of_nat (gauss_int_norm z)) = multiplicity (of_nat q) (z * gauss_cnj z)

goal (2 subgoals):
 1. z = 0 \<Longrightarrow> multiplicity q (gauss_int_norm z) = 2 * multiplicity (of_nat q) z
 2. z \<noteq> 0 \<Longrightarrow> multiplicity q (gauss_int_norm z) = 2 * multiplicity (of_nat q) z
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
multiplicity (of_nat q) (of_nat (gauss_int_norm z)) = multiplicity (of_nat q) (z * gauss_cnj z)

goal (2 subgoals):
 1. z = 0 \<Longrightarrow> multiplicity q (gauss_int_norm z) = 2 * multiplicity (of_nat q) z
 2. z \<noteq> 0 \<Longrightarrow> multiplicity q (gauss_int_norm z) = 2 * multiplicity (of_nat q) z
[PROOF STEP]
have "\<dots> = multiplicity (of_nat q) z + multiplicity (gauss_cnj (of_nat q)) (gauss_cnj z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicity (of_nat q) (z * gauss_cnj z) = multiplicity (of_nat q) z + multiplicity (gauss_cnj (of_nat q)) (gauss_cnj z)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
prime (of_nat q)

goal (1 subgoal):
 1. multiplicity (of_nat q) (z * gauss_cnj z) = multiplicity (of_nat q) z + multiplicity (gauss_cnj (of_nat q)) (gauss_cnj z)
[PROOF STEP]
by (subst prime_elem_multiplicity_mult_distrib) auto
[PROOF STATE]
proof (state)
this:
multiplicity (of_nat q) (z * gauss_cnj z) = multiplicity (of_nat q) z + multiplicity (gauss_cnj (of_nat q)) (gauss_cnj z)

goal (2 subgoals):
 1. z = 0 \<Longrightarrow> multiplicity q (gauss_int_norm z) = 2 * multiplicity (of_nat q) z
 2. z \<noteq> 0 \<Longrightarrow> multiplicity q (gauss_int_norm z) = 2 * multiplicity (of_nat q) z
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
multiplicity (of_nat q) (z * gauss_cnj z) = multiplicity (of_nat q) z + multiplicity (gauss_cnj (of_nat q)) (gauss_cnj z)

goal (2 subgoals):
 1. z = 0 \<Longrightarrow> multiplicity q (gauss_int_norm z) = 2 * multiplicity (of_nat q) z
 2. z \<noteq> 0 \<Longrightarrow> multiplicity q (gauss_int_norm z) = 2 * multiplicity (of_nat q) z
[PROOF STEP]
have "multiplicity (gauss_cnj (of_nat q)) (gauss_cnj z) = multiplicity (of_nat q) z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicity (gauss_cnj (of_nat q)) (gauss_cnj z) = multiplicity (of_nat q) z
[PROOF STEP]
by (subst multiplicity_gauss_cnj) auto
[PROOF STATE]
proof (state)
this:
multiplicity (gauss_cnj (of_nat q)) (gauss_cnj z) = multiplicity (of_nat q) z

goal (2 subgoals):
 1. z = 0 \<Longrightarrow> multiplicity q (gauss_int_norm z) = 2 * multiplicity (of_nat q) z
 2. z \<noteq> 0 \<Longrightarrow> multiplicity q (gauss_int_norm z) = 2 * multiplicity (of_nat q) z
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
multiplicity (gauss_cnj (of_nat q)) (gauss_cnj z) = multiplicity (of_nat q) z

goal (2 subgoals):
 1. z = 0 \<Longrightarrow> multiplicity q (gauss_int_norm z) = 2 * multiplicity (of_nat q) z
 2. z \<noteq> 0 \<Longrightarrow> multiplicity q (gauss_int_norm z) = 2 * multiplicity (of_nat q) z
[PROOF STEP]
have "\<dots> + \<dots> = 2 * \<dots>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicity (of_nat q) z + multiplicity (of_nat q) z = 2 * multiplicity (of_nat q) z
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
multiplicity (of_nat q) z + multiplicity (of_nat q) z = 2 * multiplicity (of_nat q) z

goal (2 subgoals):
 1. z = 0 \<Longrightarrow> multiplicity q (gauss_int_norm z) = 2 * multiplicity (of_nat q) z
 2. z \<noteq> 0 \<Longrightarrow> multiplicity q (gauss_int_norm z) = 2 * multiplicity (of_nat q) z
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
multiplicity q (gauss_int_norm z) = 2 * multiplicity (of_nat q) z
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
multiplicity q (gauss_int_norm z) = 2 * multiplicity (of_nat q) z

goal (1 subgoal):
 1. multiplicity q (gauss_int_norm z) = 2 * multiplicity (of_nat q) z
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
multiplicity q (gauss_int_norm z) = 2 * multiplicity (of_nat q) z

goal (1 subgoal):
 1. z = 0 \<Longrightarrow> multiplicity q (gauss_int_norm z) = 2 * multiplicity (of_nat q) z
[PROOF STEP]
qed auto


[STATEMENT]
lemma multiplicity_prime_cong_1_mod_4_aux:
  fixes p :: gauss_int
  assumes "prime_elem p" "ReZ p > 0" "ImZ p > 0" "ImZ p \<noteq> ReZ p"
  shows "multiplicity p (of_nat c) = multiplicity (gauss_int_norm p) c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicity p (of_nat c) = multiplicity (gauss_int_norm p) c
[PROOF STEP]
proof (cases "c = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. c = 0 \<Longrightarrow> multiplicity p (of_nat c) = multiplicity (gauss_int_norm p) c
 2. c \<noteq> 0 \<Longrightarrow> multiplicity p (of_nat c) = multiplicity (gauss_int_norm p) c
[PROOF STEP]
case [simp]: False
[PROOF STATE]
proof (state)
this:
c \<noteq> 0

goal (2 subgoals):
 1. c = 0 \<Longrightarrow> multiplicity p (of_nat c) = multiplicity (gauss_int_norm p) c
 2. c \<noteq> 0 \<Longrightarrow> multiplicity p (of_nat c) = multiplicity (gauss_int_norm p) c
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicity p (of_nat c) = multiplicity (gauss_int_norm p) c
[PROOF STEP]
proof (intro antisym multiplicity_geI)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. c \<noteq> 0
 2. \<not> is_unit (gauss_int_norm p)
 3. gauss_int_norm p ^ multiplicity p (of_nat c) dvd c
 4. of_nat c \<noteq> 0
 5. \<not> is_unit p
 6. p ^ multiplicity (gauss_int_norm p) c dvd of_nat c
[PROOF STEP]
define k where "k = multiplicity p (of_nat c)"
[PROOF STATE]
proof (state)
this:
k = multiplicity p (of_nat c)

goal (6 subgoals):
 1. c \<noteq> 0
 2. \<not> is_unit (gauss_int_norm p)
 3. gauss_int_norm p ^ multiplicity p (of_nat c) dvd c
 4. of_nat c \<noteq> 0
 5. \<not> is_unit p
 6. p ^ multiplicity (gauss_int_norm p) c dvd of_nat c
[PROOF STEP]
have "p ^ k dvd of_nat c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p ^ k dvd of_nat c
[PROOF STEP]
by (simp add: multiplicity_dvd k_def)
[PROOF STATE]
proof (state)
this:
p ^ k dvd of_nat c

goal (6 subgoals):
 1. c \<noteq> 0
 2. \<not> is_unit (gauss_int_norm p)
 3. gauss_int_norm p ^ multiplicity p (of_nat c) dvd c
 4. of_nat c \<noteq> 0
 5. \<not> is_unit p
 6. p ^ multiplicity (gauss_int_norm p) c dvd of_nat c
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
p ^ k dvd of_nat c

goal (6 subgoals):
 1. c \<noteq> 0
 2. \<not> is_unit (gauss_int_norm p)
 3. gauss_int_norm p ^ multiplicity p (of_nat c) dvd c
 4. of_nat c \<noteq> 0
 5. \<not> is_unit p
 6. p ^ multiplicity (gauss_int_norm p) c dvd of_nat c
[PROOF STEP]
have "gauss_cnj p ^ k dvd of_nat c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gauss_cnj p ^ k dvd of_nat c
[PROOF STEP]
using multiplicity_dvd[of "gauss_cnj p" "of_nat c"]
            multiplicity_gauss_cnj[of p "of_nat c"]
[PROOF STATE]
proof (prove)
using this:
gauss_cnj p ^ multiplicity (gauss_cnj p) (of_nat c) dvd of_nat c
multiplicity (gauss_cnj p) (gauss_cnj (of_nat c)) = multiplicity p (of_nat c)

goal (1 subgoal):
 1. gauss_cnj p ^ k dvd of_nat c
[PROOF STEP]
by (simp add: k_def)
[PROOF STATE]
proof (state)
this:
gauss_cnj p ^ k dvd of_nat c

goal (6 subgoals):
 1. c \<noteq> 0
 2. \<not> is_unit (gauss_int_norm p)
 3. gauss_int_norm p ^ multiplicity p (of_nat c) dvd c
 4. of_nat c \<noteq> 0
 5. \<not> is_unit p
 6. p ^ multiplicity (gauss_int_norm p) c dvd of_nat c
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
gauss_cnj p ^ k dvd of_nat c

goal (6 subgoals):
 1. c \<noteq> 0
 2. \<not> is_unit (gauss_int_norm p)
 3. gauss_int_norm p ^ multiplicity p (of_nat c) dvd c
 4. of_nat c \<noteq> 0
 5. \<not> is_unit p
 6. p ^ multiplicity (gauss_int_norm p) c dvd of_nat c
[PROOF STEP]
have "\<not>p dvd gauss_cnj p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> p dvd gauss_cnj p
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
prime_elem p
0 < ReZ p
0 < ImZ p
ImZ p \<noteq> ReZ p

goal (1 subgoal):
 1. \<not> p dvd gauss_cnj p
[PROOF STEP]
by (subst self_dvd_gauss_cnj_iff) auto
[PROOF STATE]
proof (state)
this:
\<not> p dvd gauss_cnj p

goal (6 subgoals):
 1. c \<noteq> 0
 2. \<not> is_unit (gauss_int_norm p)
 3. gauss_int_norm p ^ multiplicity p (of_nat c) dvd c
 4. of_nat c \<noteq> 0
 5. \<not> is_unit p
 6. p ^ multiplicity (gauss_int_norm p) c dvd of_nat c
[PROOF STEP]
hence "\<not>p dvd gauss_cnj p ^ k"
[PROOF STATE]
proof (prove)
using this:
\<not> p dvd gauss_cnj p

goal (1 subgoal):
 1. \<not> p dvd gauss_cnj p ^ k
[PROOF STEP]
using assms prime_elem_dvd_power
[PROOF STATE]
proof (prove)
using this:
\<not> p dvd gauss_cnj p
prime_elem p
0 < ReZ p
0 < ImZ p
ImZ p \<noteq> ReZ p
\<lbrakk>prime_elem ?p; ?p dvd ?x ^ ?n\<rbrakk> \<Longrightarrow> ?p dvd ?x

goal (1 subgoal):
 1. \<not> p dvd gauss_cnj p ^ k
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> p dvd gauss_cnj p ^ k

goal (6 subgoals):
 1. c \<noteq> 0
 2. \<not> is_unit (gauss_int_norm p)
 3. gauss_int_norm p ^ multiplicity p (of_nat c) dvd c
 4. of_nat c \<noteq> 0
 5. \<not> is_unit p
 6. p ^ multiplicity (gauss_int_norm p) c dvd of_nat c
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
p ^ k dvd of_nat c
gauss_cnj p ^ k dvd of_nat c
\<not> p dvd gauss_cnj p ^ k
[PROOF STEP]
have "p ^ k * gauss_cnj p ^ k dvd of_nat c"
[PROOF STATE]
proof (prove)
using this:
p ^ k dvd of_nat c
gauss_cnj p ^ k dvd of_nat c
\<not> p dvd gauss_cnj p ^ k

goal (1 subgoal):
 1. p ^ k * gauss_cnj p ^ k dvd of_nat c
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
p ^ k dvd of_nat c
gauss_cnj p ^ k dvd of_nat c
\<not> p dvd gauss_cnj p ^ k
prime_elem p
0 < ReZ p
0 < ImZ p
ImZ p \<noteq> ReZ p

goal (1 subgoal):
 1. p ^ k * gauss_cnj p ^ k dvd of_nat c
[PROOF STEP]
by (intro prime_elem_power_mult_dvdI) auto
[PROOF STATE]
proof (state)
this:
p ^ k * gauss_cnj p ^ k dvd of_nat c

goal (6 subgoals):
 1. c \<noteq> 0
 2. \<not> is_unit (gauss_int_norm p)
 3. gauss_int_norm p ^ multiplicity p (of_nat c) dvd c
 4. of_nat c \<noteq> 0
 5. \<not> is_unit p
 6. p ^ multiplicity (gauss_int_norm p) c dvd of_nat c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
p ^ k * gauss_cnj p ^ k dvd of_nat c

goal (6 subgoals):
 1. c \<noteq> 0
 2. \<not> is_unit (gauss_int_norm p)
 3. gauss_int_norm p ^ multiplicity p (of_nat c) dvd c
 4. of_nat c \<noteq> 0
 5. \<not> is_unit p
 6. p ^ multiplicity (gauss_int_norm p) c dvd of_nat c
[PROOF STEP]
have "p ^ k * gauss_cnj p ^ k = of_nat (gauss_int_norm p ^ k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p ^ k * gauss_cnj p ^ k = of_nat (gauss_int_norm p ^ k)
[PROOF STEP]
by (simp flip: self_mult_gauss_cnj add: power_mult_distrib)
[PROOF STATE]
proof (state)
this:
p ^ k * gauss_cnj p ^ k = of_nat (gauss_int_norm p ^ k)

goal (6 subgoals):
 1. c \<noteq> 0
 2. \<not> is_unit (gauss_int_norm p)
 3. gauss_int_norm p ^ multiplicity p (of_nat c) dvd c
 4. of_nat c \<noteq> 0
 5. \<not> is_unit p
 6. p ^ multiplicity (gauss_int_norm p) c dvd of_nat c
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
of_nat (gauss_int_norm p ^ k) dvd of_nat c
[PROOF STEP]
show "gauss_int_norm p ^ k dvd c"
[PROOF STATE]
proof (prove)
using this:
of_nat (gauss_int_norm p ^ k) dvd of_nat c

goal (1 subgoal):
 1. gauss_int_norm p ^ k dvd c
[PROOF STEP]
by (subst (asm) of_nat_dvd_of_nat_gauss_int_iff)
[PROOF STATE]
proof (state)
this:
gauss_int_norm p ^ k dvd c

goal (5 subgoals):
 1. c \<noteq> 0
 2. \<not> is_unit (gauss_int_norm p)
 3. of_nat c \<noteq> 0
 4. \<not> is_unit p
 5. p ^ multiplicity (gauss_int_norm p) c dvd of_nat c
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. c \<noteq> 0
 2. \<not> is_unit (gauss_int_norm p)
 3. of_nat c \<noteq> 0
 4. \<not> is_unit p
 5. p ^ multiplicity (gauss_int_norm p) c dvd of_nat c
[PROOF STEP]
define k where "k = multiplicity (gauss_int_norm p) c"
[PROOF STATE]
proof (state)
this:
k = multiplicity (gauss_int_norm p) c

goal (5 subgoals):
 1. c \<noteq> 0
 2. \<not> is_unit (gauss_int_norm p)
 3. of_nat c \<noteq> 0
 4. \<not> is_unit p
 5. p ^ multiplicity (gauss_int_norm p) c dvd of_nat c
[PROOF STEP]
have "p ^ k dvd (p * gauss_cnj p) ^ k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p ^ k dvd (p * gauss_cnj p) ^ k
[PROOF STEP]
by (intro dvd_power_same) auto
[PROOF STATE]
proof (state)
this:
p ^ k dvd (p * gauss_cnj p) ^ k

goal (5 subgoals):
 1. c \<noteq> 0
 2. \<not> is_unit (gauss_int_norm p)
 3. of_nat c \<noteq> 0
 4. \<not> is_unit p
 5. p ^ multiplicity (gauss_int_norm p) c dvd of_nat c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
p ^ k dvd (p * gauss_cnj p) ^ k

goal (5 subgoals):
 1. c \<noteq> 0
 2. \<not> is_unit (gauss_int_norm p)
 3. of_nat c \<noteq> 0
 4. \<not> is_unit p
 5. p ^ multiplicity (gauss_int_norm p) c dvd of_nat c
[PROOF STEP]
have "\<dots> = of_nat (gauss_int_norm p ^ k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p * gauss_cnj p) ^ k = of_nat (gauss_int_norm p ^ k)
[PROOF STEP]
by (simp add: self_mult_gauss_cnj)
[PROOF STATE]
proof (state)
this:
(p * gauss_cnj p) ^ k = of_nat (gauss_int_norm p ^ k)

goal (5 subgoals):
 1. c \<noteq> 0
 2. \<not> is_unit (gauss_int_norm p)
 3. of_nat c \<noteq> 0
 4. \<not> is_unit p
 5. p ^ multiplicity (gauss_int_norm p) c dvd of_nat c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(p * gauss_cnj p) ^ k = of_nat (gauss_int_norm p ^ k)

goal (5 subgoals):
 1. c \<noteq> 0
 2. \<not> is_unit (gauss_int_norm p)
 3. of_nat c \<noteq> 0
 4. \<not> is_unit p
 5. p ^ multiplicity (gauss_int_norm p) c dvd of_nat c
[PROOF STEP]
have "\<dots> dvd of_nat c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_nat (gauss_int_norm p ^ k) dvd of_nat c
[PROOF STEP]
unfolding of_nat_dvd_of_nat_gauss_int_iff
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gauss_int_norm p ^ k dvd c
[PROOF STEP]
by (auto simp: k_def multiplicity_dvd)
[PROOF STATE]
proof (state)
this:
of_nat (gauss_int_norm p ^ k) dvd of_nat c

goal (5 subgoals):
 1. c \<noteq> 0
 2. \<not> is_unit (gauss_int_norm p)
 3. of_nat c \<noteq> 0
 4. \<not> is_unit p
 5. p ^ multiplicity (gauss_int_norm p) c dvd of_nat c
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
p ^ k dvd of_nat c
[PROOF STEP]
show "p ^ k dvd of_nat c"
[PROOF STATE]
proof (prove)
using this:
p ^ k dvd of_nat c

goal (1 subgoal):
 1. p ^ k dvd of_nat c
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
p ^ k dvd of_nat c

goal (4 subgoals):
 1. c \<noteq> 0
 2. \<not> is_unit (gauss_int_norm p)
 3. of_nat c \<noteq> 0
 4. \<not> is_unit p
[PROOF STEP]
qed (use assms in \<open>auto simp: gauss_int_norm_eq_Suc_0_iff\<close>)
[PROOF STATE]
proof (state)
this:
multiplicity p (of_nat c) = multiplicity (gauss_int_norm p) c

goal (1 subgoal):
 1. c = 0 \<Longrightarrow> multiplicity p (of_nat c) = multiplicity (gauss_int_norm p) c
[PROOF STEP]
qed auto


[STATEMENT]
lemma multiplicity_prime_cong_1_mod_4:
  fixes p :: gauss_int
  assumes "prime_elem p" "ReZ p > 0" "ImZ p > 0" "ImZ p \<noteq> ReZ p"
  shows "multiplicity (gauss_int_norm p) (gauss_int_norm z) =
           multiplicity p z + multiplicity (gauss_cnj p) z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicity (gauss_int_norm p) (gauss_int_norm z) = multiplicity p z + multiplicity (gauss_cnj p) z
[PROOF STEP]
proof (cases "z = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. z = 0 \<Longrightarrow> multiplicity (gauss_int_norm p) (gauss_int_norm z) = multiplicity p z + multiplicity (gauss_cnj p) z
 2. z \<noteq> 0 \<Longrightarrow> multiplicity (gauss_int_norm p) (gauss_int_norm z) = multiplicity p z + multiplicity (gauss_cnj p) z
[PROOF STEP]
case [simp]: False
[PROOF STATE]
proof (state)
this:
z \<noteq> 0

goal (2 subgoals):
 1. z = 0 \<Longrightarrow> multiplicity (gauss_int_norm p) (gauss_int_norm z) = multiplicity p z + multiplicity (gauss_cnj p) z
 2. z \<noteq> 0 \<Longrightarrow> multiplicity (gauss_int_norm p) (gauss_int_norm z) = multiplicity p z + multiplicity (gauss_cnj p) z
[PROOF STEP]
have "multiplicity (gauss_int_norm p) (gauss_int_norm z) =
          multiplicity p (of_nat (gauss_int_norm z))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicity (gauss_int_norm p) (gauss_int_norm z) = multiplicity p (of_nat (gauss_int_norm z))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
prime_elem p
0 < ReZ p
0 < ImZ p
ImZ p \<noteq> ReZ p

goal (1 subgoal):
 1. multiplicity (gauss_int_norm p) (gauss_int_norm z) = multiplicity p (of_nat (gauss_int_norm z))
[PROOF STEP]
by (subst multiplicity_prime_cong_1_mod_4_aux) auto
[PROOF STATE]
proof (state)
this:
multiplicity (gauss_int_norm p) (gauss_int_norm z) = multiplicity p (of_nat (gauss_int_norm z))

goal (2 subgoals):
 1. z = 0 \<Longrightarrow> multiplicity (gauss_int_norm p) (gauss_int_norm z) = multiplicity p z + multiplicity (gauss_cnj p) z
 2. z \<noteq> 0 \<Longrightarrow> multiplicity (gauss_int_norm p) (gauss_int_norm z) = multiplicity p z + multiplicity (gauss_cnj p) z
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
multiplicity (gauss_int_norm p) (gauss_int_norm z) = multiplicity p (of_nat (gauss_int_norm z))

goal (2 subgoals):
 1. z = 0 \<Longrightarrow> multiplicity (gauss_int_norm p) (gauss_int_norm z) = multiplicity p z + multiplicity (gauss_cnj p) z
 2. z \<noteq> 0 \<Longrightarrow> multiplicity (gauss_int_norm p) (gauss_int_norm z) = multiplicity p z + multiplicity (gauss_cnj p) z
[PROOF STEP]
have "\<dots> = multiplicity p (z * gauss_cnj z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicity p (of_nat (gauss_int_norm z)) = multiplicity p (z * gauss_cnj z)
[PROOF STEP]
by (simp add: self_mult_gauss_cnj)
[PROOF STATE]
proof (state)
this:
multiplicity p (of_nat (gauss_int_norm z)) = multiplicity p (z * gauss_cnj z)

goal (2 subgoals):
 1. z = 0 \<Longrightarrow> multiplicity (gauss_int_norm p) (gauss_int_norm z) = multiplicity p z + multiplicity (gauss_cnj p) z
 2. z \<noteq> 0 \<Longrightarrow> multiplicity (gauss_int_norm p) (gauss_int_norm z) = multiplicity p z + multiplicity (gauss_cnj p) z
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
multiplicity p (of_nat (gauss_int_norm z)) = multiplicity p (z * gauss_cnj z)

goal (2 subgoals):
 1. z = 0 \<Longrightarrow> multiplicity (gauss_int_norm p) (gauss_int_norm z) = multiplicity p z + multiplicity (gauss_cnj p) z
 2. z \<noteq> 0 \<Longrightarrow> multiplicity (gauss_int_norm p) (gauss_int_norm z) = multiplicity p z + multiplicity (gauss_cnj p) z
[PROOF STEP]
have "\<dots> = multiplicity p z + multiplicity p (gauss_cnj z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicity p (z * gauss_cnj z) = multiplicity p z + multiplicity p (gauss_cnj z)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
prime_elem p
0 < ReZ p
0 < ImZ p
ImZ p \<noteq> ReZ p

goal (1 subgoal):
 1. multiplicity p (z * gauss_cnj z) = multiplicity p z + multiplicity p (gauss_cnj z)
[PROOF STEP]
by (subst prime_elem_multiplicity_mult_distrib) auto
[PROOF STATE]
proof (state)
this:
multiplicity p (z * gauss_cnj z) = multiplicity p z + multiplicity p (gauss_cnj z)

goal (2 subgoals):
 1. z = 0 \<Longrightarrow> multiplicity (gauss_int_norm p) (gauss_int_norm z) = multiplicity p z + multiplicity (gauss_cnj p) z
 2. z \<noteq> 0 \<Longrightarrow> multiplicity (gauss_int_norm p) (gauss_int_norm z) = multiplicity p z + multiplicity (gauss_cnj p) z
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
multiplicity p (z * gauss_cnj z) = multiplicity p z + multiplicity p (gauss_cnj z)

goal (2 subgoals):
 1. z = 0 \<Longrightarrow> multiplicity (gauss_int_norm p) (gauss_int_norm z) = multiplicity p z + multiplicity (gauss_cnj p) z
 2. z \<noteq> 0 \<Longrightarrow> multiplicity (gauss_int_norm p) (gauss_int_norm z) = multiplicity p z + multiplicity (gauss_cnj p) z
[PROOF STEP]
have "multiplicity p (gauss_cnj z) = multiplicity (gauss_cnj p) z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicity p (gauss_cnj z) = multiplicity (gauss_cnj p) z
[PROOF STEP]
by (subst multiplicity_gauss_cnj [symmetric]) auto
[PROOF STATE]
proof (state)
this:
multiplicity p (gauss_cnj z) = multiplicity (gauss_cnj p) z

goal (2 subgoals):
 1. z = 0 \<Longrightarrow> multiplicity (gauss_int_norm p) (gauss_int_norm z) = multiplicity p z + multiplicity (gauss_cnj p) z
 2. z \<noteq> 0 \<Longrightarrow> multiplicity (gauss_int_norm p) (gauss_int_norm z) = multiplicity p z + multiplicity (gauss_cnj p) z
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
multiplicity (gauss_int_norm p) (gauss_int_norm z) = multiplicity p z + multiplicity (gauss_cnj p) z
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
multiplicity (gauss_int_norm p) (gauss_int_norm z) = multiplicity p z + multiplicity (gauss_cnj p) z

goal (1 subgoal):
 1. multiplicity (gauss_int_norm p) (gauss_int_norm z) = multiplicity p z + multiplicity (gauss_cnj p) z
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
multiplicity (gauss_int_norm p) (gauss_int_norm z) = multiplicity p z + multiplicity (gauss_cnj p) z

goal (1 subgoal):
 1. z = 0 \<Longrightarrow> multiplicity (gauss_int_norm p) (gauss_int_norm z) = multiplicity p z + multiplicity (gauss_cnj p) z
[PROOF STEP]
qed auto


[STATEMENT]
lemma multiplicity_prime_1_plus_i: "multiplicity (1 + \<i>\<^sub>\<int>) z = multiplicity 2 (gauss_int_norm z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicity (1 + \<i>\<^sub>\<int>) z = multiplicity 2 (gauss_int_norm z)
[PROOF STEP]
proof (cases "z = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. z = 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) z = multiplicity 2 (gauss_int_norm z)
 2. z \<noteq> 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) z = multiplicity 2 (gauss_int_norm z)
[PROOF STEP]
case [simp]: False
[PROOF STATE]
proof (state)
this:
z \<noteq> 0

goal (2 subgoals):
 1. z = 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) z = multiplicity 2 (gauss_int_norm z)
 2. z \<noteq> 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) z = multiplicity 2 (gauss_int_norm z)
[PROOF STEP]
note [simp] = prime_elem_one_plus_i_gauss_int
[PROOF STATE]
proof (state)
this:
prime_elem (1 + \<i>\<^sub>\<int>)

goal (2 subgoals):
 1. z = 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) z = multiplicity 2 (gauss_int_norm z)
 2. z \<noteq> 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) z = multiplicity 2 (gauss_int_norm z)
[PROOF STEP]
have "2 * multiplicity 2 (gauss_int_norm z) = multiplicity (1 + \<i>\<^sub>\<int>) (of_nat (gauss_int_norm z))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * multiplicity 2 (gauss_int_norm z) = multiplicity (1 + \<i>\<^sub>\<int>) (of_nat (gauss_int_norm z))
[PROOF STEP]
by (rule multiplicity_prime_1_plus_i_aux [symmetric])
[PROOF STATE]
proof (state)
this:
2 * multiplicity 2 (gauss_int_norm z) = multiplicity (1 + \<i>\<^sub>\<int>) (of_nat (gauss_int_norm z))

goal (2 subgoals):
 1. z = 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) z = multiplicity 2 (gauss_int_norm z)
 2. z \<noteq> 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) z = multiplicity 2 (gauss_int_norm z)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
2 * multiplicity 2 (gauss_int_norm z) = multiplicity (1 + \<i>\<^sub>\<int>) (of_nat (gauss_int_norm z))

goal (2 subgoals):
 1. z = 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) z = multiplicity 2 (gauss_int_norm z)
 2. z \<noteq> 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) z = multiplicity 2 (gauss_int_norm z)
[PROOF STEP]
have "\<dots> = multiplicity (1 + \<i>\<^sub>\<int>) (z * gauss_cnj z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicity (1 + \<i>\<^sub>\<int>) (of_nat (gauss_int_norm z)) = multiplicity (1 + \<i>\<^sub>\<int>) (z * gauss_cnj z)
[PROOF STEP]
by (simp add: self_mult_gauss_cnj)
[PROOF STATE]
proof (state)
this:
multiplicity (1 + \<i>\<^sub>\<int>) (of_nat (gauss_int_norm z)) = multiplicity (1 + \<i>\<^sub>\<int>) (z * gauss_cnj z)

goal (2 subgoals):
 1. z = 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) z = multiplicity 2 (gauss_int_norm z)
 2. z \<noteq> 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) z = multiplicity 2 (gauss_int_norm z)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
multiplicity (1 + \<i>\<^sub>\<int>) (of_nat (gauss_int_norm z)) = multiplicity (1 + \<i>\<^sub>\<int>) (z * gauss_cnj z)

goal (2 subgoals):
 1. z = 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) z = multiplicity 2 (gauss_int_norm z)
 2. z \<noteq> 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) z = multiplicity 2 (gauss_int_norm z)
[PROOF STEP]
have "\<dots> = multiplicity (1 + \<i>\<^sub>\<int>) z + multiplicity (gauss_cnj (1 - \<i>\<^sub>\<int>)) (gauss_cnj z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicity (1 + \<i>\<^sub>\<int>) (z * gauss_cnj z) = multiplicity (1 + \<i>\<^sub>\<int>) z + multiplicity (gauss_cnj (1 - \<i>\<^sub>\<int>)) (gauss_cnj z)
[PROOF STEP]
by (subst prime_elem_multiplicity_mult_distrib) auto
[PROOF STATE]
proof (state)
this:
multiplicity (1 + \<i>\<^sub>\<int>) (z * gauss_cnj z) = multiplicity (1 + \<i>\<^sub>\<int>) z + multiplicity (gauss_cnj (1 - \<i>\<^sub>\<int>)) (gauss_cnj z)

goal (2 subgoals):
 1. z = 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) z = multiplicity 2 (gauss_int_norm z)
 2. z \<noteq> 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) z = multiplicity 2 (gauss_int_norm z)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
multiplicity (1 + \<i>\<^sub>\<int>) (z * gauss_cnj z) = multiplicity (1 + \<i>\<^sub>\<int>) z + multiplicity (gauss_cnj (1 - \<i>\<^sub>\<int>)) (gauss_cnj z)

goal (2 subgoals):
 1. z = 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) z = multiplicity 2 (gauss_int_norm z)
 2. z \<noteq> 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) z = multiplicity 2 (gauss_int_norm z)
[PROOF STEP]
have "multiplicity (gauss_cnj (1 - \<i>\<^sub>\<int>)) (gauss_cnj z) = multiplicity (1 - \<i>\<^sub>\<int>) z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicity (gauss_cnj (1 - \<i>\<^sub>\<int>)) (gauss_cnj z) = multiplicity (1 - \<i>\<^sub>\<int>) z
[PROOF STEP]
by (subst multiplicity_gauss_cnj) auto
[PROOF STATE]
proof (state)
this:
multiplicity (gauss_cnj (1 - \<i>\<^sub>\<int>)) (gauss_cnj z) = multiplicity (1 - \<i>\<^sub>\<int>) z

goal (2 subgoals):
 1. z = 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) z = multiplicity 2 (gauss_int_norm z)
 2. z \<noteq> 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) z = multiplicity 2 (gauss_int_norm z)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
multiplicity (gauss_cnj (1 - \<i>\<^sub>\<int>)) (gauss_cnj z) = multiplicity (1 - \<i>\<^sub>\<int>) z

goal (2 subgoals):
 1. z = 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) z = multiplicity 2 (gauss_int_norm z)
 2. z \<noteq> 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) z = multiplicity 2 (gauss_int_norm z)
[PROOF STEP]
have "1 - \<i>\<^sub>\<int> = (-\<i>\<^sub>\<int>) * (1 + \<i>\<^sub>\<int>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 - \<i>\<^sub>\<int> = - \<i>\<^sub>\<int> * (1 + \<i>\<^sub>\<int>)
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
1 - \<i>\<^sub>\<int> = - \<i>\<^sub>\<int> * (1 + \<i>\<^sub>\<int>)

goal (2 subgoals):
 1. z = 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) z = multiplicity 2 (gauss_int_norm z)
 2. z \<noteq> 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) z = multiplicity 2 (gauss_int_norm z)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
1 - \<i>\<^sub>\<int> = - \<i>\<^sub>\<int> * (1 + \<i>\<^sub>\<int>)

goal (2 subgoals):
 1. z = 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) z = multiplicity 2 (gauss_int_norm z)
 2. z \<noteq> 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) z = multiplicity 2 (gauss_int_norm z)
[PROOF STEP]
have "multiplicity \<dots> z = multiplicity (1 + \<i>\<^sub>\<int>) z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicity (- \<i>\<^sub>\<int> * (1 + \<i>\<^sub>\<int>)) z = multiplicity (1 + \<i>\<^sub>\<int>) z
[PROOF STEP]
by (subst multiplicity_times_unit_left) auto
[PROOF STATE]
proof (state)
this:
multiplicity (- \<i>\<^sub>\<int> * (1 + \<i>\<^sub>\<int>)) z = multiplicity (1 + \<i>\<^sub>\<int>) z

goal (2 subgoals):
 1. z = 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) z = multiplicity 2 (gauss_int_norm z)
 2. z \<noteq> 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) z = multiplicity 2 (gauss_int_norm z)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
multiplicity (- \<i>\<^sub>\<int> * (1 + \<i>\<^sub>\<int>)) z = multiplicity (1 + \<i>\<^sub>\<int>) z

goal (2 subgoals):
 1. z = 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) z = multiplicity 2 (gauss_int_norm z)
 2. z \<noteq> 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) z = multiplicity 2 (gauss_int_norm z)
[PROOF STEP]
have "\<dots> + \<dots> = 2 * \<dots>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicity (1 + \<i>\<^sub>\<int>) z + multiplicity (1 + \<i>\<^sub>\<int>) z = 2 * multiplicity (1 + \<i>\<^sub>\<int>) z
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
multiplicity (1 + \<i>\<^sub>\<int>) z + multiplicity (1 + \<i>\<^sub>\<int>) z = 2 * multiplicity (1 + \<i>\<^sub>\<int>) z

goal (2 subgoals):
 1. z = 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) z = multiplicity 2 (gauss_int_norm z)
 2. z \<noteq> 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) z = multiplicity 2 (gauss_int_norm z)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
2 * multiplicity 2 (gauss_int_norm z) = 2 * multiplicity (1 + \<i>\<^sub>\<int>) z
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
2 * multiplicity 2 (gauss_int_norm z) = 2 * multiplicity (1 + \<i>\<^sub>\<int>) z

goal (1 subgoal):
 1. multiplicity (1 + \<i>\<^sub>\<int>) z = multiplicity 2 (gauss_int_norm z)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
multiplicity (1 + \<i>\<^sub>\<int>) z = multiplicity 2 (gauss_int_norm z)

goal (1 subgoal):
 1. z = 0 \<Longrightarrow> multiplicity (1 + \<i>\<^sub>\<int>) z = multiplicity 2 (gauss_int_norm z)
[PROOF STEP]
qed auto


[STATEMENT]
lemma coprime_self_gauss_cnj:
  assumes "coprime (ReZ z) (ImZ z)" and "odd (gauss_int_norm z)"
  shows   "coprime z (gauss_cnj z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coprime z (gauss_cnj z)
[PROOF STEP]
proof (rule coprimeI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>c. \<lbrakk>c dvd z; c dvd gauss_cnj z\<rbrakk> \<Longrightarrow> is_unit c
[PROOF STEP]
fix d
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>c. \<lbrakk>c dvd z; c dvd gauss_cnj z\<rbrakk> \<Longrightarrow> is_unit c
[PROOF STEP]
assume "d dvd z" "d dvd gauss_cnj z"
[PROOF STATE]
proof (state)
this:
d dvd z
d dvd gauss_cnj z

goal (1 subgoal):
 1. \<And>c. \<lbrakk>c dvd z; c dvd gauss_cnj z\<rbrakk> \<Longrightarrow> is_unit c
[PROOF STEP]
have *: False if "p \<in> prime_factors z" "p \<in> prime_factors (gauss_cnj z)" for p
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. False
[PROOF STEP]
from that
[PROOF STATE]
proof (chain)
picking this:
p \<in># prime_factorization z
p \<in># prime_factorization (gauss_cnj z)
[PROOF STEP]
have p: "prime p" "p dvd z" "p dvd gauss_cnj z"
[PROOF STATE]
proof (prove)
using this:
p \<in># prime_factorization z
p \<in># prime_factorization (gauss_cnj z)

goal (1 subgoal):
 1. prime p &&& p dvd z &&& p dvd gauss_cnj z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
prime p
p dvd z
p dvd gauss_cnj z

goal (1 subgoal):
 1. False
[PROOF STEP]
define p' where "p' = gauss_cnj p"
[PROOF STATE]
proof (state)
this:
p' = gauss_cnj p

goal (1 subgoal):
 1. False
[PROOF STEP]
define d where "d = gauss_int_norm p"
[PROOF STATE]
proof (state)
this:
d = gauss_int_norm p

goal (1 subgoal):
 1. False
[PROOF STEP]
have of_nat_d_eq: "of_nat d = p * p'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_nat d = p * p'
[PROOF STEP]
by (simp add: p'_def self_mult_gauss_cnj d_def)
[PROOF STATE]
proof (state)
this:
of_nat d = p * p'

goal (1 subgoal):
 1. False
[PROOF STEP]
have "prime_elem p" "prime_elem p'" "p dvd z" "p' dvd z" "p dvd gauss_cnj z" "p' dvd gauss_cnj z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (prime_elem p &&& prime_elem p' &&& p dvd z) &&& p' dvd z &&& p dvd gauss_cnj z &&& p' dvd gauss_cnj z
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
p \<in># prime_factorization z
p \<in># prime_factorization (gauss_cnj z)

goal (1 subgoal):
 1. (prime_elem p &&& prime_elem p' &&& p dvd z) &&& p' dvd z &&& p dvd gauss_cnj z &&& p' dvd gauss_cnj z
[PROOF STEP]
by (auto simp: in_prime_factors_iff p'_def gauss_cnj_dvd_left_iff)
[PROOF STATE]
proof (state)
this:
prime_elem p
prime_elem p'
p dvd z
p' dvd z
p dvd gauss_cnj z
p' dvd gauss_cnj z

goal (1 subgoal):
 1. False
[PROOF STEP]
have "prime p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime p
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
p \<in># prime_factorization z
p \<in># prime_factorization (gauss_cnj z)

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

goal (1 subgoal):
 1. False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
prime p
[PROOF STEP]
obtain q where q: "prime q" "of_nat q dvd z"
[PROOF STATE]
proof (prove)
using this:
prime p

goal (1 subgoal):
 1. (\<And>q. \<lbrakk>prime q; of_nat q dvd z\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof (cases rule: gauss_int_prime_classification)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrakk>\<And>q. \<lbrakk>prime q; of_nat q dvd z\<rbrakk> \<Longrightarrow> thesis; p = 1 + \<i>\<^sub>\<int>\<rbrakk> \<Longrightarrow> thesis
 2. \<And>pa. \<lbrakk>\<And>q. \<lbrakk>prime q; of_nat q dvd z\<rbrakk> \<Longrightarrow> thesis; p = of_nat pa; prime pa; [pa = 3] (mod 4)\<rbrakk> \<Longrightarrow> thesis
 3. \<lbrakk>\<And>q. \<lbrakk>prime q; of_nat q dvd z\<rbrakk> \<Longrightarrow> thesis; prime (gauss_int_norm p); [gauss_int_norm p = 1] (mod 4); 0 < ReZ p; 0 < ImZ p; ReZ p \<noteq> ImZ p\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case one_plus_i
[PROOF STATE]
proof (state)
this:
p = 1 + \<i>\<^sub>\<int>

goal (3 subgoals):
 1. \<lbrakk>\<And>q. \<lbrakk>prime q; of_nat q dvd z\<rbrakk> \<Longrightarrow> thesis; p = 1 + \<i>\<^sub>\<int>\<rbrakk> \<Longrightarrow> thesis
 2. \<And>pa. \<lbrakk>\<And>q. \<lbrakk>prime q; of_nat q dvd z\<rbrakk> \<Longrightarrow> thesis; p = of_nat pa; prime pa; [pa = 3] (mod 4)\<rbrakk> \<Longrightarrow> thesis
 3. \<lbrakk>\<And>q. \<lbrakk>prime q; of_nat q dvd z\<rbrakk> \<Longrightarrow> thesis; prime (gauss_int_norm p); [gauss_int_norm p = 1] (mod 4); 0 < ReZ p; 0 < ImZ p; ReZ p \<noteq> ImZ p\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
hence "2 = gauss_int_norm p"
[PROOF STATE]
proof (prove)
using this:
p = 1 + \<i>\<^sub>\<int>

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

goal (3 subgoals):
 1. \<lbrakk>\<And>q. \<lbrakk>prime q; of_nat q dvd z\<rbrakk> \<Longrightarrow> thesis; p = 1 + \<i>\<^sub>\<int>\<rbrakk> \<Longrightarrow> thesis
 2. \<And>pa. \<lbrakk>\<And>q. \<lbrakk>prime q; of_nat q dvd z\<rbrakk> \<Longrightarrow> thesis; p = of_nat pa; prime pa; [pa = 3] (mod 4)\<rbrakk> \<Longrightarrow> thesis
 3. \<lbrakk>\<And>q. \<lbrakk>prime q; of_nat q dvd z\<rbrakk> \<Longrightarrow> thesis; prime (gauss_int_norm p); [gauss_int_norm p = 1] (mod 4); 0 < ReZ p; 0 < ImZ p; ReZ p \<noteq> ImZ p\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
2 = gauss_int_norm p

goal (3 subgoals):
 1. \<lbrakk>\<And>q. \<lbrakk>prime q; of_nat q dvd z\<rbrakk> \<Longrightarrow> thesis; p = 1 + \<i>\<^sub>\<int>\<rbrakk> \<Longrightarrow> thesis
 2. \<And>pa. \<lbrakk>\<And>q. \<lbrakk>prime q; of_nat q dvd z\<rbrakk> \<Longrightarrow> thesis; p = of_nat pa; prime pa; [pa = 3] (mod 4)\<rbrakk> \<Longrightarrow> thesis
 3. \<lbrakk>\<And>q. \<lbrakk>prime q; of_nat q dvd z\<rbrakk> \<Longrightarrow> thesis; prime (gauss_int_norm p); [gauss_int_norm p = 1] (mod 4); 0 < ReZ p; 0 < ImZ p; ReZ p \<noteq> ImZ p\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have "gauss_int_norm p dvd gauss_int_norm z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gauss_int_norm p dvd gauss_int_norm z
[PROOF STEP]
using p
[PROOF STATE]
proof (prove)
using this:
prime p
p dvd z
p dvd gauss_cnj z

goal (1 subgoal):
 1. gauss_int_norm p dvd gauss_int_norm z
[PROOF STEP]
by (intro gauss_int_norm_dvd_mono) auto
[PROOF STATE]
proof (state)
this:
gauss_int_norm p dvd gauss_int_norm z

goal (3 subgoals):
 1. \<lbrakk>\<And>q. \<lbrakk>prime q; of_nat q dvd z\<rbrakk> \<Longrightarrow> thesis; p = 1 + \<i>\<^sub>\<int>\<rbrakk> \<Longrightarrow> thesis
 2. \<And>pa. \<lbrakk>\<And>q. \<lbrakk>prime q; of_nat q dvd z\<rbrakk> \<Longrightarrow> thesis; p = of_nat pa; prime pa; [pa = 3] (mod 4)\<rbrakk> \<Longrightarrow> thesis
 3. \<lbrakk>\<And>q. \<lbrakk>prime q; of_nat q dvd z\<rbrakk> \<Longrightarrow> thesis; prime (gauss_int_norm p); [gauss_int_norm p = 1] (mod 4); 0 < ReZ p; 0 < ImZ p; ReZ p \<noteq> ImZ p\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
even (gauss_int_norm z)
[PROOF STEP]
have "even (gauss_int_norm z)"
[PROOF STATE]
proof (prove)
using this:
even (gauss_int_norm z)

goal (1 subgoal):
 1. even (gauss_int_norm z)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
even (gauss_int_norm z)

goal (3 subgoals):
 1. \<lbrakk>\<And>q. \<lbrakk>prime q; of_nat q dvd z\<rbrakk> \<Longrightarrow> thesis; p = 1 + \<i>\<^sub>\<int>\<rbrakk> \<Longrightarrow> thesis
 2. \<And>pa. \<lbrakk>\<And>q. \<lbrakk>prime q; of_nat q dvd z\<rbrakk> \<Longrightarrow> thesis; p = of_nat pa; prime pa; [pa = 3] (mod 4)\<rbrakk> \<Longrightarrow> thesis
 3. \<lbrakk>\<And>q. \<lbrakk>prime q; of_nat q dvd z\<rbrakk> \<Longrightarrow> thesis; prime (gauss_int_norm p); [gauss_int_norm p = 1] (mod 4); 0 < ReZ p; 0 < ImZ p; ReZ p \<noteq> ImZ p\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
with \<open>odd (gauss_int_norm z)\<close>
[PROOF STATE]
proof (chain)
picking this:
odd (gauss_int_norm z)
even (gauss_int_norm z)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
odd (gauss_int_norm z)
even (gauss_int_norm z)

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

goal (2 subgoals):
 1. \<And>pa. \<lbrakk>\<And>q. \<lbrakk>prime q; of_nat q dvd z\<rbrakk> \<Longrightarrow> thesis; p = of_nat pa; prime pa; [pa = 3] (mod 4)\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>q. \<lbrakk>prime q; of_nat q dvd z\<rbrakk> \<Longrightarrow> thesis; prime (gauss_int_norm p); [gauss_int_norm p = 1] (mod 4); 0 < ReZ p; 0 < ImZ p; ReZ p \<noteq> ImZ p\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>pa. \<lbrakk>\<And>q. \<lbrakk>prime q; of_nat q dvd z\<rbrakk> \<Longrightarrow> thesis; p = of_nat pa; prime pa; [pa = 3] (mod 4)\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>q. \<lbrakk>prime q; of_nat q dvd z\<rbrakk> \<Longrightarrow> thesis; prime (gauss_int_norm p); [gauss_int_norm p = 1] (mod 4); 0 < ReZ p; 0 < ImZ p; ReZ p \<noteq> ImZ p\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case (cong_3_mod_4 q)
[PROOF STATE]
proof (state)
this:
p = of_nat q
prime q
[q = 3] (mod 4)

goal (2 subgoals):
 1. \<And>pa. \<lbrakk>\<And>q. \<lbrakk>prime q; of_nat q dvd z\<rbrakk> \<Longrightarrow> thesis; p = of_nat pa; prime pa; [pa = 3] (mod 4)\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>q. \<lbrakk>prime q; of_nat q dvd z\<rbrakk> \<Longrightarrow> thesis; prime (gauss_int_norm p); [gauss_int_norm p = 1] (mod 4); 0 < ReZ p; 0 < ImZ p; ReZ p \<noteq> ImZ p\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
p = of_nat q
prime q
[q = 3] (mod 4)

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that[of q] p
[PROOF STATE]
proof (prove)
using this:
p = of_nat q
prime q
[q = 3] (mod 4)
\<lbrakk>prime q; of_nat q dvd z\<rbrakk> \<Longrightarrow> thesis
prime p
p dvd z
p dvd gauss_cnj z

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

goal (1 subgoal):
 1. \<lbrakk>\<And>q. \<lbrakk>prime q; of_nat q dvd z\<rbrakk> \<Longrightarrow> thesis; prime (gauss_int_norm p); [gauss_int_norm p = 1] (mod 4); 0 < ReZ p; 0 < ImZ p; ReZ p \<noteq> ImZ p\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>q. \<lbrakk>prime q; of_nat q dvd z\<rbrakk> \<Longrightarrow> thesis; prime (gauss_int_norm p); [gauss_int_norm p = 1] (mod 4); 0 < ReZ p; 0 < ImZ p; ReZ p \<noteq> ImZ p\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case cong_1_mod_4
[PROOF STATE]
proof (state)
this:
prime (gauss_int_norm p)
[gauss_int_norm p = 1] (mod 4)
0 < ReZ p
0 < ImZ p
ReZ p \<noteq> ImZ p

goal (1 subgoal):
 1. \<lbrakk>\<And>q. \<lbrakk>prime q; of_nat q dvd z\<rbrakk> \<Longrightarrow> thesis; prime (gauss_int_norm p); [gauss_int_norm p = 1] (mod 4); 0 < ReZ p; 0 < ImZ p; ReZ p \<noteq> ImZ p\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
hence "\<not>p dvd p'"
[PROOF STATE]
proof (prove)
using this:
prime (gauss_int_norm p)
[gauss_int_norm p = 1] (mod 4)
0 < ReZ p
0 < ImZ p
ReZ p \<noteq> ImZ p

goal (1 subgoal):
 1. \<not> p dvd p'
[PROOF STEP]
unfolding p'_def
[PROOF STATE]
proof (prove)
using this:
prime (gauss_int_norm p)
[gauss_int_norm p = 1] (mod 4)
0 < ReZ p
0 < ImZ p
ReZ p \<noteq> ImZ p

goal (1 subgoal):
 1. \<not> p dvd gauss_cnj p
[PROOF STEP]
by (subst self_dvd_gauss_cnj_iff) auto
[PROOF STATE]
proof (state)
this:
\<not> p dvd p'

goal (1 subgoal):
 1. \<lbrakk>\<And>q. \<lbrakk>prime q; of_nat q dvd z\<rbrakk> \<Longrightarrow> thesis; prime (gauss_int_norm p); [gauss_int_norm p = 1] (mod 4); 0 < ReZ p; 0 < ImZ p; ReZ p \<noteq> ImZ p\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
hence "p * p' dvd z"
[PROOF STATE]
proof (prove)
using this:
\<not> p dvd p'

goal (1 subgoal):
 1. p * p' dvd z
[PROOF STEP]
using p
[PROOF STATE]
proof (prove)
using this:
\<not> p dvd p'
prime p
p dvd z
p dvd gauss_cnj z

goal (1 subgoal):
 1. p * p' dvd z
[PROOF STEP]
by (intro prime_elem_mult_dvdI) (auto simp: p'_def gauss_cnj_dvd_left_iff)
[PROOF STATE]
proof (state)
this:
p * p' dvd z

goal (1 subgoal):
 1. \<lbrakk>\<And>q. \<lbrakk>prime q; of_nat q dvd z\<rbrakk> \<Longrightarrow> thesis; prime (gauss_int_norm p); [gauss_int_norm p = 1] (mod 4); 0 < ReZ p; 0 < ImZ p; ReZ p \<noteq> ImZ p\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
p * p' dvd z

goal (1 subgoal):
 1. \<lbrakk>\<And>q. \<lbrakk>prime q; of_nat q dvd z\<rbrakk> \<Longrightarrow> thesis; prime (gauss_int_norm p); [gauss_int_norm p = 1] (mod 4); 0 < ReZ p; 0 < ImZ p; ReZ p \<noteq> ImZ p\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have "p * p' = of_nat (gauss_int_norm p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p * p' = of_nat (gauss_int_norm p)
[PROOF STEP]
by (simp add: p'_def self_mult_gauss_cnj)
[PROOF STATE]
proof (state)
this:
p * p' = of_nat (gauss_int_norm p)

goal (1 subgoal):
 1. \<lbrakk>\<And>q. \<lbrakk>prime q; of_nat q dvd z\<rbrakk> \<Longrightarrow> thesis; prime (gauss_int_norm p); [gauss_int_norm p = 1] (mod 4); 0 < ReZ p; 0 < ImZ p; ReZ p \<noteq> ImZ p\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
of_nat (gauss_int_norm p) dvd z
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
of_nat (gauss_int_norm p) dvd z

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that[of "gauss_int_norm p"] cong_1_mod_4
[PROOF STATE]
proof (prove)
using this:
of_nat (gauss_int_norm p) dvd z
\<lbrakk>prime (gauss_int_norm p); of_nat (gauss_int_norm p) dvd z\<rbrakk> \<Longrightarrow> thesis
prime (gauss_int_norm p)
[gauss_int_norm p = 1] (mod 4)
0 < ReZ p
0 < ImZ p
ReZ p \<noteq> ImZ p

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
prime q
of_nat q dvd z

goal (1 subgoal):
 1. False
[PROOF STEP]
have "of_nat q dvd gcd (2 * of_int (ReZ z)) (2 * \<i>\<^sub>\<int> * of_int (ImZ z))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_nat q dvd gcd (2 * of_int (ReZ z)) (2 * \<i>\<^sub>\<int> * of_int (ImZ z))
[PROOF STEP]
proof (rule gcd_greatest)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. of_nat q dvd 2 * of_int (ReZ z)
 2. of_nat q dvd 2 * \<i>\<^sub>\<int> * of_int (ImZ z)
[PROOF STEP]
have "of_nat q dvd (z + gauss_cnj z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_nat q dvd z + gauss_cnj z
[PROOF STEP]
using q
[PROOF STATE]
proof (prove)
using this:
prime q
of_nat q dvd z

goal (1 subgoal):
 1. of_nat q dvd z + gauss_cnj z
[PROOF STEP]
by (auto simp: gauss_cnj_dvd_right_iff)
[PROOF STATE]
proof (state)
this:
of_nat q dvd z + gauss_cnj z

goal (2 subgoals):
 1. of_nat q dvd 2 * of_int (ReZ z)
 2. of_nat q dvd 2 * \<i>\<^sub>\<int> * of_int (ImZ z)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
of_nat q dvd z + gauss_cnj z

goal (2 subgoals):
 1. of_nat q dvd 2 * of_int (ReZ z)
 2. of_nat q dvd 2 * \<i>\<^sub>\<int> * of_int (ImZ z)
[PROOF STEP]
have "\<dots> = 2 * of_int (ReZ z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z + gauss_cnj z = 2 * of_int (ReZ z)
[PROOF STEP]
by (simp add: self_plus_gauss_cnj)
[PROOF STATE]
proof (state)
this:
z + gauss_cnj z = 2 * of_int (ReZ z)

goal (2 subgoals):
 1. of_nat q dvd 2 * of_int (ReZ z)
 2. of_nat q dvd 2 * \<i>\<^sub>\<int> * of_int (ImZ z)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
of_nat q dvd 2 * of_int (ReZ z)
[PROOF STEP]
show "of_nat q dvd (2 * of_int (ReZ z) :: gauss_int)"
[PROOF STATE]
proof (prove)
using this:
of_nat q dvd 2 * of_int (ReZ z)

goal (1 subgoal):
 1. of_nat q dvd 2 * of_int (ReZ z)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
of_nat q dvd 2 * of_int (ReZ z)

goal (1 subgoal):
 1. of_nat q dvd 2 * \<i>\<^sub>\<int> * of_int (ImZ z)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. of_nat q dvd 2 * \<i>\<^sub>\<int> * of_int (ImZ z)
[PROOF STEP]
have "of_nat q dvd (z - gauss_cnj z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_nat q dvd z - gauss_cnj z
[PROOF STEP]
using q
[PROOF STATE]
proof (prove)
using this:
prime q
of_nat q dvd z

goal (1 subgoal):
 1. of_nat q dvd z - gauss_cnj z
[PROOF STEP]
by (auto simp: gauss_cnj_dvd_right_iff)
[PROOF STATE]
proof (state)
this:
of_nat q dvd z - gauss_cnj z

goal (1 subgoal):
 1. of_nat q dvd 2 * \<i>\<^sub>\<int> * of_int (ImZ z)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
of_nat q dvd z - gauss_cnj z

goal (1 subgoal):
 1. of_nat q dvd 2 * \<i>\<^sub>\<int> * of_int (ImZ z)
[PROOF STEP]
have "\<dots> = 2 * \<i>\<^sub>\<int> * of_int (ImZ z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z - gauss_cnj z = 2 * \<i>\<^sub>\<int> * of_int (ImZ z)
[PROOF STEP]
by (simp add: self_minus_gauss_cnj)
[PROOF STATE]
proof (state)
this:
z - gauss_cnj z = 2 * \<i>\<^sub>\<int> * of_int (ImZ z)

goal (1 subgoal):
 1. of_nat q dvd 2 * \<i>\<^sub>\<int> * of_int (ImZ z)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
of_nat q dvd 2 * \<i>\<^sub>\<int> * of_int (ImZ z)
[PROOF STEP]
show "of_nat q dvd (2 * \<i>\<^sub>\<int> * of_int (ImZ z))"
[PROOF STATE]
proof (prove)
using this:
of_nat q dvd 2 * \<i>\<^sub>\<int> * of_int (ImZ z)

goal (1 subgoal):
 1. of_nat q dvd 2 * \<i>\<^sub>\<int> * of_int (ImZ z)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
of_nat q dvd 2 * \<i>\<^sub>\<int> * of_int (ImZ z)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
of_nat q dvd gcd (2 * of_int (ReZ z)) (2 * \<i>\<^sub>\<int> * of_int (ImZ z))

goal (1 subgoal):
 1. False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
of_nat q dvd gcd (2 * of_int (ReZ z)) (2 * \<i>\<^sub>\<int> * of_int (ImZ z))

goal (1 subgoal):
 1. False
[PROOF STEP]
have "\<dots> = 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcd (2 * of_int (ReZ z)) (2 * \<i>\<^sub>\<int> * of_int (ImZ z)) = 2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. gcd (2 * of_int (ReZ z)) (2 * \<i>\<^sub>\<int> * of_int (ImZ z)) = 2
[PROOF STEP]
have "odd (ReZ z) \<or> odd (ImZ z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. odd (ReZ z) \<or> odd (ImZ z)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
coprime (ReZ z) (ImZ z)
odd (gauss_int_norm z)

goal (1 subgoal):
 1. odd (ReZ z) \<or> odd (ImZ z)
[PROOF STEP]
by (auto simp: gauss_int_norm_def even_nat_iff)
[PROOF STATE]
proof (state)
this:
odd (ReZ z) \<or> odd (ImZ z)

goal (1 subgoal):
 1. gcd (2 * of_int (ReZ z)) (2 * \<i>\<^sub>\<int> * of_int (ImZ z)) = 2
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
odd (ReZ z) \<or> odd (ImZ z)

goal (1 subgoal):
 1. gcd (2 * of_int (ReZ z)) (2 * \<i>\<^sub>\<int> * of_int (ImZ z)) = 2
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. odd (ReZ z) \<Longrightarrow> gcd (2 * of_int (ReZ z)) (2 * \<i>\<^sub>\<int> * of_int (ImZ z)) = 2
 2. odd (ImZ z) \<Longrightarrow> gcd (2 * of_int (ReZ z)) (2 * \<i>\<^sub>\<int> * of_int (ImZ z)) = 2
[PROOF STEP]
assume "odd (ReZ z)"
[PROOF STATE]
proof (state)
this:
odd (ReZ z)

goal (2 subgoals):
 1. odd (ReZ z) \<Longrightarrow> gcd (2 * of_int (ReZ z)) (2 * \<i>\<^sub>\<int> * of_int (ImZ z)) = 2
 2. odd (ImZ z) \<Longrightarrow> gcd (2 * of_int (ReZ z)) (2 * \<i>\<^sub>\<int> * of_int (ImZ z)) = 2
[PROOF STEP]
hence "coprime (of_int (ReZ z)) (of_int 2 :: gauss_int)"
[PROOF STATE]
proof (prove)
using this:
odd (ReZ z)

goal (1 subgoal):
 1. coprime (of_int (ReZ z)) (of_int 2)
[PROOF STEP]
unfolding coprime_of_int_gauss_int coprime_right_2_iff_odd
[PROOF STATE]
proof (prove)
using this:
odd (ReZ z)

goal (1 subgoal):
 1. odd (ReZ z)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
coprime (of_int (ReZ z)) (of_int 2)

goal (2 subgoals):
 1. odd (ReZ z) \<Longrightarrow> gcd (2 * of_int (ReZ z)) (2 * \<i>\<^sub>\<int> * of_int (ImZ z)) = 2
 2. odd (ImZ z) \<Longrightarrow> gcd (2 * of_int (ReZ z)) (2 * \<i>\<^sub>\<int> * of_int (ImZ z)) = 2
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
coprime (of_int (ReZ z)) (of_int 2)

goal (1 subgoal):
 1. gcd (2 * of_int (ReZ z)) (2 * \<i>\<^sub>\<int> * of_int (ImZ z)) = 2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
coprime (of_int (ReZ z)) (of_int 2)
coprime (ReZ z) (ImZ z)
odd (gauss_int_norm z)

goal (1 subgoal):
 1. gcd (2 * of_int (ReZ z)) (2 * \<i>\<^sub>\<int> * of_int (ImZ z)) = 2
[PROOF STEP]
by (subst gcd_mult_left_right_cancel)
             (auto simp: coprime_of_int_gauss_int coprime_commute is_unit_left_imp_coprime
                         is_unit_right_imp_coprime gcd_proj1_if_dvd gcd_proj2_if_dvd)
[PROOF STATE]
proof (state)
this:
gcd (2 * of_int (ReZ z)) (2 * \<i>\<^sub>\<int> * of_int (ImZ z)) = 2

goal (1 subgoal):
 1. odd (ImZ z) \<Longrightarrow> gcd (2 * of_int (ReZ z)) (2 * \<i>\<^sub>\<int> * of_int (ImZ z)) = 2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. odd (ImZ z) \<Longrightarrow> gcd (2 * of_int (ReZ z)) (2 * \<i>\<^sub>\<int> * of_int (ImZ z)) = 2
[PROOF STEP]
assume "odd (ImZ z)"
[PROOF STATE]
proof (state)
this:
odd (ImZ z)

goal (1 subgoal):
 1. odd (ImZ z) \<Longrightarrow> gcd (2 * of_int (ReZ z)) (2 * \<i>\<^sub>\<int> * of_int (ImZ z)) = 2
[PROOF STEP]
hence "coprime (of_int (ImZ z)) (of_int 2 :: gauss_int)"
[PROOF STATE]
proof (prove)
using this:
odd (ImZ z)

goal (1 subgoal):
 1. coprime (of_int (ImZ z)) (of_int 2)
[PROOF STEP]
unfolding coprime_of_int_gauss_int coprime_right_2_iff_odd
[PROOF STATE]
proof (prove)
using this:
odd (ImZ z)

goal (1 subgoal):
 1. odd (ImZ z)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
coprime (of_int (ImZ z)) (of_int 2)

goal (1 subgoal):
 1. odd (ImZ z) \<Longrightarrow> gcd (2 * of_int (ReZ z)) (2 * \<i>\<^sub>\<int> * of_int (ImZ z)) = 2
[PROOF STEP]
hence "gcd (2 * of_int (ReZ z)) (2 * \<i>\<^sub>\<int> * of_int (ImZ z)) = gcd (2 * of_int (ReZ z)) (2 * \<i>\<^sub>\<int>)"
[PROOF STATE]
proof (prove)
using this:
coprime (of_int (ImZ z)) (of_int 2)

goal (1 subgoal):
 1. gcd (2 * of_int (ReZ z)) (2 * \<i>\<^sub>\<int> * of_int (ImZ z)) = gcd (2 * of_int (ReZ z)) (2 * \<i>\<^sub>\<int>)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
coprime (of_int (ImZ z)) (of_int 2)
coprime (ReZ z) (ImZ z)
odd (gauss_int_norm z)

goal (1 subgoal):
 1. gcd (2 * of_int (ReZ z)) (2 * \<i>\<^sub>\<int> * of_int (ImZ z)) = gcd (2 * of_int (ReZ z)) (2 * \<i>\<^sub>\<int>)
[PROOF STEP]
by (subst gcd_mult_right_right_cancel)
             (auto simp: coprime_of_int_gauss_int coprime_commute is_unit_left_imp_coprime
                         is_unit_right_imp_coprime)
[PROOF STATE]
proof (state)
this:
gcd (2 * of_int (ReZ z)) (2 * \<i>\<^sub>\<int> * of_int (ImZ z)) = gcd (2 * of_int (ReZ z)) (2 * \<i>\<^sub>\<int>)

goal (1 subgoal):
 1. odd (ImZ z) \<Longrightarrow> gcd (2 * of_int (ReZ z)) (2 * \<i>\<^sub>\<int> * of_int (ImZ z)) = 2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
gcd (2 * of_int (ReZ z)) (2 * \<i>\<^sub>\<int> * of_int (ImZ z)) = gcd (2 * of_int (ReZ z)) (2 * \<i>\<^sub>\<int>)

goal (1 subgoal):
 1. odd (ImZ z) \<Longrightarrow> gcd (2 * of_int (ReZ z)) (2 * \<i>\<^sub>\<int> * of_int (ImZ z)) = 2
[PROOF STEP]
have "\<dots> = normalize (2 * gcd (of_int (ReZ z)) \<i>\<^sub>\<int>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcd (2 * of_int (ReZ z)) (2 * \<i>\<^sub>\<int>) = normalize (2 * gcd (of_int (ReZ z)) \<i>\<^sub>\<int>)
[PROOF STEP]
by (subst gcd_mult_left) auto
[PROOF STATE]
proof (state)
this:
gcd (2 * of_int (ReZ z)) (2 * \<i>\<^sub>\<int>) = normalize (2 * gcd (of_int (ReZ z)) \<i>\<^sub>\<int>)

goal (1 subgoal):
 1. odd (ImZ z) \<Longrightarrow> gcd (2 * of_int (ReZ z)) (2 * \<i>\<^sub>\<int> * of_int (ImZ z)) = 2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
gcd (2 * of_int (ReZ z)) (2 * \<i>\<^sub>\<int>) = normalize (2 * gcd (of_int (ReZ z)) \<i>\<^sub>\<int>)

goal (1 subgoal):
 1. odd (ImZ z) \<Longrightarrow> gcd (2 * of_int (ReZ z)) (2 * \<i>\<^sub>\<int> * of_int (ImZ z)) = 2
[PROOF STEP]
have "gcd (of_int (ReZ z)) \<i>\<^sub>\<int> = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcd (of_int (ReZ z)) \<i>\<^sub>\<int> = 1
[PROOF STEP]
by (subst coprime_iff_gcd_eq_1 [symmetric], rule is_unit_right_imp_coprime) auto
[PROOF STATE]
proof (state)
this:
gcd (of_int (ReZ z)) \<i>\<^sub>\<int> = 1

goal (1 subgoal):
 1. odd (ImZ z) \<Longrightarrow> gcd (2 * of_int (ReZ z)) (2 * \<i>\<^sub>\<int> * of_int (ImZ z)) = 2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
gcd (2 * of_int (ReZ z)) (2 * \<i>\<^sub>\<int> * of_int (ImZ z)) = normalize (2 * 1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
gcd (2 * of_int (ReZ z)) (2 * \<i>\<^sub>\<int> * of_int (ImZ z)) = normalize (2 * 1)

goal (1 subgoal):
 1. gcd (2 * of_int (ReZ z)) (2 * \<i>\<^sub>\<int> * of_int (ImZ z)) = 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
gcd (2 * of_int (ReZ z)) (2 * \<i>\<^sub>\<int> * of_int (ImZ z)) = 2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
gcd (2 * of_int (ReZ z)) (2 * \<i>\<^sub>\<int> * of_int (ImZ z)) = 2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
gcd (2 * of_int (ReZ z)) (2 * \<i>\<^sub>\<int> * of_int (ImZ z)) = 2

goal (1 subgoal):
 1. False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
of_nat q dvd 2
[PROOF STEP]
have "of_nat q dvd (of_nat 2 :: gauss_int)"
[PROOF STATE]
proof (prove)
using this:
of_nat q dvd 2

goal (1 subgoal):
 1. of_nat q dvd of_nat 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
of_nat q dvd of_nat 2

goal (1 subgoal):
 1. False
[PROOF STEP]
hence "q dvd 2"
[PROOF STATE]
proof (prove)
using this:
of_nat q dvd of_nat 2

goal (1 subgoal):
 1. q dvd 2
[PROOF STEP]
by (simp only: of_nat_dvd_of_nat_gauss_int_iff)
[PROOF STATE]
proof (state)
this:
q dvd 2

goal (1 subgoal):
 1. False
[PROOF STEP]
with \<open>prime q\<close>
[PROOF STATE]
proof (chain)
picking this:
prime q
q dvd 2
[PROOF STEP]
have "q = 2"
[PROOF STATE]
proof (prove)
using this:
prime q
q dvd 2

goal (1 subgoal):
 1. q = 2
[PROOF STEP]
using primes_dvd_imp_eq two_is_prime_nat
[PROOF STATE]
proof (prove)
using this:
prime q
q dvd 2
\<lbrakk>prime ?p; prime ?q; ?p dvd ?q\<rbrakk> \<Longrightarrow> ?p = ?q
prime 2

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

goal (1 subgoal):
 1. False
[PROOF STEP]
with q
[PROOF STATE]
proof (chain)
picking this:
prime q
of_nat q dvd z
q = 2
[PROOF STEP]
have "2 dvd z"
[PROOF STATE]
proof (prove)
using this:
prime q
of_nat q dvd z
q = 2

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

goal (1 subgoal):
 1. False
[PROOF STEP]
have "2 dvd gauss_int_norm 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. even (gauss_int_norm 2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
even (gauss_int_norm 2)

goal (1 subgoal):
 1. False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
even (gauss_int_norm 2)

goal (1 subgoal):
 1. False
[PROOF STEP]
have "\<dots> dvd gauss_int_norm z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gauss_int_norm 2 dvd gauss_int_norm z
[PROOF STEP]
using \<open>2 dvd z\<close>
[PROOF STATE]
proof (prove)
using this:
2 dvd z

goal (1 subgoal):
 1. gauss_int_norm 2 dvd gauss_int_norm z
[PROOF STEP]
by (intro gauss_int_norm_dvd_mono)
[PROOF STATE]
proof (state)
this:
gauss_int_norm 2 dvd gauss_int_norm z

goal (1 subgoal):
 1. False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
even (gauss_int_norm z)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
even (gauss_int_norm z)

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>odd (gauss_int_norm z)\<close>
[PROOF STATE]
proof (prove)
using this:
even (gauss_int_norm z)
odd (gauss_int_norm z)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?p \<in># prime_factorization z; ?p \<in># prime_factorization (gauss_cnj z)\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. \<And>c. \<lbrakk>c dvd z; c dvd gauss_cnj z\<rbrakk> \<Longrightarrow> is_unit c
[PROOF STEP]
fix d :: gauss_int
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>c. \<lbrakk>c dvd z; c dvd gauss_cnj z\<rbrakk> \<Longrightarrow> is_unit c
[PROOF STEP]
assume d: "d dvd z" "d dvd gauss_cnj z"
[PROOF STATE]
proof (state)
this:
d dvd z
d dvd gauss_cnj z

goal (1 subgoal):
 1. \<And>c. \<lbrakk>c dvd z; c dvd gauss_cnj z\<rbrakk> \<Longrightarrow> is_unit c
[PROOF STEP]
show "is_unit d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_unit d
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> is_unit d \<Longrightarrow> False
[PROOF STEP]
assume "\<not>is_unit d"
[PROOF STATE]
proof (state)
this:
\<not> is_unit d

goal (1 subgoal):
 1. \<not> is_unit d \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> is_unit d

goal (1 subgoal):
 1. \<not> is_unit d \<Longrightarrow> False
[PROOF STEP]
from d assms
[PROOF STATE]
proof (chain)
picking this:
d dvd z
d dvd gauss_cnj z
coprime (ReZ z) (ImZ z)
odd (gauss_int_norm z)
[PROOF STEP]
have "d \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
d dvd z
d dvd gauss_cnj z
coprime (ReZ z) (ImZ z)
odd (gauss_int_norm z)

goal (1 subgoal):
 1. d \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
d \<noteq> 0

goal (1 subgoal):
 1. \<not> is_unit d \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<not> is_unit d
d \<noteq> 0
[PROOF STEP]
obtain p where p: "prime p" "p dvd d"
[PROOF STATE]
proof (prove)
using this:
\<not> is_unit d
d \<noteq> 0

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>prime p; p dvd d\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prime_divisorE
[PROOF STATE]
proof (prove)
using this:
\<not> is_unit d
d \<noteq> 0
\<lbrakk>?a \<noteq> (0::?'a); \<not> is_unit ?a; \<And>p. \<lbrakk>prime p; p dvd ?a\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>prime p; p dvd d\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
prime p
p dvd d

goal (1 subgoal):
 1. \<not> is_unit d \<Longrightarrow> False
[PROOF STEP]
with d
[PROOF STATE]
proof (chain)
picking this:
d dvd z
d dvd gauss_cnj z
prime p
p dvd d
[PROOF STEP]
have "p \<in> prime_factors z" "p \<in> prime_factors (gauss_cnj z)"
[PROOF STATE]
proof (prove)
using this:
d dvd z
d dvd gauss_cnj z
prime p
p dvd d

goal (1 subgoal):
 1. p \<in># prime_factorization z &&& p \<in># prime_factorization (gauss_cnj z)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
d dvd z
d dvd gauss_cnj z
prime p
p dvd d
coprime (ReZ z) (ImZ z)
odd (gauss_int_norm z)

goal (1 subgoal):
 1. p \<in># prime_factorization z &&& p \<in># prime_factorization (gauss_cnj z)
[PROOF STEP]
by (auto simp: in_prime_factors_iff)
[PROOF STATE]
proof (state)
this:
p \<in># prime_factorization z
p \<in># prime_factorization (gauss_cnj z)

goal (1 subgoal):
 1. \<not> is_unit d \<Longrightarrow> False
[PROOF STEP]
with *[of p]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>p \<in># prime_factorization z; p \<in># prime_factorization (gauss_cnj z)\<rbrakk> \<Longrightarrow> False
p \<in># prime_factorization z
p \<in># prime_factorization (gauss_cnj z)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>p \<in># prime_factorization z; p \<in># prime_factorization (gauss_cnj z)\<rbrakk> \<Longrightarrow> False
p \<in># prime_factorization z
p \<in># prime_factorization (gauss_cnj z)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
is_unit d

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prime_1_mod_4_sum_of_squares_unique_aux:
  fixes p x y :: nat
  assumes "prime p" "[p = 1] (mod 4)" "x ^ 2 + y ^ 2 = p"
  shows   "x > 0 \<and> y > 0 \<and> x \<noteq> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < x \<and> 0 < y \<and> x \<noteq> y
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. 0 < x
 2. 0 < y
 3. x = y \<Longrightarrow> False
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
prime p
[p = 1] (mod 4)
x\<^sup>2 + y\<^sup>2 = p
[PROOF STEP]
show "x > 0" "y > 0"
[PROOF STATE]
proof (prove)
using this:
prime p
[p = 1] (mod 4)
x\<^sup>2 + y\<^sup>2 = p

goal (1 subgoal):
 1. 0 < x &&& 0 < y
[PROOF STEP]
by (auto intro!: Nat.gr0I simp: prime_power_iff)
[PROOF STATE]
proof (state)
this:
0 < x
0 < y

goal (1 subgoal):
 1. x = y \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x = y \<Longrightarrow> False
[PROOF STEP]
assume "x = y"
[PROOF STATE]
proof (state)
this:
x = y

goal (1 subgoal):
 1. x = y \<Longrightarrow> False
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
prime p
[p = 1] (mod 4)
x\<^sup>2 + y\<^sup>2 = p
x = y
[PROOF STEP]
have "p = 2 * x ^ 2"
[PROOF STATE]
proof (prove)
using this:
prime p
[p = 1] (mod 4)
x\<^sup>2 + y\<^sup>2 = p
x = y

goal (1 subgoal):
 1. p = 2 * x\<^sup>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
p = 2 * x\<^sup>2

goal (1 subgoal):
 1. x = y \<Longrightarrow> False
[PROOF STEP]
with \<open>prime p\<close>
[PROOF STATE]
proof (chain)
picking this:
prime p
p = 2 * x\<^sup>2
[PROOF STEP]
have "p = 2"
[PROOF STATE]
proof (prove)
using this:
prime p
p = 2 * x\<^sup>2

goal (1 subgoal):
 1. p = 2
[PROOF STEP]
by (auto dest: prime_product)
[PROOF STATE]
proof (state)
this:
p = 2

goal (1 subgoal):
 1. x = y \<Longrightarrow> False
[PROOF STEP]
with \<open>[p = 1] (mod 4)\<close>
[PROOF STATE]
proof (chain)
picking this:
[p = 1] (mod 4)
p = 2
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
[p = 1] (mod 4)
p = 2

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

goal:
No subgoals!
[PROOF STEP]
qed