Theorem dfprm2

Description: The positive irreducible elements of ZZ are the prime numbers. This is an alternative way to define Prime . (Contributed by Mario Carneiro, 5-Dec-2014) (Revised by AV, 10-Jun-2019)

	Ref	Expression
Hypothesis	prmirred.i	$$⊢I=\mathrm{Irred}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
Assertion	dfprm2	$$⊢\mathbb{P}=\mathbb{N}\cap I$$

Proof

Step	Hyp	Ref	Expression
1		prmirred.i	$$⊢I=\mathrm{Irred}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
2		prmnn	$$⊢x\in \mathbb{P}\to x\in \mathbb{N}$$
3	1	prmirredlem	$$⊢x\in \mathbb{N}\to \left(x\in I\leftrightarrow x\in \mathbb{P}\right)$$
4	3	bicomd	$$⊢x\in \mathbb{N}\to \left(x\in \mathbb{P}\leftrightarrow x\in I\right)$$
5	2 4	biadanii	$$⊢x\in \mathbb{P}\leftrightarrow \left(x\in \mathbb{N}\wedge x\in I\right)$$
6		elin	$$⊢x\in \left(\mathbb{N}\cap I\right)\leftrightarrow \left(x\in \mathbb{N}\wedge x\in I\right)$$
7	5 6	bitr4i	$$⊢x\in \mathbb{P}\leftrightarrow x\in \left(\mathbb{N}\cap I\right)$$
8	7	eqriv	$$⊢\mathbb{P}=\mathbb{N}\cap I$$