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 e. NN0
	numma.2	|- A e. NN0
	numma.3	|- B e. NN0
	numma.4	|- C e. NN0
	numma.5	|- D e. NN0
	numma.6	|- M = ( ( T x. A ) + B )
	numma.7	|- N = ( ( T x. C ) + D )
	numma2c.8	|- P e. NN0
	numma2c.9	|- F e. NN0
	numma2c.10	|- G e. NN0
	numma2c.11	|- ( ( P x. A ) + ( C + G ) ) = E
	numma2c.12	|- ( ( P x. B ) + D ) = ( ( T x. G ) + F )
Assertion	numma2c	|- ( ( P x. M ) + N ) = ( ( T x. E ) + F )

Proof

Step	Hyp	Ref	Expression
1		numma.1	|- T e. NN0
2		numma.2	|- A e. NN0
3		numma.3	|- B e. NN0
4		numma.4	|- C e. NN0
5		numma.5	|- D e. NN0
6		numma.6	|- M = ( ( T x. A ) + B )
7		numma.7	|- N = ( ( T x. C ) + D )
8		numma2c.8	|- P e. NN0
9		numma2c.9	|- F e. NN0
10		numma2c.10	|- G e. NN0
11		numma2c.11	|- ( ( P x. A ) + ( C + G ) ) = E
12		numma2c.12	|- ( ( P x. B ) + D ) = ( ( T x. G ) + F )
13	8	nn0cni	|- P e. CC
14	1 2 3	numcl	|- ( ( T x. A ) + B ) e. NN0
15	6 14	eqeltri	|- M e. NN0
16	15	nn0cni	|- M e. CC
17	13 16	mulcomi	|- ( P x. M ) = ( M x. P )
18	17	oveq1i	|- ( ( P x. M ) + N ) = ( ( M x. P ) + N )
19	2	nn0cni	|- A e. CC
20	19 13	mulcomi	|- ( A x. P ) = ( P x. A )
21	20	oveq1i	|- ( ( A x. P ) + ( C + G ) ) = ( ( P x. A ) + ( C + G ) )
22	21 11	eqtri	|- ( ( A x. P ) + ( C + G ) ) = E
23	3	nn0cni	|- B e. CC
24	23 13	mulcomi	|- ( B x. P ) = ( P x. B )
25	24	oveq1i	|- ( ( B x. P ) + D ) = ( ( P x. B ) + D )
26	25 12	eqtri	|- ( ( B x. P ) + D ) = ( ( T x. G ) + F )
27	1 2 3 4 5 6 7 8 9 10 22 26	nummac	|- ( ( M x. P ) + N ) = ( ( T x. E ) + F )
28	18 27	eqtri	|- ( ( P x. M ) + N ) = ( ( T x. E ) + F )