lgamp1

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

		Ref	Expression
	Assertion	lgamp1	$⊢ A \in (ℂ ∖ (ℤ ∖ ℕ)) \to \log Γ (A + 1) = \log Γ (A) + \log A$

Step	Hyp	Ref	Expression
1		eqid	$⊢ (m \in ℕ ⟼ A \log (\frac{m + 1}{m}) - \log ((\frac{A}{m}) + 1)) = (m \in ℕ ⟼ A \log (\frac{m + 1}{m}) - \log ((\frac{A}{m}) + 1))$
2		id	$⊢ A \in (ℂ ∖ (ℤ ∖ ℕ)) \to A \in (ℂ ∖ (ℤ ∖ ℕ))$
3	1 2	lgamcvg2	$⊢ A \in (ℂ ∖ (ℤ ∖ ℕ)) \to seq 1 (+ (m \in ℕ ⟼ A \log (\frac{m + 1}{m}) - \log ((\frac{A}{m}) + 1))) ⇝ \log Γ (A + 1)$
4	1 2	lgamcvg	$⊢ A \in (ℂ ∖ (ℤ ∖ ℕ)) \to seq 1 (+ (m \in ℕ ⟼ A \log (\frac{m + 1}{m}) - \log ((\frac{A}{m}) + 1))) ⇝ (\log Γ (A) + \log A)$
5		climuni	$⊢ (seq 1 (+ (m \in ℕ ⟼ A \log (\frac{m + 1}{m}) - \log ((\frac{A}{m}) + 1))) ⇝ \log Γ (A + 1) \land seq 1 (+ (m \in ℕ ⟼ A \log (\frac{m + 1}{m}) - \log ((\frac{A}{m}) + 1))) ⇝ (\log Γ (A) + \log A)) \to \log Γ (A + 1) = \log Γ (A) + \log A$
6	3 4 5	syl2anc	$⊢ A \in (ℂ ∖ (ℤ ∖ ℕ)) \to \log Γ (A + 1) = \log Γ (A) + \log A$

Metamath Proof Explorer