This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 addlidi ⊢ ( 0 + 𝐴 ) = 𝐴
8 5 7 eqtr2i ⊢ 𝐴 = ( ( 𝑇 · 0 ) + 𝐴 )