decpmul

Description: Partial products algorithm for two digit multiplication. (Contributed by Steven Nguyen, 10-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$
	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 ℕ_{0}$
	decpmul.h	$⊢ H \in ℕ_{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 ℕ_{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		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 ℕ_{0}$
10		decpmul.h	$⊢ H \in ℕ_{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	$⊢ A C \in ℕ_{0}$
14	5 13	eqeltrri	$⊢ E \in ℕ_{0}$
15	2 3	nn0mulcli	$⊢ B C \in ℕ_{0}$
16	1 4 15	numcl	$⊢ A D + B C \in ℕ_{0}$
17	6 16	eqeltrri	$⊢ F \in ℕ_{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 ℕ_{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	addlidi	$⊢ 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 \|-

Metamath Proof Explorer

Theorem decpmul

Proof