Theorem decmul1c

Description: The product of a numeral with a number (with carry). (Contributed by Mario Carneiro, 18-Feb-2014) (Revised by AV, 6-Sep-2021)

	Ref	Expression
Hypotheses	decmul1.p	|- P e. NN0
	decmul1.a	|- A e. NN0
	decmul1.b	|- B e. NN0
	decmul1.n	|- N = ; A B
	decmul1.0	|- D e. NN0
	decmul1c.e	|- E e. NN0
	decmul1c.c	|- ( ( A x. P ) + E ) = C
	decmul1c.2	|- ( B x. P ) = ; E D
Assertion	decmul1c	|- ( N x. P ) = ; C D

Proof

Step	Hyp	Ref	Expression
1		decmul1.p	|- P e. NN0
2		decmul1.a	|- A e. NN0
3		decmul1.b	|- B e. NN0
4		decmul1.n	|- N = ; A B
5		decmul1.0	|- D e. NN0
6		decmul1c.e	|- E e. NN0
7		decmul1c.c	|- ( ( A x. P ) + E ) = C
8		decmul1c.2	|- ( B x. P ) = ; E D
9		10nn0	|- ; 1 0 e. NN0
10		dfdec10	|- ; A B = ( ( ; 1 0 x. A ) + B )
11	4 10	eqtri	|- N = ( ( ; 1 0 x. A ) + B )
12		dfdec10	|- ; E D = ( ( ; 1 0 x. E ) + D )
13	8 12	eqtri	|- ( B x. P ) = ( ( ; 1 0 x. E ) + D )
14	9 1 2 3 11 5 6 7 13	nummul1c	|- ( N x. P ) = ( ( ; 1 0 x. C ) + D )
15		dfdec10	|- ; C D = ( ( ; 1 0 x. C ) + D )
16	14 15	eqtr4i	|- ( N x. P ) = ; C D