wheel840_accepts

formal source

 115  simpa [Nat.not_even_iff_odd] using (not_congr (chi8_eq_zero_iff_even n))
 116
 117/-- If `n` is coprime to `840`, then none of `2,3,5,7` divide `n`. -/
 118theorem wheel840_accepts (n : ℕ) (h : Nat.Coprime n wheel840) :
 119    (¬ 2 ∣ n) ∧ (¬ 3 ∣ n) ∧ (¬ 5 ∣ n) ∧ (¬ 7 ∣ n) := by
 120  have h2 : Nat.Coprime 2 n := (h.coprime_dvd_right (by native_decide : 2 ∣ wheel840)).symm
 121  have h3 : Nat.Coprime 3 n := (h.coprime_dvd_right (by native_decide : 3 ∣ wheel840)).symm
 122  have h5 : Nat.Coprime 5 n := (h.coprime_dvd_right (by native_decide : 5 ∣ wheel840)).symm
 123  have h7 : Nat.Coprime 7 n := (h.coprime_dvd_right (by native_decide : 7 ∣ wheel840)).symm
 124  refine ⟨?_, ?_, ?_, ?_⟩
 125  · exact (Nat.Prime.coprime_iff_not_dvd prime_two).1 h2
 126  · exact (Nat.Prime.coprime_iff_not_dvd prime_three).1 h3
 127  · exact (Nat.Prime.coprime_iff_not_dvd prime_five).1 h5
 128  · exact (Nat.Prime.coprime_iff_not_dvd (by decide : Nat.Prime 7)).1 h7
 129
 130/-! ### Complement: rejection when not coprime -/
 131
 132/-- Any prime divisor of `wheel840` is one of `2,3,5,7`. -/
 133theorem prime_dvd_wheel840 {p : ℕ} (hp : Prime p) (h : p ∣ wheel840) :
 134    p = 2 ∨ p = 3 ∨ p = 5 ∨ p = 7 := by
 135  have hp' : Nat.Prime p := (prime_iff p).1 hp
 136  have h840 : p ∣ (840 : ℕ) := by
 137    simpa [wheel840] using h
 138  have hprod : p ∣ 2^3 * 3 * 5 * 7 := by
 139    simpa [wheel840_factorization] using h840
 140  have h1 : p ∣ (2^3 * 3 * 5) ∨ p ∣ 7 := (hp'.dvd_mul).1 hprod
 141  rcases h1 with h235 | h7
 142  · have h2 : p ∣ (2^3 * 3) ∨ p ∣ 5 := (hp'.dvd_mul).1 h235
 143    rcases h2 with h23 | h5
 144    · have h3 : p ∣ 2^3 ∨ p ∣ 3 := (hp'.dvd_mul).1 h23
 145      rcases h3 with h2pow | h3
 146      · have h2 : p ∣ 2 := hp'.dvd_of_dvd_pow (m := 2) (n := 3) h2pow
 147        exact Or.inl ((Nat.prime_dvd_prime_iff_eq hp' prime_two).1 h2)
 148      · exact Or.inr (Or.inl ((Nat.prime_dvd_prime_iff_eq hp' prime_three).1 h3))