lgsquadlem3 - Metamath Proof Explorer

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

Theorem lgsquadlem3 24283

Description: Lemma for lgsquad 24284. (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 2691	. . . . 5
5		lgsquad.5	. . . . 5
6		lgsquad.4	. . . . 5
7		eleq1 2495	. . . . . . . . . 10
8		eleq1 2495	. . . . . . . . . 10
9	7, 8	bi2anan9 881	. . . . . . . . 9 $/\$ $/\$ $/\$
10		ancom 451	. . . . . . . . 9 $/\$ $/\$
11	9, 10	syl6bb 264	. . . . . . . 8 $/\$ $/\$ $/\$
12		oveq1 6313	. . . . . . . . 9
13		oveq1 6313	. . . . . . . . 9
14	12, 13	breqan12d 4439	. . . . . . . 8 $/\$
15	11, 14	anbi12d 715	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
16	15	ancoms 454	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
17	16	cbvopabv 4493	. . . . 5 $/\$ $/\$ $/\$ $/\$
18	1, 2, 4, 5, 6, 17	lgsquadlem2 24282	. . . 4 $/\$ $/\$
19		relopab 4979	. . . . . . . 8 $/\$ $/\$
20		fzfid 12193	. . . . . . . . . 10
21		fzfid 12193	. . . . . . . . . 10
22		xpfi 7852	. . . . . . . . . 10 $/\$
23	20, 21, 22	syl2anc 665	. . . . . . . . 9
24		opabssxp 4928	. . . . . . . . 9 $/\$ $/\$
25		ssfi 7802	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
26	23, 24, 25	sylancl 666	. . . . . . . 8 $/\$ $/\$
27		cnven 7656	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
28	19, 26, 27	sylancr 667	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
29		cnvopab 5256	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
30	28, 29	syl6breq 4463	. . . . . 6 $/\$ $/\$ $/\$ $/\$
31		hasheni 12538	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
32	30, 31	syl 17	. . . . 5 $/\$ $/\$ $/\$ $/\$
33	32	oveq2d 6322	. . . 4 $/\$ $/\$ $/\$ $/\$
34	18, 33	eqtr4d 2466	. . 3 $/\$ $/\$
35		lgsquad.6	. . . 4 $/\$ $/\$
36	2, 1, 3, 6, 5, 35	lgsquadlem2 24282	. . 3
37	34, 36	oveq12d 6324	. 2 $/\$ $/\$
38		neg1cn 10721	. . . 4
39	38	a1i 11	. . 3
40		opabssxp 4928	. . . . . 6 $/\$ $/\$
41	35, 40	eqsstri 3494	. . . . 5
42		ssfi 7802	. . . . 5 $/\$
43	23, 41, 42	sylancl 666	. . . 4
44		hashcl 12545	. . . 4
45	43, 44	syl 17	. . 3
46		hashcl 12545	. . . 4 $/\$ $/\$ $/\$ $/\$
47	26, 46	syl 17	. . 3 $/\$ $/\$
48	39, 45, 47	expaddd 12425	. 2 $/\$ $/\$ $/\$ $/\$
49	1	eldifad 3448	. . . . . . . . . . . . . . . . 17
50	49	adantr 466	. . . . . . . . . . . . . . . 16 $/\$ $/\$
51		prmnn 14625	. . . . . . . . . . . . . . . 16
52	50, 51	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$
53		oddprm 14765	. . . . . . . . . . . . . . . . . . . . . 22 $\$
54	1, 53	syl 17	. . . . . . . . . . . . . . . . . . . . 21
55	5, 54	syl5eqel 2511	. . . . . . . . . . . . . . . . . . . 20
56	55	adantr 466	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
57	56	nnzd 11047	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
58		prmz 14626	. . . . . . . . . . . . . . . . . . . 20
59	50, 58	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
60		peano2zm 10988	. . . . . . . . . . . . . . . . . . 19
61	59, 60	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
62	56	nnred 10632	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
63	61	zred 11048	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
64		prmuz2 14642	. . . . . . . . . . . . . . . . . . . . . . . 24
65	50, 64	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
66		uz2m1nn 11241	. . . . . . . . . . . . . . . . . . . . . . 23
67	65, 66	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
68	67	nnrpd 11347	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
69		rphalflt 11337	. . . . . . . . . . . . . . . . . . . . 21
70	68, 69	syl 17	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
71	5, 70	syl5eqbr 4457	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
72	62, 63, 71	ltled 9791	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
73		eluz2 11173	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
74	57, 61, 72, 73	syl3anbrc 1189	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
75		fzss2 11846	. . . . . . . . . . . . . . . . 17
76	74, 75	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$
77		simprr 764	. . . . . . . . . . . . . . . 16 $/\$ $/\$
78	76, 77	sseldd 3465	. . . . . . . . . . . . . . 15 $/\$ $/\$
79		fzm1ndvds 14357	. . . . . . . . . . . . . . 15 $/\$
80	52, 78, 79	syl2anc 665	. . . . . . . . . . . . . 14 $/\$ $/\$
81	4	adantr 466	. . . . . . . . . . . . . . . 16 $/\$ $/\$
82	2	eldifad 3448	. . . . . . . . . . . . . . . . . 18
83	82	adantr 466	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
84		prmrp 14658	. . . . . . . . . . . . . . . . 17 $/\$
85	50, 83, 84	syl2anc 665	. . . . . . . . . . . . . . . 16 $/\$ $/\$
86	81, 85	mpbird 235	. . . . . . . . . . . . . . 15 $/\$ $/\$
87		prmz 14626	. . . . . . . . . . . . . . . . 17
88	83, 87	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$
89		elfzelz 11808	. . . . . . . . . . . . . . . . 17
90	89	ad2antll 733	. . . . . . . . . . . . . . . 16 $/\$ $/\$
91		coprmdvds 14659	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
92	59, 88, 90, 91	syl3anc 1264	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
93	86, 92	mpan2d 678	. . . . . . . . . . . . . 14 $/\$ $/\$
94	80, 93	mtod 180	. . . . . . . . . . . . 13 $/\$ $/\$
95		prmnn 14625	. . . . . . . . . . . . . . . . 17
96	83, 95	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$
97	96	nncnd 10633	. . . . . . . . . . . . . . 15 $/\$ $/\$
98		elfznn 11836	. . . . . . . . . . . . . . . . 17
99	98	ad2antll 733	. . . . . . . . . . . . . . . 16 $/\$ $/\$
100	99	nncnd 10633	. . . . . . . . . . . . . . 15 $/\$ $/\$
101	97, 100	mulcomd 9672	. . . . . . . . . . . . . 14 $/\$ $/\$
102	101	breq2d 4435	. . . . . . . . . . . . 13 $/\$ $/\$
103	94, 102	mtbid 301	. . . . . . . . . . . 12 $/\$ $/\$
104		elfzelz 11808	. . . . . . . . . . . . . . . 16
105	104	ad2antrl 732	. . . . . . . . . . . . . . 15 $/\$ $/\$
106		dvdsmul2 14325	. . . . . . . . . . . . . . 15 $/\$
107	105, 59, 106	syl2anc 665	. . . . . . . . . . . . . 14 $/\$ $/\$
108		breq2 4427	. . . . . . . . . . . . . 14
109	107, 108	syl5ibcom 223	. . . . . . . . . . . . 13 $/\$ $/\$
110	109	necon3bd 2632	. . . . . . . . . . . 12 $/\$ $/\$
111	103, 110	mpd 15	. . . . . . . . . . 11 $/\$ $/\$
112		elfznn 11836	. . . . . . . . . . . . . . 15
113	112	ad2antrl 732	. . . . . . . . . . . . . 14 $/\$ $/\$
114	113, 52	nnmulcld 10665	. . . . . . . . . . . . 13 $/\$ $/\$
115	114	nnred 10632	. . . . . . . . . . . 12 $/\$ $/\$
116	99, 96	nnmulcld 10665	. . . . . . . . . . . . 13 $/\$ $/\$
117	116	nnred 10632	. . . . . . . . . . . 12 $/\$ $/\$
118	115, 117	lttri2d 9782	. . . . . . . . . . 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 4487	. . . . . 6 $/\$ $/\$ $\/$ $/\$
125		unopab 4499	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
126	35	uneq2i 3617	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
127		andi 875	. . . . . . . 8 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $/\$
128	127	opabbii 4488	. . . . . . 7 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $/\$
129	125, 126, 128	3eqtr4i 2461	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $\/$
130		df-xp 4859	. . . . . 6 $/\$
131	124, 129, 130	3eqtr4g 2488	. . . . 5 $/\$ $/\$
132	131	fveq2d 5886	. . . 4 $/\$ $/\$
133		inopab 4984	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
134	35	ineq2i 3661	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
135		anandi 835	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
136	135	opabbii 4488	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
137	133, 134, 136	3eqtr4i 2461	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
138		ltnsym2 9741	. . . . . . . . . . . 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 1775	. . . . . . . 8 $/\$ $/\$ $/\$
144	143	nexdv 1775	. . . . . . 7 $/\$ $/\$ $/\$
145		opabn0 4751	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
146	145	necon1bbii 2684	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
147	144, 146	sylib 199	. . . . . 6 $/\$ $/\$ $/\$
148	137, 147	syl5eq 2475	. . . . 5 $/\$ $/\$
149		hashun 12568	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
150	26, 43, 148, 149	syl3anc 1264	. . . 4 $/\$ $/\$ $/\$ $/\$
151		hashxp 12611	. . . . . 6 $/\$
152	20, 21, 151	syl2anc 665	. . . . 5
153		oddprm 14765	. . . . . . . . . 10 $\$
154	2, 153	syl 17	. . . . . . . . 9
155	6, 154	syl5eqel 2511	. . . . . . . 8
156	155	nnnn0d 10933	. . . . . . 7
157		hashfz1 12536	. . . . . . 7
158	156, 157	syl 17	. . . . . 6
159	55	nnnn0d 10933	. . . . . . 7
160		hashfz1 12536	. . . . . . 7
161	159, 160	syl 17	. . . . . 6
162	158, 161	oveq12d 6324	. . . . 5
163	152, 162	eqtrd 2463	. . . 4
164	132, 150, 163	3eqtr3d 2471	. . 3 $/\$ $/\$
165	164	oveq2d 6322	. 2 $/\$ $/\$
166	37, 48, 165	3eqtr2d 2469	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1437

wex 1657

wcel 1872

wne 2614 $\$ cdif 3433

cun 3434

cin 3435

wss 3436

c0 3761

csn 3998 class class class wbr 4423

copab 4481

cxp 4851

ccnv 4852

wrel 4858

cfv 5601 (class class class)co 6306

cen 7578

cfn 7581

cc 9545

cr 9546

c1 9548

caddc 9550

cmul 9552

clt 9683

cle 9684

cmin 9868

cneg 9869

cdiv 10277

cn 10617

c2 10667

cn0 10877

cz 10945

cuz 11167

crp 11310

cfz 11792

cexp 12279

chash 12522

cdvds 14305

cgcd 14468

cprime 14622

clgs 24221

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1663 ax-4 1676 ax-5 1752 ax-6 1798 ax-7 1843 ax-8 1874 ax-9 1876 ax-10 1891 ax-11 1896 ax-12 1909 ax-13 2057 ax-ext 2401 ax-rep 4536 ax-sep 4546 ax-nul 4555 ax-pow 4602 ax-pr 4660 ax-un 6598 ax-inf2 8156 ax-cnex 9603 ax-resscn 9604 ax-1cn 9605 ax-icn 9606 ax-addcl 9607 ax-addrcl 9608 ax-mulcl 9609 ax-mulrcl 9610 ax-mulcom 9611 ax-addass 9612 ax-mulass 9613 ax-distr 9614 ax-i2m1 9615 ax-1ne0 9616 ax-1rid 9617 ax-rnegex 9618 ax-rrecex 9619 ax-cnre 9620 ax-pre-lttri 9621 ax-pre-lttrn 9622 ax-pre-ltadd 9623 ax-pre-mulgt0 9624 ax-pre-sup 9625 ax-addf 9626 ax-mulf 9627

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 1658 df-nf 1662 df-sb 1791 df-eu 2273 df-mo 2274 df-clab 2408 df-cleq 2414 df-clel 2417 df-nfc 2568 df-ne 2616 df-nel 2617 df-ral 2776 df-rex 2777 df-reu 2778 df-rmo 2779 df-rab 2780 df-v 3082 df-sbc 3300 df-csb 3396 df-dif 3439 df-un 3441 df-in 3443 df-ss 3450 df-pss 3452 df-nul 3762 df-if 3912 df-pw 3983 df-sn 3999 df-pr 4001 df-tp 4003 df-op 4005 df-uni 4220 df-int 4256 df-iun 4301 df-disj 4395 df-br 4424 df-opab 4483 df-mpt 4484 df-tr 4519 df-eprel 4764 df-id 4768 df-po 4774 df-so 4775 df-fr 4812 df-se 4813 df-we 4814 df-xp 4859 df-rel 4860 df-cnv 4861 df-co 4862 df-dm 4863 df-rn 4864 df-res 4865 df-ima 4866 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 6268 df-ov 6309 df-oprab 6310 df-mpt2 6311 df-of 6546 df-om 6708 df-1st 6808 df-2nd 6809 df-supp 6927 df-tpos 6985 df-wrecs 7040 df-recs 7102 df-rdg 7140 df-1o 7194 df-2o 7195 df-oadd 7198 df-er 7375 df-ec 7377 df-qs 7381 df-map 7486 df-en 7582 df-dom 7583 df-sdom 7584 df-fin 7585 df-fsupp 7894 df-sup 7966 df-inf 7967 df-oi 8035 df-card 8382 df-cda 8606 df-pnf 9685 df-mnf 9686 df-xr 9687 df-ltxr 9688 df-le 9689 df-sub 9870 df-neg 9871 df-div 10278 df-nn 10618 df-2 10676 df-3 10677 df-4 10678 df-5 10679 df-6 10680 df-7 10681 df-8 10682 df-9 10683 df-10 10684 df-n0 10878 df-z 10946 df-dec 11060 df-uz 11168 df-q 11273 df-rp 11311 df-fz 11793 df-fzo 11924 df-fl 12035 df-mod 12104 df-seq 12221 df-exp 12280 df-hash 12523 df-cj 13163 df-re 13164 df-im 13165 df-sqrt 13299 df-abs 13300 df-clim 13552 df-sum 13753 df-dvds 14306 df-gcd 14469 df-prm 14623 df-phi 14714 df-pc 14787 df-struct 15123 df-ndx 15124 df-slot 15125 df-base 15126 df-sets 15127 df-ress 15128 df-plusg 15203 df-mulr 15204 df-starv 15205 df-sca 15206 df-vsca 15207 df-ip 15208 df-tset 15209 df-ple 15210 df-ds 15212 df-unif 15213 df-0g 15340 df-gsum 15341 df-imas 15407 df-qus 15409 df-mgm 16488 df-sgrp 16527 df-mnd 16537 df-mhm 16582 df-submnd 16583 df-grp 16673 df-minusg 16674 df-sbg 16675 df-mulg 16676 df-subg 16814 df-nsg 16815 df-eqg 16816 df-ghm 16881 df-cntz 16971 df-cmn 17432 df-abl 17433 df-mgp 17724 df-ur 17736 df-ring 17782 df-cring 17783 df-oppr 17851 df-dvdsr 17869 df-unit 17870 df-invr 17900 df-dvr 17911 df-rnghom 17943 df-drng 17977 df-field 17978 df-subrg 18006 df-lmod 18093 df-lss 18156 df-lsp 18195 df-sra 18395 df-rgmod 18396 df-lidl 18397 df-rsp 18398 df-2idl 18456 df-nzr 18482 df-rlreg 18507 df-domn 18508 df-idom 18509 df-cnfld 18971 df-zring 19039 df-zrh 19074 df-zn 19077 df-lgs 24222

This theorem is referenced by: lgsquad 24284

W3C validator