Metamath Proof Explorer
Description: Add two numerals M and N (with 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 |
|
|
decaddc.e |
|- ( ( A + C ) + 1 ) = E |
|
|
decaddc2.t |
|- ( B + D ) = ; 1 0 |
|
Assertion |
decaddc2 |
|- ( M + N ) = ; E 0 |
Proof
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 |
|
decaddc.e |
|- ( ( A + C ) + 1 ) = E |
8 |
|
decaddc2.t |
|- ( B + D ) = ; 1 0 |
9 |
|
0nn0 |
|- 0 e. NN0 |
10 |
1 2 3 4 5 6 7 9 8
|
decaddc |
|- ( M + N ) = ; E 0 |