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	|- Prime = ( NN i^i ( RPrime ` ZZring ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( Irred ` ZZring ) = ( Irred ` ZZring )
2	1	dfprm2	|- Prime = ( NN i^i ( Irred ` ZZring ) )
3		eqid	|- ( RPrime ` ZZring ) = ( RPrime ` ZZring )
4		zringpid	|- ZZring e. PID
5	4	a1i	|- ( T. -> ZZring e. PID )
6	3 1 5	rprmirredb	|- ( T. -> ( Irred ` ZZring ) = ( RPrime ` ZZring ) )
7	6	mptru	|- ( Irred ` ZZring ) = ( RPrime ` ZZring )
8	7	ineq2i	|- ( NN i^i ( Irred ` ZZring ) ) = ( NN i^i ( RPrime ` ZZring ) )
9	2 8	eqtri	|- Prime = ( NN i^i ( RPrime ` ZZring ) )