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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ovexd | |
|
2 | df-lgam | |
|
3 | 2 | a1i | |
4 | lgamcl | |
|
5 | 4 | adantl | |
6 | 1 3 5 | fmpt2d | |
7 | 6 | mptru | |