Metamath Proof Explorer

Theorem fallfacval2

Description: One-based value of falling factorial. (Contributed by Scott Fenton, 15-Jan-2018)

Ref Expression
Assertion fallfacval2 
|- ( ( A e. CC /\ N e. NN0 ) -> ( A FallFac N ) = prod_ k e. ( 1 ... N ) ( A - ( k - 1 ) ) )

Proof

Step Hyp Ref Expression
1 fallfacval 
 |-  ( ( A e. CC /\ N e. NN0 ) -> ( A FallFac N ) = prod_ n e. ( 0 ... ( N - 1 ) ) ( A - n ) )
2 1zzd 
 |-  ( ( A e. CC /\ N e. NN0 ) -> 1 e. ZZ )
3 0zd 
 |-  ( ( A e. CC /\ N e. NN0 ) -> 0 e. ZZ )
4 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
5 peano2zm 
 |-  ( N e. ZZ -> ( N - 1 ) e. ZZ )
6 4 5 syl 
 |-  ( N e. NN0 -> ( N - 1 ) e. ZZ )
7 6 adantl 
 |-  ( ( A e. CC /\ N e. NN0 ) -> ( N - 1 ) e. ZZ )
8 simpl 
 |-  ( ( A e. CC /\ N e. NN0 ) -> A e. CC )
9 elfznn0 
 |-  ( n e. ( 0 ... ( N - 1 ) ) -> n e. NN0 )
10 9 nn0cnd 
 |-  ( n e. ( 0 ... ( N - 1 ) ) -> n e. CC )
11 subcl 
 |-  ( ( A e. CC /\ n e. CC ) -> ( A - n ) e. CC )
12 8 10 11 syl2an 
 |-  ( ( ( A e. CC /\ N e. NN0 ) /\ n e. ( 0 ... ( N - 1 ) ) ) -> ( A - n ) e. CC )
13 oveq2 
 |-  ( n = ( k - 1 ) -> ( A - n ) = ( A - ( k - 1 ) ) )
14 2 3 7 12 13 fprodshft 
 |-  ( ( A e. CC /\ N e. NN0 ) -> prod_ n e. ( 0 ... ( N - 1 ) ) ( A - n ) = prod_ k e. ( ( 0 + 1 ) ... ( ( N - 1 ) + 1 ) ) ( A - ( k - 1 ) ) )
15 0p1e1 
 |-  ( 0 + 1 ) = 1
16 15 a1i 
 |-  ( ( A e. CC /\ N e. NN0 ) -> ( 0 + 1 ) = 1 )
17 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
18 1cnd 
 |-  ( N e. NN0 -> 1 e. CC )
19 17 18 npcand 
 |-  ( N e. NN0 -> ( ( N - 1 ) + 1 ) = N )
20 19 adantl 
 |-  ( ( A e. CC /\ N e. NN0 ) -> ( ( N - 1 ) + 1 ) = N )
21 16 20 oveq12d 
 |-  ( ( A e. CC /\ N e. NN0 ) -> ( ( 0 + 1 ) ... ( ( N - 1 ) + 1 ) ) = ( 1 ... N ) )
22 21 prodeq1d 
 |-  ( ( A e. CC /\ N e. NN0 ) -> prod_ k e. ( ( 0 + 1 ) ... ( ( N - 1 ) + 1 ) ) ( A - ( k - 1 ) ) = prod_ k e. ( 1 ... N ) ( A - ( k - 1 ) ) )
23 1 14 22 3eqtrd 
 |-  ( ( A e. CC /\ N e. NN0 ) -> ( A FallFac N ) = prod_ k e. ( 1 ... N ) ( A - ( k - 1 ) ) )