[STATEMENT]
lemma zprime_is_sum4sq: "prime (nat p) \<Longrightarrow> is_sum4sq_int p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime (nat p) \<Longrightarrow> is_sum4sq_int p
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>prime (nat p); ?P\<rbrakk> \<Longrightarrow> is_sum4sq_int p
 2. \<lbrakk>prime (nat p); \<not> ?P\<rbrakk> \<Longrightarrow> is_sum4sq_int p
[PROOF STEP]
assume p2: "p=2"
[PROOF STATE]
proof (state)
this:
p = 2

goal (2 subgoals):
 1. \<lbrakk>prime (nat p); ?P\<rbrakk> \<Longrightarrow> is_sum4sq_int p
 2. \<lbrakk>prime (nat p); \<not> ?P\<rbrakk> \<Longrightarrow> is_sum4sq_int p
[PROOF STEP]
hence "p = sum4sq_int(1,1,0,0)"
[PROOF STATE]
proof (prove)
using this:
p = 2

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

goal (2 subgoals):
 1. \<lbrakk>prime (nat p); ?P\<rbrakk> \<Longrightarrow> is_sum4sq_int p
 2. \<lbrakk>prime (nat p); \<not> ?P\<rbrakk> \<Longrightarrow> is_sum4sq_int p
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
p = sum4sq_int (1, 1, 0, 0)

goal (1 subgoal):
 1. is_sum4sq_int p
[PROOF STEP]
by (auto simp add: is_sum4sq_int_def)
[PROOF STATE]
proof (state)
this:
is_sum4sq_int p

goal (1 subgoal):
 1. \<lbrakk>prime (nat p); p \<noteq> 2\<rbrakk> \<Longrightarrow> is_sum4sq_int p
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>prime (nat p); p \<noteq> 2\<rbrakk> \<Longrightarrow> is_sum4sq_int p
[PROOF STEP]
assume "\<not> p =2" and prp: "prime (nat p)"
[PROOF STATE]
proof (state)
this:
p \<noteq> 2
prime (nat p)

goal (1 subgoal):
 1. \<lbrakk>prime (nat p); p \<noteq> 2\<rbrakk> \<Longrightarrow> is_sum4sq_int p
[PROOF STEP]
hence "\<not> nat p = 2"
[PROOF STATE]
proof (prove)
using this:
p \<noteq> 2
prime (nat p)

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

goal (1 subgoal):
 1. \<lbrakk>prime (nat p); p \<noteq> 2\<rbrakk> \<Longrightarrow> is_sum4sq_int p
[PROOF STEP]
with prp
[PROOF STATE]
proof (chain)
picking this:
prime (nat p)
nat p \<noteq> 2
[PROOF STEP]
have "2 < nat p"
[PROOF STATE]
proof (prove)
using this:
prime (nat p)
nat p \<noteq> 2

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

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

goal (1 subgoal):
 1. \<lbrakk>prime (nat p); p \<noteq> 2\<rbrakk> \<Longrightarrow> is_sum4sq_int p
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
2 < nat p

goal (1 subgoal):
 1. \<lbrakk>prime (nat p); p \<noteq> 2\<rbrakk> \<Longrightarrow> is_sum4sq_int p
[PROOF STEP]
with prp
[PROOF STATE]
proof (chain)
picking this:
prime (nat p)
2 < nat p
[PROOF STEP]
have "odd (nat p)"
[PROOF STATE]
proof (prove)
using this:
prime (nat p)
2 < nat p

goal (1 subgoal):
 1. odd (nat p)
[PROOF STEP]
using prime_odd_nat[of "nat p"]
[PROOF STATE]
proof (prove)
using this:
prime (nat p)
2 < nat p
\<lbrakk>prime (nat p); 2 < nat p\<rbrakk> \<Longrightarrow> odd (nat p)

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

goal (1 subgoal):
 1. \<lbrakk>prime (nat p); p \<noteq> 2\<rbrakk> \<Longrightarrow> is_sum4sq_int p
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
2 < nat p
odd (nat p)
[PROOF STEP]
have "odd p"
[PROOF STATE]
proof (prove)
using this:
2 < nat p
odd (nat p)

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

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

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

goal (1 subgoal):
 1. \<lbrakk>prime (nat p); p \<noteq> 2\<rbrakk> \<Longrightarrow> is_sum4sq_int p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>t>0. t < p \<and> is_sum4sq_int (p * t)
[PROOF STEP]
obtain a b c d t where pt_sol: "0<t \<and> t<p \<and> p*t = sum4sq_int(a,b,c,d)"
[PROOF STATE]
proof (prove)
using this:
\<exists>t>0. t < p \<and> is_sum4sq_int (p * t)

goal (1 subgoal):
 1. (\<And>t a b c d. 0 < t \<and> t < p \<and> p * t = sum4sq_int (a, b, c, d) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (unfold is_sum4sq_int_def, blast)
[PROOF STATE]
proof (state)
this:
0 < t \<and> t < p \<and> p * t = sum4sq_int (a, b, c, d)

goal (1 subgoal):
 1. \<lbrakk>prime (nat p); p \<noteq> 2\<rbrakk> \<Longrightarrow> is_sum4sq_int p
[PROOF STEP]
hence Qt: "0<t \<and> t<p \<and> (\<exists> a1 a2 a3 a4. p*t = sum4sq_int(a1,a2,a3,a4))"
    (is "?Q t")
[PROOF STATE]
proof (prove)
using this:
0 < t \<and> t < p \<and> p * t = sum4sq_int (a, b, c, d)

goal (1 subgoal):
 1. 0 < t \<and> t < p \<and> (\<exists>a1 a2 a3 a4. p * t = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
0 < t \<and> t < p \<and> (\<exists>a1 a2 a3 a4. p * t = sum4sq_int (a1, a2, a3, a4))

goal (1 subgoal):
 1. \<lbrakk>prime (nat p); p \<noteq> 2\<rbrakk> \<Longrightarrow> is_sum4sq_int p
[PROOF STEP]
have "?Q 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < 1 \<and> 1 < p \<and> (\<exists>a1 a2 a3 a4. p * 1 = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (0 < 1 \<and> 1 < p \<and> (\<exists>a1 a2 a3 a4. p * 1 = sum4sq_int (a1, a2, a3, a4))) \<Longrightarrow> False
[PROOF STEP]
assume nQ1: "\<not> ?Q 1"
[PROOF STATE]
proof (state)
this:
\<not> (0 < 1 \<and> 1 < p \<and> (\<exists>a1 a2 a3 a4. p * 1 = sum4sq_int (a1, a2, a3, a4)))

goal (1 subgoal):
 1. \<not> (0 < 1 \<and> 1 < p \<and> (\<exists>a1 a2 a3 a4. p * 1 = sum4sq_int (a1, a2, a3, a4))) \<Longrightarrow> False
[PROOF STEP]
have "\<not> ?Q t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (0 < t \<and> t < p \<and> (\<exists>a1 a2 a3 a4. p * t = sum4sq_int (a1, a2, a3, a4)))
[PROOF STEP]
proof (induct t rule: infinite_descent0_measure[where V="\<lambda>x. (nat x)- 1"], clarify)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x a1 a2 a3 a4. \<lbrakk>nat x - 1 = 0; 0 < x; x < p; p * x = sum4sq_int (a1, a2, a3, a4)\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>0 < nat x - 1; \<not> \<not> (0 < x \<and> x < p \<and> (\<exists>a1 a2 a3 a4. p * x = sum4sq_int (a1, a2, a3, a4)))\<rbrakk> \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> \<not> \<not> (0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4)))
[PROOF STEP]
fix x a b c d
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x a1 a2 a3 a4. \<lbrakk>nat x - 1 = 0; 0 < x; x < p; p * x = sum4sq_int (a1, a2, a3, a4)\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>0 < nat x - 1; \<not> \<not> (0 < x \<and> x < p \<and> (\<exists>a1 a2 a3 a4. p * x = sum4sq_int (a1, a2, a3, a4)))\<rbrakk> \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> \<not> \<not> (0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4)))
[PROOF STEP]
assume "nat x - 1 = 0" and "x > 0" and s: "p*x=sum4sq_int(a,b,c,d)" and "x < p"
[PROOF STATE]
proof (state)
this:
nat x - 1 = 0
0 < x
p * x = sum4sq_int (a, b, c, d)
x < p

goal (2 subgoals):
 1. \<And>x a1 a2 a3 a4. \<lbrakk>nat x - 1 = 0; 0 < x; x < p; p * x = sum4sq_int (a1, a2, a3, a4)\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>0 < nat x - 1; \<not> \<not> (0 < x \<and> x < p \<and> (\<exists>a1 a2 a3 a4. p * x = sum4sq_int (a1, a2, a3, a4)))\<rbrakk> \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> \<not> \<not> (0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
nat x - 1 = 0
0 < x
p * x = sum4sq_int (a, b, c, d)
x < p

goal (2 subgoals):
 1. \<And>x a1 a2 a3 a4. \<lbrakk>nat x - 1 = 0; 0 < x; x < p; p * x = sum4sq_int (a1, a2, a3, a4)\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>0 < nat x - 1; \<not> \<not> (0 < x \<and> x < p \<and> (\<exists>a1 a2 a3 a4. p * x = sum4sq_int (a1, a2, a3, a4)))\<rbrakk> \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> \<not> \<not> (0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4)))
[PROOF STEP]
hence "x = 1"
[PROOF STATE]
proof (prove)
using this:
nat x - 1 = 0
0 < x
p * x = sum4sq_int (a, b, c, d)
x < p

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

goal (2 subgoals):
 1. \<And>x a1 a2 a3 a4. \<lbrakk>nat x - 1 = 0; 0 < x; x < p; p * x = sum4sq_int (a1, a2, a3, a4)\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>0 < nat x - 1; \<not> \<not> (0 < x \<and> x < p \<and> (\<exists>a1 a2 a3 a4. p * x = sum4sq_int (a1, a2, a3, a4)))\<rbrakk> \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> \<not> \<not> (0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4)))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
nat x - 1 = 0
0 < x
p * x = sum4sq_int (a, b, c, d)
x < p
x = 1
[PROOF STEP]
have "?Q 1"
[PROOF STATE]
proof (prove)
using this:
nat x - 1 = 0
0 < x
p * x = sum4sq_int (a, b, c, d)
x < p
x = 1

goal (1 subgoal):
 1. 0 < 1 \<and> 1 < p \<and> (\<exists>a1 a2 a3 a4. p * 1 = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < 1 \<and> 1 < p \<and> (\<exists>a1 a2 a3 a4. p * 1 = sum4sq_int (a1, a2, a3, a4))

goal (2 subgoals):
 1. \<And>x a1 a2 a3 a4. \<lbrakk>nat x - 1 = 0; 0 < x; x < p; p * x = sum4sq_int (a1, a2, a3, a4)\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>0 < nat x - 1; \<not> \<not> (0 < x \<and> x < p \<and> (\<exists>a1 a2 a3 a4. p * x = sum4sq_int (a1, a2, a3, a4)))\<rbrakk> \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> \<not> \<not> (0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4)))
[PROOF STEP]
with nQ1
[PROOF STATE]
proof (chain)
picking this:
\<not> (0 < 1 \<and> 1 < p \<and> (\<exists>a1 a2 a3 a4. p * 1 = sum4sq_int (a1, a2, a3, a4)))
0 < 1 \<and> 1 < p \<and> (\<exists>a1 a2 a3 a4. p * 1 = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<not> (0 < 1 \<and> 1 < p \<and> (\<exists>a1 a2 a3 a4. p * 1 = sum4sq_int (a1, a2, a3, a4)))
0 < 1 \<and> 1 < p \<and> (\<exists>a1 a2 a3 a4. p * 1 = sum4sq_int (a1, a2, a3, a4))

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

goal (1 subgoal):
 1. \<And>x. \<lbrakk>0 < nat x - 1; \<not> \<not> (0 < x \<and> x < p \<and> (\<exists>a1 a2 a3 a4. p * x = sum4sq_int (a1, a2, a3, a4)))\<rbrakk> \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> \<not> \<not> (0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>0 < nat x - 1; \<not> \<not> (0 < x \<and> x < p \<and> (\<exists>a1 a2 a3 a4. p * x = sum4sq_int (a1, a2, a3, a4)))\<rbrakk> \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> \<not> \<not> (0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4)))
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>0 < nat x - 1; \<not> \<not> (0 < x \<and> x < p \<and> (\<exists>a1 a2 a3 a4. p * x = sum4sq_int (a1, a2, a3, a4)))\<rbrakk> \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> \<not> \<not> (0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4)))
[PROOF STEP]
assume "0 < nat x - 1" and "\<not> \<not> ?Q x"
[PROOF STATE]
proof (state)
this:
0 < nat x - 1
\<not> \<not> (0 < x \<and> x < p \<and> (\<exists>a1 a2 a3 a4. p * x = sum4sq_int (a1, a2, a3, a4)))

