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 |
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 |