Theorem nummul1c

Description: The product of a decimal integer with a number. (Contributed by Mario Carneiro, 18-Feb-2014)

	Ref	Expression
Hypotheses	nummul1c.1	$$⊢T\in {\mathbb{N}}_0$$
	nummul1c.2	$$⊢P\in {\mathbb{N}}_0$$
	nummul1c.3	$$⊢A\in {\mathbb{N}}_0$$
	nummul1c.4	$$⊢B\in {\mathbb{N}}_0$$
	nummul1c.5	$$⊢N=TA+B$$
	nummul1c.6	$$⊢D\in {\mathbb{N}}_0$$
	nummul1c.7	$$⊢E\in {\mathbb{N}}_0$$
	nummul1c.8	$$⊢AP+E=C$$
	nummul1c.9	$$⊢BP=TE+D$$
Assertion	nummul1c	$$⊢NP=TC+D$$

Proof

Step	Hyp	Ref	Expression
1		nummul1c.1	$$⊢T\in {\mathbb{N}}_0$$
2		nummul1c.2	$$⊢P\in {\mathbb{N}}_0$$
3		nummul1c.3	$$⊢A\in {\mathbb{N}}_0$$
4		nummul1c.4	$$⊢B\in {\mathbb{N}}_0$$
5		nummul1c.5	$$⊢N=TA+B$$
6		nummul1c.6	$$⊢D\in {\mathbb{N}}_0$$
7		nummul1c.7	$$⊢E\in {\mathbb{N}}_0$$
8		nummul1c.8	$$⊢AP+E=C$$
9		nummul1c.9	$$⊢BP=TE+D$$
10	1 3 4	numcl	$$⊢TA+B\in {\mathbb{N}}_0$$
11	5 10	eqeltri	$$⊢N\in {\mathbb{N}}_0$$
12	11 2	num0u	$$⊢NP=NP+0$$
13		0nn0	$$⊢0\in {\mathbb{N}}_0$$
14	1 13	num0h	$$⊢0=T\cdot 0+0$$
15	7	nn0cni	$$⊢E\in ℂ$$
16	15	addid2i	$$⊢0+E=E$$
17	16	oveq2i	$$⊢AP+0+E=AP+E$$
18	17 8	eqtri	$$⊢AP+0+E=C$$
19	4 2	num0u	$$⊢BP=BP+0$$
20	19 9	eqtr3i	$$⊢BP+0=TE+D$$
21	1 3 4 13 13 5 14 2 6 7 18 20	nummac	$$⊢NP+0=TC+D$$
22	12 21	eqtri	$$⊢NP=TC+D$$