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	|- M = ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) )
Assertion	cnmgpabl	|- M e. Abel

Proof

Step	Hyp	Ref	Expression
1		cnmgpabl.m	|- M = ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) )
2		cncrng	|- CCfld e. CRing
3		cnfldbas	|- CC = ( Base ` CCfld )
4		cnfld0	|- 0 = ( 0g ` CCfld )
5		cndrng	|- CCfld e. DivRing
6	3 4 5	drngui	|- ( CC \ { 0 } ) = ( Unit ` CCfld )
7	6 1	unitabl	|- ( CCfld e. CRing -> M e. Abel )
8	2 7	ax-mp	|- M e. Abel