Metamath Proof Explorer

Theorem gamfac

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

Ref Expression
Assertion gamfac ⊢ N ∈ ℕ → Γ ⁡ N = N − 1 !

Proof

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