Description: The successor of a decimal integer (with carry). (Contributed by Mario Carneiro, 18-Feb-2014) (Revised by AV, 6-Sep-2021)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | decsucc.1 | |- A e. NN0 |
|
| decsucc.2 | |- ( A + 1 ) = B |
||
| decsucc.3 | |- N = ; A 9 |
||
| Assertion | decsucc | |- ( N + 1 ) = ; B 0 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | decsucc.1 | |- A e. NN0 |
|
| 2 | decsucc.2 | |- ( A + 1 ) = B |
|
| 3 | decsucc.3 | |- N = ; A 9 |
|
| 4 | 9nn0 | |- 9 e. NN0 |
|
| 5 | 9p1e10 | |- ( 9 + 1 ) = ; 1 0 |
|
| 6 | 5 | eqcomi | |- ; 1 0 = ( 9 + 1 ) |
| 7 | dfdec10 | |- ; A 9 = ( ( ; 1 0 x. A ) + 9 ) |
|
| 8 | 3 7 | eqtri | |- N = ( ( ; 1 0 x. A ) + 9 ) |
| 9 | 4 6 1 2 8 | numsucc | |- ( N + 1 ) = ( ( ; 1 0 x. B ) + 0 ) |
| 10 | dfdec10 | |- ; B 0 = ( ( ; 1 0 x. B ) + 0 ) |
|
| 11 | 9 10 | eqtr4i | |- ( N + 1 ) = ; B 0 |