smumul

Description: For sequences that correspond to valid integers, the sequence multiplication function produces the sequence for the product. This is effectively a proof of the correctness of the multiplication process, implemented in terms of logic gates for df-sad , whose correctness is verified in sadadd .

Outside this range, the sequences cannot be representing integers, but the smul function still "works". This extended function is best interpreted in terms of the ring structure of the 2-adic integers. (Contributed by Mario Carneiro, 22-Sep-2016)

		Ref	Expression
	Assertion	smumul	$⊢ (A \in ℤ \land B \in ℤ) \to bits (A) smul bits (B) = bits (A B)$

Proof

Step	Hyp	Ref	Expression
1		bitsss	$⊢ bits (A) \subseteq ℕ_{0}$
2		bitsss	$⊢ bits (B) \subseteq ℕ_{0}$
3		smucl	$⊢ (bits (A) \subseteq ℕ_{0} \land bits (B) \subseteq ℕ_{0}) \to bits (A) smul bits (B) \subseteq ℕ_{0}$
4	1 2 3	mp2an	$⊢ bits (A) smul bits (B) \subseteq ℕ_{0}$
5	4	sseli	$⊢ k \in (bits (A) smul bits (B)) \to k \in ℕ_{0}$
6	5	a1i	$⊢ (A \in ℤ \land B \in ℤ) \to (k \in (bits (A) smul 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		simpll	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to A \in ℤ$
11		simplr	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to B \in ℤ$
12		simpr	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to k \in ℕ_{0}$
13		1nn0	$⊢ 1 \in ℕ_{0}$
14	13	a1i	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to 1 \in ℕ_{0}$
15	12 14	nn0addcld	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to k + 1 \in ℕ_{0}$
16	10 11 15	smumullem	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to (bits (A) \cap (0 ..^k + 1)) smul bits (B) = bits ((A \mod 2^{k + 1}) B)$
17	16	ineq1d	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to ((bits (A) \cap (0 ..^k + 1)) smul bits (B)) \cap (0 ..^k + 1) = bits ((A \mod 2^{k + 1}) B) \cap (0 ..^k + 1)$
18		2nn	$⊢ 2 \in ℕ$
19	18	a1i	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to 2 \in ℕ$
20	19 15	nnexpcld	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to 2^{k + 1} \in ℕ$
21	10 20	zmodcld	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to A \mod 2^{k + 1} \in ℕ_{0}$
22	21	nn0zd	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to A \mod 2^{k + 1} \in ℤ$
23	22 11	zmulcld	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to (A \mod 2^{k + 1}) B \in ℤ$
24		bitsmod	$⊢ ((A \mod 2^{k + 1}) B \in ℤ \land k + 1 \in ℕ_{0}) \to bits ((A \mod 2^{k + 1}) B \mod 2^{k + 1}) = bits ((A \mod 2^{k + 1}) B) \cap (0 ..^k + 1)$
25	23 15 24	syl2anc	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to bits ((A \mod 2^{k + 1}) B \mod 2^{k + 1}) = bits ((A \mod 2^{k + 1}) B) \cap (0 ..^k + 1)$
26	17 25	eqtr4d	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to ((bits (A) \cap (0 ..^k + 1)) smul bits (B)) \cap (0 ..^k + 1) = bits ((A \mod 2^{k + 1}) B \mod 2^{k + 1})$
27		inass	$⊢ (bits (A) \cap (0 ..^k + 1)) \cap (0 ..^k + 1) = bits (A) \cap ((0 ..^k + 1) \cap (0 ..^k + 1))$
28		inidm	$⊢ (0 ..^k + 1) \cap (0 ..^k + 1) = (0 ..^k + 1)$
29	28	ineq2i	$⊢ bits (A) \cap ((0 ..^k + 1) \cap (0 ..^k + 1)) = bits (A) \cap (0 ..^k + 1)$
30	27 29	eqtri	$⊢ (bits (A) \cap (0 ..^k + 1)) \cap (0 ..^k + 1) = bits (A) \cap (0 ..^k + 1)$
31	30	oveq1i	$⊢ ((bits (A) \cap (0 ..^k + 1)) \cap (0 ..^k + 1)) smul (bits (B) \cap (0 ..^k + 1)) = (bits (A) \cap (0 ..^k + 1)) smul (bits (B) \cap (0 ..^k + 1))$
32	31	ineq1i	$⊢ (((bits (A) \cap (0 ..^k + 1)) \cap (0 ..^k + 1)) smul (bits (B) \cap (0 ..^k + 1))) \cap (0 ..^k + 1) = ((bits (A) \cap (0 ..^k + 1)) smul (bits (B) \cap (0 ..^k + 1))) \cap (0 ..^k + 1)$
33		inss1	$⊢ bits (A) \cap (0 ..^k + 1) \subseteq bits (A)$
34	1	a1i	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to bits (A) \subseteq ℕ_{0}$
35	33 34	sstrid	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to bits (A) \cap (0 ..^k + 1) \subseteq ℕ_{0}$
36	2	a1i	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to bits (B) \subseteq ℕ_{0}$
37	35 36 15	smueq	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to ((bits (A) \cap (0 ..^k + 1)) smul bits (B)) \cap (0 ..^k + 1) = (((bits (A) \cap (0 ..^k + 1)) \cap (0 ..^k + 1)) smul (bits (B) \cap (0 ..^k + 1))) \cap (0 ..^k + 1)$
38	34 36 15	smueq	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to (bits (A) smul bits (B)) \cap (0 ..^k + 1) = ((bits (A) \cap (0 ..^k + 1)) smul (bits (B) \cap (0 ..^k + 1))) \cap (0 ..^k + 1)$
39	32 37 38	3eqtr4a	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to ((bits (A) \cap (0 ..^k + 1)) smul bits (B)) \cap (0 ..^k + 1) = (bits (A) smul bits (B)) \cap (0 ..^k + 1)$
40	20	nnrpd	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to 2^{k + 1} \in ℝ^{+}$
41	10	zred	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to A \in ℝ$
42		modabs2	$⊢ (A \in ℝ \land 2^{k + 1} \in ℝ^{+}) \to (A \mod 2^{k + 1}) \mod 2^{k + 1} = A \mod 2^{k + 1}$
43	41 40 42	syl2anc	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to (A \mod 2^{k + 1}) \mod 2^{k + 1} = A \mod 2^{k + 1}$
44		eqidd	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to B \mod 2^{k + 1} = B \mod 2^{k + 1}$
45	22 10 11 11 40 43 44	modmul12d	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to (A \mod 2^{k + 1}) B \mod 2^{k + 1} = A B \mod 2^{k + 1}$
46	45	fveq2d	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to bits ((A \mod 2^{k + 1}) B \mod 2^{k + 1}) = bits (A B \mod 2^{k + 1})$
47	26 39 46	3eqtr3d	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to (bits (A) smul bits (B)) \cap (0 ..^k + 1) = bits (A B \mod 2^{k + 1})$
48	10 11	zmulcld	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to A B \in ℤ$
49		bitsmod	$⊢ (A B \in ℤ \land k + 1 \in ℕ_{0}) \to bits (A B \mod 2^{k + 1}) = bits (A B) \cap (0 ..^k + 1)$
50	48 15 49	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)$
51	47 50	eqtrd	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to (bits (A) smul bits (B)) \cap (0 ..^k + 1) = bits (A B) \cap (0 ..^k + 1)$
52	51	eleq2d	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to (k \in ((bits (A) smul bits (B)) \cap (0 ..^k + 1)) \leftrightarrow k \in (bits (A B) \cap (0 ..^k + 1)))$
53		elin	$⊢ k \in ((bits (A) smul bits (B)) \cap (0 ..^k + 1)) \leftrightarrow (k \in (bits (A) smul bits (B)) \land k \in (0 ..^k + 1))$
54		elin	$⊢ k \in (bits (A B) \cap (0 ..^k + 1)) \leftrightarrow (k \in bits (A B) \land k \in (0 ..^k + 1))$
55	52 53 54	3bitr3g	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to ((k \in (bits (A) smul bits (B)) \land k \in (0 ..^k + 1)) \leftrightarrow (k \in bits (A B) \land k \in (0 ..^k + 1)))$
56		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
57	12 56	eleqtrdi	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to k \in ℤ_{\geq 0}$
58		eluzfz2b	$⊢ k \in ℤ_{\geq 0} \leftrightarrow k \in (0 \dots k)$
59	57 58	sylib	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to k \in (0 \dots k)$
60	12	nn0zd	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to k \in ℤ$
61		fzval3	$⊢ k \in ℤ \to (0 \dots k) = (0 ..^k + 1)$
62	60 61	syl	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to (0 \dots k) = (0 ..^k + 1)$
63	59 62	eleqtrd	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to k \in (0 ..^k + 1)$
64	63	biantrud	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to (k \in (bits (A) smul bits (B)) \leftrightarrow (k \in (bits (A) smul bits (B)) \land k \in (0 ..^k + 1)))$
65	63	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)))$
66	55 64 65	3bitr4d	$⊢ ((A \in ℤ \land B \in ℤ) \land k \in ℕ_{0}) \to (k \in (bits (A) smul bits (B)) \leftrightarrow k \in bits (A B))$
67	66	ex	$⊢ (A \in ℤ \land B \in ℤ) \to (k \in ℕ_{0} \to (k \in (bits (A) smul bits (B)) \leftrightarrow k \in bits (A B)))$
68	6 9 67	pm5.21ndd	$⊢ (A \in ℤ \land B \in ℤ) \to (k \in (bits (A) smul bits (B)) \leftrightarrow k \in bits (A B))$
69	68	eqrdv	$⊢ (A \in ℤ \land B \in ℤ) \to bits (A) smul bits (B) = bits (A B)$

Metamath Proof Explorer

Theorem smumul

Proof