lgsquadlem3 - Metamath Proof Explorer

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

Theorem lgsquadlem3 23756

Description: Lemma for lgsquad 23757. (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 2728	. . . . 5
5		lgsquad.5	. . . . 5
6		lgsquad.4	. . . . 5
7		eleq1 2529	. . . . . . . . . 10
8		eleq1 2529	. . . . . . . . . 10
9	7, 8	bi2anan9 873	. . . . . . . . 9 $/\$ $/\$ $/\$
10		ancom 450	. . . . . . . . 9 $/\$ $/\$
11	9, 10	syl6bb 261	. . . . . . . 8 $/\$ $/\$ $/\$
12		oveq1 6303	. . . . . . . . 9
13		oveq1 6303	. . . . . . . . 9
14	12, 13	breqan12d 4471	. . . . . . . 8 $/\$
15	11, 14	anbi12d 710	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
16	15	ancoms 453	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
17	16	cbvopabv 4526	. . . . 5 $/\$ $/\$ $/\$ $/\$
18	1, 2, 4, 5, 6, 17	lgsquadlem2 23755	. . . 4 $/\$ $/\$
19		relopab 5138	. . . . . . . 8 $/\$ $/\$
20		fzfid 12085	. . . . . . . . . 10
21		fzfid 12085	. . . . . . . . . 10
22		xpfi 7809	. . . . . . . . . 10 $/\$
23	20, 21, 22	syl2anc 661	. . . . . . . . 9
24		opabssxp 5083	. . . . . . . . 9 $/\$ $/\$
25		ssfi 7759	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
26	23, 24, 25	sylancl 662	. . . . . . . 8 $/\$ $/\$
27		cnven 7610	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
28	19, 26, 27	sylancr 663	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
29		cnvopab 5414	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
30	28, 29	syl6breq 4495	. . . . . 6 $/\$ $/\$ $/\$ $/\$
31		hasheni 12423	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
32	30, 31	syl 16	. . . . 5 $/\$ $/\$ $/\$ $/\$
33	32	oveq2d 6312	. . . 4 $/\$ $/\$ $/\$ $/\$
34	18, 33	eqtr4d 2501	. . 3 $/\$ $/\$
35		lgsquad.6	. . . 4 $/\$ $/\$
36	2, 1, 3, 6, 5, 35	lgsquadlem2 23755	. . 3
37	34, 36	oveq12d 6314	. 2 $/\$ $/\$
38		neg1cn 10660	. . . 4
39	38	a1i 11	. . 3
40		opabssxp 5083	. . . . . 6 $/\$ $/\$
41	35, 40	eqsstri 3529	. . . . 5
42		ssfi 7759	. . . . 5 $/\$
43	23, 41, 42	sylancl 662	. . . 4
44		hashcl 12430	. . . 4
45	43, 44	syl 16	. . 3
46		hashcl 12430	. . . 4 $/\$ $/\$ $/\$ $/\$
47	26, 46	syl 16	. . 3 $/\$ $/\$
48	39, 45, 47	expaddd 12314	. 2 $/\$ $/\$ $/\$ $/\$
49	1	eldifad 3483	. . . . . . . . . . . . . . . . 17
50	49	adantr 465	. . . . . . . . . . . . . . . 16 $/\$ $/\$
51		prmnn 14231	. . . . . . . . . . . . . . . 16
52	50, 51	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$
53		oddprm 14350	. . . . . . . . . . . . . . . . . . . . . 22 $\$
54	1, 53	syl 16	. . . . . . . . . . . . . . . . . . . . 21
55	5, 54	syl5eqel 2549	. . . . . . . . . . . . . . . . . . . 20
56	55	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
57	56	nnzd 10989	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
58		prmz 14232	. . . . . . . . . . . . . . . . . . . 20
59	50, 58	syl 16	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
60		peano2zm 10928	. . . . . . . . . . . . . . . . . . 19
61	59, 60	syl 16	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
62	56	nnred 10571	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
63	61	zred 10990	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
64		prmuz2 14246	. . . . . . . . . . . . . . . . . . . . . . . 24
65	50, 64	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
66		uz2m1nn 11181	. . . . . . . . . . . . . . . . . . . . . . 23
67	65, 66	syl 16	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
68	67	nnrpd 11280	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
69		rphalflt 11271	. . . . . . . . . . . . . . . . . . . . 21
70	68, 69	syl 16	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
71	5, 70	syl5eqbr 4489	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
72	62, 63, 71	ltled 9750	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
73		eluz2 11112	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
74	57, 61, 72, 73	syl3anbrc 1180	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
75		fzss2 11748	. . . . . . . . . . . . . . . . 17
76	74, 75	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$
77		simprr 757	. . . . . . . . . . . . . . . 16 $/\$ $/\$
78	76, 77	sseldd 3500	. . . . . . . . . . . . . . 15 $/\$ $/\$
79		fzm1ndvds 14049	. . . . . . . . . . . . . . 15 $/\$
80	52, 78, 79	syl2anc 661	. . . . . . . . . . . . . 14 $/\$ $/\$
81	4	adantr 465	. . . . . . . . . . . . . . . 16 $/\$ $/\$
82	2	eldifad 3483	. . . . . . . . . . . . . . . . . 18
83	82	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
84		prmrp 14253	. . . . . . . . . . . . . . . . 17 $/\$
85	50, 83, 84	syl2anc 661	. . . . . . . . . . . . . . . 16 $/\$ $/\$
86	81, 85	mpbird 232	. . . . . . . . . . . . . . 15 $/\$ $/\$
87		prmz 14232	. . . . . . . . . . . . . . . . 17
88	83, 87	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$
89		elfzelz 11713	. . . . . . . . . . . . . . . . 17
90	89	ad2antll 728	. . . . . . . . . . . . . . . 16 $/\$ $/\$
91		coprmdvds 14254	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
92	59, 88, 90, 91	syl3anc 1228	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
93	86, 92	mpan2d 674	. . . . . . . . . . . . . 14 $/\$ $/\$
94	80, 93	mtod 177	. . . . . . . . . . . . 13 $/\$ $/\$
95		prmnn 14231	. . . . . . . . . . . . . . . . 17
96	83, 95	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$
97	96	nncnd 10572	. . . . . . . . . . . . . . 15 $/\$ $/\$
98		elfznn 11739	. . . . . . . . . . . . . . . . 17
99	98	ad2antll 728	. . . . . . . . . . . . . . . 16 $/\$ $/\$
100	99	nncnd 10572	. . . . . . . . . . . . . . 15 $/\$ $/\$
101	97, 100	mulcomd 9634	. . . . . . . . . . . . . 14 $/\$ $/\$
102	101	breq2d 4468	. . . . . . . . . . . . 13 $/\$ $/\$
103	94, 102	mtbid 300	. . . . . . . . . . . 12 $/\$ $/\$
104		elfzelz 11713	. . . . . . . . . . . . . . . 16
105	104	ad2antrl 727	. . . . . . . . . . . . . . 15 $/\$ $/\$
106		dvdsmul2 14017	. . . . . . . . . . . . . . 15 $/\$
107	105, 59, 106	syl2anc 661	. . . . . . . . . . . . . 14 $/\$ $/\$
108		breq2 4460	. . . . . . . . . . . . . 14
109	107, 108	syl5ibcom 220	. . . . . . . . . . . . 13 $/\$ $/\$
110	109	necon3bd 2669	. . . . . . . . . . . 12 $/\$ $/\$
111	103, 110	mpd 15	. . . . . . . . . . 11 $/\$ $/\$
112		elfznn 11739	. . . . . . . . . . . . . . 15
113	112	ad2antrl 727	. . . . . . . . . . . . . 14 $/\$ $/\$
114	113, 52	nnmulcld 10604	. . . . . . . . . . . . 13 $/\$ $/\$
115	114	nnred 10571	. . . . . . . . . . . 12 $/\$ $/\$
116	99, 96	nnmulcld 10604	. . . . . . . . . . . . 13 $/\$ $/\$
117	116	nnred 10571	. . . . . . . . . . . 12 $/\$ $/\$
118	115, 117	lttri2d 9741	. . . . . . . . . . 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 4520	. . . . . 6 $/\$ $/\$ $\/$ $/\$
125		unopab 4532	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
126	35	uneq2i 3651	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
127		andi 867	. . . . . . . 8 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $/\$
128	127	opabbii 4521	. . . . . . 7 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $/\$
129	125, 126, 128	3eqtr4i 2496	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $\/$
130		df-xp 5014	. . . . . 6 $/\$
131	124, 129, 130	3eqtr4g 2523	. . . . 5 $/\$ $/\$
132	131	fveq2d 5876	. . . 4 $/\$ $/\$
133		inopab 5143	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
134	35	ineq2i 3693	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
135		anandi 828	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
136	135	opabbii 4521	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
137	133, 134, 136	3eqtr4i 2496	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
138		ltnsym2 9701	. . . . . . . . . . . 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 1885	. . . . . . . 8 $/\$ $/\$ $/\$
144	143	nexdv 1885	. . . . . . 7 $/\$ $/\$ $/\$
145		opabn0 4787	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
146	145	necon1bbii 2721	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
147	144, 146	sylib 196	. . . . . 6 $/\$ $/\$ $/\$
148	137, 147	syl5eq 2510	. . . . 5 $/\$ $/\$
149		hashun 12452	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
150	26, 43, 148, 149	syl3anc 1228	. . . 4 $/\$ $/\$ $/\$ $/\$
151		hashxp 12495	. . . . . 6 $/\$
152	20, 21, 151	syl2anc 661	. . . . 5
153		oddprm 14350	. . . . . . . . . 10 $\$
154	2, 153	syl 16	. . . . . . . . 9
155	6, 154	syl5eqel 2549	. . . . . . . 8
156	155	nnnn0d 10873	. . . . . . 7
157		hashfz1 12421	. . . . . . 7
158	156, 157	syl 16	. . . . . 6
159	55	nnnn0d 10873	. . . . . . 7
160		hashfz1 12421	. . . . . . 7
161	159, 160	syl 16	. . . . . 6
162	158, 161	oveq12d 6314	. . . . 5
163	152, 162	eqtrd 2498	. . . 4
164	132, 150, 163	3eqtr3d 2506	. . 3 $/\$ $/\$
165	164	oveq2d 6312	. 2 $/\$ $/\$
166	37, 48, 165	3eqtr2d 2504	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1395

wex 1613

wcel 1819

wne 2652 $\$ cdif 3468

cun 3469

cin 3470

wss 3471

c0 3793

csn 4032 class class class wbr 4456

copab 4514

cxp 5006

ccnv 5007

wrel 5013

cfv 5594 (class class class)co 6296

cen 7532

cfn 7535

cc 9507

cr 9508

c1 9510

caddc 9512

cmul 9514

clt 9645

cle 9646

cmin 9824

cneg 9825

cdiv 10227

cn 10556

c2 10606

cn0 10816

cz 10885

cuz 11106

crp 11245

cfz 11697

cexp 12168

chash 12407

cdvds 13997

cgcd 14155

cprime 14228

clgs 23694

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1619 ax-4 1632 ax-5 1705 ax-6 1748 ax-7 1791 ax-8 1821 ax-9 1823 ax-10 1838 ax-11 1843 ax-12 1855 ax-13 2000 ax-ext 2435 ax-rep 4568 ax-sep 4578 ax-nul 4586 ax-pow 4634 ax-pr 4695 ax-un 6591 ax-inf2 8075 ax-cnex 9565 ax-resscn 9566 ax-1cn 9567 ax-icn 9568 ax-addcl 9569 ax-addrcl 9570 ax-mulcl 9571 ax-mulrcl 9572 ax-mulcom 9573 ax-addass 9574 ax-mulass 9575 ax-distr 9576 ax-i2m1 9577 ax-1ne0 9578 ax-1rid 9579 ax-rnegex 9580 ax-rrecex 9581 ax-cnre 9582 ax-pre-lttri 9583 ax-pre-lttrn 9584 ax-pre-ltadd 9585 ax-pre-mulgt0 9586 ax-pre-sup 9587 ax-addf 9588 ax-mulf 9589

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1398 df-fal 1401 df-ex 1614 df-nf 1618 df-sb 1741 df-eu 2287 df-mo 2288 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-nel 2655 df-ral 2812 df-rex 2813 df-reu 2814 df-rmo 2815 df-rab 2816 df-v 3111 df-sbc 3328 df-csb 3431 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-pss 3487 df-nul 3794 df-if 3945 df-pw 4017 df-sn 4033 df-pr 4035 df-tp 4037 df-op 4039 df-uni 4252 df-int 4289 df-iun 4334 df-disj 4428 df-br 4457 df-opab 4516 df-mpt 4517 df-tr 4551 df-eprel 4800 df-id 4804 df-po 4809 df-so 4810 df-fr 4847 df-se 4848 df-we 4849 df-ord 4890 df-on 4891 df-lim 4892 df-suc 4893 df-xp 5014 df-rel 5015 df-cnv 5016 df-co 5017 df-dm 5018 df-rn 5019 df-res 5020 df-ima 5021 df-iota 5557 df-fun 5596 df-fn 5597 df-f 5598 df-f1 5599 df-fo 5600 df-f1o 5601 df-fv 5602 df-isom 5603 df-riota 6258 df-ov 6299 df-oprab 6300 df-mpt2 6301 df-of 6539 df-om 6700 df-1st 6799 df-2nd 6800 df-supp 6918 df-tpos 6973 df-recs 7060 df-rdg 7094 df-1o 7148 df-2o 7149 df-oadd 7152 df-er 7329 df-ec 7331 df-qs 7335 df-map 7440 df-en 7536 df-dom 7537 df-sdom 7538 df-fin 7539 df-fsupp 7848 df-sup 7919 df-oi 7953 df-card 8337 df-cda 8565 df-pnf 9647 df-mnf 9648 df-xr 9649 df-ltxr 9650 df-le 9651 df-sub 9826 df-neg 9827 df-div 10228 df-nn 10557 df-2 10615 df-3 10616 df-4 10617 df-5 10618 df-6 10619 df-7 10620 df-8 10621 df-9 10622 df-10 10623 df-n0 10817 df-z 10886 df-dec 11001 df-uz 11107 df-q 11208 df-rp 11246 df-fz 11698 df-fzo 11821 df-fl 11931 df-mod 11999 df-seq 12110 df-exp 12169 df-hash 12408 df-cj 12943 df-re 12944 df-im 12945 df-sqrt 13079 df-abs 13080 df-clim 13322 df-sum 13520 df-dvds 13998 df-gcd 14156 df-prm 14229 df-phi 14307 df-pc 14372 df-struct 14645 df-ndx 14646 df-slot 14647 df-base 14648 df-sets 14649 df-ress 14650 df-plusg 14724 df-mulr 14725 df-starv 14726 df-sca 14727 df-vsca 14728 df-ip 14729 df-tset 14730 df-ple 14731 df-ds 14733 df-unif 14734 df-0g 14858 df-gsum 14859 df-imas 14924 df-qus 14925 df-mgm 15998 df-sgrp 16037 df-mnd 16047 df-mhm 16092 df-submnd 16093 df-grp 16183 df-minusg 16184 df-sbg 16185 df-mulg 16186 df-subg 16324 df-nsg 16325 df-eqg 16326 df-ghm 16391 df-cntz 16481 df-cmn 16926 df-abl 16927 df-mgp 17268 df-ur 17280 df-ring 17326 df-cring 17327 df-oppr 17398 df-dvdsr 17416 df-unit 17417 df-invr 17447 df-dvr 17458 df-rnghom 17490 df-drng 17524 df-field 17525 df-subrg 17553 df-lmod 17640 df-lss 17705 df-lsp 17744 df-sra 17944 df-rgmod 17945 df-lidl 17946 df-rsp 17947 df-2idl 18006 df-nzr 18032 df-rlreg 18057 df-domn 18058 df-idom 18059 df-cnfld 18547 df-zring 18615 df-zrh 18667 df-zn 18670 df-lgs 23695

This theorem is referenced by: lgsquad 23757

W3C validator