Metamath Proof Explorer

Theorem facgam

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

Ref Expression
Assertion facgam ⊢N∈ℕ0→N!=Γ⁡N+1

Proof

Step Hyp Ref Expression
1 fveq2 ⊢x=0→x!=0!
2 fv0p1e1 ⊢x=0→Γ⁡x+1=Γ⁡1
3 gam1 ⊢Γ⁡1=1
4 2 3 eqtrdi ⊢x=0→Γ⁡x+1=1
5 1 4 eqeq12d ⊢x=0→x!=Γ⁡x+1↔0!=1
6 fveq2 ⊢x=n→x!=n!
7 fvoveq1 ⊢x=n→Γ⁡x+1=Γ⁡n+1
8 6 7 eqeq12d ⊢x=n→x!=Γ⁡x+1↔n!=Γ⁡n+1
9 fveq2 ⊢x=n+1→x!=n+1!
10 fvoveq1 ⊢x=n+1→Γ⁡x+1=Γ⁡n+1+1
11 9 10 eqeq12d ⊢x=n+1→x!=Γ⁡x+1↔n+1!=Γ⁡n+1+1
12 fveq2 ⊢x=N→x!=N!
13 fvoveq1 ⊢x=N→Γ⁡x+1=Γ⁡N+1
14 12 13 eqeq12d ⊢x=N→x!=Γ⁡x+1↔N!=Γ⁡N+1
15 fac0 ⊢0!=1
16 oveq1 ⊢n!=Γ⁡n+1→n!⁢n+1=Γ⁡n+1⁢n+1
17 facp1 ⊢n∈ℕ0→n+1!=n!⁢n+1
18 nn0p1nn ⊢n∈ℕ0→n+1∈ℕ
19 18 nncnd ⊢n∈ℕ0→n+1∈ℂ
20 eldifn ⊢n+1∈ℤ∖ℕ→¬n+1∈ℕ
21 20 18 nsyl3 ⊢n∈ℕ0→¬n+1∈ℤ∖ℕ
22 19 21 eldifd ⊢n∈ℕ0→n+1∈ℂ∖ℤ∖ℕ
23 gamp1 ⊢n+1∈ℂ∖ℤ∖ℕ→Γ⁡n+1+1=Γ⁡n+1⁢n+1
24 22 23 syl ⊢n∈ℕ0→Γ⁡n+1+1=Γ⁡n+1⁢n+1
25 17 24 eqeq12d ⊢n∈ℕ0→n+1!=Γ⁡n+1+1↔n!⁢n+1=Γ⁡n+1⁢n+1
26 16 25 imbitrrid ⊢n∈ℕ0→n!=Γ⁡n+1→n+1!=Γ⁡n+1+1
27 5 8 11 14 15 26 nn0ind ⊢N∈ℕ0→N!=Γ⁡N+1