Description: Add two numerals M and N (no carry). (Contributed by Mario Carneiro, 18-Feb-2014) (Revised by AV, 6-Sep-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | decma.a | |- A e. NN0 |
|
decma.b | |- B e. NN0 |
||
decma.c | |- C e. NN0 |
||
decma.d | |- D e. NN0 |
||
decma.m | |- M = ; A B |
||
decma.n | |- N = ; C D |
||
decadd.e | |- ( A + C ) = E |
||
decadd.f | |- ( B + D ) = F |
||
Assertion | decadd | |- ( M + N ) = ; E F |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | decma.a | |- A e. NN0 |
|
2 | decma.b | |- B e. NN0 |
|
3 | decma.c | |- C e. NN0 |
|
4 | decma.d | |- D e. NN0 |
|
5 | decma.m | |- M = ; A B |
|
6 | decma.n | |- N = ; C D |
|
7 | decadd.e | |- ( A + C ) = E |
|
8 | decadd.f | |- ( B + D ) = F |
|
9 | 10nn0 | |- ; 1 0 e. NN0 |
|
10 | dfdec10 | |- ; A B = ( ( ; 1 0 x. A ) + B ) |
|
11 | 5 10 | eqtri | |- M = ( ( ; 1 0 x. A ) + B ) |
12 | dfdec10 | |- ; C D = ( ( ; 1 0 x. C ) + D ) |
|
13 | 6 12 | eqtri | |- N = ( ( ; 1 0 x. C ) + D ) |
14 | 9 1 2 3 4 11 13 7 8 | numadd | |- ( M + N ) = ( ( ; 1 0 x. E ) + F ) |
15 | dfdec10 | |- ; E F = ( ( ; 1 0 x. E ) + F ) |
|
16 | 14 15 | eqtr4i | |- ( M + N ) = ; E F |