Theorem numma

Description: Perform a multiply-add of two decimal integers M and N against a fixed multiplicand P (no 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$$
	numma.8	$$⊢P\in {\mathbb{N}}_0$$
	numma.9	$$⊢AP+C=E$$
	numma.10	$$⊢BP+D=F$$
Assertion	numma	$$⊢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		numma.8	$$⊢P\in {\mathbb{N}}_0$$
9		numma.9	$$⊢AP+C=E$$
10		numma.10	$$⊢BP+D=F$$
11	6	oveq1i	$$⊢MP=\left(TA+B\right)P$$
12	11 7	oveq12i	$$⊢MP+N=\left(TA+B\right)P+TC+D$$
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	13 16 17	adddii	$$⊢T\left(AP+C\right)=TAP+TC$$
19	13 14 15	mulassi	$$⊢TAP=TAP$$
20	19	oveq1i	$$⊢TAP+TC=TAP+TC$$
21	18 20	eqtr4i	$$⊢T\left(AP+C\right)=TAP+TC$$
22	21	oveq1i	$$⊢T\left(AP+C\right)+BP+D=TAP+TC+BP+D$$
23	13 14	mulcli	$$⊢TA\in ℂ$$
24	3	nn0cni	$$⊢B\in ℂ$$
25	23 24 15	adddiri	$$⊢\left(TA+B\right)P=TAP+BP$$
26	25	oveq1i	$$⊢\left(TA+B\right)P+TC+D=TAP+BP+TC+D$$
27	23 15	mulcli	$$⊢TAP\in ℂ$$
28	13 17	mulcli	$$⊢TC\in ℂ$$
29	24 15	mulcli	$$⊢BP\in ℂ$$
30	5	nn0cni	$$⊢D\in ℂ$$
31	27 28 29 30	add4i	$$⊢TAP+TC+BP+D=TAP+BP+TC+D$$
32	26 31	eqtr4i	$$⊢\left(TA+B\right)P+TC+D=TAP+TC+BP+D$$
33	22 32	eqtr4i	$$⊢T\left(AP+C\right)+BP+D=\left(TA+B\right)P+TC+D$$
34	9	oveq2i	$$⊢T\left(AP+C\right)=TE$$
35	34 10	oveq12i	$$⊢T\left(AP+C\right)+BP+D=TE+F$$
36	12 33 35	3eqtr2i	$$⊢MP+N=TE+F$$