Theorem numma2c

Description: Perform a multiply-add of two decimal integers M and N against a fixed multiplicand P (with carry). (Contributed by Mario Carneiro, 18-Feb-2014)

	Ref	Expression
Hypotheses	numma.1	$$⊢T\in {\mathbb{N}}_0$$
	numma.2	$$⊢A\in {\mathbb{N}}_0$$
	numma.3	$$⊢B\in {\mathbb{N}}_0$$
	numma.4	$$⊢C\in {\mathbb{N}}_0$$
	numma.5	$$⊢D\in {\mathbb{N}}_0$$
	numma.6	$$⊢M=TA+B$$
	numma.7	$$⊢N=TC+D$$
	numma2c.8	$$⊢P\in {\mathbb{N}}_0$$
	numma2c.9	$$⊢F\in {\mathbb{N}}_0$$
	numma2c.10	$$⊢G\in {\mathbb{N}}_0$$
	numma2c.11	$$⊢PA+C+G=E$$
	numma2c.12	$$⊢PB+D=TG+F$$
Assertion	numma2c	$$⊢P\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}+N=TE+F$$

Proof

Step	Hyp	Ref	Expression
1		numma.1	$$⊢T\in {\mathbb{N}}_0$$
2		numma.2	$$⊢A\in {\mathbb{N}}_0$$
3		numma.3	$$⊢B\in {\mathbb{N}}_0$$
4		numma.4	$$⊢C\in {\mathbb{N}}_0$$
5		numma.5	$$⊢D\in {\mathbb{N}}_0$$
6		numma.6	$$⊢M=TA+B$$
7		numma.7	$$⊢N=TC+D$$
8		numma2c.8	$$⊢P\in {\mathbb{N}}_0$$
9		numma2c.9	$$⊢F\in {\mathbb{N}}_0$$
10		numma2c.10	$$⊢G\in {\mathbb{N}}_0$$
11		numma2c.11	$$⊢PA+C+G=E$$
12		numma2c.12	$$⊢PB+D=TG+F$$
13	8	nn0cni	$$⊢P\in ℂ$$
14	1 2 3	numcl	$$⊢TA+B\in {\mathbb{N}}_0$$
15	6 14	eqeltri	$$⊢M\in {\mathbb{N}}_0$$
16	15	nn0cni	$$⊢M\in ℂ$$
17	13 16	mulcomi	$$⊢P\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=MP$$
18	17	oveq1i	$$⊢P\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}+N=MP+N$$
19	2	nn0cni	$$⊢A\in ℂ$$
20	19 13	mulcomi	$$⊢AP=PA$$
21	20	oveq1i	$$⊢AP+C+G=PA+C+G$$
22	21 11	eqtri	$$⊢AP+C+G=E$$
23	3	nn0cni	$$⊢B\in ℂ$$
24	23 13	mulcomi	$$⊢BP=PB$$
25	24	oveq1i	$$⊢BP+D=PB+D$$
26	25 12	eqtri	$$⊢BP+D=TG+F$$
27	1 2 3 4 5 6 7 8 9 10 22 26	nummac	$$⊢MP+N=TE+F$$
28	18 27	eqtri	$$⊢P\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}+N=TE+F$$