Metamath Proof Explorer

Theorem fallfacval

Description: The value of the falling factorial function. (Contributed by Scott Fenton, 5-Jan-2018)

Ref Expression
Assertion fallfacval 
|- ( ( A e. CC /\ N e. NN0 ) -> ( A FallFac N ) = prod_ k e. ( 0 ... ( N - 1 ) ) ( A - k ) )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( x = A -> ( x - k ) = ( A - k ) )
2 1 prodeq2sdv 
 |-  ( x = A -> prod_ k e. ( 0 ... ( n - 1 ) ) ( x - k ) = prod_ k e. ( 0 ... ( n - 1 ) ) ( A - k ) )
3 oveq1 
 |-  ( n = N -> ( n - 1 ) = ( N - 1 ) )
4 3 oveq2d 
 |-  ( n = N -> ( 0 ... ( n - 1 ) ) = ( 0 ... ( N - 1 ) ) )
5 4 prodeq1d 
 |-  ( n = N -> prod_ k e. ( 0 ... ( n - 1 ) ) ( A - k ) = prod_ k e. ( 0 ... ( N - 1 ) ) ( A - k ) )
6 df-fallfac 
 |-  FallFac = ( x e. CC , n e. NN0 |-> prod_ k e. ( 0 ... ( n - 1 ) ) ( x - k ) )
7 prodex 
 |-  prod_ k e. ( 0 ... ( N - 1 ) ) ( A - k ) e. _V
8 2 5 6 7 ovmpo 
 |-  ( ( A e. CC /\ N e. NN0 ) -> ( A FallFac N ) = prod_ k e. ( 0 ... ( N - 1 ) ) ( A - k ) )