Theorem dpmul10

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

	Ref	Expression
Hypotheses	dpval2.a	$$⊢A\in {\mathbb{N}}_0$$
	dpval2.b	$$⊢B\in ℝ$$
Assertion	dpmul10	Could not format assertion : No typesetting found for |- ( ( A . B ) x. ; 1 0 ) = ; A B with typecode |-

Proof

Step	Hyp	Ref	Expression
1		dpval2.a	$$⊢A\in {\mathbb{N}}_0$$
2		dpval2.b	$$⊢B\in ℝ$$
3	2	recni	$$⊢B\in ℂ$$
4		10nn	$$⊢10\in \mathbb{N}$$
5	4	nncni	$$⊢10\in ℂ$$
6	4	nnne0i	$$⊢10\ne 0$$
7	3 5 6	divcan2i	$$⊢10\left(\frac{B}{10}\right)=B$$
8	7	oveq2i	$$⊢10A+10\left(\frac{B}{10}\right)=10A+B$$
9	1 2	dpval2	$$⊢A.B=A+\left(\frac{B}{10}\right)$$
10	9	oveq2i	$$⊢10\left(A.B\right)=10\left(A+\left(\frac{B}{10}\right)\right)$$
11		dpcl	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in ℝ\right)\to A.B\in ℝ$$
12	1 2 11	mp2an	$$⊢A.B\in ℝ$$
13	12	recni	$$⊢A.B\in ℂ$$
14	5 13	mulcomi	$$⊢10\left(A.B\right)=\left(A.B\right)\cdot 10$$
15	1	nn0cni	$$⊢A\in ℂ$$
16	3 5 6	divcli	$$⊢\frac{B}{10}\in ℂ$$
17	5 15 16	adddii	$$⊢10\left(A+\left(\frac{B}{10}\right)\right)=10A+10\left(\frac{B}{10}\right)$$
18	10 14 17	3eqtr3i	$$⊢\left(A.B\right)\cdot 10=10A+10\left(\frac{B}{10}\right)$$
19		dfdec10	Could not format ; A B = ( ( ; 1 0 x. A ) + B ) : No typesetting found for |- ; A B = ( ( ; 1 0 x. A ) + B ) with typecode |-
20	8 18 19	3eqtr4i	Could not format ( ( A . B ) x. ; 1 0 ) = ; A B : No typesetting found for |- ( ( A . B ) x. ; 1 0 ) = ; A B with typecode |-