Theorem numnncl

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

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

Proof

Step	Hyp	Ref	Expression
1		numnncl.1	⊢ 𝑇 ∈ ℕ0
2		numnncl.2	⊢ 𝐴 ∈ ℕ0
3		numnncl.3	⊢ 𝐵 ∈ ℕ
4	1 2	nn0mulcli	⊢ ( 𝑇 · 𝐴 ) ∈ ℕ0
5		nn0nnaddcl	⊢ ( ( ( 𝑇 · 𝐴 ) ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → ( ( 𝑇 · 𝐴 ) + 𝐵 ) ∈ ℕ )
6	4 3 5	mp2an	⊢ ( ( 𝑇 · 𝐴 ) + 𝐵 ) ∈ ℕ