Step | Hyp | Ref
| Expression |
1 | | bitsss 16367 |
. . . . . 6
β’
(bitsβπ΄)
β β0 |
2 | | bitsss 16367 |
. . . . . 6
β’
(bitsβπ΅)
β β0 |
3 | | smucl 16425 |
. . . . . 6
β’
(((bitsβπ΄)
β β0 β§ (bitsβπ΅) β β0) β
((bitsβπ΄) smul
(bitsβπ΅)) β
β0) |
4 | 1, 2, 3 | mp2an 691 |
. . . . 5
β’
((bitsβπ΄) smul
(bitsβπ΅)) β
β0 |
5 | 4 | sseli 3979 |
. . . 4
β’ (π β ((bitsβπ΄) smul (bitsβπ΅)) β π β β0) |
6 | 5 | a1i 11 |
. . 3
β’ ((π΄ β β€ β§ π΅ β β€) β (π β ((bitsβπ΄) smul (bitsβπ΅)) β π β
β0)) |
7 | | bitsss 16367 |
. . . . 5
β’
(bitsβ(π΄
Β· π΅)) β
β0 |
8 | 7 | sseli 3979 |
. . . 4
β’ (π β (bitsβ(π΄ Β· π΅)) β π β β0) |
9 | 8 | a1i 11 |
. . 3
β’ ((π΄ β β€ β§ π΅ β β€) β (π β (bitsβ(π΄ Β· π΅)) β π β
β0)) |
10 | | simpll 766 |
. . . . . . . . . . . 12
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β π΄ β
β€) |
11 | | simplr 768 |
. . . . . . . . . . . 12
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β π΅ β
β€) |
12 | | simpr 486 |
. . . . . . . . . . . . 13
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β π β
β0) |
13 | | 1nn0 12488 |
. . . . . . . . . . . . . 14
β’ 1 β
β0 |
14 | 13 | a1i 11 |
. . . . . . . . . . . . 13
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β 1 β β0) |
15 | 12, 14 | nn0addcld 12536 |
. . . . . . . . . . . 12
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β (π + 1) β
β0) |
16 | 10, 11, 15 | smumullem 16433 |
. . . . . . . . . . 11
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β (((bitsβπ΄)
β© (0..^(π + 1))) smul
(bitsβπ΅)) =
(bitsβ((π΄ mod
(2β(π + 1))) Β·
π΅))) |
17 | 16 | ineq1d 4212 |
. . . . . . . . . 10
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β ((((bitsβπ΄)
β© (0..^(π + 1))) smul
(bitsβπ΅)) β©
(0..^(π + 1))) =
((bitsβ((π΄ mod
(2β(π + 1))) Β·
π΅)) β© (0..^(π + 1)))) |
18 | | 2nn 12285 |
. . . . . . . . . . . . . . . 16
β’ 2 β
β |
19 | 18 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β 2 β β) |
20 | 19, 15 | nnexpcld 14208 |
. . . . . . . . . . . . . 14
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β (2β(π + 1))
β β) |
21 | 10, 20 | zmodcld 13857 |
. . . . . . . . . . . . 13
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β (π΄ mod
(2β(π + 1))) β
β0) |
22 | 21 | nn0zd 12584 |
. . . . . . . . . . . 12
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β (π΄ mod
(2β(π + 1))) β
β€) |
23 | 22, 11 | zmulcld 12672 |
. . . . . . . . . . 11
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β ((π΄ mod
(2β(π + 1))) Β·
π΅) β
β€) |
24 | | bitsmod 16377 |
. . . . . . . . . . 11
β’ ((((π΄ mod (2β(π + 1))) Β· π΅) β β€ β§ (π + 1) β β0) β
(bitsβ(((π΄ mod
(2β(π + 1))) Β·
π΅) mod (2β(π + 1)))) = ((bitsβ((π΄ mod (2β(π + 1))) Β· π΅)) β© (0..^(π + 1)))) |
25 | 23, 15, 24 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β (bitsβ(((π΄ mod
(2β(π + 1))) Β·
π΅) mod (2β(π + 1)))) = ((bitsβ((π΄ mod (2β(π + 1))) Β· π΅)) β© (0..^(π + 1)))) |
26 | 17, 25 | eqtr4d 2776 |
. . . . . . . . 9
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β ((((bitsβπ΄)
β© (0..^(π + 1))) smul
(bitsβπ΅)) β©
(0..^(π + 1))) =
(bitsβ(((π΄ mod
(2β(π + 1))) Β·
π΅) mod (2β(π + 1))))) |
27 | | inass 4220 |
. . . . . . . . . . . . 13
β’
(((bitsβπ΄)
β© (0..^(π + 1))) β©
(0..^(π + 1))) =
((bitsβπ΄) β©
((0..^(π + 1)) β©
(0..^(π +
1)))) |
28 | | inidm 4219 |
. . . . . . . . . . . . . 14
β’
((0..^(π + 1)) β©
(0..^(π + 1))) =
(0..^(π +
1)) |
29 | 28 | ineq2i 4210 |
. . . . . . . . . . . . 13
β’
((bitsβπ΄)
β© ((0..^(π + 1)) β©
(0..^(π + 1)))) =
((bitsβπ΄) β©
(0..^(π +
1))) |
30 | 27, 29 | eqtri 2761 |
. . . . . . . . . . . 12
β’
(((bitsβπ΄)
β© (0..^(π + 1))) β©
(0..^(π + 1))) =
((bitsβπ΄) β©
(0..^(π +
1))) |
31 | 30 | oveq1i 7419 |
. . . . . . . . . . 11
β’
((((bitsβπ΄)
β© (0..^(π + 1))) β©
(0..^(π + 1))) smul
((bitsβπ΅) β©
(0..^(π + 1)))) =
(((bitsβπ΄) β©
(0..^(π + 1))) smul
((bitsβπ΅) β©
(0..^(π +
1)))) |
32 | 31 | ineq1i 4209 |
. . . . . . . . . 10
β’
(((((bitsβπ΄)
β© (0..^(π + 1))) β©
(0..^(π + 1))) smul
((bitsβπ΅) β©
(0..^(π + 1)))) β©
(0..^(π + 1))) =
((((bitsβπ΄) β©
(0..^(π + 1))) smul
((bitsβπ΅) β©
(0..^(π + 1)))) β©
(0..^(π +
1))) |
33 | | inss1 4229 |
. . . . . . . . . . . 12
β’
((bitsβπ΄)
β© (0..^(π + 1)))
β (bitsβπ΄) |
34 | 1 | a1i 11 |
. . . . . . . . . . . 12
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β (bitsβπ΄)
β β0) |
35 | 33, 34 | sstrid 3994 |
. . . . . . . . . . 11
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β ((bitsβπ΄)
β© (0..^(π + 1)))
β β0) |
36 | 2 | a1i 11 |
. . . . . . . . . . 11
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β (bitsβπ΅)
β β0) |
37 | 35, 36, 15 | smueq 16432 |
. . . . . . . . . 10
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β ((((bitsβπ΄)
β© (0..^(π + 1))) smul
(bitsβπ΅)) β©
(0..^(π + 1))) =
(((((bitsβπ΄) β©
(0..^(π + 1))) β©
(0..^(π + 1))) smul
((bitsβπ΅) β©
(0..^(π + 1)))) β©
(0..^(π +
1)))) |
38 | 34, 36, 15 | smueq 16432 |
. . . . . . . . . 10
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β (((bitsβπ΄)
smul (bitsβπ΅)) β©
(0..^(π + 1))) =
((((bitsβπ΄) β©
(0..^(π + 1))) smul
((bitsβπ΅) β©
(0..^(π + 1)))) β©
(0..^(π +
1)))) |
39 | 32, 37, 38 | 3eqtr4a 2799 |
. . . . . . . . 9
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β ((((bitsβπ΄)
β© (0..^(π + 1))) smul
(bitsβπ΅)) β©
(0..^(π + 1))) =
(((bitsβπ΄) smul
(bitsβπ΅)) β©
(0..^(π +
1)))) |
40 | 20 | nnrpd 13014 |
. . . . . . . . . . 11
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β (2β(π + 1))
β β+) |
41 | 10 | zred 12666 |
. . . . . . . . . . . 12
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β π΄ β
β) |
42 | | modabs2 13870 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§
(2β(π + 1)) β
β+) β ((π΄ mod (2β(π + 1))) mod (2β(π + 1))) = (π΄ mod (2β(π + 1)))) |
43 | 41, 40, 42 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β ((π΄ mod
(2β(π + 1))) mod
(2β(π + 1))) = (π΄ mod (2β(π + 1)))) |
44 | | eqidd 2734 |
. . . . . . . . . . 11
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β (π΅ mod
(2β(π + 1))) = (π΅ mod (2β(π + 1)))) |
45 | 22, 10, 11, 11, 40, 43, 44 | modmul12d 13890 |
. . . . . . . . . 10
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β (((π΄ mod
(2β(π + 1))) Β·
π΅) mod (2β(π + 1))) = ((π΄ Β· π΅) mod (2β(π + 1)))) |
46 | 45 | fveq2d 6896 |
. . . . . . . . 9
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β (bitsβ(((π΄ mod
(2β(π + 1))) Β·
π΅) mod (2β(π + 1)))) = (bitsβ((π΄ Β· π΅) mod (2β(π + 1))))) |
47 | 26, 39, 46 | 3eqtr3d 2781 |
. . . . . . . 8
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β (((bitsβπ΄)
smul (bitsβπ΅)) β©
(0..^(π + 1))) =
(bitsβ((π΄ Β·
π΅) mod (2β(π + 1))))) |
48 | 10, 11 | zmulcld 12672 |
. . . . . . . . 9
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β (π΄ Β· π΅) β
β€) |
49 | | bitsmod 16377 |
. . . . . . . . 9
β’ (((π΄ Β· π΅) β β€ β§ (π + 1) β β0) β
(bitsβ((π΄ Β·
π΅) mod (2β(π + 1)))) = ((bitsβ(π΄ Β· π΅)) β© (0..^(π + 1)))) |
50 | 48, 15, 49 | syl2anc 585 |
. . . . . . . 8
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β (bitsβ((π΄
Β· π΅) mod
(2β(π + 1)))) =
((bitsβ(π΄ Β·
π΅)) β© (0..^(π + 1)))) |
51 | 47, 50 | eqtrd 2773 |
. . . . . . 7
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β (((bitsβπ΄)
smul (bitsβπ΅)) β©
(0..^(π + 1))) =
((bitsβ(π΄ Β·
π΅)) β© (0..^(π + 1)))) |
52 | 51 | eleq2d 2820 |
. . . . . 6
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β (π β
(((bitsβπ΄) smul
(bitsβπ΅)) β©
(0..^(π + 1))) β π β ((bitsβ(π΄ Β· π΅)) β© (0..^(π + 1))))) |
53 | | elin 3965 |
. . . . . 6
β’ (π β (((bitsβπ΄) smul (bitsβπ΅)) β© (0..^(π + 1))) β (π β ((bitsβπ΄) smul (bitsβπ΅)) β§ π β (0..^(π + 1)))) |
54 | | elin 3965 |
. . . . . 6
β’ (π β ((bitsβ(π΄ Β· π΅)) β© (0..^(π + 1))) β (π β (bitsβ(π΄ Β· π΅)) β§ π β (0..^(π + 1)))) |
55 | 52, 53, 54 | 3bitr3g 313 |
. . . . 5
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β ((π β
((bitsβπ΄) smul
(bitsβπ΅)) β§ π β (0..^(π + 1))) β (π β (bitsβ(π΄ Β· π΅)) β§ π β (0..^(π + 1))))) |
56 | | nn0uz 12864 |
. . . . . . . . 9
β’
β0 = (β€β₯β0) |
57 | 12, 56 | eleqtrdi 2844 |
. . . . . . . 8
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β π β
(β€β₯β0)) |
58 | | eluzfz2b 13510 |
. . . . . . . 8
β’ (π β
(β€β₯β0) β π β (0...π)) |
59 | 57, 58 | sylib 217 |
. . . . . . 7
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β π β (0...π)) |
60 | 12 | nn0zd 12584 |
. . . . . . . 8
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β π β
β€) |
61 | | fzval3 13701 |
. . . . . . . 8
β’ (π β β€ β
(0...π) = (0..^(π + 1))) |
62 | 60, 61 | syl 17 |
. . . . . . 7
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β (0...π) =
(0..^(π +
1))) |
63 | 59, 62 | eleqtrd 2836 |
. . . . . 6
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β π β (0..^(π + 1))) |
64 | 63 | biantrud 533 |
. . . . 5
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β (π β
((bitsβπ΄) smul
(bitsβπ΅)) β
(π β
((bitsβπ΄) smul
(bitsβπ΅)) β§ π β (0..^(π + 1))))) |
65 | 63 | biantrud 533 |
. . . . 5
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β (π β
(bitsβ(π΄ Β·
π΅)) β (π β (bitsβ(π΄ Β· π΅)) β§ π β (0..^(π + 1))))) |
66 | 55, 64, 65 | 3bitr4d 311 |
. . . 4
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β (π β
((bitsβπ΄) smul
(bitsβπ΅)) β
π β (bitsβ(π΄ Β· π΅)))) |
67 | 66 | ex 414 |
. . 3
β’ ((π΄ β β€ β§ π΅ β β€) β (π β β0
β (π β
((bitsβπ΄) smul
(bitsβπ΅)) β
π β (bitsβ(π΄ Β· π΅))))) |
68 | 6, 9, 67 | pm5.21ndd 381 |
. 2
β’ ((π΄ β β€ β§ π΅ β β€) β (π β ((bitsβπ΄) smul (bitsβπ΅)) β π β (bitsβ(π΄ Β· π΅)))) |
69 | 68 | eqrdv 2731 |
1
β’ ((π΄ β β€ β§ π΅ β β€) β
((bitsβπ΄) smul
(bitsβπ΅)) =
(bitsβ(π΄ Β·
π΅))) |