Theorem lgamcl

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

	Ref	Expression
Assertion	lgamcl	$$⊢A\in \left(ℂ\setminus \left(\mathbb{Z}\setminus \mathbb{N}\right)\right)\to \log \mathrm{\Gamma }\left(A\right)\in ℂ$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\left\{x\in ℂ|\left(\left|x\right|\le r\wedge \forall k\in {\mathbb{N}}_0\frac{1}{r}\le \left|x+k\right|\right)\right\}=\left\{x\in ℂ|\left(\left|x\right|\le r\wedge \forall k\in {\mathbb{N}}_0\frac{1}{r}\le \left|x+k\right|\right)\right\}$$
2		id	$$⊢A\in \left(ℂ\setminus \left(\mathbb{Z}\setminus \mathbb{N}\right)\right)\to A\in \left(ℂ\setminus \left(\mathbb{Z}\setminus \mathbb{N}\right)\right)$$
3		eqid	$$⊢\left(n\in \mathbb{N}⟼A\log \left(\frac{n+1}{n}\right)-\log \left(\left(\frac{A}{n}\right)+1\right)\right)=\left(n\in \mathbb{N}⟼A\log \left(\frac{n+1}{n}\right)-\log \left(\left(\frac{A}{n}\right)+1\right)\right)$$
4	1 2 3	lgamcvglem	$$⊢A\in \left(ℂ\setminus \left(\mathbb{Z}\setminus \mathbb{N}\right)\right)\to \left(\log \mathrm{\Gamma }\left(A\right)\in ℂ\wedge seq1\left(+,\left(n\in \mathbb{N}⟼A\log \left(\frac{n+1}{n}\right)-\log \left(\left(\frac{A}{n}\right)+1\right)\right)\right)⇝\left(\log \mathrm{\Gamma }\left(A\right)+\log A\right)\right)$$
5	4	simpld	$$⊢A\in \left(ℂ\setminus \left(\mathbb{Z}\setminus \mathbb{N}\right)\right)\to \log \mathrm{\Gamma }\left(A\right)\in ℂ$$