Description: The exponential of the log-Gamma function is the Gamma function (by definition). (Contributed by Mario Carneiro, 8-Jul-2017)
Ref | Expression | ||
---|---|---|---|
Assertion | gamcl | ⊢ ( 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) → ( Γ ‘ 𝐴 ) ∈ ℂ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | gamf | ⊢ Γ : ( ℂ ∖ ( ℤ ∖ ℕ ) ) ⟶ ℂ | |
2 | 1 | ffvelrni | ⊢ ( 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) → ( Γ ‘ 𝐴 ) ∈ ℂ ) |