Metamath Proof Explorer

Theorem zringnrg

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

Ref Expression
Assertion zringnrg ring NrmRing


Step Hyp Ref Expression
1 cnnrg fld NrmRing
2 zsubrg SubRing fld
3 df-zring ring = fld 𝑠
4 3 subrgnrg fld NrmRing SubRing fld ring NrmRing
5 1 2 4 mp2an ring NrmRing