Metamath Proof Explorer


Theorem eluznn0

Description: Membership in a nonnegative upper set of integers implies membership in NN0 . (Contributed by Paul Chapman, 22-Jun-2011)

Ref Expression
Assertion eluznn0 ( ( 𝑁 ∈ ℕ0𝑀 ∈ ( ℤ𝑁 ) ) → 𝑀 ∈ ℕ0 )

Proof

Step Hyp Ref Expression
1 nn0uz 0 = ( ℤ ‘ 0 )
2 1 uztrn2 ( ( 𝑁 ∈ ℕ0𝑀 ∈ ( ℤ𝑁 ) ) → 𝑀 ∈ ℕ0 )