Metamath Proof Explorer

Theorem elfzm11

Description: Membership in a finite set of sequential integers. (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Assertion elfzm11 
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( K e. ( M ... ( N - 1 ) ) <-> ( K e. ZZ /\ M <_ K /\ K < N ) ) )

Proof

Step Hyp Ref Expression
1 peano2zm 
 |-  ( N e. ZZ -> ( N - 1 ) e. ZZ )
2 elfz1 
 |-  ( ( M e. ZZ /\ ( N - 1 ) e. ZZ ) -> ( K e. ( M ... ( N - 1 ) ) <-> ( K e. ZZ /\ M <_ K /\ K <_ ( N - 1 ) ) ) )
3 1 2 sylan2 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( K e. ( M ... ( N - 1 ) ) <-> ( K e. ZZ /\ M <_ K /\ K <_ ( N - 1 ) ) ) )
4 zltlem1 
 |-  ( ( K e. ZZ /\ N e. ZZ ) -> ( K < N <-> K <_ ( N - 1 ) ) )
5 4 anbi2d 
 |-  ( ( K e. ZZ /\ N e. ZZ ) -> ( ( M <_ K /\ K < N ) <-> ( M <_ K /\ K <_ ( N - 1 ) ) ) )
6 5 expcom 
 |-  ( N e. ZZ -> ( K e. ZZ -> ( ( M <_ K /\ K < N ) <-> ( M <_ K /\ K <_ ( N - 1 ) ) ) ) )
7 6 pm5.32d 
 |-  ( N e. ZZ -> ( ( K e. ZZ /\ ( M <_ K /\ K < N ) ) <-> ( K e. ZZ /\ ( M <_ K /\ K <_ ( N - 1 ) ) ) ) )
8 3anass 
 |-  ( ( K e. ZZ /\ M <_ K /\ K < N ) <-> ( K e. ZZ /\ ( M <_ K /\ K < N ) ) )
9 3anass 
 |-  ( ( K e. ZZ /\ M <_ K /\ K <_ ( N - 1 ) ) <-> ( K e. ZZ /\ ( M <_ K /\ K <_ ( N - 1 ) ) ) )
10 7 8 9 3bitr4g 
 |-  ( N e. ZZ -> ( ( K e. ZZ /\ M <_ K /\ K < N ) <-> ( K e. ZZ /\ M <_ K /\ K <_ ( N - 1 ) ) ) )
11 10 adantl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( K e. ZZ /\ M <_ K /\ K < N ) <-> ( K e. ZZ /\ M <_ K /\ K <_ ( N - 1 ) ) ) )
12 3 11 bitr4d 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( K e. ( M ... ( N - 1 ) ) <-> ( K e. ZZ /\ M <_ K /\ K < N ) ) )