Metamath Proof Explorer


Theorem gamf

Description: The Gamma function is a complex function defined on the whole complex plane except for the negative integers. (Contributed by Mario Carneiro, 6-Jul-2017)

Ref Expression
Assertion gamf Γ :

Proof

Step Hyp Ref Expression
1 eff exp :
2 lgamf log Γ :
3 fco exp : log Γ : exp log Γ :
4 1 2 3 mp2an exp log Γ :
5 df-gam Γ = exp log Γ
6 5 feq1i Γ : exp log Γ :
7 4 6 mpbir Γ :