Theorem numnncl

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

	Ref	Expression
Hypotheses	numnncl.1	$$⊢T\in {\mathbb{N}}_0$$
	numnncl.2	$$⊢A\in {\mathbb{N}}_0$$
	numnncl.3	$$⊢B\in \mathbb{N}$$
Assertion	numnncl	$$⊢TA+B\in \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		numnncl.1	$$⊢T\in {\mathbb{N}}_0$$
2		numnncl.2	$$⊢A\in {\mathbb{N}}_0$$
3		numnncl.3	$$⊢B\in \mathbb{N}$$
4	1 2	nn0mulcli	$$⊢TA\in {\mathbb{N}}_0$$
5		nn0nnaddcl	$$⊢\left(TA\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to TA+B\in \mathbb{N}$$
6	4 3 5	mp2an	$$⊢TA+B\in \mathbb{N}$$