Theorem sadval

Description: The full adder sequence is the half adder function applied to the inputs and the carry sequence. (Contributed by Mario Carneiro, 5-Sep-2016)

	Ref	Expression
Hypotheses	sadval.a	$$⊢\phi \to A\subseteq {\mathbb{N}}_0$$
	sadval.b	$$⊢\phi \to B\subseteq {\mathbb{N}}_0$$
	sadval.c	$$⊢C=seq0\left(\left(c\in 2_{𝑜},m\in {\mathbb{N}}_0⟼if\left(cadd\left(m\in A,m\in B,\varnothing \in c\right),1_{𝑜},\varnothing \right)\right),\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\right)$$
	sadcp1.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
Assertion	sadval	$$⊢\phi \to \left(N\in \left(A\mathrm{sadd}B\right)\leftrightarrow hadd\left(N\in A,N\in B,\varnothing \in C\left(N\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		sadval.a	$$⊢\phi \to A\subseteq {\mathbb{N}}_0$$
2		sadval.b	$$⊢\phi \to B\subseteq {\mathbb{N}}_0$$
3		sadval.c	$$⊢C=seq0\left(\left(c\in 2_{𝑜},m\in {\mathbb{N}}_0⟼if\left(cadd\left(m\in A,m\in B,\varnothing \in c\right),1_{𝑜},\varnothing \right)\right),\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\right)$$
4		sadcp1.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
5	1 2 3	sadfval	$$⊢\phi \to A\mathrm{sadd}B=\left\{k\in {\mathbb{N}}_0|hadd\left(k\in A,k\in B,\varnothing \in C\left(k\right)\right)\right\}$$
6	5	eleq2d	$$⊢\phi \to \left(N\in \left(A\mathrm{sadd}B\right)\leftrightarrow N\in \left\{k\in {\mathbb{N}}_0|hadd\left(k\in A,k\in B,\varnothing \in C\left(k\right)\right)\right\}\right)$$
7		eleq1	$$⊢k=N\to \left(k\in A\leftrightarrow N\in A\right)$$
8		eleq1	$$⊢k=N\to \left(k\in B\leftrightarrow N\in B\right)$$
9		fveq2	$$⊢k=N\to C\left(k\right)=C\left(N\right)$$
10	9	eleq2d	$$⊢k=N\to \left(\varnothing \in C\left(k\right)\leftrightarrow \varnothing \in C\left(N\right)\right)$$
11	7 8 10	hadbi123d	$$⊢k=N\to \left(hadd\left(k\in A,k\in B,\varnothing \in C\left(k\right)\right)\leftrightarrow hadd\left(N\in A,N\in B,\varnothing \in C\left(N\right)\right)\right)$$
12	11	elrab3	$$⊢N\in {\mathbb{N}}_0\to \left(N\in \left\{k\in {\mathbb{N}}_0|hadd\left(k\in A,k\in B,\varnothing \in C\left(k\right)\right)\right\}\leftrightarrow hadd\left(N\in A,N\in B,\varnothing \in C\left(N\right)\right)\right)$$
13	4 12	syl	$$⊢\phi \to \left(N\in \left\{k\in {\mathbb{N}}_0|hadd\left(k\in A,k\in B,\varnothing \in C\left(k\right)\right)\right\}\leftrightarrow hadd\left(N\in A,N\in B,\varnothing \in C\left(N\right)\right)\right)$$
14	6 13	bitrd	$$⊢\phi \to \left(N\in \left(A\mathrm{sadd}B\right)\leftrightarrow hadd\left(N\in A,N\in B,\varnothing \in C\left(N\right)\right)\right)$$