Database
REAL AND COMPLEX NUMBERS
Integer sets
Extended nonnegative integers
0xnn0
Next ⟩
pnf0xnn0
Metamath Proof Explorer
Ascii
Structured
Theorem
0xnn0
Description:
Zero is an extended nonnegative integer.
(Contributed by
AV
, 10-Dec-2020)
Ref
Expression
Assertion
0xnn0
⊢
0 ∈ ℕ
0
*
Proof
Step
Hyp
Ref
Expression
1
nn0ssxnn0
⊢
ℕ
0
⊆ ℕ
0
*
2
0nn0
⊢
0 ∈ ℕ
0
3
1
2
sselii
⊢
0 ∈ ℕ
0
*