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 ) ) ... 𝐴 ) 𝑘 )