emirp_onehundredfortynine
plain-language theorem explainer
149 reversed is 941, and both numbers are prime while remaining distinct. Researchers cataloging emirps or reversible primes would cite this concrete numerical instance. The proof is a one-line term that invokes native_decide to evaluate the primality predicates and inequality directly in the kernel.
Claim. $149$ and $941$ are both prime and $149 ≠ 941$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Prime is the transparent alias for Nat.Prime. The declaration sits among sibling results on Möbius and big-Omega but records an isolated numerical fact rather than an arithmetic identity. Upstream results supply interface structures such as collision-free classes and algebraic tautologies, none of which are invoked in the present statement.
proof idea
The proof is a one-line term wrapper that applies native_decide to the conjunction of the two primality checks and the inequality.
why it matters
The result supplies a verified emirp example inside the number-theory layer. It feeds no downstream theorems. It touches the prime predicate but remains outside the Recognition forcing chain, RCL, and phi-ladder constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.