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 ) ) )