Theorem decsucc

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\in {\mathbb{N}}_0$$
	decsucc.2	$$⊢A+1=B$$
	decsucc.3	No typesetting found for |- N = ; A 9 with typecode |-
Assertion	decsucc	Could not format assertion : No typesetting found for |- ( N + 1 ) = ; B 0 with typecode |-

Proof

Step	Hyp	Ref	Expression
1		decsucc.1	$$⊢A\in {\mathbb{N}}_0$$
2		decsucc.2	$$⊢A+1=B$$
3		decsucc.3	Could not format N = ; A 9 : No typesetting found for |- N = ; A 9 with typecode |-
4		9nn0	$$⊢9\in {\mathbb{N}}_0$$
5		9p1e10	$$⊢9+1=10$$
6	5	eqcomi	$$⊢10=9+1$$
7		dfdec10	Could not format ; A 9 = ( ( ; 1 0 x. A ) + 9 ) : No typesetting found for |- ; A 9 = ( ( ; 1 0 x. A ) + 9 ) with typecode |-
8	3 7	eqtri	$$⊢N=10A+9$$
9	4 6 1 2 8	numsucc	$$⊢N+1=10B+0$$
10		dfdec10	Could not format ; B 0 = ( ( ; 1 0 x. B ) + 0 ) : No typesetting found for |- ; B 0 = ( ( ; 1 0 x. B ) + 0 ) with typecode |-
11	9 10	eqtr4i	Could not format ( N + 1 ) = ; B 0 : No typesetting found for |- ( N + 1 ) = ; B 0 with typecode |-