Metamath Proof Explorer

Theorem fallfacval3

Description: A product representation of falling factorial when A is a nonnegative integer. (Contributed by Scott Fenton, 20-Mar-2018)

Ref Expression
Assertion fallfacval3 ⊢ N ∈ 0 … A → A N _ = ∏ k = A − N − 1 A k

Proof

Step Hyp Ref Expression
1 elfz3nn0 ⊢ N ∈ 0 … A → A ∈ ℕ 0
2 1 nn0cnd ⊢ N ∈ 0 … A → A ∈ ℂ
3 elfznn0 ⊢ N ∈ 0 … A → N ∈ ℕ 0
4 fallfacval ⊢ A ∈ ℂ ∧ N ∈ ℕ 0 → A N _ = ∏ j = 0 N − 1 A − j
5 2 3 4 syl2anc ⊢ N ∈ 0 … A → A N _ = ∏ j = 0 N − 1 A − j
6 elfzel2 ⊢ N ∈ 0 … A → A ∈ ℤ
7 elfzel1 ⊢ N ∈ 0 … A → 0 ∈ ℤ
8 elfzelz ⊢ N ∈ 0 … A → N ∈ ℤ
9 peano2zm ⊢ N ∈ ℤ → N − 1 ∈ ℤ
10 8 9 syl ⊢ N ∈ 0 … A → N − 1 ∈ ℤ
11 elfzelz ⊢ j ∈ 0 … N − 1 → j ∈ ℤ
12 11 zcnd ⊢ j ∈ 0 … N − 1 → j ∈ ℂ
13 subcl ⊢ A ∈ ℂ ∧ j ∈ ℂ → A − j ∈ ℂ
14 2 12 13 syl2an ⊢ N ∈ 0 … A ∧ j ∈ 0 … N − 1 → A − j ∈ ℂ
15 oveq2 ⊢ j = A − k → A − j = A − A − k
16 6 7 10 14 15 fprodrev ⊢ N ∈ 0 … A → ∏ j = 0 N − 1 A − j = ∏ k = A − N − 1 A − 0 A − A − k
17 2 subid1d ⊢ N ∈ 0 … A → A − 0 = A
18 17 oveq2d ⊢ N ∈ 0 … A → A − N − 1 … A − 0 = A − N − 1 … A
19 2 adantr ⊢ N ∈ 0 … A ∧ k ∈ A − N − 1 … A − 0 → A ∈ ℂ
20 elfzelz ⊢ k ∈ A − N − 1 … A − 0 → k ∈ ℤ
21 20 zcnd ⊢ k ∈ A − N − 1 … A − 0 → k ∈ ℂ
22 21 adantl ⊢ N ∈ 0 … A ∧ k ∈ A − N − 1 … A − 0 → k ∈ ℂ
23 19 22 nncand ⊢ N ∈ 0 … A ∧ k ∈ A − N − 1 … A − 0 → A − A − k = k
24 18 23 prodeq12dv ⊢ N ∈ 0 … A → ∏ k = A − N − 1 A − 0 A − A − k = ∏ k = A − N − 1 A k
25 5 16 24 3eqtrd ⊢ N ∈ 0 … A → A N _ = ∏ k = A − N − 1 A k