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 ) = 𝐴