Theorem decma2c

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

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

Proof

Step	Hyp	Ref	Expression
1		decma.a	$$⊢A\in {\mathbb{N}}_0$$
2		decma.b	$$⊢B\in {\mathbb{N}}_0$$
3		decma.c	$$⊢C\in {\mathbb{N}}_0$$
4		decma.d	$$⊢D\in {\mathbb{N}}_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		decma2c.p	$$⊢P\in {\mathbb{N}}_0$$
8		decma2c.f	$$⊢F\in {\mathbb{N}}_0$$
9		decma2c.g	$$⊢G\in {\mathbb{N}}_0$$
10		decma2c.e	$$⊢PA+C+G=E$$
11		decma2c.2	Could not format ( ( P x. B ) + D ) = ; G F : No typesetting found for |- ( ( P x. B ) + D ) = ; G F with typecode |-
12		10nn0	$$⊢10\in {\mathbb{N}}_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=10A+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=10C+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	$$⊢PB+D=10G+F$$
19	12 1 2 3 4 14 16 7 8 9 10 18	numma2c	$$⊢P\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}+N=10E+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 ( ( P x. M ) + N ) = ; E F : No typesetting found for |- ( ( P x. M ) + N ) = ; E F with typecode |-