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 ` R )
	lringnz.2	|- .0. = ( 0g ` R )
Assertion	lringnz	|- ( R e. LRing -> .1. =/= .0. )

Proof

Step	Hyp	Ref	Expression
1		lringnz.1	|- .1. = ( 1r ` R )
2		lringnz.2	|- .0. = ( 0g ` R )
3		lringnzr	|- ( R e. LRing -> R e. NzRing )
4	1 2	nzrnz	|- ( R e. NzRing -> .1. =/= .0. )
5	3 4	syl	|- ( R e. LRing -> .1. =/= .0. )