Metamath Proof Explorer


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 )