Theory TwoSquares
theory TwoSquares
imports
"HOL-Number_Theory.Number_Theory"
begin
context
fixes sum2sq_nat :: "nat ⇒ nat ⇒ nat"
defines "sum2sq_nat a b ≡ a^2+b^2"
fixes is_sum2sq_nat :: "nat ⇒ bool"
defines "is_sum2sq_nat n ≡ (∃ a b. n = sum2sq_nat a b)"
begin
private lemma best_division_abs: "(n::int) > 0 ⟹ ∃ k. 2 * ¦a - k*n¦ ≤ n"
proof -
assume a: "n > 0"
define k where "k = a div n"
hence h: "a - k * n = a mod n" by (simp add: mod_div_mult_eq algebra_simps)
thus ?thesis
proof (cases "2 * (a mod n) ≤ n")
case True
hence "2 * ¦a - k*n¦ ≤ n" using h pos_mod_sign a by auto
thus ?thesis by blast
next
case False
hence "2 * (n - a mod n) ≤ n" by auto
have "a - (k+1)*n = a mod n - n" using h by (simp add: algebra_simps)
hence "2 * ¦a - (k+1)*n¦ ≤ n" using h pos_mod_bound[of n a] a False by fastforce
thus ?thesis by blast
qed
qed
private definition
sum2sq_int :: "int × int ⇒ int" where
"sum2sq_int = (λ(a,b). a^2+b^2)"
private definition
is_sum2sq_int :: "int ⇒ bool" where
"is_sum2sq_int n ⟷ (∃ a b. n = sum2sq_int(a,b))"
private lemma sum2sq_int_nat_eq: "sum2sq_nat a b = sum2sq_int (a, b)"
unfolding sum2sq_nat_def sum2sq_int_def by simp
private lemma is_sum2sq_int_nat_eq: "is_sum2sq_nat n = is_sum2sq_int (int n)"
unfolding is_sum2sq_nat_def is_sum2sq_int_def
proof
assume "∃a b. n = sum2sq_nat a b"
thus "∃a b. int n = sum2sq_int (a, b)" using sum2sq_int_nat_eq by force
next
assume "∃a b. int n = sum2sq_int (a, b)"
then obtain a b where "int n = sum2sq_int (a, b)" by blast
hence "int n = sum2sq_int (int (nat ¦a¦), int (nat ¦b¦))" unfolding sum2sq_int_def by simp
hence "int n = int (sum2sq_nat (nat ¦a¦) (nat ¦b¦))" using sum2sq_int_nat_eq by presburger
thus "∃a b. n = sum2sq_nat a b" by auto
qed
private lemma product_two_squares_aux: "sum2sq_int(a, b) * sum2sq_int(c, d) = sum2sq_int(a*c - b*d, a*d + b*c)"
unfolding power2_eq_square sum2sq_int_def by (simp add: algebra_simps)
private lemma product_two_squares_int: "is_sum2sq_int m ⟹ is_sum2sq_int n ⟹ is_sum2sq_int (m*n)"
by (unfold is_sum2sq_int_def, auto simp only: product_two_squares_aux, blast)
private lemma product_two_squares_nat: "is_sum2sq_nat m ⟹ is_sum2sq_nat n ⟹ is_sum2sq_nat (m*n)"
using product_two_squares_int is_sum2sq_int_nat_eq by simp
private lemma sots1_aux:
assumes "prime (4*k+3)"
assumes "odd (multiplicity (4*k+3) n)"
shows "¬ is_sum2sq_nat n"
proof
assume "is_sum2sq_nat n"
then obtain a b where h1: "n = a^2 + b^2" unfolding is_sum2sq_nat_def sum2sq_nat_def by blast
have ab_nz: "a ≠ 0 ∨ b ≠ 0" by (rule ccontr) (insert assms, auto simp: h1)
let ?p = "4*k+3"
let ?g = "gcd a b"
have h2: "?g ≠ 0" using assms(2) h1 odd_pos by fastforce
then obtain a' b' where h3: "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
using gcd_coprime_exists by blast
have "?g^2 dvd n" using dvd_add h1 by auto
then obtain m where h4: "m * ?g^2 = n" using dvd_div_mult_self by blast
also have "… = (a' * ?g)^2 + (b' * ?g)^2" unfolding h1 using h3 by presburger
also have "… = ?g^2 * a'^2 + ?g^2 * b'^2" unfolding power2_eq_square by simp
finally have "?g^2 * m = ?g^2 * (a'^2 + b'^2)" by (simp add: distrib_left mult.commute)
hence h5: "m = a'^2 + b'^2" using h2 by auto
let ?mul = "multiplicity ?p ?g"
have "multiplicity ?p (?g^2) = ?mul + ?mul"
unfolding power2_eq_square using h2 assms
by (subst prime_elem_multiplicity_mult_distrib) simp_all
hence "even (multiplicity ?p (?g^2))" by simp
moreover have "m ≠ 0" using assms(2) h4 odd_pos by fastforce
ultimately have "odd (multiplicity ?p m)"
using assms ab_nz by (simp_all add: h4 [symmetric] prime_elem_multiplicity_mult_distrib)
hence "?p dvd m" using not_dvd_imp_multiplicity_0 by force
hence h6: "?p dvd a'^2+b'^2" using h5 by auto
{
assume "?p dvd a'^2"
moreover hence "?p dvd b'^2" using h6 dvd_add_right_iff by blast
ultimately have "?p dvd a'" "?p dvd b'" using assms(1) prime_dvd_power_nat by blast+
hence "False"
using assms(1) h3(3) coprime_common_divisor_nat[of a' b' ?p] not_prime_1 by linarith
}
hence "¬ (?p dvd a'^2)" ..
hence h7: "¬ (?p dvd a')" using assms(1)
by (simp add: power2_eq_square prime_dvd_mult_iff)
hence "coprime ?p a'"
using assms(1) by (simp add: prime_imp_coprime)
thm prime_imp_coprime_nat
moreover have "a' ≠ 0" using h7 dvd_0_right[of ?p] by meson
ultimately obtain ainv aux where "a' * ainv = ?p * aux + 1"
using bezout_nat[of "a'" ?p]
by (auto simp: ac_simps)
hence "[a' * ainv = 1] (mod ?p)" using cong_to_1'_nat by auto
from cong_mult [OF this this] have h11: "[1 = ainv^2 * a'^2] (mod ?p)"
unfolding power2_eq_square by (simp add: algebra_simps cong_sym)
let ?bdiva = "ainv * b'"
have "[ainv^2 * (a'^2 + b'^2) = 0] (mod ?p)"
using h6 cong_dvd_modulus_nat cong_mult_self_right by blast
from cong_add [OF h11 this] have "[1 + ainv^2 * b'^2 = 0] (mod ?p)"
unfolding add_mult_distrib2 using cong_add_lcancel_nat[of "ainv^2 * a'^2"]
by fastforce
hence h8: "[?bdiva^2 + 1 = 0] (mod ?p)" by (simp add: power_mult_distrib)
{
assume "?p dvd ?bdiva"
hence "?p dvd (?bdiva^2)" by (simp add: assms(1) prime_dvd_power_nat_iff)
hence "[?bdiva^2 = 0] (mod ?p)" using cong_altdef_nat by auto
hence "[?bdiva^2 +1 = 1] (mod ?p)" using cong_add_rcancel_0_nat by blast
from this h8 have "[0 = 1] (mod ?p)" using cong_sym cong_trans by blast
hence "?p dvd 1" using cong_0_1_nat by auto
hence "False" using assms(1) by simp
}
hence "¬ (?p dvd ?bdiva)" ..
hence h9: "[?bdiva^(?p-1) = 1] (mod ?p)"
using assms(1) fermat_theorem [of ?p ?bdiva] by simp
have h10: "?p≥3" by simp
have h11: "[?bdiva^(4*k+2) = 1] (mod ?p)" using h9 by auto
have "[(?bdiva^2 + 1)^2 = 0] (mod ?p)" using h8 cong_pow [of "?bdiva^2 + 1" 0 ?p 2] by auto
moreover have "?bdiva ^ 4 = (?bdiva ^ 2) ^ 2" by auto
hence "(?bdiva^2 + 1)^2 = ?bdiva^4 + ?bdiva^2 + ?bdiva^2 + 1"
by (auto simp: algebra_simps power2_eq_square)
ultimately have "[?bdiva^4 + ?bdiva^2 + ?bdiva^2 + 1 = 0] (mod ?p)" by simp
moreover have "[?bdiva^4 + ?bdiva^2 + (?bdiva^2 + 1) = ?bdiva^4 + ?bdiva^2 + 0] (mod ?p)"
using h8 cong_add_lcancel_nat by blast
ultimately have "[?bdiva^4 + ?bdiva^2 = 0] (mod ?p)" by (simp add: cong_def)
hence "[?bdiva^4 + ?bdiva^2 + 1 = 0 + 1] (mod ?p)" using cong_add_rcancel_nat by blast
moreover have "[?bdiva^4 + (?bdiva^2 + 1) = ?bdiva^4 + 0] (mod ?p)"
using h8 cong_add_lcancel_nat by blast
ultimately have "[?bdiva^4 = 1] (mod ?p)" by (simp add: cong_def)
hence "[(?bdiva^4)^k = 1^k] (mod ?p)" using cong_pow by blast
hence h12: "[?bdiva^(4*k) = 1] (mod ?p)" by (simp add: power_mult)
hence h13: "[?bdiva^(4*k)*(?bdiva^2 + 1) = 1*(?bdiva^2 + 1)] (mod ?p)"
using cong_scalar_right by blast
have "?bdiva^(4*k)*(?bdiva^2 + 1) = ?bdiva^(4*k+2)+?bdiva^(4*k)"
unfolding add_mult_distrib2 power_add by simp
hence "[?bdiva^(4*k+2)+?bdiva^(4*k) = ?bdiva^2 + 1] (mod ?p)"
using h13 unfolding nat_mult_1 by presburger
moreover have "[?bdiva^(4*k+2) + ?bdiva^(4*k) = 1 + 1] (mod ?p)"
using h11 h12 cong_add by blast
ultimately have "[?bdiva^2 + 1 = 2] (mod ?p)"
by (auto simp add: cong_def)
hence "[0 = 2] (mod ?p)" using h8 by (simp add: cong_def)
then have "?p dvd 2" by (auto dest: cong_dvd_iff)
then show False
by (auto dest: dvd_imp_le)
qed
private lemma sots1: assumes "is_sum2sq_nat n"
shows "⋀ k. prime (4*k+3) ⟶ even (multiplicity (4*k+3) n)"
using sots1_aux assms by blast
private lemma aux_lemma: assumes "[(a::nat) = b] (mod c)" "b < c"
shows "∃ k. a = c*k + b"
proof -
have "a mod c = b" using assms by (simp add: cong_def mod_if)
hence "b ≤ a" using assms by auto
thus ?thesis using cong_le_nat assms(1) by auto
qed
private lemma Legendre_1mod4: "prime (4*k+1::nat) ⟹ (Legendre (-1) (4*k+1)) = 1"
proof -
let ?p = "4*k+1"
let ?L = "Legendre (-1) ?p"
assume p: "prime ?p"
from p have "k ≠ 0" by (intro notI) simp_all
hence p2: "?p > 2" by simp
with p have "[?L = (-1)^((?p - 1) div 2)] (mod ?p)"
by (rule euler_criterion)
hence "[?L = (-1)^(2 * nat k)] (mod ?p)" by auto
hence "[?L = 1] (mod ?p)" unfolding power_mult by simp
hence "?p dvd 1-?L"
using cong_iff_dvd_diff dvd_minus_iff[of ?p "?L-1"] by auto
moreover have "?L=1 ∨ ?L=0 ∨ ?L=-1" by (simp add: Legendre_def)
ultimately have "?L = 1 ∨ ?p dvd 1 ∨ ?p dvd (2::int)" by auto
moreover
{ assume "?p dvd 1 ∨ ?p dvd (2::int)"
with p2 have False by (auto simp add: zdvd_not_zless) }
ultimately show ?thesis by auto
qed
private lemma qf1_prime_exists: "prime (4*k+1) ⟹ is_sum2sq_nat (4*k+1)"
proof -
let ?p = "4*k+1"
assume p: "prime ?p"
hence "Legendre (-1) ?p = 1" by (rule Legendre_1mod4)
moreover
{ assume "¬ QuadRes ?p (-1)"
hence "Legendre (-1) ?p ≠ 1" by (unfold Legendre_def, auto) }
ultimately have "QuadRes ?p (-1)" by auto
then obtain s1 where s1: "[s1^2 = -1] (mod ?p)" by (auto simp add: QuadRes_def)
hence s1': "[s1^2 + 1 = 0] (mod ?p)" by (simp add: cong_iff_dvd_diff)
define s2 where "s2 = nat ¦s1¦"
hence "int (s2^2 + 1) = s1^2 + 1" by auto
with s1' have "[int (s2^2 + 1) = 0] (mod ?p)" by presburger
hence s2: "[s2^2 + 1 = 0] (mod ?p)"
using cong_int_iff by fastforce
from p have p0: "?p > 0" by simp
then obtain s where s0p: "0 ≤ s ∧ s < ?p ∧ [s2 = s] (mod ?p)"
using cong_less_unique_nat[of ?p] by fastforce
then have "[s^2 = s2^2] (mod ?p)"
by (simp add: cong_sym cong_pow)
with s2 have s: "[s^2 + 1 = 0] (mod ?p)"
using cong_trans cong_add_rcancel_nat by blast
hence "?p dvd s^2 + 1" using cong_altdef_nat by auto
then obtain t where t: "s^2 + 1 = ?p*t" by (auto simp add: dvd_def)
hence "?p*t = sum2sq_nat s 1" by (simp add: sum2sq_nat_def)
hence qf1pt: "is_sum2sq_nat (?p*t)" by (auto simp add: is_sum2sq_nat_def)
have t_l_p: "t < ?p"
proof (rule ccontr)
assume "¬ t < ?p"
hence "t > ?p - 1" by simp
with p0 have "?p*(?p - 1) < ?p*t" by (simp only: mult_less_mono2)
also with t have "… = s^2 + 1" by simp
also have "… ≤ ?p*(?p - 1) - ?p + 2"
proof -
from s0p have "s ≤ ?p - 1" by (auto simp add: less_le)
with s0p have "s^2 ≤ (?p - 1)^2" by (simp only: power_mono)
also have "… = ?p*(?p - 1) - 1*(?p - 1)" by (simp only: power2_eq_square diff_mult_distrib)
finally show ?thesis by auto
qed
finally have "?p < 2" by simp
with p show False by (unfold prime_def, auto)
qed
have tpos: "t ≥ 1"
proof (rule ccontr)
assume "¬ t ≥ 1"
hence "t < 1" by auto
moreover
{ assume "t = 0" with t have "s^2 + 1 = 0" by simp }
moreover
{ assume "t < 0"
with p0 have "?p*t < ?p*0" by (simp only: zmult_zless_mono2)
with t have "s^2 + 1 < 0" by auto }
moreover have "s^2 ≥ 0" by (simp only: zero_le_power2)
ultimately show False by (auto simp add: less_le)
qed
moreover
{ assume t1: "t > 0"
then obtain tn where tn: "tn = t - 1" by auto
have "is_sum2sq_nat (?p*(1+ 0))" (is "?Q 0")
proof (rule ccontr)
assume nQ1: "¬ ?Q 0"
have "(1 + tn) < ?p ⟹ ¬ ?Q tn"
proof (induct tn rule: infinite_descent0)
case 0
from nQ1 show "1+ 0 < ?p ⟹ ¬ ?Q 0" by simp
next
case (smaller n)
hence n0: "n > 0" and IH: "1+ n < ?p ∧ ?Q n" by auto
then obtain x y where "x^2 + y^2 = int (?p*(1+ n))"
using is_sum2sq_int_nat_eq by (unfold is_sum2sq_int_def sum2sq_int_def, auto)
hence xy: "x^2 + y^2 = (int ?p)*(int (1+ n))" unfolding of_nat_mult by presburger
let ?n1 = "int (1 + n)"
from n0 have n1pos: "?n1 > 0" by simp
then obtain r v where rv: "v = x-r*?n1 ∧ 2*¦v¦ ≤ ?n1"
by (frule_tac n="?n1" in best_division_abs, auto)
from n1pos obtain s w where sw: "w = y-s*?n1 ∧ 2*¦w¦ ≤ ?n1"
by (frule_tac n="?n1" in best_division_abs, auto)
let ?C = "v^2 + w^2"
have "?n1 dvd ?C"
proof
from rv sw have "?C = (x-r*?n1)^2 + (y-s*?n1)^2" by simp
also have "… = x^2 + y^2 - 2*x*(r*?n1) - 2*y*(s*?n1) + (r*?n1)^2 + (s*?n1)^2"
unfolding power2_eq_square by (simp add: algebra_simps)
also with xy have "… = ?n1*?p - ?n1*(2*x*r) - ?n1*(2*y*s) + ?n1^2*r^2 + ?n1^2*s^2"
by (simp only: ac_simps power_mult_distrib)
finally show "?C = ?n1*(?p - 2*x*r - 2*y*s + ?n1*(r^2 + s^2))"
by (simp only: power_mult_distrib distrib_left ac_simps
left_diff_distrib right_diff_distrib power2_eq_square)
qed
then obtain m1 where m1: "?C = ?n1*m1" by (auto simp add: dvd_def)
have mn: "m1 < ?n1"
proof (rule ccontr)
assume "¬ m1 < ?n1" hence "?n1-m1 ≤ 0" by simp
hence "4*?n1 - 4*m1 ≤ 0" by simp
with n1pos have "2*?n1 - 4*m1 < 0" by simp
with n1pos have "?n1*(2*?n1 - 4*m1) < ?n1*0" by (simp only: zmult_zless_mono2)
hence contr: "?n1*(2*?n1- 4*m1) < 0" by simp
have hlp: "2*¦v¦ ≥ 0 ∧ 2*¦w¦ ≥ 0" by simp
from m1 have "4*?n1*m1 = 4*v^2 + 4*w^2" by arith
also have "… = (2*¦v¦)^2 + (2*¦w¦)^2"
by (auto simp add: power_mult_distrib)
also from rv hlp have "… ≤ ?n1^2 + (2*¦w¦)^2"
using power_mono [of "2*¦b¦" "1 + int n" 2 for b] by auto
also from sw hlp have "… ≤ ?n1^2 + ?n1^2"
using power_mono [of "2*¦b¦" "1 + int n" 2 for b] by auto
finally have "?n1*m1*4 ≤ ?n1*?n1*2" by (simp add: power2_eq_square ac_simps)
hence "?n1*(2*?n1- 4*m1) ≥ 0" by (simp only: right_diff_distrib ac_simps)
with contr show False by auto
qed
have "?p*m1 = (r*v + s*w + m1)^2 + (r*w - s*v)^2"
proof -
from m1 xy have "(?p*?n1)*?C = (x^2+y^2)*(v^2+w^2)" by simp
also have "… = (x*v + y*w)^2 + (x*w - y*v)^2"
by (simp add: eval_nat_numeral field_simps)
also with rv sw have "… = ((r*?n1+v)*v + (s*?n1+w)*w)^2 + ((r*?n1+v)*w - (s*?n1+w)*v)^2"
by simp
also have "… = (?n1*(r*v) + ?n1*(s*w) + (v^2+w^2))^2 + (?n1*(r*w) - ?n1*(s*v))^2"
by (simp add: eval_nat_numeral field_simps)
also from m1 have "… = (?n1*(r*v) + ?n1*(s*w) + ?n1*m1)^2 + (?n1*(r*w) - ?n1*(s*v))^2"
by simp
finally have "(?p*?n1)*?C = ?n1^2*(r*v + s*w + m1)^2 + ?n1^2*(r*w - s*v)^2"
by (simp add: eval_nat_numeral field_simps)
with m1 have "?n1^2*(?p*m1) = ?n1^2*((r*v + s*w + m1)^2 + (r*w - s*v)^2)"
by (simp only: ac_simps power2_eq_square, simp add: distrib_left)
hence "?n1^2*(?p*m1 - (r*v+s*w+m1)^2 - (r*w-s*v)^2) = 0"
by (auto simp add: distrib_left right_diff_distrib)
moreover from n1pos have "?n1^2 ≠ 0" by (simp add: power2_eq_square)
ultimately show ?thesis by simp
qed
hence qf1pm1: "is_sum2sq_int ((int ?p)*m1)"
by (unfold is_sum2sq_int_def sum2sq_int_def, auto)
have m1pos: "m1 > 0"
proof -
{ assume "v^2 + w^2 = 0"
hence "v = 0 ∧ w = 0" using sum_power2_eq_zero_iff by blast
with rv sw have "?n1 dvd x ∧ ?n1 dvd y" by (unfold dvd_def, auto)
hence "?n1^2 dvd x^2 ∧ ?n1^2 dvd y^2" by simp
hence "?n1^2 dvd x^2 + y^2" by (simp only: dvd_add)
with xy have "?n1*?n1 dvd ?n1*?p" by (simp only: power2_eq_square ac_simps)
moreover from n1pos have "?n1 ≠ 0" by simp
ultimately have "?n1 dvd ?p" by (rule zdvd_mult_cancel)
with n1pos have "?n1 ≥ 0 ∧ ?n1 dvd ?p" by simp
with p have "?n1 = 1 ∨ ?n1 = ?p" unfolding prime_nat_iff by presburger
with IH have "?Q 0" by auto
with nQ1 have False by simp }
moreover
{ assume "v^2 + 1*w^2 ≠ 0"
moreover have "v^2 + w^2 ≥ 0" by simp
ultimately have vwpos: "v^2 + w^2 > 0" by arith
with m1 have "m1 ≠ 0" by auto
moreover have "m1 ≥ 0"
proof (rule ccontr)
assume "¬ m1 ≥ 0"
hence "m1 < 0" by simp
with n1pos have "?n1*m1 < ?n1*0" by (simp only: zmult_zless_mono2)
with m1 vwpos show False by simp
qed
ultimately have ?thesis by auto }
ultimately show ?thesis by auto
qed
hence "1 + int((nat m1) - 1) = m1" by arith
with qf1pm1 have Qm1: "?Q ((nat m1) - 1)"
using is_sum2sq_int_nat_eq by (simp add: algebra_simps)
then obtain mm where tmp: "mm = (nat m1) - 1 ∧ ?Q mm" by auto
moreover have "mm<n" using tmp mn m1pos by arith
moreover with IH have "1 + int mm < ?p" by auto
ultimately show ?case by auto
qed
hence "¬ is_sum2sq_nat (?p*t)" using tn tpos t_l_p by auto
with qf1pt show False by simp
qed
hence ?thesis by auto }
ultimately show ?thesis by (auto simp add: less_le)
qed
private lemma fermat_two_squares: assumes "prime p" "(¬ [p = 3] (mod 4))"
shows "is_sum2sq_nat p"
proof (cases "p=2")
case True
have "(2::nat)=1^2+1^2" using power2_eq_square by simp
thus ?thesis unfolding is_sum2sq_nat_def sum2sq_nat_def using True by fast
next
case False
hence "p > 2" using assms(1) unfolding prime_nat_iff by auto
hence h1: "odd p" using assms(1) prime_odd_nat by simp
hence h2: "¬ [p = 0] (mod 4)" unfolding cong_def by fastforce
have h3: "¬ [p = 2] (mod 4)" using h1 cong_dvd_iff [of p 2 2] cong_dvd_modulus_nat by auto
obtain x where h4: "[p = x] (mod 4) ∧ x<4" by (meson cong_less_unique_nat zero_less_numeral)
from h1 h2 h3 h4 assms have "x≠0 ∧ x≠2 ∧ x≠3 ∧ x<4" by meson
hence "x=1" by linarith
from this h4 have "[p = 1] (mod 4)" by simp
then obtain k where "p = 4*k+1" using aux_lemma by fastforce
thus ?thesis using qf1_prime_exists assms by blast
qed
private lemma sots2: assumes "⋀ k. prime (4*k+3) ⟶ even (multiplicity (4*k+3) n)"
shows "is_sum2sq_nat n" using assms
proof (induction n rule: nat_less_induct)
case (1 n)
thus ?case
proof (cases "n>1")
case f: False
thus ?thesis
proof (cases "n=1")
case True
have "(1::nat)=0^2+1^2" by (simp add: power2_eq_square)
thus ?thesis using True unfolding is_sum2sq_nat_def sum2sq_nat_def by blast
next
case False
hence "n=0" using f by simp
moreover have "(0::nat)=0^2+0^2" by (simp add: power2_eq_square)
ultimately show ?thesis unfolding is_sum2sq_nat_def sum2sq_nat_def by blast
qed
next
case True
then obtain p m where h1: "prime p ∧ n = p * m" using prime_divisor_exists[of n]
by (auto elim: dvdE)
with True have m_nz: "m ≠ 0" by (intro notI) auto
from h1 have h2: "m<n" using n_less_m_mult_n[of m p] prime_gt_Suc_0_nat[of p] True by linarith
{
assume a1: "[p = 3] (mod 4)"
then obtain kp where "p = 4*kp+3" using aux_lemma by fastforce
hence "even (multiplicity p n)" using "1.prems" h1 by auto
moreover have "multiplicity p n ≠ 0" using h1 True m_nz
by (subst multiplicity_eq_zero_iff) (auto simp: prime_gt_0_nat)
ultimately have h3: "multiplicity p n ≥ 2" by presburger
have "p dvd m"
proof (rule ccontr)
assume a2: "¬ p dvd m"
hence "multiplicity p m = 0" by (rule not_dvd_imp_multiplicity_0)
moreover from h1 have "multiplicity p p = 1" by (intro multiplicity_prime) auto
moreover have "m > 0" using h1 True by (cases "m = 0") simp_all
ultimately have "multiplicity p n = 1" using h1
using prime_elem_multiplicity_mult_distrib [of p p m] m_nz prime_gt_0_nat
by auto
thus "False" using h3 by simp
qed
then obtain m' where h4: "m = p * m'" using dvdE by blast
with h1 have h5: "n = p^2 * m'" by (simp add: power2_eq_square)
have h6: "m'<n"
using dual_order.strict_trans h1 h2 h4 nat_mult_less_cancel1 prime_gt_0_nat[of p] by blast
have "⋀ kq. prime (4*kq + 3) ⟹ even (multiplicity (4*kq + 3) m')"
proof -
fix kq::nat
let ?q = "4*kq + 3"
assume a2: "prime ?q"
{
assume p: "p=?q"
hence h7: "multiplicity ?q (p^2) = 2" using h1
by (auto intro!: multiplicity_prime_power)
have "even (multiplicity ?q n)" using 1(2)[of kq] a2 by blast
also note h5
also from p h1 h4 m_nz
have "multiplicity (4 * kq + 3) (p^2 * m') =
Suc (Suc (multiplicity (4 * kq + 3) m'))"
by (subst prime_elem_multiplicity_mult_distrib) auto
finally have "even (multiplicity ?q m')" by simp
}
moreover {
assume "p≠?q"
from a2 h4 m_nz have "multiplicity ?q n =
multiplicity (4 * kq + 3) (p⇧2) + multiplicity (4 * kq + 3) m'"
unfolding h5 by (subst prime_elem_multiplicity_mult_distrib) simp_all
also from ‹p ≠ ?q› a2 h1 have "multiplicity ?q (p^2) = 0"
by (intro multiplicity_distinct_prime_power) simp_all
finally have "multiplicity ?q n = multiplicity ?q m'" by simp
moreover have "even (multiplicity ?q n)" using 1(2)[of kq] a2 by blast
ultimately have "even (multiplicity ?q m')" by simp
}
ultimately show "even (multiplicity ?q m')" by blast
qed
hence "is_sum2sq_nat m'" by (simp add: 1 h6)
moreover have "p^2 = p^2 + 0^2" by simp
hence "is_sum2sq_nat (p^2)" unfolding is_sum2sq_nat_def sum2sq_nat_def by blast
ultimately have ?thesis using product_two_squares_nat h5 by blast
} moreover
{
assume a1: "¬ [p = 3] (mod 4)"
have "⋀ kq. prime (4*kq+3) ⟹ even (multiplicity (4*kq+3) m)"
proof -
fix kq
let ?q = "4*(kq::nat) + 3"
assume a2: "prime ?q"
{ assume "p = ?q"
then have False using a1 cong_add_rcancel_0_nat [of "4 * kq" 3 4]
by (auto simp add: cong_def)
}
hence "p≠?q" ..
have "n = p * m" using h1 by simp
also from h1 a2 m_nz have "multiplicity ?q … =
multiplicity (4 * kq + 3) p + multiplicity (4 * kq + 3) m"
by (subst prime_elem_multiplicity_mult_distrib) (simp_all add: prime_gt_0_nat)
also from ‹p ≠ ?q› a2 h1 have "multiplicity ?q p = 0"
by (intro prime_multiplicity_other) simp_all
finally have "multiplicity ?q n = multiplicity ?q m" by simp
moreover have "even (multiplicity ?q n)" using 1(2)[of kq] a2 by blast
ultimately show "even (multiplicity ?q m)" by simp
qed
hence "is_sum2sq_nat m" by (simp add: 1 h2)
moreover have "is_sum2sq_nat p" using fermat_two_squares a1 h1 by blast
ultimately have ?thesis using product_two_squares_nat h1 by blast
} ultimately
show ?thesis by blast
qed
qed
theorem sum_of_two_squares:
"is_sum2sq_nat n ⟷ (∀ k. prime (4*k+3) ⟶ even (multiplicity (4*k+3) n))"
using sots1[of n] sots2[of n] by blast
private lemma k_mod_eq: "(∀p::nat. prime p ∧ [p = 3] (mod 4) ⟶ P p) = (∀k. prime (4*k+3) ⟶ P (4*k+3))"
proof
assume a1: "∀p. prime p ∧ [p = 3] (mod 4) ⟶ P p"
{
fix k :: nat
assume "prime (4 * k + 3)"
moreover hence "[4*k+3 = 3] (mod 4)"
by (simp add: cong_add_rcancel_0_nat cong_mult_self_left)
ultimately have "P (4 * k + 3)" using a1 by blast
}
thus "∀k. prime (4 * k + 3) ⟶ P (4 * k + 3)" by blast
next
assume a1: "∀k. prime (4 * k + 3) ⟶ P (4 * k + 3)"
{
fix p :: nat
assume "prime p" "[p = 3] (mod 4)"
moreover with aux_lemma obtain k where "p = 4*k+3" by fastforce
ultimately have "P p" using a1 by blast
}
thus "∀p. prime p ∧ [p = 3] (mod 4) ⟶ P p" by blast
qed
theorem sum_of_two_squares':
"is_sum2sq_nat n ⟷ (∀ p. prime p ∧ [p = 3] (mod 4) ⟶ even (multiplicity p n))"
using sum_of_two_squares k_mod_eq by presburger
theorem sum_of_two_squares_prime: assumes "prime p"
shows "is_sum2sq_nat p = [p≠3] (mod 4)"
proof (cases "[p=3] (mod 4)")
case True
have "odd (multiplicity p p)" using assms by simp
hence "¬ (is_sum2sq_nat p)" using assms True sum_of_two_squares' by blast
with True show ?thesis by simp
qed (simp add: fermat_two_squares assms)
end
end