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