Theorem eluz1

Description: Membership in the upper set of integers starting at M . (Contributed by NM, 5-Sep-2005)

	Ref	Expression
Assertion	eluz1	|- ( M e. ZZ -> ( N e. ( ZZ>= ` M ) <-> ( N e. ZZ /\ M <_ N ) ) )

Proof

Step	Hyp	Ref	Expression
1		uzval	|- ( M e. ZZ -> ( ZZ>= ` M ) = { k e. ZZ | M <_ k } )
2	1	eleq2d	|- ( M e. ZZ -> ( N e. ( ZZ>= ` M ) <-> N e. { k e. ZZ | M <_ k } ) )
3		breq2	|- ( k = N -> ( M <_ k <-> M <_ N ) )
4	3	elrab	|- ( N e. { k e. ZZ | M <_ k } <-> ( N e. ZZ /\ M <_ N ) )
5	2 4	bitrdi	|- ( M e. ZZ -> ( N e. ( ZZ>= ` M ) <-> ( N e. ZZ /\ M <_ N ) ) )