Theorem lgamp1

Description: The functional equation of the (log) Gamma function. (Contributed by Mario Carneiro, 9-Jul-2017)

	Ref	Expression
Assertion	lgamp1	|- ( A e. ( CC \ ( ZZ \ NN ) ) -> ( log_G ` ( A + 1 ) ) = ( ( log_G ` A ) + ( log ` A ) ) )

Proof

Step	Hyp	Ref	Expression
1		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 ) ) ) )
2		id	|- ( A e. ( CC \ ( ZZ \ NN ) ) -> A e. ( CC \ ( ZZ \ NN ) ) )
3	1 2	lgamcvg2	|- ( A e. ( CC \ ( ZZ \ NN ) ) -> seq 1 ( + , ( m e. NN |-> ( ( A x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( A / m ) + 1 ) ) ) ) ) ~~> ( log_G ` ( A + 1 ) ) )
4	1 2	lgamcvg	|- ( A e. ( CC \ ( ZZ \ NN ) ) -> seq 1 ( + , ( m e. NN |-> ( ( A x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( A / m ) + 1 ) ) ) ) ) ~~> ( ( log_G ` A ) + ( log ` A ) ) )
5		climuni	|- ( ( seq 1 ( + , ( m e. NN |-> ( ( A x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( A / m ) + 1 ) ) ) ) ) ~~> ( log_G ` ( A + 1 ) ) /\ seq 1 ( + , ( m e. NN |-> ( ( A x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( A / m ) + 1 ) ) ) ) ) ~~> ( ( log_G ` A ) + ( log ` A ) ) ) -> ( log_G ` ( A + 1 ) ) = ( ( log_G ` A ) + ( log ` A ) ) )
6	3 4 5	syl2anc	|- ( A e. ( CC \ ( ZZ \ NN ) ) -> ( log_G ` ( A + 1 ) ) = ( ( log_G ` A ) + ( log ` A ) ) )