Theorem dp20u

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

	Ref	Expression
Hypothesis	dp20u.1	⊢ 𝐴 ∈ ℕ0
Assertion	dp20u	⊢ _ 𝐴 0 = 𝐴

Proof

Step	Hyp	Ref	Expression
1		dp20u.1	⊢ 𝐴 ∈ ℕ0
2		df-dp2	⊢ _ 𝐴 0 = ( 𝐴 + ( 0 / ; 1 0 ) )
3		10nn0	⊢ ; 1 0 ∈ ℕ0
4	3	nn0rei	⊢ ; 1 0 ∈ ℝ
5	4	recni	⊢ ; 1 0 ∈ ℂ
6		0re	⊢ 0 ∈ ℝ
7		10pos	⊢ 0 < ; 1 0
8	6 7	gtneii	⊢ ; 1 0 ≠ 0
9		div0	⊢ ( ( ; 1 0 ∈ ℂ ∧ ; 1 0 ≠ 0 ) → ( 0 / ; 1 0 ) = 0 )
10	5 8 9	mp2an	⊢ ( 0 / ; 1 0 ) = 0
11	10	oveq2i	⊢ ( 𝐴 + ( 0 / ; 1 0 ) ) = ( 𝐴 + 0 )
12	1	nn0cni	⊢ 𝐴 ∈ ℂ
13	12	addid1i	⊢ ( 𝐴 + 0 ) = 𝐴
14	2 11 13	3eqtri	⊢ _ 𝐴 0 = 𝐴