Theorem lgamp1

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

	Ref	Expression
Assertion	lgamp1	⊢ ( 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) → ( log Γ ‘ ( 𝐴 + 1 ) ) = ( ( log Γ ‘ 𝐴 ) + ( log ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑚 ) + 1 ) ) ) ) = ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑚 ) + 1 ) ) ) )
2		id	⊢ ( 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) → 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
3	1 2	lgamcvg2	⊢ ( 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) → seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑚 ) + 1 ) ) ) ) ) ⇝ ( log Γ ‘ ( 𝐴 + 1 ) ) )
4	1 2	lgamcvg	⊢ ( 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) → seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑚 ) + 1 ) ) ) ) ) ⇝ ( ( log Γ ‘ 𝐴 ) + ( log ‘ 𝐴 ) ) )
5		climuni	⊢ ( ( seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑚 ) + 1 ) ) ) ) ) ⇝ ( log Γ ‘ ( 𝐴 + 1 ) ) ∧ seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑚 ) + 1 ) ) ) ) ) ⇝ ( ( log Γ ‘ 𝐴 ) + ( log ‘ 𝐴 ) ) ) → ( log Γ ‘ ( 𝐴 + 1 ) ) = ( ( log Γ ‘ 𝐴 ) + ( log ‘ 𝐴 ) ) )
6	3 4 5	syl2anc	⊢ ( 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) → ( log Γ ‘ ( 𝐴 + 1 ) ) = ( ( log Γ ‘ 𝐴 ) + ( log ‘ 𝐴 ) ) )