Theory Arith_Prog_Rel_Primes
section ‹Problem ARITHMETIC PROGRESSIONS (Putnam exam problems 2002)›
theory Arith_Prog_Rel_Primes
imports
Complex_Main
"HOL-Number_Theory.Number_Theory"
begin
text ‹
Statement of the problem (from ~\<^cite>‹"putnam"›): For which integers $n>1$ does the set of positive
integers less than and relatively prime to $n$ constitute an arithmetic progression?
The solution of the above problem is theorem @{text arith_prog_rel_primes_solution}.
First, we will require some auxiliary material before we get started with the actual
solution.
›
subsection ‹Auxiliary results›
lemma even_and_odd_parts:
fixes n::nat
assumes ‹n ≠ 0›
shows ‹∃ k q::nat. n = (2::nat)^k*q ∧ odd q›
proof-
have ‹prime (2::nat)›
by simp
thus ?thesis
using prime_power_canonical[where p = "2" and m = "n"]
assms semiring_normalization_rules(7) by auto
qed
lemma only_one_odd_div_power2:
fixes n::nat
assumes ‹n ≠ 0› and ‹⋀ x. x dvd n ⟹ odd x ⟹ x = 1›
shows ‹∃ k. n = (2::nat)^k›
by (metis even_and_odd_parts assms(1) assms(2) dvd_triv_left semiring_normalization_rules(11)
semiring_normalization_rules(7))
lemma coprime_power2:
fixes n::nat
assumes ‹n ≠ 0› and ‹⋀ x. x < n ⟹ (coprime x n ⟷ odd x)›
shows ‹∃ k. n = (2::nat)^k›
proof-
have ‹x dvd n ⟹ odd x ⟹ x = 1›
for x
by (metis neq0_conv One_nat_def Suc_1 Suc_lessI assms(1) assms(2) coprime_left_2_iff_odd
dvd_refl linorder_neqE_nat nat_dvd_1_iff_1 nat_dvd_not_less not_coprimeI)
thus ?thesis
using assms(1) only_one_odd_div_power2
by auto
qed
subsection ‹Main result›
text ‹
The solution to the problem ARITHMETIC PROGRESSIONS (Putnam exam problems 2002)
›
theorem arith_prog_rel_primes_solution:
fixes n :: nat
assumes ‹n > 1›
shows ‹(prime n ∨ (∃ k. n = 2^k) ∨ n = 6) ⟷
(∃ a b m. m ≠ 0 ∧ {x | x. x < n ∧ coprime x n} = {a+j*b| j::nat. j < m})›
proof-
have ‹ (prime n ∨ (∃ k. n = 2^k) ∨ n = 6) ⟷
(∃ b m. m ≠ 0 ∧ {x | x :: nat. x < n ∧ coprime x n} = {1+j*b| j::nat. j < m})›
proof
show "∃b m. m ≠ 0 ∧ {x |x. x < n ∧ coprime x n} = {1 + j * b |j. j < m}"
if "prime n ∨ (∃k. n = 2 ^ k) ∨ n = 6"
proof-
have "∃b m. m ≠ 0 ∧ {x |x. x < n ∧ coprime x n} = {1 + j * b |j. j < m}"
if "prime n"
proof-
have ‹∃m. m ≠ 0 ∧ {x | x :: nat. x < n ∧ coprime x n} = {1+j| j::nat. j < m}›
proof-
have ‹{x | x :: nat. x < n ∧ coprime x n} = {x | x :: nat. x ≠ 0 ∧ x < n}›
proof
show "{x |x. x < n ∧ coprime x n} ⊆ {x |x. x ≠ 0 ∧ x < n}"
using prime_nat_iff'' that by fastforce
show "{x |x. x ≠ 0 ∧ x < n} ⊆ {x |x. x < n ∧ coprime x n}"
using coprime_commute prime_nat_iff'' that
by fastforce
qed
obtain m where ‹m+1 = n›
using add.commute assms less_imp_add_positive by blast
have ‹{1+j| j::nat. j < (m::nat)} = {x | x :: nat. x ≠ 0 ∧ x < m+1}›
by (metis Suc_eq_plus1 ‹m + 1 = n› gr0_implies_Suc le_simps(3) less_nat_zero_code linorder_not_less nat.simps(3) nat_neq_iff plus_1_eq_Suc )
hence ‹{x | x :: nat. x < n ∧ coprime x n} = {1+j| j::nat. j < (m::nat)}›
using ‹{x | x :: nat. x < n ∧ coprime x n} = {x | x :: nat. x ≠ 0 ∧ x < n}› ‹m+1 = n›
by auto
from ‹n > 1› have ‹m ≠ 0›
using ‹m + 1 = n› by linarith
have ‹{x | x :: nat. x < n ∧ coprime x n} = {1+j| j::nat. j < m}›
using Suc_eq_plus1 ‹1 < n› ‹{x |x. x < n ∧ coprime x n} = {1 + j |j. j < m}›
by auto
hence ‹(∃ m. m ≠ 0 ∧ {x | x :: nat. x < n ∧ coprime x n} = {1+j| j::nat. j < m})›
using ‹m ≠ 0›
by blast
thus ?thesis by blast
qed
hence ‹∃m. m ≠ 0 ∧ {x | x :: nat. x < n ∧ coprime x n} = {1+j*1| j::nat. j < m}›
by auto
thus ?thesis
by blast
qed
moreover have "∃b m. m ≠ 0 ∧ {x |x. x < n ∧ coprime x n} = {1 + j * b |j. j < m}"
if "∃k. n = 2 ^ k"
proof-
obtain k where ‹n = 2 ^ k›
using ‹∃k. n = 2 ^ k› by auto
have ‹k ≠ 0›
by (metis ‹1 < n› ‹n = 2 ^ k› nat_less_le power.simps(1))
obtain t where ‹Suc t = k›
by (metis ‹k ≠ 0› fib.cases)
have ‹n = 2^(Suc t)›
by (simp add: ‹Suc t = k› ‹n = 2 ^ k›)
have ‹{x | x :: nat. x < n ∧ coprime x n} = {1+j*2| j::nat. j < 2^t}›
proof
show "{x |x. x < n ∧ coprime x n} ⊆ {1 + j * 2 |j. j < 2^t}"
proof
fix x
assume ‹x ∈ {x |x. x < n ∧ coprime x n}›
hence ‹x < n›
by blast
have ‹coprime x n›
using ‹x ∈ {x |x. x < n ∧ coprime x n}›
by blast
hence ‹coprime x (2^(Suc k))›
by (simp add: ‹k ≠ 0› ‹n = 2 ^ k›)
have ‹odd x›
using ‹coprime x n› ‹k ≠ 0› ‹n = 2 ^ k›
by auto
then obtain j where ‹x = 1+j*2›
by (metis add.commute add.left_commute left_add_twice mult_2_right oddE)
have ‹x < 2^k›
using ‹n = 2 ^ k› ‹x < n› ‹x = 1+j*2›
by linarith
hence ‹1+j*2 < 2^k›
using ‹x = 1+j*2›
by blast
hence ‹j < 2^t›
using ‹Suc t = k› by auto
thus ‹x ∈ {1 + j * 2 |j. j < 2^t}›
using ‹x = 1+j*2›
by blast
qed
show "{1 + j * 2 |j. j < 2 ^ t} ⊆ {x |x. x < n ∧ coprime x n}"
proof
fix x::nat
assume ‹x ∈ {1 + j * 2 |j. j < 2 ^ t}›
then obtain j where ‹x = 1 + j * 2› and ‹j < 2 ^ t›
by blast
have ‹x < 2*(2^t)›
using ‹x = 1 + j * 2› ‹j < 2 ^ t›
by linarith
hence ‹x < n›
by (simp add: ‹n = 2 ^ Suc t›)
moreover have ‹coprime x n›
by (metis (no_types) ‹⋀thesis. (⋀j. ⟦x = 1 + j * 2; j < 2 ^ t⟧ ⟹ thesis) ⟹ thesis› ‹n = 2 ^ k› coprime_Suc_left_nat coprime_mult_right_iff coprime_power_right_iff plus_1_eq_Suc)
ultimately show ‹x ∈ {x |x. x < n ∧ coprime x n}›
by blast
qed
qed
have ‹(2::nat)^(t::nat) ≠ 0›
by simp
obtain m where ‹m = (2::nat)^t› by blast
have ‹m ≠ 0›
using ‹m = 2 ^ t›
by auto
have ‹{x | x :: nat. x < n ∧ coprime x n} = {1+j*2| j::nat. j < m}›
using ‹m = 2 ^ t› ‹{x |x. x < n ∧ coprime x n} = {1 + j * 2 |j. j < 2 ^ t}›
by auto
from ‹m ≠ 0› ‹{x | x :: nat. x < n ∧ coprime x n} = {1+j*2| j::nat. j < m}›
show ?thesis by blast
qed
moreover have "∃b m. m ≠ 0 ∧ {x |x. x < n ∧ coprime x n} = {1 + j * b |j. j < m}"
if "n = 6"
proof-
have ‹{x | x. x < 6 ∧ coprime x 6} = {1+j*4| j::nat. j < 2}›
proof-
have ‹{x | x::nat. x < 6 ∧ coprime x 6} = {1, 5}›
proof
show "{u. ∃x. u = (x::nat) ∧ x < 6 ∧ coprime x 6} ⊆ {1, 5}"
proof
fix u::nat
assume ‹u ∈ {u. ∃x. u = x ∧ x < 6 ∧ coprime x 6}›
hence ‹coprime u 6›
by blast
have ‹u < 6›
using ‹u ∈ {u. ∃x. u = x ∧ x < 6 ∧ coprime x 6}›
by blast
moreover have ‹u ≠ 0›
using ‹coprime u 6› ord_eq_0
by fastforce
moreover have ‹u ≠ 2›
using ‹coprime u 6›
by auto
moreover have ‹u ≠ 3›
proof-
have ‹gcd (3::nat) 6 = 3›
by auto
thus ?thesis
by (metis (no_types) ‹coprime u 6› ‹gcd 3 6 = 3› coprime_iff_gcd_eq_1
numeral_eq_one_iff semiring_norm(86))
qed
moreover have ‹u ≠ 4›
proof-
have ‹gcd (4::nat) 6 = 2›
by (metis (no_types, lifting) add_numeral_left gcd_add1 gcd_add2 gcd_nat.idem
numeral_Bit0 numeral_One one_plus_numeral semiring_norm(4) semiring_norm(5))
thus ?thesis
using ‹coprime u 6› coprime_iff_gcd_eq_1
by auto
qed
ultimately have ‹u = 1 ∨ u = 5›
by auto
thus ‹u ∈ {1, 5}›
by blast
qed
show "{1::nat, 5} ⊆ {x |x. x < 6 ∧ coprime x 6}"
proof-
have ‹(1::nat) ∈ {x |x. x < 6 ∧ coprime x 6}›
by simp
moreover have ‹(5::nat) ∈ {x |x. x < 6 ∧ coprime x 6}›
by (metis Suc_numeral coprime_Suc_right_nat less_add_one mem_Collect_eq
numeral_plus_one semiring_norm(5) semiring_norm(8))
ultimately show ?thesis
by blast
qed
qed
moreover have ‹{1+j*4| j::nat. j < 2} = {1, 5}›
by auto
ultimately show ?thesis by auto
qed
moreover have ‹(2::nat) ≠ 0›
by simp
ultimately have ‹∃ m. m ≠ 0 ∧ {x | x :: nat. x < 6 ∧ coprime x 6} = {1+j*4| j::nat. j < m}›
by blast
thus ?thesis
using that
by auto
qed
ultimately show ?thesis
using that
by blast
qed
show "prime n ∨ (∃k. n = 2 ^ k) ∨ n = 6"
if "∃b m. m ≠ 0 ∧ {x |x. x < n ∧ coprime x n} = {1 + j * b |j. j < m}"
proof-
obtain b m where ‹m ≠ 0› and ‹{x |x. x < n ∧ coprime x n} = {1 + j * b |j. j < m}›
using ‹∃b m. m ≠ 0 ∧ {x |x. x < n ∧ coprime x n} = {1 + j * b |j. j < m}›
by auto
show ?thesis
proof(cases ‹n = 2›)
case True
thus ?thesis
by auto
next
case False
have ‹b ≤ 4›
proof(cases ‹odd b›)
case True
show ?thesis
proof(rule classical)
assume ‹¬(b ≤ 4)›
hence ‹b > 4›
using le_less_linear
by blast
obtain m where ‹m ≠ 0›
and ‹{x | x :: nat. x < n ∧ coprime x n} = {1+j*b| j::nat. j < m}›
using ‹m ≠ 0› ‹{x |x. x < n ∧ coprime x n} = {1 + j * b |j. j < m}›
by blast
have ‹b ≠ 0›
using ‹4 < b›
by linarith
have ‹n = 2 + (m-1)*b›
proof-
have ‹n-1 ∈ {x | x :: nat. x < n ∧ coprime x n}›
using ‹1 < n› coprime_diff_one_left_nat
by auto
have ‹n-1 ∈ {1+j*b| j::nat. j < m}›
using ‹n - 1 ∈ {x |x. x < n ∧ coprime x n}›
‹{x |x. x < n ∧ coprime x n} = {1 + j * b |j. j < m}›
by blast
then obtain i::nat where ‹n-1 = 1+i*b› and ‹i < m›
by blast
have ‹i ≤ m-1›
using ‹i < m›
by linarith
have ‹1 + (m-1)*b ∈ {1+j*b| j::nat. j < m}›
using ‹m ≠ 0›
by auto
hence ‹1 + (m-1)*b ∈ {x | x::nat. x < n ∧ coprime x n}›
using ‹{x |x. x < n ∧ coprime x n} = {1 + j * b |j. j < m}›
by blast
hence ‹1 + (m-1)*b < n›
by blast
hence ‹1 + (m-1)*b ≤ n-1›
by linarith
hence ‹1 + (m-1)*b ≤ 1+i*b›
using ‹n - 1 = 1 + i * b›
by linarith
hence ‹(m-1)*b ≤ i*b›
by linarith
hence ‹m-1 ≤ i›
using ‹b ≠ 0›
by auto
hence ‹m-1 = i›
using ‹i ≤ m - 1› le_antisym
by blast
thus ?thesis
using ‹m ≠ 0› ‹n - 1 = 1 + i * b›
by auto
qed
have ‹m ≥ 2›
using ‹n = 2 + (m - 1)*b› ‹n ≠ 2›
by auto
hence ‹1+b ∈ {1+j*b| j. j < m}›
by fastforce
hence ‹1+b ∈ {x | x::nat. x < n ∧ coprime x n}›
using ‹{x |x. x < n ∧ coprime x n} = {1 + j * b |j. j < m}›
by blast
hence ‹coprime (1+b) n›
by blast
have ‹(2::nat) dvd (1+b)›
using ‹odd b›
by simp
hence ‹coprime (2::nat) n›
using ‹coprime (1 + b) n› coprime_common_divisor coprime_left_2_iff_odd odd_one
by blast
have ‹(2::nat) < n›
using ‹1 < n› ‹n ≠ 2›
by linarith
have ‹2 ∈ {x | x :: nat. x < n ∧ coprime x n}›
using ‹2 < n› ‹coprime 2 n›
by blast
hence ‹2 ∈ {1+j*b| j::nat. j < m}›
using ‹{x |x. x < n ∧ coprime x n} = {1 + j * b |j. j < m}›
by blast
then obtain j::nat where ‹2 = 1+j*b›
by blast
have ‹1 = j*b›
using ‹2 = 1+j*b›
by linarith
thus ?thesis
by simp
qed
next
case False
hence ‹even b›
by simp
show ?thesis
proof(rule classical)
assume ‹¬(b ≤ 4)›
hence ‹b > 4›
using le_less_linear
by blast
obtain m where ‹ m ≠ 0›
and ‹{x | x::nat. x < n ∧ coprime x n} = {1+j*b| j::nat. j < m}›
using ‹m ≠ 0› ‹{x |x. x < n ∧ coprime x n} = {1 + j * b |j. j < m}›
by blast
have ‹b ≠ 0›
using ‹4 < b›
by linarith
have ‹n = 2 + (m-1)*b›
proof-
have ‹n-1 ∈ {x | x::nat. x < n ∧ coprime x n}›
using ‹1 < n› coprime_diff_one_left_nat
by auto
have ‹n-1 ∈ {1+j*b| j::nat. j < m}›
using ‹n - 1 ∈ {x |x. x < n ∧ coprime x n}›
‹{x |x. x < n ∧ coprime x n} = {1 + j * b |j. j < m}›
by blast
then obtain i::nat where ‹n-1 = 1+i*b› and ‹i < m›
by blast
have ‹i ≤ m-1›
using ‹i < m›
by linarith
have ‹1 + (m-1)*b ∈ {1+j*b| j::nat. j < m}›
using ‹m ≠ 0›
by auto
hence ‹1 + (m-1)*b ∈ {x | x :: nat. x < n ∧ coprime x n}›
using ‹{x |x. x < n ∧ coprime x n} = {1 + j * b |j. j < m}›
by blast
hence ‹1 + (m-1)*b < n›
by blast
hence ‹1 + (m-1)*b ≤ n-1›
by linarith
hence ‹1 + (m-1)*b ≤ 1+i*b›
using ‹n - 1 = 1 + i * b›
by linarith
hence ‹(m-1)*b ≤ i*b›
by linarith
hence ‹m-1 ≤ i›
using ‹b ≠ 0›
by auto
hence ‹m-1 = i›
using ‹i ≤ m - 1› le_antisym
by blast
thus ?thesis
using ‹m ≠ 0› ‹n - 1 = 1 + i * b›
by auto
qed
obtain k :: nat where ‹b = 2*k›
using ‹even b›
by blast
have ‹n = 2*(1 + (m-1)*k)›
using ‹n = 2 + (m-1)*b› ‹b = 2*k›
by simp
show ?thesis
proof (cases ‹odd m›)
case True
hence ‹odd m› by blast
then obtain t::nat where ‹m-1 = 2*t›
by (metis odd_two_times_div_two_nat)
have ‹n = 2*(1 + b*t)›
using ‹m - 1 = 2 * t› ‹n = 2 + (m - 1) * b›
by auto
have ‹t < m›
using ‹m - 1 = 2 * t› ‹m ≠ 0›
by linarith
have ‹1 + b*t ∈ {1+j*b| j::nat. j < m}›
using ‹t < m›
by auto
hence ‹1 + b*t ∈ {x | x::nat. x < n ∧ coprime x n}›
using ‹{x |x. x < n ∧ coprime x n} = {1 + j * b |j. j < m}›
by blast
hence ‹coprime (1 + b*t) n›
by auto
thus ?thesis
by (metis (no_types, lifting) ‹b = 2 * k› ‹n = 2 * (1 + (m - 1) * k)› ‹n = 2 * (1 + b * t)› ‹n = 2 + (m - 1) * b› ‹n ≠ 2› add_cancel_right_right coprime_mult_right_iff coprime_self mult_cancel_left mult_is_0 nat_dvd_1_iff_1)
next
case False
thus ?thesis
proof(cases ‹odd k›)
case True
hence ‹odd k›
by blast
have ‹even (1 + (m - 1) * k)›
by (simp add: False True ‹m ≠ 0›)
have ‹coprime (2 + (m - 1) * k) (1 + (m - 1) * k)›
by simp
have ‹coprime (2 + (m - 1) * k) n›
using ‹coprime (2 + (m - 1) * k) (1 + (m - 1) * k)› ‹even (1 + (m - 1) * k)›
‹n = 2 * (1 + (m - 1) * k)› coprime_common_divisor coprime_mult_right_iff
coprime_right_2_iff_odd odd_one
by blast
have ‹2 + (m - 1) * k < n›
by (metis (no_types, lifting) ‹even (1 + (m - 1) * k)› ‹n = 2 * (1 + (m - 1) * k)›
add_gr_0 add_mono_thms_linordered_semiring(1) dvd_add_left_iff dvd_add_triv_left_iff dvd_imp_le le_add2 le_neq_implies_less less_numeral_extra(1) mult_2 odd_one)
have ‹2 + (m - 1) * k ∈ {x | x :: nat. x < n ∧ coprime x n}›
using ‹2 + (m - 1) * k < n› ‹coprime (2 + (m - 1) * k) n›
by blast
hence ‹2 + (m - 1) * k ∈ {1 + j * b |j. j < m}›
using ‹{x |x. x < n ∧ coprime x n} = {1 + j * b |j. j < m}›
by blast
then obtain j::nat where ‹2 + (m - 1) * k = 1 + j * b› and ‹j < m›
by blast
have ‹1 + (m - 1) * k = j * b›
using ‹2 + (m - 1) * k = 1 + j * b›
by simp
hence ‹1 + (m - 1) * k = j * (2*k)›
using ‹b = 2 * k› by blast
thus ?thesis
by (metis ‹b = 2 * k› ‹even b› ‹n = 2 * (1 + (m - 1) * k)› ‹n = 2 + (m - 1) * b› dvd_add_times_triv_right_iff dvd_antisym dvd_imp_le dvd_triv_right even_numeral mult_2 zero_less_numeral)
next
case False
hence ‹even k› by auto
have ‹odd (1 + (m - 1) * k)›
by (simp add: ‹even k› )
hence ‹coprime (3 + (m - 1) * k) (1 + (m - 1) * k)›
by (smt (verit) add_numeral_left coprime_common_divisor coprime_right_2_iff_odd dvd_add_left_iff not_coprimeE numeral_Bit1 numeral_One numeral_plus_one one_add_one)
hence ‹coprime (3 + (m - 1) * k) n›
by (metis ‹even k› ‹n = 2 * (1 + (m - 1) * k)› coprime_mult_right_iff coprime_right_2_iff_odd even_add even_mult_iff odd_numeral)
have ‹3 + (m - 1) * k < n›
by (smt (verit) Groups.add_ac(2) ‹even k› ‹n = 2 * (1 + (m - 1) * k)› ‹n = 2 + (m - 1) * b› ‹n ≠ 2› add_Suc_right add_cancel_right_right add_mono_thms_linordered_semiring(1) dvd_imp_le even_add even_mult_iff le_add2 le_neq_implies_less left_add_twice mult_2 neq0_conv numeral_Bit1 numeral_One odd_numeral one_add_one plus_1_eq_Suc)
have ‹3 + (m - 1) * k ∈ {x |x. x < n ∧ coprime x n}›
using ‹3 + (m - 1) * k < n› ‹coprime (3 + (m - 1) * k) n›
by blast
hence ‹3 + (m - 1) * k ∈ {1 + j * b |j. j < m}›
using ‹{x |x. x < n ∧ coprime x n} = {1 + j * b |j. j < m}›
by blast
then obtain j::nat where ‹3 + (m - 1) * k = 1 + j * b›
by blast
have ‹2 + (m - 1) * k = j * b›
using ‹3 + (m - 1) * k = 1 + j * b›
by simp
hence ‹2 + (m - 1) * k = j * 2*k›
by (simp add: ‹b = 2 * k›)
thus ?thesis
by (metis ‹4 < b› ‹b = 2 * k› ‹even k› dvd_add_times_triv_right_iff dvd_antisym
dvd_triv_right mult_2 nat_neq_iff numeral_Bit0)
qed
qed
qed
qed
moreover have ‹b ≠ 3›
proof (rule classical)
assume ‹¬ (b ≠ 3)›
hence ‹b = 3›
by blast
obtain m where ‹m ≠ 0› and
‹{x | x::nat. x < n ∧ coprime x n} = {1+j*b| j::nat. j < m}›
using ‹m ≠ 0› ‹{x |x. x < n ∧ coprime x n} = {1 + j * b |j. j < m}›
by blast
have ‹b ≠ 0›
by (simp add: ‹b = 3›)
have ‹n = 2 + (m-1)*b›
proof-
have ‹n-1 ∈ {x | x::nat. x < n ∧ coprime x n}›
using ‹1 < n› coprime_diff_one_left_nat
by auto
have ‹n-1 ∈ {1+j*b| j::nat. j < m}›
using ‹n - 1 ∈ {x |x. x < n ∧ coprime x n}›
‹{x |x. x < n ∧ coprime x n} = {1 + j * b |j. j < m}›
by blast
then obtain i::nat where ‹n-1 = 1+i*b› and ‹i < m›
by blast
have ‹i ≤ m-1›
using ‹i < m›
by linarith
have ‹1 + (m-1)*b ∈ {1+j*b| j::nat. j < m}›
using ‹m ≠ 0›
by auto
hence ‹1 + (m-1)*b ∈ {x | x :: nat. x < n ∧ coprime x n}›
using ‹{x |x. x < n ∧ coprime x n} = {1 + j * b |j. j < m}›
by blast
hence ‹1 + (m-1)*b < n›
by blast
hence ‹1 + (m-1)*b ≤ n-1›
by linarith
hence ‹1 + (m-1)*b ≤ 1+i*b›
using ‹n - 1 = 1 + i * b›
by linarith
hence ‹(m-1)*b ≤ i*b›
by linarith
hence ‹m-1 ≤ i›
using ‹b ≠ 0›
by auto
hence ‹m-1 = i›
using ‹i ≤ m - 1› le_antisym
by blast
thus ?thesis
using ‹m ≠ 0› ‹n - 1 = 1 + i * b›
by auto
qed
have ‹n > 2›
using ‹1 < n› ‹n ≠ 2›
by linarith
hence ‹ m ≥ 2 › using ‹n = 2 + (m-1)*b› ‹b = 3›
by simp
have ‹4 ∈ {1+j*(b::nat)| j::nat. j < m}›
using ‹2 ≤ m› ‹b = 3›
by force
hence ‹(4::nat) ∈ {x | x :: nat. x < n ∧ coprime x n}›
using ‹{x |x. x < n ∧ coprime x n} = {1 + j * b |j. j < m}›
by auto
hence ‹coprime (4::nat) n›
by blast
have ‹(2::nat) dvd 4›
by auto
hence ‹coprime (2::nat) n›
using ‹coprime (4::nat) n› coprime_divisors dvd_refl
by blast
have ‹4 < n›
using ‹4 ∈ {x |x. x < n ∧ coprime x n}›
by blast
have ‹2 < (4::nat)›
by auto
have ‹2 < n›
by (simp add: ‹2 < n›)
hence ‹2 ∈ {x | x :: nat. x < n ∧ coprime x n}›
using ‹coprime (2::nat) n›
by blast
hence ‹2 ∈ {1+j*(b::nat)| j::nat. j < m}›
using ‹{x |x. x < n ∧ coprime x n} = {1 + j * b |j. j < m}›
by blast
then obtain j::nat where ‹2 = 1+j*3›
using ‹b = 3›
by blast
from ‹2 = 1+j*3›
have ‹1 = j*3›
by auto
hence ‹3 dvd 1›
by auto
thus ?thesis
using nat_dvd_1_iff_1 numeral_eq_one_iff
by blast
qed
ultimately have ‹b = 0 ∨ b = 1 ∨ b = 2 ∨ b = 4›
by auto
moreover have ‹b = 0 ⟹ ∃k. n = 2^k›
proof-
assume ‹b = 0›
have ‹{1 + j * b |j. j < m} = {1}›
using ‹b = 0› ‹m ≠ 0›
by auto
hence ‹{x |x. x < n ∧ coprime x n} = {1}›
using ‹{x |x. x < n ∧ coprime x n} = {1 + j * b |j. j < m}›
by blast
hence ‹n = 2›
proof-
have ‹n-1 ∈ {x | x :: nat. x < n ∧ coprime x n}›
using ‹1 < n› coprime_diff_one_left_nat
by auto
have ‹n-1 ∈ {1}›
using ‹n - 1 ∈ {x |x. x < n ∧ coprime x n}› ‹{x |x. x < n ∧ coprime x n} = {1}›
by blast
hence ‹n-1 = 1›
by blast
hence ‹n = 2›
by simp
thus ?thesis
by blast
qed
hence ‹n = 2^1›
by auto
thus ?thesis
by blast
qed
moreover have ‹b = 1 ⟹ prime n›
proof-
assume ‹b = 1›
have ‹x < n ⟹ x ≠ 0 ⟹ coprime x n›
for x
proof-
assume ‹x < n› and ‹x ≠ 0›
have ‹{1+j| j::nat. j < m} = {x | x::nat. x < m+1 ∧ x ≠ 0}›
by (metis (full_types) Suc_eq_plus1 add_mono1 less_Suc_eq_0_disj nat.simps(3) plus_1_eq_Suc )
hence ‹{x | x :: nat. x < n ∧ coprime x n} = {x | x :: nat. x < m+1 ∧ x ≠ 0}›
using ‹b = 1› ‹{x |x. x < n ∧ coprime x n} = {1 + j * b |j. j < m}›
by auto
have ‹coprime (n-1) n›
using ‹1 < n› coprime_diff_one_left_nat
by auto
have ‹n-1 < n›
using ‹1 < n›
by auto
have ‹n-1 ∈ {x |x. x < n ∧ coprime x n}›
using ‹coprime (n - 1) n› ‹n - 1 < n›
by blast
have ‹n-1 ≤ m›
by (metis (no_types, lifting) CollectD Suc_eq_plus1 Suc_less_eq2 ‹n - 1 ∈ {x |x. x < n ∧ coprime x n}› ‹{x |x. x < n ∧ coprime x n} = {x |x. x < m + 1 ∧ x ≠ 0}› leD le_less_linear not_less_eq_eq )
have ‹m ∈ {x | x :: nat. x < m+1 ∧ x ≠ 0}›
using ‹m ≠ 0›
by auto
have ‹m ∈ {x |x. x < n ∧ coprime x n} ›
using ‹m ∈ {x |x. x < m + 1 ∧ x ≠ 0}›
‹{x |x. x < n ∧ coprime x n} = {x |x. x < m + 1 ∧ x ≠ 0}›
by blast
have ‹m < n›
using ‹m ∈ {x |x. x < n ∧ coprime x n}›
by blast
have ‹m+1 = n›
using ‹m < n› ‹n - 1 ≤ m›
by linarith
have ‹x ∈ {x | x :: nat. x < m+1 ∧ x ≠ 0}›
using ‹m + 1 = n› ‹x < n› ‹x ≠ 0›
by blast
hence ‹x ∈ {x |x. x < n ∧ coprime x n}›
using ‹{x |x. x < n ∧ coprime x n} = {x |x. x < m + 1 ∧ x ≠ 0}›
by blast
thus ?thesis
by blast
qed
thus ?thesis
using assms coprime_commute nat_neq_iff prime_nat_iff'' by auto
qed
moreover have ‹b = 2 ⟹ ∃ k. n = 2^k›
proof-
assume ‹b = 2›
have ‹{x | x :: nat. x < n ∧ coprime x n} = {1+j*2| j::nat. j < m}›
using ‹b = 2› ‹{x |x. x < n ∧ coprime x n} = {1 + j * b |j. j < m}›
by auto
have ‹x < n ⟹ coprime x n ⟷ odd x›
for x::nat
proof-
assume ‹x < n›
have ‹coprime x n ⟹ odd x›
proof-
assume ‹coprime x n›
have ‹x ∈ {x | x :: nat. x < n ∧ coprime x n}›
by (simp add: ‹coprime x n› ‹x < n›)
hence ‹x ∈ {1+j*2| j::nat. j < m}›
using ‹{x |x. x < n ∧ coprime x n} = {1 + j * 2 |j. j < m}›
by blast
then obtain j where ‹x = 1+j*2›
by blast
thus ?thesis
by simp
qed
moreover have ‹odd x ⟹ coprime x n›
proof-
assume ‹odd x›
obtain j::nat where ‹x = 1+j*2›
by (metis ‹odd x› add.commute mult_2_right odd_two_times_div_two_succ one_add_one semiring_normalization_rules(16))
have ‹j < (n-1)/2›
using ‹x < n› ‹x = 1 + j * 2›
by linarith
have ‹n = 2*m›
proof-
have ‹(2::nat) ≠ 0›
by auto
have ‹n = 2+(m-1)*2›
proof-
have ‹n-1 ∈ {x | x :: nat. x < n ∧ coprime x n}›
using ‹1 < n› coprime_diff_one_left_nat
by auto
have ‹n-1 ∈ {1+j*b| j::nat. j < m}›
using ‹n - 1 ∈ {x |x. x < n ∧ coprime x n}›
‹{x |x. x < n ∧ coprime x n} = {1 + j * b |j. j < m}›
by blast
then obtain i::nat where ‹n-1 = 1+i*b› and ‹i < m›
by blast
have ‹i ≤ m-1›
using ‹i < m›
by linarith
have ‹1 + (m-1)*b ∈ {1+j*b| j::nat. j < m}›
using ‹m ≠ 0› by auto
hence ‹1 + (m-1)*b ∈ {x | x :: nat. x < n ∧ coprime x n}›
using ‹{x |x. x < n ∧ coprime x n} = {1 + j * b |j. j < m}›
by blast
hence ‹1 + (m-1)*b < n›
by blast
hence ‹1 + (m-1)*b ≤ n-1›
by linarith
hence ‹1 + (m-1)*b ≤ 1+i*b›
using ‹n - 1 = 1 + i * b›
by linarith
hence ‹(m-1)*b ≤ i*b›
by linarith
hence ‹m-1 ≤ i›
proof-
have ‹b ≠ 0›
using ‹b = 2›
by simp
thus ?thesis
using ‹(m - 1) * b ≤ i * b› mult_le_cancel2
by blast
qed
hence ‹m-1 = i›
using ‹i ≤ m - 1› le_antisym
by blast
thus ?thesis
using ‹m ≠ 0› ‹n - 1 = 1 + i * b›
by (simp add: ‹b = 2›)
qed
thus ?thesis
by (simp add: ‹m ≠ 0› ‹n = 2 + (m - 1) * 2› mult.commute mult_eq_if)
qed
hence ‹j < m›
using ‹x < n› ‹x = 1 + j * 2›
by linarith
hence ‹x ∈ {1+j*2| j::nat. j < m}›
using ‹x = 1 + j * 2›
by blast
hence ‹x ∈ {x | x :: nat. x < n ∧ coprime x n}›
using ‹{x |x. x < n ∧ coprime x n} = {1 + j * 2 |j. j < m}›
by blast
thus ?thesis
by blast
qed
ultimately show ?thesis
by blast
qed
thus ?thesis
using coprime_power2 assms
by auto
qed
moreover have ‹b = 4 ⟹ n = 6›
proof-
assume ‹b = 4›
have ‹n = 2 ∨ n = 6›
proof(rule classical)
assume ‹¬ (n = 2 ∨ n = 6)›
have ‹(4::nat) ≠ 0›
by auto
have ‹n = 2+(m-1)*4›
proof-
have ‹n-1 ∈ {x | x :: nat. x < n ∧ coprime x n}›
using ‹1 < n› coprime_diff_one_left_nat
by auto
have ‹n-1 ∈ {1+j*b| j::nat. j < m}›
using ‹n - 1 ∈ {x |x. x < n ∧ coprime x n}›
‹{x |x. x < n ∧ coprime x n} = {1 + j * b |j. j < m}›
by blast
then obtain i::nat where ‹n-1 = 1+i*b› and ‹i < m›
by blast
have ‹i ≤ m-1›
using ‹i < m›
by linarith
have ‹1 + (m-1)*b ∈ {1+j*b| j::nat. j < m}›
using ‹m ≠ 0›
by auto
hence ‹1 + (m-1)*b ∈ {x | x :: nat. x < n ∧ coprime x n}›
using ‹{x |x. x < n ∧ coprime x n} = {1 + j * b |j. j < m}›
by blast
hence ‹1 + (m-1)*b < n›
by blast
hence ‹1 + (m-1)*b ≤ n-1›
by linarith
hence ‹1 + (m-1)*b ≤ 1+i*b›
using ‹n - 1 = 1 + i * b›
by linarith
hence ‹(m-1)*b ≤ i*b›
by linarith
hence ‹m-1 ≤ i›
proof-
have ‹b ≠ 0›
using ‹b = 4› by auto
thus ?thesis
using ‹(m - 1) * b ≤ i * b› mult_le_cancel2
by blast
qed
hence ‹m-1 = i›
using ‹i ≤ m - 1› le_antisym
by blast
thus ?thesis
using ‹m ≠ 0› ‹n - 1 = 1 + i * b›
by (simp add: ‹b = 4›)
qed
hence ‹n = 4*m - 2›
by (simp add: ‹m ≠ 0› mult.commute mult_eq_if)
have ‹m ≥ 3›
using ‹¬ (n = 2 ∨ n = 6)› ‹n = 2 + (m - 1) * 4›
by auto
hence ‹ {1+j*4| j::nat. j < 3} ⊆ {1+j*4| j::nat. j < m}›
by force
hence ‹9 ∈ {1+j*4| j::nat. j < 3}›
by force
hence ‹9 ∈ {1+j*4| j::nat. j < m}›
using ‹ {1+j*4| j::nat. j < 3} ⊆ {1+j*4| j::nat. j < m}›
by blast
hence ‹9 ∈ {x | x :: nat. x < n ∧ coprime x n}›
using ‹b = 4› ‹{x |x. x < n ∧ coprime x n} = {1 + j * b |j. j < m}›
by auto
hence ‹coprime (9::nat) n›
by blast
have ‹(3::nat) dvd 9›
by auto
have ‹coprime (3::nat) n› using ‹coprime (9::nat) n› ‹(3::nat) dvd 9›
by (metis coprime_commute coprime_mult_right_iff dvd_def)
have ‹(3::nat) < n›
by (metis One_nat_def Suc_lessI ‹1 < n› ‹¬ (n = 2 ∨ n = 6)› ‹coprime 3 n›
coprime_self numeral_2_eq_2 numeral_3_eq_3 less_numeral_extra(1) nat_dvd_not_less)
have ‹3 ∈ {x | x :: nat. x < n ∧ coprime x n}›
using ‹3 < n› ‹coprime 3 n›
by blast
hence ‹(3::nat) ∈ {1+j*4| j::nat. j < m}›
using ‹b = 4› ‹{x |x. x < n ∧ coprime x n} = {1 + j * b |j. j < m}›
by blast
then obtain j::nat where ‹(3::nat) = 1 + j*4›
by blast
have ‹2 = j*4›
using numeral_3_eq_3 ‹(3::nat) = 1 + j*4›
by linarith
hence ‹1 = j*2›
by linarith
hence ‹even 1›
by simp
thus ?thesis
using odd_one
by blast
qed
thus ?thesis
by (simp add: False)
qed
ultimately show ?thesis
by blast
qed
qed
qed
moreover have ‹(∃ b m. m ≠ 0 ∧ {x | x :: nat. x < n ∧ coprime x n} = {1+j*b| j::nat. j < m})
⟷ (∃ a b m. m ≠ 0 ∧ {x | x :: nat. x < n ∧ coprime x n} = {a+j*b| j::nat. j < m})›
proof
show "∃a b m. m ≠ 0 ∧ {x |x. x < n ∧ coprime x n} = {a + j * b |j. j < m}"
if "∃b m. m ≠ 0 ∧ {x |x. x < n ∧ coprime x n} = {1 + j * b |j. j < m}"
using that
by blast
show "∃b m. m ≠ 0 ∧ {x |x. x < n ∧ coprime x n} = {1 + j * b |j. j < m}"
if "∃a b m. m ≠ 0 ∧ {x |x. x < n ∧ coprime x n} = {a + j * b |j. j < m}"
proof-
obtain a b m::nat where ‹m ≠ 0›
and ‹{x | x :: nat. x < n ∧ coprime x n} = {a+j*b| j::nat. j < m}›
using ‹∃a b m. m ≠ 0 ∧ {x |x. x < n ∧ coprime x n} = {a + j * b |j. j < m}›
by auto
have ‹a = 1›
proof-
have ‹{x | x :: nat. x < n ∧ coprime x n} = {(a::nat)+j*(b::nat)| j::nat. j < m} ⟹ a = 1›
proof-
have ‹Min {x | x :: nat. x < n ∧ coprime x n} = Min {a+j*b| j::nat. j < m}›
using ‹{x |x. x < n ∧ coprime x n} = {a + j * b |j. j < m}›
by auto
have ‹Min {x | x :: nat. x < n ∧ coprime x n} = 1›
proof-
have ‹finite {x | x :: nat. x < n ∧ coprime x n}›
by auto
have ‹{x | x :: nat. x < n ∧ coprime x n} ≠ {}›
using ‹1 < n› by auto
have ‹1 ∈ {x | x :: nat. x < n ∧ coprime x n}›
using ‹1 < n›
by auto
have ‹∀ x. coprime x n ⟶ x ≥ 1›
using ‹1 < n› le_less_linear
by fastforce
hence ‹∀ x. x < n ∧ coprime x n ⟶ x ≥ 1›
by blast
hence ‹∀ x ∈ {x | x :: nat. x < n ∧ coprime x n}. x ≥ 1›
by blast
hence ‹Min {x | x :: nat. x < n ∧ coprime x n} ≥ 1›
using ‹finite {x | x :: nat. x < n ∧ coprime x n}› ‹{x |x. x < n ∧ coprime x n} ≠ {}›
by auto
thus ?thesis
using Min_le ‹1 ∈ {x |x. x < n ∧ coprime x n}› ‹finite {x |x. x < n ∧ coprime x n}›
antisym by blast
qed
have ‹Min {a+j*b| j::nat. j < m} = a›
proof -
have f1: "∃n. a = a + n * b ∧ n < m"
using ‹m ≠ 0›
by auto
have f2: "∃n. 1 = a + n * b ∧ n < m"
using ‹{x |x. x < n ∧ coprime x n} = {a + j * b |j. j < m}› assms coprime_1_left
by blast
have f3: "∃na. a = na ∧ na < n ∧ coprime na n"
using f1 ‹{x |x. x < n ∧ coprime x n} = {a + j * b |j. j < m}› by blast
have "n ≠ 1"
by (metis (lifting) assms less_irrefl_nat)
then have "¬ coprime 0 n"
by simp
then show ?thesis
using f3 f2 by (metis ‹Min {x |x. x < n ∧ coprime x n} = 1› ‹{x |x. x < n ∧ coprime x n} = {a + j * b |j. j < m}› less_one linorder_neqE_nat not_add_less1)
qed
hence ‹Min {a+j*b| j::nat. j < m} = a› by blast
thus ?thesis
using ‹Min {x | x :: nat. x < n ∧ coprime x n} = 1› ‹Min {x | x :: nat. x < n ∧ coprime x n} = Min {a+j*b| j::nat. j < m}›
by linarith
qed
thus ?thesis
using ‹{x |x. x < n ∧ coprime x n} = {a + j * b |j. j < m}›
by blast
qed
thus ?thesis using ‹m ≠ 0› ‹{x | x. x < n ∧ coprime x n} = {a+j*b| j::nat. j < m}›
by auto
qed
qed
ultimately show ?thesis
by simp
qed
end