sadadd

Description: For sequences that correspond to valid integers, the adder sequence function produces the sequence for the sum. This is effectively a proof of the correctness of the ripple carry adder, implemented with logic gates corresponding to df-had and df-cad .

It is interesting to consider in what sense the sadd function can be said to be "adding" things outside the range of the bits function, that is, when adding sequences that are not eventually constant and so do not denote any integer. The correct interpretation is that the sequences are representations of 2-adic integers, which have a natural ring structure. (Contributed by Mario Carneiro, 9-Sep-2016)

		Ref	Expression
	Assertion	sadadd	$⊢ (A \in ℤ \land B \in ℤ) \to bits (A) sadd bits (B) = bits (A + B)$

Proof

Step	Hyp	Ref	Expression
1		bitsss	$⊢ bits (A) \subseteq ℕ_{0}$
2		bitsss	$⊢ bits (B) \subseteq ℕ_{0}$
3		sadcl	$⊢ (bits (A) \subseteq ℕ_{0} \land bits (B) \subseteq ℕ_{0}) \to bits (A) sadd bits (B) \subseteq ℕ_{0}$
4	1 2 3	mp2an	$⊢ bits (A) sadd bits (B) \subseteq ℕ_{0}$
5	4	sseli	$⊢ k \in (bits (A) sadd bits (B)) \to k \in ℕ_{0}$
6	5	a1i	$⊢ (A \in ℤ \land B \in ℤ) \to (k \in (bits (A) sadd bits (B)) \to k \in ℕ_{0})$
7		bitsss	$⊢ bits (A + B) \subseteq ℕ_{0}$
8	7	sseli	$⊢ k \in bits (A + B) \to k \in ℕ_{0}$
9	8	a1i	$⊢ (A \in ℤ \land B \in ℤ) \to (k \in bits (A + B) \to k \in ℕ_{0})$
10		eqid	$⊢ seq 0 ((c \in 2_{𝑜}, m \in ℕ_{0} ⟼ if (cadd (m \in bits (A), m \in bits (B), \emptyset \in c), 1_{𝑜}, \emptyset)), (n \in ℕ_{0} ⟼ if (n = 0, \emptyset, n - 1))) = seq 0 ((c \in 2_{𝑜}, m \in ℕ_{0} ⟼ if (cadd (m \in bits (A), m \in bits (B), \emptyset \in c), 1_{𝑜}, \emptyset)), (n \in ℕ_{0} ⟼ if (n = 0, \emptyset, n - 1)))$
11		eqid	$⊢ {({bits ↾}_{ℕ_{0}})}^{-1} = {({bits ↾}_{ℕ_{0}})}^{-1}$
12		simpll	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to A \in ℤ$
13		simplr	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to B \in ℤ$
14		simpr	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to k \in ℕ_{0}$
15		1nn0	$⊢ 1 \in ℕ_{0}$
16	15	a1i	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to 1 \in ℕ_{0}$
17	14 16	nn0addcld	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to k + 1 \in ℕ_{0}$
18	10 11 12 13 17	sadaddlem	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to (bits (A) sadd bits (B)) \cap (0 ..^k + 1) = bits ((A + B) \mod 2^{k + 1})$
19	12 13	zaddcld	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to A + B \in ℤ$
20		bitsmod	$⊢ (A + B \in ℤ \land k + 1 \in ℕ_{0}) \to bits ((A + B) \mod 2^{k + 1}) = bits (A + B) \cap (0 ..^k + 1)$
21	19 17 20	syl2anc	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to bits ((A + B) \mod 2^{k + 1}) = bits (A + B) \cap (0 ..^k + 1)$
22	18 21	eqtrd	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to (bits (A) sadd bits (B)) \cap (0 ..^k + 1) = bits (A + B) \cap (0 ..^k + 1)$
23	22	eleq2d	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to (k \in ((bits (A) sadd bits (B)) \cap (0 ..^k + 1)) \leftrightarrow k \in (bits (A + B) \cap (0 ..^k + 1)))$
24		elin	$⊢ k \in ((bits (A) sadd bits (B)) \cap (0 ..^k + 1)) \leftrightarrow (k \in (bits (A) sadd bits (B)) \land k \in (0 ..^k + 1))$
25		elin	$⊢ k \in (bits (A + B) \cap (0 ..^k + 1)) \leftrightarrow (k \in bits (A + B) \land k \in (0 ..^k + 1))$
26	23 24 25	3bitr3g	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to ((k \in (bits (A) sadd bits (B)) \land k \in (0 ..^k + 1)) \leftrightarrow (k \in bits (A + B) \land k \in (0 ..^k + 1)))$
27		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
28	14 27	eleqtrdi	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to k \in ℤ_{\geq 0}$
29		eluzfz2	$⊢ k \in ℤ_{\geq 0} \to k \in (0 \dots k)$
30	28 29	syl	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to k \in (0 \dots k)$
31	14	nn0zd	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to k \in ℤ$
32		fzval3	$⊢ k \in ℤ \to (0 \dots k) = (0 ..^k + 1)$
33	31 32	syl	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to (0 \dots k) = (0 ..^k + 1)$
34	30 33	eleqtrd	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to k \in (0 ..^k + 1)$
35	34	biantrud	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to (k \in (bits (A) sadd bits (B)) \leftrightarrow (k \in (bits (A) sadd bits (B)) \land k \in (0 ..^k + 1)))$
36	34	biantrud	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to (k \in bits (A + B) \leftrightarrow (k \in bits (A + B) \land k \in (0 ..^k + 1)))$
37	26 35 36	3bitr4d	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to (k \in (bits (A) sadd bits (B)) \leftrightarrow k \in bits (A + B))$
38	37	ex	$⊢ (A \in ℤ \land B \in ℤ) \to (k \in ℕ_{0} \to (k \in (bits (A) sadd bits (B)) \leftrightarrow k \in bits (A + B)))$
39	6 9 38	pm5.21ndd	$⊢ (A \in ℤ \land B \in ℤ) \to (k \in (bits (A) sadd bits (B)) \leftrightarrow k \in bits (A + B))$
40	39	eqrdv	$⊢ (A \in ℤ \land B \in ℤ) \to bits (A) sadd bits (B) = bits (A + B)$

Metamath Proof Explorer

Theorem sadadd

Proof