Metamath Proof Explorer

Theorem 0fallfac

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

Ref Expression
Assertion 0fallfac 
|- ( N e. NN -> ( 0 FallFac N ) = 0 )

Proof

Step Hyp Ref Expression
1 0cn 
 |-  0 e. CC
2 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
3 fallfacval 
 |-  ( ( 0 e. CC /\ N e. NN0 ) -> ( 0 FallFac N ) = prod_ k e. ( 0 ... ( N - 1 ) ) ( 0 - k ) )
4 1 2 3 sylancr 
 |-  ( N e. NN -> ( 0 FallFac N ) = prod_ k e. ( 0 ... ( N - 1 ) ) ( 0 - k ) )
5 nnm1nn0 
 |-  ( N e. NN -> ( N - 1 ) e. NN0 )
6 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
7 5 6 eleqtrdi 
 |-  ( N e. NN -> ( N - 1 ) e. ( ZZ>= ` 0 ) )
8 elfzelz 
 |-  ( k e. ( 0 ... ( N - 1 ) ) -> k e. ZZ )
9 8 zcnd 
 |-  ( k e. ( 0 ... ( N - 1 ) ) -> k e. CC )
10 subcl 
 |-  ( ( 0 e. CC /\ k e. CC ) -> ( 0 - k ) e. CC )
11 1 9 10 sylancr 
 |-  ( k e. ( 0 ... ( N - 1 ) ) -> ( 0 - k ) e. CC )
12 11 adantl 
 |-  ( ( N e. NN /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( 0 - k ) e. CC )
13 oveq2 
 |-  ( k = 0 -> ( 0 - k ) = ( 0 - 0 ) )
14 0m0e0 
 |-  ( 0 - 0 ) = 0
15 13 14 eqtrdi 
 |-  ( k = 0 -> ( 0 - k ) = 0 )
16 7 12 15 fprod1p 
 |-  ( N e. NN -> prod_ k e. ( 0 ... ( N - 1 ) ) ( 0 - k ) = ( 0 x. prod_ k e. ( ( 0 + 1 ) ... ( N - 1 ) ) ( 0 - k ) ) )
17 fzfid 
 |-  ( N e. NN -> ( ( 0 + 1 ) ... ( N - 1 ) ) e. Fin )
18 elfzelz 
 |-  ( k e. ( ( 0 + 1 ) ... ( N - 1 ) ) -> k e. ZZ )
19 18 zcnd 
 |-  ( k e. ( ( 0 + 1 ) ... ( N - 1 ) ) -> k e. CC )
20 1 19 10 sylancr 
 |-  ( k e. ( ( 0 + 1 ) ... ( N - 1 ) ) -> ( 0 - k ) e. CC )
21 20 adantl 
 |-  ( ( N e. NN /\ k e. ( ( 0 + 1 ) ... ( N - 1 ) ) ) -> ( 0 - k ) e. CC )
22 17 21 fprodcl 
 |-  ( N e. NN -> prod_ k e. ( ( 0 + 1 ) ... ( N - 1 ) ) ( 0 - k ) e. CC )
23 22 mul02d 
 |-  ( N e. NN -> ( 0 x. prod_ k e. ( ( 0 + 1 ) ... ( N - 1 ) ) ( 0 - k ) ) = 0 )
24 4 16 23 3eqtrd 
 |-  ( N e. NN -> ( 0 FallFac N ) = 0 )