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

wheel840_accepts

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)

 118theorem wheel840_accepts (n : ℕ) (h : Nat.Coprime n wheel840) :
 119    (¬ 2 ∣ n) ∧ (¬ 3 ∣ n) ∧ (¬ 5 ∣ n) ∧ (¬ 7 ∣ n) := by

proof body

Term-mode proof.

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

depends on (18)

Lean names referenced from this declaration's body.