Theorem decmul1

Description: The product of a numeral with a number (no carry). (Contributed by AV, 22-Jul-2021) (Revised by AV, 6-Sep-2021) Remove hypothesis D e. NN0 . (Revised by Steven Nguyen, 7-Dec-2022)

	Ref	Expression
Hypotheses	decmul1.p	|- P e. NN0
	decmul1.a	|- A e. NN0
	decmul1.b	|- B e. NN0
	decmul1.n	|- N = ; A B
	decmul1.c	|- ( A x. P ) = C
	decmul1.d	|- ( B x. P ) = D
Assertion	decmul1	|- ( 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.c	|- ( A x. P ) = C
6		decmul1.d	|- ( B x. P ) = D
7	2 3	deccl	|- ; A B e. NN0
8	4 7	eqeltri	|- N e. NN0
9	8 1	num0u	|- ( N x. P ) = ( ( N x. P ) + 0 )
10		0nn0	|- 0 e. NN0
11	3 1	nn0mulcli	|- ( B x. P ) e. NN0
12	11	nn0cni	|- ( B x. P ) e. CC
13	12	addid1i	|- ( ( B x. P ) + 0 ) = ( B x. P )
14	13 6	eqtri	|- ( ( B x. P ) + 0 ) = D
15	2 3 10 4 1 5 14	decrmanc	|- ( ( N x. P ) + 0 ) = ; C D
16	9 15	eqtri	|- ( N x. P ) = ; C D