Theorem gamcvg2

Description: An infinite product expression for the gamma function. (Contributed by Mario Carneiro, 9-Jul-2017)

	Ref	Expression
Hypotheses	gamcvg2.f	|- F = ( m e. NN |-> ( ( ( ( m + 1 ) / m ) ^c A ) / ( ( A / m ) + 1 ) ) )
	gamcvg2.a	|- ( ph -> A e. ( CC \ ( ZZ \ NN ) ) )
Assertion	gamcvg2	|- ( ph -> seq 1 ( x. , F ) ~~> ( ( _G ` A ) x. A ) )

Proof

Step	Hyp	Ref	Expression
1		gamcvg2.f	|- F = ( m e. NN |-> ( ( ( ( m + 1 ) / m ) ^c A ) / ( ( A / m ) + 1 ) ) )
2		gamcvg2.a	|- ( ph -> A e. ( CC \ ( ZZ \ NN ) ) )
3		eqid	|- ( m e. NN |-> ( ( A x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( A / m ) + 1 ) ) ) ) = ( m e. NN |-> ( ( A x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( A / m ) + 1 ) ) ) )
4	1 2 3	gamcvg2lem	|- ( ph -> ( exp o. seq 1 ( + , ( m e. NN |-> ( ( A x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( A / m ) + 1 ) ) ) ) ) ) = seq 1 ( x. , F ) )
5	3 2	gamcvg	|- ( ph -> ( exp o. seq 1 ( + , ( m e. NN |-> ( ( A x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( A / m ) + 1 ) ) ) ) ) ) ~~> ( ( _G ` A ) x. A ) )
6	4 5	eqbrtrrd	|- ( ph -> seq 1 ( x. , F ) ~~> ( ( _G ` A ) x. A ) )