Metamath Proof Explorer

Theorem elfz

Description: Membership in a finite set of sequential integers. (Contributed by NM, 29-Sep-2005)

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

Proof

Step Hyp Ref Expression
1 elfz1 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( K e. ( M ... N ) <-> ( K e. ZZ /\ M <_ K /\ K <_ N ) ) )
2 3anass 
 |-  ( ( K e. ZZ /\ M <_ K /\ K <_ N ) <-> ( K e. ZZ /\ ( M <_ K /\ K <_ N ) ) )
3 2 baib 
 |-  ( K e. ZZ -> ( ( K e. ZZ /\ M <_ K /\ K <_ N ) <-> ( M <_ K /\ K <_ N ) ) )
4 1 3 sylan9bb 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ K e. ZZ ) -> ( K e. ( M ... N ) <-> ( M <_ K /\ K <_ N ) ) )
5 4 3impa 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) -> ( K e. ( M ... N ) <-> ( M <_ K /\ K <_ N ) ) )
6 5 3comr 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K e. ( M ... N ) <-> ( M <_ K /\ K <_ N ) ) )