This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ N ∈ ℕ 0 ∧ M ∈ ℤ ≥ N → M ∈ ℕ 0

Proof

Step Hyp Ref Expression
1 nn0uz ⊢ ℕ 0 = ℤ ≥ 0
2 1 uztrn2 ⊢ N ∈ ℕ 0 ∧ M ∈ ℤ ≥ N → M ∈ ℕ 0