goal (1 subgoal):
 1. \<And>x. \<lbrakk>0 < nat x - 1; \<not> \<not> (0 < x \<and> x < p \<and> (\<exists>a1 a2 a3 a4. p * x = sum4sq_int (a1, a2, a3, a4)))\<rbrakk> \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> \<not> \<not> (0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < nat x - 1
\<not> \<not> (0 < x \<and> x < p \<and> (\<exists>a1 a2 a3 a4. p * x = sum4sq_int (a1, a2, a3, a4)))
[PROOF STEP]
obtain a1 a2 a3 a4 where ass: "1<x \<and> x<p \<and> p*x = sum4sq_int(a1,a2,a3,a4)"
[PROOF STATE]
proof (prove)
using this:
0 < nat x - 1
\<not> \<not> (0 < x \<and> x < p \<and> (\<exists>a1 a2 a3 a4. p * x = sum4sq_int (a1, a2, a3, a4)))

goal (1 subgoal):
 1. (\<And>a1 a2 a3 a4. 1 < x \<and> x < p \<and> p * x = sum4sq_int (a1, a2, a3, a4) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 < x \<and> x < p \<and> p * x = sum4sq_int (a1, a2, a3, a4)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>0 < nat x - 1; \<not> \<not> (0 < x \<and> x < p \<and> (\<exists>a1 a2 a3 a4. p * x = sum4sq_int (a1, a2, a3, a4)))\<rbrakk> \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> \<not> \<not> (0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4)))
[PROOF STEP]
have "\<exists> y. nat y - 1 < nat x - 1 \<and> ?Q y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
 2. \<not> ?P \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
assume evx: "even x"
[PROOF STATE]
proof (state)
this:
even x

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
 2. \<not> ?P \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
hence "even (x*p)"
[PROOF STATE]
proof (prove)
using this:
even x

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
 2. \<not> ?P \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
with ass
[PROOF STATE]
proof (chain)
picking this:
1 < x \<and> x < p \<and> p * x = sum4sq_int (a1, a2, a3, a4)
even (x * p)
[PROOF STEP]
have ev1234: "even (a1^2+a2^2 + a3^2+a4^2)"
[PROOF STATE]
proof (prove)
using this:
1 < x \<and> x < p \<and> p * x = sum4sq_int (a1, a2, a3, a4)
even (x * p)

goal (1 subgoal):
 1. even (a1\<^sup>2 + a2\<^sup>2 + a3\<^sup>2 + a4\<^sup>2)
[PROOF STEP]
by (auto simp add: sum4sq_int_def ac_simps)
[PROOF STATE]
proof (state)
this:
even (a1\<^sup>2 + a2\<^sup>2 + a3\<^sup>2 + a4\<^sup>2)

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
 2. \<not> ?P \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
have "\<exists> b1 b2 b3 b4. p*x=sum4sq_int(b1,b2,b3,b4) \<and> even (b1+b2) \<and> even (b3+b4)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
 2. \<not> ?P \<Longrightarrow> \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
[PROOF STEP]
assume ev12: "even (a1^2+a2^2)"
[PROOF STATE]
proof (state)
this:
even (a1\<^sup>2 + a2\<^sup>2)

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
 2. \<not> ?P \<Longrightarrow> \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
[PROOF STEP]
with ev1234 ass
[PROOF STATE]
proof (chain)
picking this:
even (a1\<^sup>2 + a2\<^sup>2 + a3\<^sup>2 + a4\<^sup>2)
1 < x \<and> x < p \<and> p * x = sum4sq_int (a1, a2, a3, a4)
even (a1\<^sup>2 + a2\<^sup>2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
even (a1\<^sup>2 + a2\<^sup>2 + a3\<^sup>2 + a4\<^sup>2)
1 < x \<and> x < p \<and> p * x = sum4sq_int (a1, a2, a3, a4)
even (a1\<^sup>2 + a2\<^sup>2)

goal (1 subgoal):
 1. \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)

goal (1 subgoal):
 1. odd (a1\<^sup>2 + a2\<^sup>2) \<Longrightarrow> \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. odd (a1\<^sup>2 + a2\<^sup>2) \<Longrightarrow> \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
[PROOF STEP]
assume "\<not> even (a1^2+a2^2)"
[PROOF STATE]
proof (state)
this:
odd (a1\<^sup>2 + a2\<^sup>2)

goal (1 subgoal):
 1. odd (a1\<^sup>2 + a2\<^sup>2) \<Longrightarrow> \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
[PROOF STEP]
hence odd12: "odd (a1^2+a2^2)"
[PROOF STATE]
proof (prove)
using this:
odd (a1\<^sup>2 + a2\<^sup>2)

goal (1 subgoal):
 1. odd (a1\<^sup>2 + a2\<^sup>2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
odd (a1\<^sup>2 + a2\<^sup>2)

goal (1 subgoal):
 1. odd (a1\<^sup>2 + a2\<^sup>2) \<Longrightarrow> \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
[PROOF STEP]
with ev1234
[PROOF STATE]
proof (chain)
picking this:
even (a1\<^sup>2 + a2\<^sup>2 + a3\<^sup>2 + a4\<^sup>2)
odd (a1\<^sup>2 + a2\<^sup>2)
[PROOF STEP]
have odd34: "odd (a3^2+a4^2)"
[PROOF STATE]
proof (prove)
using this:
even (a1\<^sup>2 + a2\<^sup>2 + a3\<^sup>2 + a4\<^sup>2)
odd (a1\<^sup>2 + a2\<^sup>2)

goal (1 subgoal):
 1. odd (a3\<^sup>2 + a4\<^sup>2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
odd (a3\<^sup>2 + a4\<^sup>2)

goal (1 subgoal):
 1. odd (a1\<^sup>2 + a2\<^sup>2) \<Longrightarrow> \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
 2. \<not> ?P \<Longrightarrow> \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
[PROOF STEP]
assume ev1: "even (a1^2)"
[PROOF STATE]
proof (state)
this:
even (a1\<^sup>2)

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
 2. \<not> ?P \<Longrightarrow> \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
[PROOF STEP]
with odd12
[PROOF STATE]
proof (chain)
picking this:
odd (a1\<^sup>2 + a2\<^sup>2)
even (a1\<^sup>2)
[PROOF STEP]
have odd2: "odd (a2^2)"
[PROOF STATE]
proof (prove)
using this:
odd (a1\<^sup>2 + a2\<^sup>2)
even (a1\<^sup>2)

goal (1 subgoal):
 1. odd (a2\<^sup>2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
odd (a2\<^sup>2)

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
 2. \<not> ?P \<Longrightarrow> \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
 2. \<not> ?P \<Longrightarrow> \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
[PROOF STEP]
assume "even (a3^2)"
[PROOF STATE]
proof (state)
this:
even (a3\<^sup>2)

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
 2. \<not> ?P \<Longrightarrow> \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
even (a3\<^sup>2)

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
 2. \<not> ?P \<Longrightarrow> \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
[PROOF STEP]
from ass
[PROOF STATE]
proof (chain)
picking this:
1 < x \<and> x < p \<and> p * x = sum4sq_int (a1, a2, a3, a4)
[PROOF STEP]
have "p*x = sum4sq_int(a1,a3,a2,a4)"
[PROOF STATE]
proof (prove)
using this:
1 < x \<and> x < p \<and> p * x = sum4sq_int (a1, a2, a3, a4)

goal (1 subgoal):
 1. p * x = sum4sq_int (a1, a3, a2, a4)
[PROOF STEP]
by (auto simp add: sum4sq_int_def)
[PROOF STATE]
proof (state)
this:
p * x = sum4sq_int (a1, a3, a2, a4)

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
 2. \<not> ?P \<Longrightarrow> \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
even (a3\<^sup>2)
p * x = sum4sq_int (a1, a3, a2, a4)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
even (a3\<^sup>2)
p * x = sum4sq_int (a1, a3, a2, a4)

goal (1 subgoal):
 1. \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
[PROOF STEP]
using odd2 odd34 ev1
[PROOF STATE]
proof (prove)
using this:
even (a3\<^sup>2)
p * x = sum4sq_int (a1, a3, a2, a4)
odd (a2\<^sup>2)
odd (a3\<^sup>2 + a4\<^sup>2)
even (a1\<^sup>2)

goal (1 subgoal):
 1. \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)

goal (1 subgoal):
 1. odd (a3\<^sup>2) \<Longrightarrow> \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. odd (a3\<^sup>2) \<Longrightarrow> \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
[PROOF STEP]
assume "\<not> even (a3^2)"
[PROOF STATE]
proof (state)
this:
odd (a3\<^sup>2)

goal (1 subgoal):
 1. odd (a3\<^sup>2) \<Longrightarrow> \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
odd (a3\<^sup>2)

goal (1 subgoal):
 1. odd (a3\<^sup>2) \<Longrightarrow> \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
[PROOF STEP]
from ass
[PROOF STATE]
proof (chain)
picking this:
1 < x \<and> x < p \<and> p * x = sum4sq_int (a1, a2, a3, a4)
[PROOF STEP]
have "p*x = sum4sq_int(a1,a4,a2,a3)"
[PROOF STATE]
proof (prove)
using this:
1 < x \<and> x < p \<and> p * x = sum4sq_int (a1, a2, a3, a4)

goal (1 subgoal):
 1. p * x = sum4sq_int (a1, a4, a2, a3)
[PROOF STEP]
by (auto simp add: sum4sq_int_def)
[PROOF STATE]
proof (state)
this:
p * x = sum4sq_int (a1, a4, a2, a3)

goal (1 subgoal):
 1. odd (a3\<^sup>2) \<Longrightarrow> \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
odd (a3\<^sup>2)
p * x = sum4sq_int (a1, a4, a2, a3)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
odd (a3\<^sup>2)
p * x = sum4sq_int (a1, a4, a2, a3)

goal (1 subgoal):
 1. \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
[PROOF STEP]
using odd34 odd2 ev1
[PROOF STATE]
proof (prove)
using this:
odd (a3\<^sup>2)
p * x = sum4sq_int (a1, a4, a2, a3)
odd (a3\<^sup>2 + a4\<^sup>2)
odd (a2\<^sup>2)
even (a1\<^sup>2)

goal (1 subgoal):
 1. \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)

goal (1 subgoal):
 1. odd (a1\<^sup>2) \<Longrightarrow> \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. odd (a1\<^sup>2) \<Longrightarrow> \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
[PROOF STEP]
assume odd1: "\<not> even (a1^2)"
[PROOF STATE]
proof (state)
this:
odd (a1\<^sup>2)

goal (1 subgoal):
 1. odd (a1\<^sup>2) \<Longrightarrow> \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
[PROOF STEP]
with odd12
[PROOF STATE]
proof (chain)
picking this:
odd (a1\<^sup>2 + a2\<^sup>2)
odd (a1\<^sup>2)
[PROOF STEP]
have ev2: "even (a2^2)"
[PROOF STATE]
proof (prove)
using this:
odd (a1\<^sup>2 + a2\<^sup>2)
odd (a1\<^sup>2)

goal (1 subgoal):
 1. even (a2\<^sup>2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
even (a2\<^sup>2)

goal (1 subgoal):
 1. odd (a1\<^sup>2) \<Longrightarrow> \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
 2. \<not> ?P \<Longrightarrow> \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
[PROOF STEP]
assume "even (a3^2)"
[PROOF STATE]
proof (state)
this:
even (a3\<^sup>2)

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
 2. \<not> ?P \<Longrightarrow> \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
even (a3\<^sup>2)

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
 2. \<not> ?P \<Longrightarrow> \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
[PROOF STEP]
from ass
[PROOF STATE]
proof (chain)
picking this:
1 < x \<and> x < p \<and> p * x = sum4sq_int (a1, a2, a3, a4)
[PROOF STEP]
have "sum4sq_int(a1,a4,a2,a3)=p*x"
[PROOF STATE]
proof (prove)
using this:
1 < x \<and> x < p \<and> p * x = sum4sq_int (a1, a2, a3, a4)

goal (1 subgoal):
 1. sum4sq_int (a1, a4, a2, a3) = p * x
[PROOF STEP]
by (auto simp add: sum4sq_int_def)
[PROOF STATE]
proof (state)
this:
sum4sq_int (a1, a4, a2, a3) = p * x

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
 2. \<not> ?P \<Longrightarrow> \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
even (a3\<^sup>2)
sum4sq_int (a1, a4, a2, a3) = p * x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
even (a3\<^sup>2)
sum4sq_int (a1, a4, a2, a3) = p * x

goal (1 subgoal):
 1. \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
[PROOF STEP]
using odd34 odd1 ev2
[PROOF STATE]
proof (prove)
using this:
even (a3\<^sup>2)
sum4sq_int (a1, a4, a2, a3) = p * x
odd (a3\<^sup>2 + a4\<^sup>2)
odd (a1\<^sup>2)
even (a2\<^sup>2)

goal (1 subgoal):
 1. \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)

goal (1 subgoal):
 1. odd (a3\<^sup>2) \<Longrightarrow> \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. odd (a3\<^sup>2) \<Longrightarrow> \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
[PROOF STEP]
assume "\<not> even (a3^2)"
[PROOF STATE]
proof (state)
this:
odd (a3\<^sup>2)

goal (1 subgoal):
 1. odd (a3\<^sup>2) \<Longrightarrow> \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
odd (a3\<^sup>2)

goal (1 subgoal):
 1. odd (a3\<^sup>2) \<Longrightarrow> \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
[PROOF STEP]
from ass
[PROOF STATE]
proof (chain)
picking this:
1 < x \<and> x < p \<and> p * x = sum4sq_int (a1, a2, a3, a4)
[PROOF STEP]
have "sum4sq_int(a1,a3,a2,a4)=p*x"
[PROOF STATE]
proof (prove)
using this:
1 < x \<and> x < p \<and> p * x = sum4sq_int (a1, a2, a3, a4)

goal (1 subgoal):
 1. sum4sq_int (a1, a3, a2, a4) = p * x
[PROOF STEP]
by (auto simp add: sum4sq_int_def)
[PROOF STATE]
proof (state)
this:
sum4sq_int (a1, a3, a2, a4) = p * x

goal (1 subgoal):
 1. odd (a3\<^sup>2) \<Longrightarrow> \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
odd (a3\<^sup>2)
sum4sq_int (a1, a3, a2, a4) = p * x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
odd (a3\<^sup>2)
sum4sq_int (a1, a3, a2, a4) = p * x

goal (1 subgoal):
 1. \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
[PROOF STEP]
using odd34 odd1 ev2
[PROOF STATE]
proof (prove)
using this:
odd (a3\<^sup>2)
sum4sq_int (a1, a3, a2, a4) = p * x
odd (a3\<^sup>2 + a4\<^sup>2)
odd (a1\<^sup>2)
even (a2\<^sup>2)

goal (1 subgoal):
 1. \<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
 2. \<not> ?P \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
[PROOF STEP]
obtain b1 b2 b3 b4
          where b: "p*x = sum4sq_int(b1,b2,b3,b4) \<and> even (b1+b2) \<and> even (b3+b4)"
[PROOF STATE]
proof (prove)
using this:
\<exists>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)

