Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-igam Structured version   Unicode version

Definition df-igam 28191
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 28188 . 2  class 1/ _G
2 vx . . 3  setvar  x
3 cc 9481 . . 3  class  CC
42cv 1373 . . . . 5  class  x
5 cz 10855 . . . . . 6  class  ZZ
6 cn 10527 . . . . . 6  class  NN
75, 6cdif 3468 . . . . 5  class  ( ZZ 
\  NN )
84, 7wcel 1762 . . . 4  wff  x  e.  ( ZZ  \  NN )
9 cc0 9483 . . . 4  class  0
10 c1 9484 . . . . 5  class  1
11 cgam 28187 . . . . . 6  class  _G
124, 11cfv 5581 . . . . 5  class  ( _G `  x )
13 cdiv 10197 . . . . 5  class  /
1410, 12, 13co 6277 . . . 4  class  ( 1  /  ( _G `  x
) )
158, 9, 14cif 3934 . . 3  class  if ( x  e.  ( ZZ 
\  NN ) ,  0 ,  ( 1  /  ( _G `  x
) ) )
162, 3, 15cmpt 4500 . 2  class  ( x  e.  CC  |->  if ( x  e.  ( ZZ 
\  NN ) ,  0 ,  ( 1  /  ( _G `  x
) ) ) )
171, 16wceq 1374 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  28217  igamf  28221
  Copyright terms: Public domain W3C validator