Step | Hyp | Ref
| Expression |
1 | | simpl 473 |
. . . . . . . 8
|
2 | | 2nn 11185 |
. . . . . . . . . 10
|
3 | 2 | a1i 11 |
. . . . . . . . 9
|
4 | | simpr 477 |
. . . . . . . . 9
|
5 | 3, 4 | nnexpcld 13030 |
. . . . . . . 8
|
6 | 1, 5 | zmodcld 12691 |
. . . . . . 7
|
7 | 6 | nn0zd 11480 |
. . . . . 6
|
8 | 7 | biantrurd 529 |
. . . . 5
|
9 | 1 | ad2antrr 762 |
. . . . . . . . . . 11
|
10 | | simplr 792 |
. . . . . . . . . . 11
|
11 | | bitsval2 15147 |
. . . . . . . . . . 11
bits
|
12 | 9, 10, 11 | syl2anc 693 |
. . . . . . . . . 10
bits
|
13 | | simpr 477 |
. . . . . . . . . . 11
|
14 | 13 | biantrud 528 |
. . . . . . . . . 10
bits
bits
|
15 | | 2z 11409 |
. . . . . . . . . . . . 13
|
16 | 15 | a1i 11 |
. . . . . . . . . . . 12
|
17 | 9 | zred 11482 |
. . . . . . . . . . . . . 14
|
18 | 2 | a1i 11 |
. . . . . . . . . . . . . . 15
|
19 | 18, 10 | nnexpcld 13030 |
. . . . . . . . . . . . . 14
|
20 | 17, 19 | nndivred 11069 |
. . . . . . . . . . . . 13
|
21 | 20 | flcld 12599 |
. . . . . . . . . . . 12
|
22 | 7 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
|
23 | 22 | zred 11482 |
. . . . . . . . . . . . . 14
|
24 | 23, 19 | nndivred 11069 |
. . . . . . . . . . . . 13
|
25 | 24 | flcld 12599 |
. . . . . . . . . . . 12
|
26 | | 2cnd 11093 |
. . . . . . . . . . . . . . . . . 18
|
27 | 26, 10 | expp1d 13009 |
. . . . . . . . . . . . . . . . 17
|
28 | | 1nn0 11308 |
. . . . . . . . . . . . . . . . . . . 20
|
29 | 28 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
|
30 | 10, 29 | nn0addcld 11355 |
. . . . . . . . . . . . . . . . . 18
|
31 | 30 | nn0zd 11480 |
. . . . . . . . . . . . . . . . . . 19
|
32 | | simplr 792 |
. . . . . . . . . . . . . . . . . . . . 21
|
33 | 32 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
34 | 33 | nn0zd 11480 |
. . . . . . . . . . . . . . . . . . 19
|
35 | | nn0ltp1le 11435 |
. . . . . . . . . . . . . . . . . . . . 21
|
36 | 10, 33, 35 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . 20
|
37 | 13, 36 | mpbid 222 |
. . . . . . . . . . . . . . . . . . 19
|
38 | | eluz2 11693 |
. . . . . . . . . . . . . . . . . . 19
|
39 | 31, 34, 37, 38 | syl3anbrc 1246 |
. . . . . . . . . . . . . . . . . 18
|
40 | | dvdsexp 15049 |
. . . . . . . . . . . . . . . . . 18
|
41 | 16, 30, 39, 40 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
|
42 | 27, 41 | eqbrtrrd 4677 |
. . . . . . . . . . . . . . . 16
|
43 | 5 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . 19
|
44 | 43 | nnrpd 11870 |
. . . . . . . . . . . . . . . . . 18
|
45 | | moddifz 12682 |
. . . . . . . . . . . . . . . . . 18
|
46 | 17, 44, 45 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
|
47 | 43 | nnzd 11481 |
. . . . . . . . . . . . . . . . . 18
|
48 | | 2ne0 11113 |
. . . . . . . . . . . . . . . . . . . 20
|
49 | 48 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
|
50 | 26, 49, 34 | expne0d 13014 |
. . . . . . . . . . . . . . . . . 18
|
51 | 9, 22 | zsubcld 11487 |
. . . . . . . . . . . . . . . . . 18
|
52 | | dvdsval2 14986 |
. . . . . . . . . . . . . . . . . 18
|
53 | 47, 50, 51, 52 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
|
54 | 46, 53 | mpbird 247 |
. . . . . . . . . . . . . . . 16
|
55 | 19 | nnzd 11481 |
. . . . . . . . . . . . . . . . . 18
|
56 | 55, 16 | zmulcld 11488 |
. . . . . . . . . . . . . . . . 17
|
57 | | dvdstr 15018 |
. . . . . . . . . . . . . . . . 17
|
58 | 56, 47, 51, 57 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
|
59 | 42, 54, 58 | mp2and 715 |
. . . . . . . . . . . . . . 15
|
60 | 51 | zcnd 11483 |
. . . . . . . . . . . . . . . 16
|
61 | 19 | nncnd 11036 |
. . . . . . . . . . . . . . . 16
|
62 | 10 | nn0zd 11480 |
. . . . . . . . . . . . . . . . 17
|
63 | 26, 49, 62 | expne0d 13014 |
. . . . . . . . . . . . . . . 16
|
64 | 60, 61, 63 | divcan2d 10803 |
. . . . . . . . . . . . . . 15
|
65 | 59, 64 | breqtrrd 4681 |
. . . . . . . . . . . . . 14
|
66 | 10 | nn0red 11352 |
. . . . . . . . . . . . . . . . . . . 20
|
67 | 33 | nn0red 11352 |
. . . . . . . . . . . . . . . . . . . 20
|
68 | 66, 67, 13 | ltled 10185 |
. . . . . . . . . . . . . . . . . . 19
|
69 | | eluz2 11693 |
. . . . . . . . . . . . . . . . . . 19
|
70 | 62, 34, 68, 69 | syl3anbrc 1246 |
. . . . . . . . . . . . . . . . . 18
|
71 | | dvdsexp 15049 |
. . . . . . . . . . . . . . . . . 18
|
72 | 16, 10, 70, 71 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
|
73 | | dvdstr 15018 |
. . . . . . . . . . . . . . . . . 18
|
74 | 55, 47, 51, 73 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
|
75 | 72, 54, 74 | mp2and 715 |
. . . . . . . . . . . . . . . 16
|
76 | | dvdsval2 14986 |
. . . . . . . . . . . . . . . . 17
|
77 | 55, 63, 51, 76 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
|
78 | 75, 77 | mpbid 222 |
. . . . . . . . . . . . . . 15
|
79 | | dvdscmulr 15010 |
. . . . . . . . . . . . . . 15
|
80 | 16, 78, 55, 63, 79 | syl112anc 1330 |
. . . . . . . . . . . . . 14
|
81 | 65, 80 | mpbid 222 |
. . . . . . . . . . . . 13
|
82 | 22 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . . 20
|
83 | 9 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . . 20
|
84 | 82, 83 | pncan3d 10395 |
. . . . . . . . . . . . . . . . . . 19
|
85 | 84 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . 18
|
86 | 82, 60, 61, 63 | divdird 10839 |
. . . . . . . . . . . . . . . . . 18
|
87 | 85, 86 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . 17
|
88 | 87 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
|
89 | | fladdz 12626 |
. . . . . . . . . . . . . . . . 17
|
90 | 24, 78, 89 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
91 | 88, 90 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
|
92 | 91 | oveq1d 6665 |
. . . . . . . . . . . . . 14
|
93 | 25 | zcnd 11483 |
. . . . . . . . . . . . . . 15
|
94 | 78 | zcnd 11483 |
. . . . . . . . . . . . . . 15
|
95 | 93, 94 | pncan2d 10394 |
. . . . . . . . . . . . . 14
|
96 | 92, 95 | eqtrd 2656 |
. . . . . . . . . . . . 13
|
97 | 81, 96 | breqtrrd 4681 |
. . . . . . . . . . . 12
|
98 | | dvdssub2 15023 |
. . . . . . . . . . . 12
|
99 | 16, 21, 25, 97, 98 | syl31anc 1329 |
. . . . . . . . . . 11
|
100 | 99 | notbid 308 |
. . . . . . . . . 10
|
101 | 12, 14, 100 | 3bitr3d 298 |
. . . . . . . . 9
bits
|
102 | | dvds0 14997 |
. . . . . . . . . . . . 13
|
103 | 15, 102 | ax-mp 5 |
. . . . . . . . . . . 12
|
104 | 1 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
|
105 | 104 | zred 11482 |
. . . . . . . . . . . . . . 15
|
106 | | 2rp 11837 |
. . . . . . . . . . . . . . . . 17
|
107 | 106 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
108 | 32 | nn0zd 11480 |
. . . . . . . . . . . . . . . . 17
|
109 | 108 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
110 | 107, 109 | rpexpcld 13032 |
. . . . . . . . . . . . . . 15
|
111 | 105, 110 | modcld 12674 |
. . . . . . . . . . . . . 14
|
112 | | simplr 792 |
. . . . . . . . . . . . . . . 16
|
113 | 112 | nn0zd 11480 |
. . . . . . . . . . . . . . 15
|
114 | 107, 113 | rpexpcld 13032 |
. . . . . . . . . . . . . 14
|
115 | 6 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
|
116 | 115 | nn0ge0d 11354 |
. . . . . . . . . . . . . 14
|
117 | 111, 114,
116 | divge0d 11912 |
. . . . . . . . . . . . 13
|
118 | 110 | rpred 11872 |
. . . . . . . . . . . . . . . . 17
|
119 | 114 | rpred 11872 |
. . . . . . . . . . . . . . . . 17
|
120 | | modlt 12679 |
. . . . . . . . . . . . . . . . . 18
|
121 | 105, 110,
120 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
|
122 | 107 | rpred 11872 |
. . . . . . . . . . . . . . . . . 18
|
123 | | 1le2 11241 |
. . . . . . . . . . . . . . . . . . 19
|
124 | 123 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
|
125 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . 20
|
126 | 109 | zred 11482 |
. . . . . . . . . . . . . . . . . . . . 21
|
127 | 112 | nn0red 11352 |
. . . . . . . . . . . . . . . . . . . . 21
|
128 | 126, 127 | lenltd 10183 |
. . . . . . . . . . . . . . . . . . . 20
|
129 | 125, 128 | mpbird 247 |
. . . . . . . . . . . . . . . . . . 19
|
130 | | eluz2 11693 |
. . . . . . . . . . . . . . . . . . 19
|
131 | 109, 113,
129, 130 | syl3anbrc 1246 |
. . . . . . . . . . . . . . . . . 18
|
132 | 122, 124,
131 | leexp2ad 13041 |
. . . . . . . . . . . . . . . . 17
|
133 | 111, 118,
119, 121, 132 | ltletrd 10197 |
. . . . . . . . . . . . . . . 16
|
134 | 114 | rpcnd 11874 |
. . . . . . . . . . . . . . . . 17
|
135 | 134 | mulid1d 10057 |
. . . . . . . . . . . . . . . 16
|
136 | 133, 135 | breqtrrd 4681 |
. . . . . . . . . . . . . . 15
|
137 | | 1red 10055 |
. . . . . . . . . . . . . . . 16
|
138 | 111, 137,
114 | ltdivmuld 11923 |
. . . . . . . . . . . . . . 15
|
139 | 136, 138 | mpbird 247 |
. . . . . . . . . . . . . 14
|
140 | | 1e0p1 11552 |
. . . . . . . . . . . . . 14
|
141 | 139, 140 | syl6breq 4694 |
. . . . . . . . . . . . 13
|
142 | 111, 114 | rerpdivcld 11903 |
. . . . . . . . . . . . . 14
|
143 | | 0z 11388 |
. . . . . . . . . . . . . 14
|
144 | | flbi 12617 |
. . . . . . . . . . . . . 14
|
145 | 142, 143,
144 | sylancl 694 |
. . . . . . . . . . . . 13
|
146 | 117, 141,
145 | mpbir2and 957 |
. . . . . . . . . . . 12
|
147 | 103, 146 | syl5breqr 4691 |
. . . . . . . . . . 11
|
148 | 125 | intnand 962 |
. . . . . . . . . . 11
bits |
149 | 147, 148 | 2thd 255 |
. . . . . . . . . 10
bits |
150 | 149 | con2bid 344 |
. . . . . . . . 9
bits
|
151 | 101, 150 | pm2.61dan 832 |
. . . . . . . 8
bits
|
152 | 108 | biantrurd 529 |
. . . . . . . 8
bits
bits
|
153 | 151, 152 | bitr3d 270 |
. . . . . . 7
bits
|
154 | | an12 838 |
. . . . . . 7
bits
bits |
155 | 153, 154 | syl6bb 276 |
. . . . . 6
bits |
156 | 155 | pm5.32da 673 |
. . . . 5
bits
|
157 | 8, 156 | bitr3d 270 |
. . . 4
bits
|
158 | | 3anass 1042 |
. . . 4
|
159 | | elfzo2 12473 |
. . . . . . 7
..^
|
160 | | elnn0uz 11725 |
. . . . . . . 8
|
161 | 160 | 3anbi1i 1253 |
. . . . . . 7
|
162 | | 3anass 1042 |
. . . . . . 7
|
163 | 159, 161,
162 | 3bitr2i 288 |
. . . . . 6
..^
|
164 | 163 | anbi2i 730 |
. . . . 5
bits ..^ bits |
165 | | an12 838 |
. . . . 5
bits
bits
|
166 | 164, 165 | bitri 264 |
. . . 4
bits ..^
bits |
167 | 157, 158,
166 | 3bitr4g 303 |
. . 3
bits
..^ |
168 | | bitsval 15146 |
. . 3
bits
|
169 | | elin 3796 |
. . 3
bits ..^ bits ..^ |
170 | 167, 168,
169 | 3bitr4g 303 |
. 2
bits
bits ..^ |
171 | 170 | eqrdv 2620 |
1
bits bits
..^ |