Theorem fzolb2

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	fzolb2	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M e. ( M ..^ N ) <-> M < N ) )

Proof

Step	Hyp	Ref	Expression
1		fzolb	|- ( M e. ( M ..^ N ) <-> ( M e. ZZ /\ N e. ZZ /\ M < N ) )
2		df-3an	|- ( ( M e. ZZ /\ N e. ZZ /\ M < N ) <-> ( ( M e. ZZ /\ N e. ZZ ) /\ M < N ) )
3	1 2	bitri	|- ( M e. ( M ..^ N ) <-> ( ( M e. ZZ /\ N e. ZZ ) /\ M < N ) )
4	3	baib	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M e. ( M ..^ N ) <-> M < N ) )