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