Metamath Proof Explorer

Theorem gamp1

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

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

Proof

Step Hyp Ref Expression
1 lgamp1 ⊢ A ∈ ℂ ∖ ℤ ∖ ℕ → log Γ ⁡ A + 1 = log Γ ⁡ A + log ⁡ A
2 1 fveq2d ⊢ A ∈ ℂ ∖ ℤ ∖ ℕ → e log Γ ⁡ A + 1 = e log Γ ⁡ A + log ⁡ A
3 lgamcl ⊢ A ∈ ℂ ∖ ℤ ∖ ℕ → log Γ ⁡ A ∈ ℂ
4 eldifi ⊢ A ∈ ℂ ∖ ℤ ∖ ℕ → A ∈ ℂ
5 id ⊢ A ∈ ℂ ∖ ℤ ∖ ℕ → A ∈ ℂ ∖ ℤ ∖ ℕ
6 5 dmgmn0 ⊢ A ∈ ℂ ∖ ℤ ∖ ℕ → A ≠ 0
7 4 6 logcld ⊢ A ∈ ℂ ∖ ℤ ∖ ℕ → log ⁡ A ∈ ℂ
8 efadd ⊢ log Γ ⁡ A ∈ ℂ ∧ log ⁡ A ∈ ℂ → e log Γ ⁡ A + log ⁡ A = e log Γ ⁡ A ⁢ e log ⁡ A
9 3 7 8 syl2anc ⊢ A ∈ ℂ ∖ ℤ ∖ ℕ → e log Γ ⁡ A + log ⁡ A = e log Γ ⁡ A ⁢ e log ⁡ A
10 eflog ⊢ A ∈ ℂ ∧ A ≠ 0 → e log ⁡ A = A
11 4 6 10 syl2anc ⊢ A ∈ ℂ ∖ ℤ ∖ ℕ → e log ⁡ A = A
12 11 oveq2d ⊢ A ∈ ℂ ∖ ℤ ∖ ℕ → e log Γ ⁡ A ⁢ e log ⁡ A = e log Γ ⁡ A ⁢ A
13 2 9 12 3eqtrd ⊢ A ∈ ℂ ∖ ℤ ∖ ℕ → e log Γ ⁡ A + 1 = e log Γ ⁡ A ⁢ A
14 1nn0 ⊢ 1 ∈ ℕ 0
15 14 a1i ⊢ A ∈ ℂ ∖ ℤ ∖ ℕ → 1 ∈ ℕ 0
16 5 15 dmgmaddnn0 ⊢ A ∈ ℂ ∖ ℤ ∖ ℕ → A + 1 ∈ ℂ ∖ ℤ ∖ ℕ
17 eflgam ⊢ A + 1 ∈ ℂ ∖ ℤ ∖ ℕ → e log Γ ⁡ A + 1 = Γ ⁡ A + 1
18 16 17 syl ⊢ A ∈ ℂ ∖ ℤ ∖ ℕ → e log Γ ⁡ A + 1 = Γ ⁡ A + 1
19 eflgam ⊢ A ∈ ℂ ∖ ℤ ∖ ℕ → e log Γ ⁡ A = Γ ⁡ A
20 19 oveq1d ⊢ A ∈ ℂ ∖ ℤ ∖ ℕ → e log Γ ⁡ A ⁢ A = Γ ⁡ A ⁢ A
21 13 18 20 3eqtr3d ⊢ A ∈ ℂ ∖ ℤ ∖ ℕ → Γ ⁡ A + 1 = Γ ⁡ A ⁢ A