[STATEMENT]
lemma minimal_QuadRes_neg1:
  assumes "QuadRes n (-1)" "n > 1" "odd n"
  obtains x :: nat where "x \<le> (n - 1) div 2" and "[x ^ 2 + 1 = 0] (mod n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<le> (n - 1) div 2; [x\<^sup>2 + 1 = 0] (mod n)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<le> (n - 1) div 2; [x\<^sup>2 + 1 = 0] (mod n)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from \<open>QuadRes n (-1)\<close>
[PROOF STATE]
proof (chain)
picking this:
QuadRes (int n) (- 1)
[PROOF STEP]
obtain x where "[x ^ 2 = (-1)] (mod (int n))"
[PROOF STATE]
proof (prove)
using this:
QuadRes (int n) (- 1)

goal (1 subgoal):
 1. (\<And>x. [x\<^sup>2 = - 1] (mod int n) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: QuadRes_def)
[PROOF STATE]
proof (state)
this:
[x\<^sup>2 = - 1] (mod int n)

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<le> (n - 1) div 2; [x\<^sup>2 + 1 = 0] (mod n)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence "[x ^ 2 + 1 = -1 + 1] (mod (int n))"
[PROOF STATE]
proof (prove)
using this:
[x\<^sup>2 = - 1] (mod int n)

goal (1 subgoal):
 1. [x\<^sup>2 + 1 = - 1 + 1] (mod int n)
[PROOF STEP]
by (intro cong_add) auto
[PROOF STATE]
proof (state)
this:
[x\<^sup>2 + 1 = - 1 + 1] (mod int n)

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<le> (n - 1) div 2; [x\<^sup>2 + 1 = 0] (mod n)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
[x\<^sup>2 + 1 = - 1 + 1] (mod int n)

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<le> (n - 1) div 2; [x\<^sup>2 + 1 = 0] (mod n)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "x ^ 2 + 1 = int (nat \<bar>x\<bar> ^ 2 + 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>2 + 1 = int ((nat \<bar>x\<bar>)\<^sup>2 + 1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x\<^sup>2 + 1 = int ((nat \<bar>x\<bar>)\<^sup>2 + 1)

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<le> (n - 1) div 2; [x\<^sup>2 + 1 = 0] (mod n)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
[int ((nat \<bar>x\<bar>)\<^sup>2 + 1) = - 1 + 1] (mod int n)
[PROOF STEP]
have "[int (nat \<bar>x\<bar> ^ 2 + 1) = int 0] (mod (int n))"
[PROOF STATE]
proof (prove)
using this:
[int ((nat \<bar>x\<bar>)\<^sup>2 + 1) = - 1 + 1] (mod int n)

