Theorem numsucc

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

	Ref	Expression
Hypotheses	numsucc.1	$$⊢Y\in {\mathbb{N}}_0$$
	numsucc.2	$$⊢T=Y+1$$
	numsucc.3	$$⊢A\in {\mathbb{N}}_0$$
	numsucc.4	$$⊢A+1=B$$
	numsucc.5	$$⊢N=TA+Y$$
Assertion	numsucc	$$⊢N+1=TB+0$$

Proof

Step	Hyp	Ref	Expression
1		numsucc.1	$$⊢Y\in {\mathbb{N}}_0$$
2		numsucc.2	$$⊢T=Y+1$$
3		numsucc.3	$$⊢A\in {\mathbb{N}}_0$$
4		numsucc.4	$$⊢A+1=B$$
5		numsucc.5	$$⊢N=TA+Y$$
6		1nn0	$$⊢1\in {\mathbb{N}}_0$$
7	1 6	nn0addcli	$$⊢Y+1\in {\mathbb{N}}_0$$
8	2 7	eqeltri	$$⊢T\in {\mathbb{N}}_0$$
9	8	nn0cni	$$⊢T\in ℂ$$
10	9	mulid1i	$$⊢T\cdot 1=T$$
11	10	oveq2i	$$⊢TA+T\cdot 1=TA+T$$
12	3	nn0cni	$$⊢A\in ℂ$$
13		ax-1cn	$$⊢1\in ℂ$$
14	9 12 13	adddii	$$⊢T\left(A+1\right)=TA+T\cdot 1$$
15	2	eqcomi	$$⊢Y+1=T$$
16	8 3 1 15 5	numsuc	$$⊢N+1=TA+T$$
17	11 14 16	3eqtr4ri	$$⊢N+1=T\left(A+1\right)$$
18	4	oveq2i	$$⊢T\left(A+1\right)=TB$$
19	3 6	nn0addcli	$$⊢A+1\in {\mathbb{N}}_0$$
20	4 19	eqeltrri	$$⊢B\in {\mathbb{N}}_0$$
21	8 20	num0u	$$⊢TB=TB+0$$
22	17 18 21	3eqtri	$$⊢N+1=TB+0$$