df-lgam - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > df-lgam		Structured version Visualization version Unicode version

Definition df-lgam 24745

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**
Step	Hyp	Ref	Expression
1		clgam 24742	. 2
2		vz	. . 3
3		cc 9934	. . . 4
4		cz 11377	. . . . 5
5		cn 11020	. . . . 5
6	4, 5	cdif 3571	. . . 4 $\$
7	3, 6	cdif 3571	. . 3 $\$ $\$
8	2	cv 1482	. . . . . . 7
9		vm	. . . . . . . . . . 11
10	9	cv 1482	. . . . . . . . . 10
11		c1 9937	. . . . . . . . . 10
12		caddc 9939	. . . . . . . . . 10
13	10, 11, 12	co 6650	. . . . . . . . 9
14		cdiv 10684	. . . . . . . . 9
15	13, 10, 14	co 6650	. . . . . . . 8
16		clog 24301	. . . . . . . 8
17	15, 16	cfv 5888	. . . . . . 7
18		cmul 9941	. . . . . . 7
19	8, 17, 18	co 6650	. . . . . 6
20	8, 10, 14	co 6650	. . . . . . . 8
21	20, 11, 12	co 6650	. . . . . . 7
22	21, 16	cfv 5888	. . . . . 6
23		cmin 10266	. . . . . 6
24	19, 22, 23	co 6650	. . . . 5
25	5, 24, 9	csu 14416	. . . 4
26	8, 16	cfv 5888	. . . 4
27	25, 26, 23	co 6650	. . 3
28	2, 7, 27	cmpt 4729	. 2 $\$ $\$
29	1, 28	wceq 1483	1 $\$ $\$

Colors of variables: wff setvar class

This definition is referenced by: lgamgulm2 24762 lgamf 24768 iprodgam 31628

W3C validator