lgsquadlem3 - Metamath Proof Explorer

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

Theorem lgsquadlem3 24340

Description: Lemma for lgsquad 24341. (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 2528	. . . . . . . . . 10
8		eleq1 2528	. . . . . . . . . 10
9	7, 8	bi2anan9 889	. . . . . . . . 9 $/\$ $/\$ $/\$
10		ancom 456	. . . . . . . . 9 $/\$ $/\$
11	9, 10	syl6bb 269	. . . . . . . 8 $/\$ $/\$ $/\$
12		oveq1 6327	. . . . . . . . 9
13		oveq1 6327	. . . . . . . . 9
14	12, 13	breqan12d 4434	. . . . . . . 8 $/\$
15	11, 14	anbi12d 722	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
16	15	ancoms 459	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
17	16	cbvopabv 4488	. . . . 5 $/\$ $/\$ $/\$ $/\$
18	1, 2, 4, 5, 6, 17	lgsquadlem2 24339	. . . 4 $/\$ $/\$
19		relopab 4982	. . . . . . . 8 $/\$ $/\$
20		fzfid 12224	. . . . . . . . . 10
21		fzfid 12224	. . . . . . . . . 10
22		xpfi 7873	. . . . . . . . . 10 $/\$
23	20, 21, 22	syl2anc 671	. . . . . . . . 9
24		opabssxp 4931	. . . . . . . . 9 $/\$ $/\$
25		ssfi 7823	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
26	23, 24, 25	sylancl 673	. . . . . . . 8 $/\$ $/\$
27		cnven 7676	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
28	19, 26, 27	sylancr 674	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
29		cnvopab 5259	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
30	28, 29	syl6breq 4458	. . . . . 6 $/\$ $/\$ $/\$ $/\$
31		hasheni 12569	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
32	30, 31	syl 17	. . . . 5 $/\$ $/\$ $/\$ $/\$
33	32	oveq2d 6336	. . . 4 $/\$ $/\$ $/\$ $/\$
34	18, 33	eqtr4d 2499	. . 3 $/\$ $/\$
35		lgsquad.6	. . . 4 $/\$ $/\$
36	2, 1, 3, 6, 5, 35	lgsquadlem2 24339	. . 3
37	34, 36	oveq12d 6338	. 2 $/\$ $/\$
38		neg1cn 10746	. . . 4
39	38	a1i 11	. . 3
40		opabssxp 4931	. . . . . 6 $/\$ $/\$
41	35, 40	eqsstri 3474	. . . . 5
42		ssfi 7823	. . . . 5 $/\$
43	23, 41, 42	sylancl 673	. . . 4
44		hashcl 12576	. . . 4
45	43, 44	syl 17	. . 3
46		hashcl 12576	. . . 4 $/\$ $/\$ $/\$ $/\$
47	26, 46	syl 17	. . 3 $/\$ $/\$
48	39, 45, 47	expaddd 12456	. 2 $/\$ $/\$ $/\$ $/\$
49	1	eldifad 3428	. . . . . . . . . . . . . . . . 17
50	49	adantr 471	. . . . . . . . . . . . . . . 16 $/\$ $/\$
51		prmnn 14680	. . . . . . . . . . . . . . . 16
52	50, 51	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$
53		oddprm 14820	. . . . . . . . . . . . . . . . . . . . . 22 $\$
54	1, 53	syl 17	. . . . . . . . . . . . . . . . . . . . 21
55	5, 54	syl5eqel 2544	. . . . . . . . . . . . . . . . . . . 20
56	55	adantr 471	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
57	56	nnzd 11073	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
58		prmz 14681	. . . . . . . . . . . . . . . . . . . 20
59	50, 58	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
60		peano2zm 11014	. . . . . . . . . . . . . . . . . . 19
61	59, 60	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
62	56	nnred 10657	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
63	61	zred 11074	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
64		prmuz2 14697	. . . . . . . . . . . . . . . . . . . . . . . 24
65	50, 64	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
66		uz2m1nn 11267	. . . . . . . . . . . . . . . . . . . . . . 23
67	65, 66	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
68	67	nnrpd 11373	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
69		rphalflt 11363	. . . . . . . . . . . . . . . . . . . . 21
70	68, 69	syl 17	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
71	5, 70	syl5eqbr 4452	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
72	62, 63, 71	ltled 9814	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
73		eluz2 11199	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
74	57, 61, 72, 73	syl3anbrc 1198	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
75		fzss2 11873	. . . . . . . . . . . . . . . . 17
76	74, 75	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$
77		simprr 771	. . . . . . . . . . . . . . . 16 $/\$ $/\$
78	76, 77	sseldd 3445	. . . . . . . . . . . . . . 15 $/\$ $/\$
79		fzm1ndvds 14412	. . . . . . . . . . . . . . 15 $/\$
80	52, 78, 79	syl2anc 671	. . . . . . . . . . . . . 14 $/\$ $/\$
81	4	adantr 471	. . . . . . . . . . . . . . . 16 $/\$ $/\$
82	2	eldifad 3428	. . . . . . . . . . . . . . . . . 18
83	82	adantr 471	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
84		prmrp 14713	. . . . . . . . . . . . . . . . 17 $/\$
85	50, 83, 84	syl2anc 671	. . . . . . . . . . . . . . . 16 $/\$ $/\$
86	81, 85	mpbird 240	. . . . . . . . . . . . . . 15 $/\$ $/\$
87		prmz 14681	. . . . . . . . . . . . . . . . 17
88	83, 87	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$
89		elfzelz 11835	. . . . . . . . . . . . . . . . 17
90	89	ad2antll 740	. . . . . . . . . . . . . . . 16 $/\$ $/\$
91		coprmdvds 14714	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
92	59, 88, 90, 91	syl3anc 1276	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
93	86, 92	mpan2d 685	. . . . . . . . . . . . . 14 $/\$ $/\$
94	80, 93	mtod 182	. . . . . . . . . . . . 13 $/\$ $/\$
95		prmnn 14680	. . . . . . . . . . . . . . . . 17
96	83, 95	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$
97	96	nncnd 10658	. . . . . . . . . . . . . . 15 $/\$ $/\$
98		elfznn 11863	. . . . . . . . . . . . . . . . 17
99	98	ad2antll 740	. . . . . . . . . . . . . . . 16 $/\$ $/\$
100	99	nncnd 10658	. . . . . . . . . . . . . . 15 $/\$ $/\$
101	97, 100	mulcomd 9695	. . . . . . . . . . . . . 14 $/\$ $/\$
102	101	breq2d 4430	. . . . . . . . . . . . 13 $/\$ $/\$
103	94, 102	mtbid 306	. . . . . . . . . . . 12 $/\$ $/\$
104		elfzelz 11835	. . . . . . . . . . . . . . . 16
105	104	ad2antrl 739	. . . . . . . . . . . . . . 15 $/\$ $/\$
106		dvdsmul2 14380	. . . . . . . . . . . . . . 15 $/\$
107	105, 59, 106	syl2anc 671	. . . . . . . . . . . . . 14 $/\$ $/\$
108		breq2 4422	. . . . . . . . . . . . . 14
109	107, 108	syl5ibcom 228	. . . . . . . . . . . . 13 $/\$ $/\$
110	109	necon3bd 2650	. . . . . . . . . . . 12 $/\$ $/\$
111	103, 110	mpd 15	. . . . . . . . . . 11 $/\$ $/\$
112		elfznn 11863	. . . . . . . . . . . . . . 15
113	112	ad2antrl 739	. . . . . . . . . . . . . 14 $/\$ $/\$
114	113, 52	nnmulcld 10690	. . . . . . . . . . . . 13 $/\$ $/\$
115	114	nnred 10657	. . . . . . . . . . . 12 $/\$ $/\$
116	99, 96	nnmulcld 10690	. . . . . . . . . . . . 13 $/\$ $/\$
117	116	nnred 10657	. . . . . . . . . . . 12 $/\$ $/\$
118	115, 117	lttri2d 9805	. . . . . . . . . . 11 $/\$ $/\$ $\/$
119	111, 118	mpbid 215	. . . . . . . . . 10 $/\$ $/\$ $\/$
120	119	ex 440	. . . . . . . . 9 $/\$ $\/$
121	120	pm4.71rd 645	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$
122		ancom 456	. . . . . . . 8 $\/$ $/\$ $/\$ $/\$ $/\$ $\/$
123	121, 122	syl6rbb 270	. . . . . . 7 $/\$ $/\$ $\/$ $/\$
124	123	opabbidv 4482	. . . . . 6 $/\$ $/\$ $\/$ $/\$
125		unopab 4494	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
126	35	uneq2i 3597	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
127		andi 883	. . . . . . . 8 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $/\$
128	127	opabbii 4483	. . . . . . 7 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $/\$
129	125, 126, 128	3eqtr4i 2494	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $\/$
130		df-xp 4862	. . . . . 6 $/\$
131	124, 129, 130	3eqtr4g 2521	. . . . 5 $/\$ $/\$
132	131	fveq2d 5896	. . . 4 $/\$ $/\$
133		inopab 4987	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
134	35	ineq2i 3643	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
135		anandi 842	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
136	135	opabbii 4483	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
137	133, 134, 136	3eqtr4i 2494	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
138		ltnsym2 9764	. . . . . . . . . . . 12 $/\$ $/\$
139	115, 117, 138	syl2anc 671	. . . . . . . . . . 11 $/\$ $/\$ $/\$
140	139	ex 440	. . . . . . . . . 10 $/\$ $/\$
141		imnan 428	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
142	140, 141	sylib 201	. . . . . . . . 9 $/\$ $/\$ $/\$
143	142	nexdv 1793	. . . . . . . 8 $/\$ $/\$ $/\$
144	143	nexdv 1793	. . . . . . 7 $/\$ $/\$ $/\$
145		opabn0 4749	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
146	145	necon1bbii 2685	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
147	144, 146	sylib 201	. . . . . 6 $/\$ $/\$ $/\$
148	137, 147	syl5eq 2508	. . . . 5 $/\$ $/\$
149		hashun 12599	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
150	26, 43, 148, 149	syl3anc 1276	. . . 4 $/\$ $/\$ $/\$ $/\$
151		hashxp 12645	. . . . . 6 $/\$
152	20, 21, 151	syl2anc 671	. . . . 5
153		oddprm 14820	. . . . . . . . . 10 $\$
154	2, 153	syl 17	. . . . . . . . 9
155	6, 154	syl5eqel 2544	. . . . . . . 8
156	155	nnnn0d 10959	. . . . . . 7
157		hashfz1 12567	. . . . . . 7
158	156, 157	syl 17	. . . . . 6
159	55	nnnn0d 10959	. . . . . . 7
160		hashfz1 12567	. . . . . . 7
161	159, 160	syl 17	. . . . . 6
162	158, 161	oveq12d 6338	. . . . 5
163	152, 162	eqtrd 2496	. . . 4
164	132, 150, 163	3eqtr3d 2504	. . 3 $/\$ $/\$
165	164	oveq2d 6336	. 2 $/\$ $/\$
166	37, 48, 165	3eqtr2d 2502	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 189 $\/$ wo 374 $/\$ wa 375

wceq 1455

wex 1674

wcel 1898

wne 2633 $\$ cdif 3413

cun 3414

cin 3415

wss 3416

c0 3743

csn 3980 class class class wbr 4418

copab 4476

cxp 4854

ccnv 4855

wrel 4861

cfv 5605 (class class class)co 6320

cen 7597

cfn 7600

cc 9568

cr 9569

c1 9571

caddc 9573

cmul 9575

clt 9706

cle 9707

cmin 9891

cneg 9892

cdiv 10302

cn 10642

c2 10692

cn0 10903

cz 10971

cuz 11193

crp 11336

cfz 11819

cexp 12310

chash 12553

cdvds 14360

cgcd 14523

cprime 14677

clgs 24278

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-8 1900 ax-9 1907 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 ax-rep 4531 ax-sep 4541 ax-nul 4550 ax-pow 4598 ax-pr 4656 ax-un 6615 ax-inf2 8177 ax-cnex 9626 ax-resscn 9627 ax-1cn 9628 ax-icn 9629 ax-addcl 9630 ax-addrcl 9631 ax-mulcl 9632 ax-mulrcl 9633 ax-mulcom 9634 ax-addass 9635 ax-mulass 9636 ax-distr 9637 ax-i2m1 9638 ax-1ne0 9639 ax-1rid 9640 ax-rnegex 9641 ax-rrecex 9642 ax-cnre 9643 ax-pre-lttri 9644 ax-pre-lttrn 9645 ax-pre-ltadd 9646 ax-pre-mulgt0 9647 ax-pre-sup 9648 ax-addf 9649 ax-mulf 9650

This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3or 992 df-3an 993 df-tru 1458 df-fal 1461 df-ex 1675 df-nf 1679 df-sb 1809 df-eu 2314 df-mo 2315 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-ne 2635 df-nel 2636 df-ral 2754 df-rex 2755 df-reu 2756 df-rmo 2757 df-rab 2758 df-v 3059 df-sbc 3280 df-csb 3376 df-dif 3419 df-un 3421 df-in 3423 df-ss 3430 df-pss 3432 df-nul 3744 df-if 3894 df-pw 3965 df-sn 3981 df-pr 3983 df-tp 3985 df-op 3987 df-uni 4213 df-int 4249 df-iun 4294 df-disj 4390 df-br 4419 df-opab 4478 df-mpt 4479 df-tr 4514 df-eprel 4767 df-id 4771 df-po 4777 df-so 4778 df-fr 4815 df-se 4816 df-we 4817 df-xp 4862 df-rel 4863 df-cnv 4864 df-co 4865 df-dm 4866 df-rn 4867 df-res 4868 df-ima 4869 df-pred 5403 df-ord 5449 df-on 5450 df-lim 5451 df-suc 5452 df-iota 5569 df-fun 5607 df-fn 5608 df-f 5609 df-f1 5610 df-fo 5611 df-f1o 5612 df-fv 5613 df-isom 5614 df-riota 6282 df-ov 6323 df-oprab 6324 df-mpt2 6325 df-of 6563 df-om 6725 df-1st 6825 df-2nd 6826 df-supp 6947 df-tpos 7004 df-wrecs 7059 df-recs 7121 df-rdg 7159 df-1o 7213 df-2o 7214 df-oadd 7217 df-er 7394 df-ec 7396 df-qs 7400 df-map 7505 df-en 7601 df-dom 7602 df-sdom 7603 df-fin 7604 df-fsupp 7915 df-sup 7987 df-inf 7988 df-oi 8056 df-card 8404 df-cda 8629 df-pnf 9708 df-mnf 9709 df-xr 9710 df-ltxr 9711 df-le 9712 df-sub 9893 df-neg 9894 df-div 10303 df-nn 10643 df-2 10701 df-3 10702 df-4 10703 df-5 10704 df-6 10705 df-7 10706 df-8 10707 df-9 10708 df-10 10709 df-n0 10904 df-z 10972 df-dec 11086 df-uz 11194 df-q 11299 df-rp 11337 df-fz 11820 df-fzo 11953 df-fl 12066 df-mod 12135 df-seq 12252 df-exp 12311 df-hash 12554 df-cj 13217 df-re 13218 df-im 13219 df-sqrt 13353 df-abs 13354 df-clim 13607 df-sum 13808 df-dvds 14361 df-gcd 14524 df-prm 14678 df-phi 14769 df-pc 14842 df-struct 15178 df-ndx 15179 df-slot 15180 df-base 15181 df-sets 15182 df-ress 15183 df-plusg 15258 df-mulr 15259 df-starv 15260 df-sca 15261 df-vsca 15262 df-ip 15263 df-tset 15264 df-ple 15265 df-ds 15267 df-unif 15268 df-0g 15395 df-gsum 15396 df-imas 15462 df-qus 15464 df-mgm 16543 df-sgrp 16582 df-mnd 16592 df-mhm 16637 df-submnd 16638 df-grp 16728 df-minusg 16729 df-sbg 16730 df-mulg 16731 df-subg 16869 df-nsg 16870 df-eqg 16871 df-ghm 16936 df-cntz 17026 df-cmn 17487 df-abl 17488 df-mgp 17779 df-ur 17791 df-ring 17837 df-cring 17838 df-oppr 17906 df-dvdsr 17924 df-unit 17925 df-invr 17955 df-dvr 17966 df-rnghom 17998 df-drng 18032 df-field 18033 df-subrg 18061 df-lmod 18148 df-lss 18211 df-lsp 18250 df-sra 18450 df-rgmod 18451 df-lidl 18452 df-rsp 18453 df-2idl 18511 df-nzr 18537 df-rlreg 18562 df-domn 18563 df-idom 18564 df-cnfld 19026 df-zring 19095 df-zrh 19130 df-zn 19133 df-lgs 24279

This theorem is referenced by: lgsquad 24341

W3C validator