Metamath Proof Explorer

Theorem risefacfac

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

Ref Expression
Assertion risefacfac 
|- ( N e. NN0 -> ( 1 RiseFac N ) = ( ! ` N ) )

Proof

Step Hyp Ref Expression
1 1cnd 
 |-  ( ( N e. NN0 /\ k e. ( 1 ... N ) ) -> 1 e. CC )
2 elfznn 
 |-  ( k e. ( 1 ... N ) -> k e. NN )
3 2 nncnd 
 |-  ( k e. ( 1 ... N ) -> k e. CC )
4 3 adantl 
 |-  ( ( N e. NN0 /\ k e. ( 1 ... N ) ) -> k e. CC )
5 1 4 pncan3d 
 |-  ( ( N e. NN0 /\ k e. ( 1 ... N ) ) -> ( 1 + ( k - 1 ) ) = k )
6 5 prodeq2dv 
 |-  ( N e. NN0 -> prod_ k e. ( 1 ... N ) ( 1 + ( k - 1 ) ) = prod_ k e. ( 1 ... N ) k )
7 ax-1cn 
 |-  1 e. CC
8 risefacval2 
 |-  ( ( 1 e. CC /\ N e. NN0 ) -> ( 1 RiseFac N ) = prod_ k e. ( 1 ... N ) ( 1 + ( k - 1 ) ) )
9 7 8 mpan 
 |-  ( N e. NN0 -> ( 1 RiseFac N ) = prod_ k e. ( 1 ... N ) ( 1 + ( k - 1 ) ) )
10 fprodfac 
 |-  ( N e. NN0 -> ( ! ` N ) = prod_ k e. ( 1 ... N ) k )
11 6 9 10 3eqtr4d 
 |-  ( N e. NN0 -> ( 1 RiseFac N ) = ( ! ` N ) )