Theorem decrmac

Description: Perform a multiply-add of two numerals M and N against a fixed multiplicand P (with carry). (Contributed by AV, 16-Sep-2021)

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

Proof

Step	Hyp	Ref	Expression
1		decrmanc.a	$$⊢A\in {\mathbb{N}}_0$$
2		decrmanc.b	$$⊢B\in {\mathbb{N}}_0$$
3		decrmanc.n	$$⊢N\in {\mathbb{N}}_0$$
4		decrmanc.m	Could not format M = ; A B : No typesetting found for |- M = ; A B with typecode |-
5		decrmanc.p	$$⊢P\in {\mathbb{N}}_0$$
6		decrmac.f	$$⊢F\in {\mathbb{N}}_0$$
7		decrmac.g	$$⊢G\in {\mathbb{N}}_0$$
8		decrmac.e	$$⊢AP+G=E$$
9		decrmac.2	Could not format ( ( B x. P ) + N ) = ; G F : No typesetting found for |- ( ( B x. P ) + N ) = ; G F with typecode |-
10		0nn0	$$⊢0\in {\mathbb{N}}_0$$
11	3	dec0h	$$⊢N=\mathrm{0\; <mi\; mathcolor="\#808">N</mi>}$$
12	7	nn0cni	$$⊢G\in ℂ$$
13	12	addid2i	$$⊢0+G=G$$
14	13	oveq2i	$$⊢AP+0+G=AP+G$$
15	14 8	eqtri	$$⊢AP+0+G=E$$
16	1 2 10 3 4 11 5 6 7 15 9	decmac	Could not format ( ( M x. P ) + N ) = ; E F : No typesetting found for |- ( ( M x. P ) + N ) = ; E F with typecode |-