Theorem decmul1

Description: The product of a numeral with a number (no carry). (Contributed by AV, 22-Jul-2021) (Revised by AV, 6-Sep-2021) Remove hypothesis D e. NN0 . (Revised by Steven Nguyen, 7-Dec-2022)

	Ref	Expression
Hypotheses	decmul1.p	$$⊢P\in {\mathbb{N}}_0$$
	decmul1.a	$$⊢A\in {\mathbb{N}}_0$$
	decmul1.b	$$⊢B\in {\mathbb{N}}_0$$
	decmul1.n	No typesetting found for |- N = ; A B with typecode |-
	decmul1.c	$$⊢AP=C$$
	decmul1.d	$$⊢BP=D$$
Assertion	decmul1	Could not format assertion : No typesetting found for |- ( N x. P ) = ; C D with typecode |-

Proof

Step	Hyp	Ref	Expression
1		decmul1.p	$$⊢P\in {\mathbb{N}}_0$$
2		decmul1.a	$$⊢A\in {\mathbb{N}}_0$$
3		decmul1.b	$$⊢B\in {\mathbb{N}}_0$$
4		decmul1.n	Could not format N = ; A B : No typesetting found for |- N = ; A B with typecode |-
5		decmul1.c	$$⊢AP=C$$
6		decmul1.d	$$⊢BP=D$$
7	2 3	deccl	Could not format ; A B e. NN0 : No typesetting found for |- ; A B e. NN0 with typecode |-
8	4 7	eqeltri	$$⊢N\in {\mathbb{N}}_0$$
9	8 1	num0u	$$⊢NP=NP+0$$
10		0nn0	$$⊢0\in {\mathbb{N}}_0$$
11	3 1	nn0mulcli	$$⊢BP\in {\mathbb{N}}_0$$
12	11	nn0cni	$$⊢BP\in ℂ$$
13	12	addid1i	$$⊢BP+0=BP$$
14	13 6	eqtri	$$⊢BP+0=D$$
15	2 3 10 4 1 5 14	decrmanc	Could not format ( ( N x. P ) + 0 ) = ; C D : No typesetting found for |- ( ( N x. P ) + 0 ) = ; C D with typecode |-
16	9 15	eqtri	Could not format ( N x. P ) = ; C D : No typesetting found for |- ( N x. P ) = ; C D with typecode |-