Database
REAL AND COMPLEX NUMBERS
Integer sets
Nonnegative integers (as a subset of complex numbers)
3nn0
Next ⟩
4nn0
Metamath Proof Explorer
Ascii
Structured
Theorem
3nn0
Description:
3 is a nonnegative integer.
(Contributed by
Mario Carneiro
, 18-Feb-2014)
Ref
Expression
Assertion
3nn0
⊢
3 ∈ ℕ
_{0}
Proof
Step
Hyp
Ref
Expression
1
3nn
⊢
3 ∈ ℕ
2
1
nnnn0i
⊢
3 ∈ ℕ
_{0}