Theorem gamf

Description: The Gamma function is a complex function defined on the whole complex plane except for the negative integers. (Contributed by Mario Carneiro, 6-Jul-2017)

	Ref	Expression
Assertion	gamf	$$⊢\mathrm{\Gamma }:ℂ\setminus \left(\mathbb{Z}\setminus \mathbb{N}\right)⟶ℂ$$

Proof

Step	Hyp	Ref	Expression
1		eff	$$⊢\exp :ℂ⟶ℂ$$
2		lgamf	$$⊢\log \mathrm{\Gamma }:ℂ\setminus \left(\mathbb{Z}\setminus \mathbb{N}\right)⟶ℂ$$
3		fco	$$⊢\left(\exp :ℂ⟶ℂ\wedge \log \mathrm{\Gamma }:ℂ\setminus \left(\mathbb{Z}\setminus \mathbb{N}\right)⟶ℂ\right)\to \left(\exp \circ \log \mathrm{\Gamma }\right):ℂ\setminus \left(\mathbb{Z}\setminus \mathbb{N}\right)⟶ℂ$$
4	1 2 3	mp2an	$$⊢\left(\exp \circ \log \mathrm{\Gamma }\right):ℂ\setminus \left(\mathbb{Z}\setminus \mathbb{N}\right)⟶ℂ$$
5		df-gam	$$⊢\mathrm{\Gamma }=\exp \circ \log \mathrm{\Gamma }$$
6	5	feq1i	$$⊢\mathrm{\Gamma }:ℂ\setminus \left(\mathbb{Z}\setminus \mathbb{N}\right)⟶ℂ\leftrightarrow \left(\exp \circ \log \mathrm{\Gamma }\right):ℂ\setminus \left(\mathbb{Z}\setminus \mathbb{N}\right)⟶ℂ$$
7	4 6	mpbir	$$⊢\mathrm{\Gamma }:ℂ\setminus \left(\mathbb{Z}\setminus \mathbb{N}\right)⟶ℂ$$