Theorem decmac

Description: Perform a multiply-add of two numerals M and N against a fixed multiplicand P (with carry). (Contributed by Mario Carneiro, 18-Feb-2014) (Revised by AV, 6-Sep-2021)

	Ref	Expression
Hypotheses	decma.a	|- A e. NN0
	decma.b	|- B e. NN0
	decma.c	|- C e. NN0
	decma.d	|- D e. NN0
	decma.m	|- M = ; A B
	decma.n	|- N = ; C D
	decmac.p	|- P e. NN0
	decmac.f	|- F e. NN0
	decmac.g	|- G e. NN0
	decmac.e	|- ( ( A x. P ) + ( C + G ) ) = E
	decmac.2	|- ( ( B x. P ) + D ) = ; G F
Assertion	decmac	|- ( ( M x. P ) + N ) = ; E F

Proof

Step	Hyp	Ref	Expression
1		decma.a	|- A e. NN0
2		decma.b	|- B e. NN0
3		decma.c	|- C e. NN0
4		decma.d	|- D e. NN0
5		decma.m	|- M = ; A B
6		decma.n	|- N = ; C D
7		decmac.p	|- P e. NN0
8		decmac.f	|- F e. NN0
9		decmac.g	|- G e. NN0
10		decmac.e	|- ( ( A x. P ) + ( C + G ) ) = E
11		decmac.2	|- ( ( B x. P ) + D ) = ; G F
12		10nn0	|- ; 1 0 e. NN0
13		dfdec10	|- ; A B = ( ( ; 1 0 x. A ) + B )
14	5 13	eqtri	|- M = ( ( ; 1 0 x. A ) + B )
15		dfdec10	|- ; C D = ( ( ; 1 0 x. C ) + D )
16	6 15	eqtri	|- N = ( ( ; 1 0 x. C ) + D )
17		dfdec10	|- ; G F = ( ( ; 1 0 x. G ) + F )
18	11 17	eqtri	|- ( ( B x. P ) + D ) = ( ( ; 1 0 x. G ) + F )
19	12 1 2 3 4 14 16 7 8 9 10 18	nummac	|- ( ( M x. P ) + N ) = ( ( ; 1 0 x. E ) + F )
20		dfdec10	|- ; E F = ( ( ; 1 0 x. E ) + F )
21	19 20	eqtr4i	|- ( ( M x. P ) + N ) = ; E F