Mathbox for Mario Carneiro < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-lgam Unicode version

Definition df-lgam 23692
 Description: Define the log-Gamma function. We can work with this form of the gamma function a bit easier than the equivalent expression for the gamma function itself, and moreover this function is not actually equal to because the branch cuts are placed differently (we do have , though). This definition is attributed to Euler, and unlike the usual integral definition is defined on the entire complex plane except the nonpositive integers , where the function has simple poles. (Contributed by Mario Carneiro, 12-Jul-2014.)
Assertion
Ref Expression
df-lgam
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-lgam
StepHypRef Expression
1 clgam 23690 . 2
2 vz . . 3
3 cc 8735 . . . 4
4 cz 10024 . . . . 5
5 cn 9746 . . . . 5
64, 5cdif 3149 . . . 4
73, 6cdif 3149 . . 3
8 vn . . . . 5
92cv 1622 . . . . . . . 8
108cv 1622 . . . . . . . . 9
11 clog 19912 . . . . . . . . 9
1210, 11cfv 5255 . . . . . . . 8
13 cmul 8742 . . . . . . . 8
149, 12, 13co 5858 . . . . . . 7
159, 11cfv 5255 . . . . . . 7
16 cmin 9037 . . . . . . 7
1714, 15, 16co 5858 . . . . . 6
18 c1 8738 . . . . . . . 8
19 cfz 10782 . . . . . . . 8
2018, 10, 19co 5858 . . . . . . 7
21 vm . . . . . . . . . . 11
2221cv 1622 . . . . . . . . . 10
23 cdiv 9423 . . . . . . . . . 10
249, 22, 23co 5858 . . . . . . . . 9
25 caddc 8740 . . . . . . . . 9
2624, 18, 25co 5858 . . . . . . . 8
2726, 11cfv 5255 . . . . . . 7
2820, 27, 21csu 12158 . . . . . 6
2917, 28, 16co 5858 . . . . 5
308, 5, 29cmpt 4077 . . . 4
31 cli 11958 . . . 4
3230, 31cfv 5255 . . 3
332, 7, 32cmpt 4077 . 2
341, 33wceq 1623 1
 Colors of variables: wff set class
 Copyright terms: Public domain W3C validator