goal (1 subgoal):
 1. (\<And>b1 b2 b3 b4. p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
 2. \<not> ?P \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
[PROOF STEP]
obtain c1 c3 where c13: "b1+b2 = 2*c1 \<and> b3+b4 = 2*c3"
[PROOF STATE]
proof (prove)
using this:
p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)

goal (1 subgoal):
 1. (\<And>c1 c3. b1 + b2 = 2 * c1 \<and> b3 + b4 = 2 * c3 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using evenE[of "b1+b2"] evenE[of "b3+b4"]
[PROOF STATE]
proof (prove)
using this:
p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
\<lbrakk>even (b1 + b2); \<And>b. b1 + b2 = 2 * b \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
\<lbrakk>even (b3 + b4); \<And>b. b3 + b4 = 2 * b \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>c1 c3. b1 + b2 = 2 * c1 \<and> b3 + b4 = 2 * c3 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
b1 + b2 = 2 * c1 \<and> b3 + b4 = 2 * c3

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
 2. \<not> ?P \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
from b
[PROOF STATE]
proof (chain)
picking this:
p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
[PROOF STEP]
have "even (b1-b2) \<and> even (b3-b4)"
[PROOF STATE]
proof (prove)
using this:
p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)

goal (1 subgoal):
 1. even (b1 - b2) \<and> even (b3 - b4)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
even (b1 - b2) \<and> even (b3 - b4)

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
 2. \<not> ?P \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
even (b1 - b2) \<and> even (b3 - b4)
[PROOF STEP]
obtain c2 c4 where c24: "b1-b2 = 2*c2 \<and> b3-b4 = 2*c4"
[PROOF STATE]
proof (prove)
using this:
even (b1 - b2) \<and> even (b3 - b4)

goal (1 subgoal):
 1. (\<And>c2 c4. b1 - b2 = 2 * c2 \<and> b3 - b4 = 2 * c4 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using evenE[of "b1-b2"] evenE[of "b3-b4"]
[PROOF STATE]
proof (prove)
using this:
even (b1 - b2) \<and> even (b3 - b4)
\<lbrakk>even (b1 - b2); \<And>b. b1 - b2 = 2 * b \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
\<lbrakk>even (b3 - b4); \<And>b. b3 - b4 = 2 * b \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>c2 c4. b1 - b2 = 2 * c2 \<and> b3 - b4 = 2 * c4 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
b1 - b2 = 2 * c2 \<and> b3 - b4 = 2 * c4

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
 2. \<not> ?P \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
from evx
[PROOF STATE]
proof (chain)
picking this:
even x
[PROOF STEP]
obtain y where y: "x = 2*y"
[PROOF STATE]
proof (prove)
using this:
even x

goal (1 subgoal):
 1. (\<And>y. x = 2 * y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using evenE
[PROOF STATE]
proof (prove)
using this:
even x
\<lbrakk>even ?a; \<And>b. ?a = (2::?'a) * b \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
 2. \<not> ?P \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
hence "4*(p*y) = 2*(p*x)"
[PROOF STATE]
proof (prove)
using this:
x = 2 * y

goal (1 subgoal):
 1. 4 * (p * y) = 2 * (p * x)
[PROOF STEP]
by (simp add: ac_simps)
[PROOF STATE]
proof (state)
this:
4 * (p * y) = 2 * (p * x)

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
 2. \<not> ?P \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
4 * (p * y) = 2 * (p * x)

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
 2. \<not> ?P \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
from b
[PROOF STATE]
proof (chain)
picking this:
p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)
[PROOF STEP]
have "\<dots> = 2*b1^2 + 2*b2^2 + 2*b3^2 + 2*b4^2"
[PROOF STATE]
proof (prove)
using this:
p * x = sum4sq_int (b1, b2, b3, b4) \<and> even (b1 + b2) \<and> even (b3 + b4)

goal (1 subgoal):
 1. 2 * (p * x) = 2 * b1\<^sup>2 + 2 * b2\<^sup>2 + 2 * b3\<^sup>2 + 2 * b4\<^sup>2
[PROOF STEP]
by (auto simp: sum4sq_int_def)
[PROOF STATE]
proof (state)
this:
2 * (p * x) = 2 * b1\<^sup>2 + 2 * b2\<^sup>2 + 2 * b3\<^sup>2 + 2 * b4\<^sup>2

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
 2. \<not> ?P \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
2 * (p * x) = 2 * b1\<^sup>2 + 2 * b2\<^sup>2 + 2 * b3\<^sup>2 + 2 * b4\<^sup>2

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
 2. \<not> ?P \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
have "\<dots> = (b1 + b2)^2 + (b1 - b2)^2 + (b3 + b4)^2 + (b3 - b4)^2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * b1\<^sup>2 + 2 * b2\<^sup>2 + 2 * b3\<^sup>2 + 2 * b4\<^sup>2 = (b1 + b2)\<^sup>2 + (b1 - b2)\<^sup>2 + (b3 + b4)\<^sup>2 + (b3 - b4)\<^sup>2
[PROOF STEP]
by (auto simp add: power2_eq_square algebra_simps)
[PROOF STATE]
proof (state)
this:
2 * b1\<^sup>2 + 2 * b2\<^sup>2 + 2 * b3\<^sup>2 + 2 * b4\<^sup>2 = (b1 + b2)\<^sup>2 + (b1 - b2)\<^sup>2 + (b3 + b4)\<^sup>2 + (b3 - b4)\<^sup>2

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
 2. \<not> ?P \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
2 * b1\<^sup>2 + 2 * b2\<^sup>2 + 2 * b3\<^sup>2 + 2 * b4\<^sup>2 = (b1 + b2)\<^sup>2 + (b1 - b2)\<^sup>2 + (b3 + b4)\<^sup>2 + (b3 - b4)\<^sup>2

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
 2. \<not> ?P \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
with c13 c24
[PROOF STATE]
proof (chain)
picking this:
b1 + b2 = 2 * c1 \<and> b3 + b4 = 2 * c3
b1 - b2 = 2 * c2 \<and> b3 - b4 = 2 * c4
2 * b1\<^sup>2 + 2 * b2\<^sup>2 + 2 * b3\<^sup>2 + 2 * b4\<^sup>2 = (b1 + b2)\<^sup>2 + (b1 - b2)\<^sup>2 + (b3 + b4)\<^sup>2 + (b3 - b4)\<^sup>2
[PROOF STEP]
have "\<dots> = 4*(c1^2 + c2^2 + c3^2 + c4^2)"
[PROOF STATE]
proof (prove)
using this:
b1 + b2 = 2 * c1 \<and> b3 + b4 = 2 * c3
b1 - b2 = 2 * c2 \<and> b3 - b4 = 2 * c4
2 * b1\<^sup>2 + 2 * b2\<^sup>2 + 2 * b3\<^sup>2 + 2 * b4\<^sup>2 = (b1 + b2)\<^sup>2 + (b1 - b2)\<^sup>2 + (b3 + b4)\<^sup>2 + (b3 - b4)\<^sup>2

goal (1 subgoal):
 1. (b1 + b2)\<^sup>2 + (b1 - b2)\<^sup>2 + (b3 + b4)\<^sup>2 + (b3 - b4)\<^sup>2 = 4 * (c1\<^sup>2 + c2\<^sup>2 + c3\<^sup>2 + c4\<^sup>2)
[PROOF STEP]
by (auto simp add: power_mult_distrib)
[PROOF STATE]
proof (state)
this:
(b1 + b2)\<^sup>2 + (b1 - b2)\<^sup>2 + (b3 + b4)\<^sup>2 + (b3 - b4)\<^sup>2 = 4 * (c1\<^sup>2 + c2\<^sup>2 + c3\<^sup>2 + c4\<^sup>2)

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
 2. \<not> ?P \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
4 * (p * y) = 4 * (c1\<^sup>2 + c2\<^sup>2 + c3\<^sup>2 + c4\<^sup>2)
[PROOF STEP]
have "p * y = sum4sq_int(c1,c2,c3,c4)"
[PROOF STATE]
proof (prove)
using this:
4 * (p * y) = 4 * (c1\<^sup>2 + c2\<^sup>2 + c3\<^sup>2 + c4\<^sup>2)

goal (1 subgoal):
 1. p * y = sum4sq_int (c1, c2, c3, c4)
[PROOF STEP]
by (auto simp add: sum4sq_int_def)
[PROOF STATE]
proof (state)
this:
p * y = sum4sq_int (c1, c2, c3, c4)

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
 2. \<not> ?P \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
p * y = sum4sq_int (c1, c2, c3, c4)

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
 2. \<not> ?P \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
from y ass
[PROOF STATE]
proof (chain)
picking this:
x = 2 * y
1 < x \<and> x < p \<and> p * x = sum4sq_int (a1, a2, a3, a4)
[PROOF STEP]
have "0 < y \<and> y < p \<and> (nat y) - 1 < (nat x) - 1"
[PROOF STATE]
proof (prove)
using this:
x = 2 * y
1 < x \<and> x < p \<and> p * x = sum4sq_int (a1, a2, a3, a4)

goal (1 subgoal):
 1. 0 < y \<and> y < p \<and> nat y - 1 < nat x - 1
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
0 < y \<and> y < p \<and> nat y - 1 < nat x - 1

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
 2. \<not> ?P \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
p * y = sum4sq_int (c1, c2, c3, c4)
0 < y \<and> y < p \<and> nat y - 1 < nat x - 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p * y = sum4sq_int (c1, c2, c3, c4)
0 < y \<and> y < p \<and> nat y - 1 < nat x - 1

goal (1 subgoal):
 1. \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))

goal (1 subgoal):
 1. odd x \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. odd x \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
assume xodd: "\<not> even x"
[PROOF STATE]
proof (state)
this:
odd x

goal (1 subgoal):
 1. odd x \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
with ass
[PROOF STATE]
proof (chain)
picking this:
1 < x \<and> x < p \<and> p * x = sum4sq_int (a1, a2, a3, a4)
odd x
[PROOF STEP]
have "\<exists> c1 c2 c3 c4. 2*\<bar>a1-c1*x\<bar>\<le>x \<and> 2*\<bar>a2-c2*x\<bar>\<le>x \<and> 2*\<bar>a3-c3*x\<bar>\<le>x \<and> 2*\<bar>a4-c4*x\<bar>\<le>x"
[PROOF STATE]
proof (prove)
using this:
1 < x \<and> x < p \<and> p * x = sum4sq_int (a1, a2, a3, a4)
odd x

