Theorem lgamf

Description: The log-Gamma function is a complex function defined on the whole complex plane except for the negative integers. (Contributed by Mario Carneiro, 6-Jul-2017)

	Ref	Expression
Assertion	lgamf	⊢ log Γ : ( ℂ ∖ ( ℤ ∖ ℕ ) ) ⟶ ℂ

Proof

Step	Hyp	Ref	Expression
1		ovexd	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) → ( Σ 𝑛 ∈ ℕ ( ( 𝑥 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝑥 / 𝑛 ) + 1 ) ) ) − ( log ‘ 𝑥 ) ) ∈ V )
2		df-lgam	⊢ log Γ = ( 𝑥 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ↦ ( Σ 𝑛 ∈ ℕ ( ( 𝑥 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝑥 / 𝑛 ) + 1 ) ) ) − ( log ‘ 𝑥 ) ) )
3	2	a1i	⊢ ( ⊤ → log Γ = ( 𝑥 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ↦ ( Σ 𝑛 ∈ ℕ ( ( 𝑥 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝑥 / 𝑛 ) + 1 ) ) ) − ( log ‘ 𝑥 ) ) ) )
4		lgamcl	⊢ ( 𝑥 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) → ( log Γ ‘ 𝑥 ) ∈ ℂ )
5	4	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) → ( log Γ ‘ 𝑥 ) ∈ ℂ )
6	1 3 5	fmpt2d	⊢ ( ⊤ → log Γ : ( ℂ ∖ ( ℤ ∖ ℕ ) ) ⟶ ℂ )
7	6	mptru	⊢ log Γ : ( ℂ ∖ ( ℤ ∖ ℕ ) ) ⟶ ℂ