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\in {\mathbb{N}}_0$$
	decmul10add.2	$$⊢B\in {\mathbb{N}}_0$$
	decmul10add.3	$$⊢M\in {\mathbb{N}}_0$$
	decmul10add.4	$$⊢E=MA$$
	decmul10add.5	$$⊢F=MB$$
Assertion	decmul10add	Could not format assertion : No typesetting found for |- ( M x. ; A B ) = ( ; E 0 + F ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		decmul10add.1	$$⊢A\in {\mathbb{N}}_0$$
2		decmul10add.2	$$⊢B\in {\mathbb{N}}_0$$
3		decmul10add.3	$$⊢M\in {\mathbb{N}}_0$$
4		decmul10add.4	$$⊢E=MA$$
5		decmul10add.5	$$⊢F=MB$$
6		dfdec10	Could not format ; A B = ( ( ; 1 0 x. A ) + B ) : No typesetting found for |- ; A B = ( ( ; 1 0 x. A ) + B ) with typecode |-
7	6	oveq2i	Could not format ( M x. ; A B ) = ( M x. ( ( ; 1 0 x. A ) + B ) ) : No typesetting found for |- ( M x. ; A B ) = ( M x. ( ( ; 1 0 x. A ) + B ) ) with typecode |-
8	3	nn0cni	$$⊢M\in ℂ$$
9		10nn0	$$⊢10\in {\mathbb{N}}_0$$
10	9 1	nn0mulcli	$$⊢10A\in {\mathbb{N}}_0$$
11	10	nn0cni	$$⊢10A\in ℂ$$
12	2	nn0cni	$$⊢B\in ℂ$$
13	8 11 12	adddii	$$⊢M\left(10A+B\right)=M10A+MB$$
14	9	nn0cni	$$⊢10\in ℂ$$
15	1	nn0cni	$$⊢A\in ℂ$$
16	8 14 15	mul12i	$$⊢M10A=10MA$$
17	3 1	nn0mulcli	$$⊢MA\in {\mathbb{N}}_0$$
18	17	dec0u	Could not format ( ; 1 0 x. ( M x. A ) ) = ; ( M x. A ) 0 : No typesetting found for |- ( ; 1 0 x. ( M x. A ) ) = ; ( M x. A ) 0 with typecode |-
19	4	eqcomi	$$⊢MA=E$$
20	19	deceq1i	Could not format ; ( M x. A ) 0 = ; E 0 : No typesetting found for |- ; ( M x. A ) 0 = ; E 0 with typecode |-
21	16 18 20	3eqtri	Could not format ( M x. ( ; 1 0 x. A ) ) = ; E 0 : No typesetting found for |- ( M x. ( ; 1 0 x. A ) ) = ; E 0 with typecode |-
22	5	eqcomi	$$⊢MB=F$$
23	21 22	oveq12i	Could not format ( ( M x. ( ; 1 0 x. A ) ) + ( M x. B ) ) = ( ; E 0 + F ) : No typesetting found for |- ( ( M x. ( ; 1 0 x. A ) ) + ( M x. B ) ) = ( ; E 0 + F ) with typecode |-
24	7 13 23	3eqtri	Could not format ( M x. ; A B ) = ( ; E 0 + F ) : No typesetting found for |- ( M x. ; A B ) = ( ; E 0 + F ) with typecode |-