Description: Define the inverse Gamma function, which is defined everywhere, unlike the Gamma function itself. (Contributed by Mario Carneiro, 16-Jul-2017)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-igam | |- 1/_G = ( x e. CC |-> if ( x e. ( ZZ \ NN ) , 0 , ( 1 / ( _G ` x ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cigam | |- 1/_G |
|
| 1 | vx | |- x |
|
| 2 | cc | |- CC |
|
| 3 | 1 | cv | |- x |
| 4 | cz | |- ZZ |
|
| 5 | cn | |- NN |
|
| 6 | 4 5 | cdif | |- ( ZZ \ NN ) |
| 7 | 3 6 | wcel | |- x e. ( ZZ \ NN ) |
| 8 | cc0 | |- 0 |
|
| 9 | c1 | |- 1 |
|
| 10 | cdiv | |- / |
|
| 11 | cgam | |- _G |
|
| 12 | 3 11 | cfv | |- ( _G ` x ) |
| 13 | 9 12 10 | co | |- ( 1 / ( _G ` x ) ) |
| 14 | 7 8 13 | cif | |- if ( x e. ( ZZ \ NN ) , 0 , ( 1 / ( _G ` x ) ) ) |
| 15 | 1 2 14 | cmpt | |- ( x e. CC |-> if ( x e. ( ZZ \ NN ) , 0 , ( 1 / ( _G ` x ) ) ) ) |
| 16 | 0 15 | wceq | |- 1/_G = ( x e. CC |-> if ( x e. ( ZZ \ NN ) , 0 , ( 1 / ( _G ` x ) ) ) ) |