Step | Hyp | Ref
| Expression |
1 | | oveq2 6658 |
. . . . . . . . . . 11
..^ ..^ |
2 | | fzo0 12492 |
. . . . . . . . . . 11
..^ |
3 | 1, 2 | syl6eq 2672 |
. . . . . . . . . 10
..^ |
4 | 3 | ineq2d 3814 |
. . . . . . . . 9
bits ..^ bits |
5 | | in0 3968 |
. . . . . . . . 9
bits |
6 | 4, 5 | syl6eq 2672 |
. . . . . . . 8
bits ..^ |
7 | 6 | sumeq1d 14431 |
. . . . . . 7
bits
..^ |
8 | | sum0 14452 |
. . . . . . 7
|
9 | 7, 8 | syl6eq 2672 |
. . . . . 6
bits
..^ |
10 | | oveq2 6658 |
. . . . . . . 8
|
11 | | 2cn 11091 |
. . . . . . . . 9
|
12 | | exp0 12864 |
. . . . . . . . 9
|
13 | 11, 12 | ax-mp 5 |
. . . . . . . 8
|
14 | 10, 13 | syl6eq 2672 |
. . . . . . 7
|
15 | 14 | oveq2d 6666 |
. . . . . 6
|
16 | 9, 15 | eqeq12d 2637 |
. . . . 5
bits ..^
|
17 | 16 | imbi2d 330 |
. . . 4
bits ..^ |
18 | | oveq2 6658 |
. . . . . . . 8
..^ ..^ |
19 | 18 | ineq2d 3814 |
. . . . . . 7
bits ..^ bits ..^ |
20 | 19 | sumeq1d 14431 |
. . . . . 6
bits
..^ bits ..^ |
21 | | oveq2 6658 |
. . . . . . 7
|
22 | 21 | oveq2d 6666 |
. . . . . 6
|
23 | 20, 22 | eqeq12d 2637 |
. . . . 5
bits ..^
bits
..^ |
24 | 23 | imbi2d 330 |
. . . 4
bits ..^ bits ..^ |
25 | | oveq2 6658 |
. . . . . . . 8
..^ ..^ |
26 | 25 | ineq2d 3814 |
. . . . . . 7
bits ..^ bits ..^ |
27 | 26 | sumeq1d 14431 |
. . . . . 6
bits
..^ bits ..^ |
28 | | oveq2 6658 |
. . . . . . 7
|
29 | 28 | oveq2d 6666 |
. . . . . 6
|
30 | 27, 29 | eqeq12d 2637 |
. . . . 5
bits ..^
bits
..^ |
31 | 30 | imbi2d 330 |
. . . 4
bits ..^ bits ..^ |
32 | | oveq2 6658 |
. . . . . . . 8
..^ ..^ |
33 | 32 | ineq2d 3814 |
. . . . . . 7
bits ..^ bits ..^ |
34 | 33 | sumeq1d 14431 |
. . . . . 6
bits
..^ bits ..^ |
35 | | oveq2 6658 |
. . . . . . 7
|
36 | 35 | oveq2d 6666 |
. . . . . 6
|
37 | 34, 36 | eqeq12d 2637 |
. . . . 5
bits ..^
bits
..^ |
38 | 37 | imbi2d 330 |
. . . 4
bits ..^ bits ..^ |
39 | | nn0z 11400 |
. . . . . 6
|
40 | | zmod10 12686 |
. . . . . 6
|
41 | 39, 40 | syl 17 |
. . . . 5
|
42 | 41 | eqcomd 2628 |
. . . 4
|
43 | | oveq1 6657 |
. . . . . . 7
bits ..^ bits ..^ bits bits |
44 | | fzonel 12483 |
. . . . . . . . . . . . 13
..^ |
45 | 44 | a1i 11 |
. . . . . . . . . . . 12
..^ |
46 | | disjsn 4246 |
. . . . . . . . . . . 12
..^
..^ |
47 | 45, 46 | sylibr 224 |
. . . . . . . . . . 11
..^ |
48 | 47 | ineq2d 3814 |
. . . . . . . . . 10
bits
..^ bits |
49 | | inindi 3830 |
. . . . . . . . . 10
bits ..^ bits
..^ bits
|
50 | 48, 49, 5 | 3eqtr3g 2679 |
. . . . . . . . 9
bits ..^ bits |
51 | | simpr 477 |
. . . . . . . . . . . . 13
|
52 | | nn0uz 11722 |
. . . . . . . . . . . . 13
|
53 | 51, 52 | syl6eleq 2711 |
. . . . . . . . . . . 12
|
54 | | fzosplitsn 12576 |
. . . . . . . . . . . 12
..^ ..^ |
55 | 53, 54 | syl 17 |
. . . . . . . . . . 11
..^ ..^ |
56 | 55 | ineq2d 3814 |
. . . . . . . . . 10
bits
..^ bits
..^ |
57 | | indi 3873 |
. . . . . . . . . 10
bits ..^ bits
..^ bits
|
58 | 56, 57 | syl6eq 2672 |
. . . . . . . . 9
bits
..^ bits ..^ bits |
59 | | fzofi 12773 |
. . . . . . . . . . 11
..^ |
60 | | inss2 3834 |
. . . . . . . . . . 11
bits ..^ ..^ |
61 | | ssfi 8180 |
. . . . . . . . . . 11
..^ bits ..^
..^ bits
..^ |
62 | 59, 60, 61 | mp2an 708 |
. . . . . . . . . 10
bits ..^ |
63 | 62 | a1i 11 |
. . . . . . . . 9
bits
..^ |
64 | | 2nn 11185 |
. . . . . . . . . . . 12
|
65 | 64 | a1i 11 |
. . . . . . . . . . 11
bits ..^ |
66 | | simpr 477 |
. . . . . . . . . . . . . 14
bits ..^ bits
..^ |
67 | 66 | elin2d 3803 |
. . . . . . . . . . . . 13
bits ..^ ..^ |
68 | | elfzouz 12474 |
. . . . . . . . . . . . 13
..^
|
69 | 67, 68 | syl 17 |
. . . . . . . . . . . 12
bits ..^ |
70 | 69, 52 | syl6eleqr 2712 |
. . . . . . . . . . 11
bits ..^ |
71 | 65, 70 | nnexpcld 13030 |
. . . . . . . . . 10
bits ..^ |
72 | 71 | nncnd 11036 |
. . . . . . . . 9
bits ..^ |
73 | 50, 58, 63, 72 | fsumsplit 14471 |
. . . . . . . 8
bits ..^ bits ..^ bits
|
74 | | bitsinv1lem 15163 |
. . . . . . . . . 10
bits |
75 | 39, 74 | sylan 488 |
. . . . . . . . 9
bits |
76 | | eqeq2 2633 |
. . . . . . . . . . 11
bits bits
bits
bits |
77 | | eqeq2 2633 |
. . . . . . . . . . 11
bits bits
bits
bits |
78 | | simpr 477 |
. . . . . . . . . . . . . . 15
bits bits |
79 | 78 | snssd 4340 |
. . . . . . . . . . . . . 14
bits bits |
80 | | sseqin2 3817 |
. . . . . . . . . . . . . 14
bits
bits |
81 | 79, 80 | sylib 208 |
. . . . . . . . . . . . 13
bits bits
|
82 | 81 | sumeq1d 14431 |
. . . . . . . . . . . 12
bits bits |
83 | | simplr 792 |
. . . . . . . . . . . . 13
bits |
84 | 64 | a1i 11 |
. . . . . . . . . . . . . . 15
bits |
85 | 84, 83 | nnexpcld 13030 |
. . . . . . . . . . . . . 14
bits |
86 | 85 | nncnd 11036 |
. . . . . . . . . . . . 13
bits |
87 | | oveq2 6658 |
. . . . . . . . . . . . . 14
|
88 | 87 | sumsn 14475 |
. . . . . . . . . . . . 13
|
89 | 83, 86, 88 | syl2anc 693 |
. . . . . . . . . . . 12
bits |
90 | 82, 89 | eqtrd 2656 |
. . . . . . . . . . 11
bits bits |
91 | | simpr 477 |
. . . . . . . . . . . . . 14
bits
bits |
92 | | disjsn 4246 |
. . . . . . . . . . . . . 14
bits
bits |
93 | 91, 92 | sylibr 224 |
. . . . . . . . . . . . 13
bits bits
|
94 | 93 | sumeq1d 14431 |
. . . . . . . . . . . 12
bits bits |
95 | 94, 8 | syl6eq 2672 |
. . . . . . . . . . 11
bits bits |
96 | 76, 77, 90, 95 | ifbothda 4123 |
. . . . . . . . . 10
bits bits |
97 | 96 | oveq2d 6666 |
. . . . . . . . 9
bits bits |
98 | 75, 97 | eqtr4d 2659 |
. . . . . . . 8
bits |
99 | 73, 98 | eqeq12d 2637 |
. . . . . . 7
bits ..^ bits ..^ bits bits |
100 | 43, 99 | syl5ibr 236 |
. . . . . 6
bits ..^ bits ..^ |
101 | 100 | expcom 451 |
. . . . 5
bits ..^ bits ..^ |
102 | 101 | a2d 29 |
. . . 4
bits ..^ bits ..^ |
103 | 17, 24, 31, 38, 42, 102 | nn0ind 11472 |
. . 3
bits
..^ |
104 | 103 | pm2.43i 52 |
. 2
bits
..^ |
105 | | id 22 |
. . . . . . 7
|
106 | 105, 52 | syl6eleq 2711 |
. . . . . 6
|
107 | 64 | a1i 11 |
. . . . . . . 8
|
108 | 107, 105 | nnexpcld 13030 |
. . . . . . 7
|
109 | 108 | nnzd 11481 |
. . . . . 6
|
110 | | 2z 11409 |
. . . . . . . 8
|
111 | | uzid 11702 |
. . . . . . . 8
|
112 | 110, 111 | ax-mp 5 |
. . . . . . 7
|
113 | | bernneq3 12992 |
. . . . . . 7
|
114 | 112, 113 | mpan 706 |
. . . . . 6
|
115 | | elfzo2 12473 |
. . . . . 6
..^ |
116 | 106, 109,
114, 115 | syl3anbrc 1246 |
. . . . 5
..^ |
117 | | bitsfzo 15157 |
. . . . . 6
..^
bits
..^ |
118 | 39, 105, 117 | syl2anc 693 |
. . . . 5
..^ bits ..^ |
119 | 116, 118 | mpbid 222 |
. . . 4
bits ..^ |
120 | | df-ss 3588 |
. . . 4
bits ..^
bits ..^ bits |
121 | 119, 120 | sylib 208 |
. . 3
bits ..^ bits |
122 | 121 | sumeq1d 14431 |
. 2
bits
..^ bits |
123 | | nn0re 11301 |
. . 3
|
124 | | 2rp 11837 |
. . . . 5
|
125 | 124 | a1i 11 |
. . . 4
|
126 | 125, 39 | rpexpcld 13032 |
. . 3
|
127 | | nn0ge0 11318 |
. . 3
|
128 | | modid 12695 |
. . 3
|
129 | 123, 126,
127, 114, 128 | syl22anc 1327 |
. 2
|
130 | 104, 122,
129 | 3eqtr3d 2664 |
1
bits |