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={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)$$
Assertion	cnmgpabl	$$⊢M\in \mathrm{Abel}$$

Proof

Step	Hyp	Ref	Expression
1		cnmgpabl.m	$$⊢M={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)$$
2		cncrng	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{CRing}$$
3		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
4		cnfld0	$$⊢0=0_{{ℂ}_{\mathrm{fld}}}$$
5		cndrng	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{DivRing}$$
6	3 4 5	drngui	$$⊢ℂ\setminus \left\{0\right\}=\mathrm{Unit}\left({ℂ}_{\mathrm{fld}}\right)$$
7	6 1	unitabl	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{CRing}\to M\in \mathrm{Abel}$$
8	2 7	ax-mp	$$⊢M\in \mathrm{Abel}$$