goal (1 subgoal):
 1. \<exists>c1 c2 c3 c4. 2 * \<bar>a1 - c1 * x\<bar> \<le> x \<and> 2 * \<bar>a2 - c2 * x\<bar> \<le> x \<and> 2 * \<bar>a3 - c3 * x\<bar> \<le> x \<and> 2 * \<bar>a4 - c4 * x\<bar> \<le> x
[PROOF STEP]
by (simp add: best_division_abs)
[PROOF STATE]
proof (state)
this:
\<exists>c1 c2 c3 c4. 2 * \<bar>a1 - c1 * x\<bar> \<le> x \<and> 2 * \<bar>a2 - c2 * x\<bar> \<le> x \<and> 2 * \<bar>a3 - c3 * x\<bar> \<le> x \<and> 2 * \<bar>a4 - c4 * x\<bar> \<le> x

goal (1 subgoal):
 1. odd x \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>c1 c2 c3 c4. 2 * \<bar>a1 - c1 * x\<bar> \<le> x \<and> 2 * \<bar>a2 - c2 * x\<bar> \<le> x \<and> 2 * \<bar>a3 - c3 * x\<bar> \<le> x \<and> 2 * \<bar>a4 - c4 * x\<bar> \<le> x
[PROOF STEP]
obtain b1 c1 b2 c2 b3 c3 b4 c4 where
          bc_def: "b1 = a1-c1*x \<and> b2 = a2-c2*x \<and> b3 = a3-c3*x \<and> b4 = a4-c4*x"
          and "2*\<bar>b1\<bar>\<le>x \<and> 2*\<bar>b2\<bar>\<le>x \<and> 2*\<bar>b3\<bar>\<le>x \<and> 2*\<bar>b4\<bar>\<le>x"
[PROOF STATE]
proof (prove)
using this:
\<exists>c1 c2 c3 c4. 2 * \<bar>a1 - c1 * x\<bar> \<le> x \<and> 2 * \<bar>a2 - c2 * x\<bar> \<le> x \<and> 2 * \<bar>a3 - c3 * x\<bar> \<le> x \<and> 2 * \<bar>a4 - c4 * x\<bar> \<le> x

