Metamath Proof Explorer


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