Theorem gamfac

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

	Ref	Expression
Assertion	gamfac	$$⊢N\in \mathbb{N}\to \mathrm{\Gamma }\left(N\right)=\left(N-1\right)!$$

Proof

Step	Hyp	Ref	Expression
1		nnm1nn0	$$⊢N\in \mathbb{N}\to N-1\in {\mathbb{N}}_0$$
2		facgam	$$⊢N-1\in {\mathbb{N}}_0\to \left(N-1\right)!=\mathrm{\Gamma }\left(N-1+1\right)$$
3	1 2	syl	$$⊢N\in \mathbb{N}\to \left(N-1\right)!=\mathrm{\Gamma }\left(N-1+1\right)$$
4		nncn	$$⊢N\in \mathbb{N}\to N\in ℂ$$
5		1cnd	$$⊢N\in \mathbb{N}\to 1\in ℂ$$
6	4 5	npcand	$$⊢N\in \mathbb{N}\to N-1+1=N$$
7	6	fveq2d	$$⊢N\in \mathbb{N}\to \mathrm{\Gamma }\left(N-1+1\right)=\mathrm{\Gamma }\left(N\right)$$
8	3 7	eqtr2d	$$⊢N\in \mathbb{N}\to \mathrm{\Gamma }\left(N\right)=\left(N-1\right)!$$