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 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nn0uz | ⊢ ℕ0 = ( ℤ≥ ‘ 0 ) | |
2 | 1 | uztrn2 | ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑀 ∈ ℕ0 ) |