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 e. ( CC \ ( ZZ \ NN ) ) -> ( log_G ` A ) e. CC )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- { x e. CC | ( ( abs ` x ) <_ r /\ A. k e. NN0 ( 1 / r ) <_ ( abs ` ( x + k ) ) ) } = { x e. CC | ( ( abs ` x ) <_ r /\ A. k e. NN0 ( 1 / r ) <_ ( abs ` ( x + k ) ) ) }
2		id	|- ( A e. ( CC \ ( ZZ \ NN ) ) -> A e. ( CC \ ( ZZ \ NN ) ) )
3		eqid	|- ( n e. NN |-> ( ( A x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( A / n ) + 1 ) ) ) ) = ( n e. NN |-> ( ( A x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( A / n ) + 1 ) ) ) )
4	1 2 3	lgamcvglem	|- ( A e. ( CC \ ( ZZ \ NN ) ) -> ( ( log_G ` A ) e. CC /\ seq 1 ( + , ( n e. NN |-> ( ( A x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( A / n ) + 1 ) ) ) ) ) ~~> ( ( log_G ` A ) + ( log ` A ) ) ) )
5	4	simpld	|- ( A e. ( CC \ ( ZZ \ NN ) ) -> ( log_G ` A ) e. CC )