Description: Add two numerals M and N (no carry). (Contributed by Mario Carneiro, 18-Feb-2014)
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 |
||
decaddci.6 | |- C e. NN0 |
||
decaddci.7 | |- ( B + N ) = ; 1 C |
||
Assertion | decaddci | |- ( M + N ) = ; D C |
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 | decaddci.6 | |- C e. NN0 |
|
7 | decaddci.7 | |- ( B + N ) = ; 1 C |
|
8 | 0nn0 | |- 0 e. NN0 |
|
9 | 3 | dec0h | |- N = ; 0 N |
10 | 1 | nn0cni | |- A e. CC |
11 | 10 | addid1i | |- ( A + 0 ) = A |
12 | 11 | oveq1i | |- ( ( A + 0 ) + 1 ) = ( A + 1 ) |
13 | 12 5 | eqtri | |- ( ( A + 0 ) + 1 ) = D |
14 | 1 2 8 3 4 9 13 6 7 | decaddc | |- ( M + N ) = ; D C |