Metamath Proof Explorer


Theorem fallfacval2

Description: One-based value of falling factorial. (Contributed by Scott Fenton, 15-Jan-2018)

Ref Expression
Assertion fallfacval2 A N 0 A N _ = k = 1 N A k 1

Proof

Step Hyp Ref Expression
1 fallfacval A N 0 A N _ = n = 0 N 1 A n
2 1zzd A N 0 1
3 0zd A N 0 0
4 nn0z N 0 N
5 peano2zm N N 1
6 4 5 syl N 0 N 1
7 6 adantl A N 0 N 1
8 simpl A N 0 A
9 elfznn0 n 0 N 1 n 0
10 9 nn0cnd n 0 N 1 n
11 subcl A n A n
12 8 10 11 syl2an A N 0 n 0 N 1 A n
13 oveq2 n = k 1 A n = A k 1
14 2 3 7 12 13 fprodshft A N 0 n = 0 N 1 A n = k = 0 + 1 N - 1 + 1 A k 1
15 0p1e1 0 + 1 = 1
16 15 a1i A N 0 0 + 1 = 1
17 nn0cn N 0 N
18 1cnd N 0 1
19 17 18 npcand N 0 N - 1 + 1 = N
20 19 adantl A N 0 N - 1 + 1 = N
21 16 20 oveq12d A N 0 0 + 1 N - 1 + 1 = 1 N
22 21 prodeq1d A N 0 k = 0 + 1 N - 1 + 1 A k 1 = k = 1 N A k 1
23 1 14 22 3eqtrd A N 0 A N _ = k = 1 N A k 1