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

goal (1 subgoal):
 1. is_sum2sq_nat n
[PROOF STEP]
proof (induction n rule: nat_less_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>m<n. (\<forall>x. prime (4 * x + 3) \<longrightarrow> even (multiplicity (4 * x + 3) m)) \<longrightarrow> is_sum2sq_nat m; \<And>k. prime (4 * k + 3) \<longrightarrow> even (multiplicity (4 * k + 3) n)\<rbrakk> \<Longrightarrow> is_sum2sq_nat n
[PROOF STEP]
case (1 n)
[PROOF STATE]
proof (state)
this:
\<forall>m<n. (\<forall>x. prime (4 * x + 3) \<longrightarrow> even (multiplicity (4 * x + 3) m)) \<longrightarrow> is_sum2sq_nat m
prime (4 * ?k + 3) \<longrightarrow> even (multiplicity (4 * ?k + 3) n)

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>m<n. (\<forall>x. prime (4 * x + 3) \<longrightarrow> even (multiplicity (4 * x + 3) m)) \<longrightarrow> is_sum2sq_nat m; \<And>k. prime (4 * k + 3) \<longrightarrow> even (multiplicity (4 * k + 3) n)\<rbrakk> \<Longrightarrow> is_sum2sq_nat n
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>m<n. (\<forall>x. prime (4 * x + 3) \<longrightarrow> even (multiplicity (4 * x + 3) m)) \<longrightarrow> is_sum2sq_nat m
prime (4 * ?k + 3) \<longrightarrow> even (multiplicity (4 * ?k + 3) n)

goal (1 subgoal):
 1. is_sum2sq_nat n
[PROOF STEP]
proof (cases "n>1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<forall>m<n. (\<forall>x. prime (4 * x + 3) \<longrightarrow> even (multiplicity (4 * x + 3) m)) \<longrightarrow> is_sum2sq_nat m; \<And>k. prime (4 * k + 3) \<longrightarrow> even (multiplicity (4 * k + 3) n); 1 < n\<rbrakk> \<Longrightarrow> is_sum2sq_nat n
 2. \<lbrakk>\<forall>m<n. (\<forall>x. prime (4 * x + 3) \<longrightarrow> even (multiplicity (4 * x + 3) m)) \<longrightarrow> is_sum2sq_nat m; \<And>k. prime (4 * k + 3) \<longrightarrow> even (multiplicity (4 * k + 3) n); \<not> 1 < n\<rbrakk> \<Longrightarrow> is_sum2sq_nat n
[PROOF STEP]
case f: False
[PROOF STATE]
proof (state)
this:
\<not> 1 < n

goal (2 subgoals):
 1. \<lbrakk>\<forall>m<n. (\<forall>x. prime (4 * x + 3) \<longrightarrow> even (multiplicity (4 * x + 3) m)) \<longrightarrow> is_sum2sq_nat m; \<And>k. prime (4 * k + 3) \<longrightarrow> even (multiplicity (4 * k + 3) n); 1 < n\<rbrakk> \<Longrightarrow> is_sum2sq_nat n
 2. \<lbrakk>\<forall>m<n. (\<forall>x. prime (4 * x + 3) \<longrightarrow> even (multiplicity (4 * x + 3) m)) \<longrightarrow> is_sum2sq_nat m; \<And>k. prime (4 * k + 3) \<longrightarrow> even (multiplicity (4 * k + 3) n); \<not> 1 < n\<rbrakk> \<Longrightarrow> is_sum2sq_nat n
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> 1 < n

goal (1 subgoal):
 1. is_sum2sq_nat n
[PROOF STEP]
proof (cases "n=1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<not> 1 < n; n = 1\<rbrakk> \<Longrightarrow> is_sum2sq_nat n
 2. \<lbrakk>\<not> 1 < n; n \<noteq> 1\<rbrakk> \<Longrightarrow> is_sum2sq_nat n
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
n = 1

goal (2 subgoals):
 1. \<lbrakk>\<not> 1 < n; n = 1\<rbrakk> \<Longrightarrow> is_sum2sq_nat n
 2. \<lbrakk>\<not> 1 < n; n \<noteq> 1\<rbrakk> \<Longrightarrow> is_sum2sq_nat n
[PROOF STEP]
have "(1::nat)=0^2+1^2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 = 0\<^sup>2 + 1\<^sup>2
[PROOF STEP]
by (simp add: power2_eq_square)
[PROOF STATE]
proof (state)
this:
1 = 0\<^sup>2 + 1\<^sup>2

goal (2 subgoals):
 1. \<lbrakk>\<not> 1 < n; n = 1\<rbrakk> \<Longrightarrow> is_sum2sq_nat n
 2. \<lbrakk>\<not> 1 < n; n \<noteq> 1\<rbrakk> \<Longrightarrow> is_sum2sq_nat n
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
1 = 0\<^sup>2 + 1\<^sup>2

goal (1 subgoal):
 1. is_sum2sq_nat n
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
1 = 0\<^sup>2 + 1\<^sup>2
n = 1

goal (1 subgoal):
 1. is_sum2sq_nat n
[PROOF STEP]
unfolding is_sum2sq_nat_def sum2sq_nat_def
[PROOF STATE]
proof (prove)
using this:
1 = 0\<^sup>2 + 1\<^sup>2
n = 1

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

goal (1 subgoal):
 1. \<lbrakk>\<not> 1 < n; n \<noteq> 1\<rbrakk> \<Longrightarrow> is_sum2sq_nat n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<not> 1 < n; n \<noteq> 1\<rbrakk> \<Longrightarrow> is_sum2sq_nat n
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
n \<noteq> 1

goal (1 subgoal):
 1. \<lbrakk>\<not> 1 < n; n \<noteq> 1\<rbrakk> \<Longrightarrow> is_sum2sq_nat n
[PROOF STEP]
hence "n=0"
[PROOF STATE]
proof (prove)
using this:
n \<noteq> 1

goal (1 subgoal):
 1. n = 0
[PROOF STEP]
using f
[PROOF STATE]
proof (prove)
using this:
n \<noteq> 1
\<not> 1 < n

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

goal (1 subgoal):
 1. \<lbrakk>\<not> 1 < n; n \<noteq> 1\<rbrakk> \<Longrightarrow> is_sum2sq_nat n
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
n = 0

goal (1 subgoal):
 1. \<lbrakk>\<not> 1 < n; n \<noteq> 1\<rbrakk> \<Longrightarrow> is_sum2sq_nat n
[PROOF STEP]
have "(0::nat)=0^2+0^2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 = 0\<^sup>2 + 0\<^sup>2
[PROOF STEP]
by (simp add: power2_eq_square)
[PROOF STATE]
proof (state)
this:
0 = 0\<^sup>2 + 0\<^sup>2

goal (1 subgoal):
 1. \<lbrakk>\<not> 1 < n; n \<noteq> 1\<rbrakk> \<Longrightarrow> is_sum2sq_nat n
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
n = 0
0 = 0\<^sup>2 + 0\<^sup>2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n = 0
0 = 0\<^sup>2 + 0\<^sup>2

goal (1 subgoal):
 1. is_sum2sq_nat n
[PROOF STEP]
unfolding is_sum2sq_nat_def sum2sq_nat_def
[PROOF STATE]
proof (prove)
using this:
n = 0
0 = 0\<^sup>2 + 0\<^sup>2

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

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

goal (1 subgoal):
 1. \<lbrakk>\<forall>m<n. (\<forall>x. prime (4 * x + 3) \<longrightarrow> even (multiplicity (4 * x + 3) m)) \<longrightarrow> is_sum2sq_nat m; \<And>k. prime (4 * k + 3) \<longrightarrow> even (multiplicity (4 * k + 3) n); 1 < n\<rbrakk> \<Longrightarrow> is_sum2sq_nat n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<forall>m<n. (\<forall>x. prime (4 * x + 3) \<longrightarrow> even (multiplicity (4 * x + 3) m)) \<longrightarrow> is_sum2sq_nat m; \<And>k. prime (4 * k + 3) \<longrightarrow> even (multiplicity (4 * k + 3) n); 1 < n\<rbrakk> \<Longrightarrow> is_sum2sq_nat n
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
1 < n

goal (1 subgoal):
 1. \<lbrakk>\<forall>m<n. (\<forall>x. prime (4 * x + 3) \<longrightarrow> even (multiplicity (4 * x + 3) m)) \<longrightarrow> is_sum2sq_nat m; \<And>k. prime (4 * k + 3) \<longrightarrow> even (multiplicity (4 * k + 3) n); 1 < n\<rbrakk> \<Longrightarrow> is_sum2sq_nat n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
1 < n
[PROOF STEP]
obtain p m where h1: "prime p \<and> n = p * m"
[PROOF STATE]
proof (prove)
using this:
1 < n

goal (1 subgoal):
 1. (\<And>p m. prime p \<and> n = p * m \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prime_divisor_exists[of n]
[PROOF STATE]
proof (prove)
using this:
1 < n
\<lbrakk>n \<noteq> 0; \<not> is_unit n\<rbrakk> \<Longrightarrow> \<exists>b. b dvd n \<and> prime b

goal (1 subgoal):
 1. (\<And>p m. prime p \<and> n = p * m \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto elim: dvdE)
[PROOF STATE]
proof (state)
this:
prime p \<and> n = p * m

goal (1 subgoal):
 1. \<lbrakk>\<forall>m<n. (\<forall>x. prime (4 * x + 3) \<longrightarrow> even (multiplicity (4 * x + 3) m)) \<longrightarrow> is_sum2sq_nat m; \<And>k. prime (4 * k + 3) \<longrightarrow> even (multiplicity (4 * k + 3) n); 1 < n\<rbrakk> \<Longrightarrow> is_sum2sq_nat n
[PROOF STEP]
with True
[PROOF STATE]
proof (chain)
picking this:
1 < n
prime p \<and> n = p * m
[PROOF STEP]
have m_nz: "m \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
1 < n
prime p \<and> n = p * m

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

goal (1 subgoal):
 1. \<lbrakk>\<forall>m<n. (\<forall>x. prime (4 * x + 3) \<longrightarrow> even (multiplicity (4 * x + 3) m)) \<longrightarrow> is_sum2sq_nat m; \<And>k. prime (4 * k + 3) \<longrightarrow> even (multiplicity (4 * k + 3) n); 1 < n\<rbrakk> \<Longrightarrow> is_sum2sq_nat n
[PROOF STEP]
from h1
[PROOF STATE]
proof (chain)
picking this:
prime p \<and> n = p * m
[PROOF STEP]
have h2: "m<n"
[PROOF STATE]
proof (prove)
using this:
prime p \<and> n = p * m

goal (1 subgoal):
 1. m < n
[PROOF STEP]
using n_less_m_mult_n[of m p] prime_gt_Suc_0_nat[of p] True
[PROOF STATE]
proof (prove)
using this:
prime p \<and> n = p * m
\<lbrakk>0 < m; Suc 0 < p\<rbrakk> \<Longrightarrow> m < p * m
prime p \<Longrightarrow> Suc 0 < p
1 < n

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

goal (1 subgoal):
 1. \<lbrakk>\<forall>m<n. (\<forall>x. prime (4 * x + 3) \<longrightarrow> even (multiplicity (4 * x + 3) m)) \<longrightarrow> is_sum2sq_nat m; \<And>k. prime (4 * k + 3) \<longrightarrow> even (multiplicity (4 * k + 3) n); 1 < n\<rbrakk> \<Longrightarrow> is_sum2sq_nat n
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
m < n

goal (1 subgoal):
 1. \<lbrakk>\<forall>m<n. (\<forall>x. prime (4 * x + 3) \<longrightarrow> even (multiplicity (4 * x + 3) m)) \<longrightarrow> is_sum2sq_nat m; \<And>k. prime (4 * k + 3) \<longrightarrow> even (multiplicity (4 * k + 3) n); 1 < n\<rbrakk> \<Longrightarrow> is_sum2sq_nat n
[PROOF STEP]
assume a1: "[p = 3] (mod 4)"
[PROOF STATE]
proof (state)
this:
[p = 3] (mod 4)

goal (1 subgoal):
 1. \<lbrakk>\<forall>m<n. (\<forall>x. prime (4 * x + 3) \<longrightarrow> even (multiplicity (4 * x + 3) m)) \<longrightarrow> is_sum2sq_nat m; \<And>k. prime (4 * k + 3) \<longrightarrow> even (multiplicity (4 * k + 3) n); 1 < n\<rbrakk> \<Longrightarrow> is_sum2sq_nat n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[p = 3] (mod 4)
[PROOF STEP]
obtain kp where "p = 4*kp+3"
[PROOF STATE]
proof (prove)
using this:
[p = 3] (mod 4)

goal (1 subgoal):
 1. (\<And>kp. p = 4 * kp + 3 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using aux_lemma
[PROOF STATE]
proof (prove)
using this:
[p = 3] (mod 4)
\<lbrakk>[?a = ?b] (mod ?c); ?b < ?c\<rbrakk> \<Longrightarrow> \<exists>k. ?a = ?c * k + ?b

goal (1 subgoal):
 1. (\<And>kp. p = 4 * kp + 3 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
p = 4 * kp + 3

goal (1 subgoal):
 1. \<lbrakk>\<forall>m<n. (\<forall>x. prime (4 * x + 3) \<longrightarrow> even (multiplicity (4 * x + 3) m)) \<longrightarrow> is_sum2sq_nat m; \<And>k. prime (4 * k + 3) \<longrightarrow> even (multiplicity (4 * k + 3) n); 1 < n\<rbrakk> \<Longrightarrow> is_sum2sq_nat n
[PROOF STEP]
hence "even (multiplicity p n)"
[PROOF STATE]
proof (prove)
using this:
p = 4 * kp + 3

goal (1 subgoal):
 1. even (multiplicity p n)
[PROOF STEP]
using "1.prems" h1
[PROOF STATE]
proof (prove)
using this:
p = 4 * kp + 3
prime (4 * ?k + 3) \<longrightarrow> even (multiplicity (4 * ?k + 3) n)
prime p \<and> n = p * m

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

goal (1 subgoal):
 1. \<lbrakk>\<forall>m<n. (\<forall>x. prime (4 * x + 3) \<longrightarrow> even (multiplicity (4 * x + 3) m)) \<longrightarrow> is_sum2sq_nat m; \<And>k. prime (4 * k + 3) \<longrightarrow> even (multiplicity (4 * k + 3) n); 1 < n\<rbrakk> \<Longrightarrow> is_sum2sq_nat n
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
even (multiplicity p n)

goal (1 subgoal):
 1. \<lbrakk>\<forall>m<n. (\<forall>x. prime (4 * x + 3) \<longrightarrow> even (multiplicity (4 * x + 3) m)) \<longrightarrow> is_sum2sq_nat m; \<And>k. prime (4 * k + 3) \<longrightarrow> even (multiplicity (4 * k + 3) n); 1 < n\<rbrakk> \<Longrightarrow> is_sum2sq_nat n
[PROOF STEP]
have "multiplicity p n \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicity p n \<noteq> 0
[PROOF STEP]
using h1 True m_nz
[PROOF STATE]
proof (prove)
using this:
prime p \<and> n = p * m
1 < n
m \<noteq> 0

goal (1 subgoal):
 1. multiplicity p n \<noteq> 0
[PROOF STEP]
by (subst multiplicity_eq_zero_iff) (auto simp: prime_gt_0_nat)
[PROOF STATE]
proof (state)
this:
multiplicity p n \<noteq> 0

goal (1 subgoal):
 1. \<lbrakk>\<forall>m<n. (\<forall>x. prime (4 * x + 3) \<longrightarrow> even (multiplicity (4 * x + 3) m)) \<longrightarrow> is_sum2sq_nat m; \<And>k. prime (4 * k + 3) \<longrightarrow> even (multiplicity (4 * k + 3) n); 1 < n\<rbrakk> \<Longrightarrow> is_sum2sq_nat n
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
even (multiplicity p n)
multiplicity p n \<noteq> 0
[PROOF STEP]
have h3: "multiplicity p n \<ge> 2"
[PROOF STATE]
proof (prove)
using this:
even (multiplicity p n)
multiplicity p n \<noteq> 0

goal (1 subgoal):
 1. 2 \<le> multiplicity p n
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
2 \<le> multiplicity p n

goal (1 subgoal):
 1. \<lbrakk>\<forall>m<n. (\<forall>x. prime (4 * x + 3) \<longrightarrow> even (multiplicity (4 * x + 3) m)) \<longrightarrow> is_sum2sq_nat m; \<And>k. prime (4 * k + 3) \<longrightarrow> even (multiplicity (4 * k + 3) n); 1 < n\<rbrakk> \<Longrightarrow> is_sum2sq_nat n
[PROOF STEP]
have "p dvd m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p dvd m
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> p dvd m \<Longrightarrow> False
[PROOF STEP]
assume a2: "\<not> p dvd m"
[PROOF STATE]
proof (state)
this:
\<not> p dvd m

goal (1 subgoal):
 1. \<not> p dvd m \<Longrightarrow> False
[PROOF STEP]
hence "multiplicity p m = 0"
[PROOF STATE]
proof (prove)
using this:
\<not> p dvd m

goal (1 subgoal):
 1. multiplicity p m = 0
[PROOF STEP]
by (rule not_dvd_imp_multiplicity_0)
[PROOF STATE]
proof (state)
this:
multiplicity p m = 0

goal (1 subgoal):
 1. \<not> p dvd m \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
multiplicity p m = 0

goal (1 subgoal):
 1. \<not> p dvd m \<Longrightarrow> False
[PROOF STEP]
from h1
[PROOF STATE]
proof (chain)
picking this:
prime p \<and> n = p * m
[PROOF STEP]
have "multiplicity p p = 1"
[PROOF STATE]
proof (prove)
using this:
prime p \<and> n = p * m

goal (1 subgoal):
 1. multiplicity p p = 1
[PROOF STEP]
by (intro multiplicity_prime) auto
[PROOF STATE]
proof (state)
this:
multiplicity p p = 1

goal (1 subgoal):
 1. \<not> p dvd m \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
multiplicity p p = 1

goal (1 subgoal):
 1. \<not> p dvd m \<Longrightarrow> False
[PROOF STEP]
have "m > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < m
[PROOF STEP]
using h1 True
[PROOF STATE]
proof (prove)
using this:
prime p \<and> n = p * m
1 < n

goal (1 subgoal):
 1. 0 < m
[PROOF STEP]
by (cases "m = 0") simp_all
[PROOF STATE]
proof (state)
this:
0 < m

goal (1 subgoal):
 1. \<not> p dvd m \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
multiplicity p m = 0
multiplicity p p = 1
0 < m
[PROOF STEP]
have "multiplicity p n = 1"
[PROOF STATE]
proof (prove)
using this:
multiplicity p m = 0
multiplicity p p = 1
0 < m

goal (1 subgoal):
 1. multiplicity p n = 1
[PROOF STEP]
using h1
[PROOF STATE]
proof (prove)
using this:
multiplicity p m = 0
multiplicity p p = 1
0 < m
prime p \<and> n = p * m

goal (1 subgoal):
 1. multiplicity p n = 1
[PROOF STEP]
using prime_elem_multiplicity_mult_distrib [of p p m] m_nz prime_gt_0_nat
[PROOF STATE]
proof (prove)
using this:
multiplicity p m = 0
multiplicity p p = 1
0 < m
prime p \<and> n = p * m
\<lbrakk>prime_elem p; p \<noteq> 0; m \<noteq> 0\<rbrakk> \<Longrightarrow> multiplicity p (p * m) = multiplicity p p + multiplicity p m
m \<noteq> 0
prime ?p \<Longrightarrow> 0 < ?p

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

goal (1 subgoal):
 1. \<not> p dvd m \<Longrightarrow> False
[PROOF STEP]
thus "False"
[PROOF STATE]
proof (prove)
using this:
multiplicity p n = 1

goal (1 subgoal):
 1. False
[PROOF STEP]
using h3
[PROOF STATE]
proof (prove)
using this:
multiplicity p n = 1
2 \<le> multiplicity p n

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:
p dvd m

goal (1 subgoal):
 1. \<lbrakk>\<forall>m<n. (\<forall>x. prime (4 * x + 3) \<longrightarrow> even (multiplicity (4 * x + 3) m)) \<longrightarrow> is_sum2sq_nat m; \<And>k. prime (4 * k + 3) \<longrightarrow> even (multiplicity (4 * k + 3) n); 1 < n\<rbrakk> \<Longrightarrow> is_sum2sq_nat n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p dvd m
[PROOF STEP]
obtain m' where h4: "m = p * m'"
[PROOF STATE]
proof (prove)
using this:
p dvd m

goal (1 subgoal):
 1. (\<And>m'. m = p * m' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using dvdE
[PROOF STATE]
proof (prove)
using this:
p dvd m
\<lbrakk>?b dvd ?a; \<And>k. ?a = ?b * k \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

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

goal (1 subgoal):
 1. \<lbrakk>\<forall>m<n. (\<forall>x. prime (4 * x + 3) \<longrightarrow> even (multiplicity (4 * x + 3) m)) \<longrightarrow> is_sum2sq_nat m; \<And>k. prime (4 * k + 3) \<longrightarrow> even (multiplicity (4 * k + 3) n); 1 < n\<rbrakk> \<Longrightarrow> is_sum2sq_nat n
[PROOF STEP]
with h1
[PROOF STATE]
proof (chain)
picking this:
prime p \<and> n = p * m
m = p * m'
[PROOF STEP]
have h5: "n = p^2 * m'"
[PROOF STATE]
proof (prove)
using this:
prime p \<and> n = p * m
m = p * m'

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

goal (1 subgoal):
 1. \<lbrakk>\<forall>m<n. (\<forall>x. prime (4 * x + 3) \<longrightarrow> even (multiplicity (4 * x + 3) m)) \<longrightarrow> is_sum2sq_nat m; \<And>k. prime (4 * k + 3) \<longrightarrow> even (multiplicity (4 * k + 3) n); 1 < n\<rbrakk> \<Longrightarrow> is_sum2sq_nat n
[PROOF STEP]
have h6: "m'<n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m' < n
[PROOF STEP]
using dual_order.strict_trans h1 h2 h4 nat_mult_less_cancel1 prime_gt_0_nat[of p]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?b < ?a; ?c < ?b\<rbrakk> \<Longrightarrow> ?c < ?a
prime p \<and> n = p * m
m < n
m = p * m'
0 < ?k \<Longrightarrow> (?k * ?m < ?k * ?n) = (?m < ?n)
prime p \<Longrightarrow> 0 < p

goal (1 subgoal):
 1. m' < n
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
m' < n

goal (1 subgoal):
 1. \<lbrakk>\<forall>m<n. (\<forall>x. prime (4 * x + 3) \<longrightarrow> even (multiplicity (4 * x + 3) m)) \<longrightarrow> is_sum2sq_nat m; \<And>k. prime (4 * k + 3) \<longrightarrow> even (multiplicity (4 * k + 3) n); 1 < n\<rbrakk> \<Longrightarrow> is_sum2sq_nat n
[PROOF STEP]
have "\<And> kq. prime (4*kq + 3) \<Longrightarrow> even (multiplicity (4*kq + 3) m')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>kq. prime (4 * kq + 3) \<Longrightarrow> even (multiplicity (4 * kq + 3) m')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>kq. prime (4 * kq + 3) \<Longrightarrow> even (multiplicity (4 * kq + 3) m')
[PROOF STEP]
fix kq::nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>kq. prime (4 * kq + 3) \<Longrightarrow> even (multiplicity (4 * kq + 3) m')
[PROOF STEP]
let ?q = "4*kq + 3"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>kq. prime (4 * kq + 3) \<Longrightarrow> even (multiplicity (4 * kq + 3) m')
[PROOF STEP]
assume a2: "prime ?q"
[PROOF STATE]
proof (state)
this:
prime (4 * kq + 3)

goal (1 subgoal):
 1. \<And>kq. prime (4 * kq + 3) \<Longrightarrow> even (multiplicity (4 * kq + 3) m')
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
prime (4 * kq + 3)

goal (1 subgoal):
 1. \<And>kq. prime (4 * kq + 3) \<Longrightarrow> even (multiplicity (4 * kq + 3) m')
[PROOF STEP]
assume p: "p=?q"
[PROOF STATE]
proof (state)
this:
p = 4 * kq + 3

goal (1 subgoal):
 1. \<And>kq. prime (4 * kq + 3) \<Longrightarrow> even (multiplicity (4 * kq + 3) m')
[PROOF STEP]
hence h7: "multiplicity ?q (p^2) = 2"
[PROOF STATE]
proof (prove)
using this:
p = 4 * kq + 3

goal (1 subgoal):
 1. multiplicity (4 * kq + 3) (p\<^sup>2) = 2
[PROOF STEP]
using h1
[PROOF STATE]
proof (prove)
using this:
p = 4 * kq + 3
prime p \<and> n = p * m

goal (1 subgoal):
 1. multiplicity (4 * kq + 3) (p\<^sup>2) = 2
[PROOF STEP]
by (auto intro!: multiplicity_prime_power)
[PROOF STATE]
proof (state)
this:
multiplicity (4 * kq + 3) (p\<^sup>2) = 2

goal (1 subgoal):
 1. \<And>kq. prime (4 * kq + 3) \<Longrightarrow> even (multiplicity (4 * kq + 3) m')
[PROOF STEP]
have "even (multiplicity ?q n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. even (multiplicity (4 * kq + 3) n)
[PROOF STEP]
using 1(2)[of kq] a2
[PROOF STATE]
proof (prove)
using this:
prime (4 * kq + 3) \<longrightarrow> even (multiplicity (4 * kq + 3) n)
prime (4 * kq + 3)

goal (1 subgoal):
 1. even (multiplicity (4 * kq + 3) n)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
even (multiplicity (4 * kq + 3) n)

goal (1 subgoal):
 1. \<And>kq. prime (4 * kq + 3) \<Longrightarrow> even (multiplicity (4 * kq + 3) m')
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
even (multiplicity (4 * kq + 3) n)

goal (1 subgoal):
 1. \<And>kq. prime (4 * kq + 3) \<Longrightarrow> even (multiplicity (4 * kq + 3) m')
[PROOF STEP]
note h5
[PROOF STATE]
proof (state)
this:
n = p\<^sup>2 * m'

goal (1 subgoal):
 1. \<And>kq. prime (4 * kq + 3) \<Longrightarrow> even (multiplicity (4 * kq + 3) m')
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
n = p\<^sup>2 * m'

goal (1 subgoal):
 1. \<And>kq. prime (4 * kq + 3) \<Longrightarrow> even (multiplicity (4 * kq + 3) m')
[PROOF STEP]
from p h1 h4 m_nz
[PROOF STATE]
proof (chain)
picking this:
p = 4 * kq + 3
prime p \<and> n = p * m
m = p * m'
m \<noteq> 0
[PROOF STEP]
have "multiplicity (4 * kq + 3) (p^2 * m') =
                    Suc (Suc (multiplicity (4 * kq + 3) m'))"
[PROOF STATE]
proof (prove)
using this:
p = 4 * kq + 3
prime p \<and> n = p * m
m = p * m'
m \<noteq> 0

goal (1 subgoal):
 1. multiplicity (4 * kq + 3) (p\<^sup>2 * m') = Suc (Suc (multiplicity (4 * kq + 3) m'))
[PROOF STEP]
by (subst prime_elem_multiplicity_mult_distrib) auto
[PROOF STATE]
proof (state)
this:
multiplicity (4 * kq + 3) (p\<^sup>2 * m') = Suc (Suc (multiplicity (4 * kq + 3) m'))

goal (1 subgoal):
 1. \<And>kq. prime (4 * kq + 3) \<Longrightarrow> even (multiplicity (4 * kq + 3) m')
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
even (Suc (Suc (multiplicity (4 * kq + 3) m')))
[PROOF STEP]
have "even (multiplicity ?q m')"
[PROOF STATE]
proof (prove)
using this:
even (Suc (Suc (multiplicity (4 * kq + 3) m')))

goal (1 subgoal):
 1. even (multiplicity (4 * kq + 3) m')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
even (multiplicity (4 * kq + 3) m')

goal (1 subgoal):
 1. \<And>kq. prime (4 * kq + 3) \<Longrightarrow> even (multiplicity (4 * kq + 3) m')
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
p = 4 * kq + 3 \<Longrightarrow> even (multiplicity (4 * kq + 3) m')

goal (1 subgoal):
 1. \<And>kq. prime (4 * kq + 3) \<Longrightarrow> even (multiplicity (4 * kq + 3) m')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
p = 4 * kq + 3 \<Longrightarrow> even (multiplicity (4 * kq + 3) m')

goal (1 subgoal):
 1. \<And>kq. prime (4 * kq + 3) \<Longrightarrow> even (multiplicity (4 * kq + 3) m')
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
p = 4 * kq + 3 \<Longrightarrow> even (multiplicity (4 * kq + 3) m')

goal (1 subgoal):
 1. \<And>kq. prime (4 * kq + 3) \<Longrightarrow> even (multiplicity (4 * kq + 3) m')
[PROOF STEP]
assume "p\<noteq>?q"
[PROOF STATE]
proof (state)
this:
p \<noteq> 4 * kq + 3

goal (1 subgoal):
 1. \<And>kq. prime (4 * kq + 3) \<Longrightarrow> even (multiplicity (4 * kq + 3) m')
[PROOF STEP]
from a2 h4 m_nz
[PROOF STATE]
proof (chain)
picking this:
prime (4 * kq + 3)
m = p * m'
m \<noteq> 0
[PROOF STEP]
have "multiplicity ?q n =
                                  multiplicity (4 * kq + 3) (p\<^sup>2) + multiplicity (4 * kq + 3) m'"
[PROOF STATE]
proof (prove)
using this:
prime (4 * kq + 3)
m = p * m'
m \<noteq> 0

goal (1 subgoal):
 1. multiplicity (4 * kq + 3) n = multiplicity (4 * kq + 3) (p\<^sup>2) + multiplicity (4 * kq + 3) m'
[PROOF STEP]
unfolding h5
[PROOF STATE]
proof (prove)
using this:
prime (4 * kq + 3)
m = p * m'
m \<noteq> 0

goal (1 subgoal):
 1. multiplicity (4 * kq + 3) (p\<^sup>2 * m') = multiplicity (4 * kq + 3) (p\<^sup>2) + multiplicity (4 * kq + 3) m'
[PROOF STEP]
by (subst prime_elem_multiplicity_mult_distrib) simp_all
[PROOF STATE]
proof (state)
this:
multiplicity (4 * kq + 3) n = multiplicity (4 * kq + 3) (p\<^sup>2) + multiplicity (4 * kq + 3) m'

goal (1 subgoal):
 1. \<And>kq. prime (4 * kq + 3) \<Longrightarrow> even (multiplicity (4 * kq + 3) m')
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
multiplicity (4 * kq + 3) n = multiplicity (4 * kq + 3) (p\<^sup>2) + multiplicity (4 * kq + 3) m'

goal (1 subgoal):
 1. \<And>kq. prime (4 * kq + 3) \<Longrightarrow> even (multiplicity (4 * kq + 3) m')
[PROOF STEP]
from \<open>p \<noteq> ?q\<close> a2 h1
[PROOF STATE]
proof (chain)
picking this:
p \<noteq> 4 * kq + 3
prime (4 * kq + 3)
prime p \<and> n = p * m
[PROOF STEP]
have "multiplicity ?q (p^2) = 0"
[PROOF STATE]
proof (prove)
using this:
p \<noteq> 4 * kq + 3
prime (4 * kq + 3)
prime p \<and> n = p * m

goal (1 subgoal):
 1. multiplicity (4 * kq + 3) (p\<^sup>2) = 0
[PROOF STEP]
by (intro multiplicity_distinct_prime_power) simp_all
[PROOF STATE]
proof (state)
this:
multiplicity (4 * kq + 3) (p\<^sup>2) = 0

goal (1 subgoal):
 1. \<And>kq. prime (4 * kq + 3) \<Longrightarrow> even (multiplicity (4 * kq + 3) m')
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
multiplicity (4 * kq + 3) n = 0 + multiplicity (4 * kq + 3) m'
[PROOF STEP]
have "multiplicity ?q n = multiplicity ?q m'"
[PROOF STATE]
proof (prove)
using this:
multiplicity (4 * kq + 3) n = 0 + multiplicity (4 * kq + 3) m'

goal (1 subgoal):
 1. multiplicity (4 * kq + 3) n = multiplicity (4 * kq + 3) m'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
multiplicity (4 * kq + 3) n = multiplicity (4 * kq + 3) m'

goal (1 subgoal):
 1. \<And>kq. prime (4 * kq + 3) \<Longrightarrow> even (multiplicity (4 * kq + 3) m')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
multiplicity (4 * kq + 3) n = multiplicity (4 * kq + 3) m'

goal (1 subgoal):
 1. \<And>kq. prime (4 * kq + 3) \<Longrightarrow> even (multiplicity (4 * kq + 3) m')
[PROOF STEP]
have "even (multiplicity ?q n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. even (multiplicity (4 * kq + 3) n)
[PROOF STEP]
using 1(2)[of kq] a2
[PROOF STATE]
proof (prove)
using this:
prime (4 * kq + 3) \<longrightarrow> even (multiplicity (4 * kq + 3) n)
prime (4 * kq + 3)

goal (1 subgoal):
 1. even (multiplicity (4 * kq + 3) n)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
even (multiplicity (4 * kq + 3) n)

goal (1 subgoal):
 1. \<And>kq. prime (4 * kq + 3) \<Longrightarrow> even (multiplicity (4 * kq + 3) m')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
multiplicity (4 * kq + 3) n = multiplicity (4 * kq + 3) m'
even (multiplicity (4 * kq + 3) n)
[PROOF STEP]
have "even (multiplicity ?q m')"
[PROOF STATE]
proof (prove)
using this:
multiplicity (4 * kq + 3) n = multiplicity (4 * kq + 3) m'
even (multiplicity (4 * kq + 3) n)

goal (1 subgoal):
 1. even (multiplicity (4 * kq + 3) m')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
even (multiplicity (4 * kq + 3) m')

goal (1 subgoal):
 1. \<And>kq. prime (4 * kq + 3) \<Longrightarrow> even (multiplicity (4 * kq + 3) m')
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
p \<noteq> 4 * kq + 3 \<Longrightarrow> even (multiplicity (4 * kq + 3) m')

goal (1 subgoal):
 1. \<And>kq. prime (4 * kq + 3) \<Longrightarrow> even (multiplicity (4 * kq + 3) m')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
p = 4 * kq + 3 \<Longrightarrow> even (multiplicity (4 * kq + 3) m')
p \<noteq> 4 * kq + 3 \<Longrightarrow> even (multiplicity (4 * kq + 3) m')
[PROOF STEP]
show "even (multiplicity ?q m')"
[PROOF STATE]
proof (prove)
using this:
p = 4 * kq + 3 \<Longrightarrow> even (multiplicity (4 * kq + 3) m')
p \<noteq> 4 * kq + 3 \<Longrightarrow> even (multiplicity (4 * kq + 3) m')

goal (1 subgoal):
 1. even (multiplicity (4 * kq + 3) m')
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
even (multiplicity (4 * kq + 3) m')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
prime (4 * ?kq + 3) \<Longrightarrow> even (multiplicity (4 * ?kq + 3) m')

goal (1 subgoal):
 1. \<lbrakk>\<forall>m<n. (\<forall>x. prime (4 * x + 3) \<longrightarrow> even (multiplicity (4 * x + 3) m)) \<longrightarrow> is_sum2sq_nat m; \<And>k. prime (4 * k + 3) \<longrightarrow> even (multiplicity (4 * k + 3) n); 1 < n\<rbrakk> \<Longrightarrow> is_sum2sq_nat n
[PROOF STEP]
hence "is_sum2sq_nat m'"
[PROOF STATE]
proof (prove)
using this:
prime (4 * ?kq + 3) \<Longrightarrow> even (multiplicity (4 * ?kq + 3) m')

goal (1 subgoal):
 1. is_sum2sq_nat m'
[PROOF STEP]
by (simp add: 1 h6)
[PROOF STATE]
proof (state)
this:
is_sum2sq_nat m'

goal (1 subgoal):
 1. \<lbrakk>\<forall>m<n. (\<forall>x. prime (4 * x + 3) \<longrightarrow> even (multiplicity (4 * x + 3) m)) \<longrightarrow> is_sum2sq_nat m; \<And>k. prime (4 * k + 3) \<longrightarrow> even (multiplicity (4 * k + 3) n); 1 < n\<rbrakk> \<Longrightarrow> is_sum2sq_nat n
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_sum2sq_nat m'

goal (1 subgoal):
 1. \<lbrakk>\<forall>m<n. (\<forall>x. prime (4 * x + 3) \<longrightarrow> even (multiplicity (4 * x + 3) m)) \<longrightarrow> is_sum2sq_nat m; \<And>k. prime (4 * k + 3) \<longrightarrow> even (multiplicity (4 * k + 3) n); 1 < n\<rbrakk> \<Longrightarrow> is_sum2sq_nat n
[PROOF STEP]
have "p^2 = p^2 + 0^2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p\<^sup>2 = p\<^sup>2 + 0\<^sup>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
p\<^sup>2 = p\<^sup>2 + 0\<^sup>2

goal (1 subgoal):
 1. \<lbrakk>\<forall>m<n. (\<forall>x. prime (4 * x + 3) \<longrightarrow> even (multiplicity (4 * x + 3) m)) \<longrightarrow> is_sum2sq_nat m; \<And>k. prime (4 * k + 3) \<longrightarrow> even (multiplicity (4 * k + 3) n); 1 < n\<rbrakk> \<Longrightarrow> is_sum2sq_nat n
[PROOF STEP]
hence "is_sum2sq_nat (p^2)"
[PROOF STATE]
proof (prove)
using this:
p\<^sup>2 = p\<^sup>2 + 0\<^sup>2

goal (1 subgoal):
 1. is_sum2sq_nat (p\<^sup>2)
[PROOF STEP]
unfolding is_sum2sq_nat_def sum2sq_nat_def
[PROOF STATE]
proof (prove)
using this:
p\<^sup>2 = p\<^sup>2 + 0\<^sup>2

goal (1 subgoal):
 1. \<exists>a b. p\<^sup>2 = a\<^sup>2 + b\<^sup>2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_sum2sq_nat (p\<^sup>2)

goal (1 subgoal):
 1. \<lbrakk>\<forall>m<n. (\<forall>x. prime (4 * x + 3) \<longrightarrow> even (multiplicity (4 * x + 3) m)) \<longrightarrow> is_sum2sq_nat m; \<And>k. prime (4 * k + 3) \<longrightarrow> even (multiplicity (4 * k + 3) n); 1 < n\<rbrakk> \<Longrightarrow> is_sum2sq_nat n
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
is_sum2sq_nat m'
is_sum2sq_nat (p\<^sup>2)
[PROOF STEP]
have ?thesis
[PROOF STATE]
proof (prove)
using this:
is_sum2sq_nat m'
is_sum2sq_nat (p\<^sup>2)

goal (1 subgoal):
 1. is_sum2sq_nat n
[PROOF STEP]
using product_two_squares_nat h5
[PROOF STATE]
proof (prove)
using this:
is_sum2sq_nat m'
is_sum2sq_nat (p\<^sup>2)
\<lbrakk>is_sum2sq_nat ?m; is_sum2sq_nat ?n\<rbrakk> \<Longrightarrow> is_sum2sq_nat (?m * ?n)
n = p\<^sup>2 * m'

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

goal (1 subgoal):
 1. \<lbrakk>\<forall>m<n. (\<forall>x. prime (4 * x + 3) \<longrightarrow> even (multiplicity (4 * x + 3) m)) \<longrightarrow> is_sum2sq_nat m; \<And>k. prime (4 * k + 3) \<longrightarrow> even (multiplicity (4 * k + 3) n); 1 < n\<rbrakk> \<Longrightarrow> is_sum2sq_nat n
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
[p = 3] (mod 4) \<Longrightarrow> is_sum2sq_nat n

goal (1 subgoal):
 1. \<lbrakk>\<forall>m<n. (\<forall>x. prime (4 * x + 3) \<longrightarrow> even (multiplicity (4 * x + 3) m)) \<longrightarrow> is_sum2sq_nat m; \<And>k. prime (4 * k + 3) \<longrightarrow> even (multiplicity (4 * k + 3) n); 1 < n\<rbrakk> \<Longrightarrow> is_sum2sq_nat n
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
[p = 3] (mod 4) \<Longrightarrow> is_sum2sq_nat n

goal (1 subgoal):
 1. \<lbrakk>\<forall>m<n. (\<forall>x. prime (4 * x + 3) \<longrightarrow> even (multiplicity (4 * x + 3) m)) \<longrightarrow> is_sum2sq_nat m; \<And>k. prime (4 * k + 3) \<longrightarrow> even (multiplicity (4 * k + 3) n); 1 < n\<rbrakk> \<Longrightarrow> is_sum2sq_nat n
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
[p = 3] (mod 4) \<Longrightarrow> is_sum2sq_nat n

goal (1 subgoal):
 1. \<lbrakk>\<forall>m<n. (\<forall>x. prime (4 * x + 3) \<longrightarrow> even (multiplicity (4 * x + 3) m)) \<longrightarrow> is_sum2sq_nat m; \<And>k. prime (4 * k + 3) \<longrightarrow> even (multiplicity (4 * k + 3) n); 1 < n\<rbrakk> \<Longrightarrow> is_sum2sq_nat n
[PROOF STEP]
assume a1: "\<not> [p = 3] (mod 4)"
[PROOF STATE]
proof (state)
this:
[p \<noteq> 3] (mod 4)

goal (1 subgoal):
 1. \<lbrakk>\<forall>m<n. (\<forall>x. prime (4 * x + 3) \<longrightarrow> even (multiplicity (4 * x + 3) m)) \<longrightarrow> is_sum2sq_nat m; \<And>k. prime (4 * k + 3) \<longrightarrow> even (multiplicity (4 * k + 3) n); 1 < n\<rbrakk> \<Longrightarrow> is_sum2sq_nat n
[PROOF STEP]
have "\<And> kq. prime (4*kq+3) \<Longrightarrow> even (multiplicity (4*kq+3) m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>kq. prime (4 * kq + 3) \<Longrightarrow> even (multiplicity (4 * kq + 3) m)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>kq. prime (4 * kq + 3) \<Longrightarrow> even (multiplicity (4 * kq + 3) m)
[PROOF STEP]
fix kq
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>kq. prime (4 * kq + 3) \<Longrightarrow> even (multiplicity (4 * kq + 3) m)
[PROOF STEP]
let ?q = "4*(kq::nat) + 3"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>kq. prime (4 * kq + 3) \<Longrightarrow> even (multiplicity (4 * kq + 3) m)
[PROOF STEP]
assume a2: "prime ?q"
[PROOF STATE]
proof (state)
this:
prime (4 * kq + 3)

goal (1 subgoal):
 1. \<And>kq. prime (4 * kq + 3) \<Longrightarrow> even (multiplicity (4 * kq + 3) m)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
prime (4 * kq + 3)

goal (1 subgoal):
 1. \<And>kq. prime (4 * kq + 3) \<Longrightarrow> even (multiplicity (4 * kq + 3) m)
[PROOF STEP]
assume "p = ?q"
[PROOF STATE]
proof (state)
this:
p = 4 * kq + 3

goal (1 subgoal):
 1. \<And>kq. prime (4 * kq + 3) \<Longrightarrow> even (multiplicity (4 * kq + 3) m)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p = 4 * kq + 3
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
p = 4 * kq + 3

goal (1 subgoal):
 1. False
[PROOF STEP]
using a1 cong_add_rcancel_0_nat [of "4 * kq" 3 4]
[PROOF STATE]
proof (prove)
using this:
p = 4 * kq + 3
[p \<noteq> 3] (mod 4)
[4 * kq + 3 = 3] (mod 4) = [4 * kq = 0] (mod 4)

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

goal (1 subgoal):
 1. \<And>kq. prime (4 * kq + 3) \<Longrightarrow> even (multiplicity (4 * kq + 3) m)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
p = 4 * kq + 3 \<Longrightarrow> False

goal (1 subgoal):
 1. \<And>kq. prime (4 * kq + 3) \<Longrightarrow> even (multiplicity (4 * kq + 3) m)
[PROOF STEP]
hence "p\<noteq>?q"
[PROOF STATE]
proof (prove)
using this:
p = 4 * kq + 3 \<Longrightarrow> False

goal (1 subgoal):
 1. p \<noteq> 4 * kq + 3
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
p \<noteq> 4 * kq + 3

goal (1 subgoal):
 1. \<And>kq. prime (4 * kq + 3) \<Longrightarrow> even (multiplicity (4 * kq + 3) m)
[PROOF STEP]
have "n = p * m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n = p * m
[PROOF STEP]
using h1
[PROOF STATE]
proof (prove)
using this:
prime p \<and> n = p * m

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

goal (1 subgoal):
 1. \<And>kq. prime (4 * kq + 3) \<Longrightarrow> even (multiplicity (4 * kq + 3) m)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
n = p * m

goal (1 subgoal):
 1. \<And>kq. prime (4 * kq + 3) \<Longrightarrow> even (multiplicity (4 * kq + 3) m)
[PROOF STEP]
from h1 a2 m_nz
[PROOF STATE]
proof (chain)
picking this:
prime p \<and> n = p * m
prime (4 * kq + 3)
m \<noteq> 0
[PROOF STEP]
have "multiplicity ?q \<dots> =
                                  multiplicity (4 * kq + 3) p + multiplicity (4 * kq + 3) m"
[PROOF STATE]
proof (prove)
using this:
prime p \<and> n = p * m
prime (4 * kq + 3)
m \<noteq> 0

goal (1 subgoal):
 1. multiplicity (4 * kq + 3) (p * m) = multiplicity (4 * kq + 3) p + multiplicity (4 * kq + 3) m
[PROOF STEP]
by (subst prime_elem_multiplicity_mult_distrib) (simp_all add: prime_gt_0_nat)
[PROOF STATE]
proof (state)
this:
multiplicity (4 * kq + 3) (p * m) = multiplicity (4 * kq + 3) p + multiplicity (4 * kq + 3) m

goal (1 subgoal):
 1. \<And>kq. prime (4 * kq + 3) \<Longrightarrow> even (multiplicity (4 * kq + 3) m)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
multiplicity (4 * kq + 3) (p * m) = multiplicity (4 * kq + 3) p + multiplicity (4 * kq + 3) m

goal (1 subgoal):
 1. \<And>kq. prime (4 * kq + 3) \<Longrightarrow> even (multiplicity (4 * kq + 3) m)
[PROOF STEP]
from \<open>p \<noteq> ?q\<close> a2 h1
[PROOF STATE]
proof (chain)
picking this:
p \<noteq> 4 * kq + 3
prime (4 * kq + 3)
prime p \<and> n = p * m
[PROOF STEP]
have "multiplicity ?q p = 0"
[PROOF STATE]
proof (prove)
using this:
p \<noteq> 4 * kq + 3
prime (4 * kq + 3)
prime p \<and> n = p * m

goal (1 subgoal):
 1. multiplicity (4 * kq + 3) p = 0
[PROOF STEP]
by (intro prime_multiplicity_other) simp_all
[PROOF STATE]
proof (state)
this:
multiplicity (4 * kq + 3) p = 0

goal (1 subgoal):
 1. \<And>kq. prime (4 * kq + 3) \<Longrightarrow> even (multiplicity (4 * kq + 3) m)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
multiplicity (4 * kq + 3) n = 0 + multiplicity (4 * kq + 3) m
[PROOF STEP]
have "multiplicity ?q n = multiplicity ?q m"
[PROOF STATE]
proof (prove)
using this:
multiplicity (4 * kq + 3) n = 0 + multiplicity (4 * kq + 3) m

goal (1 subgoal):
 1. multiplicity (4 * kq + 3) n = multiplicity (4 * kq + 3) m
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
multiplicity (4 * kq + 3) n = multiplicity (4 * kq + 3) m

goal (1 subgoal):
 1. \<And>kq. prime (4 * kq + 3) \<Longrightarrow> even (multiplicity (4 * kq + 3) m)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
multiplicity (4 * kq + 3) n = multiplicity (4 * kq + 3) m

goal (1 subgoal):
 1. \<And>kq. prime (4 * kq + 3) \<Longrightarrow> even (multiplicity (4 * kq + 3) m)
[PROOF STEP]
have "even (multiplicity ?q n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. even (multiplicity (4 * kq + 3) n)
[PROOF STEP]
using 1(2)[of kq] a2
[PROOF STATE]
proof (prove)
using this:
prime (4 * kq + 3) \<longrightarrow> even (multiplicity (4 * kq + 3) n)
prime (4 * kq + 3)

goal (1 subgoal):
 1. even (multiplicity (4 * kq + 3) n)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
even (multiplicity (4 * kq + 3) n)

goal (1 subgoal):
 1. \<And>kq. prime (4 * kq + 3) \<Longrightarrow> even (multiplicity (4 * kq + 3) m)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
multiplicity (4 * kq + 3) n = multiplicity (4 * kq + 3) m
even (multiplicity (4 * kq + 3) n)
[PROOF STEP]
show "even (multiplicity ?q m)"
[PROOF STATE]
proof (prove)
using this:
multiplicity (4 * kq + 3) n = multiplicity (4 * kq + 3) m
even (multiplicity (4 * kq + 3) n)

goal (1 subgoal):
 1. even (multiplicity (4 * kq + 3) m)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
even (multiplicity (4 * kq + 3) m)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
prime (4 * ?kq + 3) \<Longrightarrow> even (multiplicity (4 * ?kq + 3) m)

goal (1 subgoal):
 1. \<lbrakk>\<forall>m<n. (\<forall>x. prime (4 * x + 3) \<longrightarrow> even (multiplicity (4 * x + 3) m)) \<longrightarrow> is_sum2sq_nat m; \<And>k. prime (4 * k + 3) \<longrightarrow> even (multiplicity (4 * k + 3) n); 1 < n\<rbrakk> \<Longrightarrow> is_sum2sq_nat n
[PROOF STEP]
hence "is_sum2sq_nat m"
[PROOF STATE]
proof (prove)
using this:
prime (4 * ?kq + 3) \<Longrightarrow> even (multiplicity (4 * ?kq + 3) m)

goal (1 subgoal):
 1. is_sum2sq_nat m
[PROOF STEP]
by (simp add: 1 h2)
[PROOF STATE]
proof (state)
this:
is_sum2sq_nat m

goal (1 subgoal):
 1. \<lbrakk>\<forall>m<n. (\<forall>x. prime (4 * x + 3) \<longrightarrow> even (multiplicity (4 * x + 3) m)) \<longrightarrow> is_sum2sq_nat m; \<And>k. prime (4 * k + 3) \<longrightarrow> even (multiplicity (4 * k + 3) n); 1 < n\<rbrakk> \<Longrightarrow> is_sum2sq_nat n
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_sum2sq_nat m

goal (1 subgoal):
 1. \<lbrakk>\<forall>m<n. (\<forall>x. prime (4 * x + 3) \<longrightarrow> even (multiplicity (4 * x + 3) m)) \<longrightarrow> is_sum2sq_nat m; \<And>k. prime (4 * k + 3) \<longrightarrow> even (multiplicity (4 * k + 3) n); 1 < n\<rbrakk> \<Longrightarrow> is_sum2sq_nat n
[PROOF STEP]
have "is_sum2sq_nat p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_sum2sq_nat p
[PROOF STEP]
using fermat_two_squares a1 h1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>prime ?p; [?p \<noteq> 3] (mod 4)\<rbrakk> \<Longrightarrow> is_sum2sq_nat ?p
[p \<noteq> 3] (mod 4)
prime p \<and> n = p * m

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

goal (1 subgoal):
 1. \<lbrakk>\<forall>m<n. (\<forall>x. prime (4 * x + 3) \<longrightarrow> even (multiplicity (4 * x + 3) m)) \<longrightarrow> is_sum2sq_nat m; \<And>k. prime (4 * k + 3) \<longrightarrow> even (multiplicity (4 * k + 3) n); 1 < n\<rbrakk> \<Longrightarrow> is_sum2sq_nat n
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
is_sum2sq_nat m
is_sum2sq_nat p
[PROOF STEP]
have ?thesis
[PROOF STATE]
proof (prove)
using this:
is_sum2sq_nat m
is_sum2sq_nat p

goal (1 subgoal):
 1. is_sum2sq_nat n
[PROOF STEP]
using product_two_squares_nat h1
[PROOF STATE]
proof (prove)
using this:
is_sum2sq_nat m
is_sum2sq_nat p
\<lbrakk>is_sum2sq_nat ?m; is_sum2sq_nat ?n\<rbrakk> \<Longrightarrow> is_sum2sq_nat (?m * ?n)
prime p \<and> n = p * m

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

goal (1 subgoal):
 1. \<lbrakk>\<forall>m<n. (\<forall>x. prime (4 * x + 3) \<longrightarrow> even (multiplicity (4 * x + 3) m)) \<longrightarrow> is_sum2sq_nat m; \<And>k. prime (4 * k + 3) \<longrightarrow> even (multiplicity (4 * k + 3) n); 1 < n\<rbrakk> \<Longrightarrow> is_sum2sq_nat n
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
[p \<noteq> 3] (mod 4) \<Longrightarrow> is_sum2sq_nat n

goal (1 subgoal):
 1. \<lbrakk>\<forall>m<n. (\<forall>x. prime (4 * x + 3) \<longrightarrow> even (multiplicity (4 * x + 3) m)) \<longrightarrow> is_sum2sq_nat m; \<And>k. prime (4 * k + 3) \<longrightarrow> even (multiplicity (4 * k + 3) n); 1 < n\<rbrakk> \<Longrightarrow> is_sum2sq_nat n
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
[p = 3] (mod 4) \<Longrightarrow> is_sum2sq_nat n
[p \<noteq> 3] (mod 4) \<Longrightarrow> is_sum2sq_nat n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
[p = 3] (mod 4) \<Longrightarrow> is_sum2sq_nat n
[p \<noteq> 3] (mod 4) \<Longrightarrow> is_sum2sq_nat n

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem sum_of_two_squares:
    "is_sum2sq_nat n \<longleftrightarrow> (\<forall> k. prime (4*k+3) \<longrightarrow> even (multiplicity (4*k+3) n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_sum2sq_nat n = (\<forall>k. prime (4 * k + 3) \<longrightarrow> even (multiplicity (4 * k + 3) n))
[PROOF STEP]
using sots1[of n] sots2[of n]
[PROOF STATE]
proof (prove)
using this:
is_sum2sq_nat n \<Longrightarrow> prime (4 * ?k + 3) \<longrightarrow> even (multiplicity (4 * ?k + 3) n)
(\<And>k. prime (4 * k + 3) \<longrightarrow> even (multiplicity (4 * k + 3) n)) \<Longrightarrow> is_sum2sq_nat n

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


[STATEMENT]
lemma k_mod_eq: "(\<forall>p::nat. prime p \<and> [p = 3] (mod 4) \<longrightarrow> P p) = (\<forall>k. prime (4*k+3) \<longrightarrow> P (4*k+3))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>p. prime p \<and> [p = 3] (mod 4) \<longrightarrow> P p) = (\<forall>k. prime (4 * k + 3) \<longrightarrow> P (4 * k + 3))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>p. prime p \<and> [p = 3] (mod 4) \<longrightarrow> P p \<Longrightarrow> \<forall>k. prime (4 * k + 3) \<longrightarrow> P (4 * k + 3)
 2. \<forall>k. prime (4 * k + 3) \<longrightarrow> P (4 * k + 3) \<Longrightarrow> \<forall>p. prime p \<and> [p = 3] (mod 4) \<longrightarrow> P p
[PROOF STEP]
assume a1: "\<forall>p. prime p \<and> [p = 3] (mod 4) \<longrightarrow> P p"
[PROOF STATE]
proof (state)
this:
\<forall>p. prime p \<and> [p = 3] (mod 4) \<longrightarrow> P p

goal (2 subgoals):
 1. \<forall>p. prime p \<and> [p = 3] (mod 4) \<longrightarrow> P p \<Longrightarrow> \<forall>k. prime (4 * k + 3) \<longrightarrow> P (4 * k + 3)
 2. \<forall>k. prime (4 * k + 3) \<longrightarrow> P (4 * k + 3) \<Longrightarrow> \<forall>p. prime p \<and> [p = 3] (mod 4) \<longrightarrow> P p
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<forall>p. prime p \<and> [p = 3] (mod 4) \<longrightarrow> P p

goal (2 subgoals):
 1. \<forall>p. prime p \<and> [p = 3] (mod 4) \<longrightarrow> P p \<Longrightarrow> \<forall>k. prime (4 * k + 3) \<longrightarrow> P (4 * k + 3)
 2. \<forall>k. prime (4 * k + 3) \<longrightarrow> P (4 * k + 3) \<Longrightarrow> \<forall>p. prime p \<and> [p = 3] (mod 4) \<longrightarrow> P p
[PROOF STEP]
fix k :: nat
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>p. prime p \<and> [p = 3] (mod 4) \<longrightarrow> P p \<Longrightarrow> \<forall>k. prime (4 * k + 3) \<longrightarrow> P (4 * k + 3)
 2. \<forall>k. prime (4 * k + 3) \<longrightarrow> P (4 * k + 3) \<Longrightarrow> \<forall>p. prime p \<and> [p = 3] (mod 4) \<longrightarrow> P p
[PROOF STEP]
assume "prime (4 * k + 3)"
[PROOF STATE]
proof (state)
this:
prime (4 * k + 3)

goal (2 subgoals):
 1. \<forall>p. prime p \<and> [p = 3] (mod 4) \<longrightarrow> P p \<Longrightarrow> \<forall>k. prime (4 * k + 3) \<longrightarrow> P (4 * k + 3)
 2. \<forall>k. prime (4 * k + 3) \<longrightarrow> P (4 * k + 3) \<Longrightarrow> \<forall>p. prime p \<and> [p = 3] (mod 4) \<longrightarrow> P p
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
prime (4 * k + 3)

goal (2 subgoals):
 1. \<forall>p. prime p \<and> [p = 3] (mod 4) \<longrightarrow> P p \<Longrightarrow> \<forall>k. prime (4 * k + 3) \<longrightarrow> P (4 * k + 3)
 2. \<forall>k. prime (4 * k + 3) \<longrightarrow> P (4 * k + 3) \<Longrightarrow> \<forall>p. prime p \<and> [p = 3] (mod 4) \<longrightarrow> P p
[PROOF STEP]
hence "[4*k+3 = 3] (mod 4)"
[PROOF STATE]
proof (prove)
using this:
prime (4 * k + 3)

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

goal (2 subgoals):
 1. \<forall>p. prime p \<and> [p = 3] (mod 4) \<longrightarrow> P p \<Longrightarrow> \<forall>k. prime (4 * k + 3) \<longrightarrow> P (4 * k + 3)
 2. \<forall>k. prime (4 * k + 3) \<longrightarrow> P (4 * k + 3) \<Longrightarrow> \<forall>p. prime p \<and> [p = 3] (mod 4) \<longrightarrow> P p
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
prime (4 * k + 3)
[4 * k + 3 = 3] (mod 4)
[PROOF STEP]
have "P (4 * k + 3)"
[PROOF STATE]
proof (prove)
using this:
prime (4 * k + 3)
[4 * k + 3 = 3] (mod 4)

goal (1 subgoal):
 1. P (4 * k + 3)
[PROOF STEP]
using a1
[PROOF STATE]
proof (prove)
using this:
prime (4 * k + 3)
[4 * k + 3 = 3] (mod 4)
\<forall>p. prime p \<and> [p = 3] (mod 4) \<longrightarrow> P p

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

goal (2 subgoals):
 1. \<forall>p. prime p \<and> [p = 3] (mod 4) \<longrightarrow> P p \<Longrightarrow> \<forall>k. prime (4 * k + 3) \<longrightarrow> P (4 * k + 3)
 2. \<forall>k. prime (4 * k + 3) \<longrightarrow> P (4 * k + 3) \<Longrightarrow> \<forall>p. prime p \<and> [p = 3] (mod 4) \<longrightarrow> P p
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
prime (4 * ?k2 + 3) \<Longrightarrow> P (4 * ?k2 + 3)

goal (2 subgoals):
 1. \<forall>p. prime p \<and> [p = 3] (mod 4) \<longrightarrow> P p \<Longrightarrow> \<forall>k. prime (4 * k + 3) \<longrightarrow> P (4 * k + 3)
 2. \<forall>k. prime (4 * k + 3) \<longrightarrow> P (4 * k + 3) \<Longrightarrow> \<forall>p. prime p \<and> [p = 3] (mod 4) \<longrightarrow> P p
[PROOF STEP]
thus "\<forall>k. prime (4 * k + 3) \<longrightarrow> P (4 * k + 3)"
[PROOF STATE]
proof (prove)
using this:
prime (4 * ?k2 + 3) \<Longrightarrow> P (4 * ?k2 + 3)

goal (1 subgoal):
 1. \<forall>k. prime (4 * k + 3) \<longrightarrow> P (4 * k + 3)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>k. prime (4 * k + 3) \<longrightarrow> P (4 * k + 3)

goal (1 subgoal):
 1. \<forall>k. prime (4 * k + 3) \<longrightarrow> P (4 * k + 3) \<Longrightarrow> \<forall>p. prime p \<and> [p = 3] (mod 4) \<longrightarrow> P p
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>k. prime (4 * k + 3) \<longrightarrow> P (4 * k + 3) \<Longrightarrow> \<forall>p. prime p \<and> [p = 3] (mod 4) \<longrightarrow> P p
[PROOF STEP]
assume a1: "\<forall>k. prime (4 * k + 3) \<longrightarrow> P (4 * k + 3)"
[PROOF STATE]
proof (state)
this:
\<forall>k. prime (4 * k + 3) \<longrightarrow> P (4 * k + 3)

goal (1 subgoal):
 1. \<forall>k. prime (4 * k + 3) \<longrightarrow> P (4 * k + 3) \<Longrightarrow> \<forall>p. prime p \<and> [p = 3] (mod 4) \<longrightarrow> P p
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<forall>k. prime (4 * k + 3) \<longrightarrow> P (4 * k + 3)

goal (1 subgoal):
 1. \<forall>k. prime (4 * k + 3) \<longrightarrow> P (4 * k + 3) \<Longrightarrow> \<forall>p. prime p \<and> [p = 3] (mod 4) \<longrightarrow> P p
[PROOF STEP]
fix p :: nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>k. prime (4 * k + 3) \<longrightarrow> P (4 * k + 3) \<Longrightarrow> \<forall>p. prime p \<and> [p = 3] (mod 4) \<longrightarrow> P p
[PROOF STEP]
assume "prime p" "[p = 3] (mod 4)"
[PROOF STATE]
proof (state)
this:
prime p
[p = 3] (mod 4)

goal (1 subgoal):
 1. \<forall>k. prime (4 * k + 3) \<longrightarrow> P (4 * k + 3) \<Longrightarrow> \<forall>p. prime p \<and> [p = 3] (mod 4) \<longrightarrow> P p
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
prime p
[p = 3] (mod 4)

goal (1 subgoal):
 1. \<forall>k. prime (4 * k + 3) \<longrightarrow> P (4 * k + 3) \<Longrightarrow> \<forall>p. prime p \<and> [p = 3] (mod 4) \<longrightarrow> P p
[PROOF STEP]
with aux_lemma
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>[?a = ?b] (mod ?c); ?b < ?c\<rbrakk> \<Longrightarrow> \<exists>k. ?a = ?c * k + ?b
prime p
[p = 3] (mod 4)
[PROOF STEP]
obtain k where "p = 4*k+3"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>[?a = ?b] (mod ?c); ?b < ?c\<rbrakk> \<Longrightarrow> \<exists>k. ?a = ?c * k + ?b
prime p
[p = 3] (mod 4)

goal (1 subgoal):
 1. (\<And>k. p = 4 * k + 3 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
p = 4 * k + 3

goal (1 subgoal):
 1. \<forall>k. prime (4 * k + 3) \<longrightarrow> P (4 * k + 3) \<Longrightarrow> \<forall>p. prime p \<and> [p = 3] (mod 4) \<longrightarrow> P p
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
prime p
[p = 3] (mod 4)
p = 4 * k + 3
[PROOF STEP]
have "P p"
[PROOF STATE]
proof (prove)
using this:
prime p
[p = 3] (mod 4)
p = 4 * k + 3

goal (1 subgoal):
 1. P p
[PROOF STEP]
using a1
[PROOF STATE]
proof (prove)
using this:
prime p
[p = 3] (mod 4)
p = 4 * k + 3
\<forall>k. prime (4 * k + 3) \<longrightarrow> P (4 * k + 3)

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

goal (1 subgoal):
 1. \<forall>k. prime (4 * k + 3) \<longrightarrow> P (4 * k + 3) \<Longrightarrow> \<forall>p. prime p \<and> [p = 3] (mod 4) \<longrightarrow> P p
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>prime ?p2; [?p2 = 3] (mod 4)\<rbrakk> \<Longrightarrow> P ?p2

goal (1 subgoal):
 1. \<forall>k. prime (4 * k + 3) \<longrightarrow> P (4 * k + 3) \<Longrightarrow> \<forall>p. prime p \<and> [p = 3] (mod 4) \<longrightarrow> P p
[PROOF STEP]
thus "\<forall>p. prime p \<and> [p = 3] (mod 4) \<longrightarrow> P p"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>prime ?p2; [?p2 = 3] (mod 4)\<rbrakk> \<Longrightarrow> P ?p2

goal (1 subgoal):
 1. \<forall>p. prime p \<and> [p = 3] (mod 4) \<longrightarrow> P p
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>p. prime p \<and> [p = 3] (mod 4) \<longrightarrow> P p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem sum_of_two_squares':
    "is_sum2sq_nat n \<longleftrightarrow> (\<forall> p. prime p \<and> [p = 3] (mod 4) \<longrightarrow> even (multiplicity p n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_sum2sq_nat n = (\<forall>p. prime p \<and> [p = 3] (mod 4) \<longrightarrow> even (multiplicity p n))
[PROOF STEP]
using sum_of_two_squares k_mod_eq
[PROOF STATE]
proof (prove)
using this:
is_sum2sq_nat ?n = (\<forall>k. prime (4 * k + 3) \<longrightarrow> even (multiplicity (4 * k + 3) ?n))
(\<forall>p. prime p \<and> [p = 3] (mod 4) \<longrightarrow> ?P p) = (\<forall>k. prime (4 * k + 3) \<longrightarrow> ?P (4 * k + 3))

goal (1 subgoal):
 1. is_sum2sq_nat n = (\<forall>p. prime p \<and> [p = 3] (mod 4) \<longrightarrow> even (multiplicity p n))
[PROOF STEP]
by presburger


[STATEMENT]
theorem sum_of_two_squares_prime: assumes "prime p"
  shows "is_sum2sq_nat p = [p\<noteq>3] (mod 4)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_sum2sq_nat p = [p \<noteq> 3] (mod 4)
[PROOF STEP]
proof (cases "[p=3] (mod 4)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. [p = 3] (mod 4) \<Longrightarrow> is_sum2sq_nat p = [p \<noteq> 3] (mod 4)
 2. [p \<noteq> 3] (mod 4) \<Longrightarrow> is_sum2sq_nat p = [p \<noteq> 3] (mod 4)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
[p = 3] (mod 4)

goal (2 subgoals):
 1. [p = 3] (mod 4) \<Longrightarrow> is_sum2sq_nat p = [p \<noteq> 3] (mod 4)
 2. [p \<noteq> 3] (mod 4) \<Longrightarrow> is_sum2sq_nat p = [p \<noteq> 3] (mod 4)
[PROOF STEP]
have "odd (multiplicity p p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. odd (multiplicity p p)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
prime p

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

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

goal (1 subgoal):
 1. \<not> is_sum2sq_nat p
[PROOF STEP]
using assms True sum_of_two_squares'
[PROOF STATE]
proof (prove)
using this:
odd (multiplicity p p)
prime p
[p = 3] (mod 4)
is_sum2sq_nat ?n = (\<forall>p. prime p \<and> [p = 3] (mod 4) \<longrightarrow> even (multiplicity p ?n))

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

goal (2 subgoals):
 1. [p = 3] (mod 4) \<Longrightarrow> is_sum2sq_nat p = [p \<noteq> 3] (mod 4)
 2. [p \<noteq> 3] (mod 4) \<Longrightarrow> is_sum2sq_nat p = [p \<noteq> 3] (mod 4)
[PROOF STEP]
with True
[PROOF STATE]
proof (chain)
picking this:
[p = 3] (mod 4)
\<not> is_sum2sq_nat p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
[p = 3] (mod 4)
\<not> is_sum2sq_nat p

goal (1 subgoal):
 1. is_sum2sq_nat p = [p \<noteq> 3] (mod 4)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
is_sum2sq_nat p = [p \<noteq> 3] (mod 4)

goal (1 subgoal):
 1. [p \<noteq> 3] (mod 4) \<Longrightarrow> is_sum2sq_nat p = [p \<noteq> 3] (mod 4)
[PROOF STEP]
qed (simp add: fermat_two_squares assms)


[STATEMENT]
lemma (in prob_space) k_wise_indep_vars_subset:
  assumes "k_wise_indep_vars k M' X I"
  assumes "J \<subseteq> I"
  assumes "finite J"
  assumes "card J \<le> k"
  shows "indep_vars M' X J"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. indep_vars M' X J
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
k_wise_indep_vars k M' X I
J \<subseteq> I
finite J
card J \<le> k

goal (1 subgoal):
 1. indep_vars M' X J
[PROOF STEP]
by (simp add:k_wise_indep_vars_def)


[STATEMENT]
lemma (in prob_space) uniform_onD:
  assumes "uniform_on X A"
  shows "prob {\<omega> \<in> space M. X \<omega> \<in> B} = card (A \<inter> B) / card A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prob {\<omega> \<in> space M. X \<omega> \<in> B} = real (card (A \<inter> B)) / real (card A)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prob {\<omega> \<in> space M. X \<omega> \<in> B} = real (card (A \<inter> B)) / real (card A)
[PROOF STEP]
have "prob {\<omega> \<in> space M. X \<omega> \<in> B} = prob (X -` B \<inter> space M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prob {\<omega> \<in> space M. X \<omega> \<in> B} = prob (X -` B \<inter> space M)
[PROOF STEP]
by (subst Int_commute, simp add:vimage_def Int_def)
[PROOF STATE]
proof (state)
this:
prob {\<omega> \<in> space M. X \<omega> \<in> B} = prob (X -` B \<inter> space M)

goal (1 subgoal):
 1. prob {\<omega> \<in> space M. X \<omega> \<in> B} = real (card (A \<inter> B)) / real (card A)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
prob {\<omega> \<in> space M. X \<omega> \<in> B} = prob (X -` B \<inter> space M)

goal (1 subgoal):
 1. prob {\<omega> \<in> space M. X \<omega> \<in> B} = real (card (A \<inter> B)) / real (card A)
[PROOF STEP]
have "... = measure (distr M (count_space UNIV) X) B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prob (X -` B \<inter> space M) = Sigma_Algebra.measure (distr M (count_space UNIV) X) B
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
uniform_on X A

goal (1 subgoal):
 1. prob (X -` B \<inter> space M) = Sigma_Algebra.measure (distr M (count_space UNIV) X) B
[PROOF STEP]
by (subst measure_distr, auto simp:uniform_on_def)
[PROOF STATE]
proof (state)
this:
prob (X -` B \<inter> space M) = Sigma_Algebra.measure (distr M (count_space UNIV) X) B

goal (1 subgoal):
 1. prob {\<omega> \<in> space M. X \<omega> \<in> B} = real (card (A \<inter> B)) / real (card A)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
prob (X -` B \<inter> space M) = Sigma_Algebra.measure (distr M (count_space UNIV) X) B

goal (1 subgoal):
 1. prob {\<omega> \<in> space M. X \<omega> \<in> B} = real (card (A \<inter> B)) / real (card A)
[PROOF STEP]
have "... = measure (uniform_measure (count_space UNIV) A) B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sigma_Algebra.measure (distr M (count_space UNIV) X) B = Sigma_Algebra.measure (uniform_measure (count_space UNIV) A) B
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
uniform_on X A

goal (1 subgoal):
 1. Sigma_Algebra.measure (distr M (count_space UNIV) X) B = Sigma_Algebra.measure (uniform_measure (count_space UNIV) A) B
[PROOF STEP]
by (simp add:uniform_on_def)
[PROOF STATE]
proof (state)
this:
Sigma_Algebra.measure (distr M (count_space UNIV) X) B = Sigma_Algebra.measure (uniform_measure (count_space UNIV) A) B

goal (1 subgoal):
 1. prob {\<omega> \<in> space M. X \<omega> \<in> B} = real (card (A \<inter> B)) / real (card A)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Sigma_Algebra.measure (distr M (count_space UNIV) X) B = Sigma_Algebra.measure (uniform_measure (count_space UNIV) A) B

goal (1 subgoal):
 1. prob {\<omega> \<in> space M. X \<omega> \<in> B} = real (card (A \<inter> B)) / real (card A)
[PROOF STEP]
have "... = card (A \<inter> B) / card A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sigma_Algebra.measure (uniform_measure (count_space UNIV) A) B = real (card (A \<inter> B)) / real (card A)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
uniform_on X A

goal (1 subgoal):
 1. Sigma_Algebra.measure (uniform_measure (count_space UNIV) A) B = real (card (A \<inter> B)) / real (card A)
[PROOF STEP]
by (subst measure_uniform_measure, auto simp:uniform_on_def)+
[PROOF STATE]
proof (state)
this:
Sigma_Algebra.measure (uniform_measure (count_space UNIV) A) B = real (card (A \<inter> B)) / real (card A)

goal (1 subgoal):
 1. prob {\<omega> \<in> space M. X \<omega> \<in> B} = real (card (A \<inter> B)) / real (card A)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
prob {\<omega> \<in> space M. X \<omega> \<in> B} = real (card (A \<inter> B)) / real (card A)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
prob {\<omega> \<in> space M. X \<omega> \<in> B} = real (card (A \<inter> B)) / real (card A)

goal (1 subgoal):
 1. prob {\<omega> \<in> space M. X \<omega> \<in> B} = real (card (A \<inter> B)) / real (card A)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
prob {\<omega> \<in> space M. X \<omega> \<in> B} = real (card (A \<inter> B)) / real (card A)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma charpoly_of_real: "charpoly (map_matrix complex_of_real A) = map_poly of_real (charpoly A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. charpoly (HMA_Connect.map_matrix complex_of_real A) = map_poly complex_of_real (charpoly A)
[PROOF STEP]
by (transfer_hma rule: of_real_hom.char_poly_hom)


[STATEMENT]
lemma HMA_M_smult[transfer_rule]: "((=) ===> HMA_M ===> HMA_M) (\<cdot>\<^sub>m) ((*k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((=) ===> HMA_M ===> HMA_M) (\<cdot>\<^sub>m) (*k)
[PROOF STEP]
unfolding smult_mat_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((=) ===> HMA_M ===> HMA_M) (\<lambda>a. map_mat ((*) a)) (*k)
[PROOF STEP]
unfolding rel_fun_def HMA_M_def from_hma\<^sub>m_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x y. x = y \<longrightarrow> (\<forall>xa ya. xa = Matrix.mat CARD('c) CARD('b) (\<lambda>(i, j). ya $h Bij_Nat.from_nat i $h Bij_Nat.from_nat j) \<longrightarrow> map_mat ((*) x) xa = Matrix.mat CARD('c) CARD('b) (\<lambda>(i, j). (y *k ya) $h Bij_Nat.from_nat i $h Bij_Nat.from_nat j))
[PROOF STEP]
by (auto simp: matrix_scalar_mult_def)


[STATEMENT]
lemma order_charpoly_smult: fixes A :: "complex ^ 'n ^ 'n"
  assumes k: "k \<noteq> 0"
  shows "order x (charpoly (k *k A)) = order (x / k) (charpoly A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. order x (charpoly (k *k A)) = order (x / k) (charpoly A)
[PROOF STEP]
by (transfer fixing: k, rule order_char_poly_smult[OF _ k])


[STATEMENT]
lemma smult_eigen_vector: fixes a :: "'a :: field"
  assumes "eigen_vector A v x"
  shows "eigen_vector (a *k A) v (a * x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eigen_vector (a *k A) v (a * x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eigen_vector (a *k A) v (a * x)
[PROOF STEP]
from assms[unfolded eigen_vector_def]
[PROOF STATE]
proof (chain)
picking this:
v \<noteq> 0 \<and> A *v v = x *s v
[PROOF STEP]
have v: "v \<noteq> 0" and id: "A *v v = x *s v"
[PROOF STATE]
proof (prove)
using this:
v \<noteq> 0 \<and> A *v v = x *s v

goal (1 subgoal):
 1. v \<noteq> 0 &&& A *v v = x *s v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v \<noteq> 0
A *v v = x *s v

goal (1 subgoal):
 1. eigen_vector (a *k A) v (a * x)
[PROOF STEP]
from arg_cong[OF id, of "(*s) a"]
[PROOF STATE]
proof (chain)
picking this:
a *s (A *v v) = a *s (x *s v)
[PROOF STEP]
have id: "(a *k A) *v v = (a * x) *s v"
[PROOF STATE]
proof (prove)
using this:
a *s (A *v v) = a *s (x *s v)

goal (1 subgoal):
 1. a *k A *v v = a * x *s v
[PROOF STEP]
unfolding scalar_matrix_vector_assoc
[PROOF STATE]
proof (prove)
using this:
a *k A *v v = a *s (x *s v)

goal (1 subgoal):
 1. a *k A *v v = a * x *s v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a *k A *v v = a * x *s v

goal (1 subgoal):
 1. eigen_vector (a *k A) v (a * x)
[PROOF STEP]
thus "eigen_vector (a *k A) v (a * x)"
[PROOF STATE]
proof (prove)
using this:
a *k A *v v = a * x *s v

goal (1 subgoal):
 1. eigen_vector (a *k A) v (a * x)
[PROOF STEP]
using v
[PROOF STATE]
proof (prove)
using this:
a *k A *v v = a * x *s v
v \<noteq> 0

goal (1 subgoal):
 1. eigen_vector (a *k A) v (a * x)
[PROOF STEP]
unfolding eigen_vector_def
[PROOF STATE]
proof (prove)
using this:
a *k A *v v = a * x *s v
v \<noteq> 0

goal (1 subgoal):
 1. v \<noteq> 0 \<and> a *k A *v v = a * x *s v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eigen_vector (a *k A) v (a * x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma smult_eigen_value: fixes a :: "'a :: field"
  assumes "eigen_value A x"
  shows "eigen_value (a *k A) (a * x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eigen_value (a *k A) (a * x)
[PROOF STEP]
using assms smult_eigen_vector[of A _ x a]
[PROOF STATE]
proof (prove)
using this:
eigen_value A x
eigen_vector A ?v x \<Longrightarrow> eigen_vector (a *k A) ?v (a * x)

goal (1 subgoal):
 1. eigen_value (a *k A) (a * x)
[PROOF STEP]
unfolding eigen_value_def
[PROOF STATE]
proof (prove)
using this:
\<exists>v. eigen_vector A v x
eigen_vector A ?v x \<Longrightarrow> eigen_vector (a *k A) ?v (a * x)

goal (1 subgoal):
 1. \<exists>v. eigen_vector (a *k A) v (a * x)
[PROOF STEP]
by blast


[STATEMENT]
lemma G_transpose:
  "fixed_mat.G (transpose A) = ((fixed_mat.G A))^-1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fixed_mat.G (Finite_Cartesian_Product.transpose A) = (fixed_mat.G A)\<inverse>
[PROOF STEP]
unfolding fixed_mat.G_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(i, j). Finite_Cartesian_Product.transpose A $h i $h j \<noteq> (0::'b)} = {(i, j). A $h i $h j \<noteq> (0::'b)}\<inverse>
[PROOF STEP]
by (force simp: transpose_def)


[STATEMENT]
lemma G_transpose_trancl:
  "(fixed_mat.G (transpose A))^+ = ((fixed_mat.G A)^+)^-1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (fixed_mat.G (Finite_Cartesian_Product.transpose A))\<^sup>+ = ((fixed_mat.G A)\<^sup>+)\<inverse>
[PROOF STEP]
unfolding G_transpose trancl_converse
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((fixed_mat.G A)\<^sup>+)\<inverse> = ((fixed_mat.G A)\<^sup>+)\<inverse>
[PROOF STEP]
by auto


[STATEMENT]
lemma nonneg: "A $ i $ j \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> A $h i $h j
[PROOF STEP]
using non_neg_mat
[PROOF STATE]
proof (prove)
using this:
non_neg_mat A

goal (1 subgoal):
 1. (0::'a) \<le> A $h i $h j
[PROOF STEP]
unfolding non_neg_mat_def elements_mat_h_def
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>range (\<lambda>(i, y). A $h i $h y). (0::'a) \<le> a

goal (1 subgoal):
 1. (0::'a) \<le> A $h i $h j
[PROOF STEP]
by auto


[STATEMENT]
lemma nonneg_matpow: "matpow A n $ i $ j \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> matpow A n $h i $h j
[PROOF STEP]
by (induct n arbitrary: i j, insert nonneg,
    auto intro!: sum_nonneg simp: matrix_matrix_mult_def mat_def)


[STATEMENT]
lemma G_relpow_matpow_pos: "(i,j) \<in> G ^^ n \<Longrightarrow> matpow A n $ i $ j > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (i, j) \<in> G ^^ n \<Longrightarrow> (0::'a) < matpow A n $h i $h j
[PROOF STEP]
proof (induct n arbitrary: i j)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i j. (i, j) \<in> G ^^ 0 \<Longrightarrow> (0::'a) < matpow A 0 $h i $h j
 2. \<And>n i j. \<lbrakk>\<And>i j. (i, j) \<in> G ^^ n \<Longrightarrow> (0::'a) < matpow A n $h i $h j; (i, j) \<in> G ^^ Suc n\<rbrakk> \<Longrightarrow> (0::'a) < matpow A (Suc n) $h i $h j
[PROOF STEP]
case (0 i)
[PROOF STATE]
proof (state)
this:
(i, j) \<in> G ^^ 0

goal (2 subgoals):
 1. \<And>i j. (i, j) \<in> G ^^ 0 \<Longrightarrow> (0::'a) < matpow A 0 $h i $h j
 2. \<And>n i j. \<lbrakk>\<And>i j. (i, j) \<in> G ^^ n \<Longrightarrow> (0::'a) < matpow A n $h i $h j; (i, j) \<in> G ^^ Suc n\<rbrakk> \<Longrightarrow> (0::'a) < matpow A (Suc n) $h i $h j
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(i, j) \<in> G ^^ 0

goal (1 subgoal):
 1. (0::'a) < matpow A 0 $h i $h j
[PROOF STEP]
by (auto simp: mat_def)
[PROOF STATE]
proof (state)
this:
(0::'a) < matpow A 0 $h i $h j

goal (1 subgoal):
 1. \<And>n i j. \<lbrakk>\<And>i j. (i, j) \<in> G ^^ n \<Longrightarrow> (0::'a) < matpow A n $h i $h j; (i, j) \<in> G ^^ Suc n\<rbrakk> \<Longrightarrow> (0::'a) < matpow A (Suc n) $h i $h j
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n i j. \<lbrakk>\<And>i j. (i, j) \<in> G ^^ n \<Longrightarrow> (0::'a) < matpow A n $h i $h j; (i, j) \<in> G ^^ Suc n\<rbrakk> \<Longrightarrow> (0::'a) < matpow A (Suc n) $h i $h j
[PROOF STEP]
case (Suc n i j)
[PROOF STATE]
proof (state)
this:
(?i, ?j) \<in> G ^^ n \<Longrightarrow> (0::'a) < matpow A n $h ?i $h ?j
(i, j) \<in> G ^^ Suc n

goal (1 subgoal):
 1. \<And>n i j. \<lbrakk>\<And>i j. (i, j) \<in> G ^^ n \<Longrightarrow> (0::'a) < matpow A n $h i $h j; (i, j) \<in> G ^^ Suc n\<rbrakk> \<Longrightarrow> (0::'a) < matpow A (Suc n) $h i $h j
[PROOF STEP]
from Suc(2)
[PROOF STATE]
proof (chain)
picking this:
(i, j) \<in> G ^^ Suc n
[PROOF STEP]
have "(i,j) \<in> G ^^ n O G"
[PROOF STATE]
proof (prove)
using this:
(i, j) \<in> G ^^ Suc n

goal (1 subgoal):
 1. (i, j) \<in> G ^^ n O G
[PROOF STEP]
by (simp add: relpow_commute)
[PROOF STATE]
proof (state)
this:
(i, j) \<in> G ^^ n O G

goal (1 subgoal):
 1. \<And>n i j. \<lbrakk>\<And>i j. (i, j) \<in> G ^^ n \<Longrightarrow> (0::'a) < matpow A n $h i $h j; (i, j) \<in> G ^^ Suc n\<rbrakk> \<Longrightarrow> (0::'a) < matpow A (Suc n) $h i $h j
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(i, j) \<in> G ^^ n O G
[PROOF STEP]
obtain k where
    ik: "A $ k $ j \<noteq> 0" and kj: "(i, k) \<in> G ^^ n"
[PROOF STATE]
proof (prove)
using this:
(i, j) \<in> G ^^ n O G

goal (1 subgoal):
 1. (\<And>k. \<lbrakk>A $h k $h j \<noteq> (0::'a); (i, k) \<in> G ^^ n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: G_def)
[PROOF STATE]
proof (state)
this:
A $h k $h j \<noteq> (0::'a)
(i, k) \<in> G ^^ n

goal (1 subgoal):
 1. \<And>n i j. \<lbrakk>\<And>i j. (i, j) \<in> G ^^ n \<Longrightarrow> (0::'a) < matpow A n $h i $h j; (i, j) \<in> G ^^ Suc n\<rbrakk> \<Longrightarrow> (0::'a) < matpow A (Suc n) $h i $h j
[PROOF STEP]
from ik nonneg[of k j]
[PROOF STATE]
proof (chain)
picking this:
A $h k $h j \<noteq> (0::'a)
(0::'a) \<le> A $h k $h j
[PROOF STEP]
have ik: "A $ k $ j > 0"
[PROOF STATE]
proof (prove)
using this:
A $h k $h j \<noteq> (0::'a)
(0::'a) \<le> A $h k $h j

goal (1 subgoal):
 1. (0::'a) < A $h k $h j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(0::'a) < A $h k $h j

goal (1 subgoal):
 1. \<And>n i j. \<lbrakk>\<And>i j. (i, j) \<in> G ^^ n \<Longrightarrow> (0::'a) < matpow A n $h i $h j; (i, j) \<in> G ^^ Suc n\<rbrakk> \<Longrightarrow> (0::'a) < matpow A (Suc n) $h i $h j
[PROOF STEP]
from Suc(1)[OF kj]
[PROOF STATE]
proof (chain)
picking this:
(0::'a) < matpow A n $h i $h k
[PROOF STEP]
have IH: "matpow A n $h i $h k > 0"
[PROOF STATE]
proof (prove)
using this:
(0::'a) < matpow A n $h i $h k

goal (1 subgoal):
 1. (0::'a) < matpow A n $h i $h k
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(0::'a) < matpow A n $h i $h k

goal (1 subgoal):
 1. \<And>n i j. \<lbrakk>\<And>i j. (i, j) \<in> G ^^ n \<Longrightarrow> (0::'a) < matpow A n $h i $h j; (i, j) \<in> G ^^ Suc n\<rbrakk> \<Longrightarrow> (0::'a) < matpow A (Suc n) $h i $h j
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(0::'a) < matpow A n $h i $h k

goal (1 subgoal):
 1. (0::'a) < matpow A (Suc n) $h i $h j
[PROOF STEP]
using ik
[PROOF STATE]
proof (prove)
using this:
(0::'a) < matpow A n $h i $h k
(0::'a) < A $h k $h j

goal (1 subgoal):
 1. (0::'a) < matpow A (Suc n) $h i $h j
[PROOF STEP]
by (auto simp: nonneg_matpow nonneg matrix_matrix_mult_def
    intro!: sum_pos2[of _ k] mult_nonneg_nonneg)
[PROOF STATE]
proof (state)
this:
(0::'a) < matpow A (Suc n) $h i $h j

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma matpow_mono: assumes B: "\<And> i j. B $ i $ j \<ge> A $ i $ j"
  shows "matpow B n $ i $ j \<ge> matpow A n $ i $ j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matpow A n $h i $h j \<le> matpow B n $h i $h j
[PROOF STEP]
proof (induct n arbitrary: i j)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i j. matpow A 0 $h i $h j \<le> matpow B 0 $h i $h j
 2. \<And>n i j. (\<And>i j. matpow A n $h i $h j \<le> matpow B n $h i $h j) \<Longrightarrow> matpow A (Suc n) $h i $h j \<le> matpow B (Suc n) $h i $h j
[PROOF STEP]
case (Suc n i j)
[PROOF STATE]
proof (state)
this:
matpow A n $h ?i $h ?j \<le> matpow B n $h ?i $h ?j

goal (2 subgoals):
 1. \<And>i j. matpow A 0 $h i $h j \<le> matpow B 0 $h i $h j
 2. \<And>n i j. (\<And>i j. matpow A n $h i $h j \<le> matpow B n $h i $h j) \<Longrightarrow> matpow A (Suc n) $h i $h j \<le> matpow B (Suc n) $h i $h j
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
matpow A n $h ?i $h ?j \<le> matpow B n $h ?i $h ?j

goal (1 subgoal):
 1. matpow A (Suc n) $h i $h j \<le> matpow B (Suc n) $h i $h j
[PROOF STEP]
using B nonneg_matpow[of n] nonneg
[PROOF STATE]
proof (prove)
using this:
matpow A n $h ?i $h ?j \<le> matpow B n $h ?i $h ?j
A $h ?i $h ?j \<le> B $h ?i $h ?j
(0::'a) \<le> matpow A n $h ?i $h ?j
(0::'a) \<le> A $h ?i $h ?j

goal (1 subgoal):
 1. matpow A (Suc n) $h i $h j \<le> matpow B (Suc n) $h i $h j
[PROOF STEP]
by (auto simp: matrix_matrix_mult_def intro!: sum_mono mult_mono')
[PROOF STATE]
proof (state)
this:
matpow A (Suc n) $h i $h j \<le> matpow B (Suc n) $h i $h j

goal (1 subgoal):
 1. \<And>i j. matpow A 0 $h i $h j \<le> matpow B 0 $h i $h j
[PROOF STEP]
qed simp


[STATEMENT]
lemma matpow_sum_one_mono: "matpow (A + mat 1) (n + k) $ i $ j \<ge> matpow (A + mat 1) n $ i $ j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matpow (A + mat (1::'a)) n $h i $h j \<le> matpow (A + mat (1::'a)) (n + k) $h i $h j
[PROOF STEP]
proof (induct k)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. matpow (A + mat (1::'a)) n $h i $h j \<le> matpow (A + mat (1::'a)) (n + 0) $h i $h j
 2. \<And>k. matpow (A + mat (1::'a)) n $h i $h j \<le> matpow (A + mat (1::'a)) (n + k) $h i $h j \<Longrightarrow> matpow (A + mat (1::'a)) n $h i $h j \<le> matpow (A + mat (1::'a)) (n + Suc k) $h i $h j
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
matpow (A + mat (1::'a)) n $h i $h j \<le> matpow (A + mat (1::'a)) (n + k) $h i $h j

goal (2 subgoals):
 1. matpow (A + mat (1::'a)) n $h i $h j \<le> matpow (A + mat (1::'a)) (n + 0) $h i $h j
 2. \<And>k. matpow (A + mat (1::'a)) n $h i $h j \<le> matpow (A + mat (1::'a)) (n + k) $h i $h j \<Longrightarrow> matpow (A + mat (1::'a)) n $h i $h j \<le> matpow (A + mat (1::'a)) (n + Suc k) $h i $h j
[PROOF STEP]
have "(matpow (A + mat 1) (n + k) ** A) $h i $h j \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> (matpow (A + mat (1::'a)) (n + k) ** A) $h i $h j
[PROOF STEP]
unfolding matrix_matrix_mult_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> (\<chi>i j. \<Sum>k\<in>UNIV. matpow (A + mat (1::'a)) (n + k) $h i $h k * A $h k $h j) $h i $h j
[PROOF STEP]
using order.trans[OF nonneg_matpow matpow_mono[of "A + mat 1" "n + k"]]
[PROOF STATE]
proof (prove)
using this:
(\<And>i j. A $h i $h j \<le> (A + mat (1::'a)) $h i $h j) \<Longrightarrow> (0::'a) \<le> matpow (A + mat (1::'a)) (n + k) $h ?i1 $h ?j1

goal (1 subgoal):
 1. (0::'a) \<le> (\<chi>i j. \<Sum>k\<in>UNIV. matpow (A + mat (1::'a)) (n + k) $h i $h k * A $h k $h j) $h i $h j
[PROOF STEP]
by (auto intro!: sum_nonneg mult_nonneg_nonneg nonneg simp: mat_def)
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> (matpow (A + mat (1::'a)) (n + k) ** A) $h i $h j

goal (2 subgoals):
 1. matpow (A + mat (1::'a)) n $h i $h j \<le> matpow (A + mat (1::'a)) (n + 0) $h i $h j
 2. \<And>k. matpow (A + mat (1::'a)) n $h i $h j \<le> matpow (A + mat (1::'a)) (n + k) $h i $h j \<Longrightarrow> matpow (A + mat (1::'a)) n $h i $h j \<le> matpow (A + mat (1::'a)) (n + Suc k) $h i $h j
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(0::'a) \<le> (matpow (A + mat (1::'a)) (n + k) ** A) $h i $h j

goal (1 subgoal):
 1. matpow (A + mat (1::'a)) n $h i $h j \<le> matpow (A + mat (1::'a)) (n + Suc k) $h i $h j
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
(0::'a) \<le> (matpow (A + mat (1::'a)) (n + k) ** A) $h i $h j
matpow (A + mat (1::'a)) n $h i $h j \<le> matpow (A + mat (1::'a)) (n + k) $h i $h j

goal (1 subgoal):
 1. matpow (A + mat (1::'a)) n $h i $h j \<le> matpow (A + mat (1::'a)) (n + Suc k) $h i $h j
[PROOF STEP]
by (simp add: matrix_add_ldistrib matrix_mul_rid)
[PROOF STATE]
proof (state)
this:
matpow (A + mat (1::'a)) n $h i $h j \<le> matpow (A + mat (1::'a)) (n + Suc k) $h i $h j

goal (1 subgoal):
 1. matpow (A + mat (1::'a)) n $h i $h j \<le> matpow (A + mat (1::'a)) (n + 0) $h i $h j
[PROOF STEP]
qed simp


[STATEMENT]
lemma G_relpow_matpow_pos_ge:
  assumes "(i,j) \<in> G ^^ m" "n \<ge> m"
  shows "matpow (A + mat 1) n $ i $ j > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) < matpow (A + mat (1::'a)) n $h i $h j
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (0::'a) < matpow (A + mat (1::'a)) n $h i $h j
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
m \<le> n
[PROOF STEP]
obtain k where n: "n = m + k"
[PROOF STATE]
proof (prove)
using this:
m \<le> n

goal (1 subgoal):
 1. (\<And>k. n = m + k \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using le_Suc_ex
[PROOF STATE]
proof (prove)
using this:
m \<le> n
?k \<le> ?l \<Longrightarrow> \<exists>n. ?l = ?k + n

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

goal (1 subgoal):
 1. (0::'a) < matpow (A + mat (1::'a)) n $h i $h j
[PROOF STEP]
have "0 < matpow A m $ i $ j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) < matpow A m $h i $h j
[PROOF STEP]
by (rule G_relpow_matpow_pos[OF assms(1)])
[PROOF STATE]
proof (state)
this:
(0::'a) < matpow A m $h i $h j

goal (1 subgoal):
 1. (0::'a) < matpow (A + mat (1::'a)) n $h i $h j
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(0::'a) < matpow A m $h i $h j

goal (1 subgoal):
 1. (0::'a) < matpow (A + mat (1::'a)) n $h i $h j
[PROOF STEP]
have "\<dots> \<le> matpow (A + mat 1) m $ i $ j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matpow A m $h i $h j \<le> matpow (A + mat (1::'a)) m $h i $h j
[PROOF STEP]
by (rule matpow_mono, auto simp: mat_def)
[PROOF STATE]
proof (state)
this:
matpow A m $h i $h j \<le> matpow (A + mat (1::'a)) m $h i $h j

goal (1 subgoal):
 1. (0::'a) < matpow (A + mat (1::'a)) n $h i $h j
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
matpow A m $h i $h j \<le> matpow (A + mat (1::'a)) m $h i $h j

goal (1 subgoal):
 1. (0::'a) < matpow (A + mat (1::'a)) n $h i $h j
[PROOF STEP]
have "\<dots> \<le> matpow (A + mat 1) n $ i $ j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matpow (A + mat (1::'a)) m $h i $h j \<le> matpow (A + mat (1::'a)) n $h i $h j
[PROOF STEP]
unfolding n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matpow (A + mat (1::'a)) m $h i $h j \<le> matpow (A + mat (1::'a)) (m + k) $h i $h j
[PROOF STEP]
using matpow_sum_one_mono
[PROOF STATE]
proof (prove)
using this:
matpow (A + mat (1::'a)) ?n $h ?i $h ?j \<le> matpow (A + mat (1::'a)) (?n + ?k) $h ?i $h ?j

goal (1 subgoal):
 1. matpow (A + mat (1::'a)) m $h i $h j \<le> matpow (A + mat (1::'a)) (m + k) $h i $h j
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
matpow (A + mat (1::'a)) m $h i $h j \<le> matpow (A + mat (1::'a)) n $h i $h j

goal (1 subgoal):
 1. (0::'a) < matpow (A + mat (1::'a)) n $h i $h j
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(0::'a) < matpow (A + mat (1::'a)) n $h i $h j
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(0::'a) < matpow (A + mat (1::'a)) n $h i $h j

goal (1 subgoal):
 1. (0::'a) < matpow (A + mat (1::'a)) n $h i $h j
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(0::'a) < matpow (A + mat (1::'a)) n $h i $h j

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma N: "\<exists> n \<le> N. ij \<in> G ^^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n\<le>N. ij \<in> G ^^ n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>n\<le>N. ij \<in> G ^^ n
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>n\<le>N. ij \<in> G ^^ n
[PROOF STEP]
fix ij
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>n\<le>N. ij \<in> G ^^ n
[PROOF STEP]
have "ij \<in> G^+"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ij \<in> G\<^sup>+
[PROOF STEP]
using irr[unfolded irreducible_def]
[PROOF STATE]
proof (prove)
using this:
UNIV \<subseteq> G\<^sup>+

goal (1 subgoal):
 1. ij \<in> G\<^sup>+
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ij \<in> G\<^sup>+

goal (1 subgoal):
 1. \<exists>n\<le>N. ij \<in> G ^^ n
[PROOF STEP]
from this[unfolded trancl_power]
[PROOF STATE]
proof (chain)
picking this:
\<exists>n>0. ij \<in> G ^^ n
[PROOF STEP]
have "\<exists> n. ij \<in> G ^^ n"
[PROOF STATE]
proof (prove)
using this:
\<exists>n>0. ij \<in> G ^^ n

goal (1 subgoal):
 1. \<exists>n. ij \<in> G ^^ n
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>n. ij \<in> G ^^ n

goal (1 subgoal):
 1. \<exists>n\<le>N. ij \<in> G ^^ n
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<exists>n. ?ija2 \<in> G ^^ n

goal (1 subgoal):
 1. \<exists>n\<le>N. ij \<in> G ^^ n
[PROOF STEP]
hence "\<forall> ij. \<exists> n. ij \<in> G ^^ n"
[PROOF STATE]
proof (prove)
using this:
\<exists>n. ?ija2 \<in> G ^^ n

goal (1 subgoal):
 1. \<forall>ij. \<exists>n. ij \<in> G ^^ n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>ij. \<exists>n. ij \<in> G ^^ n

goal (1 subgoal):
 1. \<exists>n\<le>N. ij \<in> G ^^ n
[PROOF STEP]
from choice[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>f. \<forall>x. x \<in> G ^^ f x
[PROOF STEP]
obtain f where f: "\<And> ij. ij \<in> G ^^ (f ij)"
[PROOF STATE]
proof (prove)
using this:
\<exists>f. \<forall>x. x \<in> G ^^ f x

goal (1 subgoal):
 1. (\<And>f. (\<And>ij. ij \<in> G ^^ f ij) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?ij \<in> G ^^ f ?ij

goal (1 subgoal):
 1. \<exists>n\<le>N. ij \<in> G ^^ n
[PROOF STEP]
define N where N: "N = Max (range f)"
[PROOF STATE]
proof (state)
this:
N = Max (range f)

goal (1 subgoal):
 1. \<exists>n\<le>N. ij \<in> G ^^ n
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
N = Max (range f)

goal (1 subgoal):
 1. \<exists>n\<le>N. ij \<in> G ^^ n
[PROOF STEP]
fix ij
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>n\<le>N. ij \<in> G ^^ n
[PROOF STEP]
from f[of ij]
[PROOF STATE]
proof (chain)
picking this:
ij \<in> G ^^ f ij
[PROOF STEP]
have "ij \<in> G ^^ f ij"
[PROOF STATE]
proof (prove)
using this:
ij \<in> G ^^ f ij

goal (1 subgoal):
 1. ij \<in> G ^^ f ij
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
ij \<in> G ^^ f ij

goal (1 subgoal):
 1. \<exists>n\<le>N. ij \<in> G ^^ n
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ij \<in> G ^^ f ij

goal (1 subgoal):
 1. \<exists>n\<le>N. ij \<in> G ^^ n
[PROOF STEP]
have "f ij \<le> N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ij \<le> N
[PROOF STEP]
unfolding N
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ij \<le> Max (range f)
[PROOF STEP]
by (rule Max_ge, auto)
[PROOF STATE]
proof (state)
this:
f ij \<le> N

goal (1 subgoal):
 1. \<exists>n\<le>N. ij \<in> G ^^ n
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ij \<in> G ^^ f ij
f ij \<le> N
[PROOF STEP]
have "\<exists> n \<le> N. ij \<in> G ^^ n"
[PROOF STATE]
proof (prove)
using this:
ij \<in> G ^^ f ij
f ij \<le> N

goal (1 subgoal):
 1. \<exists>n\<le>N. ij \<in> G ^^ n
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>n\<le>N. ij \<in> G ^^ n

goal (1 subgoal):
 1. \<exists>n\<le>N. ij \<in> G ^^ n
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<exists>n\<le>N. ?ija2 \<in> G ^^ n

goal (1 subgoal):
 1. \<exists>n\<le>N. ij \<in> G ^^ n
[PROOF STEP]
note main = this
[PROOF STATE]
proof (state)
this:
\<exists>n\<le>N. ?ija2 \<in> G ^^ n

goal (1 subgoal):
 1. \<exists>n\<le>N. ij \<in> G ^^ n
[PROOF STEP]
let ?P = "\<lambda> N. \<forall> ij. \<exists> n \<le> N. ij \<in> G ^^ n"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>n\<le>N. ij \<in> G ^^ n
[PROOF STEP]
from main
[PROOF STATE]
proof (chain)
picking this:
\<exists>n\<le>N. ?ija2 \<in> G ^^ n
[PROOF STEP]
have "?P N"
[PROOF STATE]
proof (prove)
using this:
\<exists>n\<le>N. ?ija2 \<in> G ^^ n

goal (1 subgoal):
 1. \<forall>ij. \<exists>n\<le>N. ij \<in> G ^^ n
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>ij. \<exists>n\<le>N. ij \<in> G ^^ n

goal (1 subgoal):
 1. \<exists>n\<le>N. ij \<in> G ^^ n
[PROOF STEP]
from someI[of ?P, OF this, folded N_def]
[PROOF STATE]
proof (chain)
picking this:
\<forall>ij. \<exists>n\<le>N. ij \<in> G ^^ n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>ij. \<exists>n\<le>N. ij \<in> G ^^ n

goal (1 subgoal):
 1. \<exists>n\<le>N. ij \<in> G ^^ n
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>n\<le>N. ij \<in> G ^^ n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma irreducible_matpow_pos: assumes irreducible
  shows "matpow (A + mat 1) N $ i $ j > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < matpow (A + mat 1) N $h i $h j
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < matpow (A + mat 1) N $h i $h j
[PROOF STEP]
from N
[PROOF STATE]
proof (chain)
picking this:
\<exists>n\<le>N. ?ij \<in> G ^^ n
[PROOF STEP]
obtain n where n: "n \<le> N" and reach: "(i,j) \<in> G ^^ n"
[PROOF STATE]
proof (prove)
using this:
\<exists>n\<le>N. ?ij \<in> G ^^ n

goal (1 subgoal):
 1. (\<And>n. \<lbrakk>n \<le> N; (i, j) \<in> G ^^ n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n \<le> N
(i, j) \<in> G ^^ n

goal (1 subgoal):
 1. 0 < matpow (A + mat 1) N $h i $h j
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < matpow (A + mat 1) N $h i $h j
[PROOF STEP]
by (rule G_relpow_matpow_pos_ge[OF reach n])
[PROOF STATE]
proof (state)
this:
0 < matpow (A + mat 1) N $h i $h j

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pf_transpose: "perron_frobenius (transpose A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. perron_frobenius (Finite_Cartesian_Product.transpose A)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. non_neg_mat (Finite_Cartesian_Product.transpose A)
 2. fixed_mat.irreducible (Finite_Cartesian_Product.transpose A)
[PROOF STEP]
show "fixed_mat.irreducible (transpose A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fixed_mat.irreducible (Finite_Cartesian_Product.transpose A)
[PROOF STEP]
unfolding fixed_mat.irreducible_def G_transpose_trancl
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. UNIV \<subseteq> (G\<^sup>+)\<inverse>
[PROOF STEP]
using irr[unfolded irreducible_def]
[PROOF STATE]
proof (prove)
using this:
UNIV \<subseteq> G\<^sup>+

goal (1 subgoal):
 1. UNIV \<subseteq> (G\<^sup>+)\<inverse>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fixed_mat.irreducible (Finite_Cartesian_Product.transpose A)

goal (1 subgoal):
 1. non_neg_mat (Finite_Cartesian_Product.transpose A)
[PROOF STEP]
qed (insert nonneg, auto simp: transpose_def non_neg_mat_def elements_mat_h_def)


[STATEMENT]
lemma nonneg_Ax: "x \<in> X \<Longrightarrow> le_vec 0 (A *v x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> X \<Longrightarrow> le_vec 0 (A *v x)
[PROOF STEP]
unfolding X_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> {x. le_vec 0 x \<and> x \<noteq> 0} \<Longrightarrow> le_vec 0 (A *v x)
[PROOF STEP]
using nonneg
[PROOF STATE]
proof (prove)
using this:
0 \<le> A $h ?i $h ?j

goal (1 subgoal):
 1. x \<in> {x. le_vec 0 x \<and> x \<noteq> 0} \<Longrightarrow> le_vec 0 (A *v x)
[PROOF STEP]
by (auto simp: matrix_vector_mult_def intro!: sum_nonneg)


[STATEMENT]
lemma A_nonzero_fixed_j: "\<exists> i. A $ i $ j \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i. A $h i $h j \<noteq> 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>i. A $h i $h j \<noteq> 0
[PROOF STEP]
from irr[unfolded irreducible_def]
[PROOF STATE]
proof (chain)
picking this:
UNIV \<subseteq> G\<^sup>+
[PROOF STEP]
have "(j,j) \<in> G^+"
[PROOF STATE]
proof (prove)
using this:
UNIV \<subseteq> G\<^sup>+

goal (1 subgoal):
 1. (j, j) \<in> G\<^sup>+
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(j, j) \<in> G\<^sup>+

goal (1 subgoal):
 1. \<exists>i. A $h i $h j \<noteq> 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(j, j) \<in> G\<^sup>+
[PROOF STEP]
obtain i where "(i,j) \<in> G"
[PROOF STATE]
proof (prove)
using this:
(j, j) \<in> G\<^sup>+

goal (1 subgoal):
 1. (\<And>i. (i, j) \<in> G \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases, auto)
[PROOF STATE]
proof (state)
this:
(i, j) \<in> G

goal (1 subgoal):
 1. \<exists>i. A $h i $h j \<noteq> 0
[PROOF STEP]
hence Aij: "A $ i $ j \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
(i, j) \<in> G

goal (1 subgoal):
 1. A $h i $h j \<noteq> 0
[PROOF STEP]
unfolding G_def
[PROOF STATE]
proof (prove)
using this:
(i, j) \<in> {(i, j). A $h i $h j \<noteq> 0}

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

goal (1 subgoal):
 1. \<exists>i. A $h i $h j \<noteq> 0
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
A $h i $h j \<noteq> 0

goal (1 subgoal):
 1. \<exists>i. A $h i $h j \<noteq> 0
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>i. A $h i $h j \<noteq> 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Ax_pos: assumes x: "lt_vec 0 x"
  shows "lt_vec 0 (A *v x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lt_vec 0 (A *v x)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. 0 $h i < (A *v x) $h i
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. 0 $h i < (A *v x) $h i
[PROOF STEP]
from A_nonzero_fixed_i[of i]
[PROOF STATE]
proof (chain)
picking this:
\<exists>j. A $h i $h j \<noteq> 0
[PROOF STEP]
obtain j where "A $ i $ j \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
\<exists>j. A $h i $h j \<noteq> 0

goal (1 subgoal):
 1. (\<And>j. A $h i $h j \<noteq> 0 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A $h i $h j \<noteq> 0

goal (1 subgoal):
 1. \<And>i. 0 $h i < (A *v x) $h i
[PROOF STEP]
with nonneg[of i j]
[PROOF STATE]
proof (chain)
picking this:
0 \<le> A $h i $h j
A $h i $h j \<noteq> 0
[PROOF STEP]
have A: "A $ i $ j > 0"
[PROOF STATE]
proof (prove)
using this:
0 \<le> A $h i $h j
A $h i $h j \<noteq> 0

goal (1 subgoal):
 1. 0 < A $h i $h j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < A $h i $h j

goal (1 subgoal):
 1. \<And>i. 0 $h i < (A *v x) $h i
[PROOF STEP]
from x
[PROOF STATE]
proof (chain)
picking this:
lt_vec 0 x
[PROOF STEP]
have "x $ j \<ge> 0" for j
[PROOF STATE]
proof (prove)
using this:
lt_vec 0 x

goal (1 subgoal):
 1. 0 \<le> x $h j
[PROOF STEP]
by (auto simp: order.strict_iff_order)
[PROOF STATE]
proof (state)
this:
0 \<le> x $h ?j

goal (1 subgoal):
 1. \<And>i. 0 $h i < (A *v x) $h i
[PROOF STEP]
note nonneg = mult_nonneg_nonneg[OF nonneg[of i] this]
[PROOF STATE]
proof (state)
this:
0 \<le> A $h i $h ?j2 * x $h ?j1

goal (1 subgoal):
 1. \<And>i. 0 $h i < (A *v x) $h i
[PROOF STEP]
have "(A *v x) $ i = (\<Sum>j\<in>UNIV. A $ i $ j * x $ j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A *v x) $h i = (\<Sum>j\<in>UNIV. A $h i $h j * x $h j)
[PROOF STEP]
unfolding matrix_vector_mult_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<chi>i. \<Sum>j\<in>UNIV. A $h i $h j * x $h j) $h i = (\<Sum>j\<in>UNIV. A $h i $h j * x $h j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(A *v x) $h i = (\<Sum>j\<in>UNIV. A $h i $h j * x $h j)

goal (1 subgoal):
 1. \<And>i. 0 $h i < (A *v x) $h i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(A *v x) $h i = (\<Sum>j\<in>UNIV. A $h i $h j * x $h j)

goal (1 subgoal):
 1. \<And>i. 0 $h i < (A *v x) $h i
[PROOF STEP]
have "\<dots> = A $ i $ j * x $ j + (\<Sum>j\<in>UNIV - {j}. A $ i $ j * x $ j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j\<in>UNIV. A $h i $h j * x $h j) = A $h i $h j * x $h j + (\<Sum>j\<in>UNIV - {j}. A $h i $h j * x $h j)
[PROOF STEP]
by (subst sum.remove, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<in>UNIV. A $h i $h j * x $h j) = A $h i $h j * x $h j + (\<Sum>j\<in>UNIV - {j}. A $h i $h j * x $h j)

goal (1 subgoal):
 1. \<And>i. 0 $h i < (A *v x) $h i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<in>UNIV. A $h i $h j * x $h j) = A $h i $h j * x $h j + (\<Sum>j\<in>UNIV - {j}. A $h i $h j * x $h j)

goal (1 subgoal):
 1. \<And>i. 0 $h i < (A *v x) $h i
[PROOF STEP]
have "\<dots> > 0 + 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 + 0 < A $h i $h j * x $h j + (\<Sum>j\<in>UNIV - {j}. A $h i $h j * x $h j)
[PROOF STEP]
by (rule add_less_le_mono, insert A x[rule_format] nonneg,
    auto intro!: sum_nonneg mult_pos_pos)
[PROOF STATE]
proof (state)
this:
0 + 0 < A $h i $h j * x $h j + (\<Sum>j\<in>UNIV - {j}. A $h i $h j * x $h j)

goal (1 subgoal):
 1. \<And>i. 0 $h i < (A *v x) $h i
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
0 + 0 < (A *v x) $h i
[PROOF STEP]
show "0 $ i < (A *v x) $ i"
[PROOF STATE]
proof (prove)
using this:
0 + 0 < (A *v x) $h i

goal (1 subgoal):
 1. 0 $h i < (A *v x) $h i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 $h i < (A *v x) $h i

goal:
No subgoals!
[PROOF STEP]
qed