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 
|- ( ( X e. CC /\ X =/= 0 ) -> ( ( invr ` CCfld ) ` X ) = ( 1 / X ) )

Proof

Step Hyp Ref Expression
1 eldifsn 
 |-  ( X e. ( CC \ { 0 } ) <-> ( X e. CC /\ X =/= 0 ) )
2 cnring 
 |-  CCfld e. Ring
3 cnfldbas 
 |-  CC = ( Base ` CCfld )
4 cnfld0 
 |-  0 = ( 0g ` CCfld )
5 cndrng 
 |-  CCfld e. DivRing
6 3 4 5 drngui 
 |-  ( CC \ { 0 } ) = ( Unit ` CCfld )
7 cnflddiv 
 |-  / = ( /r ` CCfld )
8 cnfld1 
 |-  1 = ( 1r ` CCfld )
9 eqid 
 |-  ( invr ` CCfld ) = ( invr ` CCfld )
10 3 6 7 8 9 ringinvdv 
 |-  ( ( CCfld e. Ring /\ X e. ( CC \ { 0 } ) ) -> ( ( invr ` CCfld ) ` X ) = ( 1 / X ) )
11 2 10 mpan 
 |-  ( X e. ( CC \ { 0 } ) -> ( ( invr ` CCfld ) ` X ) = ( 1 / X ) )
12 1 11 sylbir 
 |-  ( ( X e. CC /\ X =/= 0 ) -> ( ( invr ` CCfld ) ` X ) = ( 1 / X ) )