nn0mullong

Description: Standard algorithm (also known as "long multiplication" or "grade-school multiplication") to calculate the product of two nonnegative integers a and b by multiplying the multiplicand b by each digit of the multiplier a and then add up all the properly shifted results. Here, the binary representation of the multiplier a is used, i.e., the above mentioned "digits" are 0 or 1. This is a similar result as provided by smumul . (Contributed by AV, 7-Jun-2020)

		Ref	Expression
	Assertion	nn0mullong	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to A B = \sum_{k \in (0 ..^#_{b(A)(k digit (2) A) 2^{k} B})}$

Proof

Step	Hyp	Ref	Expression
1		nn0sumshdig	$⊢ A \in ℕ_{0} \to A = \sum_{k \in (0 ..^#_{b(A)(k digit (2) A) 2^{k}})}$
2	1	adantr	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to A = \sum_{k \in (0 ..^#_{b(A)(k digit (2) A) 2^{k}})}$
3	2	oveq1d	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to A B = \sum_{k \in (0 ..^#_{b(A)(k digit (2) A) 2^{k}B})}$
4		fzofi	$⊢ (0 ..^#_{b(A)\inFin})$
5	4	a1i	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to (0 ..^#_{b(A)\inFin})$
6		nn0cn	$⊢ B \in ℕ_{0} \to B \in ℂ$
7	6	adantl	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to B \in ℂ$
8		2nn	$⊢ 2 \in ℕ$
9	8	a1i	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0}) \land k \in (0 ..^#_{b(A)\to2 \in ℕ}))$
10		elfzoelz	$⊢ k \in (0 ..^#_{b(A)\tok \in ℤ})$
11	10	adantl	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0}) \land k \in (0 ..^#_{b(A)\tok \in ℤ}))$
12		nn0rp0	$⊢ A \in ℕ_{0} \to A \in [0, +∞)$
13	12	adantr	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to A \in [0, +∞)$
14	13	adantr	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0}) \land k \in (0 ..^#_{b(A)\toA \in [0, +∞)}))$
15		digvalnn0	$⊢ (2 \in ℕ \land k \in ℤ \land A \in [0, +∞)) \to k digit (2) A \in ℕ_{0}$
16	9 11 14 15	syl3anc	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0}) \land k \in (0 ..^#_{b(A)\tok digit (2) A \in ℕ_{0}}))$
17	16	nn0cnd	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0}) \land k \in (0 ..^#_{b(A)\tok digit (2) A \in ℂ}))$
18		2nn0	$⊢ 2 \in ℕ_{0}$
19	18	a1i	$⊢ k \in (0 ..^#_{b(A)\to2 \in ℕ_{0}})$
20		elfzonn0	$⊢ k \in (0 ..^#_{b(A)\tok \in ℕ_{0}})$
21	19 20	nn0expcld	$⊢ k \in (0 ..^#_{b(A)\to2^{k} \in ℕ_{0}})$
22	21	nn0cnd	$⊢ k \in (0 ..^#_{b(A)\to2^{k} \in ℂ})$
23	22	adantl	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0}) \land k \in (0 ..^#_{b(A)\to2^{k} \in ℂ}))$
24	17 23	mulcld	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0}) \land k \in (0 ..^#_{b(A)\to(k digit (2) A) 2^{k} \in ℂ}))$
25	5 7 24	fsummulc1	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to \sum_{k \in (0 ..^#_{b(A)(k digit (2) A) 2^{k}B=\sum_{k \in (0 ..^#_{b} (A))} (k digit (2) A) 2^{k} B})}$
26	3 25	eqtrd	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to A B = \sum_{k \in (0 ..^#_{b(A)(k digit (2) A) 2^{k} B})}$

Metamath Proof Explorer

Theorem nn0mullong

Proof