dp20u

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

		Ref	Expression
	Hypothesis	dp20u.1	$⊢ A \in ℕ_{0}$
	Assertion	dp20u	Could not format assertion : No typesetting found for \|- _ A 0 = A with typecode \|-

Step	Hyp	Ref	Expression
1		dp20u.1	$⊢ A \in ℕ_{0}$
2		df-dp2	Could not format _ A 0 = ( A + ( 0 / ; 1 0 ) ) : No typesetting found for \|- _ A 0 = ( A + ( 0 / ; 1 0 ) ) with typecode \|-
3		10nn0	$⊢ 10 \in ℕ_{0}$
4	3	nn0rei	$⊢ 10 \in ℝ$
5	4	recni	$⊢ 10 \in ℂ$
6		0re	$⊢ 0 \in ℝ$
7		10pos	$⊢ 0 < 10$
8	6 7	gtneii	$⊢ 10 \neq 0$
9		div0	$⊢ (10 \in ℂ \land 10 \neq 0) \to \frac{0}{10} = 0$
10	5 8 9	mp2an	$⊢ \frac{0}{10} = 0$
11	10	oveq2i	$⊢ A + (\frac{0}{10}) = A + 0$
12	1	nn0cni	$⊢ A \in ℂ$
13	12	addridi	$⊢ A + 0 = A$
14	2 11 13	3eqtri	Could not format _ A 0 = A : No typesetting found for \|- _ A 0 = A with typecode \|-

Metamath Proof Explorer