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

Metamath Proof Explorer

Theorem deccl

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

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

Proof

Step Hyp Ref Expression
1 deccl.1 ⊢ 𝐴 ∈ ℕ0
2 deccl.2 ⊢ 𝐵 ∈ ℕ0
3 df-dec ⊢ 𝐴 𝐵 = ( ( ( 9 + 1 ) · 𝐴 ) + 𝐵 )
4 9nn0 ⊢ 9 ∈ ℕ0
5 1nn0 ⊢ 1 ∈ ℕ0
6 4 5 nn0addcli ⊢ ( 9 + 1 ) ∈ ℕ0
7 6 1 2 numcl ⊢ ( ( ( 9 + 1 ) · 𝐴 ) + 𝐵 ) ∈ ℕ0
8 3 7 eqeltri ⊢ 𝐴 𝐵 ∈ ℕ0