lgsquadlem3 - Metamath Proof Explorer

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

Theorem lgsquadlem3 24147

Description: Lemma for lgsquad 24148. (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 2702	. . . . 5
5		lgsquad.5	. . . . 5
6		lgsquad.4	. . . . 5
7		eleq1 2501	. . . . . . . . . 10
8		eleq1 2501	. . . . . . . . . 10
9	7, 8	bi2anan9 881	. . . . . . . . 9 $/\$ $/\$ $/\$
10		ancom 451	. . . . . . . . 9 $/\$ $/\$
11	9, 10	syl6bb 264	. . . . . . . 8 $/\$ $/\$ $/\$
12		oveq1 6312	. . . . . . . . 9
13		oveq1 6312	. . . . . . . . 9
14	12, 13	breqan12d 4441	. . . . . . . 8 $/\$
15	11, 14	anbi12d 715	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
16	15	ancoms 454	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
17	16	cbvopabv 4495	. . . . 5 $/\$ $/\$ $/\$ $/\$
18	1, 2, 4, 5, 6, 17	lgsquadlem2 24146	. . . 4 $/\$ $/\$
19		relopab 4980	. . . . . . . 8 $/\$ $/\$
20		fzfid 12183	. . . . . . . . . 10
21		fzfid 12183	. . . . . . . . . 10
22		xpfi 7848	. . . . . . . . . 10 $/\$
23	20, 21, 22	syl2anc 665	. . . . . . . . 9
24		opabssxp 4929	. . . . . . . . 9 $/\$ $/\$
25		ssfi 7798	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
26	23, 24, 25	sylancl 666	. . . . . . . 8 $/\$ $/\$
27		cnven 7652	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
28	19, 26, 27	sylancr 667	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
29		cnvopab 5257	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
30	28, 29	syl6breq 4465	. . . . . 6 $/\$ $/\$ $/\$ $/\$
31		hasheni 12528	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
32	30, 31	syl 17	. . . . 5 $/\$ $/\$ $/\$ $/\$
33	32	oveq2d 6321	. . . 4 $/\$ $/\$ $/\$ $/\$
34	18, 33	eqtr4d 2473	. . 3 $/\$ $/\$
35		lgsquad.6	. . . 4 $/\$ $/\$
36	2, 1, 3, 6, 5, 35	lgsquadlem2 24146	. . 3
37	34, 36	oveq12d 6323	. 2 $/\$ $/\$
38		neg1cn 10713	. . . 4
39	38	a1i 11	. . 3
40		opabssxp 4929	. . . . . 6 $/\$ $/\$
41	35, 40	eqsstri 3500	. . . . 5
42		ssfi 7798	. . . . 5 $/\$
43	23, 41, 42	sylancl 666	. . . 4
44		hashcl 12535	. . . 4
45	43, 44	syl 17	. . 3
46		hashcl 12535	. . . 4 $/\$ $/\$ $/\$ $/\$
47	26, 46	syl 17	. . 3 $/\$ $/\$
48	39, 45, 47	expaddd 12415	. 2 $/\$ $/\$ $/\$ $/\$
49	1	eldifad 3454	. . . . . . . . . . . . . . . . 17
50	49	adantr 466	. . . . . . . . . . . . . . . 16 $/\$ $/\$
51		prmnn 14596	. . . . . . . . . . . . . . . 16
52	50, 51	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$
53		oddprm 14728	. . . . . . . . . . . . . . . . . . . . . 22 $\$
54	1, 53	syl 17	. . . . . . . . . . . . . . . . . . . . 21
55	5, 54	syl5eqel 2521	. . . . . . . . . . . . . . . . . . . 20
56	55	adantr 466	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
57	56	nnzd 11039	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
58		prmz 14597	. . . . . . . . . . . . . . . . . . . 20
59	50, 58	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
60		peano2zm 10980	. . . . . . . . . . . . . . . . . . 19
61	59, 60	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
62	56	nnred 10624	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
63	61	zred 11040	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
64		prmuz2 14613	. . . . . . . . . . . . . . . . . . . . . . . 24
65	50, 64	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
66		uz2m1nn 11233	. . . . . . . . . . . . . . . . . . . . . . 23
67	65, 66	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
68	67	nnrpd 11339	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
69		rphalflt 11329	. . . . . . . . . . . . . . . . . . . . 21
70	68, 69	syl 17	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
71	5, 70	syl5eqbr 4459	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
72	62, 63, 71	ltled 9782	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
73		eluz2 11165	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
74	57, 61, 72, 73	syl3anbrc 1189	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
75		fzss2 11836	. . . . . . . . . . . . . . . . 17
76	74, 75	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$
77		simprr 764	. . . . . . . . . . . . . . . 16 $/\$ $/\$
78	76, 77	sseldd 3471	. . . . . . . . . . . . . . 15 $/\$ $/\$
79		fzm1ndvds 14335	. . . . . . . . . . . . . . 15 $/\$
80	52, 78, 79	syl2anc 665	. . . . . . . . . . . . . 14 $/\$ $/\$
81	4	adantr 466	. . . . . . . . . . . . . . . 16 $/\$ $/\$
82	2	eldifad 3454	. . . . . . . . . . . . . . . . . 18
83	82	adantr 466	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
84		prmrp 14629	. . . . . . . . . . . . . . . . 17 $/\$
85	50, 83, 84	syl2anc 665	. . . . . . . . . . . . . . . 16 $/\$ $/\$
86	81, 85	mpbird 235	. . . . . . . . . . . . . . 15 $/\$ $/\$
87		prmz 14597	. . . . . . . . . . . . . . . . 17
88	83, 87	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$
89		elfzelz 11798	. . . . . . . . . . . . . . . . 17
90	89	ad2antll 733	. . . . . . . . . . . . . . . 16 $/\$ $/\$
91		coprmdvds 14630	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
92	59, 88, 90, 91	syl3anc 1264	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
93	86, 92	mpan2d 678	. . . . . . . . . . . . . 14 $/\$ $/\$
94	80, 93	mtod 180	. . . . . . . . . . . . 13 $/\$ $/\$
95		prmnn 14596	. . . . . . . . . . . . . . . . 17
96	83, 95	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$
97	96	nncnd 10625	. . . . . . . . . . . . . . 15 $/\$ $/\$
98		elfznn 11826	. . . . . . . . . . . . . . . . 17
99	98	ad2antll 733	. . . . . . . . . . . . . . . 16 $/\$ $/\$
100	99	nncnd 10625	. . . . . . . . . . . . . . 15 $/\$ $/\$
101	97, 100	mulcomd 9663	. . . . . . . . . . . . . 14 $/\$ $/\$
102	101	breq2d 4438	. . . . . . . . . . . . 13 $/\$ $/\$
103	94, 102	mtbid 301	. . . . . . . . . . . 12 $/\$ $/\$
104		elfzelz 11798	. . . . . . . . . . . . . . . 16
105	104	ad2antrl 732	. . . . . . . . . . . . . . 15 $/\$ $/\$
106		dvdsmul2 14303	. . . . . . . . . . . . . . 15 $/\$
107	105, 59, 106	syl2anc 665	. . . . . . . . . . . . . 14 $/\$ $/\$
108		breq2 4430	. . . . . . . . . . . . . 14
109	107, 108	syl5ibcom 223	. . . . . . . . . . . . 13 $/\$ $/\$
110	109	necon3bd 2643	. . . . . . . . . . . 12 $/\$ $/\$
111	103, 110	mpd 15	. . . . . . . . . . 11 $/\$ $/\$
112		elfznn 11826	. . . . . . . . . . . . . . 15
113	112	ad2antrl 732	. . . . . . . . . . . . . 14 $/\$ $/\$
114	113, 52	nnmulcld 10657	. . . . . . . . . . . . 13 $/\$ $/\$
115	114	nnred 10624	. . . . . . . . . . . 12 $/\$ $/\$
116	99, 96	nnmulcld 10657	. . . . . . . . . . . . 13 $/\$ $/\$
117	116	nnred 10624	. . . . . . . . . . . 12 $/\$ $/\$
118	115, 117	lttri2d 9773	. . . . . . . . . . 11 $/\$ $/\$ $\/$
119	111, 118	mpbid 213	. . . . . . . . . 10 $/\$ $/\$ $\/$
120	119	ex 435	. . . . . . . . 9 $/\$ $\/$
121	120	pm4.71rd 639	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$
122		ancom 451	. . . . . . . 8 $\/$ $/\$ $/\$ $/\$ $/\$ $\/$
123	121, 122	syl6rbb 265	. . . . . . 7 $/\$ $/\$ $\/$ $/\$
124	123	opabbidv 4489	. . . . . 6 $/\$ $/\$ $\/$ $/\$
125		unopab 4501	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
126	35	uneq2i 3623	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
127		andi 875	. . . . . . . 8 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $/\$
128	127	opabbii 4490	. . . . . . 7 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $/\$
129	125, 126, 128	3eqtr4i 2468	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $\/$
130		df-xp 4860	. . . . . 6 $/\$
131	124, 129, 130	3eqtr4g 2495	. . . . 5 $/\$ $/\$
132	131	fveq2d 5885	. . . 4 $/\$ $/\$
133		inopab 4985	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
134	35	ineq2i 3667	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
135		anandi 835	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
136	135	opabbii 4490	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
137	133, 134, 136	3eqtr4i 2468	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
138		ltnsym2 9732	. . . . . . . . . . . 12 $/\$ $/\$
139	115, 117, 138	syl2anc 665	. . . . . . . . . . 11 $/\$ $/\$ $/\$
140	139	ex 435	. . . . . . . . . 10 $/\$ $/\$
141		imnan 423	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
142	140, 141	sylib 199	. . . . . . . . 9 $/\$ $/\$ $/\$
143	142	nexdv 1774	. . . . . . . 8 $/\$ $/\$ $/\$
144	143	nexdv 1774	. . . . . . 7 $/\$ $/\$ $/\$
145		opabn0 4752	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
146	145	necon1bbii 2695	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
147	144, 146	sylib 199	. . . . . 6 $/\$ $/\$ $/\$
148	137, 147	syl5eq 2482	. . . . 5 $/\$ $/\$
149		hashun 12558	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
150	26, 43, 148, 149	syl3anc 1264	. . . 4 $/\$ $/\$ $/\$ $/\$
151		hashxp 12601	. . . . . 6 $/\$
152	20, 21, 151	syl2anc 665	. . . . 5
153		oddprm 14728	. . . . . . . . . 10 $\$
154	2, 153	syl 17	. . . . . . . . 9
155	6, 154	syl5eqel 2521	. . . . . . . 8
156	155	nnnn0d 10925	. . . . . . 7
157		hashfz1 12526	. . . . . . 7
158	156, 157	syl 17	. . . . . 6
159	55	nnnn0d 10925	. . . . . . 7
160		hashfz1 12526	. . . . . . 7
161	159, 160	syl 17	. . . . . 6
162	158, 161	oveq12d 6323	. . . . 5
163	152, 162	eqtrd 2470	. . . 4
164	132, 150, 163	3eqtr3d 2478	. . 3 $/\$ $/\$
165	164	oveq2d 6321	. 2 $/\$ $/\$
166	37, 48, 165	3eqtr2d 2476	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 187 $\/$ wo 369 $/\$ wa 370

wceq 1437

wex 1659

wcel 1870

wne 2625 $\$ cdif 3439

cun 3440

cin 3441

wss 3442

c0 3767

csn 4002 class class class wbr 4426

copab 4483

cxp 4852

ccnv 4853

wrel 4859

cfv 5601 (class class class)co 6305

cen 7574

cfn 7577

cc 9536

cr 9537

c1 9539

caddc 9541

cmul 9543

clt 9674

cle 9675

cmin 9859

cneg 9860

cdiv 10268

cn 10609

c2 10659

cn0 10869

cz 10937

cuz 11159

crp 11302

cfz 11782

cexp 12269

chash 12512

cdvds 14283

cgcd 14442

cprime 14593

clgs 24085

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1665 ax-4 1678 ax-5 1751 ax-6 1797 ax-7 1841 ax-8 1872 ax-9 1874 ax-10 1889 ax-11 1894 ax-12 1907 ax-13 2055 ax-ext 2407 ax-rep 4538 ax-sep 4548 ax-nul 4556 ax-pow 4603 ax-pr 4661 ax-un 6597 ax-inf2 8146 ax-cnex 9594 ax-resscn 9595 ax-1cn 9596 ax-icn 9597 ax-addcl 9598 ax-addrcl 9599 ax-mulcl 9600 ax-mulrcl 9601 ax-mulcom 9602 ax-addass 9603 ax-mulass 9604 ax-distr 9605 ax-i2m1 9606 ax-1ne0 9607 ax-1rid 9608 ax-rnegex 9609 ax-rrecex 9610 ax-cnre 9611 ax-pre-lttri 9612 ax-pre-lttrn 9613 ax-pre-ltadd 9614 ax-pre-mulgt0 9615 ax-pre-sup 9616 ax-addf 9617 ax-mulf 9618

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3or 983 df-3an 984 df-tru 1440 df-fal 1443 df-ex 1660 df-nf 1664 df-sb 1790 df-eu 2270 df-mo 2271 df-clab 2415 df-cleq 2421 df-clel 2424 df-nfc 2579 df-ne 2627 df-nel 2628 df-ral 2787 df-rex 2788 df-reu 2789 df-rmo 2790 df-rab 2791 df-v 3089 df-sbc 3306 df-csb 3402 df-dif 3445 df-un 3447 df-in 3449 df-ss 3456 df-pss 3458 df-nul 3768 df-if 3916 df-pw 3987 df-sn 4003 df-pr 4005 df-tp 4007 df-op 4009 df-uni 4223 df-int 4259 df-iun 4304 df-disj 4398 df-br 4427 df-opab 4485 df-mpt 4486 df-tr 4521 df-eprel 4765 df-id 4769 df-po 4775 df-so 4776 df-fr 4813 df-se 4814 df-we 4815 df-xp 4860 df-rel 4861 df-cnv 4862 df-co 4863 df-dm 4864 df-rn 4865 df-res 4866 df-ima 4867 df-pred 5399 df-ord 5445 df-on 5446 df-lim 5447 df-suc 5448 df-iota 5565 df-fun 5603 df-fn 5604 df-f 5605 df-f1 5606 df-fo 5607 df-f1o 5608 df-fv 5609 df-isom 5610 df-riota 6267 df-ov 6308 df-oprab 6309 df-mpt2 6310 df-of 6545 df-om 6707 df-1st 6807 df-2nd 6808 df-supp 6926 df-tpos 6981 df-wrecs 7036 df-recs 7098 df-rdg 7136 df-1o 7190 df-2o 7191 df-oadd 7194 df-er 7371 df-ec 7373 df-qs 7377 df-map 7482 df-en 7578 df-dom 7579 df-sdom 7580 df-fin 7581 df-fsupp 7890 df-sup 7962 df-inf 7963 df-oi 8025 df-card 8372 df-cda 8596 df-pnf 9676 df-mnf 9677 df-xr 9678 df-ltxr 9679 df-le 9680 df-sub 9861 df-neg 9862 df-div 10269 df-nn 10610 df-2 10668 df-3 10669 df-4 10670 df-5 10671 df-6 10672 df-7 10673 df-8 10674 df-9 10675 df-10 10676 df-n0 10870 df-z 10938 df-dec 11052 df-uz 11160 df-q 11265 df-rp 11303 df-fz 11783 df-fzo 11914 df-fl 12025 df-mod 12094 df-seq 12211 df-exp 12270 df-hash 12513 df-cj 13141 df-re 13142 df-im 13143 df-sqrt 13277 df-abs 13278 df-clim 13530 df-sum 13731 df-dvds 14284 df-gcd 14443 df-prm 14594 df-phi 14683 df-pc 14750 df-struct 15086 df-ndx 15087 df-slot 15088 df-base 15089 df-sets 15090 df-ress 15091 df-plusg 15165 df-mulr 15166 df-starv 15167 df-sca 15168 df-vsca 15169 df-ip 15170 df-tset 15171 df-ple 15172 df-ds 15174 df-unif 15175 df-0g 15299 df-gsum 15300 df-imas 15365 df-qus 15366 df-mgm 16439 df-sgrp 16478 df-mnd 16488 df-mhm 16533 df-submnd 16534 df-grp 16624 df-minusg 16625 df-sbg 16626 df-mulg 16627 df-subg 16765 df-nsg 16766 df-eqg 16767 df-ghm 16832 df-cntz 16922 df-cmn 17367 df-abl 17368 df-mgp 17659 df-ur 17671 df-ring 17717 df-cring 17718 df-oppr 17786 df-dvdsr 17804 df-unit 17805 df-invr 17835 df-dvr 17846 df-rnghom 17878 df-drng 17912 df-field 17913 df-subrg 17941 df-lmod 18028 df-lss 18091 df-lsp 18130 df-sra 18330 df-rgmod 18331 df-lidl 18332 df-rsp 18333 df-2idl 18391 df-nzr 18417 df-rlreg 18442 df-domn 18443 df-idom 18444 df-cnfld 18906 df-zring 18974 df-zrh 19006 df-zn 19009 df-lgs 24086

This theorem is referenced by: lgsquad 24148

W3C validator