Metamath Proof Explorer

Theorem fallfacval4

Description: Represent the falling factorial via factorials when the first argument is a natural. (Contributed by Scott Fenton, 20-Mar-2018)

Ref Expression
Assertion fallfacval4 
|- ( N e. ( 0 ... A ) -> ( A FallFac N ) = ( ( ! ` A ) / ( ! ` ( A - N ) ) ) )

Proof

Step Hyp Ref Expression
1 fzfid 
 |-  ( N e. ( 0 ... A ) -> ( ( ( A - N ) + 1 ) ... A ) e. Fin )
2 elfzelz 
 |-  ( k e. ( ( ( A - N ) + 1 ) ... A ) -> k e. ZZ )
3 2 zcnd 
 |-  ( k e. ( ( ( A - N ) + 1 ) ... A ) -> k e. CC )
4 3 adantl 
 |-  ( ( N e. ( 0 ... A ) /\ k e. ( ( ( A - N ) + 1 ) ... A ) ) -> k e. CC )
5 1 4 fprodcl 
 |-  ( N e. ( 0 ... A ) -> prod_ k e. ( ( ( A - N ) + 1 ) ... A ) k e. CC )
6 fzfid 
 |-  ( N e. ( 0 ... A ) -> ( 1 ... ( A - N ) ) e. Fin )
7 elfznn 
 |-  ( k e. ( 1 ... ( A - N ) ) -> k e. NN )
8 7 adantl 
 |-  ( ( N e. ( 0 ... A ) /\ k e. ( 1 ... ( A - N ) ) ) -> k e. NN )
9 8 nncnd 
 |-  ( ( N e. ( 0 ... A ) /\ k e. ( 1 ... ( A - N ) ) ) -> k e. CC )
10 6 9 fprodcl 
 |-  ( N e. ( 0 ... A ) -> prod_ k e. ( 1 ... ( A - N ) ) k e. CC )
11 8 nnne0d 
 |-  ( ( N e. ( 0 ... A ) /\ k e. ( 1 ... ( A - N ) ) ) -> k =/= 0 )
12 6 9 11 fprodn0 
 |-  ( N e. ( 0 ... A ) -> prod_ k e. ( 1 ... ( A - N ) ) k =/= 0 )
13 5 10 12 divcan3d 
 |-  ( N e. ( 0 ... A ) -> ( ( prod_ k e. ( 1 ... ( A - N ) ) k x. prod_ k e. ( ( ( A - N ) + 1 ) ... A ) k ) / prod_ k e. ( 1 ... ( A - N ) ) k ) = prod_ k e. ( ( ( A - N ) + 1 ) ... A ) k )
14 fznn0sub 
 |-  ( N e. ( 0 ... A ) -> ( A - N ) e. NN0 )
15 14 nn0red 
 |-  ( N e. ( 0 ... A ) -> ( A - N ) e. RR )
16 15 ltp1d 
 |-  ( N e. ( 0 ... A ) -> ( A - N ) < ( ( A - N ) + 1 ) )
17 fzdisj 
 |-  ( ( A - N ) < ( ( A - N ) + 1 ) -> ( ( 1 ... ( A - N ) ) i^i ( ( ( A - N ) + 1 ) ... A ) ) = (/) )
18 16 17 syl 
 |-  ( N e. ( 0 ... A ) -> ( ( 1 ... ( A - N ) ) i^i ( ( ( A - N ) + 1 ) ... A ) ) = (/) )
19 nn0p1nn 
 |-  ( ( A - N ) e. NN0 -> ( ( A - N ) + 1 ) e. NN )
20 14 19 syl 
 |-  ( N e. ( 0 ... A ) -> ( ( A - N ) + 1 ) e. NN )
21 nnuz 
 |-  NN = ( ZZ>= ` 1 )
22 20 21 eleqtrdi 
 |-  ( N e. ( 0 ... A ) -> ( ( A - N ) + 1 ) e. ( ZZ>= ` 1 ) )
23 14 nn0zd 
 |-  ( N e. ( 0 ... A ) -> ( A - N ) e. ZZ )
24 elfzel2 
 |-  ( N e. ( 0 ... A ) -> A e. ZZ )
25 elfzle1 
 |-  ( N e. ( 0 ... A ) -> 0 <_ N )
26 24 zred 
 |-  ( N e. ( 0 ... A ) -> A e. RR )
27 elfzelz 
 |-  ( N e. ( 0 ... A ) -> N e. ZZ )
28 27 zred 
 |-  ( N e. ( 0 ... A ) -> N e. RR )
29 26 28 subge02d 
 |-  ( N e. ( 0 ... A ) -> ( 0 <_ N <-> ( A - N ) <_ A ) )
30 25 29 mpbid 
 |-  ( N e. ( 0 ... A ) -> ( A - N ) <_ A )
