This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	$⊢ A \in ℝ^{+}$
	Assertion	dp0h	$⊢ 0 . A = \frac{A}{10}$

Step	Hyp	Ref	Expression
1		dp0h.1	$⊢ A \in ℝ^{+}$
2		0nn0	$⊢ 0 \in ℕ_{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}$