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	⊢ ( 𝐴 + 𝐵 ) = 𝐹
	unitadd.2	⊢ ( 𝐶 + 1 ) = 𝐵
	unitadd.3	⊢ 𝐴 ∈ ℕ0
	unitadd.4	⊢ 𝐶 ∈ ℕ0
Assertion	unitadd	⊢ ( ( 𝐴 + 𝐶 ) + 1 ) = 𝐹

Proof

Step	Hyp	Ref	Expression
1		unitadd.1	⊢ ( 𝐴 + 𝐵 ) = 𝐹
2		unitadd.2	⊢ ( 𝐶 + 1 ) = 𝐵
3		unitadd.3	⊢ 𝐴 ∈ ℕ0
4		unitadd.4	⊢ 𝐶 ∈ ℕ0
5	3	nn0cni	⊢ 𝐴 ∈ ℂ
6	4	nn0cni	⊢ 𝐶 ∈ ℂ
7		ax-1cn	⊢ 1 ∈ ℂ
8	5 6 7	addassi	⊢ ( ( 𝐴 + 𝐶 ) + 1 ) = ( 𝐴 + ( 𝐶 + 1 ) )
9	2	eqcomi	⊢ 𝐵 = ( 𝐶 + 1 )
10	9	oveq2i	⊢ ( 𝐴 + 𝐵 ) = ( 𝐴 + ( 𝐶 + 1 ) )
11	10 1	eqtr3i	⊢ ( 𝐴 + ( 𝐶 + 1 ) ) = 𝐹
12	8 11	eqtri	⊢ ( ( 𝐴 + 𝐶 ) + 1 ) = 𝐹