Description: Value of the inverse Gamma function in terms of the Gamma function. (Contributed by Mario Carneiro, 16-Jul-2017)
Ref | Expression | ||
---|---|---|---|
Assertion | igamgam | |- ( A e. ( CC \ ( ZZ \ NN ) ) -> ( 1/_G ` A ) = ( 1 / ( _G ` A ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eldif | |- ( A e. ( CC \ ( ZZ \ NN ) ) <-> ( A e. CC /\ -. A e. ( ZZ \ NN ) ) ) |
|
2 | igamval | |- ( A e. CC -> ( 1/_G ` A ) = if ( A e. ( ZZ \ NN ) , 0 , ( 1 / ( _G ` A ) ) ) ) |
|
3 | iffalse | |- ( -. A e. ( ZZ \ NN ) -> if ( A e. ( ZZ \ NN ) , 0 , ( 1 / ( _G ` A ) ) ) = ( 1 / ( _G ` A ) ) ) |
|
4 | 2 3 | sylan9eq | |- ( ( A e. CC /\ -. A e. ( ZZ \ NN ) ) -> ( 1/_G ` A ) = ( 1 / ( _G ` A ) ) ) |
5 | 1 4 | sylbi | |- ( A e. ( CC \ ( ZZ \ NN ) ) -> ( 1/_G ` A ) = ( 1 / ( _G ` A ) ) ) |