Metamath Proof Explorer

Theorem 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∈ℕ0∧B∈ℕ0→A⁢B=∑k∈0..^#b ⁡ A kdigit⁡2A⁢2k⁢B

Proof

Step Hyp Ref Expression
1 nn0sumshdig ⊢A∈ℕ0→A=∑k∈0..^#b ⁡ A kdigit⁡2A⁢2k
2 1 adantr ⊢A∈ℕ0∧B∈ℕ0→A=∑k∈0..^#b ⁡ A kdigit⁡2A⁢2k
3 2 oveq1d ⊢A∈ℕ0∧B∈ℕ0→A⁢B=∑k∈0..^#b ⁡ A kdigit⁡2A⁢2k ⁢ B
4 fzofi ⊢0..^#b ⁡ A ∈ Fin
5 4 a1i ⊢A∈ℕ0∧B∈ℕ0→0..^#b ⁡ A ∈ Fin
6 nn0cn ⊢B∈ℕ0→B∈ℂ
7 6 adantl ⊢A∈ℕ0∧B∈ℕ0→B∈ℂ
8 2nn ⊢2∈ℕ
9 8 a1i ⊢A∈ℕ0∧B∈ℕ0∧k∈0..^#b ⁡ A → 2∈ℕ
10 elfzoelz ⊢k∈0..^#b ⁡ A → k∈ℤ
11 10 adantl ⊢A∈ℕ0∧B∈ℕ0∧k∈0..^#b ⁡ A → k∈ℤ
12 nn0rp0 ⊢A∈ℕ0→A∈0+∞
13 12 adantr ⊢A∈ℕ0∧B∈ℕ0→A∈0+∞
14 13 adantr ⊢A∈ℕ0∧B∈ℕ0∧k∈0..^#b ⁡ A → A∈0+∞
15 digvalnn0 ⊢2∈ℕ∧k∈ℤ∧A∈0+∞→kdigit⁡2A∈ℕ0
16 9 11 14 15 syl3anc ⊢A∈ℕ0∧B∈ℕ0∧k∈0..^#b ⁡ A → kdigit⁡2A∈ℕ0
17 16 nn0cnd ⊢A∈ℕ0∧B∈ℕ0∧k∈0..^#b ⁡ A → kdigit⁡2A∈ℂ
18 2nn0 ⊢2∈ℕ0
19 18 a1i ⊢k∈0..^#b ⁡ A → 2∈ℕ0
20 elfzonn0 ⊢k∈0..^#b ⁡ A → k∈ℕ0
21 19 20 nn0expcld ⊢k∈0..^#b ⁡ A → 2k∈ℕ0
22 21 nn0cnd ⊢k∈0..^#b ⁡ A → 2k∈ℂ
23 22 adantl ⊢A∈ℕ0∧B∈ℕ0∧k∈0..^#b ⁡ A → 2k∈ℂ
24 17 23 mulcld ⊢A∈ℕ0∧B∈ℕ0∧k∈0..^#b ⁡ A → kdigit⁡2A⁢2k∈ℂ
25 5 7 24 fsummulc1 ⊢A∈ℕ0∧B∈ℕ0→∑k∈0..^#b ⁡ A kdigit⁡2A⁢2k ⁢ B = ∑k∈0..^#b ⁡Akdigit⁡2A⁢2k⁢B
26 3 25 eqtrd ⊢A∈ℕ0∧B∈ℕ0→A⁢B=∑k∈0..^#b ⁡ A kdigit⁡2A⁢2k⁢B