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 = ( CCfld |`s S )
	subrgcccrng.s	|- S e. ( SubRing ` CCfld )
Assertion	subrgccnzr	|- R e. NzRing

Proof

Step	Hyp	Ref	Expression
1		subrgcccrng.r	|- R = ( CCfld |`s S )
2		subrgcccrng.s	|- S e. ( SubRing ` CCfld )
3	1 2	subrgcccrng	|- R e. CRing
4		crngring	|- ( R e. CRing -> R e. Ring )
5	3 4	ax-mp	|- R e. Ring
6		ax-1ne0	|- 1 =/= 0
7	1 2	subrgcccrng1	|- 1 = ( 1r ` R )
8	1 2	subrgcccrng0	|- 0 = ( 0g ` R )
9	7 8	isnzr	|- ( R e. NzRing <-> ( R e. Ring /\ 1 =/= 0 ) )
10	5 6 9	mpbir2an	|- R e. NzRing