emirp_onehundredseven
plain-language theorem explainer
107 and its digit reversal 701 are distinct primes. Number theorists checking small emirps or populating prime tables would cite the fact. The proof reduces to a single native decision that evaluates the primality predicates by direct computation.
Claim. $107$ is prime, $701$ is prime, and $107$ is distinct from $701$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. This theorem records a concrete emirp instance inside the primes subsection. It depends on the transparent alias Prime for the standard predicate Nat.Prime on natural numbers.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to discharge the conjunction by direct evaluation.
why it matters
The result supplies a verified emirp datum in the arithmetic-functions file. It has no downstream citations yet and sits outside the main Recognition forcing chain or RCL. It simply populates a small concrete fact in the number-theory layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.