prime_dvd_wheel840
plain-language theorem explainer
Any prime dividing the wheel number 840 must be 2, 3, 5 or 7. Number theorists working on sieve methods or wheel factorization cite this soundness lemma. The tactic proof rewrites divisibility of wheel840 to divisibility of 840, applies the explicit factorization 2^3 * 3 * 5 * 7, branches via repeated dvd_mul cases, and concludes each branch with prime_dvd_prime_iff_eq.
Claim. If $p$ is a prime natural number and $p$ divides the wheel number 840, then $p = 2$ or $p = 3$ or $p = 5$ or $p = 7$.
background
The module NumberTheory.Primes.Modular introduces modular arithmetic and wheel filters for primes. wheel840 is the integer 840, built as the product 2^3 * 3 * 5 * 7. The theorem records the soundness property that this wheel admits only those four primes as divisors. Module documentation states the complementary claim: if a number is coprime to 840, then it is not divisible by the small primes 2,3,5,7 that make up the wheel.
proof idea
The tactic proof first obtains Nat.Prime p via prime_iff. It rewrites p | wheel840 to p | 840, then applies wheel840_factorization to reach p | 2^3 * 3 * 5 * 7. Repeated use of hp'.dvd_mul splits the product into cases on the factors. Each terminal case invokes Nat.prime_dvd_prime_iff_eq (with prime_two, prime_three, prime_five, or a decided prime_seven) to obtain the required disjunct.
why it matters
The result is used by wheel840_rejects, which states that if n is not coprime to wheel840 then 2, 3, 5 or 7 divides n. It supplies the soundness half of the wheel filter in the modular primes section. In the Recognition framework the lemma supports discrete prime sieving that interfaces with the phi-ladder and the eight-tick octave, closing a modular-arithmetic prerequisite for later empirical-program checks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.