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 )