Description: An integer greater than or equal to 2 is not 0. (Contributed by AV, 25-May-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | eluz2n0 | ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ≠ 0 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eluz2nn | ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℕ ) | |
2 | 1 | nnne0d | ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ≠ 0 ) |