Description: A positive integer expressed as a member of an upper set of integers. (Contributed by NM, 6-Jun-2006)
Ref | Expression | ||
---|---|---|---|
Assertion | elnnuz | ⊢ ( 𝑁 ∈ ℕ ↔ 𝑁 ∈ ( ℤ_{≥} ‘ 1 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nnuz | ⊢ ℕ = ( ℤ_{≥} ‘ 1 ) | |
2 | 1 | eleq2i | ⊢ ( 𝑁 ∈ ℕ ↔ 𝑁 ∈ ( ℤ_{≥} ‘ 1 ) ) |