Theorem decmul10add

Description: A multiplication of a number and a numeral expressed as addition with first summand as multiple of 10. (Contributed by AV, 22-Jul-2021) (Revised by AV, 6-Sep-2021)

	Ref	Expression
Hypotheses	decmul10add.1	|- A e. NN0
	decmul10add.2	|- B e. NN0
	decmul10add.3	|- M e. NN0
	decmul10add.4	|- E = ( M x. A )
	decmul10add.5	|- F = ( M x. B )
Assertion	decmul10add	|- ( M x. ; A B ) = ( ; E 0 + F )

Proof

Step	Hyp	Ref	Expression
1		decmul10add.1	|- A e. NN0
2		decmul10add.2	|- B e. NN0
3		decmul10add.3	|- M e. NN0
4		decmul10add.4	|- E = ( M x. A )
5		decmul10add.5	|- F = ( M x. B )
6		dfdec10	|- ; A B = ( ( ; 1 0 x. A ) + B )
7	6	oveq2i	|- ( M x. ; A B ) = ( M x. ( ( ; 1 0 x. A ) + B ) )
8	3	nn0cni	|- M e. CC
9		10nn0	|- ; 1 0 e. NN0
10	9 1	nn0mulcli	|- ( ; 1 0 x. A ) e. NN0
11	10	nn0cni	|- ( ; 1 0 x. A ) e. CC
12	2	nn0cni	|- B e. CC
13	8 11 12	adddii	|- ( M x. ( ( ; 1 0 x. A ) + B ) ) = ( ( M x. ( ; 1 0 x. A ) ) + ( M x. B ) )
14	9	nn0cni	|- ; 1 0 e. CC
15	1	nn0cni	|- A e. CC
16	8 14 15	mul12i	|- ( M x. ( ; 1 0 x. A ) ) = ( ; 1 0 x. ( M x. A ) )
17	3 1	nn0mulcli	|- ( M x. A ) e. NN0
18	17	dec0u	|- ( ; 1 0 x. ( M x. A ) ) = ; ( M x. A ) 0
19	4	eqcomi	|- ( M x. A ) = E
20	19	deceq1i	|- ; ( M x. A ) 0 = ; E 0
21	16 18 20	3eqtri	|- ( M x. ( ; 1 0 x. A ) ) = ; E 0
22	5	eqcomi	|- ( M x. B ) = F
23	21 22	oveq12i	|- ( ( M x. ( ; 1 0 x. A ) ) + ( M x. B ) ) = ( ; E 0 + F )
24	7 13 23	3eqtri	|- ( M x. ; A B ) = ( ; E 0 + F )