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 \|-

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 ℕ_{0}$
6	5	nn0cni	$⊢ 10 \in ℂ$
7		0re	$⊢ 0 \in ℝ$
8		10pos	$⊢ 0 < 10$
9	7 8	gtneii	$⊢ 10 \neq 0$
10	4 6 9	divcli	$⊢ \frac{A}{10} \in ℂ$
11	10	addlidi	$⊢ 0 + (\frac{A}{10}) = \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 \|-

Metamath Proof Explorer