Theorem zringcrng

Description: The ring of integers is a commutative ring. (Contributed by AV, 13-Jun-2019)

	Ref	Expression
Assertion	zringcrng	|- ZZring e. CRing

Proof

Step	Hyp	Ref	Expression
1		cncrng	|- CCfld e. CRing
2		zsubrg	|- ZZ e. ( SubRing ` CCfld )
3		df-zring	|- ZZring = ( CCfld |`s ZZ )
4	3	subrgcrng	|- ( ( CCfld e. CRing /\ ZZ e. ( SubRing ` CCfld ) ) -> ZZring e. CRing )
5	1 2 4	mp2an	|- ZZring e. CRing