[STATEMENT]
lemma mult_oddprime_is_sum4sq: "\<lbrakk> prime (nat p); odd p \<rbrakk> \<Longrightarrow>
  \<exists> t. 0<t \<and> t<p \<and> is_sum4sq_int (p*t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prime (nat p); odd p\<rbrakk> \<Longrightarrow> \<exists>t>0. t < p \<and> is_sum4sq_int (p * t)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>prime (nat p); odd p\<rbrakk> \<Longrightarrow> \<exists>t>0. t < p \<and> is_sum4sq_int (p * t)
[PROOF STEP]
assume p1: "prime (nat p)"
[PROOF STATE]
proof (state)
this:
prime (nat p)

goal (1 subgoal):
 1. \<lbrakk>prime (nat p); odd p\<rbrakk> \<Longrightarrow> \<exists>t>0. t < p \<and> is_sum4sq_int (p * t)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
prime (nat p)
[PROOF STEP]
have p0: "p > 1" and "prime p"
[PROOF STATE]
proof (prove)
using this:
prime (nat p)

goal (1 subgoal):
 1. 1 < p &&& prime p
[PROOF STEP]
by (simp_all add: prime_int_nat_transfer prime_nat_iff)
[PROOF STATE]
proof (state)
this:
1 < p
prime p

goal (1 subgoal):
 1. \<lbrakk>prime (nat p); odd p\<rbrakk> \<Longrightarrow> \<exists>t>0. t < p \<and> is_sum4sq_int (p * t)
[PROOF STEP]
assume p2: "odd p"
[PROOF STATE]
proof (state)
this:
odd p

goal (1 subgoal):
 1. \<lbrakk>prime (nat p); odd p\<rbrakk> \<Longrightarrow> \<exists>t>0. t < p \<and> is_sum4sq_int (p * t)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
odd p
[PROOF STEP]
obtain n where n: "p = 2*n+1"
[PROOF STATE]
proof (prove)
using this:
odd p

goal (1 subgoal):
 1. (\<And>n. p = 2 * n + 1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using oddE
[PROOF STATE]
proof (prove)
using this:
odd p
\<lbrakk>odd ?a; \<And>b. ?a = (2::?'a) * b + (1::?'a) \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>n. p = 2 * n + 1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p = 2 * n + 1

goal (1 subgoal):
 1. \<lbrakk>prime (nat p); odd p\<rbrakk> \<Longrightarrow> \<exists>t>0. t < p \<and> is_sum4sq_int (p * t)
[PROOF STEP]
with p1
[PROOF STATE]
proof (chain)
picking this:
prime (nat p)
p = 2 * n + 1
[PROOF STEP]
have n0: "n > 0"
[PROOF STATE]
proof (prove)
using this:
prime (nat p)
p = 2 * n + 1

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

goal (1 subgoal):
 1. \<lbrakk>prime (nat p); odd p\<rbrakk> \<Longrightarrow> \<exists>t>0. t < p \<and> is_sum4sq_int (p * t)
[PROOF STEP]
let ?C = "{0 ..< p}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>prime (nat p); odd p\<rbrakk> \<Longrightarrow> \<exists>t>0. t < p \<and> is_sum4sq_int (p * t)
[PROOF STEP]
let ?D = "{0 .. n}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>prime (nat p); odd p\<rbrakk> \<Longrightarrow> \<exists>t>0. t < p \<and> is_sum4sq_int (p * t)
[PROOF STEP]
let ?f = "%x. x^2 mod p"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>prime (nat p); odd p\<rbrakk> \<Longrightarrow> \<exists>t>0. t < p \<and> is_sum4sq_int (p * t)
[PROOF STEP]
let ?g = "%x. (-1-x^2) mod p"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>prime (nat p); odd p\<rbrakk> \<Longrightarrow> \<exists>t>0. t < p \<and> is_sum4sq_int (p * t)
[PROOF STEP]
let ?A = "?f ` ?D"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>prime (nat p); odd p\<rbrakk> \<Longrightarrow> \<exists>t>0. t < p \<and> is_sum4sq_int (p * t)
[PROOF STEP]
let ?B = "?g ` ?D"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>prime (nat p); odd p\<rbrakk> \<Longrightarrow> \<exists>t>0. t < p \<and> is_sum4sq_int (p * t)
[PROOF STEP]
have finC: "finite ?C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {0..<p}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite {0..<p}

goal (1 subgoal):
 1. \<lbrakk>prime (nat p); odd p\<rbrakk> \<Longrightarrow> \<exists>t>0. t < p \<and> is_sum4sq_int (p * t)
[PROOF STEP]
have finD: "finite ?D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {0..n}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite {0..n}

goal (1 subgoal):
 1. \<lbrakk>prime (nat p); odd p\<rbrakk> \<Longrightarrow> \<exists>t>0. t < p \<and> is_sum4sq_int (p * t)
[PROOF STEP]
from p0
[PROOF STATE]
proof (chain)
picking this:
1 < p
[PROOF STEP]
have AsubC: "?A \<subseteq> ?C" and BsubC: "?B \<subseteq> ?C"
[PROOF STATE]
proof (prove)
using this:
1 < p

goal (1 subgoal):
 1. (\<lambda>x. x\<^sup>2 mod p) ` {0..n} \<subseteq> {0..<p} &&& (\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n} \<subseteq> {0..<p}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>x. x\<^sup>2 mod p) ` {0..n} \<subseteq> {0..<p}
(\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n} \<subseteq> {0..<p}

goal (1 subgoal):
 1. \<lbrakk>prime (nat p); odd p\<rbrakk> \<Longrightarrow> \<exists>t>0. t < p \<and> is_sum4sq_int (p * t)
[PROOF STEP]
with finC
[PROOF STATE]
proof (chain)
picking this:
finite {0..<p}
(\<lambda>x. x\<^sup>2 mod p) ` {0..n} \<subseteq> {0..<p}
(\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n} \<subseteq> {0..<p}
[PROOF STEP]
have finA: "finite ?A" and finB: "finite ?B"
[PROOF STATE]
proof (prove)
using this:
finite {0..<p}
(\<lambda>x. x\<^sup>2 mod p) ` {0..n} \<subseteq> {0..<p}
(\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n} \<subseteq> {0..<p}

goal (1 subgoal):
 1. finite ((\<lambda>x. x\<^sup>2 mod p) ` {0..n}) &&& finite ((\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n})
[PROOF STEP]
by (auto simp add: finite_subset)
[PROOF STATE]
proof (state)
this:
finite ((\<lambda>x. x\<^sup>2 mod p) ` {0..n})
finite ((\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n})

goal (1 subgoal):
 1. \<lbrakk>prime (nat p); odd p\<rbrakk> \<Longrightarrow> \<exists>t>0. t < p \<and> is_sum4sq_int (p * t)
[PROOF STEP]
from AsubC BsubC
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. x\<^sup>2 mod p) ` {0..n} \<subseteq> {0..<p}
(\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n} \<subseteq> {0..<p}
[PROOF STEP]
have AunBsubC: "?A \<union> ?B \<subseteq> ?C"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. x\<^sup>2 mod p) ` {0..n} \<subseteq> {0..<p}
(\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n} \<subseteq> {0..<p}

goal (1 subgoal):
 1. (\<lambda>x. x\<^sup>2 mod p) ` {0..n} \<union> (\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n} \<subseteq> {0..<p}
[PROOF STEP]
by (rule Un_least)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. x\<^sup>2 mod p) ` {0..n} \<union> (\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n} \<subseteq> {0..<p}

goal (1 subgoal):
 1. \<lbrakk>prime (nat p); odd p\<rbrakk> \<Longrightarrow> \<exists>t>0. t < p \<and> is_sum4sq_int (p * t)
[PROOF STEP]
from p0
[PROOF STATE]
proof (chain)
picking this:
1 < p
[PROOF STEP]
have cardC: "card ?C = nat p"
[PROOF STATE]
proof (prove)
using this:
1 < p

goal (1 subgoal):
 1. card {0..<p} = nat p
[PROOF STEP]
using card_atLeastZeroLessThan_int
[PROOF STATE]
proof (prove)
using this:
1 < p
card {0..<?u} = nat ?u

goal (1 subgoal):
 1. card {0..<p} = nat p
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
card {0..<p} = nat p

goal (1 subgoal):
 1. \<lbrakk>prime (nat p); odd p\<rbrakk> \<Longrightarrow> \<exists>t>0. t < p \<and> is_sum4sq_int (p * t)
[PROOF STEP]
from n0
[PROOF STATE]
proof (chain)
picking this:
0 < n
[PROOF STEP]
have cardD: "card ?D = 1+ nat n"
[PROOF STATE]
proof (prove)
using this:
0 < n

goal (1 subgoal):
 1. card {0..n} = 1 + nat n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card {0..n} = 1 + nat n

goal (1 subgoal):
 1. \<lbrakk>prime (nat p); odd p\<rbrakk> \<Longrightarrow> \<exists>t>0. t < p \<and> is_sum4sq_int (p * t)
[PROOF STEP]
have cardA: "card ?A = card ?D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card ((\<lambda>x. x\<^sup>2 mod p) ` {0..n}) = card {0..n}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card ((\<lambda>x. x\<^sup>2 mod p) ` {0..n}) = card {0..n}
[PROOF STEP]
have "inj_on ?f ?D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (\<lambda>x. x\<^sup>2 mod p) {0..n}
[PROOF STEP]
proof (unfold inj_on_def, auto)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x\<^sup>2 mod p = y\<^sup>2 mod p; 0 \<le> x; x \<le> n; 0 \<le> y; y \<le> n\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x\<^sup>2 mod p = y\<^sup>2 mod p; 0 \<le> x; x \<le> n; 0 \<le> y; y \<le> n\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x\<^sup>2 mod p = y\<^sup>2 mod p; 0 \<le> x; x \<le> n; 0 \<le> y; y \<le> n\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
assume x0: "0 \<le> x" and xn: "x \<le> n" and y0: "0 \<le> y" and yn: " y \<le> n"
        and xyp: "x^2 mod p = y^2 mod p"
[PROOF STATE]
proof (state)
this:
0 \<le> x
x \<le> n
0 \<le> y
y \<le> n
x\<^sup>2 mod p = y\<^sup>2 mod p

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x\<^sup>2 mod p = y\<^sup>2 mod p; 0 \<le> x; x \<le> n; 0 \<le> y; y \<le> n\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
with p0
[PROOF STATE]
proof (chain)
picking this:
1 < p
0 \<le> x
x \<le> n
0 \<le> y
y \<le> n
x\<^sup>2 mod p = y\<^sup>2 mod p
[PROOF STEP]
have "[x^2 = y^2] (mod p)"
[PROOF STATE]
proof (prove)
using this:
1 < p
0 \<le> x
x \<le> n
0 \<le> y
y \<le> n
x\<^sup>2 mod p = y\<^sup>2 mod p

goal (1 subgoal):
 1. [x\<^sup>2 = y\<^sup>2] (mod p)
[PROOF STEP]
using cong_def
[PROOF STATE]
proof (prove)
using this:
1 < p
0 \<le> x
x \<le> n
0 \<le> y
y \<le> n
x\<^sup>2 mod p = y\<^sup>2 mod p
[?b = ?c] (mod ?a) = (?b mod ?a = ?c mod ?a)

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

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

goal (1 subgoal):
 1. p dvd x\<^sup>2 - y\<^sup>2
[PROOF STEP]
using cong_iff_dvd_diff
[PROOF STATE]
proof (prove)
using this:
[x\<^sup>2 = y\<^sup>2] (mod p)
[?a = ?b] (mod ?m) = (?m dvd ?a - ?b)

goal (1 subgoal):
 1. p dvd x\<^sup>2 - y\<^sup>2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p dvd x\<^sup>2 - y\<^sup>2

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

goal (1 subgoal):
 1. p dvd (x + y) * (x - y)
[PROOF STEP]
by (simp add: power2_eq_square algebra_simps)
[PROOF STATE]
proof (state)
this:
p dvd (x + y) * (x - y)

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

goal (1 subgoal):
 1. p dvd x + y \<or> p dvd x - y
[PROOF STEP]
using \<open>prime p\<close> p0
[PROOF STATE]
proof (prove)
using this:
p dvd (x + y) * (x - y)
prime p
1 < p

goal (1 subgoal):
 1. p dvd x + y \<or> p dvd x - y
[PROOF STEP]
by (auto dest: prime_dvd_multD)
[PROOF STATE]
proof (state)
this:
p dvd x + y \<or> p dvd x - y

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

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

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

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

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x\<^sup>2 mod p = y\<^sup>2 mod p; 0 \<le> x; x \<le> n; 0 \<le> y; y \<le> n\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
from xn yn n
[PROOF STATE]
proof (chain)
picking this:
x \<le> n
y \<le> n
p = 2 * n + 1
[PROOF STEP]
have "x+y < p"
[PROOF STATE]
proof (prove)
using this:
x \<le> n
y \<le> n
p = 2 * n + 1

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

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x\<^sup>2 mod p = y\<^sup>2 mod p; 0 \<le> x; x \<le> n; 0 \<le> y; y \<le> n\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
p dvd x + y
x + y < p
[PROOF STEP]
have "\<not> x+y > 0"
[PROOF STATE]
proof (prove)
using this:
p dvd x + y
x + y < p

goal (1 subgoal):
 1. \<not> 0 < x + y
[PROOF STEP]
by (auto simp add: zdvd_not_zless)
[PROOF STATE]
proof (state)
this:
\<not> 0 < x + y

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x\<^sup>2 mod p = y\<^sup>2 mod p; 0 \<le> x; x \<le> n; 0 \<le> y; y \<le> n\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
with x0 y0
[PROOF STATE]
proof (chain)
picking this:
0 \<le> x
0 \<le> y
\<not> 0 < x + y
[PROOF STEP]
have "x = y"
[PROOF STATE]
proof (prove)
using this:
0 \<le> x
0 \<le> y
\<not> 0 < x + y

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

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x\<^sup>2 mod p = y\<^sup>2 mod p; 0 \<le> x; x \<le> n; 0 \<le> y; y \<le> n\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
} \<comment> \<open>both are zero\<close>
[PROOF STATE]
proof (state)
this:
p dvd x + y \<Longrightarrow> x = y

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

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

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x\<^sup>2 mod p = y\<^sup>2 mod p; 0 \<le> x; x \<le> n; 0 \<le> y; y \<le> n\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
assume ass: "p dvd x-y"
[PROOF STATE]
proof (state)
this:
p dvd x - y

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x\<^sup>2 mod p = y\<^sup>2 mod p; 0 \<le> x; x \<le> n; 0 \<le> y; y \<le> n\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
have "x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = y
[PROOF STEP]
proof (rule ccontr, case_tac "x-y \<ge> 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>x \<noteq> y; 0 \<le> x - y\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>x \<noteq> y; \<not> 0 \<le> x - y\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "x-y \<ge> 0" and "x \<noteq> y"
[PROOF STATE]
proof (state)
this:
0 \<le> x - y
x \<noteq> y

goal (2 subgoals):
 1. \<lbrakk>x \<noteq> y; 0 \<le> x - y\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>x \<noteq> y; \<not> 0 \<le> x - y\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence "x-y > 0"
[PROOF STATE]
proof (prove)
using this:
0 \<le> x - y
x \<noteq> y

goal (1 subgoal):
 1. 0 < x - y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < x - y

goal (2 subgoals):
 1. \<lbrakk>x \<noteq> y; 0 \<le> x - y\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>x \<noteq> y; \<not> 0 \<le> x - y\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with ass
[PROOF STATE]
proof (chain)
picking this:
p dvd x - y
0 < x - y
[PROOF STEP]
have "\<not> x-y < p"
[PROOF STATE]
proof (prove)
using this:
p dvd x - y
0 < x - y

goal (1 subgoal):
 1. \<not> x - y < p
[PROOF STEP]
by (auto simp add: zdvd_not_zless)
[PROOF STATE]
proof (state)
this:
\<not> x - y < p

goal (2 subgoals):
 1. \<lbrakk>x \<noteq> y; 0 \<le> x - y\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>x \<noteq> y; \<not> 0 \<le> x - y\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with xn y0 n p0
[PROOF STATE]
proof (chain)
picking this:
x \<le> n
0 \<le> y
p = 2 * n + 1
1 < p
\<not> x - y < p
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
x \<le> n
0 \<le> y
p = 2 * n + 1
1 < p
\<not> x - y < p

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

goal (1 subgoal):
 1. \<lbrakk>x \<noteq> y; \<not> 0 \<le> x - y\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>x \<noteq> y; \<not> 0 \<le> x - y\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "\<not> 0 \<le> x-y"
[PROOF STATE]
proof (state)
this:
\<not> 0 \<le> x - y

goal (1 subgoal):
 1. \<lbrakk>x \<noteq> y; \<not> 0 \<le> x - y\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence "y-x > 0"
[PROOF STATE]
proof (prove)
using this:
\<not> 0 \<le> x - y

goal (1 subgoal):
 1. 0 < y - x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < y - x

goal (1 subgoal):
 1. \<lbrakk>x \<noteq> y; \<not> 0 \<le> x - y\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 < y - x

goal (1 subgoal):
 1. \<lbrakk>x \<noteq> y; \<not> 0 \<le> x - y\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from x0 yn n p0
[PROOF STATE]
proof (chain)
picking this:
0 \<le> x
y \<le> n
p = 2 * n + 1
1 < p
[PROOF STEP]
have "y-x < p"
[PROOF STATE]
proof (prove)
using this:
0 \<le> x
y \<le> n
p = 2 * n + 1
1 < p

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

goal (1 subgoal):
 1. \<lbrakk>x \<noteq> y; \<not> 0 \<le> x - y\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
0 < y - x
y - x < p
[PROOF STEP]
have "\<not> p dvd y-x"
[PROOF STATE]
proof (prove)
using this:
0 < y - x
y - x < p

goal (1 subgoal):
 1. \<not> p dvd y - x
[PROOF STEP]
by (auto simp add: zdvd_not_zless)
[PROOF STATE]
proof (state)
this:
\<not> p dvd y - x

goal (1 subgoal):
 1. \<lbrakk>x \<noteq> y; \<not> 0 \<le> x - y\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> p dvd y - x

goal (1 subgoal):
 1. \<lbrakk>x \<noteq> y; \<not> 0 \<le> x - y\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from ass
[PROOF STATE]
proof (chain)
picking this:
p dvd x - y
[PROOF STEP]
have "p dvd -(x-y)"
[PROOF STATE]
proof (prove)
using this:
p dvd x - y

goal (1 subgoal):
 1. p dvd - (x - y)
[PROOF STEP]
by (simp only: dvd_minus_iff)
[PROOF STATE]
proof (state)
this:
p dvd - (x - y)

goal (1 subgoal):
 1. \<lbrakk>x \<noteq> y; \<not> 0 \<le> x - y\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<not> p dvd y - x
p dvd - (x - y)
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
\<not> p dvd y - x
p dvd - (x - y)

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:
x = y

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inj_on (\<lambda>x. x\<^sup>2 mod p) {0..n}

goal (1 subgoal):
 1. card ((\<lambda>x. x\<^sup>2 mod p) ` {0..n}) = card {0..n}
[PROOF STEP]
with finD
[PROOF STATE]
proof (chain)
picking this:
finite {0..n}
inj_on (\<lambda>x. x\<^sup>2 mod p) {0..n}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite {0..n}
inj_on (\<lambda>x. x\<^sup>2 mod p) {0..n}

goal (1 subgoal):
 1. card ((\<lambda>x. x\<^sup>2 mod p) ` {0..n}) = card {0..n}
[PROOF STEP]
by (simp only: inj_on_iff_eq_card)
[PROOF STATE]
proof (state)
this:
card ((\<lambda>x. x\<^sup>2 mod p) ` {0..n}) = card {0..n}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
card ((\<lambda>x. x\<^sup>2 mod p) ` {0..n}) = card {0..n}

goal (1 subgoal):
 1. \<lbrakk>prime (nat p); odd p\<rbrakk> \<Longrightarrow> \<exists>t>0. t < p \<and> is_sum4sq_int (p * t)
[PROOF STEP]
have cardB: "card ?B = card ?D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card ((\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n}) = card {0..n}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card ((\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n}) = card {0..n}
[PROOF STEP]
have "inj_on ?g ?D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (\<lambda>x. (- 1 - x\<^sup>2) mod p) {0..n}
[PROOF STEP]
proof (unfold inj_on_def, auto)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>(- 1 - x\<^sup>2) mod p = (- 1 - y\<^sup>2) mod p; 0 \<le> x; x \<le> n; 0 \<le> y; y \<le> n\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>(- 1 - x\<^sup>2) mod p = (- 1 - y\<^sup>2) mod p; 0 \<le> x; x \<le> n; 0 \<le> y; y \<le> n\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>(- 1 - x\<^sup>2) mod p = (- 1 - y\<^sup>2) mod p; 0 \<le> x; x \<le> n; 0 \<le> y; y \<le> n\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
assume x0: "0 \<le> x" and xn: "x \<le> n" and y0: "0 \<le> y" and yn: " y \<le> n"
        and xyp: "(-1-x^2) mod p = (-1-y^2) mod p"
[PROOF STATE]
proof (state)
this:
0 \<le> x
x \<le> n
0 \<le> y
y \<le> n
(- 1 - x\<^sup>2) mod p = (- 1 - y\<^sup>2) mod p

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>(- 1 - x\<^sup>2) mod p = (- 1 - y\<^sup>2) mod p; 0 \<le> x; x \<le> n; 0 \<le> y; y \<le> n\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
with p0
[PROOF STATE]
proof (chain)
picking this:
1 < p
0 \<le> x
x \<le> n
0 \<le> y
y \<le> n
(- 1 - x\<^sup>2) mod p = (- 1 - y\<^sup>2) mod p
[PROOF STEP]
have "[-1-y^2 = -1-x^2] (mod p)"
[PROOF STATE]
proof (prove)
using this:
1 < p
0 \<le> x
x \<le> n
0 \<le> y
y \<le> n
(- 1 - x\<^sup>2) mod p = (- 1 - y\<^sup>2) mod p

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

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

goal (1 subgoal):
 1. p dvd - 1 - y\<^sup>2 - (- 1 - x\<^sup>2)
[PROOF STEP]
by (simp only: cong_iff_dvd_diff)
[PROOF STATE]
proof (state)
this:
p dvd - 1 - y\<^sup>2 - (- 1 - x\<^sup>2)

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

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>(- 1 - x\<^sup>2) mod p = (- 1 - y\<^sup>2) mod p; 0 \<le> x; x \<le> n; 0 \<le> y; y \<le> n\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
have "-1-y^2 - (-1-x^2) = x^2 - y^2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - 1 - y\<^sup>2 - (- 1 - x\<^sup>2) = x\<^sup>2 - y\<^sup>2
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
- 1 - y\<^sup>2 - (- 1 - x\<^sup>2) = x\<^sup>2 - y\<^sup>2

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>(- 1 - x\<^sup>2) mod p = (- 1 - y\<^sup>2) mod p; 0 \<le> x; x \<le> n; 0 \<le> y; y \<le> n\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
p dvd - 1 - y\<^sup>2 - (- 1 - x\<^sup>2)
- 1 - y\<^sup>2 - (- 1 - x\<^sup>2) = x\<^sup>2 - y\<^sup>2
[PROOF STEP]
have "p dvd x^2-y^2"
[PROOF STATE]
proof (prove)
using this:
p dvd - 1 - y\<^sup>2 - (- 1 - x\<^sup>2)
- 1 - y\<^sup>2 - (- 1 - x\<^sup>2) = x\<^sup>2 - y\<^sup>2

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

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

goal (1 subgoal):
 1. p dvd (x + y) * (x - y)
[PROOF STEP]
by (simp add: power2_eq_square algebra_simps)
[PROOF STATE]
proof (state)
this:
p dvd (x + y) * (x - y)

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>(- 1 - x\<^sup>2) mod p = (- 1 - y\<^sup>2) mod p; 0 \<le> x; x \<le> n; 0 \<le> y; y \<le> n\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
with p1
[PROOF STATE]
proof (chain)
picking this:
prime (nat p)
p dvd (x + y) * (x - y)
[PROOF STEP]
have "p dvd x+y \<or> p dvd x-y"
[PROOF STATE]
proof (prove)
using this:
prime (nat p)
p dvd (x + y) * (x - y)

goal (1 subgoal):
 1. p dvd x + y \<or> p dvd x - y
[PROOF STEP]
using \<open>prime p\<close> p0
[PROOF STATE]
proof (prove)
using this:
prime (nat p)
p dvd (x + y) * (x - y)
prime p
1 < p

goal (1 subgoal):
 1. p dvd x + y \<or> p dvd x - y
[PROOF STEP]
by (auto dest: prime_dvd_multD)
[PROOF STATE]
proof (state)
this:
p dvd x + y \<or> p dvd x - y

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

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

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

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

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>(- 1 - x\<^sup>2) mod p = (- 1 - y\<^sup>2) mod p; 0 \<le> x; x \<le> n; 0 \<le> y; y \<le> n\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
from xn yn n
[PROOF STATE]
proof (chain)
picking this:
x \<le> n
y \<le> n
p = 2 * n + 1
[PROOF STEP]
have "x+y < p"
[PROOF STATE]
proof (prove)
using this:
x \<le> n
y \<le> n
p = 2 * n + 1

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

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>(- 1 - x\<^sup>2) mod p = (- 1 - y\<^sup>2) mod p; 0 \<le> x; x \<le> n; 0 \<le> y; y \<le> n\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
p dvd x + y
x + y < p
[PROOF STEP]
have "\<not> x+y > 0"
[PROOF STATE]
proof (prove)
using this:
p dvd x + y
x + y < p

goal (1 subgoal):
 1. \<not> 0 < x + y
[PROOF STEP]
by (auto simp add: zdvd_not_zless)
[PROOF STATE]
proof (state)
this:
\<not> 0 < x + y

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>(- 1 - x\<^sup>2) mod p = (- 1 - y\<^sup>2) mod p; 0 \<le> x; x \<le> n; 0 \<le> y; y \<le> n\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
with x0 y0
[PROOF STATE]
proof (chain)
picking this:
0 \<le> x
0 \<le> y
\<not> 0 < x + y
[PROOF STEP]
have "x = y"
[PROOF STATE]
proof (prove)
using this:
0 \<le> x
0 \<le> y
\<not> 0 < x + y

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

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>(- 1 - x\<^sup>2) mod p = (- 1 - y\<^sup>2) mod p; 0 \<le> x; x \<le> n; 0 \<le> y; y \<le> n\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
} \<comment> \<open>both are zero\<close>
[PROOF STATE]
proof (state)
this:
p dvd x + y \<Longrightarrow> x = y

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

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

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>(- 1 - x\<^sup>2) mod p = (- 1 - y\<^sup>2) mod p; 0 \<le> x; x \<le> n; 0 \<le> y; y \<le> n\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
assume ass: "p dvd x-y"
[PROOF STATE]
proof (state)
this:
p dvd x - y

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>(- 1 - x\<^sup>2) mod p = (- 1 - y\<^sup>2) mod p; 0 \<le> x; x \<le> n; 0 \<le> y; y \<le> n\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
have "x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = y
[PROOF STEP]
proof (rule ccontr, case_tac "x-y \<ge> 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>x \<noteq> y; 0 \<le> x - y\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>x \<noteq> y; \<not> 0 \<le> x - y\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "x-y \<ge> 0" and "x \<noteq> y"
[PROOF STATE]
proof (state)
this:
0 \<le> x - y
x \<noteq> y

goal (2 subgoals):
 1. \<lbrakk>x \<noteq> y; 0 \<le> x - y\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>x \<noteq> y; \<not> 0 \<le> x - y\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence "x-y > 0"
[PROOF STATE]
proof (prove)
using this:
0 \<le> x - y
x \<noteq> y

goal (1 subgoal):
 1. 0 < x - y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < x - y

goal (2 subgoals):
 1. \<lbrakk>x \<noteq> y; 0 \<le> x - y\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>x \<noteq> y; \<not> 0 \<le> x - y\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with ass
[PROOF STATE]
proof (chain)
picking this:
p dvd x - y
0 < x - y
[PROOF STEP]
have "\<not> x-y < p"
[PROOF STATE]
proof (prove)
using this:
p dvd x - y
0 < x - y

goal (1 subgoal):
 1. \<not> x - y < p
[PROOF STEP]
by (auto simp add: zdvd_not_zless)
[PROOF STATE]
proof (state)
this:
\<not> x - y < p

goal (2 subgoals):
 1. \<lbrakk>x \<noteq> y; 0 \<le> x - y\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>x \<noteq> y; \<not> 0 \<le> x - y\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with xn y0 n p0
[PROOF STATE]
proof (chain)
picking this:
x \<le> n
0 \<le> y
p = 2 * n + 1
1 < p
\<not> x - y < p
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
x \<le> n
0 \<le> y
p = 2 * n + 1
1 < p
\<not> x - y < p

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

goal (1 subgoal):
 1. \<lbrakk>x \<noteq> y; \<not> 0 \<le> x - y\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>x \<noteq> y; \<not> 0 \<le> x - y\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "\<not> 0 \<le> x-y"
[PROOF STATE]
proof (state)
this:
\<not> 0 \<le> x - y

goal (1 subgoal):
 1. \<lbrakk>x \<noteq> y; \<not> 0 \<le> x - y\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence "y-x > 0"
[PROOF STATE]
proof (prove)
using this:
\<not> 0 \<le> x - y

goal (1 subgoal):
 1. 0 < y - x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < y - x

goal (1 subgoal):
 1. \<lbrakk>x \<noteq> y; \<not> 0 \<le> x - y\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 < y - x

goal (1 subgoal):
 1. \<lbrakk>x \<noteq> y; \<not> 0 \<le> x - y\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from x0 yn n p0
[PROOF STATE]
proof (chain)
picking this:
0 \<le> x
y \<le> n
p = 2 * n + 1
1 < p
[PROOF STEP]
have "y-x < p"
[PROOF STATE]
proof (prove)
using this:
0 \<le> x
y \<le> n
p = 2 * n + 1
1 < p

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

goal (1 subgoal):
 1. \<lbrakk>x \<noteq> y; \<not> 0 \<le> x - y\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
0 < y - x
y - x < p
[PROOF STEP]
have "\<not> p dvd y-x"
[PROOF STATE]
proof (prove)
using this:
0 < y - x
y - x < p

goal (1 subgoal):
 1. \<not> p dvd y - x
[PROOF STEP]
by (auto simp add: zdvd_not_zless)
[PROOF STATE]
proof (state)
this:
\<not> p dvd y - x

goal (1 subgoal):
 1. \<lbrakk>x \<noteq> y; \<not> 0 \<le> x - y\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> p dvd y - x

goal (1 subgoal):
 1. \<lbrakk>x \<noteq> y; \<not> 0 \<le> x - y\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from ass
[PROOF STATE]
proof (chain)
picking this:
p dvd x - y
[PROOF STEP]
have "p dvd -(x-y)"
[PROOF STATE]
proof (prove)
using this:
p dvd x - y

goal (1 subgoal):
 1. p dvd - (x - y)
[PROOF STEP]
by (simp only: dvd_minus_iff)
[PROOF STATE]
proof (state)
this:
p dvd - (x - y)

goal (1 subgoal):
 1. \<lbrakk>x \<noteq> y; \<not> 0 \<le> x - y\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<not> p dvd y - x
p dvd - (x - y)
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
\<not> p dvd y - x
p dvd - (x - y)

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:
x = y

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inj_on (\<lambda>x. (- 1 - x\<^sup>2) mod p) {0..n}

goal (1 subgoal):
 1. card ((\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n}) = card {0..n}
[PROOF STEP]
with finD
[PROOF STATE]
proof (chain)
picking this:
finite {0..n}
inj_on (\<lambda>x. (- 1 - x\<^sup>2) mod p) {0..n}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite {0..n}
inj_on (\<lambda>x. (- 1 - x\<^sup>2) mod p) {0..n}

goal (1 subgoal):
 1. card ((\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n}) = card {0..n}
[PROOF STEP]
by (simp only: inj_on_iff_eq_card)
[PROOF STATE]
proof (state)
this:
card ((\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n}) = card {0..n}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
card ((\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n}) = card {0..n}

goal (1 subgoal):
 1. \<lbrakk>prime (nat p); odd p\<rbrakk> \<Longrightarrow> \<exists>t>0. t < p \<and> is_sum4sq_int (p * t)
[PROOF STEP]
have "?A \<inter> ?B \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. x\<^sup>2 mod p) ` {0..n} \<inter> (\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n} \<noteq> {}
[PROOF STEP]
proof (rule ccontr, auto)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>x. x\<^sup>2 mod p) ` {0..n} \<inter> (\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n} = {} \<Longrightarrow> False
[PROOF STEP]
assume ABdisj: "?A \<inter> ?B = {}"
[PROOF STATE]
proof (state)
this:
(\<lambda>x. x\<^sup>2 mod p) ` {0..n} \<inter> (\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n} = {}

