Definition df-igam 24747

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

Step	Hyp	Ref	Expression
1		cigam 24744	. 2 class 1/ _G
2		vx	. . 3 setvar x
3		cc 9934	. . 3 class CC
4	2	cv 1482	. . . . 5 class x
5		cz 11377	. . . . . 6 class ZZ
6		cn 11020	. . . . . 6 class NN
7	5, 6	cdif 3571	. . . . 5 class ( ZZ \ NN )
8	4, 7	wcel 1990	. . . 4 wff x e. ( ZZ \ NN )
9		cc0 9936	. . . 4 class 0
10		c1 9937	. . . . 5 class 1
11		cgam 24743	. . . . . 6 class _G
12	4, 11	cfv 5888	. . . . 5 class ( _G ` x )
13		cdiv 10684	. . . . 5 class /
14	10, 12, 13	co 6650	. . . 4 class ( 1 / ( _G ` x ) )
15	8, 9, 14	cif 4086	. . 3 class if ( x e. ( ZZ \ NN ) , 0 , ( 1 / ( _G ` x ) ) )
16	2, 3, 15	cmpt 4729	. 2 class ( x e. CC |-> if ( x e. ( ZZ \ NN ) , 0 , ( 1 / ( _G ` x ) ) ) )
17	1, 16	wceq 1483	1 wff 1/ _G = ( x e. CC |-> if ( x e. ( ZZ \ NN ) , 0 , ( 1 / ( _G ` x ) ) ) )

This definition is referenced by:  igamval  24773  igamf  24777