Theorem decaddci

Description: Add two numerals M and N (no carry). (Contributed by Mario Carneiro, 18-Feb-2014)

	Ref	Expression
Hypotheses	decaddi.1	|- A e. NN0
	decaddi.2	|- B e. NN0
	decaddi.3	|- N e. NN0
	decaddi.4	|- M = ; A B
	decaddci.5	|- ( A + 1 ) = D
	decaddci.6	|- C e. NN0
	decaddci.7	|- ( B + N ) = ; 1 C
Assertion	decaddci	|- ( M + N ) = ; D C

Proof

Step	Hyp	Ref	Expression
1		decaddi.1	|- A e. NN0
2		decaddi.2	|- B e. NN0
3		decaddi.3	|- N e. NN0
4		decaddi.4	|- M = ; A B
5		decaddci.5	|- ( A + 1 ) = D
6		decaddci.6	|- C e. NN0
7		decaddci.7	|- ( B + N ) = ; 1 C
8		0nn0	|- 0 e. NN0
9	3	dec0h	|- N = ; 0 N
10	1	nn0cni	|- A e. CC
11	10	addid1i	|- ( A + 0 ) = A
12	11	oveq1i	|- ( ( A + 0 ) + 1 ) = ( A + 1 )
13	12 5	eqtri	|- ( ( A + 0 ) + 1 ) = D
14	1 2 8 3 4 9 13 6 7	decaddc	|- ( M + N ) = ; D C