decma2c

Description: Perform a multiply-add of two numerals M and N against a fixed multiplier 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
	decma2c.p	\|- P e. NN0
	decma2c.f	\|- F e. NN0
	decma2c.g	\|- G e. NN0
	decma2c.e	\|- ( ( P x. A ) + ( C + G ) ) = E
	decma2c.2	\|- ( ( P x. B ) + D ) = ; G F
Assertion	decma2c	\|- ( ( P x. M ) + 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		decma2c.p	\|- P e. NN0
8		decma2c.f	\|- F e. NN0
9		decma2c.g	\|- G e. NN0
10		decma2c.e	\|- ( ( P x. A ) + ( C + G ) ) = E
11		decma2c.2	\|- ( ( P x. B ) + 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	\|- ( ( P x. B ) + D ) = ( ( ; 1 0 x. G ) + F )
19	12 1 2 3 4 14 16 7 8 9 10 18	numma2c	\|- ( ( P x. M ) + N ) = ( ( ; 1 0 x. E ) + F )
20		dfdec10	\|- ; E F = ( ( ; 1 0 x. E ) + F )
21	19 20	eqtr4i	\|- ( ( P x. M ) + N ) = ; E F

Metamath Proof Explorer

Theorem decma2c

Proof