Theorem lringnz

Description: A local ring is a nonzero ring. (Contributed by Jim Kingdon, 20-Feb-2025) (Revised by SN, 23-Feb-2025)

	Ref	Expression
Hypotheses	lringnz.1	⊢ 1 = ( 1r ‘ 𝑅 )
	lringnz.2	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	lringnz	⊢ ( 𝑅 ∈ LRing → 1 ≠ 0 )

Proof

Step	Hyp	Ref	Expression
1		lringnz.1	⊢ 1 = ( 1r ‘ 𝑅 )
2		lringnz.2	⊢ 0 = ( 0g ‘ 𝑅 )
3		lringnzr	⊢ ( 𝑅 ∈ LRing → 𝑅 ∈ NzRing )
4	1 2	nzrnz	⊢ ( 𝑅 ∈ NzRing → 1 ≠ 0 )
5	3 4	syl	⊢ ( 𝑅 ∈ LRing → 1 ≠ 0 )