Metamath Proof Explorer


Theorem risefallfac

Description: A relationship between rising and falling factorials. (Contributed by Scott Fenton, 15-Jan-2018)

Ref Expression
Assertion risefallfac X N 0 X N = 1 N X N _

Proof

Step Hyp Ref Expression
1 negcl X X
2 1 adantr X N 0 X
3 elfznn k 1 N k
4 nnm1nn0 k k 1 0
5 3 4 syl k 1 N k 1 0
6 5 nn0cnd k 1 N k 1
7 subcl X k 1 - X - k 1
8 2 6 7 syl2an X N 0 k 1 N - X - k 1
9 8 mulm1d X N 0 k 1 N -1 - X - k 1 = - X - k 1
10 simpll X N 0 k 1 N X
11 6 adantl X N 0 k 1 N k 1
12 10 11 negdi2d X N 0 k 1 N X + k - 1 = - X - k 1
13 12 negeqd X N 0 k 1 N X + k - 1 = - X - k 1
14 simpl X N 0 X
15 addcl X k 1 X + k - 1
16 14 6 15 syl2an X N 0 k 1 N X + k - 1
17 16 negnegd X N 0 k 1 N X + k - 1 = X + k - 1
18 9 13 17 3eqtr2rd X N 0 k 1 N X + k - 1 = -1 - X - k 1
19 18 prodeq2dv X N 0 k = 1 N X + k - 1 = k = 1 N -1 - X - k 1
20 risefacval2 X N 0 X N = k = 1 N X + k - 1
21 fzfi 1 N Fin
22 neg1cn 1
23 fprodconst 1 N Fin 1 k = 1 N -1 = 1 1 N
24 21 22 23 mp2an k = 1 N -1 = 1 1 N
25 hashfz1 N 0 1 N = N
26 25 oveq2d N 0 1 1 N = 1 N
27 24 26 eqtr2id N 0 1 N = k = 1 N -1
28 27 adantl X N 0 1 N = k = 1 N -1
29 fallfacval2 X N 0 X N _ = k = 1 N - X - k 1
30 1 29 sylan X N 0 X N _ = k = 1 N - X - k 1
31 28 30 oveq12d X N 0 1 N X N _ = k = 1 N -1 k = 1 N - X - k 1
32 fzfid X N 0 1 N Fin
33 22 a1i X N 0 k 1 N 1
34 32 33 8 fprodmul X N 0 k = 1 N -1 - X - k 1 = k = 1 N -1 k = 1 N - X - k 1
35 31 34 eqtr4d X N 0 1 N X N _ = k = 1 N -1 - X - k 1
36 19 20 35 3eqtr4d X N 0 X N = 1 N X N _