Theorem dp3mul10

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

	Ref	Expression
Hypotheses	dp3mul10.a	|- A e. NN0
	dp3mul10.b	|- B e. NN0
	dp3mul10.c	|- C e. RR
Assertion	dp3mul10	|- ( ( A . _ B C ) x. ; 1 0 ) = ( ; A B . C )

Proof

Step	Hyp	Ref	Expression
1		dp3mul10.a	|- A e. NN0
2		dp3mul10.b	|- B e. NN0
3		dp3mul10.c	|- C e. RR
4	2	nn0rei	|- B e. RR
5		dp2cl	|- ( ( B e. RR /\ C e. RR ) -> _ B C e. RR )
6	4 3 5	mp2an	|- _ B C e. RR
7	1 6	dpmul10	|- ( ( A . _ B C ) x. ; 1 0 ) = ; A _ B C
8		dfdec10	|- ; A _ B C = ( ( ; 1 0 x. A ) + _ B C )
9		10nn	|- ; 1 0 e. NN
10	9	nncni	|- ; 1 0 e. CC
11	1	nn0cni	|- A e. CC
12	10 11	mulcli	|- ( ; 1 0 x. A ) e. CC
13	4	recni	|- B e. CC
14	3	recni	|- C e. CC
15	9	nnne0i	|- ; 1 0 =/= 0
16	14 10 15	divcli	|- ( C / ; 1 0 ) e. CC
17	12 13 16	addassi	|- ( ( ( ; 1 0 x. A ) + B ) + ( C / ; 1 0 ) ) = ( ( ; 1 0 x. A ) + ( B + ( C / ; 1 0 ) ) )
18		dfdec10	|- ; A B = ( ( ; 1 0 x. A ) + B )
19	18	oveq1i	|- ( ; A B + ( C / ; 1 0 ) ) = ( ( ( ; 1 0 x. A ) + B ) + ( C / ; 1 0 ) )
20		df-dp2	|- _ B C = ( B + ( C / ; 1 0 ) )
21	20	oveq2i	|- ( ( ; 1 0 x. A ) + _ B C ) = ( ( ; 1 0 x. A ) + ( B + ( C / ; 1 0 ) ) )
22	17 19 21	3eqtr4ri	|- ( ( ; 1 0 x. A ) + _ B C ) = ( ; A B + ( C / ; 1 0 ) )
23	1 2	deccl	|- ; A B e. NN0
24	23 3	dpval2	|- ( ; A B . C ) = ( ; A B + ( C / ; 1 0 ) )
25	22 24	eqtr4i	|- ( ( ; 1 0 x. A ) + _ B C ) = ( ; A B . C )
26	7 8 25	3eqtri	|- ( ( A . _ B C ) x. ; 1 0 ) = ( ; A B . C )