Theorem numsuc

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

	Ref	Expression
Hypotheses	numnncl.1	|- T e. NN0
	numnncl.2	|- A e. NN0
	numcl.2	|- B e. NN0
	numsuc.4	|- ( B + 1 ) = C
	numsuc.5	|- N = ( ( T x. A ) + B )
Assertion	numsuc	|- ( N + 1 ) = ( ( T x. A ) + C )

Proof

Step	Hyp	Ref	Expression
1		numnncl.1	|- T e. NN0
2		numnncl.2	|- A e. NN0
3		numcl.2	|- B e. NN0
4		numsuc.4	|- ( B + 1 ) = C
5		numsuc.5	|- N = ( ( T x. A ) + B )
6	5	oveq1i	|- ( N + 1 ) = ( ( ( T x. A ) + B ) + 1 )
7	1 2	nn0mulcli	|- ( T x. A ) e. NN0
8	7	nn0cni	|- ( T x. A ) e. CC
9	3	nn0cni	|- B e. CC
10		ax-1cn	|- 1 e. CC
11	8 9 10	addassi	|- ( ( ( T x. A ) + B ) + 1 ) = ( ( T x. A ) + ( B + 1 ) )
12	4	oveq2i	|- ( ( T x. A ) + ( B + 1 ) ) = ( ( T x. A ) + C )
13	6 11 12	3eqtri	|- ( N + 1 ) = ( ( T x. A ) + C )