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