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