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 ℕ_{0}$
	decpmulnc.b	$⊢ B \in ℕ_{0}$
	decpmulnc.c	$⊢ C \in ℕ_{0}$
	decpmulnc.d	$⊢ D \in ℕ_{0}$
	decpmulnc.1	$⊢ A C = E$
	decpmulnc.2	$⊢ A D + B C = F$
	decpmulnc.3	$⊢ B D = G$
Assertion	decpmulnc	Could not format assertion : No typesetting found for \|- ( ; A B x. ; C D ) = ; ; E F G with typecode \|-

Step	Hyp	Ref	Expression
1		decpmulnc.a	$⊢ A \in ℕ_{0}$
2		decpmulnc.b	$⊢ B \in ℕ_{0}$
3		decpmulnc.c	$⊢ C \in ℕ_{0}$
4		decpmulnc.d	$⊢ D \in ℕ_{0}$
5		decpmulnc.1	$⊢ A C = E$
6		decpmulnc.2	$⊢ A D + B C = F$
7		decpmulnc.3	$⊢ B D = 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	$⊢ B D \in ℕ_{0}$
11	7 10	eqeltrri	$⊢ G \in ℕ_{0}$
12	1 4	nn0mulcli	$⊢ A D \in ℕ_{0}$
13		eqid	Could not format ; A B = ; A B : No typesetting found for \|- ; A B = ; A B with typecode \|-
14	12	nn0cni	$⊢ A D \in ℂ$
15	2 3	nn0mulcli	$⊢ B C \in ℕ_{0}$
16	15	nn0cni	$⊢ B C \in ℂ$
17	14 16 6	addcomli	$⊢ B C + A D = 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	$⊢ A D = A D$
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 \|-

Metamath Proof Explorer