Theorem numcl

Description: Closure for a decimal integer (with units place). (Contributed by Mario Carneiro, 18-Feb-2014)

	Ref	Expression
Hypotheses	numnncl.1	⊢ 𝑇 ∈ ℕ0
	numnncl.2	⊢ 𝐴 ∈ ℕ0
	numcl.2	⊢ 𝐵 ∈ ℕ0
Assertion	numcl	⊢ ( ( 𝑇 · 𝐴 ) + 𝐵 ) ∈ ℕ0

Proof

Step	Hyp	Ref	Expression
1		numnncl.1	⊢ 𝑇 ∈ ℕ0
2		numnncl.2	⊢ 𝐴 ∈ ℕ0
3		numcl.2	⊢ 𝐵 ∈ ℕ0
4	1 2	nn0mulcli	⊢ ( 𝑇 · 𝐴 ) ∈ ℕ0
5	4 3	nn0addcli	⊢ ( ( 𝑇 · 𝐴 ) + 𝐵 ) ∈ ℕ0