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 e. NN0
	nummul1c.2	|- P e. NN0
	nummul1c.3	|- A e. NN0
	nummul1c.4	|- B e. NN0
	nummul1c.5	|- N = ( ( T x. A ) + B )
	nummul1c.6	|- D e. NN0
	nummul1c.7	|- E e. NN0
	nummul1c.8	|- ( ( A x. P ) + E ) = C
	nummul1c.9	|- ( B x. P ) = ( ( T x. E ) + D )
Assertion	nummul1c	|- ( N x. P ) = ( ( T x. C ) + D )

Proof

Step	Hyp	Ref	Expression
1		nummul1c.1	|- T e. NN0
2		nummul1c.2	|- P e. NN0
3		nummul1c.3	|- A e. NN0
4		nummul1c.4	|- B e. NN0
5		nummul1c.5	|- N = ( ( T x. A ) + B )
6		nummul1c.6	|- D e. NN0
7		nummul1c.7	|- E e. NN0
8		nummul1c.8	|- ( ( A x. P ) + E ) = C
9		nummul1c.9	|- ( B x. P ) = ( ( T x. E ) + D )
10	1 3 4	numcl	|- ( ( T x. A ) + B ) e. NN0
11	5 10	eqeltri	|- N e. NN0
12	11 2	num0u	|- ( N x. P ) = ( ( N x. P ) + 0 )
13		0nn0	|- 0 e. NN0
14	1 13	num0h	|- 0 = ( ( T x. 0 ) + 0 )
15	7	nn0cni	|- E e. CC
16	15	addid2i	|- ( 0 + E ) = E
17	16	oveq2i	|- ( ( A x. P ) + ( 0 + E ) ) = ( ( A x. P ) + E )
18	17 8	eqtri	|- ( ( A x. P ) + ( 0 + E ) ) = C
19	4 2	num0u	|- ( B x. P ) = ( ( B x. P ) + 0 )
20	19 9	eqtr3i	|- ( ( B x. P ) + 0 ) = ( ( T x. E ) + D )
21	1 3 4 13 13 5 14 2 6 7 18 20	nummac	|- ( ( N x. P ) + 0 ) = ( ( T x. C ) + D )
22	12 21	eqtri	|- ( N x. P ) = ( ( T x. C ) + D )