Metamath Proof Explorer


Theorem decmul1c

Description: The product of a numeral with a number (with carry). (Contributed by Mario Carneiro, 18-Feb-2014) (Revised by AV, 6-Sep-2021)

Ref Expression
Hypotheses decmul1.p
|- P e. NN0
decmul1.a
|- A e. NN0
decmul1.b
|- B e. NN0
decmul1.n
|- N = ; A B
decmul1.0
|- D e. NN0
decmul1c.e
|- E e. NN0
decmul1c.c
|- ( ( A x. P ) + E ) = C
decmul1c.2
|- ( B x. P ) = ; E D
Assertion decmul1c
|- ( N x. P ) = ; C D

Proof

Step Hyp Ref Expression
1 decmul1.p
 |-  P e. NN0
2 decmul1.a
 |-  A e. NN0
3 decmul1.b
 |-  B e. NN0
4 decmul1.n
 |-  N = ; A B
5 decmul1.0
 |-  D e. NN0
6 decmul1c.e
 |-  E e. NN0
7 decmul1c.c
 |-  ( ( A x. P ) + E ) = C
8 decmul1c.2
 |-  ( B x. P ) = ; E D
9 10nn0
 |-  ; 1 0 e. NN0
10 dfdec10
 |-  ; A B = ( ( ; 1 0 x. A ) + B )
11 4 10 eqtri
 |-  N = ( ( ; 1 0 x. A ) + B )
12 dfdec10
 |-  ; E D = ( ( ; 1 0 x. E ) + D )
13 8 12 eqtri
 |-  ( B x. P ) = ( ( ; 1 0 x. E ) + D )
14 9 1 2 3 11 5 6 7 13 nummul1c
 |-  ( N x. P ) = ( ( ; 1 0 x. C ) + D )
15 dfdec10
 |-  ; C D = ( ( ; 1 0 x. C ) + D )
16 14 15 eqtr4i
 |-  ( N x. P ) = ; C D