Metamath Proof Explorer

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 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
nummul2c.7 
|- ( ( P x. A ) + E ) = C
nummul2c.8 
|- ( P x. B ) = ( ( T x. E ) + D )
Assertion nummul2c 
|- ( P x. N ) = ( ( 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 nummul2c.7 
 |-  ( ( P x. A ) + E ) = C
9 nummul2c.8 
 |-  ( P x. B ) = ( ( T x. E ) + D )
10 1 3 4 numcl 
 |-  ( ( T x. A ) + B ) e. NN0
11 5 10 eqeltri 
 |-  N e. NN0
12 11 nn0cni 
 |-  N e. CC
13 2 nn0cni 
 |-  P e. CC
14 3 nn0cni 
 |-  A e. CC
15 14 13 mulcomi 
 |-  ( A x. P ) = ( P x. A )
16 15 oveq1i 
 |-  ( ( A x. P ) + E ) = ( ( P x. A ) + E )
17 16 8 eqtri 
 |-  ( ( A x. P ) + E ) = C
18 4 nn0cni 
 |-  B e. CC
19 13 18 9 mulcomli 
 |-  ( B x. P ) = ( ( T x. E ) + D )
20 1 2 3 4 5 6 7 17 19 nummul1c 
 |-  ( N x. P ) = ( ( T x. C ) + D )
21 12 13 20 mulcomli 
 |-  ( P x. N ) = ( ( T x. C ) + D )