Step | Hyp | Ref
| Expression |
1 | | smumullem.n |
. 2
|
2 | | oveq2 6658 |
. . . . . . . . . 10
..^ ..^ |
3 | | fzo0 12492 |
. . . . . . . . . 10
..^ |
4 | 2, 3 | syl6eq 2672 |
. . . . . . . . 9
..^ |
5 | 4 | ineq2d 3814 |
. . . . . . . 8
bits ..^ bits |
6 | | in0 3968 |
. . . . . . . 8
bits |
7 | 5, 6 | syl6eq 2672 |
. . . . . . 7
bits ..^ |
8 | 7 | oveq1d 6665 |
. . . . . 6
bits
..^ smul bits
smul bits |
9 | | bitsss 15148 |
. . . . . . 7
bits |
10 | | smu02 15209 |
. . . . . . 7
bits smul bits |
11 | 9, 10 | ax-mp 5 |
. . . . . 6
smul bits |
12 | 8, 11 | syl6eq 2672 |
. . . . 5
bits
..^ smul bits |
13 | | oveq2 6658 |
. . . . . . . . 9
|
14 | | 2cn 11091 |
. . . . . . . . . 10
|
15 | | exp0 12864 |
. . . . . . . . . 10
|
16 | 14, 15 | ax-mp 5 |
. . . . . . . . 9
|
17 | 13, 16 | syl6eq 2672 |
. . . . . . . 8
|
18 | 17 | oveq2d 6666 |
. . . . . . 7
|
19 | 18 | oveq1d 6665 |
. . . . . 6
|
20 | 19 | fveq2d 6195 |
. . . . 5
bits bits |
21 | 12, 20 | eqeq12d 2637 |
. . . 4
bits ..^ smul bits bits
bits |
22 | 21 | imbi2d 330 |
. . 3
bits ..^ smul bits bits
bits |
23 | | oveq2 6658 |
. . . . . . 7
..^ ..^ |
24 | 23 | ineq2d 3814 |
. . . . . 6
bits ..^ bits ..^ |
25 | 24 | oveq1d 6665 |
. . . . 5
bits
..^ smul bits bits ..^ smul bits |
26 | | oveq2 6658 |
. . . . . . . 8
|
27 | 26 | oveq2d 6666 |
. . . . . . 7
|
28 | 27 | oveq1d 6665 |
. . . . . 6
|
29 | 28 | fveq2d 6195 |
. . . . 5
bits bits |
30 | 25, 29 | eqeq12d 2637 |
. . . 4
bits ..^ smul bits bits
bits ..^ smul bits bits |
31 | 30 | imbi2d 330 |
. . 3
bits ..^ smul bits bits
bits ..^ smul bits bits |
32 | | oveq2 6658 |
. . . . . . 7
..^ ..^ |
33 | 32 | ineq2d 3814 |
. . . . . 6
bits ..^ bits ..^ |
34 | 33 | oveq1d 6665 |
. . . . 5
bits
..^ smul bits bits ..^ smul bits |
35 | | oveq2 6658 |
. . . . . . . 8
|
36 | 35 | oveq2d 6666 |
. . . . . . 7
|
37 | 36 | oveq1d 6665 |
. . . . . 6
|
38 | 37 | fveq2d 6195 |
. . . . 5
bits bits |
39 | 34, 38 | eqeq12d 2637 |
. . . 4
bits ..^ smul bits bits
bits ..^ smul bits bits |
40 | 39 | imbi2d 330 |
. . 3
bits ..^ smul bits bits
bits ..^ smul bits bits |
41 | | oveq2 6658 |
. . . . . . 7
..^ ..^ |
42 | 41 | ineq2d 3814 |
. . . . . 6
bits ..^ bits ..^ |
43 | 42 | oveq1d 6665 |
. . . . 5
bits
..^ smul bits bits ..^ smul bits |
44 | | oveq2 6658 |
. . . . . . . 8
|
45 | 44 | oveq2d 6666 |
. . . . . . 7
|
46 | 45 | oveq1d 6665 |
. . . . . 6
|
47 | 46 | fveq2d 6195 |
. . . . 5
bits bits |
48 | 43, 47 | eqeq12d 2637 |
. . . 4
bits ..^ smul bits bits
bits ..^ smul bits bits |
49 | 48 | imbi2d 330 |
. . 3
bits ..^ smul bits bits
bits ..^ smul bits bits |
50 | | smumullem.a |
. . . . . . . 8
|
51 | | zmod10 12686 |
. . . . . . . 8
|
52 | 50, 51 | syl 17 |
. . . . . . 7
|
53 | 52 | oveq1d 6665 |
. . . . . 6
|
54 | | smumullem.b |
. . . . . . . 8
|
55 | 54 | zcnd 11483 |
. . . . . . 7
|
56 | 55 | mul02d 10234 |
. . . . . 6
|
57 | 53, 56 | eqtrd 2656 |
. . . . 5
|
58 | 57 | fveq2d 6195 |
. . . 4
bits bits |
59 | | 0bits 15161 |
. . . 4
bits |
60 | 58, 59 | syl6req 2673 |
. . 3
bits |
61 | | oveq1 6657 |
. . . . . 6
bits
..^ smul bits bits bits ..^ smul bits sadd bits bits bits sadd bits
bits |
62 | | bitsss 15148 |
. . . . . . . . 9
bits |
63 | 62 | a1i 11 |
. . . . . . . 8
bits
|
64 | 9 | a1i 11 |
. . . . . . . 8
bits
|
65 | | simpr 477 |
. . . . . . . 8
|
66 | 63, 64, 65 | smup1 15211 |
. . . . . . 7
bits ..^ smul bits bits ..^ smul bits sadd bits bits |
67 | | bitsinv1lem 15163 |
. . . . . . . . . . . 12
bits |
68 | 50, 67 | sylan 488 |
. . . . . . . . . . 11
bits |
69 | 68 | oveq1d 6665 |
. . . . . . . . . 10
bits |
70 | 50 | adantr 481 |
. . . . . . . . . . . . 13
|
71 | | 2nn 11185 |
. . . . . . . . . . . . . . 15
|
72 | 71 | a1i 11 |
. . . . . . . . . . . . . 14
|
73 | 72, 65 | nnexpcld 13030 |
. . . . . . . . . . . . 13
|
74 | 70, 73 | zmodcld 12691 |
. . . . . . . . . . . 12
|
75 | 74 | nn0cnd 11353 |
. . . . . . . . . . 11
|
76 | 73 | nnnn0d 11351 |
. . . . . . . . . . . . 13
|
77 | | 0nn0 11307 |
. . . . . . . . . . . . 13
|
78 | | ifcl 4130 |
. . . . . . . . . . . . 13
bits |
79 | 76, 77, 78 | sylancl 694 |
. . . . . . . . . . . 12
bits |
80 | 79 | nn0cnd 11353 |
. . . . . . . . . . 11
bits |
81 | 55 | adantr 481 |
. . . . . . . . . . 11
|
82 | 75, 80, 81 | adddird 10065 |
. . . . . . . . . 10
bits bits |
83 | 80, 81 | mulcomd 10061 |
. . . . . . . . . . 11
bits bits |
84 | 83 | oveq2d 6666 |
. . . . . . . . . 10
bits bits |
85 | 69, 82, 84 | 3eqtrd 2660 |
. . . . . . . . 9
bits |
86 | 85 | fveq2d 6195 |
. . . . . . . 8
bits bits bits |
87 | 74 | nn0zd 11480 |
. . . . . . . . . 10
|
88 | 54 | adantr 481 |
. . . . . . . . . 10
|
89 | 87, 88 | zmulcld 11488 |
. . . . . . . . 9
|
90 | 79 | nn0zd 11480 |
. . . . . . . . . 10
bits |
91 | 88, 90 | zmulcld 11488 |
. . . . . . . . 9
bits |
92 | | sadadd 15189 |
. . . . . . . . 9
bits bits sadd bits
bits bits bits |
93 | 89, 91, 92 | syl2anc 693 |
. . . . . . . 8
bits sadd bits
bits bits bits |
94 | | oveq2 6658 |
. . . . . . . . . . . 12
bits
bits |
95 | 94 | fveq2d 6195 |
. . . . . . . . . . 11
bits bits bits bits |
96 | 95 | eqeq1d 2624 |
. . . . . . . . . 10
bits bits bits bits
bits
bits bits
bits |
97 | | oveq2 6658 |
. . . . . . . . . . . 12
bits
bits |
98 | 97 | fveq2d 6195 |
. . . . . . . . . . 11
bits bits bits bits |
99 | 98 | eqeq1d 2624 |
. . . . . . . . . 10
bits bits bits bits
bits
bits bits
bits |
100 | | bitsshft 15197 |
. . . . . . . . . . . 12
bits bits |
101 | 54, 100 | sylan 488 |
. . . . . . . . . . 11
bits
bits
|
102 | | ibar 525 |
. . . . . . . . . . . 12
bits
bits bits bits |
103 | 102 | rabbidv 3189 |
. . . . . . . . . . 11
bits
bits
bits
bits |
104 | 101, 103 | sylan9req 2677 |
. . . . . . . . . 10
bits
bits
bits
bits |
105 | 81 | adantr 481 |
. . . . . . . . . . . . 13
bits |
106 | 105 | mul01d 10235 |
. . . . . . . . . . . 12
bits
|
107 | 106 | fveq2d 6195 |
. . . . . . . . . . 11
bits bits bits |
108 | | simpr 477 |
. . . . . . . . . . . . . 14
bits
bits |
109 | 108 | intnanrd 963 |
. . . . . . . . . . . . 13
bits bits bits |
110 | 109 | ralrimivw 2967 |
. . . . . . . . . . . 12
bits bits
bits |
111 | | rabeq0 3957 |
. . . . . . . . . . . 12
bits bits bits bits |
112 | 110, 111 | sylibr 224 |
. . . . . . . . . . 11
bits bits
bits |
113 | 59, 107, 112 | 3eqtr4a 2682 |
. . . . . . . . . 10
bits bits bits bits |
114 | 96, 99, 104, 113 | ifbothda 4123 |
. . . . . . . . 9
bits
bits bits
bits |
115 | 114 | oveq2d 6666 |
. . . . . . . 8
bits sadd bits
bits bits sadd bits bits |
116 | 86, 93, 115 | 3eqtr2d 2662 |
. . . . . . 7
bits bits sadd bits
bits |
117 | 66, 116 | eqeq12d 2637 |
. . . . . 6
bits
..^ smul bits bits
bits
..^ smul bits sadd bits bits bits sadd bits
bits |
118 | 61, 117 | syl5ibr 236 |
. . . . 5
bits
..^ smul bits bits bits ..^ smul bits bits |
119 | 118 | expcom 451 |
. . . 4
bits ..^ smul bits bits bits
..^ smul bits bits |
120 | 119 | a2d 29 |
. . 3
bits ..^ smul bits bits
bits ..^ smul bits bits |
121 | 22, 31, 40, 49, 60, 120 | nn0ind 11472 |
. 2
bits ..^ smul bits bits |
122 | 1, 121 | mpcom 38 |
1
bits ..^ smul bits bits |