Metamath Proof Explorer

Theorem eluz

Description: Membership in an upper set of integers. (Contributed by NM, 2-Oct-2005)

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

Proof

Step Hyp Ref Expression
1 eluz1 
 |-  ( M e. ZZ -> ( N e. ( ZZ>= ` M ) <-> ( N e. ZZ /\ M <_ N ) ) )
2 1 baibd 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( N e. ( ZZ>= ` M ) <-> M <_ N ) )