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 N0AAN_=A!AN!

Proof

Step Hyp Ref Expression
1 fzfid N0AA-N+1AFin
2 elfzelz kA-N+1Ak
3 2 zcnd kA-N+1Ak
4 3 adantl N0AkA-N+1Ak
5 1 4 fprodcl N0Ak=A-N+1Ak
6 fzfid N0A1ANFin
7 elfznn k1ANk
8 7 adantl N0Ak1ANk
9 8 nncnd N0Ak1ANk
10 6 9 fprodcl N0Ak=1ANk
11 8 nnne0d N0Ak1ANk0
12 6 9 11 fprodn0 N0Ak=1ANk0
13 5 10 12 divcan3d N0Ak=1ANkk=A-N+1Akk=1ANk=k=A-N+1Ak
14 fznn0sub N0AAN0
15 14 nn0red N0AAN
16 15 ltp1d N0AAN<A-N+1
17 fzdisj AN<A-N+11ANA-N+1A=
18 16 17 syl N0A1ANA-N+1A=
19 nn0p1nn AN0A-N+1
20 14 19 syl N0AA-N+1
21 nnuz =1
22 20 21 eleqtrdi N0AA-N+11
23 14 nn0zd N0AAN
24 elfzel2 N0AA
25 elfzle1 N0A0N
26 24 zred N0AA
27 elfzelz N0AN
28 27 zred N0AN
29 26 28 subge02d N0A0NANA
30 25 29 mpbid N0AANA
31 eluz2 AANANAANA
32 23 24 30 31 syl3anbrc N0AAAN
33 fzsplit2 A-N+11AAN1A=1ANA-N+1A
34 22 32 33 syl2anc N0A1A=1ANA-N+1A
35 fzfid N0A1AFin
36 elfznn k1Ak
37 36 nncnd k1Ak
38 37 adantl N0Ak1Ak
39 18 34 35 38 fprodsplit N0Ak=1Ak=k=1ANkk=A-N+1Ak
40 39 oveq1d N0Ak=1Akk=1ANk=k=1ANkk=A-N+1Akk=1ANk
41 24 zcnd N0AA
42 27 zcnd N0AN
43 1cnd N0A1
44 41 42 43 subsubd N0AAN1=A-N+1
45 44 oveq1d N0AAN1A=A-N+1A
46 45 prodeq1d N0Ak=AN1Ak=k=A-N+1Ak
47 13 40 46 3eqtr4rd N0Ak=AN1Ak=k=1Akk=1ANk
48 fallfacval3 N0AAN_=k=AN1Ak
49 elfz3nn0 N0AA0
50 fprodfac A0A!=k=1Ak
51 49 50 syl N0AA!=k=1Ak
52 fprodfac AN0AN!=k=1ANk
53 14 52 syl N0AAN!=k=1ANk
54 51 53 oveq12d N0AA!AN!=k=1Akk=1ANk
55 47 48 54 3eqtr4d N0AAN_=A!AN!