Theorem dp0h

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

	Ref	Expression
Hypothesis	dp0h.1	$$⊢A\in {ℝ}^{+}$$
Assertion	dp0h	$$⊢0.A=\frac{A}{10}$$

Proof

Step	Hyp	Ref	Expression
1		dp0h.1	$$⊢A\in {ℝ}^{+}$$
2		0nn0	$$⊢0\in {\mathbb{N}}_0$$
3	2 1	dpval3rp	Could not format ( 0 . A ) = _ 0 A : No typesetting found for |- ( 0 . A ) = _ 0 A with typecode |-
4	1	dp20h	Could not format _ 0 A = ( A / ; 1 0 ) : No typesetting found for |- _ 0 A = ( A / ; 1 0 ) with typecode |-
5	3 4	eqtri	$$⊢0.A=\frac{A}{10}$$