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

Metamath Proof Explorer

Theorem decmul2c

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
decmul2c.c 
|- ( ( P x. A ) + E ) = C
decmul2c.2 
|- ( P x. B ) = ; E D
Assertion decmul2c 
|- ( P x. N ) = ; 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 decmul2c.c 
 |-  ( ( P x. A ) + E ) = C
8 decmul2c.2 
 |-  ( P x. B ) = ; 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 
 |-  ( P x. B ) = ( ( ; 1 0 x. E ) + D )
14 9 1 2 3 11 5 6 7 13 nummul2c 
 |-  ( P x. N ) = ( ( ; 1 0 x. C ) + D )
15 dfdec10 
 |-  ; C D = ( ( ; 1 0 x. C ) + D )
16 14 15 eqtr4i 
 |-  ( P x. N ) = ; C D