Theorem cnfldinv

Description: The multiplicative inverse in the field of complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014)

	Ref	Expression
Assertion	cnfldinv	$$⊢\left(X\in ℂ\wedge X\ne 0\right)\to {inv}_r\left({ℂ}_{\mathrm{fld}}\right)\left(X\right)=\frac{1}{X}$$

Proof

Step	Hyp	Ref	Expression
1		eldifsn	$$⊢X\in \left(ℂ\setminus \left\{0\right\}\right)\leftrightarrow \left(X\in ℂ\wedge X\ne 0\right)$$
2		cnring	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$$
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		cnflddiv	$$⊢÷={/}_r\left({ℂ}_{\mathrm{fld}}\right)$$
8		cnfld1	$$⊢1=1_{{ℂ}_{\mathrm{fld}}}$$
9		eqid	$$⊢{inv}_r\left({ℂ}_{\mathrm{fld}}\right)={inv}_r\left({ℂ}_{\mathrm{fld}}\right)$$
10	3 6 7 8 9	ringinvdv	$$⊢\left({ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\wedge X\in \left(ℂ\setminus \left\{0\right\}\right)\right)\to {inv}_r\left({ℂ}_{\mathrm{fld}}\right)\left(X\right)=\frac{1}{X}$$
11	2 10	mpan	$$⊢X\in \left(ℂ\setminus \left\{0\right\}\right)\to {inv}_r\left({ℂ}_{\mathrm{fld}}\right)\left(X\right)=\frac{1}{X}$$
12	1 11	sylbir	$$⊢\left(X\in ℂ\wedge X\ne 0\right)\to {inv}_r\left({ℂ}_{\mathrm{fld}}\right)\left(X\right)=\frac{1}{X}$$