[STATEMENT]
lemma sots1_aux:
  assumes "prime (4*k+3)"
  assumes "odd (multiplicity (4*k+3) n)"
  shows "\<not> is_sum2sq_nat n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_sum2sq_nat n
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
assume "is_sum2sq_nat n"
[PROOF STATE]
proof (state)
this:
is_sum2sq_nat n

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_sum2sq_nat n
[PROOF STEP]
obtain a b where h1: "n = a^2 + b^2"
[PROOF STATE]
proof (prove)
using this:
is_sum2sq_nat n

goal (1 subgoal):
 1. (\<And>a b. n = a\<^sup>2 + b\<^sup>2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding is_sum2sq_nat_def sum2sq_nat_def
[PROOF STATE]
proof (prove)
using this:
\<exists>a b. n = a\<^sup>2 + b\<^sup>2

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

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
have ab_nz: "a \<noteq> 0 \<or> b \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<noteq> 0 \<or> b \<noteq> 0
[PROOF STEP]
by (rule ccontr) (insert assms, auto simp: h1)
[PROOF STATE]
proof (state)
this:
a \<noteq> 0 \<or> b \<noteq> 0

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
let ?p = "4*k+3"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
let ?g = "gcd a b"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
have h2: "?g \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcd a b \<noteq> 0
[PROOF STEP]
using assms(2) h1 odd_pos
[PROOF STATE]
proof (prove)
using this:
odd (multiplicity (4 * k + 3) n)
n = a\<^sup>2 + b\<^sup>2
odd ?n \<Longrightarrow> 0 < ?n

goal (1 subgoal):
 1. gcd a b \<noteq> 0
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
gcd a b \<noteq> 0

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
gcd a b \<noteq> 0
[PROOF STEP]
obtain a' b' where h3: "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
[PROOF STATE]
proof (prove)
using this:
gcd a b \<noteq> 0

goal (1 subgoal):
 1. (\<And>a' b'. \<lbrakk>a = a' * gcd a b; b = b' * gcd a b; coprime a' b'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using gcd_coprime_exists
[PROOF STATE]
proof (prove)
using this:
gcd a b \<noteq> 0
gcd ?a ?b \<noteq> (0::?'a) \<Longrightarrow> \<exists>a' b'. ?a = a' * gcd ?a ?b \<and> ?b = b' * gcd ?a ?b \<and> coprime a' b'

goal (1 subgoal):
 1. (\<And>a' b'. \<lbrakk>a = a' * gcd a b; b = b' * gcd a b; coprime a' b'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a = a' * gcd a b
b = b' * gcd a b
coprime a' b'

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
have "?g^2 dvd n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (gcd a b)\<^sup>2 dvd n
[PROOF STEP]
using dvd_add h1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?a dvd ?b; ?a dvd ?c\<rbrakk> \<Longrightarrow> ?a dvd ?b + ?c
n = a\<^sup>2 + b\<^sup>2

goal (1 subgoal):
 1. (gcd a b)\<^sup>2 dvd n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(gcd a b)\<^sup>2 dvd n

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(gcd a b)\<^sup>2 dvd n
[PROOF STEP]
obtain m where h4: "m * ?g^2 = n"
[PROOF STATE]
proof (prove)
using this:
(gcd a b)\<^sup>2 dvd n

goal (1 subgoal):
 1. (\<And>m. m * (gcd a b)\<^sup>2 = n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using dvd_div_mult_self
[PROOF STATE]
proof (prove)
using this:
(gcd a b)\<^sup>2 dvd n
?a dvd ?b \<Longrightarrow> ?b div ?a * ?a = ?b

goal (1 subgoal):
 1. (\<And>m. m * (gcd a b)\<^sup>2 = n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
m * (gcd a b)\<^sup>2 = n

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
m * (gcd a b)\<^sup>2 = n

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
have "\<dots> = (a' * ?g)^2 + (b' * ?g)^2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n = (a' * gcd a b)\<^sup>2 + (b' * gcd a b)\<^sup>2
[PROOF STEP]
unfolding h1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a\<^sup>2 + b\<^sup>2 = (a' * gcd a b)\<^sup>2 + (b' * gcd a b)\<^sup>2
[PROOF STEP]
using h3
[PROOF STATE]
proof (prove)
using this:
a = a' * gcd a b
b = b' * gcd a b
coprime a' b'

goal (1 subgoal):
 1. a\<^sup>2 + b\<^sup>2 = (a' * gcd a b)\<^sup>2 + (b' * gcd a b)\<^sup>2
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
n = (a' * gcd a b)\<^sup>2 + (b' * gcd a b)\<^sup>2

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
n = (a' * gcd a b)\<^sup>2 + (b' * gcd a b)\<^sup>2

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
have "\<dots> = ?g^2 * a'^2 + ?g^2 * b'^2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a' * gcd a b)\<^sup>2 + (b' * gcd a b)\<^sup>2 = (gcd a b)\<^sup>2 * a'\<^sup>2 + (gcd a b)\<^sup>2 * b'\<^sup>2
[PROOF STEP]
unfolding power2_eq_square
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a' * gcd a b * (a' * gcd a b) + b' * gcd a b * (b' * gcd a b) = gcd a b * gcd a b * (a' * a') + gcd a b * gcd a b * (b' * b')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(a' * gcd a b)\<^sup>2 + (b' * gcd a b)\<^sup>2 = (gcd a b)\<^sup>2 * a'\<^sup>2 + (gcd a b)\<^sup>2 * b'\<^sup>2

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
m * (gcd a b)\<^sup>2 = (gcd a b)\<^sup>2 * a'\<^sup>2 + (gcd a b)\<^sup>2 * b'\<^sup>2
[PROOF STEP]
have "?g^2 * m = ?g^2 * (a'^2 + b'^2)"
[PROOF STATE]
proof (prove)
using this:
m * (gcd a b)\<^sup>2 = (gcd a b)\<^sup>2 * a'\<^sup>2 + (gcd a b)\<^sup>2 * b'\<^sup>2

goal (1 subgoal):
 1. (gcd a b)\<^sup>2 * m = (gcd a b)\<^sup>2 * (a'\<^sup>2 + b'\<^sup>2)
[PROOF STEP]
by (simp add: distrib_left mult.commute)
[PROOF STATE]
proof (state)
this:
(gcd a b)\<^sup>2 * m = (gcd a b)\<^sup>2 * (a'\<^sup>2 + b'\<^sup>2)

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
hence h5: "m = a'^2 + b'^2"
[PROOF STATE]
proof (prove)
using this:
(gcd a b)\<^sup>2 * m = (gcd a b)\<^sup>2 * (a'\<^sup>2 + b'\<^sup>2)

goal (1 subgoal):
 1. m = a'\<^sup>2 + b'\<^sup>2
[PROOF STEP]
using h2
[PROOF STATE]
proof (prove)
using this:
(gcd a b)\<^sup>2 * m = (gcd a b)\<^sup>2 * (a'\<^sup>2 + b'\<^sup>2)
gcd a b \<noteq> 0

goal (1 subgoal):
 1. m = a'\<^sup>2 + b'\<^sup>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
m = a'\<^sup>2 + b'\<^sup>2

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
let ?mul = "multiplicity ?p ?g"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
have "multiplicity ?p (?g^2) = ?mul + ?mul"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicity (4 * k + 3) ((gcd a b)\<^sup>2) = multiplicity (4 * k + 3) (gcd a b) + multiplicity (4 * k + 3) (gcd a b)
[PROOF STEP]
unfolding power2_eq_square
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicity (4 * k + 3) (gcd a b * gcd a b) = multiplicity (4 * k + 3) (gcd a b) + multiplicity (4 * k + 3) (gcd a b)
[PROOF STEP]
using h2 assms
[PROOF STATE]
proof (prove)
using this:
gcd a b \<noteq> 0
prime (4 * k + 3)
odd (multiplicity (4 * k + 3) n)

goal (1 subgoal):
 1. multiplicity (4 * k + 3) (gcd a b * gcd a b) = multiplicity (4 * k + 3) (gcd a b) + multiplicity (4 * k + 3) (gcd a b)
[PROOF STEP]
by (subst prime_elem_multiplicity_mult_distrib) simp_all
[PROOF STATE]
proof (state)
this:
multiplicity (4 * k + 3) ((gcd a b)\<^sup>2) = multiplicity (4 * k + 3) (gcd a b) + multiplicity (4 * k + 3) (gcd a b)

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
hence "even (multiplicity ?p (?g^2))"
[PROOF STATE]
proof (prove)
using this:
multiplicity (4 * k + 3) ((gcd a b)\<^sup>2) = multiplicity (4 * k + 3) (gcd a b) + multiplicity (4 * k + 3) (gcd a b)

goal (1 subgoal):
 1. even (multiplicity (4 * k + 3) ((gcd a b)\<^sup>2))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
even (multiplicity (4 * k + 3) ((gcd a b)\<^sup>2))

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
even (multiplicity (4 * k + 3) ((gcd a b)\<^sup>2))

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
have "m \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<noteq> 0
[PROOF STEP]
using assms(2) h4 odd_pos
[PROOF STATE]
proof (prove)
using this:
odd (multiplicity (4 * k + 3) n)
m * (gcd a b)\<^sup>2 = n
odd ?n \<Longrightarrow> 0 < ?n

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

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
even (multiplicity (4 * k + 3) ((gcd a b)\<^sup>2))
m \<noteq> 0
[PROOF STEP]
have "odd (multiplicity ?p m)"
[PROOF STATE]
proof (prove)
using this:
even (multiplicity (4 * k + 3) ((gcd a b)\<^sup>2))
m \<noteq> 0

goal (1 subgoal):
 1. odd (multiplicity (4 * k + 3) m)
[PROOF STEP]
using assms ab_nz
[PROOF STATE]
proof (prove)
using this:
even (multiplicity (4 * k + 3) ((gcd a b)\<^sup>2))
m \<noteq> 0
prime (4 * k + 3)
odd (multiplicity (4 * k + 3) n)
a \<noteq> 0 \<or> b \<noteq> 0

goal (1 subgoal):
 1. odd (multiplicity (4 * k + 3) m)
[PROOF STEP]
by (simp_all add: h4 [symmetric] prime_elem_multiplicity_mult_distrib)
[PROOF STATE]
proof (state)
this:
odd (multiplicity (4 * k + 3) m)

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
hence "?p dvd m"
[PROOF STATE]
proof (prove)
using this:
odd (multiplicity (4 * k + 3) m)

goal (1 subgoal):
 1. 4 * k + 3 dvd m
[PROOF STEP]
using not_dvd_imp_multiplicity_0
[PROOF STATE]
proof (prove)
using this:
odd (multiplicity (4 * k + 3) m)
\<not> ?p dvd ?x \<Longrightarrow> multiplicity ?p ?x = 0

goal (1 subgoal):
 1. 4 * k + 3 dvd m
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
4 * k + 3 dvd m

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
hence h6: "?p dvd a'^2+b'^2"
[PROOF STATE]
proof (prove)
using this:
4 * k + 3 dvd m

goal (1 subgoal):
 1. 4 * k + 3 dvd a'\<^sup>2 + b'\<^sup>2
[PROOF STEP]
using h5
[PROOF STATE]
proof (prove)
using this:
4 * k + 3 dvd m
m = a'\<^sup>2 + b'\<^sup>2

goal (1 subgoal):
 1. 4 * k + 3 dvd a'\<^sup>2 + b'\<^sup>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
4 * k + 3 dvd a'\<^sup>2 + b'\<^sup>2

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
4 * k + 3 dvd a'\<^sup>2 + b'\<^sup>2

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
assume "?p dvd a'^2"
[PROOF STATE]
proof (state)
this:
4 * k + 3 dvd a'\<^sup>2

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
4 * k + 3 dvd a'\<^sup>2

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
hence "?p dvd b'^2"
[PROOF STATE]
proof (prove)
using this:
4 * k + 3 dvd a'\<^sup>2

goal (1 subgoal):
 1. 4 * k + 3 dvd b'\<^sup>2
[PROOF STEP]
using h6 dvd_add_right_iff
[PROOF STATE]
proof (prove)
using this:
4 * k + 3 dvd a'\<^sup>2
4 * k + 3 dvd a'\<^sup>2 + b'\<^sup>2
?a dvd ?b \<Longrightarrow> (?a dvd ?b + ?c) = (?a dvd ?c)

goal (1 subgoal):
 1. 4 * k + 3 dvd b'\<^sup>2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
4 * k + 3 dvd b'\<^sup>2

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
4 * k + 3 dvd a'\<^sup>2
4 * k + 3 dvd b'\<^sup>2
[PROOF STEP]
have "?p dvd a'" "?p dvd b'"
[PROOF STATE]
proof (prove)
using this:
4 * k + 3 dvd a'\<^sup>2
4 * k + 3 dvd b'\<^sup>2

goal (1 subgoal):
 1. 4 * k + 3 dvd a' &&& 4 * k + 3 dvd b'
[PROOF STEP]
using assms(1) prime_dvd_power_nat
[PROOF STATE]
proof (prove)
using this:
4 * k + 3 dvd a'\<^sup>2
4 * k + 3 dvd b'\<^sup>2
prime (4 * k + 3)
\<lbrakk>prime ?p; ?p dvd ?x ^ ?n\<rbrakk> \<Longrightarrow> ?p dvd ?x

goal (1 subgoal):
 1. 4 * k + 3 dvd a' &&& 4 * k + 3 dvd b'
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
4 * k + 3 dvd a'
4 * k + 3 dvd b'

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
hence "False"
[PROOF STATE]
proof (prove)
using this:
4 * k + 3 dvd a'
4 * k + 3 dvd b'

goal (1 subgoal):
 1. False
[PROOF STEP]
using assms(1) h3(3) coprime_common_divisor_nat[of a' b' ?p] not_prime_1
[PROOF STATE]
proof (prove)
using this:
4 * k + 3 dvd a'
4 * k + 3 dvd b'
prime (4 * k + 3)
coprime a' b'
\<lbrakk>coprime a' b'; 4 * k + 3 dvd a'; 4 * k + 3 dvd b'\<rbrakk> \<Longrightarrow> 4 * k + 3 = 1
\<not> prime (1::?'a)

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

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
4 * k + 3 dvd a'\<^sup>2 \<Longrightarrow> False

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
hence "\<not> (?p dvd a'^2)"
[PROOF STATE]
proof (prove)
using this:
4 * k + 3 dvd a'\<^sup>2 \<Longrightarrow> False

goal (1 subgoal):
 1. \<not> 4 * k + 3 dvd a'\<^sup>2
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<not> 4 * k + 3 dvd a'\<^sup>2

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
hence h7: "\<not> (?p dvd a')"
[PROOF STATE]
proof (prove)
using this:
\<not> 4 * k + 3 dvd a'\<^sup>2

goal (1 subgoal):
 1. \<not> 4 * k + 3 dvd a'
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
\<not> 4 * k + 3 dvd a'\<^sup>2
prime (4 * k + 3)

goal (1 subgoal):
 1. \<not> 4 * k + 3 dvd a'
[PROOF STEP]
by (simp add: power2_eq_square prime_dvd_mult_iff)
[PROOF STATE]
proof (state)
this:
\<not> 4 * k + 3 dvd a'

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
hence "coprime ?p a'"
[PROOF STATE]
proof (prove)
using this:
\<not> 4 * k + 3 dvd a'

goal (1 subgoal):
 1. coprime (4 * k + 3) a'
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
\<not> 4 * k + 3 dvd a'
prime (4 * k + 3)

goal (1 subgoal):
 1. coprime (4 * k + 3) a'
[PROOF STEP]
by (simp add: prime_imp_coprime)
[PROOF STATE]
proof (state)
this:
coprime (4 * k + 3) a'

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
thm prime_imp_coprime_nat
[PROOF STATE]
proof (state)
this:
coprime (4 * k + 3) a'

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
coprime (4 * k + 3) a'

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
have "a' \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a' \<noteq> 0
[PROOF STEP]
using h7 dvd_0_right[of ?p]
[PROOF STATE]
proof (prove)
using this:
\<not> 4 * k + 3 dvd a'
4 * k + 3 dvd 0

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

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
coprime (4 * k + 3) a'
a' \<noteq> 0
[PROOF STEP]
obtain ainv aux where "a' * ainv = ?p * aux + 1"
[PROOF STATE]
proof (prove)
using this:
coprime (4 * k + 3) a'
a' \<noteq> 0

goal (1 subgoal):
 1. (\<And>ainv aux. a' * ainv = (4 * k + 3) * aux + 1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using bezout_nat[of "a'" ?p]
[PROOF STATE]
proof (prove)
using this:
coprime (4 * k + 3) a'
a' \<noteq> 0
a' \<noteq> 0 \<Longrightarrow> \<exists>x y. a' * x = (4 * k + 3) * y + gcd a' (4 * k + 3)

goal (1 subgoal):
 1. (\<And>ainv aux. a' * ainv = (4 * k + 3) * aux + 1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: ac_simps)
[PROOF STATE]
proof (state)
this:
a' * ainv = (4 * k + 3) * aux + 1

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
hence "[a' * ainv = 1] (mod ?p)"
[PROOF STATE]
proof (prove)
using this:
a' * ainv = (4 * k + 3) * aux + 1

goal (1 subgoal):
 1. [a' * ainv = 1] (mod 4 * k + 3)
[PROOF STEP]
using cong_to_1'_nat
[PROOF STATE]
proof (prove)
using this:
a' * ainv = (4 * k + 3) * aux + 1
[?a = 1] (mod ?n) = (?a = 0 \<and> ?n = 1 \<or> (\<exists>m. ?a = 1 + m * ?n))

goal (1 subgoal):
 1. [a' * ainv = 1] (mod 4 * k + 3)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
[a' * ainv = 1] (mod 4 * k + 3)

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
from cong_mult [OF this this]
[PROOF STATE]
proof (chain)
picking this:
[a' * ainv * (a' * ainv) = 1 * 1] (mod 4 * k + 3)
[PROOF STEP]
have h11: "[1 = ainv^2 * a'^2] (mod ?p)"
[PROOF STATE]
proof (prove)
using this:
[a' * ainv * (a' * ainv) = 1 * 1] (mod 4 * k + 3)

goal (1 subgoal):
 1. [1 = ainv\<^sup>2 * a'\<^sup>2] (mod 4 * k + 3)
[PROOF STEP]
unfolding power2_eq_square
[PROOF STATE]
proof (prove)
using this:
[a' * ainv * (a' * ainv) = 1 * 1] (mod 4 * k + 3)

goal (1 subgoal):
 1. [1 = ainv * ainv * (a' * a')] (mod 4 * k + 3)
[PROOF STEP]
by (simp add: algebra_simps cong_sym)
[PROOF STATE]
proof (state)
this:
[1 = ainv\<^sup>2 * a'\<^sup>2] (mod 4 * k + 3)

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
let ?bdiva = "ainv * b'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
have "[ainv^2 * (a'^2 + b'^2) = 0] (mod ?p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [ainv\<^sup>2 * (a'\<^sup>2 + b'\<^sup>2) = 0] (mod 4 * k + 3)
[PROOF STEP]
using h6 cong_dvd_modulus_nat cong_mult_self_right
[PROOF STATE]
proof (prove)
using this:
4 * k + 3 dvd a'\<^sup>2 + b'\<^sup>2
\<lbrakk>[?x = ?y] (mod ?m); ?n dvd ?m\<rbrakk> \<Longrightarrow> [?x = ?y] (mod ?n)
[?b * ?a = 0::?'a] (mod ?a)

goal (1 subgoal):
 1. [ainv\<^sup>2 * (a'\<^sup>2 + b'\<^sup>2) = 0] (mod 4 * k + 3)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[ainv\<^sup>2 * (a'\<^sup>2 + b'\<^sup>2) = 0] (mod 4 * k + 3)

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
from cong_add [OF h11 this]
[PROOF STATE]
proof (chain)
picking this:
[1 + ainv\<^sup>2 * (a'\<^sup>2 + b'\<^sup>2) = ainv\<^sup>2 * a'\<^sup>2 + 0] (mod 4 * k + 3)
[PROOF STEP]
have "[1 + ainv^2 * b'^2 = 0] (mod ?p)"
[PROOF STATE]
proof (prove)
using this:
[1 + ainv\<^sup>2 * (a'\<^sup>2 + b'\<^sup>2) = ainv\<^sup>2 * a'\<^sup>2 + 0] (mod 4 * k + 3)

goal (1 subgoal):
 1. [1 + ainv\<^sup>2 * b'\<^sup>2 = 0] (mod 4 * k + 3)
[PROOF STEP]
unfolding add_mult_distrib2
[PROOF STATE]
proof (prove)
using this:
[1 + (ainv\<^sup>2 * a'\<^sup>2 + ainv\<^sup>2 * b'\<^sup>2) = ainv\<^sup>2 * a'\<^sup>2 + 0] (mod 4 * k + 3)

goal (1 subgoal):
 1. [1 + ainv\<^sup>2 * b'\<^sup>2 = 0] (mod 4 * k + 3)
[PROOF STEP]
using cong_add_lcancel_nat[of "ainv^2 * a'^2"]
[PROOF STATE]
proof (prove)
using this:
[1 + (ainv\<^sup>2 * a'\<^sup>2 + ainv\<^sup>2 * b'\<^sup>2) = ainv\<^sup>2 * a'\<^sup>2 + 0] (mod 4 * k + 3)
[ainv\<^sup>2 * a'\<^sup>2 + ?x = ainv\<^sup>2 * a'\<^sup>2 + ?y] (mod ?n) = [?x = ?y] (mod ?n)

goal (1 subgoal):
 1. [1 + ainv\<^sup>2 * b'\<^sup>2 = 0] (mod 4 * k + 3)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
[1 + ainv\<^sup>2 * b'\<^sup>2 = 0] (mod 4 * k + 3)

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
hence h8: "[?bdiva^2 + 1 = 0] (mod ?p)"
[PROOF STATE]
proof (prove)
using this:
[1 + ainv\<^sup>2 * b'\<^sup>2 = 0] (mod 4 * k + 3)

goal (1 subgoal):
 1. [(ainv * b')\<^sup>2 + 1 = 0] (mod 4 * k + 3)
[PROOF STEP]
by (simp add: power_mult_distrib)
[PROOF STATE]
proof (state)
this:
[(ainv * b')\<^sup>2 + 1 = 0] (mod 4 * k + 3)

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
[(ainv * b')\<^sup>2 + 1 = 0] (mod 4 * k + 3)

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
assume "?p dvd ?bdiva"
[PROOF STATE]
proof (state)
this:
4 * k + 3 dvd ainv * b'

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
hence "?p dvd (?bdiva^2)"
[PROOF STATE]
proof (prove)
using this:
4 * k + 3 dvd ainv * b'

goal (1 subgoal):
 1. 4 * k + 3 dvd (ainv * b')\<^sup>2
[PROOF STEP]
by (simp add: assms(1) prime_dvd_power_nat_iff)
[PROOF STATE]
proof (state)
this:
4 * k + 3 dvd (ainv * b')\<^sup>2

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
hence "[?bdiva^2 = 0] (mod ?p)"
[PROOF STATE]
proof (prove)
using this:
4 * k + 3 dvd (ainv * b')\<^sup>2

goal (1 subgoal):
 1. [(ainv * b')\<^sup>2 = 0] (mod 4 * k + 3)
[PROOF STEP]
using cong_altdef_nat
[PROOF STATE]
proof (prove)
using this:
4 * k + 3 dvd (ainv * b')\<^sup>2
?b \<le> ?a \<Longrightarrow> [?a = ?b] (mod ?m) = (?m dvd ?a - ?b)

goal (1 subgoal):
 1. [(ainv * b')\<^sup>2 = 0] (mod 4 * k + 3)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
[(ainv * b')\<^sup>2 = 0] (mod 4 * k + 3)

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
hence "[?bdiva^2 +1 = 1] (mod ?p)"
[PROOF STATE]
proof (prove)
using this:
[(ainv * b')\<^sup>2 = 0] (mod 4 * k + 3)

goal (1 subgoal):
 1. [(ainv * b')\<^sup>2 + 1 = 1] (mod 4 * k + 3)
[PROOF STEP]
using cong_add_rcancel_0_nat
[PROOF STATE]
proof (prove)
using this:
[(ainv * b')\<^sup>2 = 0] (mod 4 * k + 3)
[?x + ?a = ?a] (mod ?n) = [?x = 0] (mod ?n)

goal (1 subgoal):
 1. [(ainv * b')\<^sup>2 + 1 = 1] (mod 4 * k + 3)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[(ainv * b')\<^sup>2 + 1 = 1] (mod 4 * k + 3)

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
from this h8
[PROOF STATE]
proof (chain)
picking this:
[(ainv * b')\<^sup>2 + 1 = 1] (mod 4 * k + 3)
[(ainv * b')\<^sup>2 + 1 = 0] (mod 4 * k + 3)
[PROOF STEP]
have "[0 = 1] (mod ?p)"
[PROOF STATE]
proof (prove)
using this:
[(ainv * b')\<^sup>2 + 1 = 1] (mod 4 * k + 3)
[(ainv * b')\<^sup>2 + 1 = 0] (mod 4 * k + 3)

goal (1 subgoal):
 1. [0 = 1] (mod 4 * k + 3)
[PROOF STEP]
using cong_sym cong_trans
[PROOF STATE]
proof (prove)
using this:
[(ainv * b')\<^sup>2 + 1 = 1] (mod 4 * k + 3)
[(ainv * b')\<^sup>2 + 1 = 0] (mod 4 * k + 3)
[?b = ?c] (mod ?a) \<Longrightarrow> [?c = ?b] (mod ?a)
\<lbrakk>[?b = ?c] (mod ?a); [?c = ?d] (mod ?a)\<rbrakk> \<Longrightarrow> [?b = ?d] (mod ?a)

goal (1 subgoal):
 1. [0 = 1] (mod 4 * k + 3)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[0 = 1] (mod 4 * k + 3)

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
hence "?p dvd 1"
[PROOF STATE]
proof (prove)
using this:
[0 = 1] (mod 4 * k + 3)

goal (1 subgoal):
 1. is_unit (4 * k + 3)
[PROOF STEP]
using cong_0_1_nat
[PROOF STATE]
proof (prove)
using this:
[0 = 1] (mod 4 * k + 3)
[0 = 1] (mod ?n) = (?n = 1)

goal (1 subgoal):
 1. is_unit (4 * k + 3)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_unit (4 * k + 3)

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
hence "False"
[PROOF STATE]
proof (prove)
using this:
is_unit (4 * k + 3)

goal (1 subgoal):
 1. False
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
is_unit (4 * k + 3)
prime (4 * k + 3)

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

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
4 * k + 3 dvd ainv * b' \<Longrightarrow> False

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
hence "\<not> (?p dvd ?bdiva)"
[PROOF STATE]
proof (prove)
using this:
4 * k + 3 dvd ainv * b' \<Longrightarrow> False

goal (1 subgoal):
 1. \<not> 4 * k + 3 dvd ainv * b'
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<not> 4 * k + 3 dvd ainv * b'

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
hence h9: "[?bdiva^(?p-1) = 1] (mod ?p)"
[PROOF STATE]
proof (prove)
using this:
\<not> 4 * k + 3 dvd ainv * b'

goal (1 subgoal):
 1. [(ainv * b') ^ (4 * k + 3 - 1) = 1] (mod 4 * k + 3)
[PROOF STEP]
using assms(1) fermat_theorem [of ?p ?bdiva]
[PROOF STATE]
proof (prove)
using this:
\<not> 4 * k + 3 dvd ainv * b'
prime (4 * k + 3)
\<lbrakk>prime (4 * k + 3); \<not> 4 * k + 3 dvd ainv * b'\<rbrakk> \<Longrightarrow> [(ainv * b') ^ (4 * k + 3 - 1) = 1] (mod 4 * k + 3)

goal (1 subgoal):
 1. [(ainv * b') ^ (4 * k + 3 - 1) = 1] (mod 4 * k + 3)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[(ainv * b') ^ (4 * k + 3 - 1) = 1] (mod 4 * k + 3)

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
have h10: "?p\<ge>3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 3 \<le> 4 * k + 3
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
3 \<le> 4 * k + 3

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
have h11: "[?bdiva^(4*k+2) = 1] (mod ?p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [(ainv * b') ^ (4 * k + 2) = 1] (mod 4 * k + 3)
[PROOF STEP]
using h9
[PROOF STATE]
proof (prove)
using this:
[(ainv * b') ^ (4 * k + 3 - 1) = 1] (mod 4 * k + 3)

goal (1 subgoal):
 1. [(ainv * b') ^ (4 * k + 2) = 1] (mod 4 * k + 3)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
[(ainv * b') ^ (4 * k + 2) = 1] (mod 4 * k + 3)

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
have "[(?bdiva^2 + 1)^2 = 0] (mod ?p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [((ainv * b')\<^sup>2 + 1)\<^sup>2 = 0] (mod 4 * k + 3)
[PROOF STEP]
using h8 cong_pow [of "?bdiva^2 + 1" 0 ?p 2]
[PROOF STATE]
proof (prove)
using this:
[(ainv * b')\<^sup>2 + 1 = 0] (mod 4 * k + 3)
[(ainv * b')\<^sup>2 + 1 = 0] (mod 4 * k + 3) \<Longrightarrow> [((ainv * b')\<^sup>2 + 1)\<^sup>2 = 0\<^sup>2] (mod 4 * k + 3)

goal (1 subgoal):
 1. [((ainv * b')\<^sup>2 + 1)\<^sup>2 = 0] (mod 4 * k + 3)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
[((ainv * b')\<^sup>2 + 1)\<^sup>2 = 0] (mod 4 * k + 3)

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
[((ainv * b')\<^sup>2 + 1)\<^sup>2 = 0] (mod 4 * k + 3)

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
have "?bdiva ^ 4 = (?bdiva ^ 2) ^ 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ainv * b') ^ 4 = ((ainv * b')\<^sup>2)\<^sup>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(ainv * b') ^ 4 = ((ainv * b')\<^sup>2)\<^sup>2

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
hence "(?bdiva^2 + 1)^2 = ?bdiva^4 + ?bdiva^2 + ?bdiva^2 + 1"
[PROOF STATE]
proof (prove)
using this:
(ainv * b') ^ 4 = ((ainv * b')\<^sup>2)\<^sup>2

goal (1 subgoal):
 1. ((ainv * b')\<^sup>2 + 1)\<^sup>2 = (ainv * b') ^ 4 + (ainv * b')\<^sup>2 + (ainv * b')\<^sup>2 + 1
[PROOF STEP]
by (auto simp: algebra_simps power2_eq_square)
[PROOF STATE]
proof (state)
this:
((ainv * b')\<^sup>2 + 1)\<^sup>2 = (ainv * b') ^ 4 + (ainv * b')\<^sup>2 + (ainv * b')\<^sup>2 + 1

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
[((ainv * b')\<^sup>2 + 1)\<^sup>2 = 0] (mod 4 * k + 3)
((ainv * b')\<^sup>2 + 1)\<^sup>2 = (ainv * b') ^ 4 + (ainv * b')\<^sup>2 + (ainv * b')\<^sup>2 + 1
[PROOF STEP]
have "[?bdiva^4 + ?bdiva^2 + ?bdiva^2 + 1 = 0] (mod ?p)"
[PROOF STATE]
proof (prove)
using this:
[((ainv * b')\<^sup>2 + 1)\<^sup>2 = 0] (mod 4 * k + 3)
((ainv * b')\<^sup>2 + 1)\<^sup>2 = (ainv * b') ^ 4 + (ainv * b')\<^sup>2 + (ainv * b')\<^sup>2 + 1

goal (1 subgoal):
 1. [(ainv * b') ^ 4 + (ainv * b')\<^sup>2 + (ainv * b')\<^sup>2 + 1 = 0] (mod 4 * k + 3)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[(ainv * b') ^ 4 + (ainv * b')\<^sup>2 + (ainv * b')\<^sup>2 + 1 = 0] (mod 4 * k + 3)

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
[(ainv * b') ^ 4 + (ainv * b')\<^sup>2 + (ainv * b')\<^sup>2 + 1 = 0] (mod 4 * k + 3)

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
have "[?bdiva^4 + ?bdiva^2 + (?bdiva^2 + 1) = ?bdiva^4 + ?bdiva^2 + 0] (mod ?p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [(ainv * b') ^ 4 + (ainv * b')\<^sup>2 + ((ainv * b')\<^sup>2 + 1) = (ainv * b') ^ 4 + (ainv * b')\<^sup>2 + 0] (mod 4 * k + 3)
[PROOF STEP]
using h8 cong_add_lcancel_nat
[PROOF STATE]
proof (prove)
using this:
[(ainv * b')\<^sup>2 + 1 = 0] (mod 4 * k + 3)
[?a + ?x = ?a + ?y] (mod ?n) = [?x = ?y] (mod ?n)

goal (1 subgoal):
 1. [(ainv * b') ^ 4 + (ainv * b')\<^sup>2 + ((ainv * b')\<^sup>2 + 1) = (ainv * b') ^ 4 + (ainv * b')\<^sup>2 + 0] (mod 4 * k + 3)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[(ainv * b') ^ 4 + (ainv * b')\<^sup>2 + ((ainv * b')\<^sup>2 + 1) = (ainv * b') ^ 4 + (ainv * b')\<^sup>2 + 0] (mod 4 * k + 3)

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
[(ainv * b') ^ 4 + (ainv * b')\<^sup>2 + (ainv * b')\<^sup>2 + 1 = 0] (mod 4 * k + 3)
[(ainv * b') ^ 4 + (ainv * b')\<^sup>2 + ((ainv * b')\<^sup>2 + 1) = (ainv * b') ^ 4 + (ainv * b')\<^sup>2 + 0] (mod 4 * k + 3)
[PROOF STEP]
have "[?bdiva^4 + ?bdiva^2 = 0] (mod ?p)"
[PROOF STATE]
proof (prove)
using this:
[(ainv * b') ^ 4 + (ainv * b')\<^sup>2 + (ainv * b')\<^sup>2 + 1 = 0] (mod 4 * k + 3)
[(ainv * b') ^ 4 + (ainv * b')\<^sup>2 + ((ainv * b')\<^sup>2 + 1) = (ainv * b') ^ 4 + (ainv * b')\<^sup>2 + 0] (mod 4 * k + 3)

goal (1 subgoal):
 1. [(ainv * b') ^ 4 + (ainv * b')\<^sup>2 = 0] (mod 4 * k + 3)
[PROOF STEP]
by (simp add: cong_def)
[PROOF STATE]
proof (state)
this:
[(ainv * b') ^ 4 + (ainv * b')\<^sup>2 = 0] (mod 4 * k + 3)

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
hence "[?bdiva^4 + ?bdiva^2 + 1 = 0 + 1] (mod ?p)"
[PROOF STATE]
proof (prove)
using this:
[(ainv * b') ^ 4 + (ainv * b')\<^sup>2 = 0] (mod 4 * k + 3)

goal (1 subgoal):
 1. [(ainv * b') ^ 4 + (ainv * b')\<^sup>2 + 1 = 0 + 1] (mod 4 * k + 3)
[PROOF STEP]
using cong_add_rcancel_nat
[PROOF STATE]
proof (prove)
using this:
[(ainv * b') ^ 4 + (ainv * b')\<^sup>2 = 0] (mod 4 * k + 3)
[?x + ?a = ?y + ?a] (mod ?n) = [?x = ?y] (mod ?n)

goal (1 subgoal):
 1. [(ainv * b') ^ 4 + (ainv * b')\<^sup>2 + 1 = 0 + 1] (mod 4 * k + 3)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[(ainv * b') ^ 4 + (ainv * b')\<^sup>2 + 1 = 0 + 1] (mod 4 * k + 3)

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
[(ainv * b') ^ 4 + (ainv * b')\<^sup>2 + 1 = 0 + 1] (mod 4 * k + 3)

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
have "[?bdiva^4 + (?bdiva^2 + 1) = ?bdiva^4 + 0] (mod ?p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [(ainv * b') ^ 4 + ((ainv * b')\<^sup>2 + 1) = (ainv * b') ^ 4 + 0] (mod 4 * k + 3)
[PROOF STEP]
using h8 cong_add_lcancel_nat
[PROOF STATE]
proof (prove)
using this:
[(ainv * b')\<^sup>2 + 1 = 0] (mod 4 * k + 3)
[?a + ?x = ?a + ?y] (mod ?n) = [?x = ?y] (mod ?n)

goal (1 subgoal):
 1. [(ainv * b') ^ 4 + ((ainv * b')\<^sup>2 + 1) = (ainv * b') ^ 4 + 0] (mod 4 * k + 3)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[(ainv * b') ^ 4 + ((ainv * b')\<^sup>2 + 1) = (ainv * b') ^ 4 + 0] (mod 4 * k + 3)

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
[(ainv * b') ^ 4 + (ainv * b')\<^sup>2 + 1 = 0 + 1] (mod 4 * k + 3)
[(ainv * b') ^ 4 + ((ainv * b')\<^sup>2 + 1) = (ainv * b') ^ 4 + 0] (mod 4 * k + 3)
[PROOF STEP]
have "[?bdiva^4 = 1] (mod ?p)"
[PROOF STATE]
proof (prove)
using this:
[(ainv * b') ^ 4 + (ainv * b')\<^sup>2 + 1 = 0 + 1] (mod 4 * k + 3)
[(ainv * b') ^ 4 + ((ainv * b')\<^sup>2 + 1) = (ainv * b') ^ 4 + 0] (mod 4 * k + 3)

goal (1 subgoal):
 1. [(ainv * b') ^ 4 = 1] (mod 4 * k + 3)
[PROOF STEP]
by (simp add: cong_def)
[PROOF STATE]
proof (state)
this:
[(ainv * b') ^ 4 = 1] (mod 4 * k + 3)

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
hence "[(?bdiva^4)^k = 1^k] (mod ?p)"
[PROOF STATE]
proof (prove)
using this:
[(ainv * b') ^ 4 = 1] (mod 4 * k + 3)

goal (1 subgoal):
 1. [((ainv * b') ^ 4) ^ k = 1 ^ k] (mod 4 * k + 3)
[PROOF STEP]
using cong_pow
[PROOF STATE]
proof (prove)
using this:
[(ainv * b') ^ 4 = 1] (mod 4 * k + 3)
[?b = ?c] (mod ?a) \<Longrightarrow> [?b ^ ?n = ?c ^ ?n] (mod ?a)

goal (1 subgoal):
 1. [((ainv * b') ^ 4) ^ k = 1 ^ k] (mod 4 * k + 3)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[((ainv * b') ^ 4) ^ k = 1 ^ k] (mod 4 * k + 3)

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
hence h12: "[?bdiva^(4*k) = 1] (mod ?p)"
[PROOF STATE]
proof (prove)
using this:
[((ainv * b') ^ 4) ^ k = 1 ^ k] (mod 4 * k + 3)

goal (1 subgoal):
 1. [(ainv * b') ^ (4 * k) = 1] (mod 4 * k + 3)
[PROOF STEP]
by (simp add: power_mult)
[PROOF STATE]
proof (state)
this:
[(ainv * b') ^ (4 * k) = 1] (mod 4 * k + 3)

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
hence h13: "[?bdiva^(4*k)*(?bdiva^2 + 1) = 1*(?bdiva^2 + 1)] (mod ?p)"
[PROOF STATE]
proof (prove)
using this:
[(ainv * b') ^ (4 * k) = 1] (mod 4 * k + 3)

goal (1 subgoal):
 1. [(ainv * b') ^ (4 * k) * ((ainv * b')\<^sup>2 + 1) = 1 * ((ainv * b')\<^sup>2 + 1)] (mod 4 * k + 3)
[PROOF STEP]
using cong_scalar_right
[PROOF STATE]
proof (prove)
using this:
[(ainv * b') ^ (4 * k) = 1] (mod 4 * k + 3)
[?b = ?c] (mod ?a) \<Longrightarrow> [?b * ?d = ?c * ?d] (mod ?a)

goal (1 subgoal):
 1. [(ainv * b') ^ (4 * k) * ((ainv * b')\<^sup>2 + 1) = 1 * ((ainv * b')\<^sup>2 + 1)] (mod 4 * k + 3)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[(ainv * b') ^ (4 * k) * ((ainv * b')\<^sup>2 + 1) = 1 * ((ainv * b')\<^sup>2 + 1)] (mod 4 * k + 3)

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
have "?bdiva^(4*k)*(?bdiva^2 + 1) = ?bdiva^(4*k+2)+?bdiva^(4*k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ainv * b') ^ (4 * k) * ((ainv * b')\<^sup>2 + 1) = (ainv * b') ^ (4 * k + 2) + (ainv * b') ^ (4 * k)
[PROOF STEP]
unfolding add_mult_distrib2 power_add
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ainv * b') ^ (4 * k) * (ainv * b')\<^sup>2 + (ainv * b') ^ (4 * k) * 1 = (ainv * b') ^ (4 * k) * (ainv * b')\<^sup>2 + (ainv * b') ^ (4 * k)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(ainv * b') ^ (4 * k) * ((ainv * b')\<^sup>2 + 1) = (ainv * b') ^ (4 * k + 2) + (ainv * b') ^ (4 * k)

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
hence "[?bdiva^(4*k+2)+?bdiva^(4*k) = ?bdiva^2 + 1] (mod ?p)"
[PROOF STATE]
proof (prove)
using this:
(ainv * b') ^ (4 * k) * ((ainv * b')\<^sup>2 + 1) = (ainv * b') ^ (4 * k + 2) + (ainv * b') ^ (4 * k)

goal (1 subgoal):
 1. [(ainv * b') ^ (4 * k + 2) + (ainv * b') ^ (4 * k) = (ainv * b')\<^sup>2 + 1] (mod 4 * k + 3)
[PROOF STEP]
using h13
[PROOF STATE]
proof (prove)
using this:
(ainv * b') ^ (4 * k) * ((ainv * b')\<^sup>2 + 1) = (ainv * b') ^ (4 * k + 2) + (ainv * b') ^ (4 * k)
[(ainv * b') ^ (4 * k) * ((ainv * b')\<^sup>2 + 1) = 1 * ((ainv * b')\<^sup>2 + 1)] (mod 4 * k + 3)

goal (1 subgoal):
 1. [(ainv * b') ^ (4 * k + 2) + (ainv * b') ^ (4 * k) = (ainv * b')\<^sup>2 + 1] (mod 4 * k + 3)
[PROOF STEP]
unfolding nat_mult_1
[PROOF STATE]
proof (prove)
using this:
(ainv * b') ^ (4 * k) * ((ainv * b')\<^sup>2 + 1) = (ainv * b') ^ (4 * k + 2) + (ainv * b') ^ (4 * k)
[(ainv * b') ^ (4 * k) * ((ainv * b')\<^sup>2 + 1) = (ainv * b')\<^sup>2 + 1] (mod 4 * k + 3)

goal (1 subgoal):
 1. [(ainv * b') ^ (4 * k + 2) + (ainv * b') ^ (4 * k) = (ainv * b')\<^sup>2 + 1] (mod 4 * k + 3)
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
[(ainv * b') ^ (4 * k + 2) + (ainv * b') ^ (4 * k) = (ainv * b')\<^sup>2 + 1] (mod 4 * k + 3)

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
[(ainv * b') ^ (4 * k + 2) + (ainv * b') ^ (4 * k) = (ainv * b')\<^sup>2 + 1] (mod 4 * k + 3)

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
have "[?bdiva^(4*k+2) + ?bdiva^(4*k) = 1 + 1] (mod ?p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [(ainv * b') ^ (4 * k + 2) + (ainv * b') ^ (4 * k) = 1 + 1] (mod 4 * k + 3)
[PROOF STEP]
using h11 h12 cong_add
[PROOF STATE]
proof (prove)
using this:
[(ainv * b') ^ (4 * k + 2) = 1] (mod 4 * k + 3)
[(ainv * b') ^ (4 * k) = 1] (mod 4 * k + 3)
\<lbrakk>[?b = ?c] (mod ?a); [?d = ?e] (mod ?a)\<rbrakk> \<Longrightarrow> [?b + ?d = ?c + ?e] (mod ?a)

goal (1 subgoal):
 1. [(ainv * b') ^ (4 * k + 2) + (ainv * b') ^ (4 * k) = 1 + 1] (mod 4 * k + 3)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[(ainv * b') ^ (4 * k + 2) + (ainv * b') ^ (4 * k) = 1 + 1] (mod 4 * k + 3)

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
[(ainv * b') ^ (4 * k + 2) + (ainv * b') ^ (4 * k) = (ainv * b')\<^sup>2 + 1] (mod 4 * k + 3)
[(ainv * b') ^ (4 * k + 2) + (ainv * b') ^ (4 * k) = 1 + 1] (mod 4 * k + 3)
[PROOF STEP]
have "[?bdiva^2 + 1 = 2] (mod ?p)"
[PROOF STATE]
proof (prove)
using this:
[(ainv * b') ^ (4 * k + 2) + (ainv * b') ^ (4 * k) = (ainv * b')\<^sup>2 + 1] (mod 4 * k + 3)
[(ainv * b') ^ (4 * k + 2) + (ainv * b') ^ (4 * k) = 1 + 1] (mod 4 * k + 3)

goal (1 subgoal):
 1. [(ainv * b')\<^sup>2 + 1 = 2] (mod 4 * k + 3)
[PROOF STEP]
by (auto simp add: cong_def)
[PROOF STATE]
proof (state)
this:
[(ainv * b')\<^sup>2 + 1 = 2] (mod 4 * k + 3)

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
hence "[0 = 2] (mod ?p)"
[PROOF STATE]
proof (prove)
using this:
[(ainv * b')\<^sup>2 + 1 = 2] (mod 4 * k + 3)

goal (1 subgoal):
 1. [0 = 2] (mod 4 * k + 3)
[PROOF STEP]
using h8
[PROOF STATE]
proof (prove)
using this:
[(ainv * b')\<^sup>2 + 1 = 2] (mod 4 * k + 3)
[(ainv * b')\<^sup>2 + 1 = 0] (mod 4 * k + 3)

goal (1 subgoal):
 1. [0 = 2] (mod 4 * k + 3)
[PROOF STEP]
by (simp add: cong_def)
[PROOF STATE]
proof (state)
this:
[0 = 2] (mod 4 * k + 3)

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[0 = 2] (mod 4 * k + 3)
[PROOF STEP]
have "?p dvd 2"
[PROOF STATE]
proof (prove)
using this:
[0 = 2] (mod 4 * k + 3)

goal (1 subgoal):
 1. 4 * k + 3 dvd 2
[PROOF STEP]
by (auto dest: cong_dvd_iff)
[PROOF STATE]
proof (state)
this:
4 * k + 3 dvd 2

goal (1 subgoal):
 1. is_sum2sq_nat n \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
4 * k + 3 dvd 2
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
4 * k + 3 dvd 2

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sots1: assumes "is_sum2sq_nat n"
  shows "\<And> k. prime (4*k+3) \<longrightarrow> even (multiplicity (4*k+3) n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. prime (4 * k + 3) \<longrightarrow> even (multiplicity (4 * k + 3) n)
[PROOF STEP]
using sots1_aux assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>prime (4 * ?k + 3); odd (multiplicity (4 * ?k + 3) ?n)\<rbrakk> \<Longrightarrow> \<not> is_sum2sq_nat ?n
is_sum2sq_nat n

goal (1 subgoal):
 1. \<And>k. prime (4 * k + 3) \<longrightarrow> even (multiplicity (4 * k + 3) n)
[PROOF STEP]
by blast


[STATEMENT]
lemma aux_lemma: assumes "[(a::nat) = b] (mod c)" "b < c"
  shows "\<exists> k. a = c*k + b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k. a = c * k + b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>k. a = c * k + b
[PROOF STEP]
have "a mod c = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a mod c = b
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
[a = b] (mod c)
b < c

goal (1 subgoal):
 1. a mod c = b
[PROOF STEP]
by (simp add: cong_def mod_if)
[PROOF STATE]
proof (state)
this:
a mod c = b

goal (1 subgoal):
 1. \<exists>k. a = c * k + b
[PROOF STEP]
hence "b \<le> a"
[PROOF STATE]
proof (prove)
using this:
a mod c = b

goal (1 subgoal):
 1. b \<le> a
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a mod c = b
[a = b] (mod c)
b < c

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

goal (1 subgoal):
 1. \<exists>k. a = c * k + b
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
b \<le> a

goal (1 subgoal):
 1. \<exists>k. a = c * k + b
[PROOF STEP]
using cong_le_nat assms(1)
[PROOF STATE]
proof (prove)
using this:
b \<le> a
?y \<le> ?x \<Longrightarrow> [?x = ?y] (mod ?n) = (\<exists>q. ?x = q * ?n + ?y)
[a = b] (mod c)

goal (1 subgoal):
 1. \<exists>k. a = c * k + b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>k. a = c * k + b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Legendre_1mod4: "prime (4*k+1::nat) \<Longrightarrow> (Legendre (-1) (4*k+1)) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime (4 * k + 1) \<Longrightarrow> Legendre (- 1) (int (4 * k + 1)) = 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prime (4 * k + 1) \<Longrightarrow> Legendre (- 1) (int (4 * k + 1)) = 1
[PROOF STEP]
let ?p = "4*k+1"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prime (4 * k + 1) \<Longrightarrow> Legendre (- 1) (int (4 * k + 1)) = 1
[PROOF STEP]
let ?L = "Legendre (-1) ?p"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prime (4 * k + 1) \<Longrightarrow> Legendre (- 1) (int (4 * k + 1)) = 1
[PROOF STEP]
assume p: "prime ?p"
[PROOF STATE]
proof (state)
this:
prime (4 * k + 1)

goal (1 subgoal):
 1. prime (4 * k + 1) \<Longrightarrow> Legendre (- 1) (int (4 * k + 1)) = 1
[PROOF STEP]
from p
[PROOF STATE]
proof (chain)
picking this:
prime (4 * k + 1)
[PROOF STEP]
have "k \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
prime (4 * k + 1)

goal (1 subgoal):
 1. k \<noteq> 0
[PROOF STEP]
by (intro notI) simp_all
[PROOF STATE]
proof (state)
this:
k \<noteq> 0

goal (1 subgoal):
 1. prime (4 * k + 1) \<Longrightarrow> Legendre (- 1) (int (4 * k + 1)) = 1
[PROOF STEP]
hence p2: "?p > 2"
[PROOF STATE]
proof (prove)
using this:
k \<noteq> 0

goal (1 subgoal):
 1. 2 < 4 * k + 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 < 4 * k + 1

goal (1 subgoal):
 1. prime (4 * k + 1) \<Longrightarrow> Legendre (- 1) (int (4 * k + 1)) = 1
[PROOF STEP]
with p
[PROOF STATE]
proof (chain)
picking this:
prime (4 * k + 1)
2 < 4 * k + 1
[PROOF STEP]
have "[?L = (-1)^((?p - 1) div 2)] (mod ?p)"
[PROOF STATE]
proof (prove)
using this:
prime (4 * k + 1)
2 < 4 * k + 1

goal (1 subgoal):
 1. [Legendre (- 1) (int (4 * k + 1)) = (- 1) ^ ((4 * k + 1 - 1) div 2)] (mod int (4 * k + 1))
[PROOF STEP]
by (rule euler_criterion)
[PROOF STATE]
proof (state)
this:
[Legendre (- 1) (int (4 * k + 1)) = (- 1) ^ ((4 * k + 1 - 1) div 2)] (mod int (4 * k + 1))

goal (1 subgoal):
 1. prime (4 * k + 1) \<Longrightarrow> Legendre (- 1) (int (4 * k + 1)) = 1
[PROOF STEP]
hence "[?L = (-1)^(2 * nat k)] (mod ?p)"
[PROOF STATE]
proof (prove)
using this:
[Legendre (- 1) (int (4 * k + 1)) = (- 1) ^ ((4 * k + 1 - 1) div 2)] (mod int (4 * k + 1))

goal (1 subgoal):
 1. [Legendre (- 1) (int (4 * k + 1)) = (- 1) ^ (2 * nat (int k))] (mod int (4 * k + 1))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
[Legendre (- 1) (int (4 * k + 1)) = (- 1) ^ (2 * nat (int k))] (mod int (4 * k + 1))

goal (1 subgoal):
 1. prime (4 * k + 1) \<Longrightarrow> Legendre (- 1) (int (4 * k + 1)) = 1
[PROOF STEP]
hence "[?L = 1] (mod ?p)"
[PROOF STATE]
proof (prove)
using this:
[Legendre (- 1) (int (4 * k + 1)) = (- 1) ^ (2 * nat (int k))] (mod int (4 * k + 1))

goal (1 subgoal):
 1. [Legendre (- 1) (int (4 * k + 1)) = 1] (mod int (4 * k + 1))
[PROOF STEP]
unfolding power_mult
[PROOF STATE]
proof (prove)
using this:
[Legendre (- 1) (int (4 * k + 1)) = (- 1)\<^sup>2 ^ nat (int k)] (mod int (4 * k + 1))

goal (1 subgoal):
 1. [Legendre (- 1) (int (4 * k + 1)) = 1] (mod int (4 * k + 1))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[Legendre (- 1) (int (4 * k + 1)) = 1] (mod int (4 * k + 1))

goal (1 subgoal):
 1. prime (4 * k + 1) \<Longrightarrow> Legendre (- 1) (int (4 * k + 1)) = 1
[PROOF STEP]
hence "?p dvd 1-?L"
[PROOF STATE]
proof (prove)
using this:
[Legendre (- 1) (int (4 * k + 1)) = 1] (mod int (4 * k + 1))

goal (1 subgoal):
 1. int (4 * k + 1) dvd 1 - Legendre (- 1) (int (4 * k + 1))
[PROOF STEP]
using cong_iff_dvd_diff dvd_minus_iff[of ?p "?L-1"]
[PROOF STATE]
proof (prove)
using this:
[Legendre (- 1) (int (4 * k + 1)) = 1] (mod int (4 * k + 1))
[?a = ?b] (mod ?m) = (?m dvd ?a - ?b)
(int (4 * k + 1) dvd - (Legendre (- 1) (int (4 * k + 1)) - 1)) = (int (4 * k + 1) dvd Legendre (- 1) (int (4 * k + 1)) - 1)

goal (1 subgoal):
 1. int (4 * k + 1) dvd 1 - Legendre (- 1) (int (4 * k + 1))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
int (4 * k + 1) dvd 1 - Legendre (- 1) (int (4 * k + 1))

goal (1 subgoal):
 1. prime (4 * k + 1) \<Longrightarrow> Legendre (- 1) (int (4 * k + 1)) = 1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
int (4 * k + 1) dvd 1 - Legendre (- 1) (int (4 * k + 1))

goal (1 subgoal):
 1. prime (4 * k + 1) \<Longrightarrow> Legendre (- 1) (int (4 * k + 1)) = 1
[PROOF STEP]
have "?L=1 \<or> ?L=0 \<or> ?L=-1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Legendre (- 1) (int (4 * k + 1)) = 1 \<or> Legendre (- 1) (int (4 * k + 1)) = 0 \<or> Legendre (- 1) (int (4 * k + 1)) = - 1
[PROOF STEP]
by (simp add: Legendre_def)
[PROOF STATE]
proof (state)
this:
Legendre (- 1) (int (4 * k + 1)) = 1 \<or> Legendre (- 1) (int (4 * k + 1)) = 0 \<or> Legendre (- 1) (int (4 * k + 1)) = - 1

goal (1 subgoal):
 1. prime (4 * k + 1) \<Longrightarrow> Legendre (- 1) (int (4 * k + 1)) = 1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
int (4 * k + 1) dvd 1 - Legendre (- 1) (int (4 * k + 1))
Legendre (- 1) (int (4 * k + 1)) = 1 \<or> Legendre (- 1) (int (4 * k + 1)) = 0 \<or> Legendre (- 1) (int (4 * k + 1)) = - 1
[PROOF STEP]
have "?L = 1 \<or> ?p dvd 1 \<or> ?p dvd (2::int)"
[PROOF STATE]
proof (prove)
using this:
int (4 * k + 1) dvd 1 - Legendre (- 1) (int (4 * k + 1))
Legendre (- 1) (int (4 * k + 1)) = 1 \<or> Legendre (- 1) (int (4 * k + 1)) = 0 \<or> Legendre (- 1) (int (4 * k + 1)) = - 1

goal (1 subgoal):
 1. Legendre (- 1) (int (4 * k + 1)) = 1 \<or> is_unit (4 * k + 1) \<or> int (4 * k + 1) dvd 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Legendre (- 1) (int (4 * k + 1)) = 1 \<or> is_unit (4 * k + 1) \<or> int (4 * k + 1) dvd 2

goal (1 subgoal):
 1. prime (4 * k + 1) \<Longrightarrow> Legendre (- 1) (int (4 * k + 1)) = 1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Legendre (- 1) (int (4 * k + 1)) = 1 \<or> is_unit (4 * k + 1) \<or> int (4 * k + 1) dvd 2

goal (1 subgoal):
 1. prime (4 * k + 1) \<Longrightarrow> Legendre (- 1) (int (4 * k + 1)) = 1
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
Legendre (- 1) (int (4 * k + 1)) = 1 \<or> is_unit (4 * k + 1) \<or> int (4 * k + 1) dvd 2

goal (1 subgoal):
 1. prime (4 * k + 1) \<Longrightarrow> Legendre (- 1) (int (4 * k + 1)) = 1
[PROOF STEP]
assume "?p dvd 1 \<or> ?p dvd (2::int)"
[PROOF STATE]
proof (state)
this:
is_unit (4 * k + 1) \<or> int (4 * k + 1) dvd 2

goal (1 subgoal):
 1. prime (4 * k + 1) \<Longrightarrow> Legendre (- 1) (int (4 * k + 1)) = 1
[PROOF STEP]
with p2
[PROOF STATE]
proof (chain)
picking this:
2 < 4 * k + 1
is_unit (4 * k + 1) \<or> int (4 * k + 1) dvd 2
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
2 < 4 * k + 1
is_unit (4 * k + 1) \<or> int (4 * k + 1) dvd 2

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

goal (1 subgoal):
 1. prime (4 * k + 1) \<Longrightarrow> Legendre (- 1) (int (4 * k + 1)) = 1
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
is_unit (4 * k + 1) \<or> int (4 * k + 1) dvd 2 \<Longrightarrow> False

goal (1 subgoal):
 1. prime (4 * k + 1) \<Longrightarrow> Legendre (- 1) (int (4 * k + 1)) = 1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Legendre (- 1) (int (4 * k + 1)) = 1 \<or> is_unit (4 * k + 1) \<or> int (4 * k + 1) dvd 2
is_unit (4 * k + 1) \<or> int (4 * k + 1) dvd 2 \<Longrightarrow> False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Legendre (- 1) (int (4 * k + 1)) = 1 \<or> is_unit (4 * k + 1) \<or> int (4 * k + 1) dvd 2
is_unit (4 * k + 1) \<or> int (4 * k + 1) dvd 2 \<Longrightarrow> False

goal (1 subgoal):
 1. Legendre (- 1) (int (4 * k + 1)) = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Legendre (- 1) (int (4 * k + 1)) = 1

goal:
No subgoals!
[PROOF STEP]
qed