Theorem decrmanc

Description: Perform a multiply-add of two numerals M and N against a fixed multiplicand P (no 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$$
	decrmanc.e	$$⊢AP=E$$
	decrmanc.f	$$⊢BP+N=F$$
Assertion	decrmanc	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		decrmanc.e	$$⊢AP=E$$
7		decrmanc.f	$$⊢BP+N=F$$
8		0nn0	$$⊢0\in {\mathbb{N}}_0$$
9	3	dec0h	$$⊢N=\mathrm{0<mi\; mathcolor="\#808">N</mi>}$$
10	1 5	nn0mulcli	$$⊢AP\in {\mathbb{N}}_0$$
11	10	nn0cni	$$⊢AP\in ℂ$$
12	11	addid1i	$$⊢AP+0=AP$$
13	12 6	eqtri	$$⊢AP+0=E$$
14	1 2 8 3 4 9 5 13 7	decma	Could not format ( ( M x. P ) + N ) = ; E F : No typesetting found for |- ( ( M x. P ) + N ) = ; E F with typecode |-