# Metamath Proof Explorer

## Theorem facgam

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

Ref Expression
Assertion facgam ${⊢}{N}\in {ℕ}_{0}\to {N}!=\mathrm{\Gamma }\left({N}+1\right)$

### Proof

Step Hyp Ref Expression
1 fveq2 ${⊢}{x}=0\to {x}!=0!$
2 fv0p1e1 ${⊢}{x}=0\to \mathrm{\Gamma }\left({x}+1\right)=\mathrm{\Gamma }\left(1\right)$
3 gam1 ${⊢}\mathrm{\Gamma }\left(1\right)=1$
4 2 3 syl6eq ${⊢}{x}=0\to \mathrm{\Gamma }\left({x}+1\right)=1$
5 1 4 eqeq12d ${⊢}{x}=0\to \left({x}!=\mathrm{\Gamma }\left({x}+1\right)↔0!=1\right)$
6 fveq2 ${⊢}{x}={n}\to {x}!={n}!$
7 fvoveq1 ${⊢}{x}={n}\to \mathrm{\Gamma }\left({x}+1\right)=\mathrm{\Gamma }\left({n}+1\right)$
8 6 7 eqeq12d ${⊢}{x}={n}\to \left({x}!=\mathrm{\Gamma }\left({x}+1\right)↔{n}!=\mathrm{\Gamma }\left({n}+1\right)\right)$
9 fveq2 ${⊢}{x}={n}+1\to {x}!=\left({n}+1\right)!$
10 fvoveq1 ${⊢}{x}={n}+1\to \mathrm{\Gamma }\left({x}+1\right)=\mathrm{\Gamma }\left({n}+1+1\right)$
11 9 10 eqeq12d ${⊢}{x}={n}+1\to \left({x}!=\mathrm{\Gamma }\left({x}+1\right)↔\left({n}+1\right)!=\mathrm{\Gamma }\left({n}+1+1\right)\right)$
12 fveq2 ${⊢}{x}={N}\to {x}!={N}!$
13 fvoveq1 ${⊢}{x}={N}\to \mathrm{\Gamma }\left({x}+1\right)=\mathrm{\Gamma }\left({N}+1\right)$
14 12 13 eqeq12d ${⊢}{x}={N}\to \left({x}!=\mathrm{\Gamma }\left({x}+1\right)↔{N}!=\mathrm{\Gamma }\left({N}+1\right)\right)$
15 fac0 ${⊢}0!=1$
16 oveq1 ${⊢}{n}!=\mathrm{\Gamma }\left({n}+1\right)\to {n}!\left({n}+1\right)=\mathrm{\Gamma }\left({n}+1\right)\left({n}+1\right)$
17 facp1 ${⊢}{n}\in {ℕ}_{0}\to \left({n}+1\right)!={n}!\left({n}+1\right)$
18 nn0p1nn ${⊢}{n}\in {ℕ}_{0}\to {n}+1\in ℕ$
19 18 nncnd ${⊢}{n}\in {ℕ}_{0}\to {n}+1\in ℂ$
20 eldifn ${⊢}{n}+1\in \left(ℤ\setminus ℕ\right)\to ¬{n}+1\in ℕ$
21 20 18 nsyl3 ${⊢}{n}\in {ℕ}_{0}\to ¬{n}+1\in \left(ℤ\setminus ℕ\right)$
22 19 21 eldifd ${⊢}{n}\in {ℕ}_{0}\to {n}+1\in \left(ℂ\setminus \left(ℤ\setminus ℕ\right)\right)$
23 gamp1 ${⊢}{n}+1\in \left(ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\to \mathrm{\Gamma }\left({n}+1+1\right)=\mathrm{\Gamma }\left({n}+1\right)\left({n}+1\right)$
24 22 23 syl ${⊢}{n}\in {ℕ}_{0}\to \mathrm{\Gamma }\left({n}+1+1\right)=\mathrm{\Gamma }\left({n}+1\right)\left({n}+1\right)$
25 17 24 eqeq12d ${⊢}{n}\in {ℕ}_{0}\to \left(\left({n}+1\right)!=\mathrm{\Gamma }\left({n}+1+1\right)↔{n}!\left({n}+1\right)=\mathrm{\Gamma }\left({n}+1\right)\left({n}+1\right)\right)$
26 16 25 syl5ibr ${⊢}{n}\in {ℕ}_{0}\to \left({n}!=\mathrm{\Gamma }\left({n}+1\right)\to \left({n}+1\right)!=\mathrm{\Gamma }\left({n}+1+1\right)\right)$
27 5 8 11 14 15 26 nn0ind ${⊢}{N}\in {ℕ}_{0}\to {N}!=\mathrm{\Gamma }\left({N}+1\right)$