Metamath Proof Explorer

Theorem eluznn

Description: Membership in a positive upper set of integers implies membership in NN . (Contributed by JJ, 1-Oct-2018)

Ref Expression
Assertion eluznn 
|- ( ( N e. NN /\ M e. ( ZZ>= ` N ) ) -> M e. NN )

Proof

Step Hyp Ref Expression
1 nnuz 
 |-  NN = ( ZZ>= ` 1 )
2 1 uztrn2 
 |-  ( ( N e. NN /\ M e. ( ZZ>= ` N ) ) -> M e. NN )