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 syl5ibr n 0 n ! = Γ n + 1 n + 1 ! = Γ n + 1 + 1
27 5 8 11 14 15 26 nn0ind N 0 N ! = Γ N + 1