pith. machine review for the scientific record. sign in
theorem proved tactic proof

wheel840_rejects

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 157theorem wheel840_rejects (n : ℕ) (h : ¬ Nat.Coprime n wheel840) :
 158    2 ∣ n ∨ 3 ∣ n ∨ 5 ∣ n ∨ 7 ∣ n := by

proof body

Tactic-mode proof.

 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). -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (11)

Lean names referenced from this declaration's body.