smumullem

	Ref	Expression
Hypotheses	smumullem.a	$⊢ φ \to A \in ℤ$
	smumullem.b	$⊢ φ \to B \in ℤ$
	smumullem.n	$⊢ φ \to N \in ℕ_{0}$
Assertion	smumullem	$⊢ φ \to (bits (A) \cap (0 ..^N)) smul bits (B) = bits ((A \mod 2^{N}) B)$

Proof

Step	Hyp	Ref	Expression
1		smumullem.a	$⊢ φ \to A \in ℤ$
2		smumullem.b	$⊢ φ \to B \in ℤ$
3		smumullem.n	$⊢ φ \to N \in ℕ_{0}$
4		oveq2	$⊢ x = 0 \to (0 ..^x) = (0 ..^0)$
5		fzo0	$⊢ (0 ..^0) = \emptyset$
6	4 5	eqtrdi	$⊢ x = 0 \to (0 ..^x) = \emptyset$
7	6	ineq2d	$⊢ x = 0 \to bits (A) \cap (0 ..^x) = bits (A) \cap \emptyset$
8		in0	$⊢ bits (A) \cap \emptyset = \emptyset$
9	7 8	eqtrdi	$⊢ x = 0 \to bits (A) \cap (0 ..^x) = \emptyset$
10	9	oveq1d	$⊢ x = 0 \to (bits (A) \cap (0 ..^x)) smul bits (B) = \emptyset smul bits (B)$
11		bitsss	$⊢ bits (B) \subseteq ℕ_{0}$
12		smu02	$⊢ bits (B) \subseteq ℕ_{0} \to \emptyset smul bits (B) = \emptyset$
13	11 12	ax-mp	$⊢ \emptyset smul bits (B) = \emptyset$
14	10 13	eqtrdi	$⊢ x = 0 \to (bits (A) \cap (0 ..^x)) smul bits (B) = \emptyset$
15		oveq2	$⊢ x = 0 \to 2^{x} = 2^{0}$
16		2cn	$⊢ 2 \in ℂ$
17		exp0	$⊢ 2 \in ℂ \to 2^{0} = 1$
18	16 17	ax-mp	$⊢ 2^{0} = 1$
19	15 18	eqtrdi	$⊢ x = 0 \to 2^{x} = 1$
20	19	oveq2d	$⊢ x = 0 \to A \mod 2^{x} = A \mod 1$
21	20	fvoveq1d	$⊢ x = 0 \to bits ((A \mod 2^{x}) B) = bits ((A \mod 1) B)$
22	14 21	eqeq12d	$⊢ x = 0 \to ((bits (A) \cap (0 ..^x)) smul bits (B) = bits ((A \mod 2^{x}) B) \leftrightarrow \emptyset = bits ((A \mod 1) B))$
23	22	imbi2d	$⊢ x = 0 \to ((φ \to (bits (A) \cap (0 ..^x)) smul bits (B) = bits ((A \mod 2^{x}) B)) \leftrightarrow (φ \to \emptyset = bits ((A \mod 1) B)))$
24		oveq2	$⊢ x = k \to (0 ..^x) = (0 ..^k)$
25	24	ineq2d	$⊢ x = k \to bits (A) \cap (0 ..^x) = bits (A) \cap (0 ..^k)$
26	25	oveq1d	$⊢ x = k \to (bits (A) \cap (0 ..^x)) smul bits (B) = (bits (A) \cap (0 ..^k)) smul bits (B)$
27		oveq2	$⊢ x = k \to 2^{x} = 2^{k}$
28	27	oveq2d	$⊢ x = k \to A \mod 2^{x} = A \mod 2^{k}$
29	28	fvoveq1d	$⊢ x = k \to bits ((A \mod 2^{x}) B) = bits ((A \mod 2^{k}) B)$
30	26 29	eqeq12d	$⊢ x = k \to ((bits (A) \cap (0 ..^x)) smul bits (B) = bits ((A \mod 2^{x}) B) \leftrightarrow (bits (A) \cap (0 ..^k)) smul bits (B) = bits ((A \mod 2^{k}) B))$
31	30	imbi2d	$⊢ x = k \to ((φ \to (bits (A) \cap (0 ..^x)) smul bits (B) = bits ((A \mod 2^{x}) B)) \leftrightarrow (φ \to (bits (A) \cap (0 ..^k)) smul bits (B) = bits ((A \mod 2^{k}) B)))$
32		oveq2	$⊢ x = k + 1 \to (0 ..^x) = (0 ..^k + 1)$
33	32	ineq2d	$⊢ x = k + 1 \to bits (A) \cap (0 ..^x) = bits (A) \cap (0 ..^k + 1)$
34	33	oveq1d	$⊢ x = k + 1 \to (bits (A) \cap (0 ..^x)) smul bits (B) = (bits (A) \cap (0 ..^k + 1)) smul bits (B)$
35		oveq2	$⊢ x = k + 1 \to 2^{x} = 2^{k + 1}$
36	35	oveq2d	$⊢ x = k + 1 \to A \mod 2^{x} = A \mod 2^{k + 1}$
37	36	fvoveq1d	$⊢ x = k + 1 \to bits ((A \mod 2^{x}) B) = bits ((A \mod 2^{k + 1}) B)$
38	34 37	eqeq12d	$⊢ x = k + 1 \to ((bits (A) \cap (0 ..^x)) smul bits (B) = bits ((A \mod 2^{x}) B) \leftrightarrow (bits (A) \cap (0 ..^k + 1)) smul bits (B) = bits ((A \mod 2^{k + 1}) B))$
39	38	imbi2d	$⊢ x = k + 1 \to ((φ \to (bits (A) \cap (0 ..^x)) smul bits (B) = bits ((A \mod 2^{x}) B)) \leftrightarrow (φ \to (bits (A) \cap (0 ..^k + 1)) smul bits (B) = bits ((A \mod 2^{k + 1}) B)))$
40		oveq2	$⊢ x = N \to (0 ..^x) = (0 ..^N)$
41	40	ineq2d	$⊢ x = N \to bits (A) \cap (0 ..^x) = bits (A) \cap (0 ..^N)$
42	41	oveq1d	$⊢ x = N \to (bits (A) \cap (0 ..^x)) smul bits (B) = (bits (A) \cap (0 ..^N)) smul bits (B)$
43		oveq2	$⊢ x = N \to 2^{x} = 2^{N}$
44	43	oveq2d	$⊢ x = N \to A \mod 2^{x} = A \mod 2^{N}$
45	44	fvoveq1d	$⊢ x = N \to bits ((A \mod 2^{x}) B) = bits ((A \mod 2^{N}) B)$
46	42 45	eqeq12d	$⊢ x = N \to ((bits (A) \cap (0 ..^x)) smul bits (B) = bits ((A \mod 2^{x}) B) \leftrightarrow (bits (A) \cap (0 ..^N)) smul bits (B) = bits ((A \mod 2^{N}) B))$
47	46	imbi2d	$⊢ x = N \to ((φ \to (bits (A) \cap (0 ..^x)) smul bits (B) = bits ((A \mod 2^{x}) B)) \leftrightarrow (φ \to (bits (A) \cap (0 ..^N)) smul bits (B) = bits ((A \mod 2^{N}) B)))$
48		zmod10	$⊢ A \in ℤ \to A \mod 1 = 0$
49	1 48	syl	$⊢ φ \to A \mod 1 = 0$
50	49	oveq1d	$⊢ φ \to (A \mod 1) B = 0 \cdot B$
51	2	zcnd	$⊢ φ \to B \in ℂ$
52	51	mul02d	$⊢ φ \to 0 \cdot B = 0$
53	50 52	eqtrd	$⊢ φ \to (A \mod 1) B = 0$
54	53	fveq2d	$⊢ φ \to bits ((A \mod 1) B) = bits (0)$
55		0bits	$⊢ bits (0) = \emptyset$
56	54 55	eqtr2di	$⊢ φ \to \emptyset = bits ((A \mod 1) B)$
57		oveq1	$⊢ (bits (A) \cap (0 ..^k)) smul bits (B) = bits ((A \mod 2^{k}) B) \to ((bits (A) \cap (0 ..^k)) smul bits (B)) sadd \{n \in ℕ_{0} \| (k \in bits (A) \land n - k \in bits (B))\} = bits ((A \mod 2^{k}) B) sadd \{n \in ℕ_{0} \| (k \in bits (A) \land n - k \in bits (B))\}$
58		bitsss	$⊢ bits (A) \subseteq ℕ_{0}$
59	58	a1i	$⊢ (φ \land k \in ℕ_{0}) \to bits (A) \subseteq ℕ_{0}$
60	11	a1i	$⊢ (φ \land k \in ℕ_{0}) \to bits (B) \subseteq ℕ_{0}$
61		simpr	$⊢ (φ \land k \in ℕ_{0}) \to k \in ℕ_{0}$
62	59 60 61	smup1	$⊢ (φ \land k \in ℕ_{0}) \to (bits (A) \cap (0 ..^k + 1)) smul bits (B) = ((bits (A) \cap (0 ..^k)) smul bits (B)) sadd \{n \in ℕ_{0} \| (k \in bits (A) \land n - k \in bits (B))\}$
63		bitsinv1lem	$⊢ (A \in ℤ \land k \in ℕ_{0}) \to A \mod 2^{k + 1} = (A \mod 2^{k}) + if (k \in bits (A), 2^{k}, 0)$
64	1 63	sylan	$⊢ (φ \land k \in ℕ_{0}) \to A \mod 2^{k + 1} = (A \mod 2^{k}) + if (k \in bits (A), 2^{k}, 0)$
65	64	oveq1d	$⊢ (φ \land k \in ℕ_{0}) \to (A \mod 2^{k + 1}) B = ((A \mod 2^{k}) + if (k \in bits (A), 2^{k}, 0)) B$
66	1	adantr	$⊢ (φ \land k \in ℕ_{0}) \to A \in ℤ$
67		2nn	$⊢ 2 \in ℕ$
68	67	a1i	$⊢ (φ \land k \in ℕ_{0}) \to 2 \in ℕ$
69	68 61	nnexpcld	$⊢ (φ \land k \in ℕ_{0}) \to 2^{k} \in ℕ$
70	66 69	zmodcld	$⊢ (φ \land k \in ℕ_{0}) \to A \mod 2^{k} \in ℕ_{0}$
71	70	nn0cnd	$⊢ (φ \land k \in ℕ_{0}) \to A \mod 2^{k} \in ℂ$
72	69	nnnn0d	$⊢ (φ \land k \in ℕ_{0}) \to 2^{k} \in ℕ_{0}$
73		0nn0	$⊢ 0 \in ℕ_{0}$
74		ifcl	$⊢ (2^{k} \in ℕ_{0} \land 0 \in ℕ_{0}) \to if (k \in bits (A), 2^{k}, 0) \in ℕ_{0}$
75	72 73 74	sylancl	$⊢ (φ \land k \in ℕ_{0}) \to if (k \in bits (A), 2^{k}, 0) \in ℕ_{0}$
76	75	nn0cnd	$⊢ (φ \land k \in ℕ_{0}) \to if (k \in bits (A), 2^{k}, 0) \in ℂ$
77	51	adantr	$⊢ (φ \land k \in ℕ_{0}) \to B \in ℂ$
78	71 76 77	adddird	$⊢ (φ \land k \in ℕ_{0}) \to ((A \mod 2^{k}) + if (k \in bits (A), 2^{k}, 0)) B = (A \mod 2^{k}) B + if (k \in bits (A), 2^{k}, 0) B$
79	76 77	mulcomd	$⊢ (φ \land k \in ℕ_{0}) \to if (k \in bits (A), 2^{k}, 0) B = B if (k \in bits (A), 2^{k}, 0)$
80	79	oveq2d	$⊢ (φ \land k \in ℕ_{0}) \to (A \mod 2^{k}) B + if (k \in bits (A), 2^{k}, 0) B = (A \mod 2^{k}) B + B if (k \in bits (A), 2^{k}, 0)$
81	65 78 80	3eqtrd	$⊢ (φ \land k \in ℕ_{0}) \to (A \mod 2^{k + 1}) B = (A \mod 2^{k}) B + B if (k \in bits (A), 2^{k}, 0)$
82	81	fveq2d	$⊢ (φ \land k \in ℕ_{0}) \to bits ((A \mod 2^{k + 1}) B) = bits ((A \mod 2^{k}) B + B if (k \in bits (A), 2^{k}, 0))$
83	70	nn0zd	$⊢ (φ \land k \in ℕ_{0}) \to A \mod 2^{k} \in ℤ$
84	2	adantr	$⊢ (φ \land k \in ℕ_{0}) \to B \in ℤ$
85	83 84	zmulcld	$⊢ (φ \land k \in ℕ_{0}) \to (A \mod 2^{k}) B \in ℤ$
86	75	nn0zd	$⊢ (φ \land k \in ℕ_{0}) \to if (k \in bits (A), 2^{k}, 0) \in ℤ$
87	84 86	zmulcld	$⊢ (φ \land k \in ℕ_{0}) \to B if (k \in bits (A), 2^{k}, 0) \in ℤ$
88		sadadd	$⊢ ((A \mod 2^{k}) B \in ℤ \land B if (k \in bits (A), 2^{k}, 0) \in ℤ) \to bits ((A \mod 2^{k}) B) sadd bits (B if (k \in bits (A), 2^{k}, 0)) = bits ((A \mod 2^{k}) B + B if (k \in bits (A), 2^{k}, 0))$
89	85 87 88	syl2anc	$⊢ (φ \land k \in ℕ_{0}) \to bits ((A \mod 2^{k}) B) sadd bits (B if (k \in bits (A), 2^{k}, 0)) = bits ((A \mod 2^{k}) B + B if (k \in bits (A), 2^{k}, 0))$
90		oveq2	$⊢ 2^{k} = if (k \in bits (A), 2^{k}, 0) \to B 2^{k} = B if (k \in bits (A), 2^{k}, 0)$
91	90	fveqeq2d	$⊢ 2^{k} = if (k \in bits (A), 2^{k}, 0) \to (bits (B 2^{k}) = \{n \in ℕ_{0} \| (k \in bits (A) \land n - k \in bits (B))\} \leftrightarrow bits (B if (k \in bits (A), 2^{k}, 0)) = \{n \in ℕ_{0} \| (k \in bits (A) \land n - k \in bits (B))\})$
92		oveq2	$⊢ 0 = if (k \in bits (A), 2^{k}, 0) \to B \cdot 0 = B if (k \in bits (A), 2^{k}, 0)$
93	92	fveqeq2d	$⊢ 0 = if (k \in bits (A), 2^{k}, 0) \to (bits (B \cdot 0) = \{n \in ℕ_{0} \| (k \in bits (A) \land n - k \in bits (B))\} \leftrightarrow bits (B if (k \in bits (A), 2^{k}, 0)) = \{n \in ℕ_{0} \| (k \in bits (A) \land n - k \in bits (B))\})$
94		bitsshft	$⊢ (B \in ℤ \land k \in ℕ_{0}) \to \{n \in ℕ_{0} \| n - k \in bits (B)\} = bits (B 2^{k})$
95	2 94	sylan	$⊢ (φ \land k \in ℕ_{0}) \to \{n \in ℕ_{0} \| n - k \in bits (B)\} = bits (B 2^{k})$
96		ibar	$⊢ k \in bits (A) \to (n - k \in bits (B) \leftrightarrow (k \in bits (A) \land n - k \in bits (B)))$
97	96	rabbidv	$⊢ k \in bits (A) \to \{n \in ℕ_{0} \| n - k \in bits (B)\} = \{n \in ℕ_{0} \| (k \in bits (A) \land n - k \in bits (B))\}$
98	95 97	sylan9req	$⊢ ((φ \land k \in ℕ_{0}) \land k \in bits (A)) \to bits (B 2^{k}) = \{n \in ℕ_{0} \| (k \in bits (A) \land n - k \in bits (B))\}$
99	77	adantr	$⊢ ((φ \land k \in ℕ_{0}) \land \neg k \in bits (A)) \to B \in ℂ$
100	99	mul01d	$⊢ ((φ \land k \in ℕ_{0}) \land \neg k \in bits (A)) \to B \cdot 0 = 0$
101	100	fveq2d	$⊢ ((φ \land k \in ℕ_{0}) \land \neg k \in bits (A)) \to bits (B \cdot 0) = bits (0)$
102		simpr	$⊢ ((φ \land k \in ℕ_{0}) \land \neg k \in bits (A)) \to \neg k \in bits (A)$
103	102	intnanrd	$⊢ ((φ \land k \in ℕ_{0}) \land \neg k \in bits (A)) \to \neg (k \in bits (A) \land n - k \in bits (B))$
104	103	ralrimivw	$⊢ ((φ \land k \in ℕ_{0}) \land \neg k \in bits (A)) \to \forall n \in ℕ_{0} \neg (k \in bits (A) \land n - k \in bits (B))$
105		rabeq0	$⊢ \{n \in ℕ_{0} \| (k \in bits (A) \land n - k \in bits (B))\} = \emptyset \leftrightarrow \forall n \in ℕ_{0} \neg (k \in bits (A) \land n - k \in bits (B))$
106	104 105	sylibr	$⊢ ((φ \land k \in ℕ_{0}) \land \neg k \in bits (A)) \to \{n \in ℕ_{0} \| (k \in bits (A) \land n - k \in bits (B))\} = \emptyset$
107	55 101 106	3eqtr4a	$⊢ ((φ \land k \in ℕ_{0}) \land \neg k \in bits (A)) \to bits (B \cdot 0) = \{n \in ℕ_{0} \| (k \in bits (A) \land n - k \in bits (B))\}$
108	91 93 98 107	ifbothda	$⊢ (φ \land k \in ℕ_{0}) \to bits (B if (k \in bits (A), 2^{k}, 0)) = \{n \in ℕ_{0} \| (k \in bits (A) \land n - k \in bits (B))\}$
109	108	oveq2d	$⊢ (φ \land k \in ℕ_{0}) \to bits ((A \mod 2^{k}) B) sadd bits (B if (k \in bits (A), 2^{k}, 0)) = bits ((A \mod 2^{k}) B) sadd \{n \in ℕ_{0} \| (k \in bits (A) \land n - k \in bits (B))\}$
110	82 89 109	3eqtr2d	$⊢ (φ \land k \in ℕ_{0}) \to bits ((A \mod 2^{k + 1}) B) = bits ((A \mod 2^{k}) B) sadd \{n \in ℕ_{0} \| (k \in bits (A) \land n - k \in bits (B))\}$
111	62 110	eqeq12d	$⊢ (φ \land k \in ℕ_{0}) \to ((bits (A) \cap (0 ..^k + 1)) smul bits (B) = bits ((A \mod 2^{k + 1}) B) \leftrightarrow ((bits (A) \cap (0 ..^k)) smul bits (B)) sadd \{n \in ℕ_{0} \| (k \in bits (A) \land n - k \in bits (B))\} = bits ((A \mod 2^{k}) B) sadd \{n \in ℕ_{0} \| (k \in bits (A) \land n - k \in bits (B))\})$
112	57 111	syl5ibr	$⊢ (φ \land k \in ℕ_{0}) \to ((bits (A) \cap (0 ..^k)) smul bits (B) = bits ((A \mod 2^{k}) B) \to (bits (A) \cap (0 ..^k + 1)) smul bits (B) = bits ((A \mod 2^{k + 1}) B))$
113	112	expcom	$⊢ k \in ℕ_{0} \to (φ \to ((bits (A) \cap (0 ..^k)) smul bits (B) = bits ((A \mod 2^{k}) B) \to (bits (A) \cap (0 ..^k + 1)) smul bits (B) = bits ((A \mod 2^{k + 1}) B)))$
114	113	a2d	$⊢ k \in ℕ_{0} \to ((φ \to (bits (A) \cap (0 ..^k)) smul bits (B) = bits ((A \mod 2^{k}) B)) \to (φ \to (bits (A) \cap (0 ..^k + 1)) smul bits (B) = bits ((A \mod 2^{k + 1}) B)))$
115	23 31 39 47 56 114	nn0ind	$⊢ N \in ℕ_{0} \to (φ \to (bits (A) \cap (0 ..^N)) smul bits (B) = bits ((A \mod 2^{N}) B))$
116	3 115	mpcom	$⊢ φ \to (bits (A) \cap (0 ..^N)) smul bits (B) = bits ((A \mod 2^{N}) B)$

Metamath Proof Explorer

Theorem smumullem

Proof