Theorem zringnrg

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

	Ref	Expression
Assertion	zringnrg	|- ZZring e. NrmRing

Proof

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