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=\mathrm{Irred}\left(R\right)$$
	irrednzr.2	$$⊢\phi \to R\in \mathrm{Ring}$$
	irrednzr.3	$$⊢\phi \to X\in I$$
Assertion	irrednzr	$$⊢\phi \to R\in \mathrm{NzRing}$$

Proof

Step	Hyp	Ref	Expression
1		irrednzr.1	$$⊢I=\mathrm{Irred}\left(R\right)$$
2		irrednzr.2	$$⊢\phi \to R\in \mathrm{Ring}$$
3		irrednzr.3	$$⊢\phi \to X\in I$$
4		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
5	1 4	irredcl	$$⊢X\in I\to X\in {\mathrm{Base}}_R$$
6	3 5	syl	$$⊢\phi \to X\in {\mathrm{Base}}_R$$
7		eqid	$$⊢0_R=0_R$$
8	1 7	irredn0	$$⊢\left(R\in \mathrm{Ring}\wedge X\in I\right)\to X\ne 0_R$$
9	2 3 8	syl2anc	$$⊢\phi \to X\ne 0_R$$
10	6 9	eldifsnd	$$⊢\phi \to X\in \left({\mathrm{Base}}_R\setminus \left\{0_R\right\}\right)$$
11	7 4	ringelnzr	$$⊢\left(R\in \mathrm{Ring}\wedge X\in \left({\mathrm{Base}}_R\setminus \left\{0_R\right\}\right)\right)\to R\in \mathrm{NzRing}$$
12	2 10 11	syl2anc	$$⊢\phi \to R\in \mathrm{NzRing}$$