sadadd3

Description: Sum of initial segments of the sadd sequence. (Contributed by Mario Carneiro, 9-Sep-2016)

	Ref	Expression
Hypotheses	sadval.a	$⊢ φ \to A \subseteq ℕ_{0}$
	sadval.b	$⊢ φ \to B \subseteq ℕ_{0}$
	sadval.c	$⊢ C = seq 0 ((c \in 2_{𝑜}, m \in ℕ_{0} ⟼ if (cadd (m \in A, m \in B, \emptyset \in c), 1_{𝑜}, \emptyset)), (n \in ℕ_{0} ⟼ if (n = 0, \emptyset, n - 1)))$
	sadcp1.n	$⊢ φ \to N \in ℕ_{0}$
	sadcadd.k	$⊢ K = {({bits ↾}_{ℕ_{0}})}^{-1}$
Assertion	sadadd3	$⊢ φ \to K ((A sadd B) \cap (0 ..^N)) \mod 2^{N} = (K (A \cap (0 ..^N)) + K (B \cap (0 ..^N))) \mod 2^{N}$

Proof

Step	Hyp	Ref	Expression
1		sadval.a	$⊢ φ \to A \subseteq ℕ_{0}$
2		sadval.b	$⊢ φ \to B \subseteq ℕ_{0}$
3		sadval.c	$⊢ C = seq 0 ((c \in 2_{𝑜}, m \in ℕ_{0} ⟼ if (cadd (m \in A, m \in B, \emptyset \in c), 1_{𝑜}, \emptyset)), (n \in ℕ_{0} ⟼ if (n = 0, \emptyset, n - 1)))$
4		sadcp1.n	$⊢ φ \to N \in ℕ_{0}$
5		sadcadd.k	$⊢ K = {({bits ↾}_{ℕ_{0}})}^{-1}$
6		2nn	$⊢ 2 \in ℕ$
7	6	a1i	$⊢ φ \to 2 \in ℕ$
8	7 4	nnexpcld	$⊢ φ \to 2^{N} \in ℕ$
9	8	nnzd	$⊢ φ \to 2^{N} \in ℤ$
10		iddvds	$⊢ 2^{N} \in ℤ \to 2^{N} ∥ 2^{N}$
11	9 10	syl	$⊢ φ \to 2^{N} ∥ 2^{N}$
12		dvds0	$⊢ 2^{N} \in ℤ \to 2^{N} ∥ 0$
13	9 12	syl	$⊢ φ \to 2^{N} ∥ 0$
14		breq2	$⊢ 2^{N} = if (\emptyset \in C (N), 2^{N}, 0) \to (2^{N} ∥ 2^{N} \leftrightarrow 2^{N} ∥ if (\emptyset \in C (N), 2^{N}, 0))$
15		breq2	$⊢ 0 = if (\emptyset \in C (N), 2^{N}, 0) \to (2^{N} ∥ 0 \leftrightarrow 2^{N} ∥ if (\emptyset \in C (N), 2^{N}, 0))$
16	14 15	ifboth	$⊢ (2^{N} ∥ 2^{N} \land 2^{N} ∥ 0) \to 2^{N} ∥ if (\emptyset \in C (N), 2^{N}, 0)$
17	11 13 16	syl2anc	$⊢ φ \to 2^{N} ∥ if (\emptyset \in C (N), 2^{N}, 0)$
18		inss1	$⊢ (A sadd B) \cap (0 ..^N) \subseteq A sadd B$
19	1 2 3	sadfval	$⊢ φ \to A sadd B = \{k \in ℕ_{0} \| hadd (k \in A, k \in B, \emptyset \in C (k))\}$
20		ssrab2	$⊢ \{k \in ℕ_{0} \| hadd (k \in A, k \in B, \emptyset \in C (k))\} \subseteq ℕ_{0}$
21	19 20	eqsstrdi	$⊢ φ \to A sadd B \subseteq ℕ_{0}$
22	18 21	sstrid	$⊢ φ \to (A sadd B) \cap (0 ..^N) \subseteq ℕ_{0}$
23		fzofi	$⊢ (0 ..^N) \in Fin$
24	23	a1i	$⊢ φ \to (0 ..^N) \in Fin$
25		inss2	$⊢ (A sadd B) \cap (0 ..^N) \subseteq (0 ..^N)$
26		ssfi	$⊢ ((0 ..^N) \in Fin \land (A sadd B) \cap (0 ..^N) \subseteq (0 ..^N)) \to (A sadd B) \cap (0 ..^N) \in Fin$
27	24 25 26	sylancl	$⊢ φ \to (A sadd B) \cap (0 ..^N) \in Fin$
28		elfpw	$⊢ (A sadd B) \cap (0 ..^N) \in (𝒫 ℕ_{0} \cap Fin) \leftrightarrow ((A sadd B) \cap (0 ..^N) \subseteq ℕ_{0} \land (A sadd B) \cap (0 ..^N) \in Fin)$
29	22 27 28	sylanbrc	$⊢ φ \to (A sadd B) \cap (0 ..^N) \in (𝒫 ℕ_{0} \cap Fin)$
30		bitsf1o	$⊢ ({bits ↾}_{ℕ_{0}}) : ℕ_{0} \underset{1-1 onto}{⟶} 𝒫 ℕ_{0} \cap Fin$
31		f1ocnv	$⊢ ({bits ↾}_{ℕ_{0}}) : ℕ_{0} \underset{1-1 onto}{⟶} 𝒫 ℕ_{0} \cap Fin \to {({bits ↾}_{ℕ_{0}})}^{-1} : 𝒫 ℕ_{0} \cap Fin \underset{1-1 onto}{⟶} ℕ_{0}$
32		f1of	$⊢ {({bits ↾}_{ℕ_{0}})}^{-1} : 𝒫 ℕ_{0} \cap Fin \underset{1-1 onto}{⟶} ℕ_{0} \to {({bits ↾}_{ℕ_{0}})}^{-1} : 𝒫 ℕ_{0} \cap Fin ⟶ ℕ_{0}$
33	30 31 32	mp2b	$⊢ {({bits ↾}_{ℕ_{0}})}^{-1} : 𝒫 ℕ_{0} \cap Fin ⟶ ℕ_{0}$
34	5	feq1i	$⊢ K : 𝒫 ℕ_{0} \cap Fin ⟶ ℕ_{0} \leftrightarrow {({bits ↾}_{ℕ_{0}})}^{-1} : 𝒫 ℕ_{0} \cap Fin ⟶ ℕ_{0}$
35	33 34	mpbir	$⊢ K : 𝒫 ℕ_{0} \cap Fin ⟶ ℕ_{0}$
36	35	ffvelcdmi	$⊢ (A sadd B) \cap (0 ..^N) \in (𝒫 ℕ_{0} \cap Fin) \to K ((A sadd B) \cap (0 ..^N)) \in ℕ_{0}$
37	29 36	syl	$⊢ φ \to K ((A sadd B) \cap (0 ..^N)) \in ℕ_{0}$
38	37	nn0cnd	$⊢ φ \to K ((A sadd B) \cap (0 ..^N)) \in ℂ$
39	8	nncnd	$⊢ φ \to 2^{N} \in ℂ$
40		0cn	$⊢ 0 \in ℂ$
41		ifcl	$⊢ (2^{N} \in ℂ \land 0 \in ℂ) \to if (\emptyset \in C (N), 2^{N}, 0) \in ℂ$
42	39 40 41	sylancl	$⊢ φ \to if (\emptyset \in C (N), 2^{N}, 0) \in ℂ$
43	38 42	pncan2d	$⊢ φ \to K ((A sadd B) \cap (0 ..^N)) + if (\emptyset \in C (N), 2^{N}, 0) - K ((A sadd B) \cap (0 ..^N)) = if (\emptyset \in C (N), 2^{N}, 0)$
44	17 43	breqtrrd	$⊢ φ \to 2^{N} ∥ (K ((A sadd B) \cap (0 ..^N)) + if (\emptyset \in C (N), 2^{N}, 0) - K ((A sadd B) \cap (0 ..^N)))$
45	37	nn0zd	$⊢ φ \to K ((A sadd B) \cap (0 ..^N)) \in ℤ$
46	9	adantr	$⊢ (φ \land \emptyset \in C (N)) \to 2^{N} \in ℤ$
47		0zd	$⊢ (φ \land \neg \emptyset \in C (N)) \to 0 \in ℤ$
48	46 47	ifclda	$⊢ φ \to if (\emptyset \in C (N), 2^{N}, 0) \in ℤ$
49	45 48	zaddcld	$⊢ φ \to K ((A sadd B) \cap (0 ..^N)) + if (\emptyset \in C (N), 2^{N}, 0) \in ℤ$
50		moddvds	$⊢ (2^{N} \in ℕ \land K ((A sadd B) \cap (0 ..^N)) + if (\emptyset \in C (N), 2^{N}, 0) \in ℤ \land K ((A sadd B) \cap (0 ..^N)) \in ℤ) \to ((K ((A sadd B) \cap (0 ..^N)) + if (\emptyset \in C (N), 2^{N}, 0)) \mod 2^{N} = K ((A sadd B) \cap (0 ..^N)) \mod 2^{N} \leftrightarrow 2^{N} ∥ (K ((A sadd B) \cap (0 ..^N)) + if (\emptyset \in C (N), 2^{N}, 0) - K ((A sadd B) \cap (0 ..^N))))$
51	8 49 45 50	syl3anc	$⊢ φ \to ((K ((A sadd B) \cap (0 ..^N)) + if (\emptyset \in C (N), 2^{N}, 0)) \mod 2^{N} = K ((A sadd B) \cap (0 ..^N)) \mod 2^{N} \leftrightarrow 2^{N} ∥ (K ((A sadd B) \cap (0 ..^N)) + if (\emptyset \in C (N), 2^{N}, 0) - K ((A sadd B) \cap (0 ..^N))))$
52	44 51	mpbird	$⊢ φ \to (K ((A sadd B) \cap (0 ..^N)) + if (\emptyset \in C (N), 2^{N}, 0)) \mod 2^{N} = K ((A sadd B) \cap (0 ..^N)) \mod 2^{N}$
53	1 2 3 4 5	sadadd2	$⊢ φ \to K ((A sadd B) \cap (0 ..^N)) + if (\emptyset \in C (N), 2^{N}, 0) = K (A \cap (0 ..^N)) + K (B \cap (0 ..^N))$
54	53	oveq1d	$⊢ φ \to (K ((A sadd B) \cap (0 ..^N)) + if (\emptyset \in C (N), 2^{N}, 0)) \mod 2^{N} = (K (A \cap (0 ..^N)) + K (B \cap (0 ..^N))) \mod 2^{N}$
55	52 54	eqtr3d	$⊢ φ \to K ((A sadd B) \cap (0 ..^N)) \mod 2^{N} = (K (A \cap (0 ..^N)) + K (B \cap (0 ..^N))) \mod 2^{N}$

Metamath Proof Explorer

Theorem sadadd3

Proof