Theorem igamcl

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

	Ref	Expression
Assertion	igamcl	$$⊢A\in ℂ\to \frac{1}{\mathrm{\Gamma }}\left(A\right)\in ℂ$$

Proof

Step	Hyp	Ref	Expression
1		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)$$
2		0cnd	$$⊢\left(A\in ℂ\wedge A\in \left(\mathbb{Z}\setminus \mathbb{N}\right)\right)\to 0\in ℂ$$
3		eldif	$$⊢A\in \left(ℂ\setminus \left(\mathbb{Z}\setminus \mathbb{N}\right)\right)\leftrightarrow \left(A\in ℂ\wedge \neg A\in \left(\mathbb{Z}\setminus \mathbb{N}\right)\right)$$
4		gamcl	$$⊢A\in \left(ℂ\setminus \left(\mathbb{Z}\setminus \mathbb{N}\right)\right)\to \mathrm{\Gamma }\left(A\right)\in ℂ$$
5		gamne0	$$⊢A\in \left(ℂ\setminus \left(\mathbb{Z}\setminus \mathbb{N}\right)\right)\to \mathrm{\Gamma }\left(A\right)\ne 0$$
6	4 5	reccld	$$⊢A\in \left(ℂ\setminus \left(\mathbb{Z}\setminus \mathbb{N}\right)\right)\to \frac{1}{\mathrm{\Gamma }\left(A\right)}\in ℂ$$
7	3 6	sylbir	$$⊢\left(A\in ℂ\wedge \neg A\in \left(\mathbb{Z}\setminus \mathbb{N}\right)\right)\to \frac{1}{\mathrm{\Gamma }\left(A\right)}\in ℂ$$
8	2 7	ifclda	$$⊢A\in ℂ\to if\left(A\in \left(\mathbb{Z}\setminus \mathbb{N}\right),0,\frac{1}{\mathrm{\Gamma }\left(A\right)}\right)\in ℂ$$
9	1 8	eqeltrd	$$⊢A\in ℂ\to \frac{1}{\mathrm{\Gamma }}\left(A\right)\in ℂ$$