This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )