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	$$⊢\underset{\dot{}}{1}=1_R$$
	lringnz.2	$$⊢\underset{\dot{}}{0}=0_R$$
Assertion	lringnz	Could not format assertion : No typesetting found for |- ( R e. LRing -> .1. =/= .0. ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		lringnz.1	$$⊢\underset{\dot{}}{1}=1_R$$
2		lringnz.2	$$⊢\underset{\dot{}}{0}=0_R$$
3		lringnzr	Could not format ( R e. LRing -> R e. NzRing ) : No typesetting found for |- ( R e. LRing -> R e. NzRing ) with typecode |-
4	1 2	nzrnz	$$⊢R\in \mathrm{NzRing}\to \underset{\dot{}}{1}\ne \underset{\dot{}}{0}$$
5	3 4	syl	Could not format ( R e. LRing -> .1. =/= .0. ) : No typesetting found for |- ( R e. LRing -> .1. =/= .0. ) with typecode |-