Metamath Proof Explorer


Theorem dp0u

Description: Add a zero in the tenths place. (Contributed by Thierry Arnoux, 16-Dec-2021)

Ref Expression
Hypothesis dp0u.1 𝐴 ∈ ℕ0
Assertion dp0u ( 𝐴 . 0 ) = 𝐴

Proof

Step Hyp Ref Expression
1 dp0u.1 𝐴 ∈ ℕ0
2 0re 0 ∈ ℝ
3 1 2 dpval3 ( 𝐴 . 0 ) = 𝐴 0
4 1 dp20u 𝐴 0 = 𝐴
5 3 4 eqtri ( 𝐴 . 0 ) = 𝐴