Metamath Proof Explorer


Theorem decsuc

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

Proof

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