Metamath Proof Explorer

Theorem dec0u

Description: Add a zero in the units place. (Contributed by Mario Carneiro, 17-Apr-2015) (Revised by AV, 6-Sep-2021)

Ref Expression
Hypothesis dec0u.1 ⊢ 𝐴 ∈ ℕ0
Assertion dec0u ( 1 0 · 𝐴 ) = 𝐴 0

Proof

Step Hyp Ref Expression
1 dec0u.1 ⊢ 𝐴 ∈ ℕ0
2 10nn0 ⊢ 1 0 ∈ ℕ0
3 2 1 num0u ⊢ ( 1 0 · 𝐴 ) = ( ( 1 0 · 𝐴 ) + 0 )
4 dfdec10 ⊢ 𝐴 0 = ( ( 1 0 · 𝐴 ) + 0 )
5 3 4 eqtr4i ⊢ ( 1 0 · 𝐴 ) = 𝐴 0