Theorem numsuc

Description: The successor of a decimal integer (no carry). (Contributed by Mario Carneiro, 18-Feb-2014)

	Ref	Expression
Hypotheses	numnncl.1	$$⊢T\in {\mathbb{N}}_0$$
	numnncl.2	$$⊢A\in {\mathbb{N}}_0$$
	numcl.2	$$⊢B\in {\mathbb{N}}_0$$
	numsuc.4	$$⊢B+1=C$$
	numsuc.5	$$⊢N=TA+B$$
Assertion	numsuc	$$⊢N+1=TA+C$$

Proof

Step	Hyp	Ref	Expression
1		numnncl.1	$$⊢T\in {\mathbb{N}}_0$$
2		numnncl.2	$$⊢A\in {\mathbb{N}}_0$$
3		numcl.2	$$⊢B\in {\mathbb{N}}_0$$
4		numsuc.4	$$⊢B+1=C$$
5		numsuc.5	$$⊢N=TA+B$$
6	5	oveq1i	$$⊢N+1=TA+B+1$$
7	1 2	nn0mulcli	$$⊢TA\in {\mathbb{N}}_0$$
8	7	nn0cni	$$⊢TA\in ℂ$$
9	3	nn0cni	$$⊢B\in ℂ$$
10		ax-1cn	$$⊢1\in ℂ$$
11	8 9 10	addassi	$$⊢TA+B+1=TA+B+1$$
12	4	oveq2i	$$⊢TA+B+1=TA+C$$
13	6 11 12	3eqtri	$$⊢N+1=TA+C$$