Metamath Proof Explorer

Theorem risefacval

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

Ref Expression
Assertion risefacval 
|- ( ( A e. CC /\ N e. NN0 ) -> ( A RiseFac 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-risefac 
 |-  RiseFac = ( 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 RiseFac N ) = prod_ k e. ( 0 ... ( N - 1 ) ) ( A + k ) )