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\in \mathbb{Z}\to \left|M\right|=\mathrm{norm}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(M\right)$$

Proof

Step	Hyp	Ref	Expression
1		fvres	$$⊢M\in \mathbb{Z}\to \left({\mathrm{abs}\upharpoonright }_{\mathbb{Z}}\right)\left(M\right)=\left|M\right|$$
2		zringnm	$$⊢\mathrm{norm}\left({\mathbb{Z}}_{\mathrm{ring}}\right)={\mathrm{abs}\upharpoonright }_{\mathbb{Z}}$$
3	2	eqcomi	$$⊢{\mathrm{abs}\upharpoonright }_{\mathbb{Z}}=\mathrm{norm}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
4	3	fveq1i	$$⊢\left({\mathrm{abs}\upharpoonright }_{\mathbb{Z}}\right)\left(M\right)=\mathrm{norm}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(M\right)$$
5	1 4	eqtr3di	$$⊢M\in \mathbb{Z}\to \left|M\right|=\mathrm{norm}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(M\right)$$