sadaddlem

	Ref	Expression
Hypotheses	sadaddlem.c	$⊢ C = 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)))$
	sadaddlem.k	$⊢ K = {({bits ↾}_{ℕ_{0}})}^{-1}$
	sadaddlem.1	$⊢ φ \to A \in ℤ$
	sadaddlem.2	$⊢ φ \to B \in ℤ$
	sadaddlem.3	$⊢ φ \to N \in ℕ_{0}$
Assertion	sadaddlem	$⊢ φ \to (bits (A) sadd bits (B)) \cap (0 ..^N) = bits ((A + B) \mod 2^{N})$

Proof

Step	Hyp	Ref	Expression
1		sadaddlem.c	$⊢ C = 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)))$
2		sadaddlem.k	$⊢ K = {({bits ↾}_{ℕ_{0}})}^{-1}$
3		sadaddlem.1	$⊢ φ \to A \in ℤ$
4		sadaddlem.2	$⊢ φ \to B \in ℤ$
5		sadaddlem.3	$⊢ φ \to N \in ℕ_{0}$
6	2	fveq1i	$⊢ K (bits (A) \cap (0 ..^N)) = {({bits ↾}_{ℕ_{0}})}^{-1} (bits (A) \cap (0 ..^N))$
7		2nn	$⊢ 2 \in ℕ$
8	7	a1i	$⊢ φ \to 2 \in ℕ$
9	8 5	nnexpcld	$⊢ φ \to 2^{N} \in ℕ$
10	3 9	zmodcld	$⊢ φ \to A \mod 2^{N} \in ℕ_{0}$
11	10	fvresd	$⊢ φ \to ({bits ↾}_{ℕ_{0}}) (A \mod 2^{N}) = bits (A \mod 2^{N})$
12		bitsmod	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to bits (A \mod 2^{N}) = bits (A) \cap (0 ..^N)$
13	3 5 12	syl2anc	$⊢ φ \to bits (A \mod 2^{N}) = bits (A) \cap (0 ..^N)$
14	11 13	eqtrd	$⊢ φ \to ({bits ↾}_{ℕ_{0}}) (A \mod 2^{N}) = bits (A) \cap (0 ..^N)$
15		bitsf1o	$⊢ ({bits ↾}_{ℕ_{0}}) : ℕ_{0} \underset{1-1 onto}{⟶} 𝒫 ℕ_{0} \cap Fin$
16		f1ocnvfv	$⊢ (({bits ↾}_{ℕ_{0}}) : ℕ_{0} \underset{1-1 onto}{⟶} 𝒫 ℕ_{0} \cap Fin \land A \mod 2^{N} \in ℕ_{0}) \to (({bits ↾}_{ℕ_{0}}) (A \mod 2^{N}) = bits (A) \cap (0 ..^N) \to {({bits ↾}_{ℕ_{0}})}^{-1} (bits (A) \cap (0 ..^N)) = A \mod 2^{N})$
17	15 10 16	sylancr	$⊢ φ \to (({bits ↾}_{ℕ_{0}}) (A \mod 2^{N}) = bits (A) \cap (0 ..^N) \to {({bits ↾}_{ℕ_{0}})}^{-1} (bits (A) \cap (0 ..^N)) = A \mod 2^{N})$
18	14 17	mpd	$⊢ φ \to {({bits ↾}_{ℕ_{0}})}^{-1} (bits (A) \cap (0 ..^N)) = A \mod 2^{N}$
19	6 18	syl5eq	$⊢ φ \to K (bits (A) \cap (0 ..^N)) = A \mod 2^{N}$
20	19	oveq2d	$⊢ φ \to A - K (bits (A) \cap (0 ..^N)) = A - (A \mod 2^{N})$
21	20	oveq1d	$⊢ φ \to \frac{A - K (bits (A) \cap (0 ..^N))}{2^{N}} = \frac{A - (A \mod 2^{N})}{2^{N}}$
22	3	zred	$⊢ φ \to A \in ℝ$
23	9	nnrpd	$⊢ φ \to 2^{N} \in ℝ^{+}$
24		moddifz	$⊢ (A \in ℝ \land 2^{N} \in ℝ^{+}) \to \frac{A - (A \mod 2^{N})}{2^{N}} \in ℤ$
25	22 23 24	syl2anc	$⊢ φ \to \frac{A - (A \mod 2^{N})}{2^{N}} \in ℤ$
26	21 25	eqeltrd	$⊢ φ \to \frac{A - K (bits (A) \cap (0 ..^N))}{2^{N}} \in ℤ$
27	9	nnzd	$⊢ φ \to 2^{N} \in ℤ$
28	9	nnne0d	$⊢ φ \to 2^{N} \neq 0$
29		inss1	$⊢ bits (A) \cap (0 ..^N) \subseteq bits (A)$
30		bitsss	$⊢ bits (A) \subseteq ℕ_{0}$
31	29 30	sstri	$⊢ bits (A) \cap (0 ..^N) \subseteq ℕ_{0}$
32		fzofi	$⊢ (0 ..^N) \in Fin$
33		inss2	$⊢ bits (A) \cap (0 ..^N) \subseteq (0 ..^N)$
34		ssfi	$⊢ ((0 ..^N) \in Fin \land bits (A) \cap (0 ..^N) \subseteq (0 ..^N)) \to bits (A) \cap (0 ..^N) \in Fin$
35	32 33 34	mp2an	$⊢ bits (A) \cap (0 ..^N) \in Fin$
36		elfpw	$⊢ bits (A) \cap (0 ..^N) \in (𝒫 ℕ_{0} \cap Fin) \leftrightarrow (bits (A) \cap (0 ..^N) \subseteq ℕ_{0} \land bits (A) \cap (0 ..^N) \in Fin)$
37	31 35 36	mpbir2an	$⊢ bits (A) \cap (0 ..^N) \in (𝒫 ℕ_{0} \cap Fin)$
38		f1ocnv	$⊢ ({bits ↾}_{ℕ_{0}}) : ℕ_{0} \underset{1-1 onto}{⟶} 𝒫 ℕ_{0} \cap Fin \to {({bits ↾}_{ℕ_{0}})}^{-1} : 𝒫 ℕ_{0} \cap Fin \underset{1-1 onto}{⟶} ℕ_{0}$
39		f1of	$⊢ {({bits ↾}_{ℕ_{0}})}^{-1} : 𝒫 ℕ_{0} \cap Fin \underset{1-1 onto}{⟶} ℕ_{0} \to {({bits ↾}_{ℕ_{0}})}^{-1} : 𝒫 ℕ_{0} \cap Fin ⟶ ℕ_{0}$
40	15 38 39	mp2b	$⊢ {({bits ↾}_{ℕ_{0}})}^{-1} : 𝒫 ℕ_{0} \cap Fin ⟶ ℕ_{0}$
41	2	feq1i	$⊢ K : 𝒫 ℕ_{0} \cap Fin ⟶ ℕ_{0} \leftrightarrow {({bits ↾}_{ℕ_{0}})}^{-1} : 𝒫 ℕ_{0} \cap Fin ⟶ ℕ_{0}$
42	40 41	mpbir	$⊢ K : 𝒫 ℕ_{0} \cap Fin ⟶ ℕ_{0}$
43	42	ffvelrni	$⊢ bits (A) \cap (0 ..^N) \in (𝒫 ℕ_{0} \cap Fin) \to K (bits (A) \cap (0 ..^N)) \in ℕ_{0}$
44	37 43	mp1i	$⊢ φ \to K (bits (A) \cap (0 ..^N)) \in ℕ_{0}$
45	44	nn0zd	$⊢ φ \to K (bits (A) \cap (0 ..^N)) \in ℤ$
46	3 45	zsubcld	$⊢ φ \to A - K (bits (A) \cap (0 ..^N)) \in ℤ$
47		dvdsval2	$⊢ (2^{N} \in ℤ \land 2^{N} \neq 0 \land A - K (bits (A) \cap (0 ..^N)) \in ℤ) \to (2^{N} ∥ (A - K (bits (A) \cap (0 ..^N))) \leftrightarrow \frac{A - K (bits (A) \cap (0 ..^N))}{2^{N}} \in ℤ)$
48	27 28 46 47	syl3anc	$⊢ φ \to (2^{N} ∥ (A - K (bits (A) \cap (0 ..^N))) \leftrightarrow \frac{A - K (bits (A) \cap (0 ..^N))}{2^{N}} \in ℤ)$
49	26 48	mpbird	$⊢ φ \to 2^{N} ∥ (A - K (bits (A) \cap (0 ..^N)))$
50	2	fveq1i	$⊢ K (bits (B) \cap (0 ..^N)) = {({bits ↾}_{ℕ_{0}})}^{-1} (bits (B) \cap (0 ..^N))$
51	4 9	zmodcld	$⊢ φ \to B \mod 2^{N} \in ℕ_{0}$
52	51	fvresd	$⊢ φ \to ({bits ↾}_{ℕ_{0}}) (B \mod 2^{N}) = bits (B \mod 2^{N})$
53		bitsmod	$⊢ (B \in ℤ \land N \in ℕ_{0}) \to bits (B \mod 2^{N}) = bits (B) \cap (0 ..^N)$
54	4 5 53	syl2anc	$⊢ φ \to bits (B \mod 2^{N}) = bits (B) \cap (0 ..^N)$
55	52 54	eqtrd	$⊢ φ \to ({bits ↾}_{ℕ_{0}}) (B \mod 2^{N}) = bits (B) \cap (0 ..^N)$
56		f1ocnvfv	$⊢ (({bits ↾}_{ℕ_{0}}) : ℕ_{0} \underset{1-1 onto}{⟶} 𝒫 ℕ_{0} \cap Fin \land B \mod 2^{N} \in ℕ_{0}) \to (({bits ↾}_{ℕ_{0}}) (B \mod 2^{N}) = bits (B) \cap (0 ..^N) \to {({bits ↾}_{ℕ_{0}})}^{-1} (bits (B) \cap (0 ..^N)) = B \mod 2^{N})$
57	15 51 56	sylancr	$⊢ φ \to (({bits ↾}_{ℕ_{0}}) (B \mod 2^{N}) = bits (B) \cap (0 ..^N) \to {({bits ↾}_{ℕ_{0}})}^{-1} (bits (B) \cap (0 ..^N)) = B \mod 2^{N})$
58	55 57	mpd	$⊢ φ \to {({bits ↾}_{ℕ_{0}})}^{-1} (bits (B) \cap (0 ..^N)) = B \mod 2^{N}$
59	50 58	syl5eq	$⊢ φ \to K (bits (B) \cap (0 ..^N)) = B \mod 2^{N}$
60	59	oveq2d	$⊢ φ \to B - K (bits (B) \cap (0 ..^N)) = B - (B \mod 2^{N})$
61	60	oveq1d	$⊢ φ \to \frac{B - K (bits (B) \cap (0 ..^N))}{2^{N}} = \frac{B - (B \mod 2^{N})}{2^{N}}$
62	4	zred	$⊢ φ \to B \in ℝ$
63		moddifz	$⊢ (B \in ℝ \land 2^{N} \in ℝ^{+}) \to \frac{B - (B \mod 2^{N})}{2^{N}} \in ℤ$
64	62 23 63	syl2anc	$⊢ φ \to \frac{B - (B \mod 2^{N})}{2^{N}} \in ℤ$
65	61 64	eqeltrd	$⊢ φ \to \frac{B - K (bits (B) \cap (0 ..^N))}{2^{N}} \in ℤ$
66		inss1	$⊢ bits (B) \cap (0 ..^N) \subseteq bits (B)$
67		bitsss	$⊢ bits (B) \subseteq ℕ_{0}$
68	66 67	sstri	$⊢ bits (B) \cap (0 ..^N) \subseteq ℕ_{0}$
69		inss2	$⊢ bits (B) \cap (0 ..^N) \subseteq (0 ..^N)$
70		ssfi	$⊢ ((0 ..^N) \in Fin \land bits (B) \cap (0 ..^N) \subseteq (0 ..^N)) \to bits (B) \cap (0 ..^N) \in Fin$
71	32 69 70	mp2an	$⊢ bits (B) \cap (0 ..^N) \in Fin$
72		elfpw	$⊢ bits (B) \cap (0 ..^N) \in (𝒫 ℕ_{0} \cap Fin) \leftrightarrow (bits (B) \cap (0 ..^N) \subseteq ℕ_{0} \land bits (B) \cap (0 ..^N) \in Fin)$
73	68 71 72	mpbir2an	$⊢ bits (B) \cap (0 ..^N) \in (𝒫 ℕ_{0} \cap Fin)$
74	42	ffvelrni	$⊢ bits (B) \cap (0 ..^N) \in (𝒫 ℕ_{0} \cap Fin) \to K (bits (B) \cap (0 ..^N)) \in ℕ_{0}$
75	73 74	mp1i	$⊢ φ \to K (bits (B) \cap (0 ..^N)) \in ℕ_{0}$
76	75	nn0zd	$⊢ φ \to K (bits (B) \cap (0 ..^N)) \in ℤ$
77	4 76	zsubcld	$⊢ φ \to B - K (bits (B) \cap (0 ..^N)) \in ℤ$
78		dvdsval2	$⊢ (2^{N} \in ℤ \land 2^{N} \neq 0 \land B - K (bits (B) \cap (0 ..^N)) \in ℤ) \to (2^{N} ∥ (B - K (bits (B) \cap (0 ..^N))) \leftrightarrow \frac{B - K (bits (B) \cap (0 ..^N))}{2^{N}} \in ℤ)$
79	27 28 77 78	syl3anc	$⊢ φ \to (2^{N} ∥ (B - K (bits (B) \cap (0 ..^N))) \leftrightarrow \frac{B - K (bits (B) \cap (0 ..^N))}{2^{N}} \in ℤ)$
80	65 79	mpbird	$⊢ φ \to 2^{N} ∥ (B - K (bits (B) \cap (0 ..^N)))$
81		dvds2add	$⊢ (2^{N} \in ℤ \land A - K (bits (A) \cap (0 ..^N)) \in ℤ \land B - K (bits (B) \cap (0 ..^N)) \in ℤ) \to ((2^{N} ∥ (A - K (bits (A) \cap (0 ..^N))) \land 2^{N} ∥ (B - K (bits (B) \cap (0 ..^N)))) \to 2^{N} ∥ ((A - K (bits (A) \cap (0 ..^N))) + B - K (bits (B) \cap (0 ..^N))))$
82	27 46 77 81	syl3anc	$⊢ φ \to ((2^{N} ∥ (A - K (bits (A) \cap (0 ..^N))) \land 2^{N} ∥ (B - K (bits (B) \cap (0 ..^N)))) \to 2^{N} ∥ ((A - K (bits (A) \cap (0 ..^N))) + B - K (bits (B) \cap (0 ..^N))))$
83	49 80 82	mp2and	$⊢ φ \to 2^{N} ∥ ((A - K (bits (A) \cap (0 ..^N))) + B - K (bits (B) \cap (0 ..^N)))$
84	3	zcnd	$⊢ φ \to A \in ℂ$
85	4	zcnd	$⊢ φ \to B \in ℂ$
86	44	nn0cnd	$⊢ φ \to K (bits (A) \cap (0 ..^N)) \in ℂ$
87	75	nn0cnd	$⊢ φ \to K (bits (B) \cap (0 ..^N)) \in ℂ$
88	84 85 86 87	addsub4d	$⊢ φ \to A + B - (K (bits (A) \cap (0 ..^N)) + K (bits (B) \cap (0 ..^N))) = (A - K (bits (A) \cap (0 ..^N))) + B - K (bits (B) \cap (0 ..^N))$
89	83 88	breqtrrd	$⊢ φ \to 2^{N} ∥ (A + B - (K (bits (A) \cap (0 ..^N)) + K (bits (B) \cap (0 ..^N))))$
90	3 4	zaddcld	$⊢ φ \to A + B \in ℤ$
91	45 76	zaddcld	$⊢ φ \to K (bits (A) \cap (0 ..^N)) + K (bits (B) \cap (0 ..^N)) \in ℤ$
92		moddvds	$⊢ (2^{N} \in ℕ \land A + B \in ℤ \land K (bits (A) \cap (0 ..^N)) + K (bits (B) \cap (0 ..^N)) \in ℤ) \to ((A + B) \mod 2^{N} = (K (bits (A) \cap (0 ..^N)) + K (bits (B) \cap (0 ..^N))) \mod 2^{N} \leftrightarrow 2^{N} ∥ (A + B - (K (bits (A) \cap (0 ..^N)) + K (bits (B) \cap (0 ..^N)))))$
93	9 90 91 92	syl3anc	$⊢ φ \to ((A + B) \mod 2^{N} = (K (bits (A) \cap (0 ..^N)) + K (bits (B) \cap (0 ..^N))) \mod 2^{N} \leftrightarrow 2^{N} ∥ (A + B - (K (bits (A) \cap (0 ..^N)) + K (bits (B) \cap (0 ..^N)))))$
94	89 93	mpbird	$⊢ φ \to (A + B) \mod 2^{N} = (K (bits (A) \cap (0 ..^N)) + K (bits (B) \cap (0 ..^N))) \mod 2^{N}$
95	30	a1i	$⊢ φ \to bits (A) \subseteq ℕ_{0}$
96	67	a1i	$⊢ φ \to bits (B) \subseteq ℕ_{0}$
97	95 96 1 5 2	sadadd3	$⊢ φ \to K ((bits (A) sadd bits (B)) \cap (0 ..^N)) \mod 2^{N} = (K (bits (A) \cap (0 ..^N)) + K (bits (B) \cap (0 ..^N))) \mod 2^{N}$
98		inss1	$⊢ (bits (A) sadd bits (B)) \cap (0 ..^N) \subseteq bits (A) sadd bits (B)$
99		sadcl	$⊢ (bits (A) \subseteq ℕ_{0} \land bits (B) \subseteq ℕ_{0}) \to bits (A) sadd bits (B) \subseteq ℕ_{0}$
100	30 67 99	mp2an	$⊢ bits (A) sadd bits (B) \subseteq ℕ_{0}$
101	98 100	sstri	$⊢ (bits (A) sadd bits (B)) \cap (0 ..^N) \subseteq ℕ_{0}$
102		inss2	$⊢ (bits (A) sadd bits (B)) \cap (0 ..^N) \subseteq (0 ..^N)$
103		ssfi	$⊢ ((0 ..^N) \in Fin \land (bits (A) sadd bits (B)) \cap (0 ..^N) \subseteq (0 ..^N)) \to (bits (A) sadd bits (B)) \cap (0 ..^N) \in Fin$
104	32 102 103	mp2an	$⊢ (bits (A) sadd bits (B)) \cap (0 ..^N) \in Fin$
105		elfpw	$⊢ (bits (A) sadd bits (B)) \cap (0 ..^N) \in (𝒫 ℕ_{0} \cap Fin) \leftrightarrow ((bits (A) sadd bits (B)) \cap (0 ..^N) \subseteq ℕ_{0} \land (bits (A) sadd bits (B)) \cap (0 ..^N) \in Fin)$
106	101 104 105	mpbir2an	$⊢ (bits (A) sadd bits (B)) \cap (0 ..^N) \in (𝒫 ℕ_{0} \cap Fin)$
107	42	ffvelrni	$⊢ (bits (A) sadd bits (B)) \cap (0 ..^N) \in (𝒫 ℕ_{0} \cap Fin) \to K ((bits (A) sadd bits (B)) \cap (0 ..^N)) \in ℕ_{0}$
108	106 107	mp1i	$⊢ φ \to K ((bits (A) sadd bits (B)) \cap (0 ..^N)) \in ℕ_{0}$
109	108	nn0red	$⊢ φ \to K ((bits (A) sadd bits (B)) \cap (0 ..^N)) \in ℝ$
110	108	nn0ge0d	$⊢ φ \to 0 \leq K ((bits (A) sadd bits (B)) \cap (0 ..^N))$
111	2	fveq1i	$⊢ K ((bits (A) sadd bits (B)) \cap (0 ..^N)) = {({bits ↾}_{ℕ_{0}})}^{-1} ((bits (A) sadd bits (B)) \cap (0 ..^N))$
112	111	fveq2i	$⊢ ({bits ↾}_{ℕ_{0}}) (K ((bits (A) sadd bits (B)) \cap (0 ..^N))) = ({bits ↾}_{ℕ_{0}}) ({({bits ↾}_{ℕ_{0}})}^{-1} ((bits (A) sadd bits (B)) \cap (0 ..^N)))$
113	108	fvresd	$⊢ φ \to ({bits ↾}_{ℕ_{0}}) (K ((bits (A) sadd bits (B)) \cap (0 ..^N))) = bits (K ((bits (A) sadd bits (B)) \cap (0 ..^N)))$
114	106	a1i	$⊢ φ \to (bits (A) sadd bits (B)) \cap (0 ..^N) \in (𝒫 ℕ_{0} \cap Fin)$
115		f1ocnvfv2	$⊢ (({bits ↾}_{ℕ_{0}}) : ℕ_{0} \underset{1-1 onto}{⟶} 𝒫 ℕ_{0} \cap Fin \land (bits (A) sadd bits (B)) \cap (0 ..^N) \in (𝒫 ℕ_{0} \cap Fin)) \to ({bits ↾}_{ℕ_{0}}) ({({bits ↾}_{ℕ_{0}})}^{-1} ((bits (A) sadd bits (B)) \cap (0 ..^N))) = (bits (A) sadd bits (B)) \cap (0 ..^N)$
116	15 114 115	sylancr	$⊢ φ \to ({bits ↾}_{ℕ_{0}}) ({({bits ↾}_{ℕ_{0}})}^{-1} ((bits (A) sadd bits (B)) \cap (0 ..^N))) = (bits (A) sadd bits (B)) \cap (0 ..^N)$
117	112 113 116	3eqtr3a	$⊢ φ \to bits (K ((bits (A) sadd bits (B)) \cap (0 ..^N))) = (bits (A) sadd bits (B)) \cap (0 ..^N)$
118	117 102	eqsstrdi	$⊢ φ \to bits (K ((bits (A) sadd bits (B)) \cap (0 ..^N))) \subseteq (0 ..^N)$
119	108	nn0zd	$⊢ φ \to K ((bits (A) sadd bits (B)) \cap (0 ..^N)) \in ℤ$
120		bitsfzo	$⊢ (K ((bits (A) sadd bits (B)) \cap (0 ..^N)) \in ℤ \land N \in ℕ_{0}) \to (K ((bits (A) sadd bits (B)) \cap (0 ..^N)) \in (0 ..^2^{N}) \leftrightarrow bits (K ((bits (A) sadd bits (B)) \cap (0 ..^N))) \subseteq (0 ..^N))$
121	119 5 120	syl2anc	$⊢ φ \to (K ((bits (A) sadd bits (B)) \cap (0 ..^N)) \in (0 ..^2^{N}) \leftrightarrow bits (K ((bits (A) sadd bits (B)) \cap (0 ..^N))) \subseteq (0 ..^N))$
122	118 121	mpbird	$⊢ φ \to K ((bits (A) sadd bits (B)) \cap (0 ..^N)) \in (0 ..^2^{N})$
123		elfzolt2	$⊢ K ((bits (A) sadd bits (B)) \cap (0 ..^N)) \in (0 ..^2^{N}) \to K ((bits (A) sadd bits (B)) \cap (0 ..^N)) < 2^{N}$
124	122 123	syl	$⊢ φ \to K ((bits (A) sadd bits (B)) \cap (0 ..^N)) < 2^{N}$
125		modid	$⊢ ((K ((bits (A) sadd bits (B)) \cap (0 ..^N)) \in ℝ \land 2^{N} \in ℝ^{+}) \land (0 \leq K ((bits (A) sadd bits (B)) \cap (0 ..^N)) \land K ((bits (A) sadd bits (B)) \cap (0 ..^N)) < 2^{N})) \to K ((bits (A) sadd bits (B)) \cap (0 ..^N)) \mod 2^{N} = K ((bits (A) sadd bits (B)) \cap (0 ..^N))$
126	109 23 110 124 125	syl22anc	$⊢ φ \to K ((bits (A) sadd bits (B)) \cap (0 ..^N)) \mod 2^{N} = K ((bits (A) sadd bits (B)) \cap (0 ..^N))$
127	94 97 126	3eqtr2d	$⊢ φ \to (A + B) \mod 2^{N} = K ((bits (A) sadd bits (B)) \cap (0 ..^N))$
128	127	fveq2d	$⊢ φ \to bits ((A + B) \mod 2^{N}) = bits (K ((bits (A) sadd bits (B)) \cap (0 ..^N)))$
129	128 117	eqtr2d	$⊢ φ \to (bits (A) sadd bits (B)) \cap (0 ..^N) = bits ((A + B) \mod 2^{N})$

Metamath Proof Explorer

Theorem sadaddlem

Proof