MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bitsmod Unicode version

Theorem bitsmod 14086
Description: Truncating the bit sequence after some is equivalent to reducing the argument 2 M. (Contributed by Mario Carneiro, 6-Sep-2016.)
Assertion
Ref Expression
bitsmod

Proof of Theorem bitsmod
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 simpl 457 . . . . . . . 8
2 2nn 10718 . . . . . . . . . 10
32a1i 11 . . . . . . . . 9
4 simpr 461 . . . . . . . . 9
53, 4nnexpcld 12331 . . . . . . . 8
61, 5zmodcld 12016 . . . . . . 7
76nn0zd 10992 . . . . . 6
87biantrurd 508 . . . . 5
91ad2antrr 725 . . . . . . . . . . 11
10 simplr 755 . . . . . . . . . . 11
11 bitsval2 14075 . . . . . . . . . . 11
129, 10, 11syl2anc 661 . . . . . . . . . 10
13 simpr 461 . . . . . . . . . . 11
1413biantrud 507 . . . . . . . . . 10
15 2z 10921 . . . . . . . . . . . . 13
1615a1i 11 . . . . . . . . . . . 12
179zred 10994 . . . . . . . . . . . . . 14
182a1i 11 . . . . . . . . . . . . . . 15
1918, 10nnexpcld 12331 . . . . . . . . . . . . . 14
2017, 19nndivred 10609 . . . . . . . . . . . . 13
2120flcld 11935 . . . . . . . . . . . 12
227ad2antrr 725 . . . . . . . . . . . . . . 15
2322zred 10994 . . . . . . . . . . . . . 14
2423, 19nndivred 10609 . . . . . . . . . . . . 13
2524flcld 11935 . . . . . . . . . . . 12
26 2cnd 10633 . . . . . . . . . . . . . . . . . 18
2726, 10expp1d 12311 . . . . . . . . . . . . . . . . 17
28 1nn0 10836 . . . . . . . . . . . . . . . . . . . 20
2928a1i 11 . . . . . . . . . . . . . . . . . . 19
3010, 29nn0addcld 10881 . . . . . . . . . . . . . . . . . 18
3130nn0zd 10992 . . . . . . . . . . . . . . . . . . 19
32 simplr 755 . . . . . . . . . . . . . . . . . . . . 21
3332adantr 465 . . . . . . . . . . . . . . . . . . . 20
3433nn0zd 10992 . . . . . . . . . . . . . . . . . . 19
35 nn0ltp1le 10946 . . . . . . . . . . . . . . . . . . . . 21
3610, 33, 35syl2anc 661 . . . . . . . . . . . . . . . . . . . 20
3713, 36mpbid 210 . . . . . . . . . . . . . . . . . . 19
38 eluz2 11116 . . . . . . . . . . . . . . . . . . 19
3931, 34, 37, 38syl3anbrc 1180 . . . . . . . . . . . . . . . . . 18
40 dvdsexp 14042 . . . . . . . . . . . . . . . . . 18
4116, 30, 39, 40syl3anc 1228 . . . . . . . . . . . . . . . . 17
4227, 41eqbrtrrd 4474 . . . . . . . . . . . . . . . 16
435ad2antrr 725 . . . . . . . . . . . . . . . . . . 19
4443nnrpd 11284 . . . . . . . . . . . . . . . . . 18
45 moddifz 12008 . . . . . . . . . . . . . . . . . 18
4617, 44, 45syl2anc 661 . . . . . . . . . . . . . . . . 17
4743nnzd 10993 . . . . . . . . . . . . . . . . . 18
48 2ne0 10653 . . . . . . . . . . . . . . . . . . . 20
4948a1i 11 . . . . . . . . . . . . . . . . . . 19
5026, 49, 34expne0d 12316 . . . . . . . . . . . . . . . . . 18
519, 22zsubcld 10999 . . . . . . . . . . . . . . . . . 18
52 dvdsval2 13989 . . . . . . . . . . . . . . . . . 18
5347, 50, 51, 52syl3anc 1228 . . . . . . . . . . . . . . . . 17
5446, 53mpbird 232 . . . . . . . . . . . . . . . 16
5519nnzd 10993 . . . . . . . . . . . . . . . . . 18
5655, 16zmulcld 11000 . . . . . . . . . . . . . . . . 17
57 dvdstr 14018 . . . . . . . . . . . . . . . . 17
5856, 47, 51, 57syl3anc 1228 . . . . . . . . . . . . . . . 16
5942, 54, 58mp2and 679 . . . . . . . . . . . . . . 15
6051zcnd 10995 . . . . . . . . . . . . . . . 16
6119nncnd 10577 . . . . . . . . . . . . . . . 16
6210nn0zd 10992 . . . . . . . . . . . . . . . . 17
6326, 49, 62expne0d 12316 . . . . . . . . . . . . . . . 16
6460, 61, 63divcan2d 10347 . . . . . . . . . . . . . . 15
6559, 64breqtrrd 4478 . . . . . . . . . . . . . 14
6610nn0red 10878 . . . . . . . . . . . . . . . . . . . 20
6733nn0red 10878 . . . . . . . . . . . . . . . . . . . 20
6866, 67, 13ltled 9754 . . . . . . . . . . . . . . . . . . 19
69 eluz2 11116 . . . . . . . . . . . . . . . . . . 19
7062, 34, 68, 69syl3anbrc 1180 . . . . . . . . . . . . . . . . . 18
71 dvdsexp 14042 . . . . . . . . . . . . . . . . . 18
7216, 10, 70, 71syl3anc 1228 . . . . . . . . . . . . . . . . 17
73 dvdstr 14018 . . . . . . . . . . . . . . . . . 18
7455, 47, 51, 73syl3anc 1228 . . . . . . . . . . . . . . . . 17
7572, 54, 74mp2and 679 . . . . . . . . . . . . . . . 16
76 dvdsval2 13989 . . . . . . . . . . . . . . . . 17
7755, 63, 51, 76syl3anc 1228 . . . . . . . . . . . . . . . 16
7875, 77mpbid 210 . . . . . . . . . . . . . . 15
79 dvdscmulr 14012 . . . . . . . . . . . . . . 15
8016, 78, 55, 63, 79syl112anc 1232 . . . . . . . . . . . . . 14
8165, 80mpbid 210 . . . . . . . . . . . . 13
8222zcnd 10995 . . . . . . . . . . . . . . . . . . . 20
839zcnd 10995 . . . . . . . . . . . . . . . . . . . 20
8482, 83pncan3d 9957 . . . . . . . . . . . . . . . . . . 19
8584oveq1d 6311 . . . . . . . . . . . . . . . . . 18
8682, 60, 61, 63divdird 10383 . . . . . . . . . . . . . . . . . 18
8785, 86eqtr3d 2500 . . . . . . . . . . . . . . . . 17
8887fveq2d 5875 . . . . . . . . . . . . . . . 16
89 fladdz 11958 . . . . . . . . . . . . . . . . 17
9024, 78, 89syl2anc 661 . . . . . . . . . . . . . . . 16
9188, 90eqtrd 2498 . . . . . . . . . . . . . . 15
9291oveq1d 6311 . . . . . . . . . . . . . 14
9325zcnd 10995 . . . . . . . . . . . . . . 15
9478zcnd 10995 . . . . . . . . . . . . . . 15
9593, 94pncan2d 9956 . . . . . . . . . . . . . 14
9692, 95eqtrd 2498 . . . . . . . . . . . . 13
9781, 96breqtrrd 4478 . . . . . . . . . . . 12
98 dvdssub2 14023 . . . . . . . . . . . 12
9916, 21, 25, 97, 98syl31anc 1231 . . . . . . . . . . 11
10099notbid 294 . . . . . . . . . 10
10112, 14, 1003bitr3d 283 . . . . . . . . 9
102 dvds0 13999 . . . . . . . . . . . . 13
10315, 102ax-mp 5 . . . . . . . . . . . 12
1041ad2antrr 725 . . . . . . . . . . . . . . . 16
105104zred 10994 . . . . . . . . . . . . . . 15
106 2rp 11254 . . . . . . . . . . . . . . . . 17
107106a1i 11 . . . . . . . . . . . . . . . 16
10832nn0zd 10992 . . . . . . . . . . . . . . . . 17
109108adantr 465 . . . . . . . . . . . . . . . 16
110107, 109rpexpcld 12333 . . . . . . . . . . . . . . 15
111105, 110modcld 12002 . . . . . . . . . . . . . 14
112 simplr 755 . . . . . . . . . . . . . . . 16
113112nn0zd 10992 . . . . . . . . . . . . . . 15
114107, 113rpexpcld 12333 . . . . . . . . . . . . . 14
1156ad2antrr 725 . . . . . . . . . . . . . . 15
116115nn0ge0d 10880 . . . . . . . . . . . . . 14
117111, 114, 116divge0d 11321 . . . . . . . . . . . . 13
118110rpred 11285 . . . . . . . . . . . . . . . . 17
119114rpred 11285 . . . . . . . . . . . . . . . . 17
120 modlt 12006 . . . . . . . . . . . . . . . . . 18
121105, 110, 120syl2anc 661 . . . . . . . . . . . . . . . . 17
122107rpred 11285 . . . . . . . . . . . . . . . . . 18
123 1le2 10774 . . . . . . . . . . . . . . . . . . 19
124123a1i 11 . . . . . . . . . . . . . . . . . 18
125 simpr 461 . . . . . . . . . . . . . . . . . . . 20
126109zred 10994 . . . . . . . . . . . . . . . . . . . . 21
127112nn0red 10878 . . . . . . . . . . . . . . . . . . . . 21
128126, 127lenltd 9752 . . . . . . . . . . . . . . . . . . . 20
129125, 128mpbird 232 . . . . . . . . . . . . . . . . . . 19
130 eluz2 11116 . . . . . . . . . . . . . . . . . . 19
131109, 113, 129, 130syl3anbrc 1180 . . . . . . . . . . . . . . . . . 18
132122, 124, 131leexp2ad 12342 . . . . . . . . . . . . . . . . 17
133111, 118, 119, 121, 132ltletrd 9763 . . . . . . . . . . . . . . . 16
134114rpcnd 11287 . . . . . . . . . . . . . . . . 17
135134mulid1d 9634 . . . . . . . . . . . . . . . 16
136133, 135breqtrrd 4478 . . . . . . . . . . . . . . 15
137 1red 9632 . . . . . . . . . . . . . . . 16
138111, 137, 114ltdivmuld 11332 . . . . . . . . . . . . . . 15
139136, 138mpbird 232 . . . . . . . . . . . . . 14
140 1e0p1 11032 . . . . . . . . . . . . . 14
141139, 140syl6breq 4491 . . . . . . . . . . . . 13
142111, 114rerpdivcld 11312 . . . . . . . . . . . . . 14
143 0z 10900 . . . . . . . . . . . . . 14
144 flbi 11952 . . . . . . . . . . . . . 14
145142, 143, 144sylancl 662 . . . . . . . . . . . . 13
146117, 141, 145mpbir2and 922 . . . . . . . . . . . 12
147103, 146syl5breqr 4488 . . . . . . . . . . 11
148125intnand 916 . . . . . . . . . . 11
149147, 1482thd 240 . . . . . . . . . 10
150149con2bid 329 . . . . . . . . 9
151101, 150pm2.61dan 791 . . . . . . . 8
152108biantrurd 508 . . . . . . . 8
153151, 152bitr3d 255 . . . . . . 7
154 an12 797 . . . . . . 7
155153, 154syl6bb 261 . . . . . 6
156155pm5.32da 641 . . . . 5
1578, 156bitr3d 255 . . . 4
158 3anass 977 . . . 4
159 elfzo2 11832 . . . . . . 7
160 elnn0uz 11147 . . . . . . . 8
1611603anbi1i 1187 . . . . . . 7
162 3anass 977 . . . . . . 7
163159, 161, 1623bitr2i 273 . . . . . 6
164163anbi2i 694 . . . . 5
165 an12 797 . . . . 5
166164, 165bitri 249 . . . 4
167157, 158, 1663bitr4g 288 . . 3
168 bitsval 14074 . . 3
169 elin 3686 . . 3
170167, 168, 1693bitr4g 288 . 2