goal (1 subgoal):
 1. [int ((nat \<bar>x\<bar>)\<^sup>2 + 1) = int 0] (mod int n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[int ((nat \<bar>x\<bar>)\<^sup>2 + 1) = int 0] (mod int n)

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<le> (n - 1) div 2; [x\<^sup>2 + 1 = 0] (mod n)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence "[nat \<bar>x\<bar> ^ 2 + 1 = 0] (mod n)"
[PROOF STATE]
proof (prove)
using this:
[int ((nat \<bar>x\<bar>)\<^sup>2 + 1) = int 0] (mod int n)

goal (1 subgoal):
 1. [(nat \<bar>x\<bar>)\<^sup>2 + 1 = 0] (mod n)
[PROOF STEP]
by (subst (asm) cong_int_iff)
[PROOF STATE]
proof (state)
this:
[(nat \<bar>x\<bar>)\<^sup>2 + 1 = 0] (mod n)

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<le> (n - 1) div 2; [x\<^sup>2 + 1 = 0] (mod n)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define x' where
    "x' = (if nat \<bar>x\<bar> mod n \<le> (n - 1) div 2 then nat \<bar>x\<bar> mod n else n - (nat \<bar>x\<bar> mod n))"
[PROOF STATE]
proof (state)
this:
x' = (if nat \<bar>x\<bar> mod n \<le> (n - 1) div 2 then nat \<bar>x\<bar> mod n else n - nat \<bar>x\<bar> mod n)

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<le> (n - 1) div 2; [x\<^sup>2 + 1 = 0] (mod n)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have x'_quadres: "[x' ^ 2 + 1 = 0] (mod n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [x'\<^sup>2 + 1 = 0] (mod n)
[PROOF STEP]
proof (cases "nat \<bar>x\<bar> mod n \<le> (n - 1) div 2")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. nat \<bar>x\<bar> mod n \<le> (n - 1) div 2 \<Longrightarrow> [x'\<^sup>2 + 1 = 0] (mod n)
 2. \<not> nat \<bar>x\<bar> mod n \<le> (n - 1) div 2 \<Longrightarrow> [x'\<^sup>2 + 1 = 0] (mod n)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
nat \<bar>x\<bar> mod n \<le> (n - 1) div 2

goal (2 subgoals):
 1. nat \<bar>x\<bar> mod n \<le> (n - 1) div 2 \<Longrightarrow> [x'\<^sup>2 + 1 = 0] (mod n)
 2. \<not> nat \<bar>x\<bar> mod n \<le> (n - 1) div 2 \<Longrightarrow> [x'\<^sup>2 + 1 = 0] (mod n)
[PROOF STEP]
hence "[x' ^ 2 + 1 = (nat \<bar>x\<bar> mod n) ^ 2 + 1] (mod n)"
[PROOF STATE]
proof (prove)
using this:
nat \<bar>x\<bar> mod n \<le> (n - 1) div 2

goal (1 subgoal):
 1. [x'\<^sup>2 + 1 = (nat \<bar>x\<bar> mod n)\<^sup>2 + 1] (mod n)
[PROOF STEP]
by (simp add: x'_def)
[PROOF STATE]
proof (state)
this:
[x'\<^sup>2 + 1 = (nat \<bar>x\<bar> mod n)\<^sup>2 + 1] (mod n)

goal (2 subgoals):
 1. nat \<bar>x\<bar> mod n \<le> (n - 1) div 2 \<Longrightarrow> [x'\<^sup>2 + 1 = 0] (mod n)
 2. \<not> nat \<bar>x\<bar> mod n \<le> (n - 1) div 2 \<Longrightarrow> [x'\<^sup>2 + 1 = 0] (mod n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
[x'\<^sup>2 + 1 = (nat \<bar>x\<bar> mod n)\<^sup>2 + 1] (mod n)

goal (2 subgoals):
 1. nat \<bar>x\<bar> mod n \<le> (n - 1) div 2 \<Longrightarrow> [x'\<^sup>2 + 1 = 0] (mod n)
 2. \<not> nat \<bar>x\<bar> mod n \<le> (n - 1) div 2 \<Longrightarrow> [x'\<^sup>2 + 1 = 0] (mod n)
[PROOF STEP]
have "[(nat \<bar>x\<bar> mod n) ^ 2 + 1 = nat \<bar>x\<bar> ^ 2 + 1] (mod n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [(nat \<bar>x\<bar> mod n)\<^sup>2 + 1 = (nat \<bar>x\<bar>)\<^sup>2 + 1] (mod n)
[PROOF STEP]
by (intro cong_add cong_pow) (auto simp: cong_def)
[PROOF STATE]
proof (state)
this:
[(nat \<bar>x\<bar> mod n)\<^sup>2 + 1 = (nat \<bar>x\<bar>)\<^sup>2 + 1] (mod n)

goal (2 subgoals):
 1. nat \<bar>x\<bar> mod n \<le> (n - 1) div 2 \<Longrightarrow> [x'\<^sup>2 + 1 = 0] (mod n)
 2. \<not> nat \<bar>x\<bar> mod n \<le> (n - 1) div 2 \<Longrightarrow> [x'\<^sup>2 + 1 = 0] (mod n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
[(nat \<bar>x\<bar> mod n)\<^sup>2 + 1 = (nat \<bar>x\<bar>)\<^sup>2 + 1] (mod n)

goal (2 subgoals):
 1. nat \<bar>x\<bar> mod n \<le> (n - 1) div 2 \<Longrightarrow> [x'\<^sup>2 + 1 = 0] (mod n)
 2. \<not> nat \<bar>x\<bar> mod n \<le> (n - 1) div 2 \<Longrightarrow> [x'\<^sup>2 + 1 = 0] (mod n)
[PROOF STEP]
have "[nat \<bar>x\<bar> ^ 2 + 1 = 0] (mod n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [(nat \<bar>x\<bar>)\<^sup>2 + 1 = 0] (mod n)
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
[(nat \<bar>x\<bar>)\<^sup>2 + 1 = 0] (mod n)

goal (2 subgoals):
 1. nat \<bar>x\<bar> mod n \<le> (n - 1) div 2 \<Longrightarrow> [x'\<^sup>2 + 1 = 0] (mod n)
 2. \<not> nat \<bar>x\<bar> mod n \<le> (n - 1) div 2 \<Longrightarrow> [x'\<^sup>2 + 1 = 0] (mod n)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
[x'\<^sup>2 + 1 = 0] (mod n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
[x'\<^sup>2 + 1 = 0] (mod n)

goal (1 subgoal):
 1. [x'\<^sup>2 + 1 = 0] (mod n)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
[x'\<^sup>2 + 1 = 0] (mod n)

goal (1 subgoal):
 1. \<not> nat \<bar>x\<bar> mod n \<le> (n - 1) div 2 \<Longrightarrow> [x'\<^sup>2 + 1 = 0] (mod n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> nat \<bar>x\<bar> mod n \<le> (n - 1) div 2 \<Longrightarrow> [x'\<^sup>2 + 1 = 0] (mod n)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> nat \<bar>x\<bar> mod n \<le> (n - 1) div 2

goal (1 subgoal):
 1. \<not> nat \<bar>x\<bar> mod n \<le> (n - 1) div 2 \<Longrightarrow> [x'\<^sup>2 + 1 = 0] (mod n)
[PROOF STEP]
hence "[int (x' ^ 2 + 1) = (int n - int (nat \<bar>x\<bar> mod n)) ^ 2 + 1] (mod int n)"
[PROOF STATE]
proof (prove)
using this:
\<not> nat \<bar>x\<bar> mod n \<le> (n - 1) div 2

goal (1 subgoal):
 1. [int (x'\<^sup>2 + 1) = (int n - int (nat \<bar>x\<bar> mod n))\<^sup>2 + 1] (mod int n)
[PROOF STEP]
using \<open>n > 1\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> nat \<bar>x\<bar> mod n \<le> (n - 1) div 2
1 < n

goal (1 subgoal):
 1. [int (x'\<^sup>2 + 1) = (int n - int (nat \<bar>x\<bar> mod n))\<^sup>2 + 1] (mod int n)
[PROOF STEP]
by (simp add: x'_def of_nat_diff add_ac)
[PROOF STATE]
proof (state)
this:
[int (x'\<^sup>2 + 1) = (int n - int (nat \<bar>x\<bar> mod n))\<^sup>2 + 1] (mod int n)

goal (1 subgoal):
 1. \<not> nat \<bar>x\<bar> mod n \<le> (n - 1) div 2 \<Longrightarrow> [x'\<^sup>2 + 1 = 0] (mod n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
[int (x'\<^sup>2 + 1) = (int n - int (nat \<bar>x\<bar> mod n))\<^sup>2 + 1] (mod int n)

goal (1 subgoal):
 1. \<not> nat \<bar>x\<bar> mod n \<le> (n - 1) div 2 \<Longrightarrow> [x'\<^sup>2 + 1 = 0] (mod n)
[PROOF STEP]
have "[(int n - int (nat \<bar>x\<bar> mod n)) ^ 2 + 1 =
                (0 - int (nat \<bar>x\<bar> mod n)) ^ 2 + 1] (mod int n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [(int n - int (nat \<bar>x\<bar> mod n))\<^sup>2 + 1 = (0 - int (nat \<bar>x\<bar> mod n))\<^sup>2 + 1] (mod int n)
[PROOF STEP]
by (intro cong_add cong_pow) (auto simp: cong_def)
[PROOF STATE]
proof (state)
this:
[(int n - int (nat \<bar>x\<bar> mod n))\<^sup>2 + 1 = (0 - int (nat \<bar>x\<bar> mod n))\<^sup>2 + 1] (mod int n)

goal (1 subgoal):
 1. \<not> nat \<bar>x\<bar> mod n \<le> (n - 1) div 2 \<Longrightarrow> [x'\<^sup>2 + 1 = 0] (mod n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
[(int n - int (nat \<bar>x\<bar> mod n))\<^sup>2 + 1 = (0 - int (nat \<bar>x\<bar> mod n))\<^sup>2 + 1] (mod int n)

goal (1 subgoal):
 1. \<not> nat \<bar>x\<bar> mod n \<le> (n - 1) div 2 \<Longrightarrow> [x'\<^sup>2 + 1 = 0] (mod n)
[PROOF STEP]
have "[(0 - int (nat \<bar>x\<bar> mod n)) ^ 2 + 1 = int ((nat \<bar>x\<bar> mod n) ^ 2 + 1)] (mod (int n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [(0 - int (nat \<bar>x\<bar> mod n))\<^sup>2 + 1 = int ((nat \<bar>x\<bar> mod n)\<^sup>2 + 1)] (mod int n)
[PROOF STEP]
by (simp add: add_ac)
[PROOF STATE]
proof (state)
this:
[(0 - int (nat \<bar>x\<bar> mod n))\<^sup>2 + 1 = int ((nat \<bar>x\<bar> mod n)\<^sup>2 + 1)] (mod int n)

goal (1 subgoal):
 1. \<not> nat \<bar>x\<bar> mod n \<le> (n - 1) div 2 \<Longrightarrow> [x'\<^sup>2 + 1 = 0] (mod n)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
[int (x'\<^sup>2 + 1) = int ((nat \<bar>x\<bar> mod n)\<^sup>2 + 1)] (mod int n)
[PROOF STEP]
have "[x' ^ 2 + 1 = (nat \<bar>x\<bar> mod n)\<^sup>2 + 1] (mod n)"
[PROOF STATE]
proof (prove)
using this:
[int (x'\<^sup>2 + 1) = int ((nat \<bar>x\<bar> mod n)\<^sup>2 + 1)] (mod int n)

goal (1 subgoal):
 1. [x'\<^sup>2 + 1 = (nat \<bar>x\<bar> mod n)\<^sup>2 + 1] (mod n)
[PROOF STEP]
by (subst (asm) cong_int_iff)
[PROOF STATE]
proof (state)
this:
[x'\<^sup>2 + 1 = (nat \<bar>x\<bar> mod n)\<^sup>2 + 1] (mod n)

goal (1 subgoal):
 1. \<not> nat \<bar>x\<bar> mod n \<le> (n - 1) div 2 \<Longrightarrow> [x'\<^sup>2 + 1 = 0] (mod n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
[x'\<^sup>2 + 1 = (nat \<bar>x\<bar> mod n)\<^sup>2 + 1] (mod n)

goal (1 subgoal):
 1. \<not> nat \<bar>x\<bar> mod n \<le> (n - 1) div 2 \<Longrightarrow> [x'\<^sup>2 + 1 = 0] (mod n)
[PROOF STEP]
have "[(nat \<bar>x\<bar> mod n)\<^sup>2 + 1 = nat \<bar>x\<bar> ^ 2 + 1] (mod n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [(nat \<bar>x\<bar> mod n)\<^sup>2 + 1 = (nat \<bar>x\<bar>)\<^sup>2 + 1] (mod n)
[PROOF STEP]
by (intro cong_add cong_pow) (auto simp: cong_def)
[PROOF STATE]
proof (state)
this:
[(nat \<bar>x\<bar> mod n)\<^sup>2 + 1 = (nat \<bar>x\<bar>)\<^sup>2 + 1] (mod n)

goal (1 subgoal):
 1. \<not> nat \<bar>x\<bar> mod n \<le> (n - 1) div 2 \<Longrightarrow> [x'\<^sup>2 + 1 = 0] (mod n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
[(nat \<bar>x\<bar> mod n)\<^sup>2 + 1 = (nat \<bar>x\<bar>)\<^sup>2 + 1] (mod n)

goal (1 subgoal):
 1. \<not> nat \<bar>x\<bar> mod n \<le> (n - 1) div 2 \<Longrightarrow> [x'\<^sup>2 + 1 = 0] (mod n)
[PROOF STEP]
have "[nat \<bar>x\<bar> ^ 2 + 1 = 0] (mod n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [(nat \<bar>x\<bar>)\<^sup>2 + 1 = 0] (mod n)
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
[(nat \<bar>x\<bar>)\<^sup>2 + 1 = 0] (mod n)

goal (1 subgoal):
 1. \<not> nat \<bar>x\<bar> mod n \<le> (n - 1) div 2 \<Longrightarrow> [x'\<^sup>2 + 1 = 0] (mod n)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
[x'\<^sup>2 + 1 = 0] (mod n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
[x'\<^sup>2 + 1 = 0] (mod n)

goal (1 subgoal):
 1. [x'\<^sup>2 + 1 = 0] (mod n)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
[x'\<^sup>2 + 1 = 0] (mod n)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[x'\<^sup>2 + 1 = 0] (mod n)

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<le> (n - 1) div 2; [x\<^sup>2 + 1 = 0] (mod n)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
[x'\<^sup>2 + 1 = 0] (mod n)

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<le> (n - 1) div 2; [x\<^sup>2 + 1 = 0] (mod n)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have x'_le: "x' \<le> (n - 1) div 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x' \<le> (n - 1) div 2
[PROOF STEP]
using \<open>odd n\<close>
[PROOF STATE]
proof (prove)
using this:
odd n

goal (1 subgoal):
 1. x' \<le> (n - 1) div 2
[PROOF STEP]
by (auto elim!: oddE simp: x'_def)
[PROOF STATE]
proof (state)
this:
x' \<le> (n - 1) div 2

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<le> (n - 1) div 2; [x\<^sup>2 + 1 = 0] (mod n)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
[x'\<^sup>2 + 1 = 0] (mod n)
x' \<le> (n - 1) div 2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
[x'\<^sup>2 + 1 = 0] (mod n)
x' \<le> (n - 1) div 2

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (intro that[of x'])
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma p_gt_2: "p > 2" and odd_p: "odd p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 < p &&& odd p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 2 < p
 2. odd p
[PROOF STEP]
from prime_p and cong_1_p
[PROOF STATE]
proof (chain)
picking this:
prime p
[p = 1] (mod 4)
[PROOF STEP]
have "p > 1" "p \<noteq> 2"
[PROOF STATE]
proof (prove)
using this:
prime p
[p = 1] (mod 4)

goal (1 subgoal):
 1. 1 < p &&& p \<noteq> 2
[PROOF STEP]
by (auto simp: prime_gt_Suc_0_nat cong_def)
[PROOF STATE]
proof (state)
this:
1 < p
p \<noteq> 2

goal (2 subgoals):
 1. 2 < p
 2. odd p
[PROOF STEP]
thus "p > 2"
[PROOF STATE]
proof (prove)
using this:
1 < p
p \<noteq> 2

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

goal (1 subgoal):
 1. odd p
[PROOF STEP]
with prime_p
[PROOF STATE]
proof (chain)
picking this:
prime p
2 < p
[PROOF STEP]
show "odd p"
[PROOF STATE]
proof (prove)
using this:
prime p
2 < p

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma minimal_QuadRes_neg1:
  obtains x where "x > 0" "x \<le> (p - 1) div 2" "[x ^ 2 + 1 = 0] (mod p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. \<lbrakk>0 < x; x \<le> (p - 1) div 2; [x\<^sup>2 + 1 = 0] (mod p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>x. \<lbrakk>0 < x; x \<le> (p - 1) div 2; [x\<^sup>2 + 1 = 0] (mod p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "[Legendre (-1) (int p) = (- 1) ^ ((p - 1) div 2)] (mod (int p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [Legendre (- 1) (int p) = (- 1) ^ ((p - 1) div 2)] (mod int p)
[PROOF STEP]
using prime_p p_gt_2
[PROOF STATE]
proof (prove)
using this:
prime p
2 < p

goal (1 subgoal):
 1. [Legendre (- 1) (int p) = (- 1) ^ ((p - 1) div 2)] (mod int p)
[PROOF STEP]
by (intro euler_criterion) auto
[PROOF STATE]
proof (state)
this:
[Legendre (- 1) (int p) = (- 1) ^ ((p - 1) div 2)] (mod int p)

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>0 < x; x \<le> (p - 1) div 2; [x\<^sup>2 + 1 = 0] (mod p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
[Legendre (- 1) (int p) = (- 1) ^ ((p - 1) div 2)] (mod int p)

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>0 < x; x \<le> (p - 1) div 2; [x\<^sup>2 + 1 = 0] (mod p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "[p - 1 = 1 - 1] (mod 4)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [p - 1 = 1 - 1] (mod 4)
[PROOF STEP]
using p_gt_2
[PROOF STATE]
proof (prove)
using this:
2 < p

goal (1 subgoal):
 1. [p - 1 = 1 - 1] (mod 4)
[PROOF STEP]
by (intro cong_diff_nat cong_refl) (use cong_1_p in auto)
[PROOF STATE]
proof (state)
this:
[p - 1 = 1 - 1] (mod 4)

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>0 < x; x \<le> (p - 1) div 2; [x\<^sup>2 + 1 = 0] (mod p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence "2 * 2 dvd p - 1"
[PROOF STATE]
proof (prove)
using this:
[p - 1 = 1 - 1] (mod 4)

goal (1 subgoal):
 1. 2 * 2 dvd p - 1
[PROOF STEP]
by (simp add: cong_0_iff)
[PROOF STATE]
proof (state)
this:
2 * 2 dvd p - 1

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>0 < x; x \<le> (p - 1) div 2; [x\<^sup>2 + 1 = 0] (mod p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence "even ((p - 1) div 2)"
[PROOF STATE]
proof (prove)
using this:
2 * 2 dvd p - 1

goal (1 subgoal):
 1. even ((p - 1) div 2)
[PROOF STEP]
using dvd_mult_imp_div
[PROOF STATE]
proof (prove)
using this:
2 * 2 dvd p - 1
?a * ?c dvd ?b \<Longrightarrow> ?a dvd ?b div ?c

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

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>0 < x; x \<le> (p - 1) div 2; [x\<^sup>2 + 1 = 0] (mod p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence "(-1) ^ ((p - 1) div 2) = (1 :: int)"
[PROOF STATE]
proof (prove)
using this:
even ((p - 1) div 2)

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

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>0 < x; x \<le> (p - 1) div 2; [x\<^sup>2 + 1 = 0] (mod p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
[Legendre (- 1) (int p) = 1] (mod int p)
[PROOF STEP]
have "Legendre (-1) (int p) mod p = 1"
[PROOF STATE]
proof (prove)
using this:
[Legendre (- 1) (int p) = 1] (mod int p)

goal (1 subgoal):
 1. Legendre (- 1) (int p) mod int p = 1
[PROOF STEP]
using p_gt_2
[PROOF STATE]
proof (prove)
using this:
[Legendre (- 1) (int p) = 1] (mod int p)
2 < p

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

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>0 < x; x \<le> (p - 1) div 2; [x\<^sup>2 + 1 = 0] (mod p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence "Legendre (-1) (int p) = 1"
[PROOF STATE]
proof (prove)
using this:
Legendre (- 1) (int p) mod int p = 1

goal (1 subgoal):
 1. Legendre (- 1) (int p) = 1
[PROOF STEP]
using p_gt_2
[PROOF STATE]
proof (prove)
using this:
Legendre (- 1) (int p) mod int p = 1
2 < p

goal (1 subgoal):
 1. Legendre (- 1) (int p) = 1
[PROOF STEP]
by (auto simp: Legendre_def cong_def zmod_minus1 split: if_splits)
[PROOF STATE]
proof (state)
this:
Legendre (- 1) (int p) = 1

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>0 < x; x \<le> (p - 1) div 2; [x\<^sup>2 + 1 = 0] (mod p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence "QuadRes p (-1)"
[PROOF STATE]
proof (prove)
using this:
Legendre (- 1) (int p) = 1

goal (1 subgoal):
 1. QuadRes (int p) (- 1)
[PROOF STEP]
by (simp add: Legendre_def split: if_splits)
[PROOF STATE]
proof (state)
this:
QuadRes (int p) (- 1)

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>0 < x; x \<le> (p - 1) div 2; [x\<^sup>2 + 1 = 0] (mod p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from minimal_QuadRes_neg1[OF this] p_gt_2 odd_p
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>1 < p; odd p; \<And>x. \<lbrakk>x \<le> (p - 1) div 2; [x\<^sup>2 + 1 = 0] (mod p)\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
2 < p
odd p
[PROOF STEP]
obtain x where x: "x \<le> (p - 1) div 2" "[x ^ 2 + 1 = 0] (mod p)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>1 < p; odd p; \<And>x. \<lbrakk>x \<le> (p - 1) div 2; [x\<^sup>2 + 1 = 0] (mod p)\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
2 < p
odd p

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<le> (p - 1) div 2; [x\<^sup>2 + 1 = 0] (mod p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<le> (p - 1) div 2
[x\<^sup>2 + 1 = 0] (mod p)

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>0 < x; x \<le> (p - 1) div 2; [x\<^sup>2 + 1 = 0] (mod p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "x > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < x
[PROOF STEP]
using x p_gt_2
[PROOF STATE]
proof (prove)
using this:
x \<le> (p - 1) div 2
[x\<^sup>2 + 1 = 0] (mod p)
2 < p

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

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>0 < x; x \<le> (p - 1) div 2; [x\<^sup>2 + 1 = 0] (mod p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from x and this
[PROOF STATE]
proof (chain)
picking this:
x \<le> (p - 1) div 2
[x\<^sup>2 + 1 = 0] (mod p)
0 < x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<le> (p - 1) div 2
[x\<^sup>2 + 1 = 0] (mod p)
0 < x

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (intro that[of x]) auto
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma not_prime: "\<not>prime_elem (of_nat p :: gauss_int)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> prime_elem (of_nat p)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prime_elem (of_nat p) \<Longrightarrow> False
[PROOF STEP]
assume prime: "prime_elem (of_nat p :: gauss_int)"
[PROOF STATE]
proof (state)
this:
prime_elem (of_nat p)

goal (1 subgoal):
 1. prime_elem (of_nat p) \<Longrightarrow> False
[PROOF STEP]
obtain x where x: "x > 0" "x \<le> (p - 1) div 2" "[x ^ 2 + 1 = 0] (mod p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. \<lbrakk>0 < x; x \<le> (p - 1) div 2; [x\<^sup>2 + 1 = 0] (mod p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using  minimal_QuadRes_neg1
[PROOF STATE]
proof (prove)
using this:
(\<And>x. \<lbrakk>0 < x; x \<le> (p - 1) div 2; [x\<^sup>2 + 1 = 0] (mod p)\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>0 < x; x \<le> (p - 1) div 2; [x\<^sup>2 + 1 = 0] (mod p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
0 < x
x \<le> (p - 1) div 2
[x\<^sup>2 + 1 = 0] (mod p)

goal (1 subgoal):
 1. prime_elem (of_nat p) \<Longrightarrow> False
[PROOF STEP]
have "of_nat p dvd (of_nat (x ^ 2 + 1) :: gauss_int)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_nat p dvd of_nat (x\<^sup>2 + 1)
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
0 < x
x \<le> (p - 1) div 2
[x\<^sup>2 + 1 = 0] (mod p)

goal (1 subgoal):
 1. of_nat p dvd of_nat (x\<^sup>2 + 1)
[PROOF STEP]
by (intro of_nat_dvd_of_nat) (auto simp: cong_0_iff)
[PROOF STATE]
proof (state)
this:
of_nat p dvd of_nat (x\<^sup>2 + 1)

goal (1 subgoal):
 1. prime_elem (of_nat p) \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
of_nat p dvd of_nat (x\<^sup>2 + 1)

goal (1 subgoal):
 1. prime_elem (of_nat p) \<Longrightarrow> False
[PROOF STEP]
have eq: "of_nat (x ^ 2 + 1) = ((of_nat x + \<i>\<^sub>\<int>) * (of_nat x - \<i>\<^sub>\<int>) :: gauss_int)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_nat (x\<^sup>2 + 1) = (of_nat x + \<i>\<^sub>\<int>) * (of_nat x - \<i>\<^sub>\<int>)
[PROOF STEP]
using \<open>x > 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < x

goal (1 subgoal):
 1. of_nat (x\<^sup>2 + 1) = (of_nat x + \<i>\<^sub>\<int>) * (of_nat x - \<i>\<^sub>\<int>)
[PROOF STEP]
by (simp add: algebra_simps gauss_int_eq_iff power2_eq_square of_nat_diff)
[PROOF STATE]
proof (state)
this:
of_nat (x\<^sup>2 + 1) = (of_nat x + \<i>\<^sub>\<int>) * (of_nat x - \<i>\<^sub>\<int>)

goal (1 subgoal):
 1. prime_elem (of_nat p) \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
of_nat p dvd (of_nat x + \<i>\<^sub>\<int>) * (of_nat x - \<i>\<^sub>\<int>)
[PROOF STEP]
have "of_nat p dvd ((of_nat x + \<i>\<^sub>\<int>) * (of_nat x - \<i>\<^sub>\<int>) :: gauss_int)"
[PROOF STATE]
proof (prove)
using this:
of_nat p dvd (of_nat x + \<i>\<^sub>\<int>) * (of_nat x - \<i>\<^sub>\<int>)

goal (1 subgoal):
 1. of_nat p dvd (of_nat x + \<i>\<^sub>\<int>) * (of_nat x - \<i>\<^sub>\<int>)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
of_nat p dvd (of_nat x + \<i>\<^sub>\<int>) * (of_nat x - \<i>\<^sub>\<int>)

goal (1 subgoal):
 1. prime_elem (of_nat p) \<Longrightarrow> False
[PROOF STEP]
from prime and this
[PROOF STATE]
proof (chain)
picking this:
prime_elem (of_nat p)
of_nat p dvd (of_nat x + \<i>\<^sub>\<int>) * (of_nat x - \<i>\<^sub>\<int>)
[PROOF STEP]
have "of_nat p dvd (of_nat x + \<i>\<^sub>\<int> :: gauss_int) \<or> of_nat p dvd (of_nat x - \<i>\<^sub>\<int> :: gauss_int)"
[PROOF STATE]
proof (prove)
using this:
prime_elem (of_nat p)
of_nat p dvd (of_nat x + \<i>\<^sub>\<int>) * (of_nat x - \<i>\<^sub>\<int>)

goal (1 subgoal):
 1. of_nat p dvd of_nat x + \<i>\<^sub>\<int> \<or> of_nat p dvd of_nat x - \<i>\<^sub>\<int>
[PROOF STEP]
by (rule prime_elem_dvd_multD)
[PROOF STATE]
proof (state)
this:
of_nat p dvd of_nat x + \<i>\<^sub>\<int> \<or> of_nat p dvd of_nat x - \<i>\<^sub>\<int>

goal (1 subgoal):
 1. prime_elem (of_nat p) \<Longrightarrow> False
[PROOF STEP]
hence dvd: "of_nat p dvd (of_nat x + \<i>\<^sub>\<int> :: gauss_int)" "of_nat p dvd (of_nat x - \<i>\<^sub>\<int> :: gauss_int)"
[PROOF STATE]
proof (prove)
using this:
of_nat p dvd of_nat x + \<i>\<^sub>\<int> \<or> of_nat p dvd of_nat x - \<i>\<^sub>\<int>

goal (1 subgoal):
 1. of_nat p dvd of_nat x + \<i>\<^sub>\<int> &&& of_nat p dvd of_nat x - \<i>\<^sub>\<int>
[PROOF STEP]
by (auto dest: of_nat_dvd_imp_dvd_gauss_cnj)
[PROOF STATE]
proof (state)
this:
of_nat p dvd of_nat x + \<i>\<^sub>\<int>
of_nat p dvd of_nat x - \<i>\<^sub>\<int>

goal (1 subgoal):
 1. prime_elem (of_nat p) \<Longrightarrow> False
[PROOF STEP]
have "of_nat (p ^ 2) = (of_nat p * of_nat p :: gauss_int)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_nat (p\<^sup>2) = of_nat p * of_nat p
[PROOF STEP]
by (simp add: power2_eq_square)
[PROOF STATE]
proof (state)
this:
of_nat (p\<^sup>2) = of_nat p * of_nat p

goal (1 subgoal):
 1. prime_elem (of_nat p) \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
of_nat (p\<^sup>2) = of_nat p * of_nat p

goal (1 subgoal):
 1. prime_elem (of_nat p) \<Longrightarrow> False
[PROOF STEP]
from dvd
[PROOF STATE]
proof (chain)
picking this:
of_nat p dvd of_nat x + \<i>\<^sub>\<int>
of_nat p dvd of_nat x - \<i>\<^sub>\<int>
[PROOF STEP]
have "\<dots> dvd ((of_nat x + \<i>\<^sub>\<int>) * (of_nat x - \<i>\<^sub>\<int>))"
[PROOF STATE]
proof (prove)
using this:
of_nat p dvd of_nat x + \<i>\<^sub>\<int>
of_nat p dvd of_nat x - \<i>\<^sub>\<int>

goal (1 subgoal):
 1. of_nat p * of_nat p dvd (of_nat x + \<i>\<^sub>\<int>) * (of_nat x - \<i>\<^sub>\<int>)
[PROOF STEP]
by (intro mult_dvd_mono)
[PROOF STATE]
proof (state)
this:
of_nat p * of_nat p dvd (of_nat x + \<i>\<^sub>\<int>) * (of_nat x - \<i>\<^sub>\<int>)

goal (1 subgoal):
 1. prime_elem (of_nat p) \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
of_nat p * of_nat p dvd (of_nat x + \<i>\<^sub>\<int>) * (of_nat x - \<i>\<^sub>\<int>)

goal (1 subgoal):
 1. prime_elem (of_nat p) \<Longrightarrow> False
[PROOF STEP]
have "\<dots> = of_nat (x ^ 2 + 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (of_nat x + \<i>\<^sub>\<int>) * (of_nat x - \<i>\<^sub>\<int>) = of_nat (x\<^sup>2 + 1)
[PROOF STEP]
by (rule eq [symmetric])
[PROOF STATE]
proof (state)
this:
(of_nat x + \<i>\<^sub>\<int>) * (of_nat x - \<i>\<^sub>\<int>) = of_nat (x\<^sup>2 + 1)

goal (1 subgoal):
 1. prime_elem (of_nat p) \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
of_nat (p\<^sup>2) dvd of_nat (x\<^sup>2 + 1)
[PROOF STEP]
have "p ^ 2 dvd (x ^ 2 + 1)"
[PROOF STATE]
proof (prove)
using this:
of_nat (p\<^sup>2) dvd of_nat (x\<^sup>2 + 1)

goal (1 subgoal):
 1. p\<^sup>2 dvd x\<^sup>2 + 1
[PROOF STEP]
by (subst (asm) of_nat_dvd_of_nat_gauss_int_iff)
[PROOF STATE]
proof (state)
this:
p\<^sup>2 dvd x\<^sup>2 + 1

goal (1 subgoal):
 1. prime_elem (of_nat p) \<Longrightarrow> False
[PROOF STEP]
hence "p ^ 2 \<le> x ^ 2 + 1"
[PROOF STATE]
proof (prove)
using this:
p\<^sup>2 dvd x\<^sup>2 + 1

goal (1 subgoal):
 1. p\<^sup>2 \<le> x\<^sup>2 + 1
[PROOF STEP]
by (intro dvd_imp_le) auto
[PROOF STATE]
proof (state)
this:
p\<^sup>2 \<le> x\<^sup>2 + 1

goal (1 subgoal):
 1. prime_elem (of_nat p) \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
p\<^sup>2 \<le> x\<^sup>2 + 1

goal (1 subgoal):
 1. prime_elem (of_nat p) \<Longrightarrow> False
[PROOF STEP]
have "p ^ 2 > x ^ 2 + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>2 + 1 < p\<^sup>2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x\<^sup>2 + 1 < p\<^sup>2
[PROOF STEP]
have "x ^ 2 + 1 \<le> ((p - 1) div 2) ^ 2 + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>2 + 1 \<le> ((p - 1) div 2)\<^sup>2 + 1
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
0 < x
x \<le> (p - 1) div 2
[x\<^sup>2 + 1 = 0] (mod p)

goal (1 subgoal):
 1. x\<^sup>2 + 1 \<le> ((p - 1) div 2)\<^sup>2 + 1
[PROOF STEP]
by (intro add_mono power_mono) auto
[PROOF STATE]
proof (state)
this:
x\<^sup>2 + 1 \<le> ((p - 1) div 2)\<^sup>2 + 1

goal (1 subgoal):
 1. x\<^sup>2 + 1 < p\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x\<^sup>2 + 1 \<le> ((p - 1) div 2)\<^sup>2 + 1

goal (1 subgoal):
 1. x\<^sup>2 + 1 < p\<^sup>2
[PROOF STEP]
have "\<dots> \<le> (p - 1) ^ 2 + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((p - 1) div 2)\<^sup>2 + 1 \<le> (p - 1)\<^sup>2 + 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((p - 1) div 2)\<^sup>2 + 1 \<le> (p - 1)\<^sup>2 + 1

goal (1 subgoal):
 1. x\<^sup>2 + 1 < p\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
((p - 1) div 2)\<^sup>2 + 1 \<le> (p - 1)\<^sup>2 + 1

goal (1 subgoal):
 1. x\<^sup>2 + 1 < p\<^sup>2
[PROOF STEP]
have "(p - 1) * (p - 1) < (p - 1) * (p + 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p - 1) * (p - 1) < (p - 1) * (p + 1)
[PROOF STEP]
using p_gt_2
[PROOF STATE]
proof (prove)
using this:
2 < p

goal (1 subgoal):
 1. (p - 1) * (p - 1) < (p - 1) * (p + 1)
[PROOF STEP]
by (intro mult_strict_left_mono) auto
[PROOF STATE]
proof (state)
this:
(p - 1) * (p - 1) < (p - 1) * (p + 1)

goal (1 subgoal):
 1. x\<^sup>2 + 1 < p\<^sup>2
[PROOF STEP]
hence "(p - 1) ^ 2 + 1 < p ^ 2"
[PROOF STATE]
proof (prove)
using this:
(p - 1) * (p - 1) < (p - 1) * (p + 1)

goal (1 subgoal):
 1. (p - 1)\<^sup>2 + 1 < p\<^sup>2
[PROOF STEP]
by (simp add: algebra_simps power2_eq_square)
[PROOF STATE]
proof (state)
this:
(p - 1)\<^sup>2 + 1 < p\<^sup>2

goal (1 subgoal):
 1. x\<^sup>2 + 1 < p\<^sup>2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x\<^sup>2 + 1 < p\<^sup>2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x\<^sup>2 + 1 < p\<^sup>2

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x\<^sup>2 + 1 < p\<^sup>2

goal (1 subgoal):
 1. prime_elem (of_nat p) \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
p\<^sup>2 \<le> x\<^sup>2 + 1
x\<^sup>2 + 1 < p\<^sup>2
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
p\<^sup>2 \<le> x\<^sup>2 + 1
x\<^sup>2 + 1 < p\<^sup>2

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma norm_prime_divisor:
  fixes q :: gauss_int
  assumes q: "prime_elem q" "q dvd of_nat p"
  shows "gauss_int_norm q = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gauss_int_norm q = p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. gauss_int_norm q = p
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
prime_elem q
q dvd of_nat p
[PROOF STEP]
obtain r where r: "of_nat p = q * r"
[PROOF STATE]
proof (prove)
using this:
prime_elem q
q dvd of_nat p

goal (1 subgoal):
 1. (\<And>r. of_nat p = q * r \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
of_nat p = q * r

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

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

goal (1 subgoal):
 1. gauss_int_norm q = p
[PROOF STEP]
have "\<dots> = gauss_int_norm q * gauss_int_norm r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gauss_int_norm (of_nat p) = gauss_int_norm q * gauss_int_norm r
[PROOF STEP]
by (auto simp: r gauss_int_norm_mult)
[PROOF STATE]
proof (state)
this:
gauss_int_norm (of_nat p) = gauss_int_norm q * gauss_int_norm r

goal (1 subgoal):
 1. gauss_int_norm q = p
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
p\<^sup>2 = gauss_int_norm q * gauss_int_norm r
[PROOF STEP]
have *: "gauss_int_norm q * gauss_int_norm r = p ^ 2"
[PROOF STATE]
proof (prove)
using this:
p\<^sup>2 = gauss_int_norm q * gauss_int_norm r

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

goal (1 subgoal):
 1. gauss_int_norm q = p
[PROOF STEP]
hence "\<exists>i j. gauss_int_norm q = p ^ i \<and> gauss_int_norm r = p ^ j"
[PROOF STATE]
proof (prove)
using this:
gauss_int_norm q * gauss_int_norm r = p\<^sup>2

goal (1 subgoal):
 1. \<exists>i j. gauss_int_norm q = p ^ i \<and> gauss_int_norm r = p ^ j
[PROOF STEP]
using prime_p
[PROOF STATE]
proof (prove)
using this:
gauss_int_norm q * gauss_int_norm r = p\<^sup>2
prime p

goal (1 subgoal):
 1. \<exists>i j. gauss_int_norm q = p ^ i \<and> gauss_int_norm r = p ^ j
[PROOF STEP]
by (intro prime_power_mult_nat)
[PROOF STATE]
proof (state)
this:
\<exists>i j. gauss_int_norm q = p ^ i \<and> gauss_int_norm r = p ^ j

goal (1 subgoal):
 1. gauss_int_norm q = p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>i j. gauss_int_norm q = p ^ i \<and> gauss_int_norm r = p ^ j
[PROOF STEP]
obtain i j where ij: "gauss_int_norm q = p ^ i" "gauss_int_norm r = p ^ j"
[PROOF STATE]
proof (prove)
using this:
\<exists>i j. gauss_int_norm q = p ^ i \<and> gauss_int_norm r = p ^ j

goal (1 subgoal):
 1. (\<And>i j. \<lbrakk>gauss_int_norm q = p ^ i; gauss_int_norm r = p ^ j\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
gauss_int_norm q = p ^ i
gauss_int_norm r = p ^ j

goal (1 subgoal):
 1. gauss_int_norm q = p
[PROOF STEP]
have ij_eq_2: "i + j = 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i + j = 2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i + j = 2
[PROOF STEP]
from *
[PROOF STATE]
proof (chain)
picking this:
gauss_int_norm q * gauss_int_norm r = p\<^sup>2
[PROOF STEP]
have "p ^ (i + j) = p ^ 2"
[PROOF STATE]
proof (prove)
using this:
gauss_int_norm q * gauss_int_norm r = p\<^sup>2

goal (1 subgoal):
 1. p ^ (i + j) = p\<^sup>2
[PROOF STEP]
by (simp add: power_add ij)
[PROOF STATE]
proof (state)
this:
p ^ (i + j) = p\<^sup>2

goal (1 subgoal):
 1. i + j = 2
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
p ^ (i + j) = p\<^sup>2

goal (1 subgoal):
 1. i + j = 2
[PROOF STEP]
using p_gt_2
[PROOF STATE]
proof (prove)
using this:
p ^ (i + j) = p\<^sup>2
2 < p

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
i + j = 2

goal (1 subgoal):
 1. gauss_int_norm q = p
[PROOF STEP]
hence "i = 0 \<and> j = 2 \<or> i = 1 \<and> j = 1 \<or> i = 2 \<and> j = 0"
[PROOF STATE]
proof (prove)
using this:
i + j = 2

goal (1 subgoal):
 1. i = 0 \<and> j = 2 \<or> i = 1 \<and> j = 1 \<or> i = 2 \<and> j = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i = 0 \<and> j = 2 \<or> i = 1 \<and> j = 1 \<or> i = 2 \<and> j = 0

goal (1 subgoal):
 1. gauss_int_norm q = p
[PROOF STEP]
hence "i = 1"
[PROOF STATE]
proof (prove)
using this:
i = 0 \<and> j = 2 \<or> i = 1 \<and> j = 1 \<or> i = 2 \<and> j = 0

goal (1 subgoal):
 1. i = 1
[PROOF STEP]
proof (elim disjE)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. i = 0 \<and> j = 2 \<Longrightarrow> i = 1
 2. i = 1 \<and> j = 1 \<Longrightarrow> i = 1
 3. i = 2 \<and> j = 0 \<Longrightarrow> i = 1
[PROOF STEP]
assume "i = 2 \<and> j = 0"
[PROOF STATE]
proof (state)
this:
i = 2 \<and> j = 0

goal (3 subgoals):
 1. i = 0 \<and> j = 2 \<Longrightarrow> i = 1
 2. i = 1 \<and> j = 1 \<Longrightarrow> i = 1
 3. i = 2 \<and> j = 0 \<Longrightarrow> i = 1
[PROOF STEP]
hence "is_unit r"
[PROOF STATE]
proof (prove)
using this:
i = 2 \<and> j = 0

goal (1 subgoal):
 1. is_unit r
[PROOF STEP]
using ij
[PROOF STATE]
proof (prove)
using this:
i = 2 \<and> j = 0
gauss_int_norm q = p ^ i
gauss_int_norm r = p ^ j

goal (1 subgoal):
 1. is_unit r
[PROOF STEP]
by (simp add: gauss_int_norm_eq_Suc_0_iff)
[PROOF STATE]
proof (state)
this:
is_unit r

goal (3 subgoals):
 1. i = 0 \<and> j = 2 \<Longrightarrow> i = 1
 2. i = 1 \<and> j = 1 \<Longrightarrow> i = 1
 3. i = 2 \<and> j = 0 \<Longrightarrow> i = 1
[PROOF STEP]
hence "prime_elem (of_nat p :: gauss_int)"
[PROOF STATE]
proof (prove)
using this:
is_unit r

goal (1 subgoal):
 1. prime_elem (of_nat p)
[PROOF STEP]
using \<open>prime_elem q\<close>
[PROOF STATE]
proof (prove)
using this:
is_unit r
prime_elem q

goal (1 subgoal):
 1. prime_elem (of_nat p)
[PROOF STEP]
by (simp add: prime_elem_mult_unit_left r mult.commute[of _ r])
[PROOF STATE]
proof (state)
this:
prime_elem (of_nat p)

goal (3 subgoals):
 1. i = 0 \<and> j = 2 \<Longrightarrow> i = 1
 2. i = 1 \<and> j = 1 \<Longrightarrow> i = 1
 3. i = 2 \<and> j = 0 \<Longrightarrow> i = 1
[PROOF STEP]
with not_prime
[PROOF STATE]
proof (chain)
picking this:
\<not> prime_elem (of_nat p)
prime_elem (of_nat p)
[PROOF STEP]
show "i = 1"
[PROOF STATE]
proof (prove)
using this:
\<not> prime_elem (of_nat p)
prime_elem (of_nat p)

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

goal (2 subgoals):
 1. i = 0 \<and> j = 2 \<Longrightarrow> i = 1
 2. i = 1 \<and> j = 1 \<Longrightarrow> i = 1
[PROOF STEP]
qed (use q ij in \<open>auto simp: gauss_int_norm_eq_Suc_0_iff\<close>)
[PROOF STATE]
proof (state)
this:
i = 1

goal (1 subgoal):
 1. gauss_int_norm q = p
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
i = 1

goal (1 subgoal):
 1. gauss_int_norm q = p
[PROOF STEP]
using ij
[PROOF STATE]
proof (prove)
using this:
i = 1
gauss_int_norm q = p ^ i
gauss_int_norm r = p ^ j

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prime_divisor_exists:
  obtains q where "prime q" "prime_elem (gauss_cnj q)" "ReZ q > 0" "ImZ q > 0"
                  "of_nat p = q * gauss_cnj q" "gauss_int_norm q = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>q. \<lbrakk>prime q; prime_elem (gauss_cnj q); 0 < ReZ q; 0 < ImZ q; of_nat p = q * gauss_cnj q; gauss_int_norm q = p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>q. \<lbrakk>prime q; prime_elem (gauss_cnj q); 0 < ReZ q; 0 < ImZ q; of_nat p = q * gauss_cnj q; gauss_int_norm q = p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "\<exists>q::gauss_int. q dvd of_nat p \<and> prime q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>q. q dvd of_nat p \<and> prime q
[PROOF STEP]
by (rule prime_divisor_exists) (use prime_p in \<open>auto simp: is_unit_gauss_int_iff'\<close>)
[PROOF STATE]
proof (state)
this:
\<exists>q. q dvd of_nat p \<and> prime q

goal (1 subgoal):
 1. (\<And>q. \<lbrakk>prime q; prime_elem (gauss_cnj q); 0 < ReZ q; 0 < ImZ q; of_nat p = q * gauss_cnj q; gauss_int_norm q = p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>q. q dvd of_nat p \<and> prime q
[PROOF STEP]
obtain q :: gauss_int where q: "prime q" "q dvd of_nat p"
[PROOF STATE]
proof (prove)
using this:
\<exists>q. q dvd of_nat p \<and> prime q

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

goal (1 subgoal):
 1. (\<And>q. \<lbrakk>prime q; prime_elem (gauss_cnj q); 0 < ReZ q; 0 < ImZ q; of_nat p = q * gauss_cnj q; gauss_int_norm q = p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from \<open>prime q\<close>
[PROOF STATE]
proof (chain)
picking this:
prime q
[PROOF STEP]
have [simp]: "q \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
prime q

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

goal (1 subgoal):
 1. (\<And>q. \<lbrakk>prime q; prime_elem (gauss_cnj q); 0 < ReZ q; 0 < ImZ q; of_nat p = q * gauss_cnj q; gauss_int_norm q = p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "normalize q = q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. normalize q = q
[PROOF STEP]
using q
[PROOF STATE]
proof (prove)
using this:
prime q
q dvd of_nat p

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

goal (1 subgoal):
 1. (\<And>q. \<lbrakk>prime q; prime_elem (gauss_cnj q); 0 < ReZ q; 0 < ImZ q; of_nat p = q * gauss_cnj q; gauss_int_norm q = p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence q_signs: "ReZ q > 0" "ImZ q \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
normalize q = q

goal (1 subgoal):
 1. 0 < ReZ q &&& 0 \<le> ImZ q
[PROOF STEP]
by (subst (asm) normalized_gauss_int_iff; simp)+
[PROOF STATE]
proof (state)
this:
0 < ReZ q
0 \<le> ImZ q

goal (1 subgoal):
 1. (\<And>q. \<lbrakk>prime q; prime_elem (gauss_cnj q); 0 < ReZ q; 0 < ImZ q; of_nat p = q * gauss_cnj q; gauss_int_norm q = p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from q
[PROOF STATE]
proof (chain)
picking this:
prime q
q dvd of_nat p
[PROOF STEP]
have "gauss_int_norm q = p"
[PROOF STATE]
proof (prove)
using this:
prime q
q dvd of_nat p

goal (1 subgoal):
 1. gauss_int_norm q = p
[PROOF STEP]
using norm_prime_divisor[of q]
[PROOF STATE]
proof (prove)
using this:
prime q
q dvd of_nat p
\<lbrakk>prime_elem q; q dvd of_nat p\<rbrakk> \<Longrightarrow> gauss_int_norm q = p

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

goal (1 subgoal):
 1. (\<And>q. \<lbrakk>prime q; prime_elem (gauss_cnj q); 0 < ReZ q; 0 < ImZ q; of_nat p = q * gauss_cnj q; gauss_int_norm q = p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
gauss_int_norm q = p

goal (1 subgoal):
 1. (\<And>q. \<lbrakk>prime q; prime_elem (gauss_cnj q); 0 < ReZ q; 0 < ImZ q; of_nat p = q * gauss_cnj q; gauss_int_norm q = p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
gauss_int_norm q = p
[PROOF STEP]
have "gauss_int_norm (gauss_cnj q) = p"
[PROOF STATE]
proof (prove)
using this:
gauss_int_norm q = p

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

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

goal (1 subgoal):
 1. prime_elem (gauss_cnj q)
[PROOF STEP]
using prime_p
[PROOF STATE]
proof (prove)
using this:
gauss_int_norm (gauss_cnj q) = p
prime p

goal (1 subgoal):
 1. prime_elem (gauss_cnj q)
[PROOF STEP]
by (intro prime_gauss_int_norm_imp_prime_elem) auto
[PROOF STATE]
proof (state)
this:
prime_elem (gauss_cnj q)

goal (1 subgoal):
 1. (\<And>q. \<lbrakk>prime q; prime_elem (gauss_cnj q); 0 < ReZ q; 0 < ImZ q; of_nat p = q * gauss_cnj q; gauss_int_norm q = p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
prime_elem (gauss_cnj q)

goal (1 subgoal):
 1. (\<And>q. \<lbrakk>prime q; prime_elem (gauss_cnj q); 0 < ReZ q; 0 < ImZ q; of_nat p = q * gauss_cnj q; gauss_int_norm q = p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "of_nat p = q * gauss_cnj q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_nat p = q * gauss_cnj q
[PROOF STEP]
using \<open>gauss_int_norm q = p\<close>
[PROOF STATE]
proof (prove)
using this:
gauss_int_norm q = p

goal (1 subgoal):
 1. of_nat p = q * gauss_cnj q
[PROOF STEP]
by (simp add: self_mult_gauss_cnj)
[PROOF STATE]
proof (state)
this:
of_nat p = q * gauss_cnj q

goal (1 subgoal):
 1. (\<And>q. \<lbrakk>prime q; prime_elem (gauss_cnj q); 0 < ReZ q; 0 < ImZ q; of_nat p = q * gauss_cnj q; gauss_int_norm q = p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
of_nat p = q * gauss_cnj q

goal (1 subgoal):
 1. (\<And>q. \<lbrakk>prime q; prime_elem (gauss_cnj q); 0 < ReZ q; 0 < ImZ q; of_nat p = q * gauss_cnj q; gauss_int_norm q = p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "ImZ q \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ImZ q \<noteq> 0
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ImZ q = 0 \<Longrightarrow> False
[PROOF STEP]
assume [simp]: "ImZ q = 0"
[PROOF STATE]
proof (state)
this:
ImZ q = 0

goal (1 subgoal):
 1. ImZ q = 0 \<Longrightarrow> False
[PROOF STEP]
define m where "m = nat (ReZ q)"
[PROOF STATE]
proof (state)
this:
m = nat (ReZ q)

goal (1 subgoal):
 1. ImZ q = 0 \<Longrightarrow> False
[PROOF STEP]
have [simp]: "q = of_nat m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q = of_nat m
[PROOF STEP]
using q_signs
[PROOF STATE]
proof (prove)
using this:
0 < ReZ q
0 \<le> ImZ q

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

goal (1 subgoal):
 1. ImZ q = 0 \<Longrightarrow> False
[PROOF STEP]
with q
[PROOF STATE]
proof (chain)
picking this:
prime q
q dvd of_nat p
q = of_nat m
[PROOF STEP]
have "m dvd p"
[PROOF STATE]
proof (prove)
using this:
prime q
q dvd of_nat p
q = of_nat m

goal (1 subgoal):
 1. m dvd p
[PROOF STEP]
by (simp add: of_nat_dvd_of_nat_gauss_int_iff)
[PROOF STATE]
proof (state)
this:
m dvd p

goal (1 subgoal):
 1. ImZ q = 0 \<Longrightarrow> False
[PROOF STEP]
with prime_p
[PROOF STATE]
proof (chain)
picking this:
prime p
m dvd p
[PROOF STEP]
have "m = 1 \<or> m = p"
[PROOF STATE]
proof (prove)
using this:
prime p
m dvd p

goal (1 subgoal):
 1. m = 1 \<or> m = p
[PROOF STEP]
using prime_nat_iff
[PROOF STATE]
proof (prove)
using this:
prime p
m dvd p
prime ?n = (1 < ?n \<and> (\<forall>m. m dvd ?n \<longrightarrow> m = 1 \<or> m = ?n))

goal (1 subgoal):
 1. m = 1 \<or> m = p
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
m = 1 \<or> m = p

goal (1 subgoal):
 1. ImZ q = 0 \<Longrightarrow> False
[PROOF STEP]
with q
[PROOF STATE]
proof (chain)
picking this:
prime q
q dvd of_nat p
m = 1 \<or> m = p
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
prime q
q dvd of_nat p
m = 1 \<or> m = p

goal (1 subgoal):
 1. False
[PROOF STEP]
using not_prime
[PROOF STATE]
proof (prove)
using this:
prime q
q dvd of_nat p
m = 1 \<or> m = p
\<not> prime_elem (of_nat p)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ImZ q \<noteq> 0

goal (1 subgoal):
 1. (\<And>q. \<lbrakk>prime q; prime_elem (gauss_cnj q); 0 < ReZ q; 0 < ImZ q; of_nat p = q * gauss_cnj q; gauss_int_norm q = p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with q_signs
[PROOF STATE]
proof (chain)
picking this:
0 < ReZ q
0 \<le> ImZ q
ImZ q \<noteq> 0
[PROOF STEP]
have "ImZ q > 0"
[PROOF STATE]
proof (prove)
using this:
0 < ReZ q
0 \<le> ImZ q
ImZ q \<noteq> 0

goal (1 subgoal):
 1. 0 < ImZ q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < ImZ q

goal (1 subgoal):
 1. (\<And>q. \<lbrakk>prime q; prime_elem (gauss_cnj q); 0 < ReZ q; 0 < ImZ q; of_nat p = q * gauss_cnj q; gauss_int_norm q = p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
gauss_int_norm q = p
prime_elem (gauss_cnj q)
of_nat p = q * gauss_cnj q
0 < ImZ q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
gauss_int_norm q = p
prime_elem (gauss_cnj q)
of_nat p = q * gauss_cnj q
0 < ImZ q

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using q q_signs
[PROOF STATE]
proof (prove)
using this:
gauss_int_norm q = p
prime_elem (gauss_cnj q)
of_nat p = q * gauss_cnj q
0 < ImZ q
prime q
q dvd of_nat p
0 < ReZ q
0 \<le> ImZ q

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem prime_factorization:
  obtains q1 q2
  where "prime q1" "prime q2" "prime_factorization (of_nat p) = {#q1, q2#}"
        "gauss_int_norm q1 = p" "gauss_int_norm q2 = p" "q2 = \<i>\<^sub>\<int> * gauss_cnj q1"
        "ReZ q1 > 0" "ImZ q1 > 0" "ReZ q1 > 0" "ImZ q2 > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>q1 q2. \<lbrakk>prime q1; prime q2; prime_factorization (of_nat p) = {#q1, q2#}; gauss_int_norm q1 = p; gauss_int_norm q2 = p; q2 = \<i>\<^sub>\<int> * gauss_cnj q1; 0 < ReZ q1; 0 < ImZ q1; 0 < ReZ q1; 0 < ImZ q2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>q1 q2. \<lbrakk>prime q1; prime q2; prime_factorization (of_nat p) = {#q1, q2#}; gauss_int_norm q1 = p; gauss_int_norm q2 = p; q2 = \<i>\<^sub>\<int> * gauss_cnj q1; 0 < ReZ q1; 0 < ImZ q1; 0 < ReZ q1; 0 < ImZ q2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain q where q: "prime q" "prime_elem (gauss_cnj q)" "ReZ q > 0" "ImZ q > 0"
                    "of_nat p = q * gauss_cnj q" "gauss_int_norm q = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>q. \<lbrakk>prime q; prime_elem (gauss_cnj q); 0 < ReZ q; 0 < ImZ q; of_nat p = q * gauss_cnj q; gauss_int_norm q = p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prime_divisor_exists
[PROOF STATE]
proof (prove)
using this:
(\<And>q. \<lbrakk>prime q; prime_elem (gauss_cnj q); 0 < ReZ q; 0 < ImZ q; of_nat p = q * gauss_cnj q; gauss_int_norm q = p\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>q. \<lbrakk>prime q; prime_elem (gauss_cnj q); 0 < ReZ q; 0 < ImZ q; of_nat p = q * gauss_cnj q; gauss_int_norm q = p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
prime q
prime_elem (gauss_cnj q)
0 < ReZ q
0 < ImZ q
of_nat p = q * gauss_cnj q
gauss_int_norm q = p

goal (1 subgoal):
 1. (\<And>q1 q2. \<lbrakk>prime q1; prime q2; prime_factorization (of_nat p) = {#q1, q2#}; gauss_int_norm q1 = p; gauss_int_norm q2 = p; q2 = \<i>\<^sub>\<int> * gauss_cnj q1; 0 < ReZ q1; 0 < ImZ q1; 0 < ReZ q1; 0 < ImZ q2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from \<open>prime q\<close>
[PROOF STATE]
proof (chain)
picking this:
prime q
[PROOF STEP]
have [simp]: "q \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
prime q

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

goal (1 subgoal):
 1. (\<And>q1 q2. \<lbrakk>prime q1; prime q2; prime_factorization (of_nat p) = {#q1, q2#}; gauss_int_norm q1 = p; gauss_int_norm q2 = p; q2 = \<i>\<^sub>\<int> * gauss_cnj q1; 0 < ReZ q1; 0 < ImZ q1; 0 < ReZ q1; 0 < ImZ q2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define q' where "q' = normalize (gauss_cnj q)"
[PROOF STATE]
proof (state)
this:
q' = normalize (gauss_cnj q)

goal (1 subgoal):
 1. (\<And>q1 q2. \<lbrakk>prime q1; prime q2; prime_factorization (of_nat p) = {#q1, q2#}; gauss_int_norm q1 = p; gauss_int_norm q2 = p; q2 = \<i>\<^sub>\<int> * gauss_cnj q1; 0 < ReZ q1; 0 < ImZ q1; 0 < ReZ q1; 0 < ImZ q2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "prime_factorization (of_nat p) = prime_factorization (prod_mset {#q, q'#})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime_factorization (of_nat p) = prime_factorization (\<Prod>\<^sub># {#q, q'#})
[PROOF STEP]
by (subst prime_factorization_unique) (auto simp: q q'_def)
[PROOF STATE]
proof (state)
this:
prime_factorization (of_nat p) = prime_factorization (\<Prod>\<^sub># {#q, q'#})

goal (1 subgoal):
 1. (\<And>q1 q2. \<lbrakk>prime q1; prime q2; prime_factorization (of_nat p) = {#q1, q2#}; gauss_int_norm q1 = p; gauss_int_norm q2 = p; q2 = \<i>\<^sub>\<int> * gauss_cnj q1; 0 < ReZ q1; 0 < ImZ q1; 0 < ReZ q1; 0 < ImZ q2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
prime_factorization (of_nat p) = prime_factorization (\<Prod>\<^sub># {#q, q'#})

goal (1 subgoal):
 1. (\<And>q1 q2. \<lbrakk>prime q1; prime q2; prime_factorization (of_nat p) = {#q1, q2#}; gauss_int_norm q1 = p; gauss_int_norm q2 = p; q2 = \<i>\<^sub>\<int> * gauss_cnj q1; 0 < ReZ q1; 0 < ImZ q1; 0 < ReZ q1; 0 < ImZ q2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "\<dots> = {#q, q'#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime_factorization (\<Prod>\<^sub># {#q, q'#}) = {#q, q'#}
[PROOF STEP]
using q
[PROOF STATE]
proof (prove)
using this:
prime q
prime_elem (gauss_cnj q)
0 < ReZ q
0 < ImZ q
of_nat p = q * gauss_cnj q
gauss_int_norm q = p

goal (1 subgoal):
 1. prime_factorization (\<Prod>\<^sub># {#q, q'#}) = {#q, q'#}
[PROOF STEP]
by (subst prime_factorization_prod_mset_primes) (auto simp: q'_def)
[PROOF STATE]
proof (state)
this:
prime_factorization (\<Prod>\<^sub># {#q, q'#}) = {#q, q'#}

goal (1 subgoal):
 1. (\<And>q1 q2. \<lbrakk>prime q1; prime q2; prime_factorization (of_nat p) = {#q1, q2#}; gauss_int_norm q1 = p; gauss_int_norm q2 = p; q2 = \<i>\<^sub>\<int> * gauss_cnj q1; 0 < ReZ q1; 0 < ImZ q1; 0 < ReZ q1; 0 < ImZ q2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
prime_factorization (of_nat p) = {#q, q'#}
[PROOF STEP]
have "prime_factorization (of_nat p) = {#q, q'#}"
[PROOF STATE]
proof (prove)
using this:
prime_factorization (of_nat p) = {#q, q'#}

goal (1 subgoal):
 1. prime_factorization (of_nat p) = {#q, q'#}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
prime_factorization (of_nat p) = {#q, q'#}

goal (1 subgoal):
 1. (\<And>q1 q2. \<lbrakk>prime q1; prime q2; prime_factorization (of_nat p) = {#q1, q2#}; gauss_int_norm q1 = p; gauss_int_norm q2 = p; q2 = \<i>\<^sub>\<int> * gauss_cnj q1; 0 < ReZ q1; 0 < ImZ q1; 0 < ReZ q1; 0 < ImZ q2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
prime_factorization (of_nat p) = {#q, q'#}

goal (1 subgoal):
 1. (\<And>q1 q2. \<lbrakk>prime q1; prime q2; prime_factorization (of_nat p) = {#q1, q2#}; gauss_int_norm q1 = p; gauss_int_norm q2 = p; q2 = \<i>\<^sub>\<int> * gauss_cnj q1; 0 < ReZ q1; 0 < ImZ q1; 0 < ReZ q1; 0 < ImZ q2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "q' = \<i>\<^sub>\<int> * gauss_cnj q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q' = \<i>\<^sub>\<int> * gauss_cnj q
[PROOF STEP]
using q
[PROOF STATE]
proof (prove)
using this:
prime q
prime_elem (gauss_cnj q)
0 < ReZ q
0 < ImZ q
of_nat p = q * gauss_cnj q
gauss_int_norm q = p

goal (1 subgoal):
 1. q' = \<i>\<^sub>\<int> * gauss_cnj q
[PROOF STEP]
by (auto simp: normalize_gauss_int_def q'_def)
[PROOF STATE]
proof (state)
this:
q' = \<i>\<^sub>\<int> * gauss_cnj q

goal (1 subgoal):
 1. (\<And>q1 q2. \<lbrakk>prime q1; prime q2; prime_factorization (of_nat p) = {#q1, q2#}; gauss_int_norm q1 = p; gauss_int_norm q2 = p; q2 = \<i>\<^sub>\<int> * gauss_cnj q1; 0 < ReZ q1; 0 < ImZ q1; 0 < ReZ q1; 0 < ImZ q2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
q' = \<i>\<^sub>\<int> * gauss_cnj q

goal (1 subgoal):
 1. (\<And>q1 q2. \<lbrakk>prime q1; prime q2; prime_factorization (of_nat p) = {#q1, q2#}; gauss_int_norm q1 = p; gauss_int_norm q2 = p; q2 = \<i>\<^sub>\<int> * gauss_cnj q1; 0 < ReZ q1; 0 < ImZ q1; 0 < ReZ q1; 0 < ImZ q2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "prime q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime q'
[PROOF STEP]
using q
[PROOF STATE]
proof (prove)
using this:
prime q
prime_elem (gauss_cnj q)
0 < ReZ q
0 < ImZ q
of_nat p = q * gauss_cnj q
gauss_int_norm q = p

goal (1 subgoal):
 1. prime q'
[PROOF STEP]
by (auto simp: q'_def)
[PROOF STATE]
proof (state)
this:
prime q'

goal (1 subgoal):
 1. (\<And>q1 q2. \<lbrakk>prime q1; prime q2; prime_factorization (of_nat p) = {#q1, q2#}; gauss_int_norm q1 = p; gauss_int_norm q2 = p; q2 = \<i>\<^sub>\<int> * gauss_cnj q1; 0 < ReZ q1; 0 < ImZ q1; 0 < ReZ q1; 0 < ImZ q2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
prime_factorization (of_nat p) = {#q, q'#}
q' = \<i>\<^sub>\<int> * gauss_cnj q
prime q'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
prime_factorization (of_nat p) = {#q, q'#}
q' = \<i>\<^sub>\<int> * gauss_cnj q
prime q'

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using q
[PROOF STATE]
proof (prove)
using this:
prime_factorization (of_nat p) = {#q, q'#}
q' = \<i>\<^sub>\<int> * gauss_cnj q
prime q'
prime q
prime_elem (gauss_cnj q)
0 < ReZ q
0 < ImZ q
of_nat p = q * gauss_cnj q
gauss_int_norm q = p

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (intro that[of q q']) (auto simp: q'_def gauss_int_norm_mult)
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prime_cong_1_mod_4_gauss_int_norm_exists:
  fixes p :: nat
  assumes "prime p" "[p = 1] (mod 4)"
  shows   "\<exists>z. gauss_int_norm z = p \<and> ReZ z > 0 \<and> ImZ z > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>z. gauss_int_norm z = p \<and> 0 < ReZ z \<and> 0 < ImZ z
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>z. gauss_int_norm z = p \<and> 0 < ReZ z \<and> 0 < ImZ z
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
prime p
[p = 1] (mod 4)
[PROOF STEP]
interpret noninert_gauss_int_prime p
[PROOF STATE]
proof (prove)
using this:
prime p
[p = 1] (mod 4)

goal (1 subgoal):
 1. noninert_gauss_int_prime p
[PROOF STEP]
by unfold_locales
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>z. gauss_int_norm z = p \<and> 0 < ReZ z \<and> 0 < ImZ z
[PROOF STEP]
from prime_divisor_exists
[PROOF STATE]
proof (chain)
picking this:
(\<And>q. \<lbrakk>prime q; prime_elem (gauss_cnj q); 0 < ReZ q; 0 < ImZ q; of_nat p = q * gauss_cnj q; gauss_int_norm q = p\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain q
    where q: "prime q" "of_nat p = q * gauss_cnj q"
             "ReZ q > 0" "ImZ q > 0" "gauss_int_norm q = p"
[PROOF STATE]
proof (prove)
using this:
(\<And>q. \<lbrakk>prime q; prime_elem (gauss_cnj q); 0 < ReZ q; 0 < ImZ q; of_nat p = q * gauss_cnj q; gauss_int_norm q = p\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>q. \<lbrakk>prime q; of_nat p = q * gauss_cnj q; 0 < ReZ q; 0 < ImZ q; gauss_int_norm q = p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
prime q
of_nat p = q * gauss_cnj q
0 < ReZ q
0 < ImZ q
gauss_int_norm q = p

goal (1 subgoal):
 1. \<exists>z. gauss_int_norm z = p \<and> 0 < ReZ z \<and> 0 < ImZ z
[PROOF STEP]
have "p = gauss_int_norm q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p = gauss_int_norm q
[PROOF STEP]
using q
[PROOF STATE]
proof (prove)
using this:
prime q
of_nat p = q * gauss_cnj q
0 < ReZ q
0 < ImZ q
gauss_int_norm q = p

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

goal (1 subgoal):
 1. \<exists>z. gauss_int_norm z = p \<and> 0 < ReZ z \<and> 0 < ImZ z
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
p = gauss_int_norm q

goal (1 subgoal):
 1. \<exists>z. gauss_int_norm z = p \<and> 0 < ReZ z \<and> 0 < ImZ z
[PROOF STEP]
using q
[PROOF STATE]
proof (prove)
using this:
p = gauss_int_norm q
prime q
of_nat p = q * gauss_cnj q
0 < ReZ q
0 < ImZ q
gauss_int_norm q = p

goal (1 subgoal):
 1. \<exists>z. gauss_int_norm z = p \<and> 0 < ReZ z \<and> 0 < ImZ z
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>z. gauss_int_norm z = p \<and> 0 < ReZ z \<and> 0 < ImZ z

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem gauss_int_prime_classification:
  fixes x :: gauss_int
  assumes "prime x"
  obtains
    (one_plus_i) "x = 1 + \<i>\<^sub>\<int>"
  | (cong_3_mod_4) p where "x = of_nat p" "prime p" "[p = 3] (mod 4)"
  | (cong_1_mod_4) "prime (gauss_int_norm x)" "[gauss_int_norm x = 1] (mod 4)"
                   "ReZ x > 0" "ImZ x > 0" "ReZ x \<noteq> ImZ x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = 1 + \<i>\<^sub>\<int> \<Longrightarrow> thesis; \<And>p. \<lbrakk>x = of_nat p; prime p; [p = 3] (mod 4)\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>prime (gauss_int_norm x); [gauss_int_norm x = 1] (mod 4); 0 < ReZ x; 0 < ImZ x; ReZ x \<noteq> ImZ x\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>x = 1 + \<i>\<^sub>\<int> \<Longrightarrow> thesis; \<And>p. \<lbrakk>x = of_nat p; prime p; [p = 3] (mod 4)\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>prime (gauss_int_norm x); [gauss_int_norm x = 1] (mod 4); 0 < ReZ x; 0 < ImZ x; ReZ x \<noteq> ImZ x\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
define N where "N = gauss_int_norm x"
[PROOF STATE]
proof (state)
this:
N = gauss_int_norm x

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

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

goal (1 subgoal):
 1. \<lbrakk>x = 1 + \<i>\<^sub>\<int> \<Longrightarrow> thesis; \<And>p. \<lbrakk>x = of_nat p; prime p; [p = 3] (mod 4)\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>prime (gauss_int_norm x); [gauss_int_norm x = 1] (mod 4); 0 < ReZ x; 0 < ImZ x; ReZ x \<noteq> ImZ x\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have "\<dots> = of_nat (gauss_int_norm x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * gauss_cnj x = of_nat (gauss_int_norm x)
[PROOF STEP]
by (simp add: self_mult_gauss_cnj)
[PROOF STATE]
proof (state)
this:
x * gauss_cnj x = of_nat (gauss_int_norm x)

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

goal (1 subgoal):
 1. x \<in># prime_factorization (of_nat N)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x dvd of_nat (gauss_int_norm x)
prime x

goal (1 subgoal):
 1. x \<in># prime_factorization (of_nat N)
[PROOF STEP]
by (auto simp: in_prime_factors_iff N_def)
[PROOF STATE]
proof (state)
this:
x \<in># prime_factorization (of_nat N)

goal (1 subgoal):
 1. \<lbrakk>x = 1 + \<i>\<^sub>\<int> \<Longrightarrow> thesis; \<And>p. \<lbrakk>x = of_nat p; prime p; [p = 3] (mod 4)\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>prime (gauss_int_norm x); [gauss_int_norm x = 1] (mod 4); 0 < ReZ x; 0 < ImZ x; ReZ x \<noteq> ImZ x\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x \<in># prime_factorization (of_nat N)

goal (1 subgoal):
 1. \<lbrakk>x = 1 + \<i>\<^sub>\<int> \<Longrightarrow> thesis; \<And>p. \<lbrakk>x = of_nat p; prime p; [p = 3] (mod 4)\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>prime (gauss_int_norm x); [gauss_int_norm x = 1] (mod 4); 0 < ReZ x; 0 < ImZ x; ReZ x \<noteq> ImZ x\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have "N = prod_mset (prime_factorization N)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. N = \<Prod>\<^sub># (prime_factorization N)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
prime x

goal (1 subgoal):
 1. N = \<Prod>\<^sub># (prime_factorization N)
[PROOF STEP]
unfolding N_def
[PROOF STATE]
proof (prove)
using this:
prime x

goal (1 subgoal):
 1. gauss_int_norm x = \<Prod>\<^sub># (prime_factorization (gauss_int_norm x))
[PROOF STEP]
by (subst prod_mset_prime_factorization_nat) auto
[PROOF STATE]
proof (state)
this:
N = \<Prod>\<^sub># (prime_factorization N)

goal (1 subgoal):
 1. \<lbrakk>x = 1 + \<i>\<^sub>\<int> \<Longrightarrow> thesis; \<And>p. \<lbrakk>x = of_nat p; prime p; [p = 3] (mod 4)\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>prime (gauss_int_norm x); [gauss_int_norm x = 1] (mod 4); 0 < ReZ x; 0 < ImZ x; ReZ x \<noteq> ImZ x\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
N = \<Prod>\<^sub># (prime_factorization N)

goal (1 subgoal):
 1. \<lbrakk>x = 1 + \<i>\<^sub>\<int> \<Longrightarrow> thesis; \<And>p. \<lbrakk>x = of_nat p; prime p; [p = 3] (mod 4)\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>prime (gauss_int_norm x); [gauss_int_norm x = 1] (mod 4); 0 < ReZ x; 0 < ImZ x; ReZ x \<noteq> ImZ x\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have "(of_nat \<dots> :: gauss_int) =
               prod_mset (image_mset of_nat (prime_factorization N))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_nat (\<Prod>\<^sub># (prime_factorization N)) = \<Prod>\<^sub># (image_mset of_nat (prime_factorization N))
[PROOF STEP]
by (subst of_nat_prod_mset) auto
[PROOF STATE]
proof (state)
this:
of_nat (\<Prod>\<^sub># (prime_factorization N)) = \<Prod>\<^sub># (image_mset of_nat (prime_factorization N))

goal (1 subgoal):
 1. \<lbrakk>x = 1 + \<i>\<^sub>\<int> \<Longrightarrow> thesis; \<And>p. \<lbrakk>x = of_nat p; prime p; [p = 3] (mod 4)\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>prime (gauss_int_norm x); [gauss_int_norm x = 1] (mod 4); 0 < ReZ x; 0 < ImZ x; ReZ x \<noteq> ImZ x\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
of_nat (\<Prod>\<^sub># (prime_factorization N)) = \<Prod>\<^sub># (image_mset of_nat (prime_factorization N))

goal (1 subgoal):
 1. \<lbrakk>x = 1 + \<i>\<^sub>\<int> \<Longrightarrow> thesis; \<And>p. \<lbrakk>x = of_nat p; prime p; [p = 3] (mod 4)\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>prime (gauss_int_norm x); [gauss_int_norm x = 1] (mod 4); 0 < ReZ x; 0 < ImZ x; ReZ x \<noteq> ImZ x\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have "prime_factors \<dots> = (\<Union>p\<in>prime_factors N. prime_factors (of_nat p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime_factors (\<Prod>\<^sub># (image_mset of_nat (prime_factorization N))) = (\<Union>p\<in>prime_factors N. prime_factors (of_nat p))
[PROOF STEP]
by (subst prime_factorization_prod_mset) auto
[PROOF STATE]
proof (state)
this:
prime_factors (\<Prod>\<^sub># (image_mset of_nat (prime_factorization N))) = (\<Union>p\<in>prime_factors N. prime_factors (of_nat p))

goal (1 subgoal):
 1. \<lbrakk>x = 1 + \<i>\<^sub>\<int> \<Longrightarrow> thesis; \<And>p. \<lbrakk>x = of_nat p; prime p; [p = 3] (mod 4)\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>prime (gauss_int_norm x); [gauss_int_norm x = 1] (mod 4); 0 < ReZ x; 0 < ImZ x; ReZ x \<noteq> ImZ x\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x \<in> (\<Union>p\<in>prime_factors N. prime_factors (of_nat p))
[PROOF STEP]
obtain p where p: "p \<in> prime_factors N" "x \<in> prime_factors (of_nat p)"
[PROOF STATE]
proof (prove)
using this:
x \<in> (\<Union>p\<in>prime_factors N. prime_factors (of_nat p))

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p \<in># prime_factorization N; x \<in># prime_factorization (of_nat p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p \<in># prime_factorization N
x \<in># prime_factorization (of_nat p)

goal (1 subgoal):
 1. \<lbrakk>x = 1 + \<i>\<^sub>\<int> \<Longrightarrow> thesis; \<And>p. \<lbrakk>x = of_nat p; prime p; [p = 3] (mod 4)\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>prime (gauss_int_norm x); [gauss_int_norm x = 1] (mod 4); 0 < ReZ x; 0 < ImZ x; ReZ x \<noteq> ImZ x\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have "prime p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime p
[PROOF STEP]
using p
[PROOF STATE]
proof (prove)
using this:
p \<in># prime_factorization N
x \<in># prime_factorization (of_nat p)

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

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

goal (1 subgoal):
 1. \<not> 2 * 2 dvd p
[PROOF STEP]
using product_dvd_irreducibleD[of p 2 2]
[PROOF STATE]
proof (prove)
using this:
prime p
\<lbrakk>irreducible p; 2 * 2 dvd p\<rbrakk> \<Longrightarrow> is_unit 2 \<or> is_unit 2

goal (1 subgoal):
 1. \<not> 2 * 2 dvd p
[PROOF STEP]
by (auto simp flip: prime_elem_iff_irreducible)
[PROOF STATE]
proof (state)
this:
\<not> 2 * 2 dvd p

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

goal (1 subgoal):
 1. [p \<noteq> 0] (mod 4)
[PROOF STEP]
using p
[PROOF STATE]
proof (prove)
using this:
\<not> 2 * 2 dvd p
p \<in># prime_factorization N
x \<in># prime_factorization (of_nat p)

goal (1 subgoal):
 1. [p \<noteq> 0] (mod 4)
[PROOF STEP]
by (auto simp: cong_0_iff in_prime_factors_iff)
[PROOF STATE]
proof (state)
this:
[p \<noteq> 0] (mod 4)

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

goal (1 subgoal):
 1. p mod 4 \<in> {1, 2, 3}
[PROOF STEP]
by (auto simp: cong_def)
[PROOF STATE]
proof (state)
this:
p mod 4 \<in> {1, 2, 3}

goal (1 subgoal):
 1. \<lbrakk>x = 1 + \<i>\<^sub>\<int> \<Longrightarrow> thesis; \<And>p. \<lbrakk>x = of_nat p; prime p; [p = 3] (mod 4)\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>prime (gauss_int_norm x); [gauss_int_norm x = 1] (mod 4); 0 < ReZ x; 0 < ImZ x; ReZ x \<noteq> ImZ x\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
p mod 4 \<in> {1, 2, 3}

goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof (elim singletonE insertE)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. p mod 4 = 1 \<Longrightarrow> thesis
 2. p mod 4 = 2 \<Longrightarrow> thesis
 3. p mod 4 = 3 \<Longrightarrow> thesis
[PROOF STEP]
assume "p mod 4 = 2"
[PROOF STATE]
proof (state)
this:
p mod 4 = 2

goal (3 subgoals):
 1. p mod 4 = 1 \<Longrightarrow> thesis
 2. p mod 4 = 2 \<Longrightarrow> thesis
 3. p mod 4 = 3 \<Longrightarrow> thesis
[PROOF STEP]
hence "p mod 4 mod 2 = 0"
[PROOF STATE]
proof (prove)
using this:
p mod 4 = 2

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

goal (3 subgoals):
 1. p mod 4 = 1 \<Longrightarrow> thesis
 2. p mod 4 = 2 \<Longrightarrow> thesis
 3. p mod 4 = 3 \<Longrightarrow> thesis
[PROOF STEP]
hence "p mod 2 = 0"
[PROOF STATE]
proof (prove)
using this:
p mod 4 mod 2 = 0

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

goal (3 subgoals):
 1. p mod 4 = 1 \<Longrightarrow> thesis
 2. p mod 4 = 2 \<Longrightarrow> thesis
 3. p mod 4 = 3 \<Longrightarrow> thesis
[PROOF STEP]
with \<open>prime p\<close>
[PROOF STATE]
proof (chain)
picking this:
prime p
p mod 2 = 0
[PROOF STEP]
have [simp]: "p = 2"
[PROOF STATE]
proof (prove)
using this:
prime p
p mod 2 = 0

goal (1 subgoal):
 1. p = 2
[PROOF STEP]
using prime_prime_factor two_is_prime_nat
[PROOF STATE]
proof (prove)
using this:
prime p
p mod 2 = 0
prime ?n = (?n \<noteq> 1 \<and> (\<forall>p. prime p \<and> p dvd ?n \<longrightarrow> p = ?n))
prime 2

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

goal (3 subgoals):
 1. p mod 4 = 1 \<Longrightarrow> thesis
 2. p mod 4 = 2 \<Longrightarrow> thesis
 3. p mod 4 = 3 \<Longrightarrow> thesis
[PROOF STEP]
have "prime_factors (of_nat p) = {1 + \<i>\<^sub>\<int> :: gauss_int}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime_factors (of_nat p) = {1 + \<i>\<^sub>\<int>}
[PROOF STEP]
by (simp add: prime_factorization_2_gauss_int)
[PROOF STATE]
proof (state)
this:
prime_factors (of_nat p) = {1 + \<i>\<^sub>\<int>}

goal (3 subgoals):
 1. p mod 4 = 1 \<Longrightarrow> thesis
 2. p mod 4 = 2 \<Longrightarrow> thesis
 3. p mod 4 = 3 \<Longrightarrow> thesis
[PROOF STEP]
with p
[PROOF STATE]
proof (chain)
picking this:
p \<in># prime_factorization N
x \<in># prime_factorization (of_nat p)
prime_factors (of_nat p) = {1 + \<i>\<^sub>\<int>}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p \<in># prime_factorization N
x \<in># prime_factorization (of_nat p)
prime_factors (of_nat p) = {1 + \<i>\<^sub>\<int>}

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that(1)
[PROOF STATE]
proof (prove)
using this:
p \<in># prime_factorization N
x \<in># prime_factorization (of_nat p)
prime_factors (of_nat p) = {1 + \<i>\<^sub>\<int>}
x = 1 + \<i>\<^sub>\<int> \<Longrightarrow> thesis

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

goal (2 subgoals):
 1. p mod 4 = 1 \<Longrightarrow> thesis
 2. p mod 4 = 3 \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p mod 4 = 1 \<Longrightarrow> thesis
 2. p mod 4 = 3 \<Longrightarrow> thesis
[PROOF STEP]
assume *: "p mod 4 = 3"
[PROOF STATE]
proof (state)
this:
p mod 4 = 3

goal (2 subgoals):
 1. p mod 4 = 1 \<Longrightarrow> thesis
 2. p mod 4 = 3 \<Longrightarrow> thesis
[PROOF STEP]
hence "prime_factors (of_nat p) = {of_nat p :: gauss_int}"
[PROOF STATE]
proof (prove)
using this:
p mod 4 = 3

goal (1 subgoal):
 1. prime_factors (of_nat p) = {of_nat p}
[PROOF STEP]
using prime_gauss_int_of_nat[of p] \<open>prime p\<close>
[PROOF STATE]
proof (prove)
using this:
p mod 4 = 3
\<lbrakk>prime p; [p = 3] (mod 4)\<rbrakk> \<Longrightarrow> prime (of_nat p)
prime p

goal (1 subgoal):
 1. prime_factors (of_nat p) = {of_nat p}
[PROOF STEP]
by (subst prime_factorization_prime) (auto simp: cong_def)
[PROOF STATE]
proof (state)
this:
prime_factors (of_nat p) = {of_nat p}

goal (2 subgoals):
 1. p mod 4 = 1 \<Longrightarrow> thesis
 2. p mod 4 = 3 \<Longrightarrow> thesis
[PROOF STEP]
with p
[PROOF STATE]
proof (chain)
picking this:
p \<in># prime_factorization N
x \<in># prime_factorization (of_nat p)
prime_factors (of_nat p) = {of_nat p}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p \<in># prime_factorization N
x \<in># prime_factorization (of_nat p)
prime_factors (of_nat p) = {of_nat p}

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that(2)[of p] *
[PROOF STATE]
proof (prove)
using this:
p \<in># prime_factorization N
x \<in># prime_factorization (of_nat p)
prime_factors (of_nat p) = {of_nat p}
\<lbrakk>x = of_nat p; prime p; [p = 3] (mod 4)\<rbrakk> \<Longrightarrow> thesis
p mod 4 = 3

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

goal (1 subgoal):
 1. p mod 4 = 1 \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p mod 4 = 1 \<Longrightarrow> thesis
[PROOF STEP]
assume *: "p mod 4 = 1"
[PROOF STATE]
proof (state)
this:
p mod 4 = 1

goal (1 subgoal):
 1. p mod 4 = 1 \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p mod 4 = 1
[PROOF STEP]
interpret noninert_gauss_int_prime p
[PROOF STATE]
proof (prove)
using this:
p mod 4 = 1

goal (1 subgoal):
 1. noninert_gauss_int_prime p
[PROOF STEP]
by unfold_locales (use \<open>prime p\<close> in \<open>auto simp: cong_def\<close>)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p mod 4 = 1 \<Longrightarrow> thesis
[PROOF STEP]
obtain q1 q2 :: gauss_int where q12:
      "prime q1" "prime q2" "prime_factorization (of_nat p) = {#q1, q2#}"
      "gauss_int_norm q1 = p" "gauss_int_norm q2 = p" "q2 = \<i>\<^sub>\<int> * gauss_cnj q1"
      "ReZ q1 > 0" "ImZ q1 > 0" "ReZ q1 > 0" "ImZ q2 > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>q1 q2. \<lbrakk>prime q1; prime q2; prime_factorization (of_nat p) = {#q1, q2#}; gauss_int_norm q1 = p; gauss_int_norm q2 = p; q2 = \<i>\<^sub>\<int> * gauss_cnj q1; 0 < ReZ q1; 0 < ImZ q1; 0 < ReZ q1; 0 < ImZ q2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prime_factorization
[PROOF STATE]
proof (prove)
using this:
(\<And>q1 q2. \<lbrakk>prime q1; prime q2; prime_factorization (of_nat p) = {#q1, q2#}; gauss_int_norm q1 = p; gauss_int_norm q2 = p; q2 = \<i>\<^sub>\<int> * gauss_cnj q1; 0 < ReZ q1; 0 < ImZ q1; 0 < ReZ q1; 0 < ImZ q2\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>q1 q2. \<lbrakk>prime q1; prime q2; prime_factorization (of_nat p) = {#q1, q2#}; gauss_int_norm q1 = p; gauss_int_norm q2 = p; q2 = \<i>\<^sub>\<int> * gauss_cnj q1; 0 < ReZ q1; 0 < ImZ q1; 0 < ReZ q1; 0 < ImZ q2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
prime q1
prime q2
prime_factorization (of_nat p) = {#q1, q2#}
gauss_int_norm q1 = p
gauss_int_norm q2 = p
q2 = \<i>\<^sub>\<int> * gauss_cnj q1
0 < ReZ q1
0 < ImZ q1
0 < ReZ q1
0 < ImZ q2

goal (1 subgoal):
 1. p mod 4 = 1 \<Longrightarrow> thesis
[PROOF STEP]
from p q12
[PROOF STATE]
proof (chain)
picking this:
p \<in># prime_factorization N
x \<in># prime_factorization (of_nat p)
prime q1
prime q2
prime_factorization (of_nat p) = {#q1, q2#}
gauss_int_norm q1 = p
gauss_int_norm q2 = p
q2 = \<i>\<^sub>\<int> * gauss_cnj q1
0 < ReZ q1
0 < ImZ q1
0 < ReZ q1
0 < ImZ q2
[PROOF STEP]
have "x = q1 \<or> x = q2"
[PROOF STATE]
proof (prove)
using this:
p \<in># prime_factorization N
x \<in># prime_factorization (of_nat p)
prime q1
prime q2
prime_factorization (of_nat p) = {#q1, q2#}
gauss_int_norm q1 = p
gauss_int_norm q2 = p
q2 = \<i>\<^sub>\<int> * gauss_cnj q1
0 < ReZ q1
0 < ImZ q1
0 < ReZ q1
0 < ImZ q2

goal (1 subgoal):
 1. x = q1 \<or> x = q2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = q1 \<or> x = q2

goal (1 subgoal):
 1. p mod 4 = 1 \<Longrightarrow> thesis
[PROOF STEP]
with q12
[PROOF STATE]
proof (chain)
picking this:
prime q1
prime q2
prime_factorization (of_nat p) = {#q1, q2#}
gauss_int_norm q1 = p
gauss_int_norm q2 = p
q2 = \<i>\<^sub>\<int> * gauss_cnj q1
0 < ReZ q1
0 < ImZ q1
0 < ReZ q1
0 < ImZ q2
x = q1 \<or> x = q2
[PROOF STEP]
have **: "gauss_int_norm x = p" "ReZ x > 0" "ImZ x > 0"
[PROOF STATE]
proof (prove)
using this:
prime q1
prime q2
prime_factorization (of_nat p) = {#q1, q2#}
gauss_int_norm q1 = p
gauss_int_norm q2 = p
q2 = \<i>\<^sub>\<int> * gauss_cnj q1
0 < ReZ q1
0 < ImZ q1
0 < ReZ q1
0 < ImZ q2
x = q1 \<or> x = q2

goal (1 subgoal):
 1. gauss_int_norm x = p &&& 0 < ReZ x &&& 0 < ImZ x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
gauss_int_norm x = p
0 < ReZ x
0 < ImZ x

goal (1 subgoal):
 1. p mod 4 = 1 \<Longrightarrow> thesis
[PROOF STEP]
have "ReZ x \<noteq> ImZ x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ReZ x \<noteq> ImZ x
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ReZ x = ImZ x \<Longrightarrow> False
[PROOF STEP]
assume "ReZ x = ImZ x"
[PROOF STATE]
proof (state)
this:
ReZ x = ImZ x

goal (1 subgoal):
 1. ReZ x = ImZ x \<Longrightarrow> False
[PROOF STEP]
hence "even (gauss_int_norm x)"
[PROOF STATE]
proof (prove)
using this:
ReZ x = ImZ x

goal (1 subgoal):
 1. even (gauss_int_norm x)
[PROOF STEP]
by (auto simp: gauss_int_norm_def nat_mult_distrib)
[PROOF STATE]
proof (state)
this:
even (gauss_int_norm x)

goal (1 subgoal):
 1. ReZ x = ImZ x \<Longrightarrow> False
[PROOF STEP]
hence "even p"
[PROOF STATE]
proof (prove)
using this:
even (gauss_int_norm x)

goal (1 subgoal):
 1. even p
[PROOF STEP]
using \<open>gauss_int_norm x = p\<close>
[PROOF STATE]
proof (prove)
using this:
even (gauss_int_norm x)
gauss_int_norm x = p

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ReZ x \<noteq> ImZ x

goal (1 subgoal):
 1. p mod 4 = 1 \<Longrightarrow> thesis
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
ReZ x \<noteq> ImZ x

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that(3) \<open>prime p\<close> * **
[PROOF STATE]
proof (prove)
using this:
ReZ x \<noteq> ImZ x
\<lbrakk>prime (gauss_int_norm x); [gauss_int_norm x = 1] (mod 4); 0 < ReZ x; 0 < ImZ x; ReZ x \<noteq> ImZ x\<rbrakk> \<Longrightarrow> thesis
prime p
p mod 4 = 1
gauss_int_norm x = p
0 < ReZ x
0 < ImZ x

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prime_gauss_int_norm_squareD:
  fixes z :: gauss_int
  assumes "prime z" "gauss_int_norm z = p ^ 2"
  shows   "prime p \<and> z = of_nat p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime p \<and> z = of_nat p
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
prime z

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

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

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

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

goal (1 subgoal):
 1. 2 = p\<^sup>2
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
z = 1 + \<i>\<^sub>\<int>
gauss_int_norm z = p\<^sup>2

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

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

goal (1 subgoal):
 1. prime p \<and> z = of_nat p
[PROOF STEP]
by (simp add: prime_power_iff)
[PROOF STATE]
proof (state)
this:
prime p \<and> z = of_nat p

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

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

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

goal (1 subgoal):
 1. prime p \<and> z = of_nat p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
prime p \<and> z = of_nat p

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

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

goal (1 subgoal):
 1. prime p \<and> z = of_nat p
[PROOF STEP]
by (auto simp: prime_power_iff)
[PROOF STATE]
proof (state)
this:
prime p \<and> z = of_nat p

goal:
No subgoals!
[PROOF STEP]
qed