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

Metamath Proof Explorer

Theorem dp0u

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

		Ref	Expression
	Hypothesis	dp0u.1	$⊢ A \in ℕ_{0}$
	Assertion	dp0u	$⊢ A . 0 = A$

Step	Hyp	Ref	Expression
1		dp0u.1	$⊢ A \in ℕ_{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$