Metamath Proof Explorer


Theorem fallfacfwd

Description: The forward difference of a falling factorial. (Contributed by Scott Fenton, 21-Jan-2018)

Ref Expression
Assertion fallfacfwd A N A + 1 N _ A N _ = N A N 1 _

Proof

Step Hyp Ref Expression
1 peano2cn A A + 1
2 nnnn0 N N 0
3 fallfacval A + 1 N 0 A + 1 N _ = k = 0 N 1 A + 1 - k
4 1 2 3 syl2an A N A + 1 N _ = k = 0 N 1 A + 1 - k
5 0p1e1 0 + 1 = 1
6 5 oveq1i 0 + 1 N 1 = 1 N 1
7 6 prodeq1i k = 0 + 1 N 1 A k 1 = k = 1 N 1 A k 1
8 7 oveq2i A -1 k = 0 + 1 N 1 A k 1 = A -1 k = 1 N 1 A k 1
9 nnm1nn0 N N 1 0
10 9 adantl A N N 1 0
11 nn0uz 0 = 0
12 10 11 eleqtrdi A N N 1 0
13 simpll A N k 0 N 1 A
14 elfzelz k 0 N 1 k
15 14 adantl A N k 0 N 1 k
16 peano2zm k k 1
17 15 16 syl A N k 0 N 1 k 1
18 17 zcnd A N k 0 N 1 k 1
19 13 18 subcld A N k 0 N 1 A k 1
20 oveq1 k = 0 k 1 = 0 1
21 df-neg 1 = 0 1
22 20 21 eqtr4di k = 0 k 1 = 1
23 22 oveq2d k = 0 A k 1 = A -1
24 12 19 23 fprod1p A N k = 0 N 1 A k 1 = A -1 k = 0 + 1 N 1 A k 1
25 fallfacval2 A N 1 0 A N 1 _ = k = 1 N 1 A k 1
26 9 25 sylan2 A N A N 1 _ = k = 1 N 1 A k 1
27 26 oveq2d A N A -1 A N 1 _ = A -1 k = 1 N 1 A k 1
28 8 24 27 3eqtr4a A N k = 0 N 1 A k 1 = A -1 A N 1 _
29 elfznn0 k 0 N 1 k 0
30 29 adantl A N k 0 N 1 k 0
31 30 nn0cnd A N k 0 N 1 k
32 1cnd A N k 0 N 1 1
33 13 31 32 subsub3d A N k 0 N 1 A k 1 = A + 1 - k
34 33 prodeq2dv A N k = 0 N 1 A k 1 = k = 0 N 1 A + 1 - k
35 simpl A N A
36 1cnd A N 1
37 35 36 subnegd A N A -1 = A + 1
38 37 oveq1d A N A -1 A N 1 _ = A + 1 A N 1 _
39 28 34 38 3eqtr3d A N k = 0 N 1 A + 1 - k = A + 1 A N 1 _
40 4 39 eqtrd A N A + 1 N _ = A + 1 A N 1 _
41 simpr A N N
42 41 nncnd A N N
43 42 36 npcand A N N - 1 + 1 = N
44 43 oveq2d A N A N - 1 + 1 _ = A N _
45 fallfacp1 A N 1 0 A N - 1 + 1 _ = A N 1 _ A N 1
46 9 45 sylan2 A N A N - 1 + 1 _ = A N 1 _ A N 1
47 44 46 eqtr3d A N A N _ = A N 1 _ A N 1
48 40 47 oveq12d A N A + 1 N _ A N _ = A + 1 A N 1 _ A N 1 _ A N 1
49 fallfaccl A N 1 0 A N 1 _
50 9 49 sylan2 A N A N 1 _
51 10 nn0cnd A N N 1
52 35 51 subcld A N A N 1
53 50 52 mulcomd A N A N 1 _ A N 1 = A N 1 A N 1 _
54 53 oveq2d A N A + 1 A N 1 _ A N 1 _ A N 1 = A + 1 A N 1 _ A N 1 A N 1 _
55 1 adantr A N A + 1
56 55 52 50 subdird A N A + 1 - A N 1 A N 1 _ = A + 1 A N 1 _ A N 1 A N 1 _
57 35 36 51 pnncand A N A + 1 - A N 1 = 1 + N - 1
58 36 42 pncan3d A N 1 + N - 1 = N
59 57 58 eqtrd A N A + 1 - A N 1 = N
60 59 oveq1d A N A + 1 - A N 1 A N 1 _ = N A N 1 _
61 54 56 60 3eqtr2d A N A + 1 A N 1 _ A N 1 _ A N 1 = N A N 1 _
62 48 61 eqtrd A N A + 1 N _ A N _ = N A N 1 _