Theorem lringnzr

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

	Ref	Expression
Assertion	lringnzr	$$⊢R\in \mathrm{LRing}\to R\in \mathrm{NzRing}$$

Proof

Step	Hyp	Ref	Expression
1		df-lring	$$⊢\mathrm{LRing}=\left\{r\in \mathrm{NzRing}|\forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_r\left(x{+}_{r}y=1_r\to \left(x\in \mathrm{Unit}\left(r\right)\vee y\in \mathrm{Unit}\left(r\right)\right)\right)\right\}$$
2	1	ssrab3	$$⊢\mathrm{LRing}\subseteq \mathrm{NzRing}$$
3	2	sseli	$$⊢R\in \mathrm{LRing}\to R\in \mathrm{NzRing}$$