Metamath Proof Explorer


Theorem lgamf

Description: The log-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 lgamf logΓ:

Proof

Step Hyp Ref Expression
1 ovexd xnxlogn+1nlogxn+1logxV
2 df-lgam logΓ=xnxlogn+1nlogxn+1logx
3 2 a1i logΓ=xnxlogn+1nlogxn+1logx
4 lgamcl xlogΓx
5 4 adantl xlogΓx
6 1 3 5 fmpt2d logΓ:
7 6 mptru logΓ: