Theorem lgamcl

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

	Ref	Expression
Assertion	lgamcl	⊢ ( 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) → ( log Γ ‘ 𝐴 ) ∈ ℂ )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ { 𝑥 ∈ ℂ ∣ ( ( abs ‘ 𝑥 ) ≤ 𝑟 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑟 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) } = { 𝑥 ∈ ℂ ∣ ( ( abs ‘ 𝑥 ) ≤ 𝑟 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑟 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) }
2		id	⊢ ( 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) → 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
3		eqid	⊢ ( 𝑛 ∈ ℕ ↦ ( ( 𝐴 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑛 ) + 1 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( 𝐴 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑛 ) + 1 ) ) ) )
4	1 2 3	lgamcvglem	⊢ ( 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) → ( ( log Γ ‘ 𝐴 ) ∈ ℂ ∧ seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( ( 𝐴 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑛 ) + 1 ) ) ) ) ) ⇝ ( ( log Γ ‘ 𝐴 ) + ( log ‘ 𝐴 ) ) ) )
5	4	simpld	⊢ ( 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) → ( log Γ ‘ 𝐴 ) ∈ ℂ )