Theorem dp20h

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

	Ref	Expression
Hypothesis	dp20h.1	⊢ 𝐴 ∈ ℝ+
Assertion	dp20h	⊢ _ 0 𝐴 = ( 𝐴 / ; 1 0 )

Proof

Step	Hyp	Ref	Expression
1		dp20h.1	⊢ 𝐴 ∈ ℝ+
2		df-dp2	⊢ _ 0 𝐴 = ( 0 + ( 𝐴 / ; 1 0 ) )
3		rpcn	⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℂ )
4	1 3	ax-mp	⊢ 𝐴 ∈ ℂ
5		10nn0	⊢ ; 1 0 ∈ ℕ0
6	5	nn0cni	⊢ ; 1 0 ∈ ℂ
7		0re	⊢ 0 ∈ ℝ
8		10pos	⊢ 0 < ; 1 0
9	7 8	gtneii	⊢ ; 1 0 ≠ 0
10	4 6 9	divcli	⊢ ( 𝐴 / ; 1 0 ) ∈ ℂ
11	10	addid2i	⊢ ( 0 + ( 𝐴 / ; 1 0 ) ) = ( 𝐴 / ; 1 0 )
12	2 11	eqtri	⊢ _ 0 𝐴 = ( 𝐴 / ; 1 0 )