Theorem dp20h

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

	Ref	Expression
Hypothesis	dp20h.1	$$⊢A\in {ℝ}^{+}$$
Assertion	dp20h	Could not format assertion : No typesetting found for |- _ 0 A = ( A / ; 1 0 ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		dp20h.1	$$⊢A\in {ℝ}^{+}$$
2		df-dp2	Could not format _ 0 A = ( 0 + ( A / ; 1 0 ) ) : No typesetting found for |- _ 0 A = ( 0 + ( A / ; 1 0 ) ) with typecode |-
3		rpcn	$$⊢A\in {ℝ}^{+}\to A\in ℂ$$
4	1 3	ax-mp	$$⊢A\in ℂ$$
5		10nn0	$$⊢10\in {\mathbb{N}}_0$$
6	5	nn0cni	$$⊢10\in ℂ$$
7		0re	$$⊢0\in ℝ$$
8		10pos	$$⊢0<10$$
9	7 8	gtneii	$$⊢10\ne 0$$
10	4 6 9	divcli	$$⊢\frac{A}{10}\in ℂ$$
11	10	addlidi	$$⊢0+\left(\frac{A}{10}\right)=\frac{A}{10}$$
12	2 11	eqtri	Could not format _ 0 A = ( A / ; 1 0 ) : No typesetting found for |- _ 0 A = ( A / ; 1 0 ) with typecode |-