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 ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( 𝐴 · 𝐵 ) = Σ 𝑘 ∈ ( 0 ..^ ( #b ‘ 𝐴 ) ) ( ( ( 𝑘 ( digit ‘ 2 ) 𝐴 ) · ( 2 ↑ 𝑘 ) ) · 𝐵 ) )

Proof

Step Hyp Ref Expression
1 nn0sumshdig ⊢ ( 𝐴 ∈ ℕ0 → 𝐴 = Σ 𝑘 ∈ ( 0 ..^ ( #b ‘ 𝐴 ) ) ( ( 𝑘 ( digit ‘ 2 ) 𝐴 ) · ( 2 ↑ 𝑘 ) ) )
2 1 adantr ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → 𝐴 = Σ 𝑘 ∈ ( 0 ..^ ( #b ‘ 𝐴 ) ) ( ( 𝑘 ( digit ‘ 2 ) 𝐴 ) · ( 2 ↑ 𝑘 ) ) )
3 2 oveq1d ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( 𝐴 · 𝐵 ) = ( Σ 𝑘 ∈ ( 0 ..^ ( #b ‘ 𝐴 ) ) ( ( 𝑘 ( digit ‘ 2 ) 𝐴 ) · ( 2 ↑ 𝑘 ) ) · 𝐵 ) )
4 fzofi ⊢ ( 0 ..^ ( #b ‘ 𝐴 ) ) ∈ Fin
5 4 a1i ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( 0 ..^ ( #b ‘ 𝐴 ) ) ∈ Fin )
6 nn0cn ⊢ ( 𝐵 ∈ ℕ0 → 𝐵 ∈ ℂ )
7 6 adantl ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → 𝐵 ∈ ℂ )
8 2nn ⊢ 2 ∈ ℕ
9 8 a1i ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ..^ ( #b ‘ 𝐴 ) ) ) → 2 ∈ ℕ )
10 elfzoelz ⊢ ( 𝑘 ∈ ( 0 ..^ ( #b ‘ 𝐴 ) ) → 𝑘 ∈ ℤ )
11 10 adantl ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ..^ ( #b ‘ 𝐴 ) ) ) → 𝑘 ∈ ℤ )
12 nn0rp0 ⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ( 0 [,) +∞ ) )
13 12 adantr ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → 𝐴 ∈ ( 0 [,) +∞ ) )
14 13 adantr ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ..^ ( #b ‘ 𝐴 ) ) ) → 𝐴 ∈ ( 0 [,) +∞ ) )
15 digvalnn0 ⊢ ( ( 2 ∈ ℕ ∧ 𝑘 ∈ ℤ ∧ 𝐴 ∈ ( 0 [,) +∞ ) ) → ( 𝑘 ( digit ‘ 2 ) 𝐴 ) ∈ ℕ0 )
16 9 11 14 15 syl3anc ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ..^ ( #b ‘ 𝐴 ) ) ) → ( 𝑘 ( digit ‘ 2 ) 𝐴 ) ∈ ℕ0 )
17 16 nn0cnd ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ..^ ( #b ‘ 𝐴 ) ) ) → ( 𝑘 ( digit ‘ 2 ) 𝐴 ) ∈ ℂ )
18 2nn0 ⊢ 2 ∈ ℕ0
19 18 a1i ⊢ ( 𝑘 ∈ ( 0 ..^ ( #b ‘ 𝐴 ) ) → 2 ∈ ℕ0 )
20 elfzonn0 ⊢ ( 𝑘 ∈ ( 0 ..^ ( #b ‘ 𝐴 ) ) → 𝑘 ∈ ℕ0 )
21 19 20 nn0expcld ⊢ ( 𝑘 ∈ ( 0 ..^ ( #b ‘ 𝐴 ) ) → ( 2 ↑ 𝑘 ) ∈ ℕ0 )
22 21 nn0cnd ⊢ ( 𝑘 ∈ ( 0 ..^ ( #b ‘ 𝐴 ) ) → ( 2 ↑ 𝑘 ) ∈ ℂ )
23 22 adantl ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ..^ ( #b ‘ 𝐴 ) ) ) → ( 2 ↑ 𝑘 ) ∈ ℂ )
24 17 23 mulcld ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ..^ ( #b ‘ 𝐴 ) ) ) → ( ( 𝑘 ( digit ‘ 2 ) 𝐴 ) · ( 2 ↑ 𝑘 ) ) ∈ ℂ )
25 5 7 24 fsummulc1 ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( Σ 𝑘 ∈ ( 0 ..^ ( #b ‘ 𝐴 ) ) ( ( 𝑘 ( digit ‘ 2 ) 𝐴 ) · ( 2 ↑ 𝑘 ) ) · 𝐵 ) = Σ 𝑘 ∈ ( 0 ..^ ( #b ‘ 𝐴 ) ) ( ( ( 𝑘 ( digit ‘ 2 ) 𝐴 ) · ( 2 ↑ 𝑘 ) ) · 𝐵 ) )
26 3 25 eqtrd ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( 𝐴 · 𝐵 ) = Σ 𝑘 ∈ ( 0 ..^ ( #b ‘ 𝐴 ) ) ( ( ( 𝑘 ( digit ‘ 2 ) 𝐴 ) · ( 2 ↑ 𝑘 ) ) · 𝐵 ) )