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 ⊢ T ∈ ℕ 0
numnncl.2 ⊢ A ∈ ℕ 0
Assertion num0h ⊢ A = T ⋅ 0 + A

Proof

Step Hyp Ref Expression
1 numnncl.1 ⊢ T ∈ ℕ 0
2 numnncl.2 ⊢ A ∈ ℕ 0
3 1 nn0cni ⊢ T ∈ ℂ
4 3 mul01i ⊢ T ⋅ 0 = 0
5 4 oveq1i ⊢ T ⋅ 0 + A = 0 + A
6 2 nn0cni ⊢ A ∈ ℂ
7 6 addlidi ⊢ 0 + A = A
8 5 7 eqtr2i ⊢ A = T ⋅ 0 + A