Theorem subrgccnzr

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

	Ref	Expression
Hypotheses	subrgcccrng.r	⊢ 𝑅 = ( ℂfld ↾s 𝑆 )
	subrgcccrng.s	⊢ 𝑆 ∈ ( SubRing ‘ ℂfld )
Assertion	subrgccnzr	⊢ 𝑅 ∈ NzRing

Proof

Step	Hyp	Ref	Expression
1		subrgcccrng.r	⊢ 𝑅 = ( ℂfld ↾s 𝑆 )
2		subrgcccrng.s	⊢ 𝑆 ∈ ( SubRing ‘ ℂfld )
3	1 2	subrgcccrng	⊢ 𝑅 ∈ CRing
4		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
5	3 4	ax-mp	⊢ 𝑅 ∈ Ring
6		ax-1ne0	⊢ 1 ≠ 0
7	1 2	subrgcccrng1	⊢ 1 = ( 1r ‘ 𝑅 )
8	1 2	subrgcccrng0	⊢ 0 = ( 0g ‘ 𝑅 )
9	7 8	isnzr	⊢ ( 𝑅 ∈ NzRing ↔ ( 𝑅 ∈ Ring ∧ 1 ≠ 0 ) )
10	5 6 9	mpbir2an	⊢ 𝑅 ∈ NzRing