Theorem gamfac

Description: The Gamma function generalizes the factorial. (Contributed by Mario Carneiro, 9-Jul-2017)

	Ref	Expression
Assertion	gamfac	|- ( N e. NN -> ( _G ` N ) = ( ! ` ( N - 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		nnm1nn0	|- ( N e. NN -> ( N - 1 ) e. NN0 )
2		facgam	|- ( ( N - 1 ) e. NN0 -> ( ! ` ( N - 1 ) ) = ( _G ` ( ( N - 1 ) + 1 ) ) )
3	1 2	syl	|- ( N e. NN -> ( ! ` ( N - 1 ) ) = ( _G ` ( ( N - 1 ) + 1 ) ) )
4		nncn	|- ( N e. NN -> N e. CC )
5		1cnd	|- ( N e. NN -> 1 e. CC )
6	4 5	npcand	|- ( N e. NN -> ( ( N - 1 ) + 1 ) = N )
7	6	fveq2d	|- ( N e. NN -> ( _G ` ( ( N - 1 ) + 1 ) ) = ( _G ` N ) )
8	3 7	eqtr2d	|- ( N e. NN -> ( _G ` N ) = ( ! ` ( N - 1 ) ) )