Step |
Hyp |
Ref |
Expression |
1 |
|
df-igam |
|- 1/_G = ( x e. CC |-> if ( x e. ( ZZ \ NN ) , 0 , ( 1 / ( _G ` x ) ) ) ) |
2 |
|
0cnd |
|- ( ( x e. CC /\ x e. ( ZZ \ NN ) ) -> 0 e. CC ) |
3 |
|
eldif |
|- ( x e. ( CC \ ( ZZ \ NN ) ) <-> ( x e. CC /\ -. x e. ( ZZ \ NN ) ) ) |
4 |
|
gamcl |
|- ( x e. ( CC \ ( ZZ \ NN ) ) -> ( _G ` x ) e. CC ) |
5 |
|
gamne0 |
|- ( x e. ( CC \ ( ZZ \ NN ) ) -> ( _G ` x ) =/= 0 ) |
6 |
4 5
|
reccld |
|- ( x e. ( CC \ ( ZZ \ NN ) ) -> ( 1 / ( _G ` x ) ) e. CC ) |
7 |
3 6
|
sylbir |
|- ( ( x e. CC /\ -. x e. ( ZZ \ NN ) ) -> ( 1 / ( _G ` x ) ) e. CC ) |
8 |
2 7
|
ifclda |
|- ( x e. CC -> if ( x e. ( ZZ \ NN ) , 0 , ( 1 / ( _G ` x ) ) ) e. CC ) |
9 |
1 8
|
fmpti |
|- 1/_G : CC --> CC |