Theorem gamf

Description: The 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	gamf	|- _G : ( CC \ ( ZZ \ NN ) ) --> CC

Proof

Step	Hyp	Ref	Expression
1		eff	|- exp : CC --> CC
2		lgamf	|- log_G : ( CC \ ( ZZ \ NN ) ) --> CC
3		fco	|- ( ( exp : CC --> CC /\ log_G : ( CC \ ( ZZ \ NN ) ) --> CC ) -> ( exp o. log_G ) : ( CC \ ( ZZ \ NN ) ) --> CC )
4	1 2 3	mp2an	|- ( exp o. log_G ) : ( CC \ ( ZZ \ NN ) ) --> CC
5		df-gam	|- _G = ( exp o. log_G )
6	5	feq1i	|- ( _G : ( CC \ ( ZZ \ NN ) ) --> CC <-> ( exp o. log_G ) : ( CC \ ( ZZ \ NN ) ) --> CC )
7	4 6	mpbir	|- _G : ( CC \ ( ZZ \ NN ) ) --> CC