cnfldinv

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

		Ref	Expression
	Assertion	cnfldinv	$⊢ (X \in ℂ \land X \neq 0) \to {inv}_{r} (ℂ_{fld}) (X) = \frac{1}{X}$

Step	Hyp	Ref	Expression
1		eldifsn	$⊢ X \in (ℂ ∖ \{0\}) \leftrightarrow (X \in ℂ \land X \neq 0)$
2		cnring	$⊢ ℂ_{fld} \in Ring$
3		cnfldbas	$⊢ ℂ = {Base}_{ℂ_{fld}}$
4		cnfld0	$⊢ 0 = 0_{ℂ_{fld}}$
5		cndrng	$⊢ ℂ_{fld} \in DivRing$
6	3 4 5	drngui	$⊢ ℂ ∖ \{0\} = Unit (ℂ_{fld})$
7		cnflddiv	$⊢ \div = /_{r} (ℂ_{fld})$
8		cnfld1	$⊢ 1 = 1_{ℂ_{fld}}$
9		eqid	$⊢ {inv}_{r} (ℂ_{fld}) = {inv}_{r} (ℂ_{fld})$
10	3 6 7 8 9	ringinvdv	$⊢ (ℂ_{fld} \in Ring \land X \in (ℂ ∖ \{0\})) \to {inv}_{r} (ℂ_{fld}) (X) = \frac{1}{X}$
11	2 10	mpan	$⊢ X \in (ℂ ∖ \{0\}) \to {inv}_{r} (ℂ_{fld}) (X) = \frac{1}{X}$
12	1 11	sylbir	$⊢ (X \in ℂ \land X \neq 0) \to {inv}_{r} (ℂ_{fld}) (X) = \frac{1}{X}$

Metamath Proof Explorer