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

Metamath Proof Explorer

Theorem sadaddlem

Proof