Step | Hyp | Ref
| Expression |
1 | | oveq1 5857 |
. . . . . . . . . . . . . 14
|
2 | 1 | eqeq1d 2179 |
. . . . . . . . . . . . 13
|
3 | | phimul.6 |
. . . . . . . . . . . . 13
|
4 | 2, 3 | elrab2 2889 |
. . . . . . . . . . . 12
|
5 | 4 | simplbi 272 |
. . . . . . . . . . 11
|
6 | 5 | adantl 275 |
. . . . . . . . . 10
|
7 | | elfzoelz 10090 |
. . . . . . . . . . . . . . 15
..^
|
8 | | crth.1 |
. . . . . . . . . . . . . . 15
..^ |
9 | 7, 8 | eleq2s 2265 |
. . . . . . . . . . . . . 14
|
10 | 6, 9 | syl 14 |
. . . . . . . . . . . . 13
|
11 | | zq 9572 |
. . . . . . . . . . . . 13
|
12 | 10, 11 | syl 14 |
. . . . . . . . . . . 12
|
13 | | crth.4 |
. . . . . . . . . . . . . . 15
|
14 | 13 | simp1d 1004 |
. . . . . . . . . . . . . 14
|
15 | 14 | adantr 274 |
. . . . . . . . . . . . 13
|
16 | | nnq 9579 |
. . . . . . . . . . . . 13
|
17 | 15, 16 | syl 14 |
. . . . . . . . . . . 12
|
18 | 15 | nngt0d 8909 |
. . . . . . . . . . . 12
|
19 | 12, 17, 18 | modqcld 10271 |
. . . . . . . . . . 11
|
20 | 13 | simp2d 1005 |
. . . . . . . . . . . . . 14
|
21 | 20 | adantr 274 |
. . . . . . . . . . . . 13
|
22 | | nnq 9579 |
. . . . . . . . . . . . 13
|
23 | 21, 22 | syl 14 |
. . . . . . . . . . . 12
|
24 | 21 | nngt0d 8909 |
. . . . . . . . . . . 12
|
25 | 12, 23, 24 | modqcld 10271 |
. . . . . . . . . . 11
|
26 | | opexg 4211 |
. . . . . . . . . . 11
|
27 | 19, 25, 26 | syl2anc 409 |
. . . . . . . . . 10
|
28 | | oveq1 5857 |
. . . . . . . . . . . 12
|
29 | | oveq1 5857 |
. . . . . . . . . . . 12
|
30 | 28, 29 | opeq12d 3771 |
. . . . . . . . . . 11
|
31 | | crth.3 |
. . . . . . . . . . 11
|
32 | 30, 31 | fvmptg 5570 |
. . . . . . . . . 10
|
33 | 6, 27, 32 | syl2anc 409 |
. . . . . . . . 9
|
34 | 5, 8 | eleqtrdi 2263 |
. . . . . . . . . . . . . 14
..^ |
35 | 34 | adantl 275 |
. . . . . . . . . . . . 13
..^ |
36 | 35, 7 | syl 14 |
. . . . . . . . . . . 12
|
37 | | zmodfzo 10290 |
. . . . . . . . . . . 12
..^ |
38 | 36, 15, 37 | syl2anc 409 |
. . . . . . . . . . 11
..^ |
39 | | modgcd 11933 |
. . . . . . . . . . . . 13
|
40 | 36, 15, 39 | syl2anc 409 |
. . . . . . . . . . . 12
|
41 | 15 | nnzd 9320 |
. . . . . . . . . . . . . . . . 17
|
42 | | gcddvds 11905 |
. . . . . . . . . . . . . . . . 17
|
43 | 36, 41, 42 | syl2anc 409 |
. . . . . . . . . . . . . . . 16
|
44 | 43 | simpld 111 |
. . . . . . . . . . . . . . 15
|
45 | | nnne0 8893 |
. . . . . . . . . . . . . . . . . . 19
|
46 | | simpr 109 |
. . . . . . . . . . . . . . . . . . . 20
|
47 | 46 | necon3ai 2389 |
. . . . . . . . . . . . . . . . . . 19
|
48 | 15, 45, 47 | 3syl 17 |
. . . . . . . . . . . . . . . . . 18
|
49 | | gcdn0cl 11904 |
. . . . . . . . . . . . . . . . . 18
|
50 | 36, 41, 48, 49 | syl21anc 1232 |
. . . . . . . . . . . . . . . . 17
|
51 | 50 | nnzd 9320 |
. . . . . . . . . . . . . . . 16
|
52 | 21 | nnzd 9320 |
. . . . . . . . . . . . . . . 16
|
53 | 43 | simprd 113 |
. . . . . . . . . . . . . . . 16
|
54 | 51, 41, 52, 53 | dvdsmultr1d 11781 |
. . . . . . . . . . . . . . 15
|
55 | 15, 21 | nnmulcld 8914 |
. . . . . . . . . . . . . . . . 17
|
56 | 55 | nnzd 9320 |
. . . . . . . . . . . . . . . 16
|
57 | | nnne0 8893 |
. . . . . . . . . . . . . . . . 17
|
58 | | simpr 109 |
. . . . . . . . . . . . . . . . . 18
|
59 | 58 | necon3ai 2389 |
. . . . . . . . . . . . . . . . 17
|
60 | 55, 57, 59 | 3syl 17 |
. . . . . . . . . . . . . . . 16
|
61 | | dvdslegcd 11906 |
. . . . . . . . . . . . . . . 16
|
62 | 51, 36, 56, 60, 61 | syl31anc 1236 |
. . . . . . . . . . . . . . 15
|
63 | 44, 54, 62 | mp2and 431 |
. . . . . . . . . . . . . 14
|
64 | 4 | simprbi 273 |
. . . . . . . . . . . . . . 15
|
65 | 64 | adantl 275 |
. . . . . . . . . . . . . 14
|
66 | 63, 65 | breqtrd 4013 |
. . . . . . . . . . . . 13
|
67 | | nnle1eq1 8889 |
. . . . . . . . . . . . . 14
|
68 | 50, 67 | syl 14 |
. . . . . . . . . . . . 13
|
69 | 66, 68 | mpbid 146 |
. . . . . . . . . . . 12
|
70 | 40, 69 | eqtrd 2203 |
. . . . . . . . . . 11
|
71 | | oveq1 5857 |
. . . . . . . . . . . . 13
|
72 | 71 | eqeq1d 2179 |
. . . . . . . . . . . 12
|
73 | | phimul.4 |
. . . . . . . . . . . 12
..^ |
74 | 72, 73 | elrab2 2889 |
. . . . . . . . . . 11
..^ |
75 | 38, 70, 74 | sylanbrc 415 |
. . . . . . . . . 10
|
76 | | zmodfzo 10290 |
. . . . . . . . . . . 12
..^ |
77 | 36, 21, 76 | syl2anc 409 |
. . . . . . . . . . 11
..^ |
78 | | modgcd 11933 |
. . . . . . . . . . . . 13
|
79 | 36, 21, 78 | syl2anc 409 |
. . . . . . . . . . . 12
|
80 | | gcddvds 11905 |
. . . . . . . . . . . . . . . . 17
|
81 | 36, 52, 80 | syl2anc 409 |
. . . . . . . . . . . . . . . 16
|
82 | 81 | simpld 111 |
. . . . . . . . . . . . . . 15
|
83 | 81 | simprd 113 |
. . . . . . . . . . . . . . . 16
|
84 | | dvdsmul2 11763 |
. . . . . . . . . . . . . . . . 17
|
85 | 41, 52, 84 | syl2anc 409 |
. . . . . . . . . . . . . . . 16
|
86 | | nnne0 8893 |
. . . . . . . . . . . . . . . . . . . 20
|
87 | | simpr 109 |
. . . . . . . . . . . . . . . . . . . . 21
|
88 | 87 | necon3ai 2389 |
. . . . . . . . . . . . . . . . . . . 20
|
89 | 21, 86, 88 | 3syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
90 | | gcdn0cl 11904 |
. . . . . . . . . . . . . . . . . . 19
|
91 | 36, 52, 89, 90 | syl21anc 1232 |
. . . . . . . . . . . . . . . . . 18
|
92 | 91 | nnzd 9320 |
. . . . . . . . . . . . . . . . 17
|
93 | | dvdstr 11777 |
. . . . . . . . . . . . . . . . 17
|
94 | 92, 52, 56, 93 | syl3anc 1233 |
. . . . . . . . . . . . . . . 16
|
95 | 83, 85, 94 | mp2and 431 |
. . . . . . . . . . . . . . 15
|
96 | | dvdslegcd 11906 |
. . . . . . . . . . . . . . . 16
|
97 | 92, 36, 56, 60, 96 | syl31anc 1236 |
. . . . . . . . . . . . . . 15
|
98 | 82, 95, 97 | mp2and 431 |
. . . . . . . . . . . . . 14
|
99 | 98, 65 | breqtrd 4013 |
. . . . . . . . . . . . 13
|
100 | | nnle1eq1 8889 |
. . . . . . . . . . . . . 14
|
101 | 91, 100 | syl 14 |
. . . . . . . . . . . . 13
|
102 | 99, 101 | mpbid 146 |
. . . . . . . . . . . 12
|
103 | 79, 102 | eqtrd 2203 |
. . . . . . . . . . 11
|
104 | | oveq1 5857 |
. . . . . . . . . . . . 13
|
105 | 104 | eqeq1d 2179 |
. . . . . . . . . . . 12
|
106 | | phimul.5 |
. . . . . . . . . . . 12
..^ |
107 | 105, 106 | elrab2 2889 |
. . . . . . . . . . 11
..^ |
108 | 77, 103, 107 | sylanbrc 415 |
. . . . . . . . . 10
|
109 | | opelxpi 4641 |
. . . . . . . . . 10
|
110 | 75, 108, 109 | syl2anc 409 |
. . . . . . . . 9
|
111 | 33, 110 | eqeltrd 2247 |
. . . . . . . 8
|
112 | 111 | ralrimiva 2543 |
. . . . . . 7
|
113 | | crth.2 |
. . . . . . . . . 10
..^ ..^ |
114 | 8, 113, 31, 13 | crth 12165 |
. . . . . . . . 9
|
115 | | f1ofn 5441 |
. . . . . . . . 9
|
116 | | fnfun 5293 |
. . . . . . . . 9
|
117 | 114, 115,
116 | 3syl 17 |
. . . . . . . 8
|
118 | | ssrab2 3232 |
. . . . . . . . . 10
|
119 | 3, 118 | eqsstri 3179 |
. . . . . . . . 9
|
120 | | fndm 5295 |
. . . . . . . . . 10
|
121 | 114, 115,
120 | 3syl 17 |
. . . . . . . . 9
|
122 | 119, 121 | sseqtrrid 3198 |
. . . . . . . 8
|
123 | | funimass4 5545 |
. . . . . . . 8
|
124 | 117, 122,
123 | syl2anc 409 |
. . . . . . 7
|
125 | 112, 124 | mpbird 166 |
. . . . . 6
|
126 | | ssrab2 3232 |
. . . . . . . . . . . . . 14
..^ ..^ |
127 | 73, 126 | eqsstri 3179 |
. . . . . . . . . . . . 13
..^ |
128 | | ssrab2 3232 |
. . . . . . . . . . . . . 14
..^ ..^ |
129 | 106, 128 | eqsstri 3179 |
. . . . . . . . . . . . 13
..^ |
130 | | xpss12 4716 |
. . . . . . . . . . . . 13
..^ ..^
..^ ..^ |
131 | 127, 129,
130 | mp2an 424 |
. . . . . . . . . . . 12
..^ ..^ |
132 | 131, 113 | sseqtrri 3182 |
. . . . . . . . . . 11
|
133 | 132 | sseli 3143 |
. . . . . . . . . 10
|
134 | | f1ocnvfv2 5754 |
. . . . . . . . . 10
|
135 | 114, 133,
134 | syl2an 287 |
. . . . . . . . 9
|
136 | | f1ocnv 5453 |
. . . . . . . . . . . . 13
|
137 | | f1of 5440 |
. . . . . . . . . . . . 13
|
138 | 114, 136,
137 | 3syl 17 |
. . . . . . . . . . . 12
|
139 | | ffvelrn 5626 |
. . . . . . . . . . . 12
|
140 | 138, 133,
139 | syl2an 287 |
. . . . . . . . . . 11
|
141 | 140, 8 | eleqtrdi 2263 |
. . . . . . . . . . . . . . 15
..^ |
142 | | elfzoelz 10090 |
. . . . . . . . . . . . . . 15
..^
|
143 | 141, 142 | syl 14 |
. . . . . . . . . . . . . 14
|
144 | 14 | adantr 274 |
. . . . . . . . . . . . . 14
|
145 | | modgcd 11933 |
. . . . . . . . . . . . . 14
|
146 | 143, 144,
145 | syl2anc 409 |
. . . . . . . . . . . . 13
|
147 | | zq 9572 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
148 | 143, 147 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . 22
|
149 | 144, 16 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . 22
|
150 | 144 | nngt0d 8909 |
. . . . . . . . . . . . . . . . . . . . . 22
|
151 | 148, 149,
150 | modqcld 10271 |
. . . . . . . . . . . . . . . . . . . . 21
|
152 | 20 | adantr 274 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
153 | 152, 22 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . 22
|
154 | 152 | nngt0d 8909 |
. . . . . . . . . . . . . . . . . . . . . 22
|
155 | 148, 153,
154 | modqcld 10271 |
. . . . . . . . . . . . . . . . . . . . 21
|
156 | | opexg 4211 |
. . . . . . . . . . . . . . . . . . . . 21
|
157 | 151, 155,
156 | syl2anc 409 |
. . . . . . . . . . . . . . . . . . . 20
|
158 | | oveq1 5857 |
. . . . . . . . . . . . . . . . . . . . . 22
|
159 | | oveq1 5857 |
. . . . . . . . . . . . . . . . . . . . . 22
|
160 | 158, 159 | opeq12d 3771 |
. . . . . . . . . . . . . . . . . . . . 21
|
161 | 30 | cbvmptv 4083 |
. . . . . . . . . . . . . . . . . . . . . 22
|
162 | 31, 161 | eqtri 2191 |
. . . . . . . . . . . . . . . . . . . . 21
|
163 | 160, 162 | fvmptg 5570 |
. . . . . . . . . . . . . . . . . . . 20
|
164 | 140, 157,
163 | syl2anc 409 |
. . . . . . . . . . . . . . . . . . 19
|
165 | 135, 164 | eqtr3d 2205 |
. . . . . . . . . . . . . . . . . 18
|
166 | | simpr 109 |
. . . . . . . . . . . . . . . . . 18
|
167 | 165, 166 | eqeltrrd 2248 |
. . . . . . . . . . . . . . . . 17
|
168 | | opelxp 4639 |
. . . . . . . . . . . . . . . . 17
|
169 | 167, 168 | sylib 121 |
. . . . . . . . . . . . . . . 16
|
170 | 169 | simpld 111 |
. . . . . . . . . . . . . . 15
|
171 | | oveq1 5857 |
. . . . . . . . . . . . . . . . 17
|
172 | 171 | eqeq1d 2179 |
. . . . . . . . . . . . . . . 16
|
173 | 172, 73 | elrab2 2889 |
. . . . . . . . . . . . . . 15
..^
|
174 | 170, 173 | sylib 121 |
. . . . . . . . . . . . . 14
..^
|
175 | 174 | simprd 113 |
. . . . . . . . . . . . 13
|
176 | 146, 175 | eqtr3d 2205 |
. . . . . . . . . . . 12
|
177 | | modgcd 11933 |
. . . . . . . . . . . . . 14
|
178 | 143, 152,
177 | syl2anc 409 |
. . . . . . . . . . . . 13
|
179 | 169 | simprd 113 |
. . . . . . . . . . . . . . 15
|
180 | | oveq1 5857 |
. . . . . . . . . . . . . . . . 17
|
181 | 180 | eqeq1d 2179 |
. . . . . . . . . . . . . . . 16
|
182 | 181, 106 | elrab2 2889 |
. . . . . . . . . . . . . . 15
..^
|
183 | 179, 182 | sylib 121 |
. . . . . . . . . . . . . 14
..^
|
184 | 183 | simprd 113 |
. . . . . . . . . . . . 13
|
185 | 178, 184 | eqtr3d 2205 |
. . . . . . . . . . . 12
|
186 | 14 | nnzd 9320 |
. . . . . . . . . . . . . 14
|
187 | 186 | adantr 274 |
. . . . . . . . . . . . 13
|
188 | 20 | nnzd 9320 |
. . . . . . . . . . . . . 14
|
189 | 188 | adantr 274 |
. . . . . . . . . . . . 13
|
190 | | rpmul 12039 |
. . . . . . . . . . . . 13
|
191 | 143, 187,
189, 190 | syl3anc 1233 |
. . . . . . . . . . . 12
|
192 | 176, 185,
191 | mp2and 431 |
. . . . . . . . . . 11
|
193 | | oveq1 5857 |
. . . . . . . . . . . . 13
|
194 | 193 | eqeq1d 2179 |
. . . . . . . . . . . 12
|
195 | 194, 3 | elrab2 2889 |
. . . . . . . . . . 11
|
196 | 140, 192,
195 | sylanbrc 415 |
. . . . . . . . . 10
|
197 | | funfvima2 5725 |
. . . . . . . . . . . 12
|
198 | 117, 122,
197 | syl2anc 409 |
. . . . . . . . . . 11
|
199 | 198 | imp 123 |
. . . . . . . . . 10
|
200 | 196, 199 | syldan 280 |
. . . . . . . . 9
|
201 | 135, 200 | eqeltrrd 2248 |
. . . . . . . 8
|
202 | 201 | ex 114 |
. . . . . . 7
|
203 | 202 | ssrdv 3153 |
. . . . . 6
|
204 | 125, 203 | eqssd 3164 |
. . . . 5
|
205 | | f1of1 5439 |
. . . . . . 7
|
206 | 114, 205 | syl 14 |
. . . . . 6
|
207 | 119 | a1i 9 |
. . . . . 6
|
208 | | 0z 9210 |
. . . . . . . . . 10
|
209 | 186, 188 | zmulcld 9327 |
. . . . . . . . . 10
|
210 | | fzofig 10375 |
. . . . . . . . . 10
..^ |
211 | 208, 209,
210 | sylancr 412 |
. . . . . . . . 9
..^ |
212 | 8, 211 | eqeltrid 2257 |
. . . . . . . 8
|
213 | | elfzoelz 10090 |
. . . . . . . . . . . . . 14
..^
|
214 | 213, 8 | eleq2s 2265 |
. . . . . . . . . . . . 13
|
215 | 214 | adantl 275 |
. . . . . . . . . . . 12
|
216 | 209 | adantr 274 |
. . . . . . . . . . . 12
|
217 | 215, 216 | gcdcld 11910 |
. . . . . . . . . . 11
|
218 | 217 | nn0zd 9319 |
. . . . . . . . . 10
|
219 | | 1zzd 9226 |
. . . . . . . . . 10
|
220 | | zdceq 9274 |
. . . . . . . . . 10
DECID |
221 | 218, 219,
220 | syl2anc 409 |
. . . . . . . . 9
DECID
|
222 | 221 | ralrimiva 2543 |
. . . . . . . 8
DECID
|
223 | 212, 222 | ssfirab 6907 |
. . . . . . 7
|
224 | 3, 223 | eqeltrid 2257 |
. . . . . 6
|
225 | | f1imaeng 6766 |
. . . . . 6
|
226 | 206, 207,
224, 225 | syl3anc 1233 |
. . . . 5
|
227 | 204, 226 | eqbrtrrd 4011 |
. . . 4
|
228 | | fzofig 10375 |
. . . . . . . . 9
..^ |
229 | 208, 186,
228 | sylancr 412 |
. . . . . . . 8
..^ |
230 | | elfzoelz 10090 |
. . . . . . . . . . . . 13
..^
|
231 | 230 | adantl 275 |
. . . . . . . . . . . 12
..^ |
232 | 186 | adantr 274 |
. . . . . . . . . . . 12
..^ |
233 | 231, 232 | gcdcld 11910 |
. . . . . . . . . . 11
..^ |
234 | 233 | nn0zd 9319 |
. . . . . . . . . 10
..^ |
235 | | 1z 9225 |
. . . . . . . . . 10
|
236 | | zdceq 9274 |
. . . . . . . . . 10
DECID |
237 | 234, 235,
236 | sylancl 411 |
. . . . . . . . 9
..^ DECID |
238 | 237 | ralrimiva 2543 |
. . . . . . . 8
..^DECID |
239 | 229, 238 | ssfirab 6907 |
. . . . . . 7
..^ |
240 | 73, 239 | eqeltrid 2257 |
. . . . . 6
|
241 | | fzofig 10375 |
. . . . . . . . 9
..^ |
242 | 208, 188,
241 | sylancr 412 |
. . . . . . . 8
..^ |
243 | | elfzoelz 10090 |
. . . . . . . . . . . . 13
..^
|
244 | 243 | adantl 275 |
. . . . . . . . . . . 12
..^ |
245 | 188 | adantr 274 |
. . . . . . . . . . . 12
..^ |
246 | 244, 245 | gcdcld 11910 |
. . . . . . . . . . 11
..^ |
247 | 246 | nn0zd 9319 |
. . . . . . . . . 10
..^ |
248 | | 1zzd 9226 |
. . . . . . . . . 10
..^ |
249 | | zdceq 9274 |
. . . . . . . . . 10
DECID |
250 | 247, 248,
249 | syl2anc 409 |
. . . . . . . . 9
..^ DECID |
251 | 250 | ralrimiva 2543 |
. . . . . . . 8
..^DECID |
252 | 242, 251 | ssfirab 6907 |
. . . . . . 7
..^ |
253 | 106, 252 | eqeltrid 2257 |
. . . . . 6
|
254 | | xpfi 6903 |
. . . . . 6
|
255 | 240, 253,
254 | syl2anc 409 |
. . . . 5
|
256 | | hashen 10705 |
. . . . 5
♯ ♯ |
257 | 255, 224,
256 | syl2anc 409 |
. . . 4
♯ ♯ |
258 | 227, 257 | mpbird 166 |
. . 3
♯ ♯ |
259 | | hashxp 10748 |
. . . 4
♯ ♯ ♯ |
260 | 240, 253,
259 | syl2anc 409 |
. . 3
♯ ♯ ♯ |
261 | 258, 260 | eqtr3d 2205 |
. 2
♯ ♯ ♯ |
262 | 14, 20 | nnmulcld 8914 |
. . 3
|
263 | | dfphi2 12161 |
. . . 4
♯ ..^ |
264 | 8 | rabeqi 2723 |
. . . . . 6
..^
|
265 | 3, 264 | eqtri 2191 |
. . . . 5
..^
|
266 | 265 | fveq2i 5497 |
. . . 4
♯ ♯ ..^ |
267 | 263, 266 | eqtr4di 2221 |
. . 3
♯ |
268 | 262, 267 | syl 14 |
. 2
♯ |
269 | | dfphi2 12161 |
. . . . 5
♯ ..^ |
270 | 73 | fveq2i 5497 |
. . . . 5
♯ ♯ ..^ |
271 | 269, 270 | eqtr4di 2221 |
. . . 4
♯ |
272 | 14, 271 | syl 14 |
. . 3
♯ |
273 | | dfphi2 12161 |
. . . . 5
♯ ..^ |
274 | 106 | fveq2i 5497 |
. . . . 5
♯ ♯ ..^ |
275 | 273, 274 | eqtr4di 2221 |
. . . 4
♯ |
276 | 20, 275 | syl 14 |
. . 3
♯ |
277 | 272, 276 | oveq12d 5868 |
. 2
♯ ♯ |
278 | 261, 268,
277 | 3eqtr4d 2213 |
1
|