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