prime_seventeen
plain-language theorem explainer
The declaration asserts that 17 is prime in the natural numbers. It functions as one of the stable arithmetic anchors collected in RSConstants for repeated use in bridge lemmas involving the prime markers 11, 17, 37, 103, and 137. The proof reduces to a single decision procedure that verifies the property directly from the definition of primality.
Claim. The natural number 17 is prime.
background
The RSConstants module gathers small decidable arithmetic facts about integers such as 8, 45, 360, 840 and the prime markers 11, 17, 37, 103, 137. These serve as stable anchors that keep later bridge lemmas readable without re-proving the same arithmetic. Prime is the transparent alias for Nat.Prime.
proof idea
The proof is a one-line wrapper that invokes the decide tactic on the concrete instance of the Prime predicate at 17.
why it matters
This supplies a basic prime fact inside the RSConstants collection of decidable anchors. It supports the set of prime markers that recur in bridge lemmas, including those tied to the alpha band near 137. No downstream uses appear in the current dependency graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.