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\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$$
	decpmulnc.3	$$⊢BD=G$$
Assertion	decpmulnc	Could not format assertion : No typesetting found for |- ( ; A B x. ; C D ) = ; ; E F G 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		decpmulnc.3	$$⊢BD=G$$
8	1 2	deccl	Could not format ; A B e. NN0 : No typesetting found for |- ; A B e. NN0 with typecode |-
9		eqid	Could not format ; C D = ; C D : No typesetting found for |- ; C D = ; C D with typecode |-
10	2 4	nn0mulcli	$$⊢BD\in {\mathbb{N}}_0$$
11	7 10	eqeltrri	$$⊢G\in {\mathbb{N}}_0$$
12	1 4	nn0mulcli	$$⊢AD\in {\mathbb{N}}_0$$
13		eqid	Could not format ; A B = ; A B : No typesetting found for |- ; A B = ; A B with typecode |-
14	12	nn0cni	$$⊢AD\in ℂ$$
15	2 3	nn0mulcli	$$⊢BC\in {\mathbb{N}}_0$$
16	15	nn0cni	$$⊢BC\in ℂ$$
17	14 16 6	addcomli	$$⊢BC+AD=F$$
18	1 2 12 13 3 5 17	decrmanc	Could not format ( ( ; A B x. C ) + ( A x. D ) ) = ; E F : No typesetting found for |- ( ( ; A B x. C ) + ( A x. D ) ) = ; E F with typecode |-
19		eqid	$$⊢AD=AD$$
20	4 1 2 13 19 7	decmul1	Could not format ( ; A B x. D ) = ; ( A x. D ) G : No typesetting found for |- ( ; A B x. D ) = ; ( A x. D ) G with typecode |-
21	8 3 4 9 11 12 18 20	decmul2c	Could not format ( ; A B x. ; C D ) = ; ; E F G : No typesetting found for |- ( ; A B x. ; C D ) = ; ; E F G with typecode |-