Theorem num0h

Description: Add a zero in the higher places. (Contributed by Mario Carneiro, 18-Feb-2014)

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

Proof

Step	Hyp	Ref	Expression
1		numnncl.1	⊢ 𝑇 ∈ ℕ0
2		numnncl.2	⊢ 𝐴 ∈ ℕ0
3	1	nn0cni	⊢ 𝑇 ∈ ℂ
4	3	mul01i	⊢ ( 𝑇 · 0 ) = 0
5	4	oveq1i	⊢ ( ( 𝑇 · 0 ) + 𝐴 ) = ( 0 + 𝐴 )
6	2	nn0cni	⊢ 𝐴 ∈ ℂ
7	6	addid2i	⊢ ( 0 + 𝐴 ) = 𝐴
8	5 7	eqtr2i	⊢ 𝐴 = ( ( 𝑇 · 0 ) + 𝐴 )