wheel840_rejects

formal source

 154    exact Or.inr (Or.inr (Or.inr ((Nat.prime_dvd_prime_iff_eq hp' h7prime).1 h7)))
 155
 156/-- If `n` is **not** coprime to `840`, then at least one of `2,3,5,7` divides `n`. -/
 157theorem wheel840_rejects (n : ℕ) (h : ¬ Nat.Coprime n wheel840) :
 158    2 ∣ n ∨ 3 ∣ n ∨ 5 ∣ n ∨ 7 ∣ n := by
 159  have hg_ne_one : Nat.gcd n wheel840 ≠ 1 := by
 160    intro hg
 161    apply h
 162    exact (Nat.coprime_iff_gcd_eq_one).2 hg
 163  obtain ⟨p, hpprime, hpdvg⟩ :=
 164    (Nat.ne_one_iff_exists_prime_dvd (n := Nat.gcd n wheel840)).1 hg_ne_one
 165  have hpdvn : p ∣ n := hpdvg.trans (Nat.gcd_dvd_left n wheel840)
 166  have hpdv840 : p ∣ wheel840 := hpdvg.trans (Nat.gcd_dvd_right n wheel840)
 167  have hp : Prime p := by
 168    simpa [Prime] using hpprime
 169  have hp_cases : p = 2 ∨ p = 3 ∨ p = 5 ∨ p = 7 :=
 170    prime_dvd_wheel840 (p := p) hp hpdv840
 171  rcases hp_cases with hp2 | hp_rest
 172  · left
 173    simpa [hp2] using hpdvn
 174  · rcases hp_rest with hp3 | hp_rest2
 175    · exact Or.inr (Or.inl (by simpa [hp3] using hpdvn))
 176    · rcases hp_rest2 with hp5 | hp7
 177      · exact Or.inr (Or.inr (Or.inl (by simpa [hp5] using hpdvn)))
 178      · exact Or.inr (Or.inr (Or.inr (by simpa [hp7] using hpdvn)))
 179
 180/-- A gcd-form of `wheel840_rejects` (sometimes more convenient in proofs). -/
 181theorem wheel840_rejects_of_gcd_ne_one (n : ℕ) (h : Nat.gcd n wheel840 ≠ 1) :
 182    2 ∣ n ∨ 3 ∣ n ∨ 5 ∣ n ∨ 7 ∣ n := by
 183  apply wheel840_rejects (n := n)
 184  intro hc
 185  apply h
 186  exact (Nat.coprime_iff_gcd_eq_one).1 hc
 187