MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-igam Structured version   Unicode version

Definition df-igam 23819
Description: Define the inverse Gamma function, which is defined everywhere, unlike the Gamma function itself. (Contributed by Mario Carneiro, 16-Jul-2017.)
Assertion
Ref Expression
df-igam  |- 1/ _G  =  ( x  e.  CC  |->  if ( x  e.  ( ZZ  \  NN ) ,  0 ,  ( 1  /  ( _G `  x ) ) ) )

Detailed syntax breakdown of Definition df-igam
StepHypRef Expression
1 cigam 23816 . 2  class 1/ _G
2 vx . . 3  setvar  x
3 cc 9536 . . 3  class  CC
42cv 1436 . . . . 5  class  x
5 cz 10937 . . . . . 6  class  ZZ
6 cn 10609 . . . . . 6  class  NN
75, 6cdif 3439 . . . . 5  class  ( ZZ 
\  NN )
84, 7wcel 1870 . . . 4  wff  x  e.  ( ZZ  \  NN )
9 cc0 9538 . . . 4  class  0
10 c1 9539 . . . . 5  class  1
11 cgam 23815 . . . . . 6  class  _G
124, 11cfv 5601 . . . . 5  class  ( _G `  x )
13 cdiv 10268 . . . . 5  class  /
1410, 12, 13co 6305 . . . 4  class  ( 1  /  ( _G `  x
) )
158, 9, 14cif 3915 . . 3  class  if ( x  e.  ( ZZ 
\  NN ) ,  0 ,  ( 1  /  ( _G `  x
) ) )
162, 3, 15cmpt 4484 . 2  class  ( x  e.  CC  |->  if ( x  e.  ( ZZ 
\  NN ) ,  0 ,  ( 1  /  ( _G `  x
) ) ) )
171, 16wceq 1437 1  wff 1/ _G  =  ( x  e.  CC  |->  if ( x  e.  ( ZZ  \  NN ) ,  0 ,  ( 1  /  ( _G `  x ) ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  igamval  23845  igamf  23849
  Copyright terms: Public domain W3C validator