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	⊢ ; 𝐴 𝐵 ∈ ℕ