# Metamath Proof Explorer

## Theorem cnngp

Description: The complex numbers form a normed group. (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Assertion cnngp ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{NrmGrp}$

### Proof

Step Hyp Ref Expression
1 cnring ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$
2 ringgrp ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to {ℂ}_{\mathrm{fld}}\in \mathrm{Grp}$
3 1 2 ax-mp ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{Grp}$
4 cnfldms ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{MetSp}$
5 ssid ${⊢}\mathrm{abs}\circ -\subseteq \mathrm{abs}\circ -$
6 cnfldnm ${⊢}\mathrm{abs}=\mathrm{norm}\left({ℂ}_{\mathrm{fld}}\right)$
7 cnfldsub ${⊢}-={-}_{{ℂ}_{\mathrm{fld}}}$
8 cnfldds ${⊢}\mathrm{abs}\circ -=\mathrm{dist}\left({ℂ}_{\mathrm{fld}}\right)$
9 6 7 8 isngp ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{NrmGrp}↔\left({ℂ}_{\mathrm{fld}}\in \mathrm{Grp}\wedge {ℂ}_{\mathrm{fld}}\in \mathrm{MetSp}\wedge \mathrm{abs}\circ -\subseteq \mathrm{abs}\circ -\right)$
10 3 4 5 9 mpbir3an ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{NrmGrp}$