This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 / 𝑋 ) )