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\in {\mathbb{N}}_0$$
	dp3mul10.b	$$⊢B\in {\mathbb{N}}_0$$
	dp3mul10.c	$$⊢C\in ℝ$$
Assertion	dp3mul10	Could not format assertion : No typesetting found for |- ( ( A . _ B C ) x. ; 1 0 ) = ( ; A B . C ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		dp3mul10.a	$$⊢A\in {\mathbb{N}}_0$$
2		dp3mul10.b	$$⊢B\in {\mathbb{N}}_0$$
3		dp3mul10.c	$$⊢C\in ℝ$$
4	2	nn0rei	$$⊢B\in ℝ$$
5		dp2cl	Could not format ( ( B e. RR /\ C e. RR ) -> _ B C e. RR ) : No typesetting found for |- ( ( B e. RR /\ C e. RR ) -> _ B C e. RR ) with typecode |-
6	4 3 5	mp2an	Could not format _ B C e. RR : No typesetting found for |- _ B C e. RR with typecode |-
7	1 6	dpmul10	Could not format ( ( A . _ B C ) x. ; 1 0 ) = ; A _ B C : No typesetting found for |- ( ( A . _ B C ) x. ; 1 0 ) = ; A _ B C with typecode |-
8		dfdec10	Could not format ; A _ B C = ( ( ; 1 0 x. A ) + _ B C ) : No typesetting found for |- ; A _ B C = ( ( ; 1 0 x. A ) + _ B C ) with typecode |-
9		10nn	$$⊢10\in \mathbb{N}$$
10	9	nncni	$$⊢10\in ℂ$$
11	1	nn0cni	$$⊢A\in ℂ$$
12	10 11	mulcli	$$⊢10A\in ℂ$$
13	4	recni	$$⊢B\in ℂ$$
14	3	recni	$$⊢C\in ℂ$$
15	9	nnne0i	$$⊢10\ne 0$$
16	14 10 15	divcli	$$⊢\frac{C}{10}\in ℂ$$
17	12 13 16	addassi	$$⊢10A+B+\left(\frac{C}{10}\right)=10A+B+\left(\frac{C}{10}\right)$$
18		dfdec10	Could not format ; A B = ( ( ; 1 0 x. A ) + B ) : No typesetting found for |- ; A B = ( ( ; 1 0 x. A ) + B ) with typecode |-
19	18	oveq1i	Could not format ( ; A B + ( C / ; 1 0 ) ) = ( ( ( ; 1 0 x. A ) + B ) + ( C / ; 1 0 ) ) : No typesetting found for |- ( ; A B + ( C / ; 1 0 ) ) = ( ( ( ; 1 0 x. A ) + B ) + ( C / ; 1 0 ) ) with typecode |-
20		df-dp2	Could not format _ B C = ( B + ( C / ; 1 0 ) ) : No typesetting found for |- _ B C = ( B + ( C / ; 1 0 ) ) with typecode |-
21	20	oveq2i	Could not format ( ( ; 1 0 x. A ) + _ B C ) = ( ( ; 1 0 x. A ) + ( B + ( C / ; 1 0 ) ) ) : No typesetting found for |- ( ( ; 1 0 x. A ) + _ B C ) = ( ( ; 1 0 x. A ) + ( B + ( C / ; 1 0 ) ) ) with typecode |-
22	17 19 21	3eqtr4ri	Could not format ( ( ; 1 0 x. A ) + _ B C ) = ( ; A B + ( C / ; 1 0 ) ) : No typesetting found for |- ( ( ; 1 0 x. A ) + _ B C ) = ( ; A B + ( C / ; 1 0 ) ) with typecode |-
23	1 2	deccl	Could not format ; A B e. NN0 : No typesetting found for |- ; A B e. NN0 with typecode |-
24	23 3	dpval2	Could not format ( ; A B . C ) = ( ; A B + ( C / ; 1 0 ) ) : No typesetting found for |- ( ; A B . C ) = ( ; A B + ( C / ; 1 0 ) ) with typecode |-
25	22 24	eqtr4i	Could not format ( ( ; 1 0 x. A ) + _ B C ) = ( ; A B . C ) : No typesetting found for |- ( ( ; 1 0 x. A ) + _ B C ) = ( ; A B . C ) with typecode |-
26	7 8 25	3eqtri	Could not format ( ( A . _ B C ) x. ; 1 0 ) = ( ; A B . C ) : No typesetting found for |- ( ( A . _ B C ) x. ; 1 0 ) = ( ; A B . C ) with typecode |-