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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fzfid | |
|
2 | elfzelz | |
|
3 | 2 | zcnd | |
4 | 3 | adantl | |
5 | 1 4 | fprodcl | |
6 | fzfid | |
|
7 | elfznn | |
|
8 | 7 | adantl | |
9 | 8 | nncnd | |
10 | 6 9 | fprodcl | |
11 | 8 | nnne0d | |
12 | 6 9 11 | fprodn0 | |
13 | 5 10 12 | divcan3d | |
14 | fznn0sub | |
|
15 | 14 | nn0red | |
16 | 15 | ltp1d | |
17 | fzdisj | |
|
18 | 16 17 | syl | |
19 | nn0p1nn | |
|
20 | 14 19 | syl | |
21 | nnuz | |
|
22 | 20 21 | eleqtrdi | |
23 | 14 | nn0zd | |
24 | elfzel2 | |
|
25 | elfzle1 | |
|
26 | 24 | zred | |
27 | elfzelz | |
|
28 | 27 | zred | |
29 | 26 28 | subge02d | |
30 | 25 29 | mpbid | |
31 | eluz2 | |
|
32 | 23 24 30 31 | syl3anbrc | |
33 | fzsplit2 | |
|
34 | 22 32 33 | syl2anc | |
35 | fzfid | |
|
36 | elfznn | |
|
37 | 36 | nncnd | |
38 | 37 | adantl | |
39 | 18 34 35 38 | fprodsplit | |
40 | 39 | oveq1d | |
41 | 24 | zcnd | |
42 | 27 | zcnd | |
43 | 1cnd | |
|
44 | 41 42 43 | subsubd | |
45 | 44 | oveq1d | |
46 | 45 | prodeq1d | |
47 | 13 40 46 | 3eqtr4rd | |
48 | fallfacval3 | |
|
49 | elfz3nn0 | |
|
50 | fprodfac | |
|
51 | 49 50 | syl | |
52 | fprodfac | |
|
53 | 14 52 | syl | |
54 | 51 53 | oveq12d | |
55 | 47 48 54 | 3eqtr4d | |