Metamath Proof Explorer

Theorem gamp1

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

Ref Expression
Assertion gamp1 ( 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) → ( Γ ‘ ( 𝐴 + 1 ) ) = ( ( Γ ‘ 𝐴 ) · 𝐴 ) )

Proof

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