Theorem dp20u

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

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

Proof

Step	Hyp	Ref	Expression
1		dp20u.1	$$⊢A\in {\mathbb{N}}_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 {\mathbb{N}}_0$$
4	3	nn0rei	$$⊢10\in ℝ$$
5	4	recni	$$⊢10\in ℂ$$
6		0re	$$⊢0\in ℝ$$
7		10pos	$$⊢0<10$$
8	6 7	gtneii	$$⊢10\ne 0$$
9		div0	$$⊢\left(10\in ℂ\wedge 10\ne 0\right)\to \frac{0}{10}=0$$
10	5 8 9	mp2an	$$⊢\frac{0}{10}=0$$
11	10	oveq2i	$$⊢A+\left(\frac{0}{10}\right)=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 |-