Theorem unitadd

Description: Theorem used in conjunction with decaddc to absorb carry when generating n-digit addition synthetic proofs. (Contributed by Stanislas Polu, 7-Apr-2020)

	Ref	Expression
Hypotheses	unitadd.1	|- ( A + B ) = F
	unitadd.2	|- ( C + 1 ) = B
	unitadd.3	|- A e. NN0
	unitadd.4	|- C e. NN0
Assertion	unitadd	|- ( ( A + C ) + 1 ) = F

Proof

Step	Hyp	Ref	Expression
1		unitadd.1	|- ( A + B ) = F
2		unitadd.2	|- ( C + 1 ) = B
3		unitadd.3	|- A e. NN0
4		unitadd.4	|- C e. NN0
5	3	nn0cni	|- A e. CC
6	4	nn0cni	|- C e. CC
7		ax-1cn	|- 1 e. CC
8	5 6 7	addassi	|- ( ( A + C ) + 1 ) = ( A + ( C + 1 ) )
9	2	eqcomi	|- B = ( C + 1 )
10	9	oveq2i	|- ( A + B ) = ( A + ( C + 1 ) )
11	10 1	eqtr3i	|- ( A + ( C + 1 ) ) = F
12	8 11	eqtri	|- ( ( A + C ) + 1 ) = F