Theorem decpmul

Description: Partial products algorithm for two digit multiplication. (Contributed by Steven Nguyen, 10-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
	decpmul.3	|- ( B x. D ) = ; G H
	decpmul.4	|- ( ; E G + F ) = I
	decpmul.g	|- G e. NN0
	decpmul.h	|- H e. NN0
Assertion	decpmul	|- ( ; A B x. ; C D ) = ; I H

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		decpmul.3	|- ( B x. D ) = ; G H
8		decpmul.4	|- ( ; E G + F ) = I
9		decpmul.g	|- G e. NN0
10		decpmul.h	|- H e. NN0
11	1 2 3 4 5 6 7	decpmulnc	|- ( ; A B x. ; C D ) = ; ; E F ; G H
12		dfdec10	|- ; ; E F ; G H = ( ( ; 1 0 x. ; E F ) + ; G H )
13	1 3	nn0mulcli	|- ( A x. C ) e. NN0
14	5 13	eqeltrri	|- E e. NN0
15	2 3	nn0mulcli	|- ( B x. C ) e. NN0
16	1 4 15	numcl	|- ( ( A x. D ) + ( B x. C ) ) e. NN0
17	6 16	eqeltrri	|- F e. NN0
18	14 17	deccl	|- ; E F e. NN0
19		0nn0	|- 0 e. NN0
20	18	dec0u	|- ( ; 1 0 x. ; E F ) = ; ; E F 0
21		eqid	|- ; G H = ; G H
22	14 17 9	decaddcom	|- ( ; E F + G ) = ( ; E G + F )
23	22 8	eqtri	|- ( ; E F + G ) = I
24	10	nn0cni	|- H e. CC
25	24	addid2i	|- ( 0 + H ) = H
26	18 19 9 10 20 21 23 25	decadd	|- ( ( ; 1 0 x. ; E F ) + ; G H ) = ; I H
27	11 12 26	3eqtri	|- ( ; A B x. ; C D ) = ; I H