Metamath Proof Explorer


Theorem fallfacval3

Description: A product representation of falling factorial when A is a nonnegative integer. (Contributed by Scott Fenton, 20-Mar-2018)

Ref Expression
Assertion fallfacval3
|- ( N e. ( 0 ... A ) -> ( A FallFac N ) = prod_ k e. ( ( A - ( N - 1 ) ) ... A ) k )

Proof

Step Hyp Ref Expression
1 elfz3nn0
 |-  ( N e. ( 0 ... A ) -> A e. NN0 )
2 1 nn0cnd
 |-  ( N e. ( 0 ... A ) -> A e. CC )
3 elfznn0
 |-  ( N e. ( 0 ... A ) -> N e. NN0 )
4 fallfacval
 |-  ( ( A e. CC /\ N e. NN0 ) -> ( A FallFac N ) = prod_ j e. ( 0 ... ( N - 1 ) ) ( A - j ) )
5 2 3 4 syl2anc
 |-  ( N e. ( 0 ... A ) -> ( A FallFac N ) = prod_ j e. ( 0 ... ( N - 1 ) ) ( A - j ) )
6 elfzel2
 |-  ( N e. ( 0 ... A ) -> A e. ZZ )
7 elfzel1
 |-  ( N e. ( 0 ... A ) -> 0 e. ZZ )
8 elfzelz
 |-  ( N e. ( 0 ... A ) -> N e. ZZ )
9 peano2zm
 |-  ( N e. ZZ -> ( N - 1 ) e. ZZ )
10 8 9 syl
 |-  ( N e. ( 0 ... A ) -> ( N - 1 ) e. ZZ )
11 elfzelz
 |-  ( j e. ( 0 ... ( N - 1 ) ) -> j e. ZZ )
12 11 zcnd
 |-  ( j e. ( 0 ... ( N - 1 ) ) -> j e. CC )
13 subcl
 |-  ( ( A e. CC /\ j e. CC ) -> ( A - j ) e. CC )
14 2 12 13 syl2an
 |-  ( ( N e. ( 0 ... A ) /\ j e. ( 0 ... ( N - 1 ) ) ) -> ( A - j ) e. CC )
15 oveq2
 |-  ( j = ( A - k ) -> ( A - j ) = ( A - ( A - k ) ) )
16 6 7 10 14 15 fprodrev
 |-  ( N e. ( 0 ... A ) -> prod_ j e. ( 0 ... ( N - 1 ) ) ( A - j ) = prod_ k e. ( ( A - ( N - 1 ) ) ... ( A - 0 ) ) ( A - ( A - k ) ) )
17 2 subid1d
 |-  ( N e. ( 0 ... A ) -> ( A - 0 ) = A )
18 17 oveq2d
 |-  ( N e. ( 0 ... A ) -> ( ( A - ( N - 1 ) ) ... ( A - 0 ) ) = ( ( A - ( N - 1 ) ) ... A ) )
19 2 adantr
 |-  ( ( N e. ( 0 ... A ) /\ k e. ( ( A - ( N - 1 ) ) ... ( A - 0 ) ) ) -> A e. CC )
20 elfzelz
 |-  ( k e. ( ( A - ( N - 1 ) ) ... ( A - 0 ) ) -> k e. ZZ )
21 20 zcnd
 |-  ( k e. ( ( A - ( N - 1 ) ) ... ( A - 0 ) ) -> k e. CC )
22 21 adantl
 |-  ( ( N e. ( 0 ... A ) /\ k e. ( ( A - ( N - 1 ) ) ... ( A - 0 ) ) ) -> k e. CC )
23 19 22 nncand
 |-  ( ( N e. ( 0 ... A ) /\ k e. ( ( A - ( N - 1 ) ) ... ( A - 0 ) ) ) -> ( A - ( A - k ) ) = k )
24 18 23 prodeq12dv
 |-  ( N e. ( 0 ... A ) -> prod_ k e. ( ( A - ( N - 1 ) ) ... ( A - 0 ) ) ( A - ( A - k ) ) = prod_ k e. ( ( A - ( N - 1 ) ) ... A ) k )
25 5 16 24 3eqtrd
 |-  ( N e. ( 0 ... A ) -> ( A FallFac N ) = prod_ k e. ( ( A - ( N - 1 ) ) ... A ) k )