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	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )