Metamath Proof Explorer

Theorem lgamp1

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

Ref Expression
Assertion lgamp1 ⊢ A ∈ ℂ ∖ ℤ ∖ ℕ → log Γ ⁡ A + 1 = log Γ ⁡ A + log ⁡ A

Proof

Step Hyp Ref Expression
1 eqid ⊢ m ∈ ℕ ⟼ A ⁢ log ⁡ m + 1 m − log ⁡ A m + 1 = m ∈ ℕ ⟼ A ⁢ log ⁡ m + 1 m − log ⁡ A m + 1
2 id ⊢ A ∈ ℂ ∖ ℤ ∖ ℕ → A ∈ ℂ ∖ ℤ ∖ ℕ
3 1 2 lgamcvg2 ⊢ A ∈ ℂ ∖ ℤ ∖ ℕ → seq 1 + m ∈ ℕ ⟼ A ⁢ log ⁡ m + 1 m − log ⁡ A m + 1 ⇝ log Γ ⁡ A + 1
4 1 2 lgamcvg ⊢ A ∈ ℂ ∖ ℤ ∖ ℕ → seq 1 + m ∈ ℕ ⟼ A ⁢ log ⁡ m + 1 m − log ⁡ A m + 1 ⇝ log Γ ⁡ A + log ⁡ A
5 climuni ⊢ seq 1 + m ∈ ℕ ⟼ A ⁢ log ⁡ m + 1 m − log ⁡ A m + 1 ⇝ log Γ ⁡ A + 1 ∧ seq 1 + m ∈ ℕ ⟼ A ⁢ log ⁡ m + 1 m − log ⁡ A m + 1 ⇝ log Γ ⁡ A + log ⁡ A → log Γ ⁡ A + 1 = log Γ ⁡ A + log ⁡ A
6 3 4 5 syl2anc ⊢ A ∈ ℂ ∖ ℤ ∖ ℕ → log Γ ⁡ A + 1 = log Γ ⁡ A + log ⁡ A