Theorem decmulnc

Description: The product of a numeral with a number (no carry). (Contributed by AV, 15-Jun-2021)

	Ref	Expression
Hypotheses	decmulnc.n	$$⊢N\in {\mathbb{N}}_0$$
	decmulnc.a	$$⊢A\in {\mathbb{N}}_0$$
	decmulnc.b	$$⊢B\in {\mathbb{N}}_0$$
Assertion	decmulnc	Could not format assertion : No typesetting found for |- ( N x. ; A B ) = ; ( N x. A ) ( N x. B ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		decmulnc.n	$$⊢N\in {\mathbb{N}}_0$$
2		decmulnc.a	$$⊢A\in {\mathbb{N}}_0$$
3		decmulnc.b	$$⊢B\in {\mathbb{N}}_0$$
4		eqid	Could not format ; A B = ; A B : No typesetting found for |- ; A B = ; A B with typecode |-
5	1 3	nn0mulcli	$$⊢NB\in {\mathbb{N}}_0$$
6		0nn0	$$⊢0\in {\mathbb{N}}_0$$
7	1 2	nn0mulcli	$$⊢NA\in {\mathbb{N}}_0$$
8	7	nn0cni	$$⊢NA\in ℂ$$
9	8	addridi	$$⊢NA+0=NA$$
10	5	dec0h	Could not format ( N x. B ) = ; 0 ( N x. B ) : No typesetting found for |- ( N x. B ) = ; 0 ( N x. B ) with typecode |-
11	1 2 3 4 5 6 9 10	decmul2c	Could not format ( N x. ; A B ) = ; ( N x. A ) ( N x. B ) : No typesetting found for |- ( N x. ; A B ) = ; ( N x. A ) ( N x. B ) with typecode |-