Theorem igamf

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

	Ref	Expression
Assertion	igamf	$$⊢\frac{1}{\mathrm{\Gamma }}:ℂ⟶ℂ$$

Proof

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