goal (1 subgoal):
 1. (\<And>b1 c1 b2 c2 b3 c3 b4 c4. \<lbrakk>b1 = a1 - c1 * x \<and> b2 = a2 - c2 * x \<and> b3 = a3 - c3 * x \<and> b4 = a4 - c4 * x; 2 * \<bar>b1\<bar> \<le> x \<and> 2 * \<bar>b2\<bar> \<le> x \<and> 2 * \<bar>b3\<bar> \<le> x \<and> 2 * \<bar>b4\<bar> \<le> x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
b1 = a1 - c1 * x \<and> b2 = a2 - c2 * x \<and> b3 = a3 - c3 * x \<and> b4 = a4 - c4 * x
2 * \<bar>b1\<bar> \<le> x \<and> 2 * \<bar>b2\<bar> \<le> x \<and> 2 * \<bar>b3\<bar> \<le> x \<and> 2 * \<bar>b4\<bar> \<le> x

goal (1 subgoal):
 1. odd x \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
b1 = a1 - c1 * x \<and> b2 = a2 - c2 * x \<and> b3 = a3 - c3 * x \<and> b4 = a4 - c4 * x
2 * \<bar>b1\<bar> \<le> x \<and> 2 * \<bar>b2\<bar> \<le> x \<and> 2 * \<bar>b3\<bar> \<le> x \<and> 2 * \<bar>b4\<bar> \<le> x

goal (1 subgoal):
 1. odd x \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
have "2*\<bar>b1\<bar>\<noteq>x \<and> 2*\<bar>b2\<bar>\<noteq>x \<and> 2*\<bar>b3\<bar>\<noteq>x \<and> 2*\<bar>b4\<bar>\<noteq>x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * \<bar>b1\<bar> \<noteq> x \<and> 2 * \<bar>b2\<bar> \<noteq> x \<and> 2 * \<bar>b3\<bar> \<noteq> x \<and> 2 * \<bar>b4\<bar> \<noteq> x
[PROOF STEP]
using xodd
[PROOF STATE]
proof (prove)
using this:
odd x

goal (1 subgoal):
 1. 2 * \<bar>b1\<bar> \<noteq> x \<and> 2 * \<bar>b2\<bar> \<noteq> x \<and> 2 * \<bar>b3\<bar> \<noteq> x \<and> 2 * \<bar>b4\<bar> \<noteq> x
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
2 * \<bar>b1\<bar> \<noteq> x \<and> 2 * \<bar>b2\<bar> \<noteq> x \<and> 2 * \<bar>b3\<bar> \<noteq> x \<and> 2 * \<bar>b4\<bar> \<noteq> x

goal (1 subgoal):
 1. odd x \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
b1 = a1 - c1 * x \<and> b2 = a2 - c2 * x \<and> b3 = a3 - c3 * x \<and> b4 = a4 - c4 * x
2 * \<bar>b1\<bar> \<le> x \<and> 2 * \<bar>b2\<bar> \<le> x \<and> 2 * \<bar>b3\<bar> \<le> x \<and> 2 * \<bar>b4\<bar> \<le> x
2 * \<bar>b1\<bar> \<noteq> x \<and> 2 * \<bar>b2\<bar> \<noteq> x \<and> 2 * \<bar>b3\<bar> \<noteq> x \<and> 2 * \<bar>b4\<bar> \<noteq> x
[PROOF STEP]
have bc_abs: "2*\<bar>b1\<bar><x \<and> 2*\<bar>b2\<bar><x \<and> 2*\<bar>b3\<bar><x \<and> 2*\<bar>b4\<bar><x"
[PROOF STATE]
proof (prove)
using this:
b1 = a1 - c1 * x \<and> b2 = a2 - c2 * x \<and> b3 = a3 - c3 * x \<and> b4 = a4 - c4 * x
2 * \<bar>b1\<bar> \<le> x \<and> 2 * \<bar>b2\<bar> \<le> x \<and> 2 * \<bar>b3\<bar> \<le> x \<and> 2 * \<bar>b4\<bar> \<le> x
2 * \<bar>b1\<bar> \<noteq> x \<and> 2 * \<bar>b2\<bar> \<noteq> x \<and> 2 * \<bar>b3\<bar> \<noteq> x \<and> 2 * \<bar>b4\<bar> \<noteq> x

goal (1 subgoal):
 1. 2 * \<bar>b1\<bar> < x \<and> 2 * \<bar>b2\<bar> < x \<and> 2 * \<bar>b3\<bar> < x \<and> 2 * \<bar>b4\<bar> < x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
2 * \<bar>b1\<bar> < x \<and> 2 * \<bar>b2\<bar> < x \<and> 2 * \<bar>b3\<bar> < x \<and> 2 * \<bar>b4\<bar> < x

goal (1 subgoal):
 1. odd x \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
let ?B = "b1^2 + b2^2 + b3^2 + b4^2"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. odd x \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
let ?C = "c1^2 + c2^2 + c3^2 + c4^2"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. odd x \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
have "x dvd ?B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x dvd b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 = x * ?k
[PROOF STEP]
from bc_def ass
[PROOF STATE]
proof (chain)
picking this:
b1 = a1 - c1 * x \<and> b2 = a2 - c2 * x \<and> b3 = a3 - c3 * x \<and> b4 = a4 - c4 * x
1 < x \<and> x < p \<and> p * x = sum4sq_int (a1, a2, a3, a4)
[PROOF STEP]
have
            "?B = p*x - 2*(a1*c1+a2*c2+a3*c3+a4*c4)*x + ?C*x^2"
[PROOF STATE]
proof (prove)
using this:
b1 = a1 - c1 * x \<and> b2 = a2 - c2 * x \<and> b3 = a3 - c3 * x \<and> b4 = a4 - c4 * x
1 < x \<and> x < p \<and> p * x = sum4sq_int (a1, a2, a3, a4)

goal (1 subgoal):
 1. b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 = p * x - 2 * (a1 * c1 + a2 * c2 + a3 * c3 + a4 * c4) * x + (c1\<^sup>2 + c2\<^sup>2 + c3\<^sup>2 + c4\<^sup>2) * x\<^sup>2
[PROOF STEP]
unfolding sum4sq_int_def
[PROOF STATE]
proof (prove)
using this:
b1 = a1 - c1 * x \<and> b2 = a2 - c2 * x \<and> b3 = a3 - c3 * x \<and> b4 = a4 - c4 * x
1 < x \<and> x < p \<and> p * x = (case (a1, a2, a3, a4) of (a, b, c, d) \<Rightarrow> a\<^sup>2 + b\<^sup>2 + c\<^sup>2 + d\<^sup>2)

goal (1 subgoal):
 1. b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 = p * x - 2 * (a1 * c1 + a2 * c2 + a3 * c3 + a4 * c4) * x + (c1\<^sup>2 + c2\<^sup>2 + c3\<^sup>2 + c4\<^sup>2) * x\<^sup>2
[PROOF STEP]
by (auto simp add: power2_eq_square algebra_simps)
[PROOF STATE]
proof (state)
this:
b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 = p * x - 2 * (a1 * c1 + a2 * c2 + a3 * c3 + a4 * c4) * x + (c1\<^sup>2 + c2\<^sup>2 + c3\<^sup>2 + c4\<^sup>2) * x\<^sup>2

goal (1 subgoal):
 1. b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 = x * ?k
[PROOF STEP]
thus "?B = x*(p - 2*(a1*c1+a2*c2+a3*c3+a4*c4) + ?C*x)"
[PROOF STATE]
proof (prove)
using this:
b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 = p * x - 2 * (a1 * c1 + a2 * c2 + a3 * c3 + a4 * c4) * x + (c1\<^sup>2 + c2\<^sup>2 + c3\<^sup>2 + c4\<^sup>2) * x\<^sup>2

goal (1 subgoal):
 1. b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 = x * (p - 2 * (a1 * c1 + a2 * c2 + a3 * c3 + a4 * c4) + (c1\<^sup>2 + c2\<^sup>2 + c3\<^sup>2 + c4\<^sup>2) * x)
[PROOF STEP]
by (auto simp add: ac_simps power2_eq_square
              distrib_left right_diff_distrib)
[PROOF STATE]
proof (state)
this:
b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 = x * (p - 2 * (a1 * c1 + a2 * c2 + a3 * c3 + a4 * c4) + (c1\<^sup>2 + c2\<^sup>2 + c3\<^sup>2 + c4\<^sup>2) * x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x dvd b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2

goal (1 subgoal):
 1. odd x \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x dvd b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2
[PROOF STEP]
obtain y where y: "?B = x * y"
[PROOF STATE]
proof (prove)
using this:
x dvd b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2

goal (1 subgoal):
 1. (\<And>y. b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 = x * y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: dvd_def)
[PROOF STATE]
proof (state)
this:
b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 = x * y

goal (1 subgoal):
 1. odd x \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
let ?A1 = "a1*b1 + a2*b2 + a3*b3 + a4*b4"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. odd x \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
let ?A2 = "a1*b2 - a2*b1 - a3*b4 + a4*b3"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. odd x \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
let ?A3 = "a1*b3 + a2*b4 - a3*b1 - a4*b2"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. odd x \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
let ?A4 = "a1*b4 - a2*b3 + a3*b2 - a4*b1"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. odd x \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
let ?A = "sum4sq_int(?A1,?A2,?A3,?A4)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. odd x \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
have "x dvd ?A1 \<and> x dvd ?A2 \<and> x dvd ?A3 \<and> x dvd ?A4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x dvd a1 * b1 + a2 * b2 + a3 * b3 + a4 * b4 \<and> x dvd a1 * b2 - a2 * b1 - a3 * b4 + a4 * b3 \<and> x dvd a1 * b3 + a2 * b4 - a3 * b1 - a4 * b2 \<and> x dvd a1 * b4 - a2 * b3 + a3 * b2 - a4 * b1
[PROOF STEP]
proof (safe)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. x dvd a1 * b1 + a2 * b2 + a3 * b3 + a4 * b4
 2. x dvd a1 * b2 - a2 * b1 - a3 * b4 + a4 * b3
 3. x dvd a1 * b3 + a2 * b4 - a3 * b1 - a4 * b2
 4. x dvd a1 * b4 - a2 * b3 + a3 * b2 - a4 * b1
[PROOF STEP]
from bc_def
[PROOF STATE]
proof (chain)
picking this:
b1 = a1 - c1 * x \<and> b2 = a2 - c2 * x \<and> b3 = a3 - c3 * x \<and> b4 = a4 - c4 * x
[PROOF STEP]
have
            "?A1 = (b1+c1*x)*b1 + (b2+c2*x)*b2 + (b3+c3*x)*b3 + (b4+c4*x)*b4"
[PROOF STATE]
proof (prove)
using this:
b1 = a1 - c1 * x \<and> b2 = a2 - c2 * x \<and> b3 = a3 - c3 * x \<and> b4 = a4 - c4 * x

goal (1 subgoal):
 1. a1 * b1 + a2 * b2 + a3 * b3 + a4 * b4 = (b1 + c1 * x) * b1 + (b2 + c2 * x) * b2 + (b3 + c3 * x) * b3 + (b4 + c4 * x) * b4
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a1 * b1 + a2 * b2 + a3 * b3 + a4 * b4 = (b1 + c1 * x) * b1 + (b2 + c2 * x) * b2 + (b3 + c3 * x) * b3 + (b4 + c4 * x) * b4

goal (4 subgoals):
 1. x dvd a1 * b1 + a2 * b2 + a3 * b3 + a4 * b4
 2. x dvd a1 * b2 - a2 * b1 - a3 * b4 + a4 * b3
 3. x dvd a1 * b3 + a2 * b4 - a3 * b1 - a4 * b2
 4. x dvd a1 * b4 - a2 * b3 + a3 * b2 - a4 * b1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
a1 * b1 + a2 * b2 + a3 * b3 + a4 * b4 = (b1 + c1 * x) * b1 + (b2 + c2 * x) * b2 + (b3 + c3 * x) * b3 + (b4 + c4 * x) * b4

goal (4 subgoals):
 1. x dvd a1 * b1 + a2 * b2 + a3 * b3 + a4 * b4
 2. x dvd a1 * b2 - a2 * b1 - a3 * b4 + a4 * b3
 3. x dvd a1 * b3 + a2 * b4 - a3 * b1 - a4 * b2
 4. x dvd a1 * b4 - a2 * b3 + a3 * b2 - a4 * b1
[PROOF STEP]
with y
[PROOF STATE]
proof (chain)
picking this:
b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 = x * y
a1 * b1 + a2 * b2 + a3 * b3 + a4 * b4 = (b1 + c1 * x) * b1 + (b2 + c2 * x) * b2 + (b3 + c3 * x) * b3 + (b4 + c4 * x) * b4
[PROOF STEP]
have "\<dots> = x*(y + c1*b1 + c2*b2 + c3*b3 + c4*b4)"
[PROOF STATE]
proof (prove)
using this:
b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 = x * y
a1 * b1 + a2 * b2 + a3 * b3 + a4 * b4 = (b1 + c1 * x) * b1 + (b2 + c2 * x) * b2 + (b3 + c3 * x) * b3 + (b4 + c4 * x) * b4

goal (1 subgoal):
 1. (b1 + c1 * x) * b1 + (b2 + c2 * x) * b2 + (b3 + c3 * x) * b3 + (b4 + c4 * x) * b4 = x * (y + c1 * b1 + c2 * b2 + c3 * b3 + c4 * b4)
[PROOF STEP]
by (auto simp add: distrib_left power2_eq_square ac_simps)
[PROOF STATE]
proof (state)
this:
(b1 + c1 * x) * b1 + (b2 + c2 * x) * b2 + (b3 + c3 * x) * b3 + (b4 + c4 * x) * b4 = x * (y + c1 * b1 + c2 * b2 + c3 * b3 + c4 * b4)

goal (4 subgoals):
 1. x dvd a1 * b1 + a2 * b2 + a3 * b3 + a4 * b4
 2. x dvd a1 * b2 - a2 * b1 - a3 * b4 + a4 * b3
 3. x dvd a1 * b3 + a2 * b4 - a3 * b1 - a4 * b2
 4. x dvd a1 * b4 - a2 * b3 + a3 * b2 - a4 * b1
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
a1 * b1 + a2 * b2 + a3 * b3 + a4 * b4 = x * (y + c1 * b1 + c2 * b2 + c3 * b3 + c4 * b4)
[PROOF STEP]
show "x dvd ?A1"
[PROOF STATE]
proof (prove)
using this:
a1 * b1 + a2 * b2 + a3 * b3 + a4 * b4 = x * (y + c1 * b1 + c2 * b2 + c3 * b3 + c4 * b4)

goal (1 subgoal):
 1. x dvd a1 * b1 + a2 * b2 + a3 * b3 + a4 * b4
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x dvd a1 * b1 + a2 * b2 + a3 * b3 + a4 * b4

goal (3 subgoals):
 1. x dvd a1 * b2 - a2 * b1 - a3 * b4 + a4 * b3
 2. x dvd a1 * b3 + a2 * b4 - a3 * b1 - a4 * b2
 3. x dvd a1 * b4 - a2 * b3 + a3 * b2 - a4 * b1
[PROOF STEP]
from bc_def
[PROOF STATE]
proof (chain)
picking this:
b1 = a1 - c1 * x \<and> b2 = a2 - c2 * x \<and> b3 = a3 - c3 * x \<and> b4 = a4 - c4 * x
[PROOF STEP]
have
            "?A2 = (b1+c1*x)*b2 - (b2+c2*x)*b1 - (b3+c3*x)*b4 + (b4+c4*x)*b3"
[PROOF STATE]
proof (prove)
using this:
b1 = a1 - c1 * x \<and> b2 = a2 - c2 * x \<and> b3 = a3 - c3 * x \<and> b4 = a4 - c4 * x

goal (1 subgoal):
 1. a1 * b2 - a2 * b1 - a3 * b4 + a4 * b3 = (b1 + c1 * x) * b2 - (b2 + c2 * x) * b1 - (b3 + c3 * x) * b4 + (b4 + c4 * x) * b3
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a1 * b2 - a2 * b1 - a3 * b4 + a4 * b3 = (b1 + c1 * x) * b2 - (b2 + c2 * x) * b1 - (b3 + c3 * x) * b4 + (b4 + c4 * x) * b3

goal (3 subgoals):
 1. x dvd a1 * b2 - a2 * b1 - a3 * b4 + a4 * b3
 2. x dvd a1 * b3 + a2 * b4 - a3 * b1 - a4 * b2
 3. x dvd a1 * b4 - a2 * b3 + a3 * b2 - a4 * b1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
a1 * b2 - a2 * b1 - a3 * b4 + a4 * b3 = (b1 + c1 * x) * b2 - (b2 + c2 * x) * b1 - (b3 + c3 * x) * b4 + (b4 + c4 * x) * b3

goal (3 subgoals):
 1. x dvd a1 * b2 - a2 * b1 - a3 * b4 + a4 * b3
 2. x dvd a1 * b3 + a2 * b4 - a3 * b1 - a4 * b2
 3. x dvd a1 * b4 - a2 * b3 + a3 * b2 - a4 * b1
[PROOF STEP]
have "\<dots> = x*(c1*b2 - c2*b1 - c3*b4 + c4*b3)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b1 + c1 * x) * b2 - (b2 + c2 * x) * b1 - (b3 + c3 * x) * b4 + (b4 + c4 * x) * b3 = x * (c1 * b2 - c2 * b1 - c3 * b4 + c4 * b3)
[PROOF STEP]
by (auto simp add: distrib_left right_diff_distrib ac_simps)
[PROOF STATE]
proof (state)
this:
(b1 + c1 * x) * b2 - (b2 + c2 * x) * b1 - (b3 + c3 * x) * b4 + (b4 + c4 * x) * b3 = x * (c1 * b2 - c2 * b1 - c3 * b4 + c4 * b3)

goal (3 subgoals):
 1. x dvd a1 * b2 - a2 * b1 - a3 * b4 + a4 * b3
 2. x dvd a1 * b3 + a2 * b4 - a3 * b1 - a4 * b2
 3. x dvd a1 * b4 - a2 * b3 + a3 * b2 - a4 * b1
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
a1 * b2 - a2 * b1 - a3 * b4 + a4 * b3 = x * (c1 * b2 - c2 * b1 - c3 * b4 + c4 * b3)
[PROOF STEP]
show "x dvd ?A2"
[PROOF STATE]
proof (prove)
using this:
a1 * b2 - a2 * b1 - a3 * b4 + a4 * b3 = x * (c1 * b2 - c2 * b1 - c3 * b4 + c4 * b3)

goal (1 subgoal):
 1. x dvd a1 * b2 - a2 * b1 - a3 * b4 + a4 * b3
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x dvd a1 * b2 - a2 * b1 - a3 * b4 + a4 * b3

goal (2 subgoals):
 1. x dvd a1 * b3 + a2 * b4 - a3 * b1 - a4 * b2
 2. x dvd a1 * b4 - a2 * b3 + a3 * b2 - a4 * b1
[PROOF STEP]
from bc_def
[PROOF STATE]
proof (chain)
picking this:
b1 = a1 - c1 * x \<and> b2 = a2 - c2 * x \<and> b3 = a3 - c3 * x \<and> b4 = a4 - c4 * x
[PROOF STEP]
have
            "?A3 = (b1+c1*x)*b3 + (b2+c2*x)*b4 - (b3+c3*x)*b1 - (b4+c4*x)*b2"
[PROOF STATE]
proof (prove)
using this:
b1 = a1 - c1 * x \<and> b2 = a2 - c2 * x \<and> b3 = a3 - c3 * x \<and> b4 = a4 - c4 * x

goal (1 subgoal):
 1. a1 * b3 + a2 * b4 - a3 * b1 - a4 * b2 = (b1 + c1 * x) * b3 + (b2 + c2 * x) * b4 - (b3 + c3 * x) * b1 - (b4 + c4 * x) * b2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a1 * b3 + a2 * b4 - a3 * b1 - a4 * b2 = (b1 + c1 * x) * b3 + (b2 + c2 * x) * b4 - (b3 + c3 * x) * b1 - (b4 + c4 * x) * b2

goal (2 subgoals):
 1. x dvd a1 * b3 + a2 * b4 - a3 * b1 - a4 * b2
 2. x dvd a1 * b4 - a2 * b3 + a3 * b2 - a4 * b1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
a1 * b3 + a2 * b4 - a3 * b1 - a4 * b2 = (b1 + c1 * x) * b3 + (b2 + c2 * x) * b4 - (b3 + c3 * x) * b1 - (b4 + c4 * x) * b2

goal (2 subgoals):
 1. x dvd a1 * b3 + a2 * b4 - a3 * b1 - a4 * b2
 2. x dvd a1 * b4 - a2 * b3 + a3 * b2 - a4 * b1
[PROOF STEP]
have "\<dots> = x*(c1*b3 + c2*b4 - c3*b1 - c4*b2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b1 + c1 * x) * b3 + (b2 + c2 * x) * b4 - (b3 + c3 * x) * b1 - (b4 + c4 * x) * b2 = x * (c1 * b3 + c2 * b4 - c3 * b1 - c4 * b2)
[PROOF STEP]
by (auto simp add: distrib_left right_diff_distrib ac_simps)
[PROOF STATE]
proof (state)
this:
(b1 + c1 * x) * b3 + (b2 + c2 * x) * b4 - (b3 + c3 * x) * b1 - (b4 + c4 * x) * b2 = x * (c1 * b3 + c2 * b4 - c3 * b1 - c4 * b2)

goal (2 subgoals):
 1. x dvd a1 * b3 + a2 * b4 - a3 * b1 - a4 * b2
 2. x dvd a1 * b4 - a2 * b3 + a3 * b2 - a4 * b1
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
a1 * b3 + a2 * b4 - a3 * b1 - a4 * b2 = x * (c1 * b3 + c2 * b4 - c3 * b1 - c4 * b2)
[PROOF STEP]
show "x dvd ?A3"
[PROOF STATE]
proof (prove)
using this:
a1 * b3 + a2 * b4 - a3 * b1 - a4 * b2 = x * (c1 * b3 + c2 * b4 - c3 * b1 - c4 * b2)

goal (1 subgoal):
 1. x dvd a1 * b3 + a2 * b4 - a3 * b1 - a4 * b2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x dvd a1 * b3 + a2 * b4 - a3 * b1 - a4 * b2

goal (1 subgoal):
 1. x dvd a1 * b4 - a2 * b3 + a3 * b2 - a4 * b1
[PROOF STEP]
from bc_def
[PROOF STATE]
proof (chain)
picking this:
b1 = a1 - c1 * x \<and> b2 = a2 - c2 * x \<and> b3 = a3 - c3 * x \<and> b4 = a4 - c4 * x
[PROOF STEP]
have
            "?A4 = (b1+c1*x)*b4 - (b2+c2*x)*b3 + (b3+c3*x)*b2 - (b4+c4*x)*b1"
[PROOF STATE]
proof (prove)
using this:
b1 = a1 - c1 * x \<and> b2 = a2 - c2 * x \<and> b3 = a3 - c3 * x \<and> b4 = a4 - c4 * x

goal (1 subgoal):
 1. a1 * b4 - a2 * b3 + a3 * b2 - a4 * b1 = (b1 + c1 * x) * b4 - (b2 + c2 * x) * b3 + (b3 + c3 * x) * b2 - (b4 + c4 * x) * b1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a1 * b4 - a2 * b3 + a3 * b2 - a4 * b1 = (b1 + c1 * x) * b4 - (b2 + c2 * x) * b3 + (b3 + c3 * x) * b2 - (b4 + c4 * x) * b1

goal (1 subgoal):
 1. x dvd a1 * b4 - a2 * b3 + a3 * b2 - a4 * b1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
a1 * b4 - a2 * b3 + a3 * b2 - a4 * b1 = (b1 + c1 * x) * b4 - (b2 + c2 * x) * b3 + (b3 + c3 * x) * b2 - (b4 + c4 * x) * b1

goal (1 subgoal):
 1. x dvd a1 * b4 - a2 * b3 + a3 * b2 - a4 * b1
[PROOF STEP]
have "\<dots> = x*(c1*b4 - c2*b3 + c3*b2 - c4*b1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b1 + c1 * x) * b4 - (b2 + c2 * x) * b3 + (b3 + c3 * x) * b2 - (b4 + c4 * x) * b1 = x * (c1 * b4 - c2 * b3 + c3 * b2 - c4 * b1)
[PROOF STEP]
by (auto simp add: distrib_left right_diff_distrib ac_simps)
[PROOF STATE]
proof (state)
this:
(b1 + c1 * x) * b4 - (b2 + c2 * x) * b3 + (b3 + c3 * x) * b2 - (b4 + c4 * x) * b1 = x * (c1 * b4 - c2 * b3 + c3 * b2 - c4 * b1)

goal (1 subgoal):
 1. x dvd a1 * b4 - a2 * b3 + a3 * b2 - a4 * b1
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
a1 * b4 - a2 * b3 + a3 * b2 - a4 * b1 = x * (c1 * b4 - c2 * b3 + c3 * b2 - c4 * b1)
[PROOF STEP]
show "x dvd ?A4"
[PROOF STATE]
proof (prove)
using this:
a1 * b4 - a2 * b3 + a3 * b2 - a4 * b1 = x * (c1 * b4 - c2 * b3 + c3 * b2 - c4 * b1)

goal (1 subgoal):
 1. x dvd a1 * b4 - a2 * b3 + a3 * b2 - a4 * b1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x dvd a1 * b4 - a2 * b3 + a3 * b2 - a4 * b1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x dvd a1 * b1 + a2 * b2 + a3 * b3 + a4 * b4 \<and> x dvd a1 * b2 - a2 * b1 - a3 * b4 + a4 * b3 \<and> x dvd a1 * b3 + a2 * b4 - a3 * b1 - a4 * b2 \<and> x dvd a1 * b4 - a2 * b3 + a3 * b2 - a4 * b1

goal (1 subgoal):
 1. odd x \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x dvd a1 * b1 + a2 * b2 + a3 * b3 + a4 * b4 \<and> x dvd a1 * b2 - a2 * b1 - a3 * b4 + a4 * b3 \<and> x dvd a1 * b3 + a2 * b4 - a3 * b1 - a4 * b2 \<and> x dvd a1 * b4 - a2 * b3 + a3 * b2 - a4 * b1
[PROOF STEP]
obtain d1 d2 d3 d4 where d:
          "?A1=x*d1 \<and> ?A2=x*d2 \<and> ?A3=x*d3 \<and> ?A4=x*d4"
[PROOF STATE]
proof (prove)
using this:
x dvd a1 * b1 + a2 * b2 + a3 * b3 + a4 * b4 \<and> x dvd a1 * b2 - a2 * b1 - a3 * b4 + a4 * b3 \<and> x dvd a1 * b3 + a2 * b4 - a3 * b1 - a4 * b2 \<and> x dvd a1 * b4 - a2 * b3 + a3 * b2 - a4 * b1

goal (1 subgoal):
 1. (\<And>d1 d2 d3 d4. a1 * b1 + a2 * b2 + a3 * b3 + a4 * b4 = x * d1 \<and> a1 * b2 - a2 * b1 - a3 * b4 + a4 * b3 = x * d2 \<and> a1 * b3 + a2 * b4 - a3 * b1 - a4 * b2 = x * d3 \<and> a1 * b4 - a2 * b3 + a3 * b2 - a4 * b1 = x * d4 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: dvd_def)
[PROOF STATE]
proof (state)
this:
a1 * b1 + a2 * b2 + a3 * b3 + a4 * b4 = x * d1 \<and> a1 * b2 - a2 * b1 - a3 * b4 + a4 * b3 = x * d2 \<and> a1 * b3 + a2 * b4 - a3 * b1 - a4 * b2 = x * d3 \<and> a1 * b4 - a2 * b3 + a3 * b2 - a4 * b1 = x * d4

goal (1 subgoal):
 1. odd x \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
let ?D = "sum4sq_int(d1,d2,d3,d4)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. odd x \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
from d
[PROOF STATE]
proof (chain)
picking this:
a1 * b1 + a2 * b2 + a3 * b3 + a4 * b4 = x * d1 \<and> a1 * b2 - a2 * b1 - a3 * b4 + a4 * b3 = x * d2 \<and> a1 * b3 + a2 * b4 - a3 * b1 - a4 * b2 = x * d3 \<and> a1 * b4 - a2 * b3 + a3 * b2 - a4 * b1 = x * d4
[PROOF STEP]
have "x^2*?D = ?A"
[PROOF STATE]
proof (prove)
using this:
a1 * b1 + a2 * b2 + a3 * b3 + a4 * b4 = x * d1 \<and> a1 * b2 - a2 * b1 - a3 * b4 + a4 * b3 = x * d2 \<and> a1 * b3 + a2 * b4 - a3 * b1 - a4 * b2 = x * d3 \<and> a1 * b4 - a2 * b3 + a3 * b2 - a4 * b1 = x * d4

goal (1 subgoal):
 1. x\<^sup>2 * sum4sq_int (d1, d2, d3, d4) = sum4sq_int (a1 * b1 + a2 * b2 + a3 * b3 + a4 * b4, a1 * b2 - a2 * b1 - a3 * b4 + a4 * b3, a1 * b3 + a2 * b4 - a3 * b1 - a4 * b2, a1 * b4 - a2 * b3 + a3 * b2 - a4 * b1)
[PROOF STEP]
by (auto simp only: sum4sq_int_def power_mult_distrib distrib_left)
[PROOF STATE]
proof (state)
this:
x\<^sup>2 * sum4sq_int (d1, d2, d3, d4) = sum4sq_int (a1 * b1 + a2 * b2 + a3 * b3 + a4 * b4, a1 * b2 - a2 * b1 - a3 * b4 + a4 * b3, a1 * b3 + a2 * b4 - a3 * b1 - a4 * b2, a1 * b4 - a2 * b3 + a3 * b2 - a4 * b1)

goal (1 subgoal):
 1. odd x \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x\<^sup>2 * sum4sq_int (d1, d2, d3, d4) = sum4sq_int (a1 * b1 + a2 * b2 + a3 * b3 + a4 * b4, a1 * b2 - a2 * b1 - a3 * b4 + a4 * b3, a1 * b3 + a2 * b4 - a3 * b1 - a4 * b2, a1 * b4 - a2 * b3 + a3 * b2 - a4 * b1)

goal (1 subgoal):
 1. odd x \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
have "\<dots> = sum4sq_int(a1,a2,a3,a4)*sum4sq_int(b1,b2,b3,b4)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum4sq_int (a1 * b1 + a2 * b2 + a3 * b3 + a4 * b4, a1 * b2 - a2 * b1 - a3 * b4 + a4 * b3, a1 * b3 + a2 * b4 - a3 * b1 - a4 * b2, a1 * b4 - a2 * b3 + a3 * b2 - a4 * b1) = sum4sq_int (a1, a2, a3, a4) * sum4sq_int (b1, b2, b3, b4)
[PROOF STEP]
by (simp only: mult_sum4sq_int)
[PROOF STATE]
proof (state)
this:
sum4sq_int (a1 * b1 + a2 * b2 + a3 * b3 + a4 * b4, a1 * b2 - a2 * b1 - a3 * b4 + a4 * b3, a1 * b3 + a2 * b4 - a3 * b1 - a4 * b2, a1 * b4 - a2 * b3 + a3 * b2 - a4 * b1) = sum4sq_int (a1, a2, a3, a4) * sum4sq_int (b1, b2, b3, b4)

goal (1 subgoal):
 1. odd x \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum4sq_int (a1 * b1 + a2 * b2 + a3 * b3 + a4 * b4, a1 * b2 - a2 * b1 - a3 * b4 + a4 * b3, a1 * b3 + a2 * b4 - a3 * b1 - a4 * b2, a1 * b4 - a2 * b3 + a3 * b2 - a4 * b1) = sum4sq_int (a1, a2, a3, a4) * sum4sq_int (b1, b2, b3, b4)

goal (1 subgoal):
 1. odd x \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
with y ass
[PROOF STATE]
proof (chain)
picking this:
b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 = x * y
1 < x \<and> x < p \<and> p * x = sum4sq_int (a1, a2, a3, a4)
sum4sq_int (a1 * b1 + a2 * b2 + a3 * b3 + a4 * b4, a1 * b2 - a2 * b1 - a3 * b4 + a4 * b3, a1 * b3 + a2 * b4 - a3 * b1 - a4 * b2, a1 * b4 - a2 * b3 + a3 * b2 - a4 * b1) = sum4sq_int (a1, a2, a3, a4) * sum4sq_int (b1, b2, b3, b4)
[PROOF STEP]
have "\<dots> = (p*x)*(x*y)"
[PROOF STATE]
proof (prove)
using this:
b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 = x * y
1 < x \<and> x < p \<and> p * x = sum4sq_int (a1, a2, a3, a4)
sum4sq_int (a1 * b1 + a2 * b2 + a3 * b3 + a4 * b4, a1 * b2 - a2 * b1 - a3 * b4 + a4 * b3, a1 * b3 + a2 * b4 - a3 * b1 - a4 * b2, a1 * b4 - a2 * b3 + a3 * b2 - a4 * b1) = sum4sq_int (a1, a2, a3, a4) * sum4sq_int (b1, b2, b3, b4)

goal (1 subgoal):
 1. sum4sq_int (a1, a2, a3, a4) * sum4sq_int (b1, b2, b3, b4) = p * x * (x * y)
[PROOF STEP]
by (auto simp add: sum4sq_int_def)
[PROOF STATE]
proof (state)
this:
sum4sq_int (a1, a2, a3, a4) * sum4sq_int (b1, b2, b3, b4) = p * x * (x * y)

goal (1 subgoal):
 1. odd x \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum4sq_int (a1, a2, a3, a4) * sum4sq_int (b1, b2, b3, b4) = p * x * (x * y)

goal (1 subgoal):
 1. odd x \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
have "\<dots> = x^2*(p*y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p * x * (x * y) = x\<^sup>2 * (p * y)
[PROOF STEP]
by (simp only: power2_eq_square ac_simps)
[PROOF STATE]
proof (state)
this:
p * x * (x * y) = x\<^sup>2 * (p * y)

goal (1 subgoal):
 1. odd x \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x\<^sup>2 * sum4sq_int (d1, d2, d3, d4) = x\<^sup>2 * (p * y)
[PROOF STEP]
have "x^2*(?D - p*y) = 0"
[PROOF STATE]
proof (prove)
using this:
x\<^sup>2 * sum4sq_int (d1, d2, d3, d4) = x\<^sup>2 * (p * y)

goal (1 subgoal):
 1. x\<^sup>2 * (sum4sq_int (d1, d2, d3, d4) - p * y) = 0
[PROOF STEP]
by (auto simp add: right_diff_distrib)
[PROOF STATE]
proof (state)
this:
x\<^sup>2 * (sum4sq_int (d1, d2, d3, d4) - p * y) = 0

goal (1 subgoal):
 1. odd x \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
with ass
[PROOF STATE]
proof (chain)
picking this:
1 < x \<and> x < p \<and> p * x = sum4sq_int (a1, a2, a3, a4)
x\<^sup>2 * (sum4sq_int (d1, d2, d3, d4) - p * y) = 0
[PROOF STEP]
have "p*y = ?D"
[PROOF STATE]
proof (prove)
using this:
1 < x \<and> x < p \<and> p * x = sum4sq_int (a1, a2, a3, a4)
x\<^sup>2 * (sum4sq_int (d1, d2, d3, d4) - p * y) = 0

goal (1 subgoal):
 1. p * y = sum4sq_int (d1, d2, d3, d4)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p * y = sum4sq_int (d1, d2, d3, d4)

goal (1 subgoal):
 1. odd x \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
p * y = sum4sq_int (d1, d2, d3, d4)

goal (1 subgoal):
 1. odd x \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
have y_l_x: "y < x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y < x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. y < x
[PROOF STEP]
have "4*b1^2 = (2*\<bar>b1\<bar>)^2 \<and> 4*b2^2 = (2*\<bar>b2\<bar>)^2 \<and>
            4*b3^2 = (2*\<bar>b3\<bar>)^2 \<and> 4*b4^2 = (2*\<bar>b4\<bar>)^2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 4 * b1\<^sup>2 = (2 * \<bar>b1\<bar>)\<^sup>2 \<and> 4 * b2\<^sup>2 = (2 * \<bar>b2\<bar>)\<^sup>2 \<and> 4 * b3\<^sup>2 = (2 * \<bar>b3\<bar>)\<^sup>2 \<and> 4 * b4\<^sup>2 = (2 * \<bar>b4\<bar>)\<^sup>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
4 * b1\<^sup>2 = (2 * \<bar>b1\<bar>)\<^sup>2 \<and> 4 * b2\<^sup>2 = (2 * \<bar>b2\<bar>)\<^sup>2 \<and> 4 * b3\<^sup>2 = (2 * \<bar>b3\<bar>)\<^sup>2 \<and> 4 * b4\<^sup>2 = (2 * \<bar>b4\<bar>)\<^sup>2

goal (1 subgoal):
 1. y < x
[PROOF STEP]
with bc_abs
[PROOF STATE]
proof (chain)
picking this:
2 * \<bar>b1\<bar> < x \<and> 2 * \<bar>b2\<bar> < x \<and> 2 * \<bar>b3\<bar> < x \<and> 2 * \<bar>b4\<bar> < x
4 * b1\<^sup>2 = (2 * \<bar>b1\<bar>)\<^sup>2 \<and> 4 * b2\<^sup>2 = (2 * \<bar>b2\<bar>)\<^sup>2 \<and> 4 * b3\<^sup>2 = (2 * \<bar>b3\<bar>)\<^sup>2 \<and> 4 * b4\<^sup>2 = (2 * \<bar>b4\<bar>)\<^sup>2
[PROOF STEP]
have "4*b1^2<x^2 \<and> 4*b2^2<x^2 \<and> 4*b3^2<x^2 \<and> 4*b4^2<x^2"
[PROOF STATE]
proof (prove)
using this:
2 * \<bar>b1\<bar> < x \<and> 2 * \<bar>b2\<bar> < x \<and> 2 * \<bar>b3\<bar> < x \<and> 2 * \<bar>b4\<bar> < x
4 * b1\<^sup>2 = (2 * \<bar>b1\<bar>)\<^sup>2 \<and> 4 * b2\<^sup>2 = (2 * \<bar>b2\<bar>)\<^sup>2 \<and> 4 * b3\<^sup>2 = (2 * \<bar>b3\<bar>)\<^sup>2 \<and> 4 * b4\<^sup>2 = (2 * \<bar>b4\<bar>)\<^sup>2

goal (1 subgoal):
 1. 4 * b1\<^sup>2 < x\<^sup>2 \<and> 4 * b2\<^sup>2 < x\<^sup>2 \<and> 4 * b3\<^sup>2 < x\<^sup>2 \<and> 4 * b4\<^sup>2 < x\<^sup>2
[PROOF STEP]
using power_strict_mono [of "2*\<bar>b\<bar>" x 2 for b]
[PROOF STATE]
proof (prove)
using this:
2 * \<bar>b1\<bar> < x \<and> 2 * \<bar>b2\<bar> < x \<and> 2 * \<bar>b3\<bar> < x \<and> 2 * \<bar>b4\<bar> < x
4 * b1\<^sup>2 = (2 * \<bar>b1\<bar>)\<^sup>2 \<and> 4 * b2\<^sup>2 = (2 * \<bar>b2\<bar>)\<^sup>2 \<and> 4 * b3\<^sup>2 = (2 * \<bar>b3\<bar>)\<^sup>2 \<and> 4 * b4\<^sup>2 = (2 * \<bar>b4\<bar>)\<^sup>2
\<lbrakk>2 * \<bar>?ba2\<bar> < x; 0 \<le> 2 * \<bar>?ba2\<bar>; 0 < 2\<rbrakk> \<Longrightarrow> (2 * \<bar>?ba2\<bar>)\<^sup>2 < x\<^sup>2

goal (1 subgoal):
 1. 4 * b1\<^sup>2 < x\<^sup>2 \<and> 4 * b2\<^sup>2 < x\<^sup>2 \<and> 4 * b3\<^sup>2 < x\<^sup>2 \<and> 4 * b4\<^sup>2 < x\<^sup>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
4 * b1\<^sup>2 < x\<^sup>2 \<and> 4 * b2\<^sup>2 < x\<^sup>2 \<and> 4 * b3\<^sup>2 < x\<^sup>2 \<and> 4 * b4\<^sup>2 < x\<^sup>2

goal (1 subgoal):
 1. y < x
[PROOF STEP]
hence "?B < x^2"
[PROOF STATE]
proof (prove)
using this:
4 * b1\<^sup>2 < x\<^sup>2 \<and> 4 * b2\<^sup>2 < x\<^sup>2 \<and> 4 * b3\<^sup>2 < x\<^sup>2 \<and> 4 * b4\<^sup>2 < x\<^sup>2

goal (1 subgoal):
 1. b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 < x\<^sup>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 < x\<^sup>2

goal (1 subgoal):
 1. y < x
[PROOF STEP]
with y
[PROOF STATE]
proof (chain)
picking this:
b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 = x * y
b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 < x\<^sup>2
[PROOF STEP]
have "x*(x-y) > 0"
[PROOF STATE]
proof (prove)
using this:
b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 = x * y
b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 < x\<^sup>2

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

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

goal (1 subgoal):
 1. y < x
[PROOF STEP]
from ass
[PROOF STATE]
proof (chain)
picking this:
1 < x \<and> x < p \<and> p * x = sum4sq_int (a1, a2, a3, a4)
[PROOF STEP]
have "x > 0"
[PROOF STATE]
proof (prove)
using this:
1 < x \<and> x < p \<and> p * x = sum4sq_int (a1, a2, a3, a4)

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

goal (1 subgoal):
 1. y < x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
0 < x * (x - y)
0 < x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < x * (x - y)
0 < x

goal (1 subgoal):
 1. y < x
[PROOF STEP]
using zero_less_mult_pos
[PROOF STATE]
proof (prove)
using this:
0 < x * (x - y)
0 < x
\<lbrakk>(0::?'a) < ?a * ?b; (0::?'a) < ?a\<rbrakk> \<Longrightarrow> (0::?'a) < ?b

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

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

goal (1 subgoal):
 1. odd x \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
y < x

goal (1 subgoal):
 1. odd x \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
have "y > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < y
[PROOF STEP]
have b2pos: "b1^2 \<ge> 0 \<and> b2^2 \<ge> 0 \<and> b3^2 \<ge> 0 \<and> b4^2 \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> b1\<^sup>2 \<and> 0 \<le> b2\<^sup>2 \<and> 0 \<le> b3\<^sup>2 \<and> 0 \<le> b4\<^sup>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 \<le> b1\<^sup>2 \<and> 0 \<le> b2\<^sup>2 \<and> 0 \<le> b3\<^sup>2 \<and> 0 \<le> b4\<^sup>2

goal (1 subgoal):
 1. 0 < y
[PROOF STEP]
hence "?B = 0 \<or> ?B > 0"
[PROOF STATE]
proof (prove)
using this:
0 \<le> b1\<^sup>2 \<and> 0 \<le> b2\<^sup>2 \<and> 0 \<le> b3\<^sup>2 \<and> 0 \<le> b4\<^sup>2

goal (1 subgoal):
 1. b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 = 0 \<or> 0 < b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 = 0 \<or> 0 < b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2

goal (1 subgoal):
 1. 0 < y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 = 0 \<or> 0 < b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2

goal (1 subgoal):
 1. 0 < y
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 = 0 \<or> 0 < b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2

goal (1 subgoal):
 1. 0 < y
[PROOF STEP]
assume "?B = 0"
[PROOF STATE]
proof (state)
this:
b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 = 0

goal (1 subgoal):
 1. 0 < y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 = 0

goal (1 subgoal):
 1. 0 < y
[PROOF STEP]
from b2pos
[PROOF STATE]
proof (chain)
picking this:
0 \<le> b1\<^sup>2 \<and> 0 \<le> b2\<^sup>2 \<and> 0 \<le> b3\<^sup>2 \<and> 0 \<le> b4\<^sup>2
[PROOF STEP]
have
              "?B-b1^2 \<ge> 0 \<and> ?B-b2^2 \<ge> 0 \<and> ?B-b3^2 \<ge> 0 \<and> ?B-b4^2 \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
0 \<le> b1\<^sup>2 \<and> 0 \<le> b2\<^sup>2 \<and> 0 \<le> b3\<^sup>2 \<and> 0 \<le> b4\<^sup>2

goal (1 subgoal):
 1. 0 \<le> b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 - b1\<^sup>2 \<and> 0 \<le> b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 - b2\<^sup>2 \<and> 0 \<le> b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 - b3\<^sup>2 \<and> 0 \<le> b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 - b4\<^sup>2
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
0 \<le> b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 - b1\<^sup>2 \<and> 0 \<le> b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 - b2\<^sup>2 \<and> 0 \<le> b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 - b3\<^sup>2 \<and> 0 \<le> b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 - b4\<^sup>2

goal (1 subgoal):
 1. 0 < y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 = 0
0 \<le> b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 - b1\<^sup>2 \<and> 0 \<le> b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 - b2\<^sup>2 \<and> 0 \<le> b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 - b3\<^sup>2 \<and> 0 \<le> b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 - b4\<^sup>2
[PROOF STEP]
have "b1^2 \<le> 0 \<and> b2^2 \<le> 0 \<and> b3^2 \<le> 0 \<and> b4^2 \<le> 0"
[PROOF STATE]
proof (prove)
using this:
b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 = 0
0 \<le> b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 - b1\<^sup>2 \<and> 0 \<le> b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 - b2\<^sup>2 \<and> 0 \<le> b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 - b3\<^sup>2 \<and> 0 \<le> b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 - b4\<^sup>2

goal (1 subgoal):
 1. b1\<^sup>2 \<le> 0 \<and> b2\<^sup>2 \<le> 0 \<and> b3\<^sup>2 \<le> 0 \<and> b4\<^sup>2 \<le> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
b1\<^sup>2 \<le> 0 \<and> b2\<^sup>2 \<le> 0 \<and> b3\<^sup>2 \<le> 0 \<and> b4\<^sup>2 \<le> 0

goal (1 subgoal):
 1. 0 < y
[PROOF STEP]
with b2pos
[PROOF STATE]
proof (chain)
picking this:
0 \<le> b1\<^sup>2 \<and> 0 \<le> b2\<^sup>2 \<and> 0 \<le> b3\<^sup>2 \<and> 0 \<le> b4\<^sup>2
b1\<^sup>2 \<le> 0 \<and> b2\<^sup>2 \<le> 0 \<and> b3\<^sup>2 \<le> 0 \<and> b4\<^sup>2 \<le> 0
[PROOF STEP]
have  "b1^2 = 0 \<and> b2^2 = 0 \<and> b3^2 = 0 \<and> b4^2 = 0"
[PROOF STATE]
proof (prove)
using this:
0 \<le> b1\<^sup>2 \<and> 0 \<le> b2\<^sup>2 \<and> 0 \<le> b3\<^sup>2 \<and> 0 \<le> b4\<^sup>2
b1\<^sup>2 \<le> 0 \<and> b2\<^sup>2 \<le> 0 \<and> b3\<^sup>2 \<le> 0 \<and> b4\<^sup>2 \<le> 0

goal (1 subgoal):
 1. b1\<^sup>2 = 0 \<and> b2\<^sup>2 = 0 \<and> b3\<^sup>2 = 0 \<and> b4\<^sup>2 = 0
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
b1\<^sup>2 = 0 \<and> b2\<^sup>2 = 0 \<and> b3\<^sup>2 = 0 \<and> b4\<^sup>2 = 0

goal (1 subgoal):
 1. 0 < y
[PROOF STEP]
hence "b1 = 0 \<and> b2 = 0 \<and> b3 = 0 \<and> b4 = 0"
[PROOF STATE]
proof (prove)
using this:
b1\<^sup>2 = 0 \<and> b2\<^sup>2 = 0 \<and> b3\<^sup>2 = 0 \<and> b4\<^sup>2 = 0

goal (1 subgoal):
 1. b1 = 0 \<and> b2 = 0 \<and> b3 = 0 \<and> b4 = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
b1 = 0 \<and> b2 = 0 \<and> b3 = 0 \<and> b4 = 0

goal (1 subgoal):
 1. 0 < y
[PROOF STEP]
with bc_def
[PROOF STATE]
proof (chain)
picking this:
b1 = a1 - c1 * x \<and> b2 = a2 - c2 * x \<and> b3 = a3 - c3 * x \<and> b4 = a4 - c4 * x
b1 = 0 \<and> b2 = 0 \<and> b3 = 0 \<and> b4 = 0
[PROOF STEP]
have "x dvd a1 \<and> x dvd a2 \<and> x dvd a3 \<and> x dvd a4"
[PROOF STATE]
proof (prove)
using this:
b1 = a1 - c1 * x \<and> b2 = a2 - c2 * x \<and> b3 = a3 - c3 * x \<and> b4 = a4 - c4 * x
b1 = 0 \<and> b2 = 0 \<and> b3 = 0 \<and> b4 = 0

goal (1 subgoal):
 1. x dvd a1 \<and> x dvd a2 \<and> x dvd a3 \<and> x dvd a4
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x dvd a1 \<and> x dvd a2 \<and> x dvd a3 \<and> x dvd a4

goal (1 subgoal):
 1. 0 < y
[PROOF STEP]
hence "x^2 dvd a1^2 \<and> x^2 dvd a2^2 \<and> x^2 dvd a3^2 \<and> x^2 dvd a4^2"
[PROOF STATE]
proof (prove)
using this:
x dvd a1 \<and> x dvd a2 \<and> x dvd a3 \<and> x dvd a4

goal (1 subgoal):
 1. x\<^sup>2 dvd a1\<^sup>2 \<and> x\<^sup>2 dvd a2\<^sup>2 \<and> x\<^sup>2 dvd a3\<^sup>2 \<and> x\<^sup>2 dvd a4\<^sup>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x\<^sup>2 dvd a1\<^sup>2 \<and> x\<^sup>2 dvd a2\<^sup>2 \<and> x\<^sup>2 dvd a3\<^sup>2 \<and> x\<^sup>2 dvd a4\<^sup>2

goal (1 subgoal):
 1. 0 < y
[PROOF STEP]
hence "x^2 dvd a1^2+a2^2+a3^2+a4^2"
[PROOF STATE]
proof (prove)
using this:
x\<^sup>2 dvd a1\<^sup>2 \<and> x\<^sup>2 dvd a2\<^sup>2 \<and> x\<^sup>2 dvd a3\<^sup>2 \<and> x\<^sup>2 dvd a4\<^sup>2

goal (1 subgoal):
 1. x\<^sup>2 dvd a1\<^sup>2 + a2\<^sup>2 + a3\<^sup>2 + a4\<^sup>2
[PROOF STEP]
by (simp only: dvd_add)
[PROOF STATE]
proof (state)
this:
x\<^sup>2 dvd a1\<^sup>2 + a2\<^sup>2 + a3\<^sup>2 + a4\<^sup>2

goal (1 subgoal):
 1. 0 < y
[PROOF STEP]
with ass
[PROOF STATE]
proof (chain)
picking this:
1 < x \<and> x < p \<and> p * x = sum4sq_int (a1, a2, a3, a4)
x\<^sup>2 dvd a1\<^sup>2 + a2\<^sup>2 + a3\<^sup>2 + a4\<^sup>2
[PROOF STEP]
have "x^2 dvd p*x"
[PROOF STATE]
proof (prove)
using this:
1 < x \<and> x < p \<and> p * x = sum4sq_int (a1, a2, a3, a4)
x\<^sup>2 dvd a1\<^sup>2 + a2\<^sup>2 + a3\<^sup>2 + a4\<^sup>2

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

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

goal (1 subgoal):
 1. x * x dvd x * p
[PROOF STEP]
by (simp only: power2_eq_square ac_simps)
[PROOF STATE]
proof (state)
this:
x * x dvd x * p

goal (1 subgoal):
 1. 0 < y
[PROOF STEP]
with ass
[PROOF STATE]
proof (chain)
picking this:
1 < x \<and> x < p \<and> p * x = sum4sq_int (a1, a2, a3, a4)
x * x dvd x * p
[PROOF STEP]
have "nat x dvd nat p"
[PROOF STATE]
proof (prove)
using this:
1 < x \<and> x < p \<and> p * x = sum4sq_int (a1, a2, a3, a4)
x * x dvd x * p

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

goal (1 subgoal):
 1. 0 < y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
nat x dvd nat p

goal (1 subgoal):
 1. 0 < y
[PROOF STEP]
from ass prp
[PROOF STATE]
proof (chain)
picking this:
1 < x \<and> x < p \<and> p * x = sum4sq_int (a1, a2, a3, a4)
prime (nat p)
[PROOF STEP]
have "x \<ge> 0 \<and> x \<noteq> 1 \<and> x \<noteq> p \<and> prime (nat p)"
[PROOF STATE]
proof (prove)
using this:
1 < x \<and> x < p \<and> p * x = sum4sq_int (a1, a2, a3, a4)
prime (nat p)

goal (1 subgoal):
 1. 0 \<le> x \<and> x \<noteq> 1 \<and> x \<noteq> p \<and> prime (nat p)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 \<le> x \<and> x \<noteq> 1 \<and> x \<noteq> p \<and> prime (nat p)

goal (1 subgoal):
 1. 0 < y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
nat x dvd nat p
0 \<le> x \<and> x \<noteq> 1 \<and> x \<noteq> p \<and> prime (nat p)
[PROOF STEP]
have "False"
[PROOF STATE]
proof (prove)
using this:
nat x dvd nat p
0 \<le> x \<and> x \<noteq> 1 \<and> x \<noteq> p \<and> prime (nat p)

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding prime_nat_iff
[PROOF STATE]
proof (prove)
using this:
nat x dvd nat p
0 \<le> x \<and> x \<noteq> 1 \<and> x \<noteq> p \<and> 1 < nat p \<and> (\<forall>m. m dvd nat p \<longrightarrow> m = 1 \<or> m = nat p)

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

goal (1 subgoal):
 1. 0 < y
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 = 0 \<Longrightarrow> False

goal (1 subgoal):
 1. 0 < y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 = 0 \<Longrightarrow> False

goal (1 subgoal):
 1. 0 < y
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 = 0 \<Longrightarrow> False

goal (1 subgoal):
 1. 0 < y
[PROOF STEP]
assume "?B > 0"
[PROOF STATE]
proof (state)
this:
0 < b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2

goal (1 subgoal):
 1. 0 < y
[PROOF STEP]
with y
[PROOF STATE]
proof (chain)
picking this:
b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 = x * y
0 < b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2
[PROOF STEP]
have "x*y > 0"
[PROOF STATE]
proof (prove)
using this:
b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 = x * y
0 < b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2

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

goal (1 subgoal):
 1. 0 < y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 < x * y

goal (1 subgoal):
 1. 0 < y
[PROOF STEP]
from ass
[PROOF STATE]
proof (chain)
picking this:
1 < x \<and> x < p \<and> p * x = sum4sq_int (a1, a2, a3, a4)
[PROOF STEP]
have "x > 0"
[PROOF STATE]
proof (prove)
using this:
1 < x \<and> x < p \<and> p * x = sum4sq_int (a1, a2, a3, a4)

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

goal (1 subgoal):
 1. 0 < y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
0 < x * y
0 < x
[PROOF STEP]
have ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < x * y
0 < x

goal (1 subgoal):
 1. 0 < y
[PROOF STEP]
using zero_less_mult_pos
[PROOF STATE]
proof (prove)
using this:
0 < x * y
0 < x
\<lbrakk>(0::?'a) < ?a * ?b; (0::?'a) < ?a\<rbrakk> \<Longrightarrow> (0::?'a) < ?b

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

goal (1 subgoal):
 1. 0 < y
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
0 < b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 \<Longrightarrow> 0 < y

goal (1 subgoal):
 1. 0 < y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 = 0 \<or> 0 < b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2
b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 = 0 \<Longrightarrow> False
0 < b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 \<Longrightarrow> 0 < y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 = 0 \<or> 0 < b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2
b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 = 0 \<Longrightarrow> False
0 < b1\<^sup>2 + b2\<^sup>2 + b3\<^sup>2 + b4\<^sup>2 \<Longrightarrow> 0 < y

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

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

goal (1 subgoal):
 1. odd x \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 < y

goal (1 subgoal):
 1. odd x \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
with y_l_x
[PROOF STATE]
proof (chain)
picking this:
y < x
0 < y
[PROOF STEP]
have "(nat y) - 1 < (nat x) - 1"
[PROOF STATE]
proof (prove)
using this:
y < x
0 < y

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

goal (1 subgoal):
 1. odd x \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
nat y - 1 < nat x - 1

goal (1 subgoal):
 1. odd x \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
from y_l_x ass
[PROOF STATE]
proof (chain)
picking this:
y < x
1 < x \<and> x < p \<and> p * x = sum4sq_int (a1, a2, a3, a4)
[PROOF STEP]
have "y < p"
[PROOF STATE]
proof (prove)
using this:
y < x
1 < x \<and> x < p \<and> p * x = sum4sq_int (a1, a2, a3, a4)

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

goal (1 subgoal):
 1. odd x \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
p * y = sum4sq_int (d1, d2, d3, d4)
y < x
0 < y
nat y - 1 < nat x - 1
y < p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p * y = sum4sq_int (d1, d2, d3, d4)
y < x
0 < y
nat y - 1 < nat x - 1
y < p

goal (1 subgoal):
 1. \<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))

goal (1 subgoal):
 1. \<And>x. \<lbrakk>0 < nat x - 1; \<not> \<not> (0 < x \<and> x < p \<and> (\<exists>a1 a2 a3 a4. p * x = sum4sq_int (a1, a2, a3, a4)))\<rbrakk> \<Longrightarrow> \<exists>y. nat y - 1 < nat x - 1 \<and> \<not> \<not> (0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4)))