31 eluz2 
 |-  ( A e. ( ZZ>= ` ( A - N ) ) <-> ( ( A - N ) e. ZZ /\ A e. ZZ /\ ( A - N ) <_ A ) )
32 23 24 30 31 syl3anbrc 
 |-  ( N e. ( 0 ... A ) -> A e. ( ZZ>= ` ( A - N ) ) )
33 fzsplit2 
 |-  ( ( ( ( A - N ) + 1 ) e. ( ZZ>= ` 1 ) /\ A e. ( ZZ>= ` ( A - N ) ) ) -> ( 1 ... A ) = ( ( 1 ... ( A - N ) ) u. ( ( ( A - N ) + 1 ) ... A ) ) )
34 22 32 33 syl2anc 
 |-  ( N e. ( 0 ... A ) -> ( 1 ... A ) = ( ( 1 ... ( A - N ) ) u. ( ( ( A - N ) + 1 ) ... A ) ) )
35 fzfid 
 |-  ( N e. ( 0 ... A ) -> ( 1 ... A ) e. Fin )
36 elfznn 
 |-  ( k e. ( 1 ... A ) -> k e. NN )
37 36 nncnd 
 |-  ( k e. ( 1 ... A ) -> k e. CC )
38 37 adantl 
 |-  ( ( N e. ( 0 ... A ) /\ k e. ( 1 ... A ) ) -> k e. CC )
39 18 34 35 38 fprodsplit 
 |-  ( N e. ( 0 ... A ) -> prod_ k e. ( 1 ... A ) k = ( prod_ k e. ( 1 ... ( A - N ) ) k x. prod_ k e. ( ( ( A - N ) + 1 ) ... A ) k ) )
40 39 oveq1d 
 |-  ( N e. ( 0 ... A ) -> ( prod_ k e. ( 1 ... A ) k / prod_ k e. ( 1 ... ( A - N ) ) k ) = ( ( prod_ k e. ( 1 ... ( A - N ) ) k x. prod_ k e. ( ( ( A - N ) + 1 ) ... A ) k ) / prod_ k e. ( 1 ... ( A - N ) ) k ) )
41 24 zcnd 
 |-  ( N e. ( 0 ... A ) -> A e. CC )
42 27 zcnd 
 |-  ( N e. ( 0 ... A ) -> N e. CC )
43 1cnd 
 |-  ( N e. ( 0 ... A ) -> 1 e. CC )
44 41 42 43 subsubd 
 |-  ( N e. ( 0 ... A ) -> ( A - ( N - 1 ) ) = ( ( A - N ) + 1 ) )
45 44 oveq1d 
 |-  ( N e. ( 0 ... A ) -> ( ( A - ( N - 1 ) ) ... A ) = ( ( ( A - N ) + 1 ) ... A ) )
46 45 prodeq1d 
 |-  ( N e. ( 0 ... A ) -> prod_ k e. ( ( A - ( N - 1 ) ) ... A ) k = prod_ k e. ( ( ( A - N ) + 1 ) ... A ) k )
47 13 40 46 3eqtr4rd 
 |-  ( N e. ( 0 ... A ) -> prod_ k e. ( ( A - ( N - 1 ) ) ... A ) k = ( prod_ k e. ( 1 ... A ) k / prod_ k e. ( 1 ... ( A - N ) ) k ) )
48 fallfacval3 
 |-  ( N e. ( 0 ... A ) -> ( A FallFac N ) = prod_ k e. ( ( A - ( N - 1 ) ) ... A ) k )
49 elfz3nn0 
 |-  ( N e. ( 0 ... A ) -> A e. NN0 )
50 fprodfac 
 |-  ( A e. NN0 -> ( ! ` A ) = prod_ k e. ( 1 ... A ) k )
51 49 50 syl 
 |-  ( N e. ( 0 ... A ) -> ( ! ` A ) = prod_ k e. ( 1 ... A ) k )
52 fprodfac 
 |-  ( ( A - N ) e. NN0 -> ( ! ` ( A - N ) ) = prod_ k e. ( 1 ... ( A - N ) ) k )
53 14 52 syl 
 |-  ( N e. ( 0 ... A ) -> ( ! ` ( A - N ) ) = prod_ k e. ( 1 ... ( A - N ) ) k )
54 51 53 oveq12d 
 |-  ( N e. ( 0 ... A ) -> ( ( ! ` A ) / ( ! ` ( A - N ) ) ) = ( prod_ k e. ( 1 ... A ) k / prod_ k e. ( 1 ... ( A - N ) ) k ) )
55 47 48 54 3eqtr4d 
 |-  ( N e. ( 0 ... A ) -> ( A FallFac N ) = ( ( ! ` A ) / ( ! ` ( A - N ) ) ) )