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