From fbb15f176ffaa02b8e7d427fc3c8a15cb9ae354d Mon Sep 17 00:00:00 2001 From: WLZPro Date: Fri, 5 Jul 2024 15:57:26 +0800 Subject: [PATCH] [Imo2003P6] Add proof --- Compfiles/Imo2003P6.lean | 228 ++++++++++++++++++++++++++++++++++++++- 1 file changed, 225 insertions(+), 3 deletions(-) diff --git a/Compfiles/Imo2003P6.lean b/Compfiles/Imo2003P6.lean index cd17326c..35255cab 100644 --- a/Compfiles/Imo2003P6.lean +++ b/Compfiles/Imo2003P6.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2023 David Renshaw. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: David Renshaw +Authors: David Renshaw, Zhiyi Luo -/ import Mathlib.Tactic @@ -20,6 +20,228 @@ by q. namespace Imo2003P6 -problem imo2003_p6 (p : Nat) (hp : p.Prime) : +open Finset + +snip begin + +lemma exists_prime_mod_m_ne_1_and_dvd + {n m : Nat} (npos : n ≠ 0) (hn : n % m ≠ 1) (hm : m ≠ 1) + : ∃ p : Nat, p.Prime ∧ p ∣ n ∧ p % m ≠ 1 := by + by_contra! h + let l := n.factors + have : ∀ p ∈ l, p % m = 1 := by + intro p pl + exact h _ (Nat.prime_of_mem_factors pl) (Nat.dvd_of_mem_factors pl) + have : n % m = 1 := calc n % m + _ = l.prod % m := by rw [Nat.prod_factors npos] + _ = (l.map (fun p ↦ p % m)).prod % m := List.prod_nat_mod l m + _ = (l.map (fun p ↦ 1)).prod % m := by rw [List.map_inj_left.mpr this] + _ = 1 % m := by rw [List.prod_eq_one (by simp)] + _ = 1 := Nat.one_mod_of_ne_one hm + contradiction + +snip end + +-- Direct translation of https://artofproblemsolving.com/community/c6h98p279 +problem imo2003_p6 (p : ℕ) (hp : p.Prime) : ∃ q : ℕ, q.Prime ∧ ∀ n, ¬((q : ℤ) ∣ (n : ℤ)^p - (p : ℤ)) := by - sorry + + rcases Nat.Prime.eq_two_or_odd hp with rfl | p_odd + + · -- p = 2 + use 5 + constructor + · exact Nat.prime_five + + intro n + by_contra hdvd + + let m := n % 5 + have : 0 ≤ m := Int.emod_nonneg n (by norm_num) + have : m < 5 := Int.emod_lt_of_pos n (by norm_num) + + have : 2 ≡ m ^ 2 [ZMOD 5] := calc + 2 ≡ n ^ 2 [ZMOD 5] := Int.modEq_iff_dvd.mpr hdvd + _ ≡ m ^ 2 [ZMOD 5] := Int.ModEq.pow 2 (Int.mod_modEq n 5).symm + have : 5 ∣ m ^ 2 - 2 := Int.dvd_sub_of_emod_eq (id (Int.ModEq.symm this)) + + interval_cases m <;> norm_num at this + + -- p > 2 + let N := ∑ i in range p, p^i + have N_nz : N ≠ 0 := by + apply Nat.ne_zero_iff_zero_lt.mpr + apply sum_pos + · exact fun _ _ ↦ Nat.pow_pos (Nat.Prime.pos hp) + exact nonempty_range_iff.mpr hp.ne_zero + + have p_ge_3 : p - 1 > 1 := by + by_contra h + simp at h + interval_cases p <;> norm_num at hp p_odd + + have N_mod_p_ne_1 : N % (p ^ 2) ≠ 1 := by + have : (p + 1) % (p ^ 2) = p + 1 := by + have : p + 1 < p ^ 2 := by + suffices 1 < p ^ 2 - p by exact Nat.add_lt_of_lt_sub' this + calc + 1 < p * (p - 1) := by + apply Nat.one_lt_mul_iff.mpr + exact ⟨Nat.Prime.pos hp, by simp [hp.one_lt], Or.inl hp.one_lt⟩ + _ = p ^ 2 - p := by simp [Nat.pow_two, Nat.mul_sub] + exact Nat.mod_eq_of_lt this + have : ∀ m ≥ 2, (∑ i in range m, p^i) % (p ^ 2) = p + 1 := by + intro m hm + cases' m with m; norm_num at hm + cases' m with m; norm_num at hm + induction' m with m ih + · simpa + simp at * + rw [sum_range_succ, Nat.add_mod, ih] + rw [Nat.mod_eq_zero_of_dvd (pow_dvd_pow p (by simp))] + simpa + rw [this _ (Nat.Prime.two_le hp)] + simp [Nat.Prime.ne_zero hp] + + have p_sq_ne_1 : p ^ 2 ≠ 1 := by + refine Ne.symm (Nat.ne_of_lt ?_) + apply one_lt_pow (Nat.Prime.one_lt hp) (by norm_num) + + rcases exists_prime_mod_m_ne_1_and_dvd + N_nz N_mod_p_ne_1 p_sq_ne_1 with ⟨q, ⟨hq, hqN, h3⟩⟩ + + have q_dvd_pp_1 : q ∣ p^p - 1 := calc + q ∣ N := hqN + _ ∣ p^p - 1 := by + use p - 1 + simp [N] + apply Nat.add_one_inj.mp + have : p^p - 1 + 1 = p^p := Nat.sub_add_cancel (Nat.one_le_pow _ _ hp.pos) + rw [this] + have : p = p - 1 + 1 := (Nat.succ_pred_prime hp).symm + nth_rw 1 [this]; nth_rw 4 [this] + rw [geom_sum_mul_add (p - 1) p] + + use q + constructor + · exact hq + + intro n hn + + have np_congr_p : (n : ZMod q) ^ p = p := by + rw [← Int.cast_pow, ← AddCommGroupWithOne.intCast_ofNat p] + rw [← (ZMod.intCast_eq_intCast_iff_dvd_sub _ _ _).mpr hn] + + have pp_congr_1 : (p : ZMod q) ^ p = (1 : ZMod q) := by + rw [← Nat.cast_pow, ← Nat.cast_one] + apply (ZMod.natCast_eq_natCast_iff' _ _ _).mpr + apply Eq.symm + apply (Nat.modEq_iff_dvd' _).mpr + · exact q_dvd_pp_1 + exact hp.one_le.trans (Nat.le_self_pow hp.ne_zero _) + + have : (n : ZMod q) ^ (p ^ 2) = 1 := by + rw [Nat.pow_two, pow_mul] + rw [np_congr_p, pp_congr_1] + + let d := orderOf (n : ZMod q) + + have : d ∣ p ^ 2 := orderOf_dvd_of_pow_eq_one this + rcases (Nat.dvd_prime_pow hp).mp this with ⟨k, ⟨k_le, d_eq_pk⟩⟩ + rcases Nat.lt_or_eq_of_le k_le with hk | rfl + + · -- k < 2 + have : (n : ZMod q) ^ p = ((1 : ℕ) : ZMod q) := by + rw [Nat.cast_one] + interval_cases k + all_goals simp at d_eq_pk + · -- k = 0 + simp [orderOf_eq_one_iff.mp d_eq_pk] + · -- k = 1 + rw [← d_eq_pk] + exact pow_orderOf_eq_one _ + have : (p : ZMod q) = ((1 : ℕ) : ZMod q) := by + rw [← Nat.cast_one] + exact (np_congr_p.symm).trans this + have : p ≡ 1 [MOD q] := (ZMod.natCast_eq_natCast_iff _ _ _).mp this + have q_dvd_p_1 : q ∣ p - 1 := (Nat.modEq_iff_dvd' hp.one_le).mp (id (Nat.ModEq.symm this)) + + have one_mod_p_1 : 1 % (p - 1) = 1 := + (Nat.mod_eq_iff_lt (by linarith [hp.ne_one])).mpr p_ge_3 + have p_mod_p_1 : p % (p - 1) = 1 := by + rw [Nat.mod_eq_sub_mod] + · have : p - (p - 1) = 1 := Nat.sub_sub_self hp.one_le + simp [this, one_mod_p_1] + · exact Nat.sub_le _ _ + have : N % (p - 1) = 1 := calc N % (p - 1) + _ = (∑ i in range p, (p^i) % (p - 1)) % (p - 1) := Finset.sum_nat_mod _ _ _ + _ = (∑ i in range p, 1) % (p - 1) := by + congr; funext i + simp [Nat.pow_mod, one_mod_p_1, p_mod_p_1] + _ = 1 := by simp [p_mod_p_1] + have : Nat.gcd N (p - 1) = 1 := + calc Nat.gcd N (p - 1) + _ = Nat.gcd (N % (p - 1)) (p - 1) := (Nat.mod_modEq _ _).symm.gcd_eq + _ = 1 := by + rw [this] + exact Nat.gcd_one_left _ + + have : q ≤ 1 := by + apply Nat.le_of_dvd (by norm_num) + rw [← this] + exact Nat.dvd_gcd hqN q_dvd_p_1 + + linarith [this, hq.one_lt] + + -- k = 2 + rcases eq_zero_or_neZero (n : ZMod q) with hn0 | hn0 + · -- n = 0 (mod q) + have : (p : ZMod q) = 0 := + calc (p : ZMod q) + _ = (n : ZMod q) ^ p := by rw [np_congr_p] + _ = 0 := by + rw [hn0, zero_pow (Nat.Prime.ne_zero hp)] + have q_dvd_p : q ∣ p := by + apply Nat.dvd_of_mod_eq_zero + rw [← Nat.zero_mod p] + change p ≡ 0 [MOD q] + apply (ZMod.natCast_eq_natCast_iff _ _ _).mp + rw [this, ← AddMonoidWithOne.natCast_zero] + + have : N % p = 1 := calc N % p + _ = (∑ i in range p, (p^i) % p) % p := Finset.sum_nat_mod _ _ _ + _ = (∑ i in range (p - 1 + 1), (p^i) % p) % p := by + nth_rw 1 [← Nat.succ_pred_prime hp] + simp + _ = (∑ i in range (p - 1), p^(i+1) % p + 1) % p := by + simp [Finset.sum_range_succ'] + _ = (∑ i in range (p - 1), 0 + 1) % p := by + congr; funext i + apply Nat.mod_eq_zero_of_dvd + exact Dvd.intro_left (p.pow i) rfl + _ = 1 := by + simp + rw [Nat.one_mod_of_ne_one (Nat.Prime.ne_one hp)] + have : Nat.gcd N p = 1 := + calc Nat.gcd N p + _ = Nat.gcd (N % p) p := (Nat.mod_modEq _ _).symm.gcd_eq + _ = 1 := by rw [this, Nat.gcd_one_left] + + have : q ≤ 1 := by + apply Nat.le_of_dvd (by norm_num) + rw [← this] + exact Nat.dvd_gcd hqN q_dvd_p + + linarith [this, hq.one_lt] + + · -- n ≠ 0 (mod q) + have : p ^ 2 ∣ q - 1 := by + rw [← d_eq_pk] + apply orderOf_dvd_of_pow_eq_one + apply @ZMod.pow_card_sub_one_eq_one _ (Fact.mk hq) _ hn0.out + have : (q - 1) % (p ^ 2) = 0 := Nat.mod_eq_zero_of_dvd this + have : q % (p ^ 2) = 1 := by + rw [← Nat.succ_pred_prime hq] + simp [Nat.add_mod, this] + exact Nat.one_mod_of_ne_one p_sq_ne_1 + contradiction