This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnnrg

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

Ref Expression
Assertion cnnrg ⊢ ℂ fld ∈ NrmRing

Proof

Step Hyp Ref Expression
1 cnngp ⊢ ℂ fld ∈ NrmGrp
2 absabv ⊢ abs ∈ AbsVal ⁡ ℂ fld
3 cnfldnm ⊢ abs = norm ⁡ ℂ fld
4 eqid ⊢ AbsVal ⁡ ℂ fld = AbsVal ⁡ ℂ fld
5 3 4 isnrg ⊢ ℂ fld ∈ NrmRing ↔ ℂ fld ∈ NrmGrp ∧ abs ∈ AbsVal ⁡ ℂ fld
6 1 2 5 mpbir2an ⊢ ℂ fld ∈ NrmRing