emirp_ninetyseven
plain-language theorem explainer
97 and its digit reversal 79 are both prime numbers and distinct. Researchers cataloging emirps or verifying small prime reversals would cite this explicit check. The proof is a direct native_decide invocation that reduces the statement to kernel-level evaluation of primality predicates.
Claim. $97$ is prime, $79$ is prime, and $97$ is not equal to $79$.
background
The module supplies lightweight wrappers for Mathlib arithmetic functions, beginning with the Möbius function. The local setting focuses on basic interfaces for Dirichlet algebra before deeper inversion results. The Prime predicate is the repository alias for the standard natural-number primality predicate from Mathlib.
proof idea
The proof is a one-line wrapper that applies native_decide to discharge the conjunction of primality statements and inequality.
why it matters
This supplies a concrete verified instance of an emirp within the number-theory layer. It supports downstream checks on prime-related arithmetic functions such as the Möbius function applied to emirps. No direct parent theorem is listed, and it touches the broader question of enumerating special primes in the Recognition framework's arithmetic scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.