Step | Hyp | Ref
| Expression |
1 | | simpr 477 |
. . . . . . . . 9
|
2 | | wilthlem2.s |
. . . . . . . . . . . . . 14
|
3 | | eleq2 2690 |
. . . . . . . . . . . . . . . 16
|
4 | | eleq2 2690 |
. . . . . . . . . . . . . . . . 17
|
5 | 4 | raleqbi1dv 3146 |
. . . . . . . . . . . . . . . 16
|
6 | 3, 5 | anbi12d 747 |
. . . . . . . . . . . . . . 15
|
7 | | wilthlem.a |
. . . . . . . . . . . . . . 15
|
8 | 6, 7 | elrab2 3366 |
. . . . . . . . . . . . . 14
|
9 | 2, 8 | sylib 208 |
. . . . . . . . . . . . 13
|
10 | 9 | simprd 479 |
. . . . . . . . . . . 12
|
11 | 10 | simpld 475 |
. . . . . . . . . . 11
|
12 | 11 | snssd 4340 |
. . . . . . . . . 10
|
13 | 12 | adantr 481 |
. . . . . . . . 9
|
14 | 1, 13 | eqssd 3620 |
. . . . . . . 8
|
15 | 14 | reseq2d 5396 |
. . . . . . 7
|
16 | | mptresid 5456 |
. . . . . . 7
|
17 | 15, 16 | syl6eqr 2674 |
. . . . . 6
|
18 | 17 | oveq2d 6666 |
. . . . 5
g g |
19 | 18 | oveq1d 6665 |
. . . 4
g g |
20 | | wilthlem2.p |
. . . . . . . . . . . 12
|
21 | | prmnn 15388 |
. . . . . . . . . . . 12
|
22 | 20, 21 | syl 17 |
. . . . . . . . . . 11
|
23 | 22 | nncnd 11036 |
. . . . . . . . . 10
|
24 | | ax-1cn 9994 |
. . . . . . . . . 10
|
25 | | negsub 10329 |
. . . . . . . . . 10
|
26 | 23, 24, 25 | sylancl 694 |
. . . . . . . . 9
|
27 | | neg1cn 11124 |
. . . . . . . . . 10
|
28 | | addcom 10222 |
. . . . . . . . . 10
|
29 | 23, 27, 28 | sylancl 694 |
. . . . . . . . 9
|
30 | 26, 29 | eqtr3d 2658 |
. . . . . . . 8
|
31 | | cnring 19768 |
. . . . . . . . . 10
ℂfld |
32 | | wilthlem.t |
. . . . . . . . . . 11
mulGrpℂfld |
33 | 32 | ringmgp 18553 |
. . . . . . . . . 10
ℂfld
|
34 | 31, 33 | mp1i 13 |
. . . . . . . . 9
|
35 | | nnm1nn0 11334 |
. . . . . . . . . . 11
|
36 | 22, 35 | syl 17 |
. . . . . . . . . 10
|
37 | 36 | nn0cnd 11353 |
. . . . . . . . 9
|
38 | | cnfldbas 19750 |
. . . . . . . . . . 11
ℂfld |
39 | 32, 38 | mgpbas 18495 |
. . . . . . . . . 10
|
40 | | id 22 |
. . . . . . . . . 10
|
41 | 39, 40 | gsumsn 18354 |
. . . . . . . . 9
g |
42 | 34, 37, 37, 41 | syl3anc 1326 |
. . . . . . . 8
g |
43 | 23 | mulid2d 10058 |
. . . . . . . . 9
|
44 | 43 | oveq2d 6666 |
. . . . . . . 8
|
45 | 30, 42, 44 | 3eqtr4d 2666 |
. . . . . . 7
g |
46 | 45 | oveq1d 6665 |
. . . . . 6
g |
47 | | neg1rr 11125 |
. . . . . . . 8
|
48 | 47 | a1i 11 |
. . . . . . 7
|
49 | 22 | nnrpd 11870 |
. . . . . . 7
|
50 | | 1zzd 11408 |
. . . . . . 7
|
51 | | modcyc 12705 |
. . . . . . 7
|
52 | 48, 49, 50, 51 | syl3anc 1326 |
. . . . . 6
|
53 | 46, 52 | eqtrd 2656 |
. . . . 5
g |
54 | 53 | adantr 481 |
. . . 4
g |
55 | 19, 54 | eqtrd 2656 |
. . 3
g |
56 | 55 | ex 450 |
. 2
g |
57 | | nss 3663 |
. . 3
|
58 | | cnfld1 19771 |
. . . . . . . . . 10
ℂfld |
59 | 32, 58 | ringidval 18503 |
. . . . . . . . 9
|
60 | | cnfldmul 19752 |
. . . . . . . . . 10
ℂfld |
61 | 32, 60 | mgpplusg 18493 |
. . . . . . . . 9
|
62 | | cncrng 19767 |
. . . . . . . . . . 11
ℂfld |
63 | 32 | crngmgp 18555 |
. . . . . . . . . . 11
ℂfld
CMnd |
64 | 62, 63 | ax-mp 5 |
. . . . . . . . . 10
CMnd |
65 | 64 | a1i 11 |
. . . . . . . . 9
CMnd |
66 | 2 | adantr 481 |
. . . . . . . . 9
|
67 | | f1oi 6174 |
. . . . . . . . . . . 12
|
68 | | f1of 6137 |
. . . . . . . . . . . 12
|
69 | 67, 68 | ax-mp 5 |
. . . . . . . . . . 11
|
70 | 9 | simpld 475 |
. . . . . . . . . . . . . 14
|
71 | 70 | elpwid 4170 |
. . . . . . . . . . . . 13
|
72 | | elfzelz 12342 |
. . . . . . . . . . . . . 14
|
73 | 72 | ssriv 3607 |
. . . . . . . . . . . . 13
|
74 | 71, 73 | syl6ss 3615 |
. . . . . . . . . . . 12
|
75 | | zsscn 11385 |
. . . . . . . . . . . 12
|
76 | 74, 75 | syl6ss 3615 |
. . . . . . . . . . 11
|
77 | | fss 6056 |
. . . . . . . . . . 11
|
78 | 69, 76, 77 | sylancr 695 |
. . . . . . . . . 10
|
79 | 78 | adantr 481 |
. . . . . . . . 9
|
80 | | fzfi 12771 |
. . . . . . . . . . . 12
|
81 | | ssfi 8180 |
. . . . . . . . . . . 12
|
82 | 80, 71, 81 | sylancr 695 |
. . . . . . . . . . 11
|
83 | | 1ex 10035 |
. . . . . . . . . . . 12
|
84 | 83 | a1i 11 |
. . . . . . . . . . 11
|
85 | 78, 82, 84 | fdmfifsupp 8285 |
. . . . . . . . . 10
finSupp |
86 | 85 | adantr 481 |
. . . . . . . . 9
finSupp |
87 | | disjdif 4040 |
. . . . . . . . . 10
|
88 | 87 | a1i 11 |
. . . . . . . . 9
|
89 | | undif2 4044 |
. . . . . . . . . 10
|
90 | | simprl 794 |
. . . . . . . . . . . 12
|
91 | 10 | simprd 479 |
. . . . . . . . . . . . . 14
|
92 | 91 | adantr 481 |
. . . . . . . . . . . . 13
|
93 | | oveq1 6657 |
. . . . . . . . . . . . . . . 16
|
94 | 93 | oveq1d 6665 |
. . . . . . . . . . . . . . 15
|
95 | 94 | eleq1d 2686 |
. . . . . . . . . . . . . 14
|
96 | 95 | rspcv 3305 |
. . . . . . . . . . . . 13
|
97 | 90, 92, 96 | sylc 65 |
. . . . . . . . . . . 12
|
98 | | prssi 4353 |
. . . . . . . . . . . 12
|
99 | 90, 97, 98 | syl2anc 693 |
. . . . . . . . . . 11
|
100 | | ssequn1 3783 |
. . . . . . . . . . 11
|
101 | 99, 100 | sylib 208 |
. . . . . . . . . 10
|
102 | 89, 101 | syl5req 2669 |
. . . . . . . . 9
|
103 | 39, 59, 61, 65, 66, 79, 86, 88, 102 | gsumsplit 18328 |
. . . . . . . 8
g
g
g |
104 | 99 | resabs1d 5428 |
. . . . . . . . . 10
|
105 | 104 | oveq2d 6666 |
. . . . . . . . 9
g
g |
106 | | difss 3737 |
. . . . . . . . . . . 12
|
107 | | resabs1 5427 |
. . . . . . . . . . . 12
|
108 | 106, 107 | ax-mp 5 |
. . . . . . . . . . 11
|
109 | 108 | oveq2i 6661 |
. . . . . . . . . 10
g g |
110 | 109 | a1i 11 |
. . . . . . . . 9
g g |
111 | 105, 110 | oveq12d 6668 |
. . . . . . . 8
g
g g
g
|
112 | 103, 111 | eqtrd 2656 |
. . . . . . 7
g
g g
|
113 | 112 | oveq1d 6665 |
. . . . . 6
g g g
|
114 | | prfi 8235 |
. . . . . . . . . 10
|
115 | 114 | a1i 11 |
. . . . . . . . 9
|
116 | | zsubrg 19799 |
. . . . . . . . . 10
SubRingℂfld |
117 | 32 | subrgsubm 18793 |
. . . . . . . . . 10
SubRingℂfld
SubMnd |
118 | 116, 117 | mp1i 13 |
. . . . . . . . 9
SubMnd |
119 | | f1oi 6174 |
. . . . . . . . . . 11
|
120 | | f1of 6137 |
. . . . . . . . . . 11
|
121 | 119, 120 | ax-mp 5 |
. . . . . . . . . 10
|
122 | 74 | adantr 481 |
. . . . . . . . . . 11
|
123 | 99, 122 | sstrd 3613 |
. . . . . . . . . 10
|
124 | | fss 6056 |
. . . . . . . . . 10
|
125 | 121, 123,
124 | sylancr 695 |
. . . . . . . . 9
|
126 | 83 | a1i 11 |
. . . . . . . . . 10
|
127 | 125, 115,
126 | fdmfifsupp 8285 |
. . . . . . . . 9
finSupp |
128 | 59, 65, 115, 118, 125, 127 | gsumsubmcl 18319 |
. . . . . . . 8
g
|
129 | 128 | zred 11482 |
. . . . . . 7
g
|
130 | | 1red 10055 |
. . . . . . 7
|
131 | 71 | adantr 481 |
. . . . . . . . . 10
|
132 | 131 | ssdifssd 3748 |
. . . . . . . . 9
|
133 | | ssfi 8180 |
. . . . . . . . 9
|
134 | 80, 132, 133 | sylancr 695 |
. . . . . . . 8
|
135 | | f1oi 6174 |
. . . . . . . . . 10
|
136 | | f1of 6137 |
. . . . . . . . . 10
|
137 | 135, 136 | ax-mp 5 |
. . . . . . . . 9
|
138 | 122 | ssdifssd 3748 |
. . . . . . . . 9
|
139 | | fss 6056 |
. . . . . . . . 9
|
140 | 137, 138,
139 | sylancr 695 |
. . . . . . . 8
|
141 | 140, 134,
126 | fdmfifsupp 8285 |
. . . . . . . 8
finSupp |
142 | 59, 65, 134, 118, 140, 141 | gsumsubmcl 18319 |
. . . . . . 7
g
|
143 | 49 | adantr 481 |
. . . . . . 7
|
144 | 34 | adantr 481 |
. . . . . . . . . . . 12
|
145 | 76 | adantr 481 |
. . . . . . . . . . . . 13
|
146 | 145, 90 | sseldd 3604 |
. . . . . . . . . . . 12
|
147 | | id 22 |
. . . . . . . . . . . . 13
|
148 | 39, 147 | gsumsn 18354 |
. . . . . . . . . . . 12
g |
149 | 144, 146,
146, 148 | syl3anc 1326 |
. . . . . . . . . . 11
g |
150 | 149 | adantr 481 |
. . . . . . . . . 10
g |
151 | | mptresid 5456 |
. . . . . . . . . . . 12
|
152 | | dfsn2 4190 |
. . . . . . . . . . . . . 14
|
153 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
|
154 | 153 | orcd 407 |
. . . . . . . . . . . . . . . 16
|
155 | 20 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
156 | 131, 90 | sseldd 3604 |
. . . . . . . . . . . . . . . . . 18
|
157 | | wilthlem1 24794 |
. . . . . . . . . . . . . . . . . 18
|
158 | 155, 156,
157 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
|
159 | 158 | biimpar 502 |
. . . . . . . . . . . . . . . 16
|
160 | 154, 159 | syldan 487 |
. . . . . . . . . . . . . . 15
|
161 | 160 | preq2d 4275 |
. . . . . . . . . . . . . 14
|
162 | 152, 161 | syl5eq 2668 |
. . . . . . . . . . . . 13
|
163 | 162 | reseq2d 5396 |
. . . . . . . . . . . 12
|
164 | 151, 163 | syl5eq 2668 |
. . . . . . . . . . 11
|
165 | 164 | oveq2d 6666 |
. . . . . . . . . 10
g g |
166 | 150, 165,
153 | 3eqtr3d 2664 |
. . . . . . . . 9
g
|
167 | 166 | oveq1d 6665 |
. . . . . . . 8
g
|
168 | | df-pr 4180 |
. . . . . . . . . . . . . . 15
|
169 | 168 | reseq2i 5393 |
. . . . . . . . . . . . . 14
|
170 | | mptresid 5456 |
. . . . . . . . . . . . . 14
|
171 | 169, 170 | eqtr4i 2647 |
. . . . . . . . . . . . 13
|
172 | 171 | oveq2i 6661 |
. . . . . . . . . . . 12
g
g
|
173 | 64 | a1i 11 |
. . . . . . . . . . . . 13
CMnd |
174 | | snfi 8038 |
. . . . . . . . . . . . . 14
|
175 | 174 | a1i 11 |
. . . . . . . . . . . . 13
|
176 | | elsni 4194 |
. . . . . . . . . . . . . . . 16
|
177 | 176 | adantl 482 |
. . . . . . . . . . . . . . 15
|
178 | 146 | adantr 481 |
. . . . . . . . . . . . . . 15
|
179 | 177, 178 | eqeltrd 2701 |
. . . . . . . . . . . . . 14
|
180 | 179 | adantlr 751 |
. . . . . . . . . . . . 13
|
181 | 145, 97 | sseldd 3604 |
. . . . . . . . . . . . . 14
|
182 | 181 | adantr 481 |
. . . . . . . . . . . . 13
|
183 | | simprr 796 |
. . . . . . . . . . . . . . . . . 18
|
184 | | velsn 4193 |
. . . . . . . . . . . . . . . . . 18
|
185 | 183, 184 | sylnib 318 |
. . . . . . . . . . . . . . . . 17
|
186 | | biorf 420 |
. . . . . . . . . . . . . . . . 17
|
187 | 185, 186 | syl 17 |
. . . . . . . . . . . . . . . 16
|
188 | | ovex 6678 |
. . . . . . . . . . . . . . . . . . 19
|
189 | 188 | elsn 4192 |
. . . . . . . . . . . . . . . . . 18
|
190 | | eqcom 2629 |
. . . . . . . . . . . . . . . . . 18
|
191 | 189, 190 | bitri 264 |
. . . . . . . . . . . . . . . . 17
|
192 | | orcom 402 |
. . . . . . . . . . . . . . . . 17
|
193 | 158, 191,
192 | 3bitr4g 303 |
. . . . . . . . . . . . . . . 16
|
194 | 187, 193 | bitr4d 271 |
. . . . . . . . . . . . . . 15
|
195 | 194 | necon3abid 2830 |
. . . . . . . . . . . . . 14
|
196 | 195 | biimpa 501 |
. . . . . . . . . . . . 13
|
197 | | id 22 |
. . . . . . . . . . . . 13
|
198 | 39, 61, 173, 175, 180, 182, 196, 182, 197 | gsumunsn 18359 |
. . . . . . . . . . . 12
g g |
199 | 172, 198 | syl5eq 2668 |
. . . . . . . . . . 11
g g |
200 | 149 | adantr 481 |
. . . . . . . . . . . 12
g |
201 | 200 | oveq1d 6665 |
. . . . . . . . . . 11
g |
202 | 199, 201 | eqtrd 2656 |
. . . . . . . . . 10
g |
203 | 202 | oveq1d 6665 |
. . . . . . . . 9
g
|
204 | 156, 72 | syl 17 |
. . . . . . . . . . . . 13
|
205 | 22 | adantr 481 |
. . . . . . . . . . . . . 14
|
206 | | fzm1ndvds 15044 |
. . . . . . . . . . . . . 14
|
207 | 205, 156,
206 | syl2anc 693 |
. . . . . . . . . . . . 13
|
208 | | eqid 2622 |
. . . . . . . . . . . . . 14
|
209 | 208 | prmdiv 15490 |
. . . . . . . . . . . . 13
|
210 | 155, 204,
207, 209 | syl3anc 1326 |
. . . . . . . . . . . 12
|
211 | 210 | simprd 479 |
. . . . . . . . . . 11
|
212 | | elfznn 12370 |
. . . . . . . . . . . . . . 15
|
213 | 156, 212 | syl 17 |
. . . . . . . . . . . . . 14
|
214 | 131, 97 | sseldd 3604 |
. . . . . . . . . . . . . . 15
|
215 | | elfznn 12370 |
. . . . . . . . . . . . . . 15
|
216 | 214, 215 | syl 17 |
. . . . . . . . . . . . . 14
|
217 | 213, 216 | nnmulcld 11068 |
. . . . . . . . . . . . 13
|
218 | 217 | nnzd 11481 |
. . . . . . . . . . . 12
|
219 | | 1zzd 11408 |
. . . . . . . . . . . 12
|
220 | | moddvds 14991 |
. . . . . . . . . . . 12
|
221 | 205, 218,
219, 220 | syl3anc 1326 |
. . . . . . . . . . 11
|
222 | 211, 221 | mpbird 247 |
. . . . . . . . . 10
|
223 | 222 | adantr 481 |
. . . . . . . . 9
|
224 | 203, 223 | eqtrd 2656 |
. . . . . . . 8
g
|
225 | 167, 224 | pm2.61dane 2881 |
. . . . . . 7
g |
226 | | modmul1 12723 |
. . . . . . 7
g
g
g
g g
g
|
227 | 129, 130,
142, 143, 225, 226 | syl221anc 1337 |
. . . . . 6
g g
g
|
228 | 142 | zcnd 11483 |
. . . . . . . . 9
g
|
229 | 228 | mulid2d 10058 |
. . . . . . . 8
g g |
230 | 229 | oveq1d 6665 |
. . . . . . 7
g
g |
231 | | ovex 6678 |
. . . . . . . . . . 11
|
232 | 231 | elpw2 4828 |
. . . . . . . . . 10
|
233 | 132, 232 | sylibr 224 |
. . . . . . . . 9
|
234 | 11 | adantr 481 |
. . . . . . . . . . 11
|
235 | | eqcom 2629 |
. . . . . . . . . . . . . . 15
|
236 | 184, 235 | bitri 264 |
. . . . . . . . . . . . . 14
|
237 | 183, 236 | sylnib 318 |
. . . . . . . . . . . . 13
|
238 | | oveq1 6657 |
. . . . . . . . . . . . . . . 16
|
239 | 238 | oveq1d 6665 |
. . . . . . . . . . . . . . 15
|
240 | 205, 35 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
241 | | nn0uz 11722 |
. . . . . . . . . . . . . . . . . . 19
|
242 | 240, 241 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . . 18
|
243 | | eluzfz2 12349 |
. . . . . . . . . . . . . . . . . 18
|
244 | 242, 243 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
245 | | prmz 15389 |
. . . . . . . . . . . . . . . . . . . 20
|
246 | 155, 245 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
247 | 122, 234 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . . 20
|
248 | | 1z 11407 |
. . . . . . . . . . . . . . . . . . . 20
|
249 | | zsubcl 11419 |
. . . . . . . . . . . . . . . . . . . 20
|
250 | 247, 248,
249 | sylancl 694 |
. . . . . . . . . . . . . . . . . . 19
|
251 | | dvdsmul1 15003 |
. . . . . . . . . . . . . . . . . . 19
|
252 | 246, 250,
251 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
|
253 | 205 | nncnd 11036 |
. . . . . . . . . . . . . . . . . . . . . 22
|
254 | 24 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
|
255 | 240 | nn0cnd 11353 |
. . . . . . . . . . . . . . . . . . . . . 22
|
256 | 253, 254,
255 | subdird 10487 |
. . . . . . . . . . . . . . . . . . . . 21
|
257 | 253, 255 | mulcld 10060 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
258 | 257, 253,
254 | subsubd 10420 |
. . . . . . . . . . . . . . . . . . . . . 22
|
259 | 255 | mulid2d 10058 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
260 | 259 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . 22
|
261 | 253, 255,
254 | subdid 10486 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
262 | 253 | mulid1d 10057 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
263 | 262 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
264 | 261, 263 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
265 | 264 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . 22
|
266 | 258, 260,
265 | 3eqtr4d 2666 |
. . . . . . . . . . . . . . . . . . . . 21
|
267 | 256, 266 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . 20
|
268 | 267 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . 19
|
269 | 250 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . . . 21
|
270 | 253, 269 | mulcld 10060 |
. . . . . . . . . . . . . . . . . . . 20
|
271 | | pncan 10287 |
. . . . . . . . . . . . . . . . . . . 20
|
272 | 270, 24, 271 | sylancl 694 |
. . . . . . . . . . . . . . . . . . 19
|
273 | 268, 272 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . 18
|
274 | 252, 273 | breqtrrd 4681 |
. . . . . . . . . . . . . . . . 17
|
275 | 131, 234 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . 19
|
276 | | fzm1ndvds 15044 |
. . . . . . . . . . . . . . . . . . 19
|
277 | 205, 275,
276 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
|
278 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
|
279 | 278 | prmdiveq 15491 |
. . . . . . . . . . . . . . . . . 18
|
280 | 155, 247,
277, 279 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
|
281 | 244, 274,
280 | mpbi2and 956 |
. . . . . . . . . . . . . . . 16
|
282 | 208 | prmdivdiv 15492 |
. . . . . . . . . . . . . . . . 17
|
283 | 155, 156,
282 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
284 | 281, 283 | eqeq12d 2637 |
. . . . . . . . . . . . . . 15
|
285 | 239, 284 | syl5ibr 236 |
. . . . . . . . . . . . . 14
|
286 | 237, 285 | mtod 189 |
. . . . . . . . . . . . 13
|
287 | | ioran 511 |
. . . . . . . . . . . . 13
|
288 | 237, 286,
287 | sylanbrc 698 |
. . . . . . . . . . . 12
|
289 | | ovex 6678 |
. . . . . . . . . . . . 13
|
290 | 289 | elpr 4198 |
. . . . . . . . . . . 12
|
291 | 288, 290 | sylnibr 319 |
. . . . . . . . . . 11
|
292 | 234, 291 | eldifd 3585 |
. . . . . . . . . 10
|
293 | | eldifi 3732 |
. . . . . . . . . . . . 13
|
294 | 92 | r19.21bi 2932 |
. . . . . . . . . . . . 13
|
295 | 293, 294 | sylan2 491 |
. . . . . . . . . . . 12
|
296 | | eldif 3584 |
. . . . . . . . . . . . 13
|
297 | 155 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
298 | 131 | sselda 3603 |
. . . . . . . . . . . . . . . . . . 19
|
299 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . 20
|
300 | 299 | prmdivdiv 15492 |
. . . . . . . . . . . . . . . . . . 19
|
301 | 297, 298,
300 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
|
302 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . 20
|
303 | 302 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . 19
|
304 | 303 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . 18
|
305 | 301, 304 | syl5ibcom 235 |
. . . . . . . . . . . . . . . . 17
|
306 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . 19
|
307 | 306 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . 18
|
308 | 283 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
309 | 301, 308 | eqeq12d 2637 |
. . . . . . . . . . . . . . . . . 18
|
310 | 307, 309 | syl5ibr 236 |
. . . . . . . . . . . . . . . . 17
|
311 | 305, 310 | orim12d 883 |
. . . . . . . . . . . . . . . 16
|
312 | | ovex 6678 |
. . . . . . . . . . . . . . . . 17
|
313 | 312 | elpr 4198 |
. . . . . . . . . . . . . . . 16
|
314 | | vex 3203 |
. . . . . . . . . . . . . . . . . 18
|
315 | 314 | elpr 4198 |
. . . . . . . . . . . . . . . . 17
|
316 | | orcom 402 |
. . . . . . . . . . . . . . . . 17
|
317 | 315, 316 | bitri 264 |
. . . . . . . . . . . . . . . 16
|
318 | 311, 313,
317 | 3imtr4g 285 |
. . . . . . . . . . . . . . 15
|
319 | 318 | con3d 148 |
. . . . . . . . . . . . . 14
|
320 | 319 | impr 649 |
. . . . . . . . . . . . 13
|
321 | 296, 320 | sylan2b 492 |
. . . . . . . . . . . 12
|
322 | 295, 321 | eldifd 3585 |
. . . . . . . . . . 11
|
323 | 322 | ralrimiva 2966 |
. . . . . . . . . 10
|
324 | 292, 323 | jca 554 |
. . . . . . . . 9
|
325 | | eleq2 2690 |
. . . . . . . . . . 11
|
326 | | eleq2 2690 |
. . . . . . . . . . . 12
|
327 | 326 | raleqbi1dv 3146 |
. . . . . . . . . . 11
|
328 | 325, 327 | anbi12d 747 |
. . . . . . . . . 10
|
329 | 328, 7 | elrab2 3366 |
. . . . . . . . 9
|
330 | 233, 324,
329 | sylanbrc 698 |
. . . . . . . 8
|
331 | | wilthlem2.r |
. . . . . . . . 9
g |
332 | 331 | adantr 481 |
. . . . . . . 8
g
|
333 | | sseqin2 3817 |
. . . . . . . . . . 11
|
334 | 99, 333 | sylib 208 |
. . . . . . . . . 10
|
335 | | vex 3203 |
. . . . . . . . . . . 12
|
336 | 335 | prnz 4310 |
. . . . . . . . . . 11
|
337 | 336 | a1i 11 |
. . . . . . . . . 10
|
338 | 334, 337 | eqnetrd 2861 |
. . . . . . . . 9
|
339 | | disj4 4025 |
. . . . . . . . . 10
|
340 | 339 | necon2abii 2844 |
. . . . . . . . 9
|
341 | 338, 340 | sylibr 224 |
. . . . . . . 8
|
342 | | psseq1 3694 |
. . . . . . . . . 10
|
343 | | reseq2 5391 |
. . . . . . . . . . . . 13
|
344 | 343 | oveq2d 6666 |
. . . . . . . . . . . 12
g g |
345 | 344 | oveq1d 6665 |
. . . . . . . . . . 11
g g |
346 | 345 | eqeq1d 2624 |
. . . . . . . . . 10
g g
|
347 | 342, 346 | imbi12d 334 |
. . . . . . . . 9
g
g
|
348 | 347 | rspcv 3305 |
. . . . . . . 8
g
g |
349 | 330, 332,
341, 348 | syl3c 66 |
. . . . . . 7
g |
350 | 230, 349 | eqtrd 2656 |
. . . . . 6
g
|
351 | 113, 227,
350 | 3eqtrd 2660 |
. . . . 5
g |
352 | 351 | ex 450 |
. . . 4
g
|
353 | 352 | exlimdv 1861 |
. . 3
g |
354 | 57, 353 | syl5bi 232 |
. 2
g |
355 | 56, 354 | pm2.61d 170 |
1
g |