Metamath Proof Explorer

Theorem zzsnm

Description: The norm of the ring of the integers. (Contributed by Thierry Arnoux, 8-Nov-2017) (Revised by AV, 13-Jun-2019)

Ref Expression
Assertion zzsnm M M = norm ring M


Step Hyp Ref Expression
1 zringnm norm ring = abs
2 1 eqcomi abs = norm ring
3 2 fveq1i abs M = norm ring M
4 fvres M abs M = M
5 3 4 syl5reqr M M = norm ring M