Database
REAL AND COMPLEX NUMBERS
Integer sets
Upper sets of integers
eluz2n0
Next ⟩
uzuzle23
Metamath Proof Explorer
Ascii
Unicode
Theorem
eluz2n0
Description:
An integer greater than or equal to 2 is not 0.
(Contributed by
AV
, 25-May-2020)
Ref
Expression
Assertion
eluz2n0
⊢
N
∈
ℤ
≥
2
→
N
≠
0
Proof
Step
Hyp
Ref
Expression
1
eluz2nn
⊢
N
∈
ℤ
≥
2
→
N
∈
ℕ
2
1
nnne0d
⊢
N
∈
ℤ
≥
2
→
N
≠
0