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 ℕ_{0}$
	numma.2	$⊢ A \in ℕ_{0}$
	numma.3	$⊢ B \in ℕ_{0}$
	numma.4	$⊢ C \in ℕ_{0}$
	numma.5	$⊢ D \in ℕ_{0}$
	numma.6	$⊢ M = T A + B$
	numma.7	$⊢ N = T C + D$
	numma2c.8	$⊢ P \in ℕ_{0}$
	numma2c.9	$⊢ F \in ℕ_{0}$
	numma2c.10	$⊢ G \in ℕ_{0}$
	numma2c.11	$⊢ P A + C + G = E$
	numma2c.12	$⊢ P B + D = T G + F$
Assertion	numma2c	$⊢ P \cdot M + N = T E + F$

Proof

Step	Hyp	Ref	Expression
1		numma.1	$⊢ T \in ℕ_{0}$
2		numma.2	$⊢ A \in ℕ_{0}$
3		numma.3	$⊢ B \in ℕ_{0}$
4		numma.4	$⊢ C \in ℕ_{0}$
5		numma.5	$⊢ D \in ℕ_{0}$
6		numma.6	$⊢ M = T A + B$
7		numma.7	$⊢ N = T C + D$
8		numma2c.8	$⊢ P \in ℕ_{0}$
9		numma2c.9	$⊢ F \in ℕ_{0}$
10		numma2c.10	$⊢ G \in ℕ_{0}$
11		numma2c.11	$⊢ P A + C + G = E$
12		numma2c.12	$⊢ P B + D = T G + F$
13	8	nn0cni	$⊢ P \in ℂ$
14	1 2 3	numcl	$⊢ T A + B \in ℕ_{0}$
15	6 14	eqeltri	$⊢ M \in ℕ_{0}$
16	15	nn0cni	$⊢ M \in ℂ$
17	13 16	mulcomi	$⊢ P \cdot M = M P$
18	17	oveq1i	$⊢ P \cdot M + N = M P + N$
19	2	nn0cni	$⊢ A \in ℂ$
20	19 13	mulcomi	$⊢ A P = P A$
21	20	oveq1i	$⊢ A P + C + G = P A + C + G$
22	21 11	eqtri	$⊢ A P + C + G = E$
23	3	nn0cni	$⊢ B \in ℂ$
24	23 13	mulcomi	$⊢ B P = P B$
25	24	oveq1i	$⊢ B P + D = P B + D$
26	25 12	eqtri	$⊢ B P + D = T G + F$
27	1 2 3 4 5 6 7 8 9 10 22 26	nummac	$⊢ M P + N = T E + F$
28	18 27	eqtri	$⊢ P \cdot M + N = T E + F$

Metamath Proof Explorer

Theorem numma2c

Proof