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\in {\mathbb{N}}_0$$
	unitadd.4	$$⊢C\in {\mathbb{N}}_0$$
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\in {\mathbb{N}}_0$$
4		unitadd.4	$$⊢C\in {\mathbb{N}}_0$$
5	3	nn0cni	$$⊢A\in ℂ$$
6	4	nn0cni	$$⊢C\in ℂ$$
7		ax-1cn	$$⊢1\in ℂ$$
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$$