Theorem prmnn

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

	Ref	Expression
Assertion	prmnn	$$⊢P\in \mathbb{P}\to P\in \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		isprm	$$⊢P\in \mathbb{P}\leftrightarrow \left(P\in \mathbb{N}\wedge \left\{z\in \mathbb{N}|z\parallel P\right\}\approx 2_{𝑜}\right)$$
2	1	simplbi	$$⊢P\in \mathbb{P}\to P\in \mathbb{N}$$