Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > eluznn | Structured version Visualization version GIF version |
Description: Membership in a positive upper set of integers implies membership in ℕ. (Contributed by JJ, 1-Oct-2018.) |
Ref | Expression |
---|---|
eluznn | ⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ ℕ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nnuz 11599 | . 2 ⊢ ℕ = (ℤ≥‘1) | |
2 | 1 | uztrn2 11581 | 1 ⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ ℕ) |
Copyright terms: Public domain | W3C validator |