emirp_seventeen
plain-language theorem explainer
The declaration asserts that 17 and its digit reversal 71 are both prime with the two numbers distinct. Number theorists referencing emirp examples inside the Recognition Science arithmetic functions module would cite this fact. The proof reduces to a single native_decide invocation that discharges the primality checks by direct kernel evaluation.
Claim. $17$ is prime, $71$ is prime, and $17$ is distinct from $71$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. The local setting keeps statements minimal so that Dirichlet algebra can be added once basic interfaces stabilize. The Prime predicate is the repository-local transparent alias for the standard natural-number primality predicate.
proof idea
The proof is a term-mode one-line wrapper that applies native_decide to the conjunction of the two primality statements and the inequality.
why it matters
The result supplies a concrete emirp instance marked RS-relevant inside the primes arithmetic-functions file. No downstream theorems currently reference it. It contributes a small verified fact that can sit alongside Möbius footholds without invoking the forcing chain or phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.