Metamath Proof Explorer

Theorem igamval

Description: Value of the inverse Gamma function. (Contributed by Mario Carneiro, 16-Jul-2017)

Ref Expression
Assertion igamval 
|- ( A e. CC -> ( 1/_G ` A ) = if ( A e. ( ZZ \ NN ) , 0 , ( 1 / ( _G ` A ) ) ) )

Proof

Step Hyp Ref Expression
1 eleq1 
 |-  ( x = A -> ( x e. ( ZZ \ NN ) <-> A e. ( ZZ \ NN ) ) )
2 fveq2 
 |-  ( x = A -> ( _G ` x ) = ( _G ` A ) )
3 2 oveq2d 
 |-  ( x = A -> ( 1 / ( _G ` x ) ) = ( 1 / ( _G ` A ) ) )
4 1 3 ifbieq2d 
 |-  ( x = A -> if ( x e. ( ZZ \ NN ) , 0 , ( 1 / ( _G ` x ) ) ) = if ( A e. ( ZZ \ NN ) , 0 , ( 1 / ( _G ` A ) ) ) )
5 df-igam 
 |-  1/_G = ( x e. CC |-> if ( x e. ( ZZ \ NN ) , 0 , ( 1 / ( _G ` x ) ) ) )
6 c0ex 
 |-  0 e. _V
7 ovex 
 |-  ( 1 / ( _G ` A ) ) e. _V
8 6 7 ifex 
 |-  if ( A e. ( ZZ \ NN ) , 0 , ( 1 / ( _G ` A ) ) ) e. _V
9 4 5 8 fvmpt 
 |-  ( A e. CC -> ( 1/_G ` A ) = if ( A e. ( ZZ \ NN ) , 0 , ( 1 / ( _G ` A ) ) ) )