decmac

Description: Perform a multiply-add of two numerals M and N against a fixed multiplicand P (with carry). (Contributed by Mario Carneiro, 18-Feb-2014) (Revised by AV, 6-Sep-2021)

	Ref	Expression
Hypotheses	decma.a	$⊢ A \in ℕ_{0}$
	decma.b	$⊢ B \in ℕ_{0}$
	decma.c	$⊢ C \in ℕ_{0}$
	decma.d	$⊢ D \in ℕ_{0}$
	decma.m	No typesetting found for \|- M = ; A B with typecode \|-
	decma.n	No typesetting found for \|- N = ; C D with typecode \|-
	decmac.p	$⊢ P \in ℕ_{0}$
	decmac.f	$⊢ F \in ℕ_{0}$
	decmac.g	$⊢ G \in ℕ_{0}$
	decmac.e	$⊢ A P + C + G = E$
	decmac.2	No typesetting found for \|- ( ( B x. P ) + D ) = ; G F with typecode \|-
Assertion	decmac	Could not format assertion : No typesetting found for \|- ( ( M x. P ) + N ) = ; E F with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		decma.a	$⊢ A \in ℕ_{0}$
2		decma.b	$⊢ B \in ℕ_{0}$
3		decma.c	$⊢ C \in ℕ_{0}$
4		decma.d	$⊢ D \in ℕ_{0}$
5		decma.m	Could not format M = ; A B : No typesetting found for \|- M = ; A B with typecode \|-
6		decma.n	Could not format N = ; C D : No typesetting found for \|- N = ; C D with typecode \|-
7		decmac.p	$⊢ P \in ℕ_{0}$
8		decmac.f	$⊢ F \in ℕ_{0}$
9		decmac.g	$⊢ G \in ℕ_{0}$
10		decmac.e	$⊢ A P + C + G = E$
11		decmac.2	Could not format ( ( B x. P ) + D ) = ; G F : No typesetting found for \|- ( ( B x. P ) + D ) = ; G F with typecode \|-
12		10nn0	$⊢ 10 \in ℕ_{0}$
13		dfdec10	Could not format ; A B = ( ( ; 1 0 x. A ) + B ) : No typesetting found for \|- ; A B = ( ( ; 1 0 x. A ) + B ) with typecode \|-
14	5 13	eqtri	$⊢ M = 10 A + B$
15		dfdec10	Could not format ; C D = ( ( ; 1 0 x. C ) + D ) : No typesetting found for \|- ; C D = ( ( ; 1 0 x. C ) + D ) with typecode \|-
16	6 15	eqtri	$⊢ N = 10 C + D$
17		dfdec10	Could not format ; G F = ( ( ; 1 0 x. G ) + F ) : No typesetting found for \|- ; G F = ( ( ; 1 0 x. G ) + F ) with typecode \|-
18	11 17	eqtri	$⊢ B P + D = 10 G + F$
19	12 1 2 3 4 14 16 7 8 9 10 18	nummac	$⊢ M P + N = 10 E + F$
20		dfdec10	Could not format ; E F = ( ( ; 1 0 x. E ) + F ) : No typesetting found for \|- ; E F = ( ( ; 1 0 x. E ) + F ) with typecode \|-
21	19 20	eqtr4i	Could not format ( ( M x. P ) + N ) = ; E F : No typesetting found for \|- ( ( M x. P ) + N ) = ; E F with typecode \|-

Metamath Proof Explorer

Theorem decmac

Proof