Theorem lgamgulm

Description: The series G is uniformly convergent on the compact region U , which describes a circle of radius R with holes of size 1 / R around the poles of the gamma function. (Contributed by Mario Carneiro, 3-Jul-2017)

	Ref	Expression
Hypotheses	lgamgulm.r	|- ( ph -> R e. NN )
	lgamgulm.u	|- U = { x e. CC | ( ( abs ` x ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( x + k ) ) ) }
	lgamgulm.g	|- G = ( m e. NN |-> ( z e. U |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) )
Assertion	lgamgulm	|- ( ph -> seq 1 ( oF + , G ) e. dom ( ~~>u ` U ) )

Proof

Step	Hyp	Ref	Expression
1		lgamgulm.r	|- ( ph -> R e. NN )
2		lgamgulm.u	|- U = { x e. CC | ( ( abs ` x ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( x + k ) ) ) }
3		lgamgulm.g	|- G = ( m e. NN |-> ( z e. U |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) )
4		eqid	|- ( m e. NN |-> if ( ( 2 x. R ) <_ m , ( R x. ( ( 2 x. ( R + 1 ) ) / ( m ^ 2 ) ) ) , ( ( R x. ( log ` ( ( m + 1 ) / m ) ) ) + ( ( log ` ( ( R + 1 ) x. m ) ) + _pi ) ) ) ) = ( m e. NN |-> if ( ( 2 x. R ) <_ m , ( R x. ( ( 2 x. ( R + 1 ) ) / ( m ^ 2 ) ) ) , ( ( R x. ( log ` ( ( m + 1 ) / m ) ) ) + ( ( log ` ( ( R + 1 ) x. m ) ) + _pi ) ) ) )
5	1 2 3 4	lgamgulmlem6	|- ( ph -> ( seq 1 ( oF + , G ) e. dom ( ~~>u ` U ) /\ ( seq 1 ( oF + , G ) ( ~~>u ` U ) ( z e. U |-> 1 ) -> E. r e. RR A. z e. U ( abs ` 1 ) <_ r ) ) )
6	5	simpld	|- ( ph -> seq 1 ( oF + , G ) e. dom ( ~~>u ` U ) )