Metamath Proof Explorer

Theorem elfz5

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

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

Proof

Step Hyp Ref Expression
1 eluzelz 
 |-  ( K e. ( ZZ>= ` M ) -> K e. ZZ )
2 eluzel2 
 |-  ( K e. ( ZZ>= ` M ) -> M e. ZZ )
3 1 2 jca 
 |-  ( K e. ( ZZ>= ` M ) -> ( K e. ZZ /\ M e. ZZ ) )
4 elfz 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K e. ( M ... N ) <-> ( M <_ K /\ K <_ N ) ) )
5 4 3expa 
 |-  ( ( ( K e. ZZ /\ M e. ZZ ) /\ N e. ZZ ) -> ( K e. ( M ... N ) <-> ( M <_ K /\ K <_ N ) ) )
6 3 5 sylan 
 |-  ( ( K e. ( ZZ>= ` M ) /\ N e. ZZ ) -> ( K e. ( M ... N ) <-> ( M <_ K /\ K <_ N ) ) )
7 eluzle 
 |-  ( K e. ( ZZ>= ` M ) -> M <_ K )
8 7 biantrurd 
 |-  ( K e. ( ZZ>= ` M ) -> ( K <_ N <-> ( M <_ K /\ K <_ N ) ) )
9 8 adantr 
 |-  ( ( K e. ( ZZ>= ` M ) /\ N e. ZZ ) -> ( K <_ N <-> ( M <_ K /\ K <_ N ) ) )
10 6 9 bitr4d 
 |-  ( ( K e. ( ZZ>= ` M ) /\ N e. ZZ ) -> ( K e. ( M ... N ) <-> K <_ N ) )