This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elfzo3

Description: Express membership in a half-open integer interval in terms of the "less than or equal to" and "less than" predicates on integers, resp. K e. ( ZZ>=M ) <-> M <_ K , K e. ( K ..^ N ) <-> K < N . (Contributed by Mario Carneiro, 29-Sep-2015)

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

Proof

Step Hyp Ref Expression
1 3anass 
 |-  ( ( K e. ( ZZ>= ` M ) /\ N e. ZZ /\ K < N ) <-> ( K e. ( ZZ>= ` M ) /\ ( N e. ZZ /\ K < N ) ) )
2 elfzo2 
 |-  ( K e. ( M ..^ N ) <-> ( K e. ( ZZ>= ` M ) /\ N e. ZZ /\ K < N ) )
3 eluzelz 
 |-  ( K e. ( ZZ>= ` M ) -> K e. ZZ )
4 fzolb 
 |-  ( K e. ( K ..^ N ) <-> ( K e. ZZ /\ N e. ZZ /\ K < N ) )
5 3anass 
 |-  ( ( K e. ZZ /\ N e. ZZ /\ K < N ) <-> ( K e. ZZ /\ ( N e. ZZ /\ K < N ) ) )
6 4 5 bitri 
 |-  ( K e. ( K ..^ N ) <-> ( K e. ZZ /\ ( N e. ZZ /\ K < N ) ) )
7 6 baib 
 |-  ( K e. ZZ -> ( K e. ( K ..^ N ) <-> ( N e. ZZ /\ K < N ) ) )
8 3 7 syl 
 |-  ( K e. ( ZZ>= ` M ) -> ( K e. ( K ..^ N ) <-> ( N e. ZZ /\ K < N ) ) )
9 8 pm5.32i 
 |-  ( ( K e. ( ZZ>= ` M ) /\ K e. ( K ..^ N ) ) <-> ( K e. ( ZZ>= ` M ) /\ ( N e. ZZ /\ K < N ) ) )
10 1 2 9 3bitr4i 
 |-  ( K e. ( M ..^ N ) <-> ( K e. ( ZZ>= ` M ) /\ K e. ( K ..^ N ) ) )