Theorem decpmul

Description: Partial products algorithm for two digit multiplication. (Contributed by Steven Nguyen, 10-Dec-2022)

	Ref	Expression
Hypotheses	decpmulnc.a	$$⊢A\in {\mathbb{N}}_0$$
	decpmulnc.b	$$⊢B\in {\mathbb{N}}_0$$
	decpmulnc.c	$$⊢C\in {\mathbb{N}}_0$$
	decpmulnc.d	$$⊢D\in {\mathbb{N}}_0$$
	decpmulnc.1	$$⊢AC=E$$
	decpmulnc.2	$$⊢AD+BC=F$$
	decpmul.3	No typesetting found for |- ( B x. D ) = ; G H with typecode |-
	decpmul.4	No typesetting found for |- ( ; E G + F ) = I with typecode |-
	decpmul.g	$$⊢G\in {\mathbb{N}}_0$$
	decpmul.h	$$⊢H\in {\mathbb{N}}_0$$
Assertion	decpmul	Could not format assertion : No typesetting found for |- ( ; A B x. ; C D ) = ; I H with typecode |-

Proof

Step	Hyp	Ref	Expression
1		decpmulnc.a	$$⊢A\in {\mathbb{N}}_0$$
2		decpmulnc.b	$$⊢B\in {\mathbb{N}}_0$$
3		decpmulnc.c	$$⊢C\in {\mathbb{N}}_0$$
4		decpmulnc.d	$$⊢D\in {\mathbb{N}}_0$$
5		decpmulnc.1	$$⊢AC=E$$
6		decpmulnc.2	$$⊢AD+BC=F$$
7		decpmul.3	Could not format ( B x. D ) = ; G H : No typesetting found for |- ( B x. D ) = ; G H with typecode |-
8		decpmul.4	Could not format ( ; E G + F ) = I : No typesetting found for |- ( ; E G + F ) = I with typecode |-
9		decpmul.g	$$⊢G\in {\mathbb{N}}_0$$
10		decpmul.h	$$⊢H\in {\mathbb{N}}_0$$
11	1 2 3 4 5 6 7	decpmulnc	Could not format ( ; A B x. ; C D ) = ; ; E F ; G H : No typesetting found for |- ( ; A B x. ; C D ) = ; ; E F ; G H with typecode |-
12		dfdec10	Could not format ; ; E F ; G H = ( ( ; 1 0 x. ; E F ) + ; G H ) : No typesetting found for |- ; ; E F ; G H = ( ( ; 1 0 x. ; E F ) + ; G H ) with typecode |-
13	1 3	nn0mulcli	$$⊢AC\in {\mathbb{N}}_0$$
14	5 13	eqeltrri	$$⊢E\in {\mathbb{N}}_0$$
15	2 3	nn0mulcli	$$⊢BC\in {\mathbb{N}}_0$$
16	1 4 15	numcl	$$⊢AD+BC\in {\mathbb{N}}_0$$
17	6 16	eqeltrri	$$⊢F\in {\mathbb{N}}_0$$
18	14 17	deccl	Could not format ; E F e. NN0 : No typesetting found for |- ; E F e. NN0 with typecode |-
19		0nn0	$$⊢0\in {\mathbb{N}}_0$$
20	18	dec0u	Could not format ( ; 1 0 x. ; E F ) = ; ; E F 0 : No typesetting found for |- ( ; 1 0 x. ; E F ) = ; ; E F 0 with typecode |-
21		eqid	Could not format ; G H = ; G H : No typesetting found for |- ; G H = ; G H with typecode |-
22	14 17 9	decaddcom	Could not format ( ; E F + G ) = ( ; E G + F ) : No typesetting found for |- ( ; E F + G ) = ( ; E G + F ) with typecode |-
23	22 8	eqtri	Could not format ( ; E F + G ) = I : No typesetting found for |- ( ; E F + G ) = I with typecode |-
24	10	nn0cni	$$⊢H\in ℂ$$
25	24	addid2i	$$⊢0+H=H$$
26	18 19 9 10 20 21 23 25	decadd	Could not format ( ( ; 1 0 x. ; E F ) + ; G H ) = ; I H : No typesetting found for |- ( ( ; 1 0 x. ; E F ) + ; G H ) = ; I H with typecode |-
27	11 12 26	3eqtri	Could not format ( ; A B x. ; C D ) = ; I H : No typesetting found for |- ( ; A B x. ; C D ) = ; I H with typecode |-