goal (1 subgoal):
 1. (\<lambda>x. x\<^sup>2 mod p) ` {0..n} \<inter> (\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n} = {} \<Longrightarrow> False
[PROOF STEP]
from cardA cardB cardD
[PROOF STATE]
proof (chain)
picking this:
card ((\<lambda>x. x\<^sup>2 mod p) ` {0..n}) = card {0..n}
card ((\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n}) = card {0..n}
card {0..n} = 1 + nat n
[PROOF STEP]
have "2 + 2*(nat n) = card ?A + card ?B"
[PROOF STATE]
proof (prove)
using this:
card ((\<lambda>x. x\<^sup>2 mod p) ` {0..n}) = card {0..n}
card ((\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n}) = card {0..n}
card {0..n} = 1 + nat n

goal (1 subgoal):
 1. 2 + 2 * nat n = card ((\<lambda>x. x\<^sup>2 mod p) ` {0..n}) + card ((\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
2 + 2 * nat n = card ((\<lambda>x. x\<^sup>2 mod p) ` {0..n}) + card ((\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n})

goal (1 subgoal):
 1. (\<lambda>x. x\<^sup>2 mod p) ` {0..n} \<inter> (\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n} = {} \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
2 + 2 * nat n = card ((\<lambda>x. x\<^sup>2 mod p) ` {0..n}) + card ((\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n})

goal (1 subgoal):
 1. (\<lambda>x. x\<^sup>2 mod p) ` {0..n} \<inter> (\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n} = {} \<Longrightarrow> False
[PROOF STEP]
with finA finB ABdisj
[PROOF STATE]
proof (chain)
picking this:
finite ((\<lambda>x. x\<^sup>2 mod p) ` {0..n})
finite ((\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n})
(\<lambda>x. x\<^sup>2 mod p) ` {0..n} \<inter> (\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n} = {}
2 + 2 * nat n = card ((\<lambda>x. x\<^sup>2 mod p) ` {0..n}) + card ((\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n})
[PROOF STEP]
have "\<dots> = card (?A \<union> ?B)"
[PROOF STATE]
proof (prove)
using this:
finite ((\<lambda>x. x\<^sup>2 mod p) ` {0..n})
finite ((\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n})
(\<lambda>x. x\<^sup>2 mod p) ` {0..n} \<inter> (\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n} = {}
2 + 2 * nat n = card ((\<lambda>x. x\<^sup>2 mod p) ` {0..n}) + card ((\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n})

goal (1 subgoal):
 1. card ((\<lambda>x. x\<^sup>2 mod p) ` {0..n}) + card ((\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n}) = card ((\<lambda>x. x\<^sup>2 mod p) ` {0..n} \<union> (\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n})
[PROOF STEP]
by (simp only: card_Un_disjoint)
[PROOF STATE]
proof (state)
this:
card ((\<lambda>x. x\<^sup>2 mod p) ` {0..n}) + card ((\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n}) = card ((\<lambda>x. x\<^sup>2 mod p) ` {0..n} \<union> (\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n})

goal (1 subgoal):
 1. (\<lambda>x. x\<^sup>2 mod p) ` {0..n} \<inter> (\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n} = {} \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card ((\<lambda>x. x\<^sup>2 mod p) ` {0..n}) + card ((\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n}) = card ((\<lambda>x. x\<^sup>2 mod p) ` {0..n} \<union> (\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n})

goal (1 subgoal):
 1. (\<lambda>x. x\<^sup>2 mod p) ` {0..n} \<inter> (\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n} = {} \<Longrightarrow> False
[PROOF STEP]
with finC AunBsubC
[PROOF STATE]
proof (chain)
picking this:
finite {0..<p}
(\<lambda>x. x\<^sup>2 mod p) ` {0..n} \<union> (\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n} \<subseteq> {0..<p}
card ((\<lambda>x. x\<^sup>2 mod p) ` {0..n}) + card ((\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n}) = card ((\<lambda>x. x\<^sup>2 mod p) ` {0..n} \<union> (\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n})
[PROOF STEP]
have "\<dots> \<le> card ?C"
[PROOF STATE]
proof (prove)
using this:
finite {0..<p}
(\<lambda>x. x\<^sup>2 mod p) ` {0..n} \<union> (\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n} \<subseteq> {0..<p}
card ((\<lambda>x. x\<^sup>2 mod p) ` {0..n}) + card ((\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n}) = card ((\<lambda>x. x\<^sup>2 mod p) ` {0..n} \<union> (\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n})

goal (1 subgoal):
 1. card ((\<lambda>x. x\<^sup>2 mod p) ` {0..n} \<union> (\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n}) \<le> card {0..<p}
[PROOF STEP]
by (simp only: card_mono)
[PROOF STATE]
proof (state)
this:
card ((\<lambda>x. x\<^sup>2 mod p) ` {0..n} \<union> (\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n}) \<le> card {0..<p}

goal (1 subgoal):
 1. (\<lambda>x. x\<^sup>2 mod p) ` {0..n} \<inter> (\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n} = {} \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card ((\<lambda>x. x\<^sup>2 mod p) ` {0..n} \<union> (\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n}) \<le> card {0..<p}

goal (1 subgoal):
 1. (\<lambda>x. x\<^sup>2 mod p) ` {0..n} \<inter> (\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n} = {} \<Longrightarrow> False
[PROOF STEP]
with cardC
[PROOF STATE]
proof (chain)
picking this:
card {0..<p} = nat p
card ((\<lambda>x. x\<^sup>2 mod p) ` {0..n} \<union> (\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n}) \<le> card {0..<p}
[PROOF STEP]
have "\<dots> = nat p"
[PROOF STATE]
proof (prove)
using this:
card {0..<p} = nat p
card ((\<lambda>x. x\<^sup>2 mod p) ` {0..n} \<union> (\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n}) \<le> card {0..<p}

goal (1 subgoal):
 1. card {0..<p} = nat p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card {0..<p} = nat p

goal (1 subgoal):
 1. (\<lambda>x. x\<^sup>2 mod p) ` {0..n} \<inter> (\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n} = {} \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
2 + 2 * nat n \<le> nat p
[PROOF STEP]
have "2 + 2*(nat n) \<le> nat p"
[PROOF STATE]
proof (prove)
using this:
2 + 2 * nat n \<le> nat p

goal (1 subgoal):
 1. 2 + 2 * nat n \<le> nat p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 + 2 * nat n \<le> nat p

goal (1 subgoal):
 1. (\<lambda>x. x\<^sup>2 mod p) ` {0..n} \<inter> (\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n} = {} \<Longrightarrow> False
[PROOF STEP]
with n
[PROOF STATE]
proof (chain)
picking this:
p = 2 * n + 1
2 + 2 * nat n \<le> nat p
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
p = 2 * n + 1
2 + 2 * nat n \<le> nat p

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<lambda>x. x\<^sup>2 mod p) ` {0..n} \<inter> (\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n} \<noteq> {}

goal (1 subgoal):
 1. \<lbrakk>prime (nat p); odd p\<rbrakk> \<Longrightarrow> \<exists>t>0. t < p \<and> is_sum4sq_int (p * t)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. x\<^sup>2 mod p) ` {0..n} \<inter> (\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n} \<noteq> {}
[PROOF STEP]
obtain z where "z \<in> ?A \<and> z \<in> ?B"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. x\<^sup>2 mod p) ` {0..n} \<inter> (\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n} \<noteq> {}

goal (1 subgoal):
 1. (\<And>z. z \<in> (\<lambda>x. x\<^sup>2 mod p) ` {0..n} \<and> z \<in> (\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z \<in> (\<lambda>x. x\<^sup>2 mod p) ` {0..n} \<and> z \<in> (\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n}

goal (1 subgoal):
 1. \<lbrakk>prime (nat p); odd p\<rbrakk> \<Longrightarrow> \<exists>t>0. t < p \<and> is_sum4sq_int (p * t)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
z \<in> (\<lambda>x. x\<^sup>2 mod p) ` {0..n} \<and> z \<in> (\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n}
[PROOF STEP]
obtain x y where xy: "x \<in> ?D \<and> y \<in> ?D \<and> z = x^2 mod p \<and> z = (-1-y^2) mod p"
[PROOF STATE]
proof (prove)
using this:
z \<in> (\<lambda>x. x\<^sup>2 mod p) ` {0..n} \<and> z \<in> (\<lambda>x. (- 1 - x\<^sup>2) mod p) ` {0..n}

goal (1 subgoal):
 1. (\<And>x y. x \<in> {0..n} \<and> y \<in> {0..n} \<and> z = x\<^sup>2 mod p \<and> z = (- 1 - y\<^sup>2) mod p \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> {0..n} \<and> y \<in> {0..n} \<and> z = x\<^sup>2 mod p \<and> z = (- 1 - y\<^sup>2) mod p

goal (1 subgoal):
 1. \<lbrakk>prime (nat p); odd p\<rbrakk> \<Longrightarrow> \<exists>t>0. t < p \<and> is_sum4sq_int (p * t)
[PROOF STEP]
with p0
[PROOF STATE]
proof (chain)
picking this:
1 < p
x \<in> {0..n} \<and> y \<in> {0..n} \<and> z = x\<^sup>2 mod p \<and> z = (- 1 - y\<^sup>2) mod p
[PROOF STEP]
have "[x^2=-1-y^2](mod p)"
[PROOF STATE]
proof (prove)
using this:
1 < p
x \<in> {0..n} \<and> y \<in> {0..n} \<and> z = x\<^sup>2 mod p \<and> z = (- 1 - y\<^sup>2) mod p

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

goal (1 subgoal):
 1. \<lbrakk>prime (nat p); odd p\<rbrakk> \<Longrightarrow> \<exists>t>0. t < p \<and> is_sum4sq_int (p * t)
[PROOF STEP]
hence "p dvd x^2-(-1-y^2)"
[PROOF STATE]
proof (prove)
using this:
[x\<^sup>2 = - 1 - y\<^sup>2] (mod p)

goal (1 subgoal):
 1. p dvd x\<^sup>2 - (- 1 - y\<^sup>2)
[PROOF STEP]
by (simp only: cong_iff_dvd_diff)
[PROOF STATE]
proof (state)
this:
p dvd x\<^sup>2 - (- 1 - y\<^sup>2)

goal (1 subgoal):
 1. \<lbrakk>prime (nat p); odd p\<rbrakk> \<Longrightarrow> \<exists>t>0. t < p \<and> is_sum4sq_int (p * t)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
p dvd x\<^sup>2 - (- 1 - y\<^sup>2)

goal (1 subgoal):
 1. \<lbrakk>prime (nat p); odd p\<rbrakk> \<Longrightarrow> \<exists>t>0. t < p \<and> is_sum4sq_int (p * t)
[PROOF STEP]
have "x^2-(-1-y^2)=x^2+y^2+1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>2 - (- 1 - y\<^sup>2) = x\<^sup>2 + y\<^sup>2 + 1
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
x\<^sup>2 - (- 1 - y\<^sup>2) = x\<^sup>2 + y\<^sup>2 + 1

goal (1 subgoal):
 1. \<lbrakk>prime (nat p); odd p\<rbrakk> \<Longrightarrow> \<exists>t>0. t < p \<and> is_sum4sq_int (p * t)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
p dvd x\<^sup>2 - (- 1 - y\<^sup>2)
x\<^sup>2 - (- 1 - y\<^sup>2) = x\<^sup>2 + y\<^sup>2 + 1
[PROOF STEP]
have "p dvd sum4sq_int(x,y,1,0)"
[PROOF STATE]
proof (prove)
using this:
p dvd x\<^sup>2 - (- 1 - y\<^sup>2)
x\<^sup>2 - (- 1 - y\<^sup>2) = x\<^sup>2 + y\<^sup>2 + 1

goal (1 subgoal):
 1. p dvd sum4sq_int (x, y, 1, 0)
[PROOF STEP]
by (auto simp add: sum4sq_int_def)
[PROOF STATE]
proof (state)
this:
p dvd sum4sq_int (x, y, 1, 0)

goal (1 subgoal):
 1. \<lbrakk>prime (nat p); odd p\<rbrakk> \<Longrightarrow> \<exists>t>0. t < p \<and> is_sum4sq_int (p * t)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p dvd sum4sq_int (x, y, 1, 0)
[PROOF STEP]
obtain t where t: "p * t = sum4sq_int(x,y,1,0)"
[PROOF STATE]
proof (prove)
using this:
p dvd sum4sq_int (x, y, 1, 0)

goal (1 subgoal):
 1. (\<And>t. p * t = sum4sq_int (x, y, 1, 0) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp only: dvd_def eq_refl)
[PROOF STATE]
proof (state)
this:
p * t = sum4sq_int (x, y, 1, 0)

goal (1 subgoal):
 1. \<lbrakk>prime (nat p); odd p\<rbrakk> \<Longrightarrow> \<exists>t>0. t < p \<and> is_sum4sq_int (p * t)
[PROOF STEP]
hence "is_sum4sq_int (p*t)"
[PROOF STATE]
proof (prove)
using this:
p * t = sum4sq_int (x, y, 1, 0)

goal (1 subgoal):
 1. is_sum4sq_int (p * t)
[PROOF STEP]
by (unfold is_sum4sq_int_def, auto)
[PROOF STATE]
proof (state)
this:
is_sum4sq_int (p * t)

goal (1 subgoal):
 1. \<lbrakk>prime (nat p); odd p\<rbrakk> \<Longrightarrow> \<exists>t>0. t < p \<and> is_sum4sq_int (p * t)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_sum4sq_int (p * t)

goal (1 subgoal):
 1. \<lbrakk>prime (nat p); odd p\<rbrakk> \<Longrightarrow> \<exists>t>0. t < p \<and> is_sum4sq_int (p * t)
[PROOF STEP]
have "t > 0 \<and> t < p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < t \<and> t < p
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 < t
 2. t < p
[PROOF STEP]
have "x^2 \<ge> 0 \<and> y^2 \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> x\<^sup>2 \<and> 0 \<le> y\<^sup>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 \<le> x\<^sup>2 \<and> 0 \<le> y\<^sup>2

goal (2 subgoals):
 1. 0 < t
 2. t < p
[PROOF STEP]
hence "x^2+y^2+1 > 0"
[PROOF STATE]
proof (prove)
using this:
0 \<le> x\<^sup>2 \<and> 0 \<le> y\<^sup>2

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

goal (2 subgoals):
 1. 0 < t
 2. t < p
[PROOF STEP]
with t
[PROOF STATE]
proof (chain)
picking this:
p * t = sum4sq_int (x, y, 1, 0)
0 < x\<^sup>2 + y\<^sup>2 + 1
[PROOF STEP]
have "p*t > 0"
[PROOF STATE]
proof (prove)
using this:
p * t = sum4sq_int (x, y, 1, 0)
0 < x\<^sup>2 + y\<^sup>2 + 1

goal (1 subgoal):
 1. 0 < p * t
[PROOF STEP]
by (unfold sum4sq_int_def, auto)
[PROOF STATE]
proof (state)
this:
0 < p * t

goal (2 subgoals):
 1. 0 < t
 2. t < p
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 < p * t

goal (2 subgoals):
 1. 0 < t
 2. t < p
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
0 < p * t

goal (2 subgoals):
 1. 0 < t
 2. t < p
[PROOF STEP]
assume "t < 0"
[PROOF STATE]
proof (state)
this:
t < 0

goal (2 subgoals):
 1. 0 < t
 2. t < p
[PROOF STEP]
with p0
[PROOF STATE]
proof (chain)
picking this:
1 < p
t < 0
[PROOF STEP]
have "p*t < p*0"
[PROOF STATE]
proof (prove)
using this:
1 < p
t < 0

goal (1 subgoal):
 1. p * t < p * 0
[PROOF STEP]
by (simp only: zmult_zless_mono2)
[PROOF STATE]
proof (state)
this:
p * t < p * 0

goal (2 subgoals):
 1. 0 < t
 2. t < p
[PROOF STEP]
hence "p*t < 0"
[PROOF STATE]
proof (prove)
using this:
p * t < p * 0

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

goal (2 subgoals):
 1. 0 < t
 2. t < p
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
t < 0 \<Longrightarrow> p * t < 0

goal (2 subgoals):
 1. 0 < t
 2. t < p
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
t < 0 \<Longrightarrow> p * t < 0

goal (2 subgoals):
 1. 0 < t
 2. t < p
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
t < 0 \<Longrightarrow> p * t < 0

goal (2 subgoals):
 1. 0 < t
 2. t < p
[PROOF STEP]
assume "t = 0"
[PROOF STATE]
proof (state)
this:
t = 0

goal (2 subgoals):
 1. 0 < t
 2. t < p
[PROOF STEP]
hence "p*t = 0"
[PROOF STATE]
proof (prove)
using this:
t = 0

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

goal (2 subgoals):
 1. 0 < t
 2. t < p
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
t = 0 \<Longrightarrow> p * t = 0

goal (2 subgoals):
 1. 0 < t
 2. t < p
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
0 < p * t
t < 0 \<Longrightarrow> p * t < 0
t = 0 \<Longrightarrow> p * t = 0
[PROOF STEP]
have "\<not> t < 0 \<and> t \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
0 < p * t
t < 0 \<Longrightarrow> p * t < 0
t = 0 \<Longrightarrow> p * t = 0

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

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

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

goal (1 subgoal):
 1. t < p
[PROOF STEP]
from xy
[PROOF STATE]
proof (chain)
picking this:
x \<in> {0..n} \<and> y \<in> {0..n} \<and> z = x\<^sup>2 mod p \<and> z = (- 1 - y\<^sup>2) mod p
[PROOF STEP]
have "x^2 \<le> n^2 \<and> y^2 \<le> n^2"
[PROOF STATE]
proof (prove)
using this:
x \<in> {0..n} \<and> y \<in> {0..n} \<and> z = x\<^sup>2 mod p \<and> z = (- 1 - y\<^sup>2) mod p

goal (1 subgoal):
 1. x\<^sup>2 \<le> n\<^sup>2 \<and> y\<^sup>2 \<le> n\<^sup>2
[PROOF STEP]
by (auto simp add: power_mono)
[PROOF STATE]
proof (state)
this:
x\<^sup>2 \<le> n\<^sup>2 \<and> y\<^sup>2 \<le> n\<^sup>2

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

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

goal (1 subgoal):
 1. t < p
[PROOF STEP]
with t
[PROOF STATE]
proof (chain)
picking this:
p * t = sum4sq_int (x, y, 1, 0)
x\<^sup>2 + y\<^sup>2 + 1 \<le> 2 * n\<^sup>2 + 1
[PROOF STEP]
have contr: "p*t \<le> 2*n^2+1"
[PROOF STATE]
proof (prove)
using this:
p * t = sum4sq_int (x, y, 1, 0)
x\<^sup>2 + y\<^sup>2 + 1 \<le> 2 * n\<^sup>2 + 1

goal (1 subgoal):
 1. p * t \<le> 2 * n\<^sup>2 + 1
[PROOF STEP]
by (simp add: sum4sq_int_def)
[PROOF STATE]
proof (state)
this:
p * t \<le> 2 * n\<^sup>2 + 1

goal (1 subgoal):
 1. t < p
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
p * t \<le> 2 * n\<^sup>2 + 1

goal (1 subgoal):
 1. t < p
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
p * t \<le> 2 * n\<^sup>2 + 1

goal (1 subgoal):
 1. t < p
[PROOF STEP]
assume "t > n+1"
[PROOF STATE]
proof (state)
this:
n + 1 < t

goal (1 subgoal):
 1. t < p
[PROOF STEP]
with p0
[PROOF STATE]
proof (chain)
picking this:
1 < p
n + 1 < t
[PROOF STEP]
have "p*(n+1) < p*t"
[PROOF STATE]
proof (prove)
using this:
1 < p
n + 1 < t

goal (1 subgoal):
 1. p * (n + 1) < p * t
[PROOF STEP]
by (simp only: zmult_zless_mono2)
[PROOF STATE]
proof (state)
this:
p * (n + 1) < p * t

goal (1 subgoal):
 1. t < p
[PROOF STEP]
with n
[PROOF STATE]
proof (chain)
picking this:
p = 2 * n + 1
p * (n + 1) < p * t
[PROOF STEP]
have "p*t > (2*n+1)*n + (2*n+1)*1"
[PROOF STATE]
proof (prove)
using this:
p = 2 * n + 1
p * (n + 1) < p * t

goal (1 subgoal):
 1. (2 * n + 1) * n + (2 * n + 1) * 1 < p * t
[PROOF STEP]
by (simp only: distrib_left)
[PROOF STATE]
proof (state)
this:
(2 * n + 1) * n + (2 * n + 1) * 1 < p * t

goal (1 subgoal):
 1. t < p
[PROOF STEP]
hence "p*t > 2*n*n + n + 2*n + 1"
[PROOF STATE]
proof (prove)
using this:
(2 * n + 1) * n + (2 * n + 1) * 1 < p * t

goal (1 subgoal):
 1. 2 * n * n + n + 2 * n + 1 < p * t
[PROOF STEP]
by (simp only: distrib_right mult_1_left)
[PROOF STATE]
proof (state)
this:
2 * n * n + n + 2 * n + 1 < p * t

goal (1 subgoal):
 1. t < p
[PROOF STEP]
with n0
[PROOF STATE]
proof (chain)
picking this:
0 < n
2 * n * n + n + 2 * n + 1 < p * t
[PROOF STEP]
have "p*t > 2*n^2 + 1"
[PROOF STATE]
proof (prove)
using this:
0 < n
2 * n * n + n + 2 * n + 1 < p * t

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

goal (1 subgoal):
 1. t < p
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
n + 1 < t \<Longrightarrow> 2 * n\<^sup>2 + 1 < p * t

goal (1 subgoal):
 1. t < p
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
p * t \<le> 2 * n\<^sup>2 + 1
n + 1 < t \<Longrightarrow> 2 * n\<^sup>2 + 1 < p * t
[PROOF STEP]
have "\<not> t > n+1"
[PROOF STATE]
proof (prove)
using this:
p * t \<le> 2 * n\<^sup>2 + 1
n + 1 < t \<Longrightarrow> 2 * n\<^sup>2 + 1 < p * t

goal (1 subgoal):
 1. \<not> n + 1 < t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> n + 1 < t

goal (1 subgoal):
 1. t < p
[PROOF STEP]
with n0 n
[PROOF STATE]
proof (chain)
picking this:
0 < n
p = 2 * n + 1
\<not> n + 1 < t
[PROOF STEP]
show "t < p"
[PROOF STATE]
proof (prove)
using this:
0 < n
p = 2 * n + 1
\<not> n + 1 < t

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 < t \<and> t < p

goal (1 subgoal):
 1. \<lbrakk>prime (nat p); odd p\<rbrakk> \<Longrightarrow> \<exists>t>0. t < p \<and> is_sum4sq_int (p * t)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
is_sum4sq_int (p * t)
0 < t \<and> t < p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_sum4sq_int (p * t)
0 < t \<and> t < p

goal (1 subgoal):
 1. \<exists>t>0. t < p \<and> is_sum4sq_int (p * t)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>t>0. t < p \<and> is_sum4sq_int (p * t)

goal:
No subgoals!
[PROOF STEP]
qed