Theorem nummac

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$$
	nummac.8	$$⊢P\in {\mathbb{N}}_0$$
	nummac.9	$$⊢F\in {\mathbb{N}}_0$$
	nummac.10	$$⊢G\in {\mathbb{N}}_0$$
	nummac.11	$$⊢AP+C+G=E$$
	nummac.12	$$⊢BP+D=TG+F$$
Assertion	nummac	$$⊢MP+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		nummac.8	$$⊢P\in {\mathbb{N}}_0$$
9		nummac.9	$$⊢F\in {\mathbb{N}}_0$$
10		nummac.10	$$⊢G\in {\mathbb{N}}_0$$
11		nummac.11	$$⊢AP+C+G=E$$
12		nummac.12	$$⊢BP+D=TG+F$$
13	1	nn0cni	$$⊢T\in ℂ$$
14	2	nn0cni	$$⊢A\in ℂ$$
15	8	nn0cni	$$⊢P\in ℂ$$
16	14 15	mulcli	$$⊢AP\in ℂ$$
17	4	nn0cni	$$⊢C\in ℂ$$
18	10	nn0cni	$$⊢G\in ℂ$$
19	16 17 18	addassi	$$⊢AP+C+G=AP+C+G$$
20	19 11	eqtri	$$⊢AP+C+G=E$$
21	16 17	addcli	$$⊢AP+C\in ℂ$$
22	21 18	addcli	$$⊢AP+C+G\in ℂ$$
23	20 22	eqeltrri	$$⊢E\in ℂ$$
24	13 23 18	subdii	$$⊢T\left(E-G\right)=TE-TG$$
25	24	oveq1i	$$⊢T\left(E-G\right)+TG+F=\left(TE-TG\right)+TG+F$$
26	23 18 21	subadd2i	$$⊢E-G=AP+C\leftrightarrow AP+C+G=E$$
27	20 26	mpbir	$$⊢E-G=AP+C$$
28	27	eqcomi	$$⊢AP+C=E-G$$
29	1 2 3 4 5 6 7 8 28 12	numma	$$⊢MP+N=T\left(E-G\right)+TG+F$$
30	13 23	mulcli	$$⊢TE\in ℂ$$
31	13 18	mulcli	$$⊢TG\in ℂ$$
32		npcan	$$⊢\left(TE\in ℂ\wedge TG\in ℂ\right)\to TE-TG+TG=TE$$
33	30 31 32	mp2an	$$⊢TE-TG+TG=TE$$
34	33	oveq1i	$$⊢\left(TE-TG\right)+TG+F=TE+F$$
35	30 31	subcli	$$⊢TE-TG\in ℂ$$
36	9	nn0cni	$$⊢F\in ℂ$$
37	35 31 36	addassi	$$⊢\left(TE-TG\right)+TG+F=\left(TE-TG\right)+TG+F$$
38	34 37	eqtr3i	$$⊢TE+F=\left(TE-TG\right)+TG+F$$
39	25 29 38	3eqtr4i	$$⊢MP+N=TE+F$$