Theorem decaddi

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
	decaddi.5	|- ( B + N ) = C
Assertion	decaddi	|- ( M + N ) = ; A 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		decaddi.5	|- ( B + N ) = C
6		0nn0	|- 0 e. NN0
7	3	dec0h	|- N = ; 0 N
8	1	nn0cni	|- A e. CC
9	8	addid1i	|- ( A + 0 ) = A
10	1 2 6 3 4 7 9 5	decadd	|- ( M + N ) = ; A C