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 ( 𝑁 ∈ ( 0 ... 𝐴 ) → ( 𝐴 FallFac 𝑁 ) = ∏ 𝑘 ∈ ( ( 𝐴 − ( 𝑁 − 1 ) ) ... 𝐴 ) 𝑘 )

Proof

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