Definition df-igam

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	$$⊢\frac{1}{\mathrm{\Gamma }}=\left(x\in ℂ⟼if\left(x\in \left(\mathbb{Z}\setminus \mathbb{N}\right),0,\frac{1}{\mathrm{\Gamma }\left(x\right)}\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cigam	$$class\frac{1}{\mathrm{\Gamma }}$$
1		vx	$$setvarx$$
2		cc	$$classℂ$$
3	1	cv	$$setvarx$$
4		cz	$$class\mathbb{Z}$$
5		cn	$$class\mathbb{N}$$
6	4 5	cdif	$$class\left(\mathbb{Z}\setminus \mathbb{N}\right)$$
7	3 6	wcel	$$wffx\in \left(\mathbb{Z}\setminus \mathbb{N}\right)$$
8		cc0	$$class0$$
9		c1	$$class1$$
10		cdiv	$$class÷$$
11		cgam	$$class\mathrm{\Gamma }$$
12	3 11	cfv	$$class\mathrm{\Gamma }\left(x\right)$$
13	9 12 10	co	$$class\left(\frac{1}{\mathrm{\Gamma }\left(x\right)}\right)$$
14	7 8 13	cif	$$classif\left(x\in \left(\mathbb{Z}\setminus \mathbb{N}\right),0,\frac{1}{\mathrm{\Gamma }\left(x\right)}\right)$$
15	1 2 14	cmpt	$$class\left(x\in ℂ⟼if\left(x\in \left(\mathbb{Z}\setminus \mathbb{N}\right),0,\frac{1}{\mathrm{\Gamma }\left(x\right)}\right)\right)$$
16	0 15	wceq	$$wff\frac{1}{\mathrm{\Gamma }}=\left(x\in ℂ⟼if\left(x\in \left(\mathbb{Z}\setminus \mathbb{N}\right),0,\frac{1}{\mathrm{\Gamma }\left(x\right)}\right)\right)$$