Theorem facgam

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

	Ref	Expression
Assertion	facgam	⊢ ( 𝑁 ∈ ℕ0 → ( ! ‘ 𝑁 ) = ( Γ ‘ ( 𝑁 + 1 ) ) )

Proof

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