Theorem eflgam

Description: The exponential of the log-Gamma function is the Gamma function (by definition). (Contributed by Mario Carneiro, 8-Jul-2017)

	Ref	Expression
Assertion	eflgam	⊢ ( 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) → ( exp ‘ ( log Γ ‘ 𝐴 ) ) = ( Γ ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		df-gam	⊢ Γ = ( exp ∘ log Γ )
2	1	fveq1i	⊢ ( Γ ‘ 𝐴 ) = ( ( exp ∘ log Γ ) ‘ 𝐴 )
3		lgamf	⊢ log Γ : ( ℂ ∖ ( ℤ ∖ ℕ ) ) ⟶ ℂ
4		fvco3	⊢ ( ( log Γ : ( ℂ ∖ ( ℤ ∖ ℕ ) ) ⟶ ℂ ∧ 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) → ( ( exp ∘ log Γ ) ‘ 𝐴 ) = ( exp ‘ ( log Γ ‘ 𝐴 ) ) )
5	3 4	mpan	⊢ ( 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) → ( ( exp ∘ log Γ ) ‘ 𝐴 ) = ( exp ‘ ( log Γ ‘ 𝐴 ) ) )
6	2 5	eqtr2id	⊢ ( 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) → ( exp ‘ ( log Γ ‘ 𝐴 ) ) = ( Γ ‘ 𝐴 ) )