Theorem dp0u

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

	Ref	Expression
Hypothesis	dp0u.1	$$⊢A\in {\mathbb{N}}_0$$
Assertion	dp0u	$$⊢A.0=A$$

Proof

Step	Hyp	Ref	Expression
1		dp0u.1	$$⊢A\in {\mathbb{N}}_0$$
2		0re	$$⊢0\in ℝ$$
3	1 2	dpval3	Could not format ( A . 0 ) = _ A 0 : No typesetting found for |- ( A . 0 ) = _ A 0 with typecode |-
4	1	dp20u	Could not format _ A 0 = A : No typesetting found for |- _ A 0 = A with typecode |-
5	3 4	eqtri	$$⊢A.0=A$$