Theorem decrmanc

Description: Perform a multiply-add of two numerals M and N against a fixed multiplicand P (no 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
	decrmanc.e	|- ( A x. P ) = E
	decrmanc.f	|- ( ( B x. P ) + N ) = F
Assertion	decrmanc	|- ( ( 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		decrmanc.e	|- ( A x. P ) = E
7		decrmanc.f	|- ( ( B x. P ) + N ) = F
8		0nn0	|- 0 e. NN0
9	3	dec0h	|- N = ; 0 N
10	1 5	nn0mulcli	|- ( A x. P ) e. NN0
11	10	nn0cni	|- ( A x. P ) e. CC
12	11	addridi	|- ( ( A x. P ) + 0 ) = ( A x. P )
13	12 6	eqtri	|- ( ( A x. P ) + 0 ) = E
14	1 2 8 3 4 9 5 13 7	decma	|- ( ( M x. P ) + N ) = ; E F