Theorem num0u

Description: Add a zero in the 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$$
Assertion	num0u	$$⊢TA=TA+0$$

Proof

Step	Hyp	Ref	Expression
1		numnncl.1	$$⊢T\in {\mathbb{N}}_0$$
2		numnncl.2	$$⊢A\in {\mathbb{N}}_0$$
3	1 2	nn0mulcli	$$⊢TA\in {\mathbb{N}}_0$$
4	3	nn0cni	$$⊢TA\in ℂ$$
5	4	addridi	$$⊢TA+0=TA$$
6	5	eqcomi	$$⊢TA=TA+0$$