Theorem gamfac

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

	Ref	Expression
Assertion	gamfac	⊢ ( 𝑁 ∈ ℕ → ( Γ ‘ 𝑁 ) = ( ! ‘ ( 𝑁 − 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		nnm1nn0	⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ0 )
2		facgam	⊢ ( ( 𝑁 − 1 ) ∈ ℕ0 → ( ! ‘ ( 𝑁 − 1 ) ) = ( Γ ‘ ( ( 𝑁 − 1 ) + 1 ) ) )
3	1 2	syl	⊢ ( 𝑁 ∈ ℕ → ( ! ‘ ( 𝑁 − 1 ) ) = ( Γ ‘ ( ( 𝑁 − 1 ) + 1 ) ) )
4		nncn	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
5		1cnd	⊢ ( 𝑁 ∈ ℕ → 1 ∈ ℂ )
6	4 5	npcand	⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
7	6	fveq2d	⊢ ( 𝑁 ∈ ℕ → ( Γ ‘ ( ( 𝑁 − 1 ) + 1 ) ) = ( Γ ‘ 𝑁 ) )
8	3 7	eqtr2d	⊢ ( 𝑁 ∈ ℕ → ( Γ ‘ 𝑁 ) = ( ! ‘ ( 𝑁 − 1 ) ) )