Theorem numsucc

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

	Ref	Expression
Hypotheses	numsucc.1	|- Y e. NN0
	numsucc.2	|- T = ( Y + 1 )
	numsucc.3	|- A e. NN0
	numsucc.4	|- ( A + 1 ) = B
	numsucc.5	|- N = ( ( T x. A ) + Y )
Assertion	numsucc	|- ( N + 1 ) = ( ( T x. B ) + 0 )

Proof

Step	Hyp	Ref	Expression
1		numsucc.1	|- Y e. NN0
2		numsucc.2	|- T = ( Y + 1 )
3		numsucc.3	|- A e. NN0
4		numsucc.4	|- ( A + 1 ) = B
5		numsucc.5	|- N = ( ( T x. A ) + Y )
6		1nn0	|- 1 e. NN0
7	1 6	nn0addcli	|- ( Y + 1 ) e. NN0
8	2 7	eqeltri	|- T e. NN0
9	8	nn0cni	|- T e. CC
10	9	mulid1i	|- ( T x. 1 ) = T
11	10	oveq2i	|- ( ( T x. A ) + ( T x. 1 ) ) = ( ( T x. A ) + T )
12	3	nn0cni	|- A e. CC
13		ax-1cn	|- 1 e. CC
14	9 12 13	adddii	|- ( T x. ( A + 1 ) ) = ( ( T x. A ) + ( T x. 1 ) )
15	2	eqcomi	|- ( Y + 1 ) = T
16	8 3 1 15 5	numsuc	|- ( N + 1 ) = ( ( T x. A ) + T )
17	11 14 16	3eqtr4ri	|- ( N + 1 ) = ( T x. ( A + 1 ) )
18	4	oveq2i	|- ( T x. ( A + 1 ) ) = ( T x. B )
19	3 6	nn0addcli	|- ( A + 1 ) e. NN0
20	4 19	eqeltrri	|- B e. NN0
21	8 20	num0u	|- ( T x. B ) = ( ( T x. B ) + 0 )
22	17 18 21	3eqtri	|- ( N + 1 ) = ( ( T x. B ) + 0 )