Theorem cnfldinv

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

	Ref	Expression
Assertion	cnfldinv	⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑋 ≠ 0 ) → ( ( invr ‘ ℂfld ) ‘ 𝑋 ) = ( 1 / 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		eldifsn	⊢ ( 𝑋 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝑋 ∈ ℂ ∧ 𝑋 ≠ 0 ) )
2		cnring	⊢ ℂfld ∈ Ring
3		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
4		cnfld0	⊢ 0 = ( 0g ‘ ℂfld )
5		cndrng	⊢ ℂfld ∈ DivRing
6	3 4 5	drngui	⊢ ( ℂ ∖ { 0 } ) = ( Unit ‘ ℂfld )
7		cnflddiv	⊢ / = ( /r ‘ ℂfld )
8		cnfld1	⊢ 1 = ( 1r ‘ ℂfld )
9		eqid	⊢ ( invr ‘ ℂfld ) = ( invr ‘ ℂfld )
10	3 6 7 8 9	ringinvdv	⊢ ( ( ℂfld ∈ Ring ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( ( invr ‘ ℂfld ) ‘ 𝑋 ) = ( 1 / 𝑋 ) )
11	2 10	mpan	⊢ ( 𝑋 ∈ ( ℂ ∖ { 0 } ) → ( ( invr ‘ ℂfld ) ‘ 𝑋 ) = ( 1 / 𝑋 ) )
12	1 11	sylbir	⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑋 ≠ 0 ) → ( ( invr ‘ ℂfld ) ‘ 𝑋 ) = ( 1 / 𝑋 ) )