emirp_seventythree
plain-language theorem explainer
73 reversed is 37, with both numbers prime and distinct. Number theorists working on emirp pairs or explicit prime reversals would cite this case. The proof applies a native decision procedure that evaluates the conjunction directly.
Claim. $73$ is prime, its digit reversal $37$ is prime, and $73$ differs from $37$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Prime is the transparent alias for the standard Nat.Prime predicate on natural numbers. The local setting keeps statements minimal, deferring deeper Dirichlet inversion until basic interfaces stabilize.
proof idea
The proof is a one-line wrapper that invokes the native_decide tactic to resolve the primality conjunction and inequality by direct evaluation.
why it matters
This supplies a concrete numerical fact inside the primes subsection of the arithmetic functions module. It has no downstream uses and does not feed any parent theorem. The declaration touches only the explicit-computation layer and does not engage the forcing chain, J-uniqueness, or phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.