Metamath Proof Explorer

Theorem eluzle

Description: Implication of membership in an upper set of integers. (Contributed by NM, 6-Sep-2005)

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

Proof

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