Theorem isprm

Description: The predicate "is a prime number". A prime number is a positive integer with exactly two positive divisors. (Contributed by Paul Chapman, 22-Jun-2011)

	Ref	Expression
Assertion	isprm	$$⊢P\in \mathbb{P}\leftrightarrow \left(P\in \mathbb{N}\wedge \left\{n\in \mathbb{N}|n\parallel P\right\}\approx 2_{𝑜}\right)$$

Proof

Step	Hyp	Ref	Expression
1		breq2	$$⊢p=P\to \left(n\parallel p\leftrightarrow n\parallel P\right)$$
2	1	rabbidv	$$⊢p=P\to \left\{n\in \mathbb{N}|n\parallel p\right\}=\left\{n\in \mathbb{N}|n\parallel P\right\}$$
3	2	breq1d	$$⊢p=P\to \left(\left\{n\in \mathbb{N}|n\parallel p\right\}\approx 2_{𝑜}\leftrightarrow \left\{n\in \mathbb{N}|n\parallel P\right\}\approx 2_{𝑜}\right)$$
4		df-prm	$$⊢\mathbb{P}=\left\{p\in \mathbb{N}|\left\{n\in \mathbb{N}|n\parallel p\right\}\approx 2_{𝑜}\right\}$$
5	3 4	elrab2	$$⊢P\in \mathbb{P}\leftrightarrow \left(P\in \mathbb{N}\wedge \left\{n\in \mathbb{N}|n\parallel P\right\}\approx 2_{𝑜}\right)$$