Theorem nummul2c

Description: The product of a decimal integer with a number (with carry). (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$$
	nummul2c.7	$$⊢PA+E=C$$
	nummul2c.8	$$⊢PB=TE+D$$
Assertion	nummul2c	$$⊢P\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=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		nummul2c.7	$$⊢PA+E=C$$
9		nummul2c.8	$$⊢PB=TE+D$$
10	1 3 4	numcl	$$⊢TA+B\in {\mathbb{N}}_0$$
11	5 10	eqeltri	$$⊢N\in {\mathbb{N}}_0$$
12	11	nn0cni	$$⊢N\in ℂ$$
13	2	nn0cni	$$⊢P\in ℂ$$
14	3	nn0cni	$$⊢A\in ℂ$$
15	14 13	mulcomi	$$⊢AP=PA$$
16	15	oveq1i	$$⊢AP+E=PA+E$$
17	16 8	eqtri	$$⊢AP+E=C$$
18	4	nn0cni	$$⊢B\in ℂ$$
19	13 18 9	mulcomli	$$⊢BP=TE+D$$
20	1 2 3 4 5 6 7 17 19	nummul1c	$$⊢NP=TC+D$$
21	12 13 20	mulcomli	$$⊢P\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=TC+D$$