Theorem numnncl2

Description: Closure for a decimal integer (zero units place). (Contributed by Mario Carneiro, 9-Mar-2015)

	Ref	Expression
Hypotheses	numnncl2.1	$$⊢T\in \mathbb{N}$$
	numnncl2.2	$$⊢A\in \mathbb{N}$$
Assertion	numnncl2	$$⊢TA+0\in \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		numnncl2.1	$$⊢T\in \mathbb{N}$$
2		numnncl2.2	$$⊢A\in \mathbb{N}$$
3	1 2	nnmulcli	$$⊢TA\in \mathbb{N}$$
4	3	nncni	$$⊢TA\in ℂ$$
5	4	addridi	$$⊢TA+0=TA$$
6	5 3	eqeltri	$$⊢TA+0\in \mathbb{N}$$