Metamath Proof Explorer

Theorem 0risefac

Description: The value of the zero rising factorial at natural N . (Contributed by Scott Fenton, 17-Feb-2018)

Ref Expression
Assertion 0risefac 
|- ( N e. NN -> ( 0 RiseFac N ) = 0 )

Proof

Step Hyp Ref Expression
1 0cn 
 |-  0 e. CC
2 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
3 risefallfac 
 |-  ( ( 0 e. CC /\ N e. NN0 ) -> ( 0 RiseFac N ) = ( ( -u 1 ^ N ) x. ( -u 0 FallFac N ) ) )
4 1 2 3 sylancr 
 |-  ( N e. NN -> ( 0 RiseFac N ) = ( ( -u 1 ^ N ) x. ( -u 0 FallFac N ) ) )
5 neg0 
 |-  -u 0 = 0
6 5 oveq1i 
 |-  ( -u 0 FallFac N ) = ( 0 FallFac N )
7 0fallfac 
 |-  ( N e. NN -> ( 0 FallFac N ) = 0 )
8 6 7 eqtrid 
 |-  ( N e. NN -> ( -u 0 FallFac N ) = 0 )
9 8 oveq2d 
 |-  ( N e. NN -> ( ( -u 1 ^ N ) x. ( -u 0 FallFac N ) ) = ( ( -u 1 ^ N ) x. 0 ) )
10 neg1cn 
 |-  -u 1 e. CC
11 expcl 
 |-  ( ( -u 1 e. CC /\ N e. NN0 ) -> ( -u 1 ^ N ) e. CC )
12 10 2 11 sylancr 
 |-  ( N e. NN -> ( -u 1 ^ N ) e. CC )
13 12 mul01d 
 |-  ( N e. NN -> ( ( -u 1 ^ N ) x. 0 ) = 0 )
14 4 9 13 3eqtrd 
 |-  ( N e. NN -> ( 0 RiseFac N ) = 0 )