Metamath Proof Explorer

Theorem cnnrg

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

Ref Expression
Assertion cnnrg 
|- CCfld e. NrmRing

Proof

Step Hyp Ref Expression
1 cnngp 
 |-  CCfld e. NrmGrp
2 absabv 
 |-  abs e. ( AbsVal ` CCfld )
3 cnfldnm 
 |-  abs = ( norm ` CCfld )
4 eqid 
 |-  ( AbsVal ` CCfld ) = ( AbsVal ` CCfld )
5 3 4 isnrg 
 |-  ( CCfld e. NrmRing <-> ( CCfld e. NrmGrp /\ abs e. ( AbsVal ` CCfld ) ) )
6 1 2 5 mpbir2an 
 |-  CCfld e. NrmRing