Metamath Proof Explorer


Theorem prmnn

Description: A prime number is a positive integer. (Contributed by Paul Chapman, 22-Jun-2011)

Ref Expression
Assertion prmnn ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )

Proof

Step Hyp Ref Expression
1 isprm ( 𝑃 ∈ ℙ ↔ ( 𝑃 ∈ ℕ ∧ { 𝑧 ∈ ℕ ∣ 𝑧𝑃 } ≈ 2o ) )
2 1 simplbi ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )