This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem decnncl

Description: Closure for a numeral. (Contributed by Mario Carneiro, 17-Apr-2015) (Revised by AV, 6-Sep-2021)

Ref Expression
Hypotheses decnncl.1 ⊢ 𝐴 ∈ ℕ0
decnncl.2 ⊢ 𝐵 ∈ ℕ
Assertion decnncl 𝐴 𝐵 ∈ ℕ

Proof

Step Hyp Ref Expression
1 decnncl.1 ⊢ 𝐴 ∈ ℕ0
2 decnncl.2 ⊢ 𝐵 ∈ ℕ
3 dfdec10 ⊢ 𝐴 𝐵 = ( ( 1 0 · 𝐴 ) + 𝐵 )
4 10nn0 ⊢ 1 0 ∈ ℕ0
5 4 1 2 numnncl ⊢ ( ( 1 0 · 𝐴 ) + 𝐵 ) ∈ ℕ
6 3 5 eqeltri ⊢ 𝐴 𝐵 ∈ ℕ