This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 addlidi 
 |-  ( 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 )