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

Definition df-lgam 28189
 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 28186 . 2
2 vz . . 3
3 cc 9481 . . . 4
4 cz 10855 . . . . 5
5 cn 10527 . . . . 5
64, 5cdif 3468 . . . 4
73, 6cdif 3468 . . 3
82cv 1373 . . . . . . 7
9 vm . . . . . . . . . . 11
109cv 1373 . . . . . . . . . 10
11 c1 9484 . . . . . . . . . 10
12 caddc 9486 . . . . . . . . . 10
1310, 11, 12co 6277 . . . . . . . . 9
14 cdiv 10197 . . . . . . . . 9
1513, 10, 14co 6277 . . . . . . . 8
16 clog 22665 . . . . . . . 8
1715, 16cfv 5581 . . . . . . 7
18 cmul 9488 . . . . . . 7
198, 17, 18co 6277 . . . . . 6
208, 10, 14co 6277 . . . . . . . 8
2120, 11, 12co 6277 . . . . . . 7
2221, 16cfv 5581 . . . . . 6
23 cmin 9796 . . . . . 6
2419, 22, 23co 6277 . . . . 5
255, 24, 9csu 13459 . . . 4
268, 16cfv 5581 . . . 4
2725, 26, 23co 6277 . . 3
282, 7, 27cmpt 4500 . 2
291, 28wceq 1374 1
 Colors of variables: wff setvar class This definition is referenced by:  lgamgulm2  28206  lgamf  28212  iprodgam  28690
 Copyright terms: Public domain W3C validator