Step |
Hyp |
Ref |
Expression |
1 |
|
elfz3nn0 |
|- ( N e. ( 0 ... A ) -> A e. NN0 ) |
2 |
1
|
nn0cnd |
|- ( N e. ( 0 ... A ) -> A e. CC ) |
3 |
|
elfznn0 |
|- ( N e. ( 0 ... A ) -> N e. NN0 ) |
4 |
|
fallfacval |
|- ( ( A e. CC /\ N e. NN0 ) -> ( A FallFac N ) = prod_ j e. ( 0 ... ( N - 1 ) ) ( A - j ) ) |
5 |
2 3 4
|
syl2anc |
|- ( N e. ( 0 ... A ) -> ( A FallFac N ) = prod_ j e. ( 0 ... ( N - 1 ) ) ( A - j ) ) |
6 |
|
elfzel2 |
|- ( N e. ( 0 ... A ) -> A e. ZZ ) |
7 |
|
elfzel1 |
|- ( N e. ( 0 ... A ) -> 0 e. ZZ ) |
8 |
|
elfzelz |
|- ( N e. ( 0 ... A ) -> N e. ZZ ) |
9 |
|
peano2zm |
|- ( N e. ZZ -> ( N - 1 ) e. ZZ ) |
10 |
8 9
|
syl |
|- ( N e. ( 0 ... A ) -> ( N - 1 ) e. ZZ ) |
11 |
|
elfzelz |
|- ( j e. ( 0 ... ( N - 1 ) ) -> j e. ZZ ) |
12 |
11
|
zcnd |
|- ( j e. ( 0 ... ( N - 1 ) ) -> j e. CC ) |
13 |
|
subcl |
|- ( ( A e. CC /\ j e. CC ) -> ( A - j ) e. CC ) |
14 |
2 12 13
|
syl2an |
|- ( ( N e. ( 0 ... A ) /\ j e. ( 0 ... ( N - 1 ) ) ) -> ( A - j ) e. CC ) |
15 |
|
oveq2 |
|- ( j = ( A - k ) -> ( A - j ) = ( A - ( A - k ) ) ) |
16 |
6 7 10 14 15
|
fprodrev |
|- ( N e. ( 0 ... A ) -> prod_ j e. ( 0 ... ( N - 1 ) ) ( A - j ) = prod_ k e. ( ( A - ( N - 1 ) ) ... ( A - 0 ) ) ( A - ( A - k ) ) ) |
17 |
2
|
subid1d |
|- ( N e. ( 0 ... A ) -> ( A - 0 ) = A ) |
18 |
17
|
oveq2d |
|- ( N e. ( 0 ... A ) -> ( ( A - ( N - 1 ) ) ... ( A - 0 ) ) = ( ( A - ( N - 1 ) ) ... A ) ) |
19 |
2
|
adantr |
|- ( ( N e. ( 0 ... A ) /\ k e. ( ( A - ( N - 1 ) ) ... ( A - 0 ) ) ) -> A e. CC ) |
20 |
|
elfzelz |
|- ( k e. ( ( A - ( N - 1 ) ) ... ( A - 0 ) ) -> k e. ZZ ) |
21 |
20
|
zcnd |
|- ( k e. ( ( A - ( N - 1 ) ) ... ( A - 0 ) ) -> k e. CC ) |
22 |
21
|
adantl |
|- ( ( N e. ( 0 ... A ) /\ k e. ( ( A - ( N - 1 ) ) ... ( A - 0 ) ) ) -> k e. CC ) |
23 |
19 22
|
nncand |
|- ( ( N e. ( 0 ... A ) /\ k e. ( ( A - ( N - 1 ) ) ... ( A - 0 ) ) ) -> ( A - ( A - k ) ) = k ) |
24 |
18 23
|
prodeq12dv |
|- ( N e. ( 0 ... A ) -> prod_ k e. ( ( A - ( N - 1 ) ) ... ( A - 0 ) ) ( A - ( A - k ) ) = prod_ k e. ( ( A - ( N - 1 ) ) ... A ) k ) |
25 |
5 16 24
|
3eqtrd |
|- ( N e. ( 0 ... A ) -> ( A FallFac N ) = prod_ k e. ( ( A - ( N - 1 ) ) ... A ) k ) |