Description: The successor of a decimal integer (no carry). (Contributed by Mario Carneiro, 17-Apr-2015) (Revised by AV, 6-Sep-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | declt.a | |- A e. NN0 |
|
declt.b | |- B e. NN0 |
||
decsuc.c | |- ( B + 1 ) = C |
||
decsuc.n | |- N = ; A B |
||
Assertion | decsuc | |- ( N + 1 ) = ; A C |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | declt.a | |- A e. NN0 |
|
2 | declt.b | |- B e. NN0 |
|
3 | decsuc.c | |- ( B + 1 ) = C |
|
4 | decsuc.n | |- N = ; A B |
|
5 | 10nn0 | |- ; 1 0 e. NN0 |
|
6 | dfdec10 | |- ; A B = ( ( ; 1 0 x. A ) + B ) |
|
7 | 4 6 | eqtri | |- N = ( ( ; 1 0 x. A ) + B ) |
8 | 5 1 2 3 7 | numsuc | |- ( N + 1 ) = ( ( ; 1 0 x. A ) + C ) |
9 | dfdec10 | |- ; A C = ( ( ; 1 0 x. A ) + C ) |
|
10 | 8 9 | eqtr4i | |- ( N + 1 ) = ; A C |