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