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