# Metamath Proof Explorer

## Theorem zringnm

Description: The norm (function) for a ring of integers is the absolute value function (restricted to the integers). (Contributed by AV, 13-Jun-2019)

Ref Expression
Assertion zringnm ${⊢}\mathrm{norm}\left({ℤ}_{\mathrm{ring}}\right)={\mathrm{abs}↾}_{ℤ}$

### Proof

Step Hyp Ref Expression
1 cnring ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$
2 ringmnd ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to {ℂ}_{\mathrm{fld}}\in \mathrm{Mnd}$
3 1 2 ax-mp ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{Mnd}$
4 0z ${⊢}0\in ℤ$
5 zsscn ${⊢}ℤ\subseteq ℂ$
6 df-zring ${⊢}{ℤ}_{\mathrm{ring}}={ℂ}_{\mathrm{fld}}{↾}_{𝑠}ℤ$
7 cnfldbas ${⊢}ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$
8 cnfld0 ${⊢}0={0}_{{ℂ}_{\mathrm{fld}}}$
9 cnfldnm ${⊢}\mathrm{abs}=\mathrm{norm}\left({ℂ}_{\mathrm{fld}}\right)$
10 6 7 8 9 ressnm ${⊢}\left({ℂ}_{\mathrm{fld}}\in \mathrm{Mnd}\wedge 0\in ℤ\wedge ℤ\subseteq ℂ\right)\to {\mathrm{abs}↾}_{ℤ}=\mathrm{norm}\left({ℤ}_{\mathrm{ring}}\right)$
11 10 eqcomd ${⊢}\left({ℂ}_{\mathrm{fld}}\in \mathrm{Mnd}\wedge 0\in ℤ\wedge ℤ\subseteq ℂ\right)\to \mathrm{norm}\left({ℤ}_{\mathrm{ring}}\right)={\mathrm{abs}↾}_{ℤ}$
12 3 4 5 11 mp3an ${⊢}\mathrm{norm}\left({ℤ}_{\mathrm{ring}}\right)={\mathrm{abs}↾}_{ℤ}$