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