Metamath Proof Explorer

Theorem risefac0

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

Ref Expression
Assertion risefac0 
|- ( A e. CC -> ( A RiseFac 0 ) = 1 )

Proof

Step Hyp Ref Expression
1 0nn0 
 |-  0 e. NN0
2 risefacval 
 |-  ( ( A e. CC /\ 0 e. NN0 ) -> ( A RiseFac 0 ) = prod_ k e. ( 0 ... ( 0 - 1 ) ) ( A + k ) )
3 1 2 mpan2 
 |-  ( A e. CC -> ( A RiseFac 0 ) = prod_ k e. ( 0 ... ( 0 - 1 ) ) ( A + k ) )
4 risefall0lem 
 |-  ( 0 ... ( 0 - 1 ) ) = (/)
5 4 prodeq1i 
 |-  prod_ k e. ( 0 ... ( 0 - 1 ) ) ( A + k ) = prod_ k e. (/) ( A + k )
6 prod0 
 |-  prod_ k e. (/) ( A + k ) = 1
7 5 6 eqtri 
 |-  prod_ k e. ( 0 ... ( 0 - 1 ) ) ( A + k ) = 1
8 3 7 eqtrdi 
 |-  ( A e. CC -> ( A RiseFac 0 ) = 1 )