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