gamp1

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

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

Proof

Step	Hyp	Ref	Expression
1		lgamp1	$⊢ A \in (ℂ ∖ (ℤ ∖ ℕ)) \to \log Γ (A + 1) = \log Γ (A) + \log A$
2	1	fveq2d	$⊢ A \in (ℂ ∖ (ℤ ∖ ℕ)) \to e^{\log Γ (A + 1)} = e^{\log Γ (A) + \log A}$
3		lgamcl	$⊢ A \in (ℂ ∖ (ℤ ∖ ℕ)) \to \log Γ (A) \in ℂ$
4		eldifi	$⊢ A \in (ℂ ∖ (ℤ ∖ ℕ)) \to A \in ℂ$
5		id	$⊢ A \in (ℂ ∖ (ℤ ∖ ℕ)) \to A \in (ℂ ∖ (ℤ ∖ ℕ))$
6	5	dmgmn0	$⊢ A \in (ℂ ∖ (ℤ ∖ ℕ)) \to A \neq 0$
7	4 6	logcld	$⊢ A \in (ℂ ∖ (ℤ ∖ ℕ)) \to \log A \in ℂ$
8		efadd	$⊢ (\log Γ (A) \in ℂ \land \log A \in ℂ) \to e^{\log Γ (A) + \log A} = e^{\log Γ (A)} e^{\log A}$
9	3 7 8	syl2anc	$⊢ A \in (ℂ ∖ (ℤ ∖ ℕ)) \to e^{\log Γ (A) + \log A} = e^{\log Γ (A)} e^{\log A}$
10		eflog	$⊢ (A \in ℂ \land A \neq 0) \to e^{\log A} = A$
11	4 6 10	syl2anc	$⊢ A \in (ℂ ∖ (ℤ ∖ ℕ)) \to e^{\log A} = A$
12	11	oveq2d	$⊢ A \in (ℂ ∖ (ℤ ∖ ℕ)) \to e^{\log Γ (A)} e^{\log A} = e^{\log Γ (A)} A$
13	2 9 12	3eqtrd	$⊢ A \in (ℂ ∖ (ℤ ∖ ℕ)) \to e^{\log Γ (A + 1)} = e^{\log Γ (A)} A$
14		1nn0	$⊢ 1 \in ℕ_{0}$
15	14	a1i	$⊢ A \in (ℂ ∖ (ℤ ∖ ℕ)) \to 1 \in ℕ_{0}$
16	5 15	dmgmaddnn0	$⊢ A \in (ℂ ∖ (ℤ ∖ ℕ)) \to A + 1 \in (ℂ ∖ (ℤ ∖ ℕ))$
17		eflgam	$⊢ A + 1 \in (ℂ ∖ (ℤ ∖ ℕ)) \to e^{\log Γ (A + 1)} = Γ (A + 1)$
18	16 17	syl	$⊢ A \in (ℂ ∖ (ℤ ∖ ℕ)) \to e^{\log Γ (A + 1)} = Γ (A + 1)$
19		eflgam	$⊢ A \in (ℂ ∖ (ℤ ∖ ℕ)) \to e^{\log Γ (A)} = Γ (A)$
20	19	oveq1d	$⊢ A \in (ℂ ∖ (ℤ ∖ ℕ)) \to e^{\log Γ (A)} A = Γ (A) A$
21	13 18 20	3eqtr3d	$⊢ A \in (ℂ ∖ (ℤ ∖ ℕ)) \to Γ (A + 1) = Γ (A) A$

Metamath Proof Explorer

Theorem gamp1

Proof