Theorem irrednzr

Description: A ring with an irreducible element cannot be the zero ring. (Contributed by Thierry Arnoux, 18-May-2025)

	Ref	Expression
Hypotheses	irrednzr.1	|- I = ( Irred ` R )
	irrednzr.2	|- ( ph -> R e. Ring )
	irrednzr.3	|- ( ph -> X e. I )
Assertion	irrednzr	|- ( ph -> R e. NzRing )

Proof

Step	Hyp	Ref	Expression
1		irrednzr.1	|- I = ( Irred ` R )
2		irrednzr.2	|- ( ph -> R e. Ring )
3		irrednzr.3	|- ( ph -> X e. I )
4		eqid	|- ( Base ` R ) = ( Base ` R )
5	1 4	irredcl	|- ( X e. I -> X e. ( Base ` R ) )
6	3 5	syl	|- ( ph -> X e. ( Base ` R ) )
7		eqid	|- ( 0g ` R ) = ( 0g ` R )
8	1 7	irredn0	|- ( ( R e. Ring /\ X e. I ) -> X =/= ( 0g ` R ) )
9	2 3 8	syl2anc	|- ( ph -> X =/= ( 0g ` R ) )
10	6 9	eldifsnd	|- ( ph -> X e. ( ( Base ` R ) \ { ( 0g ` R ) } ) )
11	7 4	ringelnzr	|- ( ( R e. Ring /\ X e. ( ( Base ` R ) \ { ( 0g ` R ) } ) ) -> R e. NzRing )
12	2 10 11	syl2anc	|- ( ph -> R e. NzRing )