Definition df-gam 24746

Description: Define the Gamma function. See df-lgam 24745 for more information about the reason for this definition in terms of the log-gamma function. (Contributed by Mario Carneiro, 12-Jul-2014.)

Assertion

Ref	Expression
df-gam	|- _G = ( exp o. log _G )

Detailed syntax breakdown of Definition df-gam

Step	Hyp	Ref	Expression
1		cgam 24743	. 2 class _G
2		ce 14792	. . 3 class exp
3		clgam 24742	. . 3 class log _G
4	2, 3	ccom 5118	. 2 class ( exp o. log _G )
5	1, 4	wceq 1483	1 wff _G = ( exp o. log _G )

This definition is referenced by:  gamf  24769  eflgam  24771