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\in {\mathbb{N}}_0$$
	declt.b	$$⊢B\in {\mathbb{N}}_0$$
	decsuc.c	$$⊢B+1=C$$
	decsuc.n	No typesetting found for |- N = ; A B with typecode |-
Assertion	decsuc	Could not format assertion : No typesetting found for |- ( N + 1 ) = ; A C with typecode |-

Proof

Step	Hyp	Ref	Expression
1		declt.a	$$⊢A\in {\mathbb{N}}_0$$
2		declt.b	$$⊢B\in {\mathbb{N}}_0$$
3		decsuc.c	$$⊢B+1=C$$
4		decsuc.n	Could not format N = ; A B : No typesetting found for |- N = ; A B with typecode |-
5		10nn0	$$⊢10\in {\mathbb{N}}_0$$
6		dfdec10	Could not format ; A B = ( ( ; 1 0 x. A ) + B ) : No typesetting found for |- ; A B = ( ( ; 1 0 x. A ) + B ) with typecode |-
7	4 6	eqtri	$$⊢N=10A+B$$
8	5 1 2 3 7	numsuc	$$⊢N+1=10A+C$$
9		dfdec10	Could not format ; A C = ( ( ; 1 0 x. A ) + C ) : No typesetting found for |- ; A C = ( ( ; 1 0 x. A ) + C ) with typecode |-
10	8 9	eqtr4i	Could not format ( N + 1 ) = ; A C : No typesetting found for |- ( N + 1 ) = ; A C with typecode |-