Step |
Hyp |
Ref |
Expression |
1 |
|
simpr |
|- ( ( J e. ZZ /\ K e. ( M ... N ) ) -> K e. ( M ... N ) ) |
2 |
|
elfzel1 |
|- ( K e. ( M ... N ) -> M e. ZZ ) |
3 |
2
|
adantl |
|- ( ( J e. ZZ /\ K e. ( M ... N ) ) -> M e. ZZ ) |
4 |
|
elfzel2 |
|- ( K e. ( M ... N ) -> N e. ZZ ) |
5 |
4
|
adantl |
|- ( ( J e. ZZ /\ K e. ( M ... N ) ) -> N e. ZZ ) |
6 |
|
simpl |
|- ( ( J e. ZZ /\ K e. ( M ... N ) ) -> J e. ZZ ) |
7 |
|
elfzelz |
|- ( K e. ( M ... N ) -> K e. ZZ ) |
8 |
7
|
adantl |
|- ( ( J e. ZZ /\ K e. ( M ... N ) ) -> K e. ZZ ) |
9 |
|
fzrev2 |
|- ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( J e. ZZ /\ K e. ZZ ) ) -> ( K e. ( M ... N ) <-> ( J - K ) e. ( ( J - N ) ... ( J - M ) ) ) ) |
10 |
3 5 6 8 9
|
syl22anc |
|- ( ( J e. ZZ /\ K e. ( M ... N ) ) -> ( K e. ( M ... N ) <-> ( J - K ) e. ( ( J - N ) ... ( J - M ) ) ) ) |
11 |
1 10
|
mpbid |
|- ( ( J e. ZZ /\ K e. ( M ... N ) ) -> ( J - K ) e. ( ( J - N ) ... ( J - M ) ) ) |