lgsquadlem3 - Metamath Proof Explorer

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

Theorem lgsquadlem3 22670

Description: Lemma for lgsquad 22671. (Contributed by Mario Carneiro, 18-Jun-2015.)

**Hypotheses**
Ref	Expression
lgseisen.1	$\$
lgseisen.2	$\$
lgseisen.3
lgsquad.4
lgsquad.5
lgsquad.6	$/\$ $/\$

**Assertion**
Ref	Expression
lgsquadlem3

Distinct variable groups:

Proof of Theorem lgsquadlem3 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		lgseisen.2	. . . . 5 $\$
2		lgseisen.1	. . . . 5 $\$
3		lgseisen.3	. . . . . 6
4	3	necomd 2690	. . . . 5
5		lgsquad.5	. . . . 5
6		lgsquad.4	. . . . 5
7		eleq1 2498	. . . . . . . . . 10
8		eleq1 2498	. . . . . . . . . 10
9	7, 8	bi2anan9 868	. . . . . . . . 9 $/\$ $/\$ $/\$
10		ancom 450	. . . . . . . . 9 $/\$ $/\$
11	9, 10	syl6bb 261	. . . . . . . 8 $/\$ $/\$ $/\$
12		oveq1 6093	. . . . . . . . 9
13		oveq1 6093	. . . . . . . . 9
14	12, 13	breqan12d 4302	. . . . . . . 8 $/\$
15	11, 14	anbi12d 710	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
16	15	ancoms 453	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
17	16	cbvopabv 4356	. . . . 5 $/\$ $/\$ $/\$ $/\$
18	1, 2, 4, 5, 6, 17	lgsquadlem2 22669	. . . 4 $/\$ $/\$
19		relopab 4961	. . . . . . . 8 $/\$ $/\$
20		fzfid 11787	. . . . . . . . . 10
21		fzfid 11787	. . . . . . . . . 10
22		xpfi 7575	. . . . . . . . . 10 $/\$
23	20, 21, 22	syl2anc 661	. . . . . . . . 9
24		opabssxp 4906	. . . . . . . . 9 $/\$ $/\$
25		ssfi 7525	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
26	23, 24, 25	sylancl 662	. . . . . . . 8 $/\$ $/\$
27		cnven 7377	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
28	19, 26, 27	sylancr 663	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
29		cnvopab 5233	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
30	28, 29	syl6breq 4326	. . . . . 6 $/\$ $/\$ $/\$ $/\$
31		hasheni 12111	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
32	30, 31	syl 16	. . . . 5 $/\$ $/\$ $/\$ $/\$
33	32	oveq2d 6102	. . . 4 $/\$ $/\$ $/\$ $/\$
34	18, 33	eqtr4d 2473	. . 3 $/\$ $/\$
35		lgsquad.6	. . . 4 $/\$ $/\$
36	2, 1, 3, 6, 5, 35	lgsquadlem2 22669	. . 3
37	34, 36	oveq12d 6104	. 2 $/\$ $/\$
38		neg1cn 10417	. . . 4
39	38	a1i 11	. . 3
40		opabssxp 4906	. . . . . 6 $/\$ $/\$
41	35, 40	eqsstri 3381	. . . . 5
42		ssfi 7525	. . . . 5 $/\$
43	23, 41, 42	sylancl 662	. . . 4
44		hashcl 12118	. . . 4
45	43, 44	syl 16	. . 3
46		hashcl 12118	. . . 4 $/\$ $/\$ $/\$ $/\$
47	26, 46	syl 16	. . 3 $/\$ $/\$
48	39, 45, 47	expaddd 12002	. 2 $/\$ $/\$ $/\$ $/\$
49	1	eldifad 3335	. . . . . . . . . . . . . . . . 17
50	49	adantr 465	. . . . . . . . . . . . . . . 16 $/\$ $/\$
51		prmnn 13758	. . . . . . . . . . . . . . . 16
52	50, 51	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$
53		oddprm 13874	. . . . . . . . . . . . . . . . . . . . . 22 $\$
54	1, 53	syl 16	. . . . . . . . . . . . . . . . . . . . 21
55	5, 54	syl5eqel 2522	. . . . . . . . . . . . . . . . . . . 20
56	55	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
57	56	nnzd 10738	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
58		prmz 13759	. . . . . . . . . . . . . . . . . . . 20
59	50, 58	syl 16	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
60		peano2zm 10680	. . . . . . . . . . . . . . . . . . 19
61	59, 60	syl 16	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
62	56	nnred 10329	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
63	61	zred 10739	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
64		prmuz2 13773	. . . . . . . . . . . . . . . . . . . . . . . 24
65	50, 64	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
66		uz2m1nn 10921	. . . . . . . . . . . . . . . . . . . . . . 23
67	65, 66	syl 16	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
68	67	nnrpd 11018	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
69		rphalflt 11009	. . . . . . . . . . . . . . . . . . . . 21
70	68, 69	syl 16	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
71	5, 70	syl5eqbr 4320	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
72	62, 63, 71	ltled 9514	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
73		eluz2 10859	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
74	57, 61, 72, 73	syl3anbrc 1172	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
75		fzss2 11490	. . . . . . . . . . . . . . . . 17
76	74, 75	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$
77		simprr 756	. . . . . . . . . . . . . . . 16 $/\$ $/\$
78	76, 77	sseldd 3352	. . . . . . . . . . . . . . 15 $/\$ $/\$
79		fzm1ndvds 13577	. . . . . . . . . . . . . . 15 $/\$
80	52, 78, 79	syl2anc 661	. . . . . . . . . . . . . 14 $/\$ $/\$
81	4	adantr 465	. . . . . . . . . . . . . . . 16 $/\$ $/\$
82	2	eldifad 3335	. . . . . . . . . . . . . . . . . 18
83	82	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
84		prmrp 13779	. . . . . . . . . . . . . . . . 17 $/\$
85	50, 83, 84	syl2anc 661	. . . . . . . . . . . . . . . 16 $/\$ $/\$
86	81, 85	mpbird 232	. . . . . . . . . . . . . . 15 $/\$ $/\$
87		prmz 13759	. . . . . . . . . . . . . . . . 17
88	83, 87	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$
89		elfzelz 11445	. . . . . . . . . . . . . . . . 17
90	89	ad2antll 728	. . . . . . . . . . . . . . . 16 $/\$ $/\$
91		coprmdvds 13780	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
92	59, 88, 90, 91	syl3anc 1218	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
93	86, 92	mpan2d 674	. . . . . . . . . . . . . 14 $/\$ $/\$
94	80, 93	mtod 177	. . . . . . . . . . . . 13 $/\$ $/\$
95		prmnn 13758	. . . . . . . . . . . . . . . . 17
96	83, 95	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$
97	96	nncnd 10330	. . . . . . . . . . . . . . 15 $/\$ $/\$
98		elfznn 11470	. . . . . . . . . . . . . . . . 17
99	98	ad2antll 728	. . . . . . . . . . . . . . . 16 $/\$ $/\$
100	99	nncnd 10330	. . . . . . . . . . . . . . 15 $/\$ $/\$
101	97, 100	mulcomd 9399	. . . . . . . . . . . . . 14 $/\$ $/\$
102	101	breq2d 4299	. . . . . . . . . . . . 13 $/\$ $/\$
103	94, 102	mtbid 300	. . . . . . . . . . . 12 $/\$ $/\$
104		elfzelz 11445	. . . . . . . . . . . . . . . 16
105	104	ad2antrl 727	. . . . . . . . . . . . . . 15 $/\$ $/\$
106		dvdsmul2 13547	. . . . . . . . . . . . . . 15 $/\$
107	105, 59, 106	syl2anc 661	. . . . . . . . . . . . . 14 $/\$ $/\$
108		breq2 4291	. . . . . . . . . . . . . 14
109	107, 108	syl5ibcom 220	. . . . . . . . . . . . 13 $/\$ $/\$
110	109	necon3bd 2640	. . . . . . . . . . . 12 $/\$ $/\$
111	103, 110	mpd 15	. . . . . . . . . . 11 $/\$ $/\$
112		elfznn 11470	. . . . . . . . . . . . . . 15
113	112	ad2antrl 727	. . . . . . . . . . . . . 14 $/\$ $/\$
114	113, 52	nnmulcld 10361	. . . . . . . . . . . . 13 $/\$ $/\$
115	114	nnred 10329	. . . . . . . . . . . 12 $/\$ $/\$
116	99, 96	nnmulcld 10361	. . . . . . . . . . . . 13 $/\$ $/\$
117	116	nnred 10329	. . . . . . . . . . . 12 $/\$ $/\$
118	115, 117	lttri2d 9505	. . . . . . . . . . 11 $/\$ $/\$ $\/$
119	111, 118	mpbid 210	. . . . . . . . . 10 $/\$ $/\$ $\/$
120	119	ex 434	. . . . . . . . 9 $/\$ $\/$
121	120	pm4.71rd 635	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$
122		ancom 450	. . . . . . . 8 $\/$ $/\$ $/\$ $/\$ $/\$ $\/$
123	121, 122	syl6rbb 262	. . . . . . 7 $/\$ $/\$ $\/$ $/\$
124	123	opabbidv 4350	. . . . . 6 $/\$ $/\$ $\/$ $/\$
125		unopab 4362	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
126	35	uneq2i 3502	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
127		andi 862	. . . . . . . 8 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $/\$
128	127	opabbii 4351	. . . . . . 7 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $/\$
129	125, 126, 128	3eqtr4i 2468	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $\/$
130		df-xp 4841	. . . . . 6 $/\$
131	124, 129, 130	3eqtr4g 2495	. . . . 5 $/\$ $/\$
132	131	fveq2d 5690	. . . 4 $/\$ $/\$
133		inopab 4965	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
134	35	ineq2i 3544	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
135		anandi 824	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
136	135	opabbii 4351	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
137	133, 134, 136	3eqtr4i 2468	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
138		ltnsym2 9466	. . . . . . . . . . . 12 $/\$ $/\$
139	115, 117, 138	syl2anc 661	. . . . . . . . . . 11 $/\$ $/\$ $/\$
140	139	ex 434	. . . . . . . . . 10 $/\$ $/\$
141		imnan 422	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
142	140, 141	sylib 196	. . . . . . . . 9 $/\$ $/\$ $/\$
143	142	nexdv 1934	. . . . . . . 8 $/\$ $/\$ $/\$
144	143	nexdv 1934	. . . . . . 7 $/\$ $/\$ $/\$
145		opabn0 4614	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
146	145	necon1bbii 2658	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
147	144, 146	sylib 196	. . . . . 6 $/\$ $/\$ $/\$
148	137, 147	syl5eq 2482	. . . . 5 $/\$ $/\$
149		hashun 12137	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
150	26, 43, 148, 149	syl3anc 1218	. . . 4 $/\$ $/\$ $/\$ $/\$
151		hashxp 12188	. . . . . 6 $/\$
152	20, 21, 151	syl2anc 661	. . . . 5
153		oddprm 13874	. . . . . . . . . 10 $\$
154	2, 153	syl 16	. . . . . . . . 9
155	6, 154	syl5eqel 2522	. . . . . . . 8
156	155	nnnn0d 10628	. . . . . . 7
157		hashfz1 12109	. . . . . . 7
158	156, 157	syl 16	. . . . . 6
159	55	nnnn0d 10628	. . . . . . 7
160		hashfz1 12109	. . . . . . 7
161	159, 160	syl 16	. . . . . 6
162	158, 161	oveq12d 6104	. . . . 5
163	152, 162	eqtrd 2470	. . . 4
164	132, 150, 163	3eqtr3d 2478	. . 3 $/\$ $/\$
165	164	oveq2d 6102	. 2 $/\$ $/\$
166	37, 48, 165	3eqtr2d 2476	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $\/$ wo 368 $/\$ wa 369

