Metamath Proof Explorer

Theorem facgam

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

Ref Expression
Assertion facgam 
|- ( N e. NN0 -> ( ! ` N ) = ( _G ` ( N + 1 ) ) )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( x = 0 -> ( ! ` x ) = ( ! ` 0 ) )
2 fv0p1e1 
 |-  ( x = 0 -> ( _G ` ( x + 1 ) ) = ( _G ` 1 ) )
3 gam1 
 |-  ( _G ` 1 ) = 1
4 2 3 eqtrdi 
 |-  ( x = 0 -> ( _G ` ( x + 1 ) ) = 1 )
5 1 4 eqeq12d 
 |-  ( x = 0 -> ( ( ! ` x ) = ( _G ` ( x + 1 ) ) <-> ( ! ` 0 ) = 1 ) )
6 fveq2 
 |-  ( x = n -> ( ! ` x ) = ( ! ` n ) )
7 fvoveq1 
 |-  ( x = n -> ( _G ` ( x + 1 ) ) = ( _G ` ( n + 1 ) ) )
8 6 7 eqeq12d 
 |-  ( x = n -> ( ( ! ` x ) = ( _G ` ( x + 1 ) ) <-> ( ! ` n ) = ( _G ` ( n + 1 ) ) ) )
9 fveq2 
 |-  ( x = ( n + 1 ) -> ( ! ` x ) = ( ! ` ( n + 1 ) ) )
10 fvoveq1 
 |-  ( x = ( n + 1 ) -> ( _G ` ( x + 1 ) ) = ( _G ` ( ( n + 1 ) + 1 ) ) )
11 9 10 eqeq12d 
 |-  ( x = ( n + 1 ) -> ( ( ! ` x ) = ( _G ` ( x + 1 ) ) <-> ( ! ` ( n + 1 ) ) = ( _G ` ( ( n + 1 ) + 1 ) ) ) )
12 fveq2 
 |-  ( x = N -> ( ! ` x ) = ( ! ` N ) )
13 fvoveq1 
 |-  ( x = N -> ( _G ` ( x + 1 ) ) = ( _G ` ( N + 1 ) ) )
14 12 13 eqeq12d 
 |-  ( x = N -> ( ( ! ` x ) = ( _G ` ( x + 1 ) ) <-> ( ! ` N ) = ( _G ` ( N + 1 ) ) ) )
15 fac0 
 |-  ( ! ` 0 ) = 1
16 oveq1 
 |-  ( ( ! ` n ) = ( _G ` ( n + 1 ) ) -> ( ( ! ` n ) x. ( n + 1 ) ) = ( ( _G ` ( n + 1 ) ) x. ( n + 1 ) ) )
17 facp1 
 |-  ( n e. NN0 -> ( ! ` ( n + 1 ) ) = ( ( ! ` n ) x. ( n + 1 ) ) )
18 nn0p1nn 
 |-  ( n e. NN0 -> ( n + 1 ) e. NN )
19 18 nncnd 
 |-  ( n e. NN0 -> ( n + 1 ) e. CC )
20 eldifn 
 |-  ( ( n + 1 ) e. ( ZZ \ NN ) -> -. ( n + 1 ) e. NN )
21 20 18 nsyl3 
 |-  ( n e. NN0 -> -. ( n + 1 ) e. ( ZZ \ NN ) )
22 19 21 eldifd 
 |-  ( n e. NN0 -> ( n + 1 ) e. ( CC \ ( ZZ \ NN ) ) )
23 gamp1 
 |-  ( ( n + 1 ) e. ( CC \ ( ZZ \ NN ) ) -> ( _G ` ( ( n + 1 ) + 1 ) ) = ( ( _G ` ( n + 1 ) ) x. ( n + 1 ) ) )
24 22 23 syl 
 |-  ( n e. NN0 -> ( _G ` ( ( n + 1 ) + 1 ) ) = ( ( _G ` ( n + 1 ) ) x. ( n + 1 ) ) )
25 17 24 eqeq12d 
 |-  ( n e. NN0 -> ( ( ! ` ( n + 1 ) ) = ( _G ` ( ( n + 1 ) + 1 ) ) <-> ( ( ! ` n ) x. ( n + 1 ) ) = ( ( _G ` ( n + 1 ) ) x. ( n + 1 ) ) ) )
26 16 25 syl5ibr 
 |-  ( n e. NN0 -> ( ( ! ` n ) = ( _G ` ( n + 1 ) ) -> ( ! ` ( n + 1 ) ) = ( _G ` ( ( n + 1 ) + 1 ) ) ) )
27 5 8 11 14 15 26 nn0ind 
 |-  ( N e. NN0 -> ( ! ` N ) = ( _G ` ( N + 1 ) ) )