Metamath Proof Explorer
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 |
decaddi.1 |
|- A e. NN0 |
|
|
decaddi.2 |
|- B e. NN0 |
|
|
decaddi.3 |
|- N e. NN0 |
|
|
decaddi.4 |
|- M = ; A B |
|
|
decaddci.5 |
|- ( A + 1 ) = D |
|
|
decaddci2.6 |
|- ( B + N ) = ; 1 0 |
|
Assertion |
decaddci2 |
|- ( M + N ) = ; D 0 |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
decaddi.1 |
|- A e. NN0 |
| 2 |
|
decaddi.2 |
|- B e. NN0 |
| 3 |
|
decaddi.3 |
|- N e. NN0 |
| 4 |
|
decaddi.4 |
|- M = ; A B |
| 5 |
|
decaddci.5 |
|- ( A + 1 ) = D |
| 6 |
|
decaddci2.6 |
|- ( B + N ) = ; 1 0 |
| 7 |
|
0nn0 |
|- 0 e. NN0 |
| 8 |
1 2 3 4 5 7 6
|
decaddci |
|- ( M + N ) = ; D 0 |