Database
REAL AND COMPLEX NUMBERS
Integer sets
Decimal arithmetic
11nn0
Next ⟩
12nn0
Metamath Proof Explorer
Ascii
Structured
Theorem
11nn0
Description:
11 is a nonnegative integer.
(Contributed by
Umit Teoman Dogan
, 10-Jun-2026)
Ref
Expression
Assertion
11nn0
⊢
;
1 1 ∈ ℕ
0
Proof
Step
Hyp
Ref
Expression
1
1nn0
⊢
1 ∈ ℕ
0
2
1
1
deccl
⊢
;
1 1 ∈ ℕ
0