Theorem dp3mul10

Description: Multiply by 10 a decimal expansion with 3 digits. (Contributed by Thierry Arnoux, 25-Dec-2021)

	Ref	Expression
Hypotheses	dp3mul10.a	⊢ 𝐴 ∈ ℕ0
	dp3mul10.b	⊢ 𝐵 ∈ ℕ0
	dp3mul10.c	⊢ 𝐶 ∈ ℝ
Assertion	dp3mul10	⊢ ( ( 𝐴 . _ 𝐵 𝐶 ) · ; 1 0 ) = ( ; 𝐴 𝐵 . 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		dp3mul10.a	⊢ 𝐴 ∈ ℕ0
2		dp3mul10.b	⊢ 𝐵 ∈ ℕ0
3		dp3mul10.c	⊢ 𝐶 ∈ ℝ
4	2	nn0rei	⊢ 𝐵 ∈ ℝ
5		dp2cl	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → _ 𝐵 𝐶 ∈ ℝ )
6	4 3 5	mp2an	⊢ _ 𝐵 𝐶 ∈ ℝ
7	1 6	dpmul10	⊢ ( ( 𝐴 . _ 𝐵 𝐶 ) · ; 1 0 ) = ; 𝐴 _ 𝐵 𝐶
8		dfdec10	⊢ ; 𝐴 _ 𝐵 𝐶 = ( ( ; 1 0 · 𝐴 ) + _ 𝐵 𝐶 )
9		10nn	⊢ ; 1 0 ∈ ℕ
10	9	nncni	⊢ ; 1 0 ∈ ℂ
11	1	nn0cni	⊢ 𝐴 ∈ ℂ
12	10 11	mulcli	⊢ ( ; 1 0 · 𝐴 ) ∈ ℂ
13	4	recni	⊢ 𝐵 ∈ ℂ
14	3	recni	⊢ 𝐶 ∈ ℂ
15	9	nnne0i	⊢ ; 1 0 ≠ 0
16	14 10 15	divcli	⊢ ( 𝐶 / ; 1 0 ) ∈ ℂ
17	12 13 16	addassi	⊢ ( ( ( ; 1 0 · 𝐴 ) + 𝐵 ) + ( 𝐶 / ; 1 0 ) ) = ( ( ; 1 0 · 𝐴 ) + ( 𝐵 + ( 𝐶 / ; 1 0 ) ) )
18		dfdec10	⊢ ; 𝐴 𝐵 = ( ( ; 1 0 · 𝐴 ) + 𝐵 )
19	18	oveq1i	⊢ ( ; 𝐴 𝐵 + ( 𝐶 / ; 1 0 ) ) = ( ( ( ; 1 0 · 𝐴 ) + 𝐵 ) + ( 𝐶 / ; 1 0 ) )
20		df-dp2	⊢ _ 𝐵 𝐶 = ( 𝐵 + ( 𝐶 / ; 1 0 ) )
21	20	oveq2i	⊢ ( ( ; 1 0 · 𝐴 ) + _ 𝐵 𝐶 ) = ( ( ; 1 0 · 𝐴 ) + ( 𝐵 + ( 𝐶 / ; 1 0 ) ) )
22	17 19 21	3eqtr4ri	⊢ ( ( ; 1 0 · 𝐴 ) + _ 𝐵 𝐶 ) = ( ; 𝐴 𝐵 + ( 𝐶 / ; 1 0 ) )
23	1 2	deccl	⊢ ; 𝐴 𝐵 ∈ ℕ0
24	23 3	dpval2	⊢ ( ; 𝐴 𝐵 . 𝐶 ) = ( ; 𝐴 𝐵 + ( 𝐶 / ; 1 0 ) )
25	22 24	eqtr4i	⊢ ( ( ; 1 0 · 𝐴 ) + _ 𝐵 𝐶 ) = ( ; 𝐴 𝐵 . 𝐶 )
26	7 8 25	3eqtri	⊢ ( ( 𝐴 . _ 𝐵 𝐶 ) · ; 1 0 ) = ( ; 𝐴 𝐵 . 𝐶 )