Theorem cnmgpabl

Description: The unit group of the complex numbers is an abelian group. (Contributed by Mario Carneiro, 21-Jun-2015)

	Ref	Expression
Hypothesis	cnmgpabl.m	⊢ 𝑀 = ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) )
Assertion	cnmgpabl	⊢ 𝑀 ∈ Abel

Proof

Step	Hyp	Ref	Expression
1		cnmgpabl.m	⊢ 𝑀 = ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) )
2		cncrng	⊢ ℂfld ∈ CRing
3		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
4		cnfld0	⊢ 0 = ( 0g ‘ ℂfld )
5		cndrng	⊢ ℂfld ∈ DivRing
6	3 4 5	drngui	⊢ ( ℂ ∖ { 0 } ) = ( Unit ‘ ℂfld )
7	6 1	unitabl	⊢ ( ℂfld ∈ CRing → 𝑀 ∈ Abel )
8	2 7	ax-mp	⊢ 𝑀 ∈ Abel