[PROOF STEP]
thus "\<exists> y. nat y - 1 < nat x - 1 \<and> \<not> \<not> ?Q y"
[PROOF STATE]
proof (prove)
using this:
\<exists>y. nat y - 1 < nat x - 1 \<and> 0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4))

goal (1 subgoal):
 1. \<exists>y. nat y - 1 < nat x - 1 \<and> \<not> \<not> (0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4)))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>y. nat y - 1 < nat x - 1 \<and> \<not> \<not> (0 < y \<and> y < p \<and> (\<exists>a1 a2 a3 a4. p * y = sum4sq_int (a1, a2, a3, a4)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> (0 < t \<and> t < p \<and> (\<exists>a1 a2 a3 a4. p * t = sum4sq_int (a1, a2, a3, a4)))

goal (1 subgoal):
 1. \<not> (0 < 1 \<and> 1 < p \<and> (\<exists>a1 a2 a3 a4. p * 1 = sum4sq_int (a1, a2, a3, a4))) \<Longrightarrow> False
[PROOF STEP]
with Qt
[PROOF STATE]
proof (chain)
picking this:
0 < t \<and> t < p \<and> (\<exists>a1 a2 a3 a4. p * t = sum4sq_int (a1, a2, a3, a4))
\<not> (0 < t \<and> t < p \<and> (\<exists>a1 a2 a3 a4. p * t = sum4sq_int (a1, a2, a3, a4)))
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
0 < t \<and> t < p \<and> (\<exists>a1 a2 a3 a4. p * t = sum4sq_int (a1, a2, a3, a4))
\<not> (0 < t \<and> t < p \<and> (\<exists>a1 a2 a3 a4. p * t = sum4sq_int (a1, a2, a3, a4)))

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 < 1 \<and> 1 < p \<and> (\<exists>a1 a2 a3 a4. p * 1 = sum4sq_int (a1, a2, a3, a4))

goal (1 subgoal):
 1. \<lbrakk>prime (nat p); p \<noteq> 2\<rbrakk> \<Longrightarrow> is_sum4sq_int p
[PROOF STEP]
thus "is_sum4sq_int p"
[PROOF STATE]
proof (prove)
using this:
0 < 1 \<and> 1 < p \<and> (\<exists>a1 a2 a3 a4. p * 1 = sum4sq_int (a1, a2, a3, a4))

goal (1 subgoal):
 1. is_sum4sq_int p
[PROOF STEP]
by (auto simp add: is_sum4sq_int_def)
[PROOF STATE]
proof (state)
this:
is_sum4sq_int p

goal:
No subgoals!
[PROOF STEP]
qed