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

Theorem wilthlem2 20844
 Description: Lemma for wilth 20846: induction step. The "hand proof" version of this theorem works by writing out the list of all numbers from to in pairs such that a number is paired with its inverse. Every number has a unique inverse different from itself except and , and so each pair multiplies to , and and multiply to , so the full product is equal to . Here we make this precise by doing the product pair by pair. The induction hypothesis says that every subset of that is closed under inverse (i.e. all pairs are matched up) and contains multiplies to . Given such a set, we take out one element . If there are no such elements, then which forms the base case. Otherwise, is also closed under inverse and contains , so the induction hypothesis says that this equals ; and the remaining two elements are either equal to each other, in which case wilthlem1 20843 gives that or , and we've already excluded the second case, so the product gives ; or and their product is . In either case the accumulated product is unaffected. (Contributed by Mario Carneiro, 24-Jan-2015.)
Hypotheses
Ref Expression
wilthlem.t mulGrpfld
wilthlem.a
wilthlem2.p
wilthlem2.s
wilthlem2.r g
Assertion
Ref Expression
wilthlem2 g
Distinct variable groups:   ,,,   ,,,   ,,   ,,,   ,,,
Allowed substitution hint:   ()

Proof of Theorem wilthlem2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpr 448 . . . . . . . . 9
2 wilthlem2.s . . . . . . . . . . . . . 14
3 eleq2 2496 . . . . . . . . . . . . . . . 16
4 eleq2 2496 . . . . . . . . . . . . . . . . 17
54raleqbi1dv 2904 . . . . . . . . . . . . . . . 16
63, 5anbi12d 692 . . . . . . . . . . . . . . 15
7 wilthlem.a . . . . . . . . . . . . . . 15
86, 7elrab2 3086 . . . . . . . . . . . . . 14
92, 8sylib 189 . . . . . . . . . . . . 13
109simprd 450 . . . . . . . . . . . 12
1110simpld 446 . . . . . . . . . . 11
1211snssd 3935 . . . . . . . . . 10
1312adantr 452 . . . . . . . . 9
141, 13eqssd 3357 . . . . . . . 8
1514reseq2d 5138 . . . . . . 7
16 mptresid 5187 . . . . . . 7
1715, 16syl6eqr 2485 . . . . . 6
1817oveq2d 6089 . . . . 5 g g
1918oveq1d 6088 . . . 4 g g
20 wilthlem2.p . . . . . . . . . . . 12
21 prmnn 13074 . . . . . . . . . . . 12
2220, 21syl 16 . . . . . . . . . . 11
2322nncnd 10008 . . . . . . . . . 10
24 ax-1cn 9040 . . . . . . . . . 10
25 negsub 9341 . . . . . . . . . 10
2623, 24, 25sylancl 644 . . . . . . . . 9
27 neg1cn 10059 . . . . . . . . . 10
28 addcom 9244 . . . . . . . . . 10
2923, 27, 28sylancl 644 . . . . . . . . 9
3026, 29eqtr3d 2469 . . . . . . . 8
31 cnrng 16715 . . . . . . . . . 10 fld
32 wilthlem.t . . . . . . . . . . 11 mulGrpfld
3332rngmgp 15662 . . . . . . . . . 10 fld
3431, 33mp1i 12 . . . . . . . . 9
35 nnm1nn0 10253 . . . . . . . . . . 11
3622, 35syl 16 . . . . . . . . . 10
3736nn0cnd 10268 . . . . . . . . 9
38 cnfldbas 16699 . . . . . . . . . . 11 fld
3932, 38mgpbas 15646 . . . . . . . . . 10
40 id 20 . . . . . . . . . 10
4139, 40gsumsn 15535 . . . . . . . . 9 g
4234, 37, 37, 41syl3anc 1184 . . . . . . . 8 g
4323mulid2d 9098 . . . . . . . . 9
4443oveq2d 6089 . . . . . . . 8
4530, 42, 443eqtr4d 2477 . . . . . . 7 g
4645oveq1d 6088 . . . . . 6 g
47 1re 9082 . . . . . . . . 9
4847renegcli 9354 . . . . . . . 8
4948a1i 11 . . . . . . 7
5022nnrpd 10639 . . . . . . 7
51 1z 10303 . . . . . . . 8
5251a1i 11 . . . . . . 7
53 modcyc 11268 . . . . . . 7
5449, 50, 52, 53syl3anc 1184 . . . . . 6
5546, 54eqtrd 2467 . . . . 5 g
5655adantr 452 . . . 4 g
5719, 56eqtrd 2467 . . 3 g
5857ex 424 . 2 g
59 nss 3398 . . 3
60 cnfld1 16718 . . . . . . . . . 10 fld
6132, 60rngidval 15658 . . . . . . . . 9
62 cnfldmul 16701 . . . . . . . . . 10 fld
6332, 62mgpplusg 15644 . . . . . . . . 9
64 cncrng 16714 . . . . . . . . . . 11 fld
6532crngmgp 15664 . . . . . . . . . . 11 fld CMnd
6664, 65ax-mp 8 . . . . . . . . . 10 CMnd
6766a1i 11 . . . . . . . . 9 CMnd
682adantr 452 . . . . . . . . 9
69 f1oi 5705 . . . . . . . . . . . 12
70 f1of 5666 . . . . . . . . . . . 12
7169, 70ax-mp 8 . . . . . . . . . . 11
729simpld 446 . . . . . . . . . . . . . 14
7372elpwid 3800 . . . . . . . . . . . . 13
74 elfzelz 11051 . . . . . . . . . . . . . 14
7574ssriv 3344 . . . . . . . . . . . . 13
7673, 75syl6ss 3352 . . . . . . . . . . . 12
77 zsscn 10282 . . . . . . . . . . . 12
7876, 77syl6ss 3352 . . . . . . . . . . 11
79 fss 5591 . . . . . . . . . . 11
8071, 78, 79sylancr 645 . . . . . . . . . 10
8180adantr 452 . . . . . . . . 9
82 fzfi 11303 . . . . . . . . . . . 12
83 ssfi 7321 . . . . . . . . . . . 12
8482, 73, 83sylancr 645 . . . . . . . . . . 11
85 cnvimass 5216 . . . . . . . . . . . 12
86 dmresi 5188 . . . . . . . . . . . 12
8785, 86sseqtri 3372 . . . . . . . . . . 11
88 ssfi 7321 . . . . . . . . . . 11
8984, 87, 88sylancl 644 . . . . . . . . . 10
9089adantr 452 . . . . . . . . 9
91 disjdif 3692 . . . . . . . . . 10
9291a1i 11 . . . . . . . . 9
93 undif2 3696 . . . . . . . . . 10
94 simprl 733 . . . . . . . . . . . 12
9510simprd 450 . . . . . . . . . . . . . 14
9695adantr 452 . . . . . . . . . . . . 13
97 oveq1 6080 . . . . . . . . . . . . . . . 16
9897oveq1d 6088 . . . . . . . . . . . . . . 15
9998eleq1d 2501 . . . . . . . . . . . . . 14
10099rspcv 3040 . . . . . . . . . . . . 13
10194, 96, 100sylc 58 . . . . . . . . . . . 12
102 prssi 3946 . . . . . . . . . . . 12
10394, 101, 102syl2anc 643 . . . . . . . . . . 11
104 ssequn1 3509 . . . . . . . . . . 11
105103, 104sylib 189 . . . . . . . . . 10
10693, 105syl5req 2480 . . . . . . . . 9
10739, 61, 63, 67, 68, 81, 90, 92, 106gsumsplit 15522 . . . . . . . 8 g g g
108 resabs1 5167 . . . . . . . . . . 11
109103, 108syl 16 . . . . . . . . . 10
110109oveq2d 6089 . . . . . . . . 9 g g
111 difss 3466 . . . . . . . . . . . 12
112 resabs1 5167 . . . . . . . . . . . 12
113111, 112ax-mp 8 . . . . . . . . . . 11
114113oveq2i 6084 . . . . . . . . . 10 g g
115114a1i 11 . . . . . . . . 9 g g
116110, 115oveq12d 6091 . . . . . . . 8 g g g g
117107, 116eqtrd 2467 . . . . . . 7 g g g
118117oveq1d 6088 . . . . . 6 g g g
119 prfi 7373 . . . . . . . . . 10
120119a1i 11 . . . . . . . . 9
121 zsubrg 16744 . . . . . . . . . 10 SubRingfld
12232subrgsubm 15873 . . . . . . . . . 10 SubRingfld SubMnd
123121, 122mp1i 12 . . . . . . . . 9 SubMnd
124 f1oi 5705 . . . . . . . . . . 11
125 f1of 5666 . . . . . . . . . . 11
126124, 125ax-mp 8 . . . . . . . . . 10
12776adantr 452 . . . . . . . . . . 11
128103, 127sstrd 3350 . . . . . . . . . 10
129 fss 5591 . . . . . . . . . 10
130126, 128, 129sylancr 645 . . . . . . . . 9
131120, 130fisuppfi 14765 . . . . . . . . 9
13261, 67, 120, 123, 130, 131gsumsubmcl 15516 . . . . . . . 8 g
133132zred 10367 . . . . . . 7 g
13447a1i 11 . . . . . . 7
13573adantr 452 . . . . . . . . . 10
136135ssdifssd 3477 . . . . . . . . 9
137 ssfi 7321 . . . . . . . . 9
13882, 136, 137sylancr 645 . . . . . . . 8
139 f1oi 5705 . . . . . . . . . 10
140 f1of 5666 . . . . . . . . . 10
141139, 140ax-mp 8 . . . . . . . . 9
142127ssdifssd 3477 . . . . . . . . 9
143 fss 5591 . . . . . . . . 9
144141, 142, 143sylancr 645 . . . . . . . 8
145138, 144fisuppfi 14765 . . . . . . . 8
14661, 67, 138, 123, 144, 145gsumsubmcl 15516 . . . . . . 7 g
14750adantr 452 . . . . . . 7
14834adantr 452 . . . . . . . . . . . 12
14978adantr 452 . . . . . . . . . . . . 13
150149, 94sseldd 3341 . . . . . . . . . . . 12
151 id 20 . . . . . . . . . . . . 13
15239, 151gsumsn 15535 . . . . . . . . . . . 12 g
153148, 150, 150, 152syl3anc 1184 . . . . . . . . . . 11 g
154153adantr 452 . . . . . . . . . 10 g
155 mptresid 5187 . . . . . . . . . . . 12
156 dfsn2 3820 . . . . . . . . . . . . . 14
157 simpr 448 . . . . . . . . . . . . . . . . 17
158157orcd 382 . . . . . . . . . . . . . . . 16
15920adantr 452 . . . . . . . . . . . . . . . . . 18
160135, 94sseldd 3341 . . . . . . . . . . . . . . . . . 18
161 wilthlem1 20843 . . . . . . . . . . . . . . . . . 18
162159, 160, 161syl2anc 643 . . . . . . . . . . . . . . . . 17
163162biimpar 472 . . . . . . . . . . . . . . . 16
164158, 163syldan 457 . . . . . . . . . . . . . . 15
165164preq2d 3882 . . . . . . . . . . . . . 14
166156, 165syl5eq 2479 . . . . . . . . . . . . 13
167166reseq2d 5138 . . . . . . . . . . . 12
168155, 167syl5eq 2479 . . . . . . . . . . 11
169168oveq2d 6089 . . . . . . . . . 10 g g
170154, 169, 1573eqtr3d 2475 . . . . . . . . 9 g
171170oveq1d 6088 . . . . . . . 8 g
172 df-pr 3813 . . . . . . . . . . . . . . 15
173172reseq2i 5135 . . . . . . . . . . . . . 14
174 mptresid 5187 . . . . . . . . . . . . . 14
175173, 174eqtr4i 2458 . . . . . . . . . . . . 13
176175oveq2i 6084 . . . . . . . . . . . 12 g g
17766a1i 11 . . . . . . . . . . . . 13 CMnd
178 snfi 7179 . . . . . . . . . . . . . 14
179178a1i 11 . . . . . . . . . . . . 13
180 elsni 3830 . . . . . . . . . . . . . . . 16
181180adantl 453 . . . . . . . . . . . . . . 15
182150adantr 452 . . . . . . . . . . . . . . 15
183181, 182eqeltrd 2509 . . . . . . . . . . . . . 14
184183adantlr 696 . . . . . . . . . . . . 13
185149, 101sseldd 3341 . . . . . . . . . . . . . 14
186185adantr 452 . . . . . . . . . . . . 13
187 simprr 734 . . . . . . . . . . . . . . . . . 18
188 elsn 3821 . . . . . . . . . . . . . . . . . 18
189187, 188sylnib 296 . . . . . . . . . . . . . . . . 17
190 biorf 395 . . . . . . . . . . . . . . . . 17
191189, 190syl 16 . . . . . . . . . . . . . . . 16
192 ovex 6098 . . . . . . . . . . . . . . . . . . 19
193192elsnc 3829 . . . . . . . . . . . . . . . . . 18
194 eqcom 2437 . . . . . . . . . . . . . . . . . 18
195193, 194bitri 241 . . . . . . . . . . . . . . . . 17
196 orcom 377 . . . . . . . . . . . . . . . . 17
197162, 195, 1963bitr4g 280 . . . . . . . . . . . . . . . 16
198191, 197bitr4d 248 . . . . . . . . . . . . . . 15
199198necon3abid 2631 . . . . . . . . . . . . . 14
200199biimpa 471 . . . . . . . . . . . . 13
201 id 20 . . . . . . . . . . . . 13
20239, 63, 177, 179, 184, 186, 200, 186, 201gsumunsn 15536 . . . . . . . . . . . 12 g g
203176, 202syl5eq 2479 . . . . . . . . . . 11 g g
204153adantr 452 . . . . . . . . . . . 12 g
205204oveq1d 6088 . . . . . . . . . . 11 g
206203, 205eqtrd 2467 . . . . . . . . . 10 g
207206oveq1d 6088 . . . . . . . . 9 g
208160, 74syl 16 . . . . . . . . . . . . 13
20922adantr 452 . . . . . . . . . . . . . 14
210 fzm1ndvds 12893 . . . . . . . . . . . . . 14
211209, 160, 210syl2anc 643 . . . . . . . . . . . . 13
212 eqid 2435 . . . . . . . . . . . . . 14
213212prmdiv 13166 . . . . . . . . . . . . 13
214159, 208, 211, 213syl3anc 1184 . . . . . . . . . . . 12
215214simprd 450 . . . . . . . . . . 11
216 elfznn 11072 . . . . . . . . . . . . . . 15
217160, 216syl 16 . . . . . . . . . . . . . 14
218135, 101sseldd 3341 . . . . . . . . . . . . . . 15
219 elfznn 11072 . . . . . . . . . . . . . . 15
220218, 219syl 16 . . . . . . . . . . . . . 14
221217, 220nnmulcld 10039 . . . . . . . . . . . . 13
222221nnzd 10366 . . . . . . . . . . . 12
22351a1i 11 . . . . . . . . . . . 12
224 moddvds 12851 . . . . . . . . . . . 12
225209, 222, 223, 224syl3anc 1184 . . . . . . . . . . 11
226215, 225mpbird 224 . . . . . . . . . 10
227226adantr 452 . . . . . . . . 9
228207, 227eqtrd 2467 . . . . . . . 8 g
229171, 228pm2.61dane 2676 . . . . . . 7 g
230 modmul1 11271 . . . . . . 7 g g g g g g
231133, 134, 146, 147, 229, 230syl221anc 1195 . . . . . 6 g g g
232146zcnd 10368 . . . . . . . . 9 g
233232mulid2d 9098 . . . . . . . 8 g g
234233oveq1d 6088 . . . . . . 7 g g
235 ovex 6098 . . . . . . . . . . 11
236235elpw2 4356 . . . . . . . . . 10
237136, 236sylibr 204 . . . . . . . . 9
23811adantr 452 . . . . . . . . . . 11
239 eqcom 2437 . . . . . . . . . . . . . . 15
240188, 239bitri 241 . . . . . . . . . . . . . 14
241187, 240sylnib 296 . . . . . . . . . . . . 13
242 oveq1 6080 . . . . . . . . . . . . . . . 16
243242oveq1d 6088 . . . . . . . . . . . . . . 15
244209, 35syl 16 . . . . . . . . . . . . . . . . . . 19
245 nn0uz 10512 . . . . . . . . . . . . . . . . . . 19
246244, 245syl6eleq 2525 . . . . . . . . . . . . . . . . . 18
247 eluzfz2 11057 . . . . . . . . . . . . . . . . . 18
248246, 247syl 16 . . . . . . . . . . . . . . . . 17
249 prmz 13075 . . . . . . . . . . . . . . . . . . . 20
250159, 249syl 16 . . . . . . . . . . . . . . . . . . 19
251127, 238sseldd 3341 . . . . . . . . . . . . . . . . . . . 20
252 zsubcl 10311 . . . . . . . . . . . . . . . . . . . 20
253251, 51, 252sylancl 644 . . . . . . . . . . . . . . . . . . 19
254 dvdsmul1 12863 . . . . . . . . . . . . . . . . . . 19
255250, 253, 254syl2anc 643 . . . . . . . . . . . . . . . . . 18
256209nncnd 10008 . . . . . . . . . . . . . . . . . . . . . 22
25724a1i 11 . . . . . . . . . . . . . . . . . . . . . 22
258244nn0cnd 10268 . . . . . . . . . . . . . . . . . . . . . 22
259256, 257, 258subdird 9482 . . . . . . . . . . . . . . . . . . . . 21
260256, 258mulcld 9100 . . . . . . . . . . . . . . . . . . . . . . 23
261260, 256, 257subsubd 9431 . . . . . . . . . . . . . . . . . . . . . 22
262258mulid2d 9098 . . . . . . . . . . . . . . . . . . . . . . 23
263262oveq2d 6089 . . . . . . . . . . . . . . . . . . . . . 22
264256, 258, 257subdid 9481 . . . . . . . . . . . . . . . . . . . . . . . 24
265256mulid1d 9097 . . . . . . . . . . . . . . . . . . . . . . . . 25
266265oveq2d 6089 . . . . . . . . . . . . . . . . . . . . . . . 24
267264, 266eqtrd 2467 . . . . . . . . . . . . . . . . . . . . . . 23
268267oveq1d 6088 . . . . . . . . . . . . . . . . . . . . . 22
269261, 263, 2683eqtr4d 2477 . . . . . . . . . . . . . . . . . . . . 21
270259, 269eqtrd 2467 . . . . . . . . . . . . . . . . . . . 20
271270oveq1d 6088 . . . . . . . . . . . . . . . . . . 19
272253zcnd 10368 . . . . . . . . . . . . . . . . . . . . 21
273256, 272mulcld 9100 . . . . . . . . . . . . . . . . . . . 20
274 pncan 9303 . . . . . . . . . . . . . . . . . . . 20
275273, 24, 274sylancl 644 . . . . . . . . . . . . . . . . . . 19
276271, 275eqtrd 2467 . . . . . . . . . . . . . . . . . 18
277255, 276breqtrrd 4230 . . . . . . . . . . . . . . . . 17
278135, 238sseldd 3341 . . . . . . . . . . . . . . . . . . 19
279 fzm1ndvds 12893 . . . . . . . . . . . . . . . . . . 19
280209, 278, 279syl2anc 643 . . . . . . . . . . . . . . . . . 18
281 eqid 2435 . . . . . . . . . . . . . . . . . . 19
282281prmdiveq 13167 . . . . . . . . . . . . . . . . . 18
283159, 251, 280, 282syl3anc 1184 . . . . . . . . . . . . . . . . 17
284248, 277, 283mpbi2and 888 . . . . . . . . . . . . . . . 16
285212prmdivdiv 13168 . . . . . . . . . . . . . . . . 17
286159, 160, 285syl2anc 643 . . . . . . . . . . . . . . . 16
287284, 286eqeq12d 2449 . . . . . . . . . . . . . . 15
288243, 287syl5ibr 213 . . . . . . . . . . . . . 14
289241, 288mtod 170 . . . . . . . . . . . . 13
290 ioran 477 . . . . . . . . . . . . 13
291241, 289, 290sylanbrc 646 . . . . . . . . . . . 12
292 ovex 6098 . . . . . . . . . . . . 13
293292elpr 3824 . . . . . . . . . . . 12
294291, 293sylnibr 297 . . . . . . . . . . 11
295238, 294eldifd 3323 . . . . . . . . . 10
296 eldifi 3461 . . . . . . . . . . . . 13
29796r19.21bi 2796 . . . . . . . . . . . . 13
298296, 297sylan2 461 . . . . . . . . . . . 12
299 eldif 3322 . . . . . . . . . . . . 13
300159adantr 452 . . . . . . . . . . . . . . . . . . 19
301135sselda 3340 . . . . . . . . . . . . . . . . . . 19
302 eqid 2435 . . . . . . . . . . . . . . . . . . . 20
303302prmdivdiv 13168 . . . . . . . . . . . . . . . . . . 19
304300, 301, 303syl2anc 643 . . . . . . . . . . . . . . . . . 18
305 oveq1 6080 . . . . . . . . . . . . . . . . . . . 20
306305oveq1d 6088 . . . . . . . . . . . . . . . . . . 19
307306eqeq2d 2446 . . . . . . . . . . . . . . . . . 18
308304, 307syl5ibcom 212 . . . . . . . . . . . . . . . . 17
309 oveq1 6080 . . . . . . . . . . . . . . . . . . 19
310309oveq1d 6088 . . . . . . . . . . . . . . . . . 18
311286adantr 452 . . . . . . . . . . . . . . . . . . 19
312304, 311eqeq12d 2449 . . . . . . . . . . . . . . . . . 18
313310, 312syl5ibr 213 . . . . . . . . . . . . . . . . 17
314308, 313orim12d 812 . . . . . . . . . . . . . . . 16
315 ovex 6098 . . . . . . . . . . . . . . . . 17
316315elpr 3824 . . . . . . . . . . . . . . . 16
317 vex 2951 . . . . . . . . . . . . . . . . . 18
318317elpr 3824 . . . . . . . . . . . . . . . . 17
319 orcom 377 . . . . . . . . . . . . . . . . 17
320318, 319bitri 241 . . . . . . . . . . . . . . . 16
321314, 316, 3203imtr4g 262 . . . . . . . . . . . . . . 15
322321con3d 127 . . . . . . . . . . . . . 14
323322impr 603 . . . . . . . . . . . . 13
324299, 323sylan2b 462 . . . . . . . . . . . 12
325298, 324eldifd 3323 . . . . . . . . . . 11
326325ralrimiva 2781 . . . . . . . . . 10
327295, 326jca 519 . . . . . . . . 9
328 eleq2 2496 . . . . . . . . . . 11
329 eleq2 2496 . . . . . . . . . . . 12
330329raleqbi1dv 2904 . . . . . . . . . . 11
331328, 330anbi12d 692 . . . . . . . . . 10
332331, 7elrab2 3086 . . . . . . . . 9
333237, 327, 332sylanbrc 646 . . . . . . . 8
334 wilthlem2.r . . . . . . . . 9 g
335334adantr 452 . . . . . . . 8 g
336 dfss1 3537 . . . . . . . . . . 11
337103, 336sylib 189 . . . . . . . . . 10
338 vex 2951 . . . . . . . . . . . 12
339338prnz 3915 . . . . . . . . . . 11
340339a1i 11 . . . . . . . . . 10
341337, 340eqnetrd 2616 . . . . . . . . 9
342 disj4 3668 . . . . . . . . . 10
343342necon2abii 2653 . . . . . . . . 9
344341, 343sylibr 204 . . . . . . . 8
345 psseq1 3426 . . . . . . . . . 10
346 reseq2 5133 . . . . . . . . . . . . 13
347346oveq2d 6089 . . . . . . . . . . . 12 g g
348347oveq1d 6088 . . . . . . . . . . 11 g g
349348eqeq1d 2443 . . . . . . . . . 10 g g
350345, 349imbi12d 312 . . . . . . . . 9 g g
351350rspcv 3040 . . . . . . . 8 g g
352333, 335, 344, 351syl3c 59 . . . . . . 7 g
353234, 352eqtrd 2467 . . . . . 6 g