Theorem decpmulnc

Description: Partial products algorithm for two digit multiplication, no carry. Compare muladdi . (Contributed by Steven Nguyen, 9-Dec-2022)

	Ref	Expression
Hypotheses	decpmulnc.a	|- A e. NN0
	decpmulnc.b	|- B e. NN0
	decpmulnc.c	|- C e. NN0
	decpmulnc.d	|- D e. NN0
	decpmulnc.1	|- ( A x. C ) = E
	decpmulnc.2	|- ( ( A x. D ) + ( B x. C ) ) = F
	decpmulnc.3	|- ( B x. D ) = G
Assertion	decpmulnc	|- ( ; A B x. ; C D ) = ; ; E F G

Proof

Step	Hyp	Ref	Expression
1		decpmulnc.a	|- A e. NN0
2		decpmulnc.b	|- B e. NN0
3		decpmulnc.c	|- C e. NN0
4		decpmulnc.d	|- D e. NN0
5		decpmulnc.1	|- ( A x. C ) = E
6		decpmulnc.2	|- ( ( A x. D ) + ( B x. C ) ) = F
7		decpmulnc.3	|- ( B x. D ) = G
8	1 2	deccl	|- ; A B e. NN0
9		eqid	|- ; C D = ; C D
10	2 4	nn0mulcli	|- ( B x. D ) e. NN0
11	7 10	eqeltrri	|- G e. NN0
12	1 4	nn0mulcli	|- ( A x. D ) e. NN0
13		eqid	|- ; A B = ; A B
14	12	nn0cni	|- ( A x. D ) e. CC
15	2 3	nn0mulcli	|- ( B x. C ) e. NN0
16	15	nn0cni	|- ( B x. C ) e. CC
17	14 16 6	addcomli	|- ( ( B x. C ) + ( A x. D ) ) = F
18	1 2 12 13 3 5 17	decrmanc	|- ( ( ; A B x. C ) + ( A x. D ) ) = ; E F
19		eqid	|- ( A x. D ) = ( A x. D )
20	4 1 2 13 19 7	decmul1	|- ( ; A B x. D ) = ; ( A x. D ) G
21	8 3 4 9 11 12 18 20	decmul2c	|- ( ; A B x. ; C D ) = ; ; E F G