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_G : ( CC \ ( ZZ \ NN ) ) --> CC

Proof

Step	Hyp	Ref	Expression
1		ovexd	|- ( ( T. /\ x e. ( CC \ ( ZZ \ NN ) ) ) -> ( sum_ n e. NN ( ( x x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( x / n ) + 1 ) ) ) - ( log ` x ) ) e. _V )
2		df-lgam	|- log_G = ( x e. ( CC \ ( ZZ \ NN ) ) |-> ( sum_ n e. NN ( ( x x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( x / n ) + 1 ) ) ) - ( log ` x ) ) )
3	2	a1i	|- ( T. -> log_G = ( x e. ( CC \ ( ZZ \ NN ) ) |-> ( sum_ n e. NN ( ( x x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( x / n ) + 1 ) ) ) - ( log ` x ) ) ) )
4		lgamcl	|- ( x e. ( CC \ ( ZZ \ NN ) ) -> ( log_G ` x ) e. CC )
5	4	adantl	|- ( ( T. /\ x e. ( CC \ ( ZZ \ NN ) ) ) -> ( log_G ` x ) e. CC )
6	1 3 5	fmpt2d	|- ( T. -> log_G : ( CC \ ( ZZ \ NN ) ) --> CC )
7	6	mptru	|- log_G : ( CC \ ( ZZ \ NN ) ) --> CC