Theorem dfprm3

Description: The (positive) prime elements of the integer ring are the prime numbers. (Contributed by Thierry Arnoux, 18-May-2025)

	Ref	Expression
Assertion	dfprm3	$$⊢\mathbb{P}=\mathbb{N}\cap \mathrm{RPrime}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\mathrm{Irred}\left({\mathbb{Z}}_{\mathrm{ring}}\right)=\mathrm{Irred}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
2	1	dfprm2	$$⊢\mathbb{P}=\mathbb{N}\cap \mathrm{Irred}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
3		eqid	$$⊢\mathrm{RPrime}\left({\mathbb{Z}}_{\mathrm{ring}}\right)=\mathrm{RPrime}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
4		zringpid	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{PID}$$
5	4	a1i	$$⊢\top \to {\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{PID}$$
6	3 1 5	rprmirredb	$$⊢\top \to \mathrm{Irred}\left({\mathbb{Z}}_{\mathrm{ring}}\right)=\mathrm{RPrime}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
7	6	mptru	$$⊢\mathrm{Irred}\left({\mathbb{Z}}_{\mathrm{ring}}\right)=\mathrm{RPrime}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
8	7	ineq2i	$$⊢\mathbb{N}\cap \mathrm{Irred}\left({\mathbb{Z}}_{\mathrm{ring}}\right)=\mathbb{N}\cap \mathrm{RPrime}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
9	2 8	eqtri	$$⊢\mathbb{P}=\mathbb{N}\cap \mathrm{RPrime}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$