Theorem num0h

Description: Add a zero in the higher places. (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	num0h	$$⊢A=T\cdot 0+A$$

Proof

Step	Hyp	Ref	Expression
1		numnncl.1	$$⊢T\in {\mathbb{N}}_0$$
2		numnncl.2	$$⊢A\in {\mathbb{N}}_0$$
3	1	nn0cni	$$⊢T\in ℂ$$
4	3	mul01i	$$⊢T\cdot 0=0$$
5	4	oveq1i	$$⊢T\cdot 0+A=0+A$$
6	2	nn0cni	$$⊢A\in ℂ$$
7	6	addlidi	$$⊢0+A=A$$
8	5 7	eqtr2i	$$⊢A=T\cdot 0+A$$