Theorem decmulnc

Description: The product of a numeral with a number (no carry). (Contributed by AV, 15-Jun-2021)

	Ref	Expression
Hypotheses	decmulnc.n	|- N e. NN0
	decmulnc.a	|- A e. NN0
	decmulnc.b	|- B e. NN0
Assertion	decmulnc	|- ( N x. ; A B ) = ; ( N x. A ) ( N x. B )

Proof

Step	Hyp	Ref	Expression
1		decmulnc.n	|- N e. NN0
2		decmulnc.a	|- A e. NN0
3		decmulnc.b	|- B e. NN0
4		eqid	|- ; A B = ; A B
5	1 3	nn0mulcli	|- ( N x. B ) e. NN0
6		0nn0	|- 0 e. NN0
7	1 2	nn0mulcli	|- ( N x. A ) e. NN0
8	7	nn0cni	|- ( N x. A ) e. CC
9	8	addid1i	|- ( ( N x. A ) + 0 ) = ( N x. A )
10	5	dec0h	|- ( N x. B ) = ; 0 ( N x. B )
11	1 2 3 4 5 6 9 10	decmul2c	|- ( N x. ; A B ) = ; ( N x. A ) ( N x. B )