Step |
Hyp |
Ref |
Expression |
1 |
|
peano2zm |
|- ( N e. ZZ -> ( N - 1 ) e. ZZ ) |
2 |
|
elfz |
|- ( ( K e. ZZ /\ M e. ZZ /\ ( N - 1 ) e. ZZ ) -> ( K e. ( M ... ( N - 1 ) ) <-> ( M <_ K /\ K <_ ( N - 1 ) ) ) ) |
3 |
1 2
|
syl3an3 |
|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K e. ( M ... ( N - 1 ) ) <-> ( M <_ K /\ K <_ ( N - 1 ) ) ) ) |
4 |
|
fzoval |
|- ( N e. ZZ -> ( M ..^ N ) = ( M ... ( N - 1 ) ) ) |
5 |
4
|
eleq2d |
|- ( N e. ZZ -> ( K e. ( M ..^ N ) <-> K e. ( M ... ( N - 1 ) ) ) ) |
6 |
5
|
3ad2ant3 |
|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K e. ( M ..^ N ) <-> K e. ( M ... ( N - 1 ) ) ) ) |
7 |
|
zltlem1 |
|- ( ( K e. ZZ /\ N e. ZZ ) -> ( K < N <-> K <_ ( N - 1 ) ) ) |
8 |
7
|
3adant2 |
|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K < N <-> K <_ ( N - 1 ) ) ) |
9 |
8
|
anbi2d |
|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( M <_ K /\ K < N ) <-> ( M <_ K /\ K <_ ( N - 1 ) ) ) ) |
10 |
3 6 9
|
3bitr4d |
|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K e. ( M ..^ N ) <-> ( M <_ K /\ K < N ) ) ) |