Step |
Hyp |
Ref |
Expression |
1 |
|
fprodshft.1 |
|- ( ph -> K e. ZZ ) |
2 |
|
fprodshft.2 |
|- ( ph -> M e. ZZ ) |
3 |
|
fprodshft.3 |
|- ( ph -> N e. ZZ ) |
4 |
|
fprodshft.4 |
|- ( ( ph /\ j e. ( M ... N ) ) -> A e. CC ) |
5 |
|
fprodrev.5 |
|- ( j = ( K - k ) -> A = B ) |
6 |
|
fzfid |
|- ( ph -> ( ( K - N ) ... ( K - M ) ) e. Fin ) |
7 |
|
eqid |
|- ( j e. ( ( K - N ) ... ( K - M ) ) |-> ( K - j ) ) = ( j e. ( ( K - N ) ... ( K - M ) ) |-> ( K - j ) ) |
8 |
1
|
adantr |
|- ( ( ph /\ j e. ( ( K - N ) ... ( K - M ) ) ) -> K e. ZZ ) |
9 |
|
elfzelz |
|- ( j e. ( ( K - N ) ... ( K - M ) ) -> j e. ZZ ) |
10 |
9
|
adantl |
|- ( ( ph /\ j e. ( ( K - N ) ... ( K - M ) ) ) -> j e. ZZ ) |
11 |
8 10
|
zsubcld |
|- ( ( ph /\ j e. ( ( K - N ) ... ( K - M ) ) ) -> ( K - j ) e. ZZ ) |
12 |
1
|
adantr |
|- ( ( ph /\ k e. ( M ... N ) ) -> K e. ZZ ) |
13 |
|
elfzelz |
|- ( k e. ( M ... N ) -> k e. ZZ ) |
14 |
13
|
adantl |
|- ( ( ph /\ k e. ( M ... N ) ) -> k e. ZZ ) |
15 |
12 14
|
zsubcld |
|- ( ( ph /\ k e. ( M ... N ) ) -> ( K - k ) e. ZZ ) |
16 |
|
simprr |
|- ( ( ph /\ ( j e. ( ( K - N ) ... ( K - M ) ) /\ k = ( K - j ) ) ) -> k = ( K - j ) ) |
17 |
|
simprl |
|- ( ( ph /\ ( j e. ( ( K - N ) ... ( K - M ) ) /\ k = ( K - j ) ) ) -> j e. ( ( K - N ) ... ( K - M ) ) ) |
18 |
2
|
adantr |
|- ( ( ph /\ ( j e. ( ( K - N ) ... ( K - M ) ) /\ k = ( K - j ) ) ) -> M e. ZZ ) |
19 |
3
|
adantr |
|- ( ( ph /\ ( j e. ( ( K - N ) ... ( K - M ) ) /\ k = ( K - j ) ) ) -> N e. ZZ ) |
20 |
1
|
adantr |
|- ( ( ph /\ ( j e. ( ( K - N ) ... ( K - M ) ) /\ k = ( K - j ) ) ) -> K e. ZZ ) |
21 |
9
|
ad2antrl |
|- ( ( ph /\ ( j e. ( ( K - N ) ... ( K - M ) ) /\ k = ( K - j ) ) ) -> j e. ZZ ) |
22 |
|
fzrev |
|- ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ j e. ZZ ) ) -> ( j e. ( ( K - N ) ... ( K - M ) ) <-> ( K - j ) e. ( M ... N ) ) ) |
23 |
18 19 20 21 22
|
syl22anc |
|- ( ( ph /\ ( j e. ( ( K - N ) ... ( K - M ) ) /\ k = ( K - j ) ) ) -> ( j e. ( ( K - N ) ... ( K - M ) ) <-> ( K - j ) e. ( M ... N ) ) ) |
24 |
17 23
|
mpbid |
|- ( ( ph /\ ( j e. ( ( K - N ) ... ( K - M ) ) /\ k = ( K - j ) ) ) -> ( K - j ) e. ( M ... N ) ) |
25 |
16 24
|
eqeltrd |
|- ( ( ph /\ ( j e. ( ( K - N ) ... ( K - M ) ) /\ k = ( K - j ) ) ) -> k e. ( M ... N ) ) |
26 |
|
oveq2 |
|- ( k = ( K - j ) -> ( K - k ) = ( K - ( K - j ) ) ) |
27 |
26
|
ad2antll |
|- ( ( ph /\ ( j e. ( ( K - N ) ... ( K - M ) ) /\ k = ( K - j ) ) ) -> ( K - k ) = ( K - ( K - j ) ) ) |
28 |
1
|
zcnd |
|- ( ph -> K e. CC ) |
29 |
28
|
adantr |
|- ( ( ph /\ ( j e. ( ( K - N ) ... ( K - M ) ) /\ k = ( K - j ) ) ) -> K e. CC ) |
30 |
9
|
zcnd |
|- ( j e. ( ( K - N ) ... ( K - M ) ) -> j e. CC ) |
31 |
30
|
ad2antrl |
|- ( ( ph /\ ( j e. ( ( K - N ) ... ( K - M ) ) /\ k = ( K - j ) ) ) -> j e. CC ) |
32 |
29 31
|
nncand |
|- ( ( ph /\ ( j e. ( ( K - N ) ... ( K - M ) ) /\ k = ( K - j ) ) ) -> ( K - ( K - j ) ) = j ) |
33 |
27 32
|
eqtr2d |
|- ( ( ph /\ ( j e. ( ( K - N ) ... ( K - M ) ) /\ k = ( K - j ) ) ) -> j = ( K - k ) ) |
34 |
25 33
|
jca |
|- ( ( ph /\ ( j e. ( ( K - N ) ... ( K - M ) ) /\ k = ( K - j ) ) ) -> ( k e. ( M ... N ) /\ j = ( K - k ) ) ) |
35 |
|
simprr |
|- ( ( ph /\ ( k e. ( M ... N ) /\ j = ( K - k ) ) ) -> j = ( K - k ) ) |
36 |
|
simprl |
|- ( ( ph /\ ( k e. ( M ... N ) /\ j = ( K - k ) ) ) -> k e. ( M ... N ) ) |
37 |
2
|
adantr |
|- ( ( ph /\ ( k e. ( M ... N ) /\ j = ( K - k ) ) ) -> M e. ZZ ) |
38 |
3
|
adantr |
|- ( ( ph /\ ( k e. ( M ... N ) /\ j = ( K - k ) ) ) -> N e. ZZ ) |
39 |
1
|
adantr |
|- ( ( ph /\ ( k e. ( M ... N ) /\ j = ( K - k ) ) ) -> K e. ZZ ) |
40 |
13
|
ad2antrl |
|- ( ( ph /\ ( k e. ( M ... N ) /\ j = ( K - k ) ) ) -> k e. ZZ ) |
41 |
|
fzrev2 |
|- ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ k e. ZZ ) ) -> ( k e. ( M ... N ) <-> ( K - k ) e. ( ( K - N ) ... ( K - M ) ) ) ) |
42 |
37 38 39 40 41
|
syl22anc |
|- ( ( ph /\ ( k e. ( M ... N ) /\ j = ( K - k ) ) ) -> ( k e. ( M ... N ) <-> ( K - k ) e. ( ( K - N ) ... ( K - M ) ) ) ) |
43 |
36 42
|
mpbid |
|- ( ( ph /\ ( k e. ( M ... N ) /\ j = ( K - k ) ) ) -> ( K - k ) e. ( ( K - N ) ... ( K - M ) ) ) |
44 |
35 43
|
eqeltrd |
|- ( ( ph /\ ( k e. ( M ... N ) /\ j = ( K - k ) ) ) -> j e. ( ( K - N ) ... ( K - M ) ) ) |
45 |
|
oveq2 |
|- ( j = ( K - k ) -> ( K - j ) = ( K - ( K - k ) ) ) |
46 |
45
|
ad2antll |
|- ( ( ph /\ ( k e. ( M ... N ) /\ j = ( K - k ) ) ) -> ( K - j ) = ( K - ( K - k ) ) ) |
47 |
28
|
adantr |
|- ( ( ph /\ ( k e. ( M ... N ) /\ j = ( K - k ) ) ) -> K e. CC ) |
48 |
13
|
zcnd |
|- ( k e. ( M ... N ) -> k e. CC ) |
49 |
48
|
ad2antrl |
|- ( ( ph /\ ( k e. ( M ... N ) /\ j = ( K - k ) ) ) -> k e. CC ) |
50 |
47 49
|
nncand |
|- ( ( ph /\ ( k e. ( M ... N ) /\ j = ( K - k ) ) ) -> ( K - ( K - k ) ) = k ) |
51 |
46 50
|
eqtr2d |
|- ( ( ph /\ ( k e. ( M ... N ) /\ j = ( K - k ) ) ) -> k = ( K - j ) ) |
52 |
44 51
|
jca |
|- ( ( ph /\ ( k e. ( M ... N ) /\ j = ( K - k ) ) ) -> ( j e. ( ( K - N ) ... ( K - M ) ) /\ k = ( K - j ) ) ) |
53 |
34 52
|
impbida |
|- ( ph -> ( ( j e. ( ( K - N ) ... ( K - M ) ) /\ k = ( K - j ) ) <-> ( k e. ( M ... N ) /\ j = ( K - k ) ) ) ) |
54 |
7 11 15 53
|
f1od |
|- ( ph -> ( j e. ( ( K - N ) ... ( K - M ) ) |-> ( K - j ) ) : ( ( K - N ) ... ( K - M ) ) -1-1-onto-> ( M ... N ) ) |
55 |
|
oveq2 |
|- ( j = k -> ( K - j ) = ( K - k ) ) |
56 |
|
ovex |
|- ( K - k ) e. _V |
57 |
55 7 56
|
fvmpt |
|- ( k e. ( ( K - N ) ... ( K - M ) ) -> ( ( j e. ( ( K - N ) ... ( K - M ) ) |-> ( K - j ) ) ` k ) = ( K - k ) ) |
58 |
57
|
adantl |
|- ( ( ph /\ k e. ( ( K - N ) ... ( K - M ) ) ) -> ( ( j e. ( ( K - N ) ... ( K - M ) ) |-> ( K - j ) ) ` k ) = ( K - k ) ) |
59 |
5 6 54 58 4
|
fprodf1o |
|- ( ph -> prod_ j e. ( M ... N ) A = prod_ k e. ( ( K - N ) ... ( K - M ) ) B ) |