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 NMNM

Proof

Step Hyp Ref Expression
1 nnuz =1
2 1 uztrn2 NMNM