Metamath Proof Explorer

Theorem fzolb

Description: The left endpoint of a half-open integer interval is in the set iff the two arguments are integers with M < N . This provides an alternative notation for the "strict upper integer" predicate by analogy to the "weak upper integer" predicate M e. ( ZZ>=N ) . (Contributed by Mario Carneiro, 29-Sep-2015)

Ref Expression
Assertion fzolb M M ..^ N M N M < N


Step Hyp Ref Expression
1 elfzo2 M M ..^ N M M N M < N
2 eluzel2 M M M
3 uzid M M M
4 2 3 impbii M M M
5 4 3anbi1i M M N M < N M N M < N
6 1 5 bitri M M ..^ N M N M < N