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	⊢ ℙ = ( ℕ ∩ ( RPrime ‘ ℤring ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( Irred ‘ ℤring ) = ( Irred ‘ ℤring )
2	1	dfprm2	⊢ ℙ = ( ℕ ∩ ( Irred ‘ ℤring ) )
3		eqid	⊢ ( RPrime ‘ ℤring ) = ( RPrime ‘ ℤring )
4		zringpid	⊢ ℤring ∈ PID
5	4	a1i	⊢ ( ⊤ → ℤring ∈ PID )
6	3 1 5	rprmirredb	⊢ ( ⊤ → ( Irred ‘ ℤring ) = ( RPrime ‘ ℤring ) )
7	6	mptru	⊢ ( Irred ‘ ℤring ) = ( RPrime ‘ ℤring )
8	7	ineq2i	⊢ ( ℕ ∩ ( Irred ‘ ℤring ) ) = ( ℕ ∩ ( RPrime ‘ ℤring ) )
9	2 8	eqtri	⊢ ℙ = ( ℕ ∩ ( RPrime ‘ ℤring ) )