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	⊢ 𝐼 = ( Irred ‘ 𝑅 )
	irrednzr.2	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	irrednzr.3	⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
Assertion	irrednzr	⊢ ( 𝜑 → 𝑅 ∈ NzRing )

Proof

Step	Hyp	Ref	Expression
1		irrednzr.1	⊢ 𝐼 = ( Irred ‘ 𝑅 )
2		irrednzr.2	⊢ ( 𝜑 → 𝑅 ∈ Ring )
3		irrednzr.3	⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
4		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
5	1 4	irredcl	⊢ ( 𝑋 ∈ 𝐼 → 𝑋 ∈ ( Base ‘ 𝑅 ) )
6	3 5	syl	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝑅 ) )
7		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
8	1 7	irredn0	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ) → 𝑋 ≠ ( 0g ‘ 𝑅 ) )
9	2 3 8	syl2anc	⊢ ( 𝜑 → 𝑋 ≠ ( 0g ‘ 𝑅 ) )
10	6 9	eldifsnd	⊢ ( 𝜑 → 𝑋 ∈ ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) )
11	7 4	ringelnzr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) ) → 𝑅 ∈ NzRing )
12	2 10 11	syl2anc	⊢ ( 𝜑 → 𝑅 ∈ NzRing )