Metamath Proof Explorer


Theorem dp0h

Description: Remove a zero in the units places. (Contributed by Thierry Arnoux, 16-Dec-2021)

Ref Expression
Hypothesis dp0h.1 𝐴 ∈ ℝ+
Assertion dp0h ( 0 . 𝐴 ) = ( 𝐴 / 1 0 )

Proof

Step Hyp Ref Expression
1 dp0h.1 𝐴 ∈ ℝ+
2 0nn0 0 ∈ ℕ0
3 2 1 dpval3rp ( 0 . 𝐴 ) = 0 𝐴
4 1 dp20h 0 𝐴 = ( 𝐴 / 1 0 )
5 3 4 eqtri ( 0 . 𝐴 ) = ( 𝐴 / 1 0 )