Theorem subrgccnzr

Description: A subring of the complex numbers is a nonzero ring. (Contributed by AV, 26-Oct-2026)

	Ref	Expression
Hypotheses	subrgcccrng.r	$$⊢R={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}S$$
	subrgcccrng.s	$$⊢S\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
Assertion	subrgccnzr	$$⊢R\in \mathrm{NzRing}$$

Proof

Step	Hyp	Ref	Expression
1		subrgcccrng.r	$$⊢R={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}S$$
2		subrgcccrng.s	$$⊢S\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
3	1 2	subrgcccrng	$$⊢R\in \mathrm{CRing}$$
4		crngring	$$⊢R\in \mathrm{CRing}\to R\in \mathrm{Ring}$$
5	3 4	ax-mp	$$⊢R\in \mathrm{Ring}$$
6		ax-1ne0	$$⊢1\ne 0$$
7	1 2	subrgcccrng1	$$⊢1=1_R$$
8	1 2	subrgcccrng0	$$⊢0=0_R$$
9	7 8	isnzr	$$⊢R\in \mathrm{NzRing}\leftrightarrow \left(R\in \mathrm{Ring}\wedge 1\ne 0\right)$$
10	5 6 9	mpbir2an	$$⊢R\in \mathrm{NzRing}$$