Theorem decrmac

Description: Perform a multiply-add of two numerals M and N against a fixed multiplicand P (with carry). (Contributed by AV, 16-Sep-2021)

	Ref	Expression
Hypotheses	decrmanc.a	|- A e. NN0
	decrmanc.b	|- B e. NN0
	decrmanc.n	|- N e. NN0
	decrmanc.m	|- M = ; A B
	decrmanc.p	|- P e. NN0
	decrmac.f	|- F e. NN0
	decrmac.g	|- G e. NN0
	decrmac.e	|- ( ( A x. P ) + G ) = E
	decrmac.2	|- ( ( B x. P ) + N ) = ; G F
Assertion	decrmac	|- ( ( M x. P ) + N ) = ; E F

Proof

Step	Hyp	Ref	Expression
1		decrmanc.a	|- A e. NN0
2		decrmanc.b	|- B e. NN0
3		decrmanc.n	|- N e. NN0
4		decrmanc.m	|- M = ; A B
5		decrmanc.p	|- P e. NN0
6		decrmac.f	|- F e. NN0
7		decrmac.g	|- G e. NN0
8		decrmac.e	|- ( ( A x. P ) + G ) = E
9		decrmac.2	|- ( ( B x. P ) + N ) = ; G F
10		0nn0	|- 0 e. NN0
11	3	dec0h	|- N = ; 0 N
12	7	nn0cni	|- G e. CC
13	12	addlidi	|- ( 0 + G ) = G
14	13	oveq2i	|- ( ( A x. P ) + ( 0 + G ) ) = ( ( A x. P ) + G )
15	14 8	eqtri	|- ( ( A x. P ) + ( 0 + G ) ) = E
16	1 2 10 3 4 11 5 6 7 15 9	decmac	|- ( ( M x. P ) + N ) = ; E F