Metamath Proof Explorer

Theorem elfzo2

Description: Membership in a half-open integer interval. (Contributed by Mario Carneiro, 29-Sep-2015)

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

Proof

Step	Hyp	Ref	Expression
1		an4	\|- ( ( ( ( K e. ZZ /\ M e. ZZ ) /\ N e. ZZ ) /\ ( M <_ K /\ K < N ) ) <-> ( ( ( K e. ZZ /\ M e. ZZ ) /\ M <_ K ) /\ ( N e. ZZ /\ K < N ) ) )
2		df-3an	\|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) <-> ( ( K e. ZZ /\ M e. ZZ ) /\ N e. ZZ ) )
3	2	anbi1i	\|- ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M <_ K /\ K < N ) ) <-> ( ( ( K e. ZZ /\ M e. ZZ ) /\ N e. ZZ ) /\ ( M <_ K /\ K < N ) ) )
4		eluz2	\|- ( K e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ K e. ZZ /\ M <_ K ) )
5		3ancoma	\|- ( ( M e. ZZ /\ K e. ZZ /\ M <_ K ) <-> ( K e. ZZ /\ M e. ZZ /\ M <_ K ) )
6		df-3an	\|- ( ( K e. ZZ /\ M e. ZZ /\ M <_ K ) <-> ( ( K e. ZZ /\ M e. ZZ ) /\ M <_ K ) )
7	4 5 6	3bitri	\|- ( K e. ( ZZ>= ` M ) <-> ( ( K e. ZZ /\ M e. ZZ ) /\ M <_ K ) )
8	7	anbi1i	\|- ( ( K e. ( ZZ>= ` M ) /\ ( N e. ZZ /\ K < N ) ) <-> ( ( ( K e. ZZ /\ M e. ZZ ) /\ M <_ K ) /\ ( N e. ZZ /\ K < N ) ) )
9	1 3 8	3bitr4i	\|- ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M <_ K /\ K < N ) ) <-> ( K e. ( ZZ>= ` M ) /\ ( N e. ZZ /\ K < N ) ) )
10		elfzoelz	\|- ( K e. ( M ..^ N ) -> K e. ZZ )
11		elfzoel1	\|- ( K e. ( M ..^ N ) -> M e. ZZ )
12		elfzoel2	\|- ( K e. ( M ..^ N ) -> N e. ZZ )
13	10 11 12	3jca	\|- ( K e. ( M ..^ N ) -> ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) )
14		elfzo	\|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K e. ( M ..^ N ) <-> ( M <_ K /\ K < N ) ) )
15	13 14	biadanii	\|- ( K e. ( M ..^ N ) <-> ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M <_ K /\ K < N ) ) )
16		3anass	\|- ( ( K e. ( ZZ>= ` M ) /\ N e. ZZ /\ K < N ) <-> ( K e. ( ZZ>= ` M ) /\ ( N e. ZZ /\ K < N ) ) )
17	9 15 16	3bitr4i	\|- ( K e. ( M ..^ N ) <-> ( K e. ( ZZ>= ` M ) /\ N e. ZZ /\ K < N ) )