Theorem lgamf

Description: The log-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	lgamf	$$⊢\log \mathrm{\Gamma }:ℂ\setminus \left(\mathbb{Z}\setminus \mathbb{N}\right)⟶ℂ$$

Proof

Step	Hyp	Ref	Expression
1		ovexd	$$⊢\left(\top \wedge x\in \left(ℂ\setminus \left(\mathbb{Z}\setminus \mathbb{N}\right)\right)\right)\to \sum _{n\in \mathbb{N}}\left(x\log \left(\frac{n+1}{n}\right)-\log \left(\left(\frac{x}{n}\right)+1\right)\right)-\log x\in \mathrm{V}$$
2		df-lgam	$$⊢\log \mathrm{\Gamma }=\left(x\in \left(ℂ\setminus \left(\mathbb{Z}\setminus \mathbb{N}\right)\right)⟼\sum _{n\in \mathbb{N}}\left(x\log \left(\frac{n+1}{n}\right)-\log \left(\left(\frac{x}{n}\right)+1\right)\right)-\log x\right)$$
3	2	a1i	$$⊢\top \to \log \mathrm{\Gamma }=\left(x\in \left(ℂ\setminus \left(\mathbb{Z}\setminus \mathbb{N}\right)\right)⟼\sum _{n\in \mathbb{N}}\left(x\log \left(\frac{n+1}{n}\right)-\log \left(\left(\frac{x}{n}\right)+1\right)\right)-\log x\right)$$
4		lgamcl	$$⊢x\in \left(ℂ\setminus \left(\mathbb{Z}\setminus \mathbb{N}\right)\right)\to \log \mathrm{\Gamma }\left(x\right)\in ℂ$$
5	4	adantl	$$⊢\left(\top \wedge x\in \left(ℂ\setminus \left(\mathbb{Z}\setminus \mathbb{N}\right)\right)\right)\to \log \mathrm{\Gamma }\left(x\right)\in ℂ$$
6	1 3 5	fmpt2d	$$⊢\top \to \log \mathrm{\Gamma }:ℂ\setminus \left(\mathbb{Z}\setminus \mathbb{N}\right)⟶ℂ$$
7	6	mptru	$$⊢\log \mathrm{\Gamma }:ℂ\setminus \left(\mathbb{Z}\setminus \mathbb{N}\right)⟶ℂ$$