Metamath Proof Explorer

Theorem fallfacfac

Description: Relate falling factorial to factorial. (Contributed by Scott Fenton, 5-Jan-2018)

Ref Expression
Assertion fallfacfac 
|- ( N e. NN0 -> ( N FallFac N ) = ( ! ` N ) )

Proof

Step Hyp Ref Expression
1 nn0fz0 
 |-  ( N e. NN0 <-> N e. ( 0 ... N ) )
2 fallfacval4 
 |-  ( N e. ( 0 ... N ) -> ( N FallFac N ) = ( ( ! ` N ) / ( ! ` ( N - N ) ) ) )
3 1 2 sylbi 
 |-  ( N e. NN0 -> ( N FallFac N ) = ( ( ! ` N ) / ( ! ` ( N - N ) ) ) )
4 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
5 4 subidd 
 |-  ( N e. NN0 -> ( N - N ) = 0 )
6 5 fveq2d 
 |-  ( N e. NN0 -> ( ! ` ( N - N ) ) = ( ! ` 0 ) )
7 fac0 
 |-  ( ! ` 0 ) = 1
8 6 7 eqtrdi 
 |-  ( N e. NN0 -> ( ! ` ( N - N ) ) = 1 )
9 8 oveq2d 
 |-  ( N e. NN0 -> ( ( ! ` N ) / ( ! ` ( N - N ) ) ) = ( ( ! ` N ) / 1 ) )
10 faccl 
 |-  ( N e. NN0 -> ( ! ` N ) e. NN )
11 10 nncnd 
 |-  ( N e. NN0 -> ( ! ` N ) e. CC )
12 11 div1d 
 |-  ( N e. NN0 -> ( ( ! ` N ) / 1 ) = ( ! ` N ) )
13 3 9 12 3eqtrd 
 |-  ( N e. NN0 -> ( N FallFac N ) = ( ! ` N ) )