wceq 1369

wex 1586

wcel 1756

wne 2601 $\$ cdif 3320

cun 3321

cin 3322

wss 3323

c0 3632

csn 3872 class class class wbr 4287

copab 4344

cxp 4833

ccnv 4834

wrel 4840

cfv 5413 (class class class)co 6086

cen 7299

cfn 7302

cc 9272

cr 9273

c1 9275

caddc 9277

cmul 9279

clt 9410

cle 9411

cmin 9587

cneg 9588

cdiv 9985

cn 10314

c2 10363

cn0 10571

cz 10638

cuz 10853

crp 10983

cfz 11429

cexp 11857

chash 12095

cdivides 13527

cgcd 13682

cprime 13755

clgs 22608

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2419 ax-rep 4398 ax-sep 4408 ax-nul 4416 ax-pow 4465 ax-pr 4526 ax-un 6367 ax-inf2 7839 ax-cnex 9330 ax-resscn 9331 ax-1cn 9332 ax-icn 9333 ax-addcl 9334 ax-addrcl 9335 ax-mulcl 9336 ax-mulrcl 9337 ax-mulcom 9338 ax-addass 9339 ax-mulass 9340 ax-distr 9341 ax-i2m1 9342 ax-1ne0 9343 ax-1rid 9344 ax-rnegex 9345 ax-rrecex 9346 ax-cnre 9347 ax-pre-lttri 9348 ax-pre-lttrn 9349 ax-pre-ltadd 9350 ax-pre-mulgt0 9351 ax-pre-sup 9352 ax-addf 9353 ax-mulf 9354

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-fal 1375 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2256 df-mo 2257 df-clab 2425 df-cleq 2431 df-clel 2434 df-nfc 2563 df-ne 2603 df-nel 2604 df-ral 2715 df-rex 2716 df-reu 2717 df-rmo 2718 df-rab 2719 df-v 2969 df-sbc 3182 df-csb 3284 df-dif 3326 df-un 3328 df-in 3330 df-ss 3337 df-pss 3339 df-nul 3633 df-if 3787 df-pw 3857 df-sn 3873 df-pr 3875 df-tp 3877 df-op 3879 df-uni 4087 df-int 4124 df-iun 4168 df-disj 4258 df-br 4288 df-opab 4346 df-mpt 4347 df-tr 4381 df-eprel 4627 df-id 4631 df-po 4636 df-so 4637 df-fr 4674 df-se 4675 df-we 4676 df-ord 4717 df-on 4718 df-lim 4719 df-suc 4720 df-xp 4841 df-rel 4842 df-cnv 4843 df-co 4844 df-dm 4845 df-rn 4846 df-res 4847 df-ima 4848 df-iota 5376 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-isom 5422 df-riota 6047 df-ov 6089 df-oprab 6090 df-mpt2 6091 df-of 6315 df-om 6472 df-1st 6572 df-2nd 6573 df-supp 6686 df-tpos 6740 df-recs 6824 df-rdg 6858 df-1o 6912 df-2o 6913 df-oadd 6916 df-er 7093 df-ec 7095 df-qs 7099 df-map 7208 df-en 7303 df-dom 7304 df-sdom 7305 df-fin 7306 df-fsupp 7613 df-sup 7683 df-oi 7716 df-card 8101 df-cda 8329 df-pnf 9412 df-mnf 9413 df-xr 9414 df-ltxr 9415 df-le 9416 df-sub 9589 df-neg 9590 df-div 9986 df-nn 10315 df-2 10372 df-3 10373 df-4 10374 df-5 10375 df-6 10376 df-7 10377 df-8 10378 df-9 10379 df-10 10380 df-n0 10572 df-z 10639 df-dec 10748 df-uz 10854 df-q 10946 df-rp 10984 df-fz 11430 df-fzo 11541 df-fl 11634 df-mod 11701 df-seq 11799 df-exp 11858 df-hash 12096 df-cj 12580 df-re 12581 df-im 12582 df-sqr 12716 df-abs 12717 df-clim 12958 df-sum 13156 df-dvds 13528 df-gcd 13683 df-prm 13756 df-phi 13833 df-pc 13896 df-struct 14168 df-ndx 14169 df-slot 14170 df-base 14171 df-sets 14172 df-ress 14173 df-plusg 14243 df-mulr 14244 df-starv 14245 df-sca 14246 df-vsca 14247 df-ip 14248 df-tset 14249 df-ple 14250 df-ds 14252 df-unif 14253 df-0g 14372 df-gsum 14373 df-imas 14438 df-divs 14439 df-mnd 15407 df-mhm 15456 df-submnd 15457 df-grp 15536 df-minusg 15537 df-sbg 15538 df-mulg 15539 df-subg 15669 df-nsg 15670 df-eqg 15671 df-ghm 15736 df-cntz 15826 df-cmn 16270 df-abl 16271 df-mgp 16580 df-ur 16592 df-rng 16635 df-cring 16636 df-oppr 16703 df-dvdsr 16721 df-unit 16722 df-invr 16752 df-dvr 16763 df-rnghom 16794 df-drng 16812 df-field 16813 df-subrg 16841 df-lmod 16928 df-lss 16991 df-lsp 17030 df-sra 17230 df-rgmod 17231 df-lidl 17232 df-rsp 17233 df-2idl 17291 df-nzr 17317 df-rlreg 17331 df-domn 17332 df-idom 17333 df-cnfld 17794 df-zring 17859 df-zrh 17910 df-zn 17913 df-lgs 22609

This theorem is referenced by: lgsquad 22671

W3C validator