Step |
Hyp |
Ref |
Expression |
1 |
|
oveq1 |
⊢ ( 𝑥 = 𝐴 → ( 𝑥 − 𝑘 ) = ( 𝐴 − 𝑘 ) ) |
2 |
1
|
prodeq2sdv |
⊢ ( 𝑥 = 𝐴 → ∏ 𝑘 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝑥 − 𝑘 ) = ∏ 𝑘 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝐴 − 𝑘 ) ) |
3 |
|
oveq1 |
⊢ ( 𝑛 = 𝑁 → ( 𝑛 − 1 ) = ( 𝑁 − 1 ) ) |
4 |
3
|
oveq2d |
⊢ ( 𝑛 = 𝑁 → ( 0 ... ( 𝑛 − 1 ) ) = ( 0 ... ( 𝑁 − 1 ) ) ) |
5 |
4
|
prodeq1d |
⊢ ( 𝑛 = 𝑁 → ∏ 𝑘 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝐴 − 𝑘 ) = ∏ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 𝐴 − 𝑘 ) ) |
6 |
|
df-fallfac |
⊢ FallFac = ( 𝑥 ∈ ℂ , 𝑛 ∈ ℕ0 ↦ ∏ 𝑘 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝑥 − 𝑘 ) ) |
7 |
|
prodex |
⊢ ∏ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 𝐴 − 𝑘 ) ∈ V |
8 |
2 5 6 7
|
ovmpo |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 FallFac 𝑁 ) = ∏ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 𝐴 − 𝑘 ) ) |