Theorem igamval

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

	Ref	Expression
Assertion	igamval	$$⊢A\in ℂ\to \frac{1}{\mathrm{\Gamma }}\left(A\right)=if\left(A\in \left(\mathbb{Z}\setminus \mathbb{N}\right),0,\frac{1}{\mathrm{\Gamma }\left(A\right)}\right)$$

Proof

Step	Hyp	Ref	Expression
1		eleq1	$$⊢x=A\to \left(x\in \left(\mathbb{Z}\setminus \mathbb{N}\right)\leftrightarrow A\in \left(\mathbb{Z}\setminus \mathbb{N}\right)\right)$$
2		fveq2	$$⊢x=A\to \mathrm{\Gamma }\left(x\right)=\mathrm{\Gamma }\left(A\right)$$
3	2	oveq2d	$$⊢x=A\to \frac{1}{\mathrm{\Gamma }\left(x\right)}=\frac{1}{\mathrm{\Gamma }\left(A\right)}$$
4	1 3	ifbieq2d	$$⊢x=A\to if\left(x\in \left(\mathbb{Z}\setminus \mathbb{N}\right),0,\frac{1}{\mathrm{\Gamma }\left(x\right)}\right)=if\left(A\in \left(\mathbb{Z}\setminus \mathbb{N}\right),0,\frac{1}{\mathrm{\Gamma }\left(A\right)}\right)$$
5		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)$$
6		c0ex	$$⊢0\in \mathrm{V}$$
7		ovex	$$⊢\frac{1}{\mathrm{\Gamma }\left(A\right)}\in \mathrm{V}$$
8	6 7	ifex	$$⊢if\left(A\in \left(\mathbb{Z}\setminus \mathbb{N}\right),0,\frac{1}{\mathrm{\Gamma }\left(A\right)}\right)\in \mathrm{V}$$
9	4 5 8	fvmpt	$$⊢A\in ℂ\to \frac{1}{\mathrm{\Gamma }}\left(A\right)=if\left(A\in \left(\mathbb{Z}\setminus \mathbb{N}\right),0,\frac{1}{\mathrm{\Gamma }\left(A\right)}\right)$$