This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ℙ \leftrightarrow (P \in ℕ \land \{n \in ℕ \| n ∥ P\} \approx 2_{𝑜})$

Proof

Step	Hyp	Ref	Expression
1		breq2	$⊢ p = P \to (n ∥ p \leftrightarrow n ∥ P)$
2	1	rabbidv	$⊢ p = P \to \{n \in ℕ \| n ∥ p\} = \{n \in ℕ \| n ∥ P\}$
3	2	breq1d	$⊢ p = P \to (\{n \in ℕ \| n ∥ p\} \approx 2_{𝑜} \leftrightarrow \{n \in ℕ \| n ∥ P\} \approx 2_{𝑜})$
4		df-prm	$⊢ ℙ = \{p \in ℕ \| \{n \in ℕ \| n ∥ p\} \approx 2_{𝑜}\}$
5	3 4	elrab2	$⊢ P \in ℙ \leftrightarrow (P \in ℕ \land \{n \in ℕ \| n ∥ P\} \approx 2_{𝑜})$