Theorem cnngp

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

	Ref	Expression
Assertion	cnngp	⊢ ℂfld ∈ NrmGrp

Proof

Step	Hyp	Ref	Expression
1		cnring	⊢ ℂfld ∈ Ring
2		ringgrp	⊢ ( ℂfld ∈ Ring → ℂfld ∈ Grp )
3	1 2	ax-mp	⊢ ℂfld ∈ Grp
4		cnfldms	⊢ ℂfld ∈ MetSp
5		ssid	⊢ ( abs ∘ − ) ⊆ ( abs ∘ − )
6		cnfldnm	⊢ abs = ( norm ‘ ℂfld )
7		cnfldsub	⊢ − = ( -g ‘ ℂfld )
8		cnfldds	⊢ ( abs ∘ − ) = ( dist ‘ ℂfld )
9	6 7 8	isngp	⊢ ( ℂfld ∈ NrmGrp ↔ ( ℂfld ∈ Grp ∧ ℂfld ∈ MetSp ∧ ( abs ∘ − ) ⊆ ( abs ∘ − ) ) )
10	3 4 5 9	mpbir3an	⊢ ℂfld ∈ NrmGrp