Database
REAL AND COMPLEX NUMBERS
Integer sets
Nonnegative integers (as a subset of complex numbers)
2nn0
Next ⟩
3nn0
Metamath Proof Explorer
Ascii
Unicode
Theorem
2nn0
Description:
2 is a nonnegative integer.
(Contributed by
Raph Levien
, 10-Dec-2002)
Ref
Expression
Assertion
2nn0
⊢
2
∈
ℕ
0
Proof
Step
Hyp
Ref
Expression
1
2nn
⊢
2
∈
ℕ
2
1
nnnn0i
⊢
2
∈
ℕ
0