lgsquadlem3 - Metamath Proof Explorer

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

Theorem lgsquadlem3 23359

Description: Lemma for lgsquad 23360. (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 2738	. . . . 5
5		lgsquad.5	. . . . 5
6		lgsquad.4	. . . . 5
7		eleq1 2539	. . . . . . . . . 10
8		eleq1 2539	. . . . . . . . . 10
9	7, 8	bi2anan9 871	. . . . . . . . 9 $/\$ $/\$ $/\$
10		ancom 450	. . . . . . . . 9 $/\$ $/\$
11	9, 10	syl6bb 261	. . . . . . . 8 $/\$ $/\$ $/\$
12		oveq1 6289	. . . . . . . . 9
13		oveq1 6289	. . . . . . . . 9
14	12, 13	breqan12d 4462	. . . . . . . 8 $/\$
15	11, 14	anbi12d 710	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
16	15	ancoms 453	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
17	16	cbvopabv 4516	. . . . 5 $/\$ $/\$ $/\$ $/\$
18	1, 2, 4, 5, 6, 17	lgsquadlem2 23358	. . . 4 $/\$ $/\$
19		relopab 5127	. . . . . . . 8 $/\$ $/\$
20		fzfid 12047	. . . . . . . . . 10
21		fzfid 12047	. . . . . . . . . 10
22		xpfi 7787	. . . . . . . . . 10 $/\$
23	20, 21, 22	syl2anc 661	. . . . . . . . 9
24		opabssxp 5072	. . . . . . . . 9 $/\$ $/\$
25		ssfi 7737	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
26	23, 24, 25	sylancl 662	. . . . . . . 8 $/\$ $/\$
27		cnven 7588	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
28	19, 26, 27	sylancr 663	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
29		cnvopab 5405	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
30	28, 29	syl6breq 4486	. . . . . 6 $/\$ $/\$ $/\$ $/\$
31		hasheni 12385	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
32	30, 31	syl 16	. . . . 5 $/\$ $/\$ $/\$ $/\$
33	32	oveq2d 6298	. . . 4 $/\$ $/\$ $/\$ $/\$
34	18, 33	eqtr4d 2511	. . 3 $/\$ $/\$
35		lgsquad.6	. . . 4 $/\$ $/\$
36	2, 1, 3, 6, 5, 35	lgsquadlem2 23358	. . 3
37	34, 36	oveq12d 6300	. 2 $/\$ $/\$
38		neg1cn 10635	. . . 4
39	38	a1i 11	. . 3
40		opabssxp 5072	. . . . . 6 $/\$ $/\$
41	35, 40	eqsstri 3534	. . . . 5
42		ssfi 7737	. . . . 5 $/\$
43	23, 41, 42	sylancl 662	. . . 4
44		hashcl 12392	. . . 4
45	43, 44	syl 16	. . 3
46		hashcl 12392	. . . 4 $/\$ $/\$ $/\$ $/\$
47	26, 46	syl 16	. . 3 $/\$ $/\$
48	39, 45, 47	expaddd 12276	. 2 $/\$ $/\$ $/\$ $/\$
49	1	eldifad 3488	. . . . . . . . . . . . . . . . 17
50	49	adantr 465	. . . . . . . . . . . . . . . 16 $/\$ $/\$
51		prmnn 14075	. . . . . . . . . . . . . . . 16
52	50, 51	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$
53		oddprm 14194	. . . . . . . . . . . . . . . . . . . . . 22 $\$
54	1, 53	syl 16	. . . . . . . . . . . . . . . . . . . . 21
55	5, 54	syl5eqel 2559	. . . . . . . . . . . . . . . . . . . 20
56	55	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
57	56	nnzd 10961	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
58		prmz 14076	. . . . . . . . . . . . . . . . . . . 20
59	50, 58	syl 16	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
60		peano2zm 10902	. . . . . . . . . . . . . . . . . . 19
61	59, 60	syl 16	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
62	56	nnred 10547	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
63	61	zred 10962	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
64		prmuz2 14090	. . . . . . . . . . . . . . . . . . . . . . . 24
65	50, 64	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
66		uz2m1nn 11152	. . . . . . . . . . . . . . . . . . . . . . 23
67	65, 66	syl 16	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
68	67	nnrpd 11251	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
69		rphalflt 11242	. . . . . . . . . . . . . . . . . . . . 21
70	68, 69	syl 16	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
71	5, 70	syl5eqbr 4480	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
72	62, 63, 71	ltled 9728	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
73		eluz2 11084	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
74	57, 61, 72, 73	syl3anbrc 1180	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
75		fzss2 11719	. . . . . . . . . . . . . . . . 17
76	74, 75	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$
77		simprr 756	. . . . . . . . . . . . . . . 16 $/\$ $/\$
78	76, 77	sseldd 3505	. . . . . . . . . . . . . . 15 $/\$ $/\$
79		fzm1ndvds 13893	. . . . . . . . . . . . . . 15 $/\$
80	52, 78, 79	syl2anc 661	. . . . . . . . . . . . . 14 $/\$ $/\$
81	4	adantr 465	. . . . . . . . . . . . . . . 16 $/\$ $/\$
82	2	eldifad 3488	. . . . . . . . . . . . . . . . . 18
83	82	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
84		prmrp 14097	. . . . . . . . . . . . . . . . 17 $/\$
85	50, 83, 84	syl2anc 661	. . . . . . . . . . . . . . . 16 $/\$ $/\$
86	81, 85	mpbird 232	. . . . . . . . . . . . . . 15 $/\$ $/\$
87		prmz 14076	. . . . . . . . . . . . . . . . 17
88	83, 87	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$
89		elfzelz 11684	. . . . . . . . . . . . . . . . 17
90	89	ad2antll 728	. . . . . . . . . . . . . . . 16 $/\$ $/\$
91		coprmdvds 14098	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
92	59, 88, 90, 91	syl3anc 1228	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
93	86, 92	mpan2d 674	. . . . . . . . . . . . . 14 $/\$ $/\$
94	80, 93	mtod 177	. . . . . . . . . . . . 13 $/\$ $/\$
95		prmnn 14075	. . . . . . . . . . . . . . . . 17
96	83, 95	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$
97	96	nncnd 10548	. . . . . . . . . . . . . . 15 $/\$ $/\$
98		elfznn 11710	. . . . . . . . . . . . . . . . 17
99	98	ad2antll 728	. . . . . . . . . . . . . . . 16 $/\$ $/\$
100	99	nncnd 10548	. . . . . . . . . . . . . . 15 $/\$ $/\$
101	97, 100	mulcomd 9613	. . . . . . . . . . . . . 14 $/\$ $/\$
102	101	breq2d 4459	. . . . . . . . . . . . 13 $/\$ $/\$
103	94, 102	mtbid 300	. . . . . . . . . . . 12 $/\$ $/\$
104		elfzelz 11684	. . . . . . . . . . . . . . . 16
105	104	ad2antrl 727	. . . . . . . . . . . . . . 15 $/\$ $/\$
106		dvdsmul2 13863	. . . . . . . . . . . . . . 15 $/\$
107	105, 59, 106	syl2anc 661	. . . . . . . . . . . . . 14 $/\$ $/\$
108		breq2 4451	. . . . . . . . . . . . . 14
109	107, 108	syl5ibcom 220	. . . . . . . . . . . . 13 $/\$ $/\$
110	109	necon3bd 2679	. . . . . . . . . . . 12 $/\$ $/\$
111	103, 110	mpd 15	. . . . . . . . . . 11 $/\$ $/\$
112		elfznn 11710	. . . . . . . . . . . . . . 15
113	112	ad2antrl 727	. . . . . . . . . . . . . 14 $/\$ $/\$
114	113, 52	nnmulcld 10579	. . . . . . . . . . . . 13 $/\$ $/\$
115	114	nnred 10547	. . . . . . . . . . . 12 $/\$ $/\$
116	99, 96	nnmulcld 10579	. . . . . . . . . . . . 13 $/\$ $/\$
117	116	nnred 10547	. . . . . . . . . . . 12 $/\$ $/\$
118	115, 117	lttri2d 9719	. . . . . . . . . . 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 4510	. . . . . 6 $/\$ $/\$ $\/$ $/\$
125		unopab 4522	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
126	35	uneq2i 3655	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
127		andi 865	. . . . . . . 8 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $/\$
128	127	opabbii 4511	. . . . . . 7 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $/\$
129	125, 126, 128	3eqtr4i 2506	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $\/$
130		df-xp 5005	. . . . . 6 $/\$
131	124, 129, 130	3eqtr4g 2533	. . . . 5 $/\$ $/\$
132	131	fveq2d 5868	. . . 4 $/\$ $/\$
133		inopab 5131	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
134	35	ineq2i 3697	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
135		anandi 826	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
136	135	opabbii 4511	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
137	133, 134, 136	3eqtr4i 2506	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
138		ltnsym2 9680	. . . . . . . . . . . 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 1832	. . . . . . . 8 $/\$ $/\$ $/\$
144	143	nexdv 1832	. . . . . . 7 $/\$ $/\$ $/\$
145		opabn0 4778	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
146	145	necon1bbii 2731	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
147	144, 146	sylib 196	. . . . . 6 $/\$ $/\$ $/\$
148	137, 147	syl5eq 2520	. . . . 5 $/\$ $/\$
149		hashun 12414	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
150	26, 43, 148, 149	syl3anc 1228	. . . 4 $/\$ $/\$ $/\$ $/\$
151		hashxp 12454	. . . . . 6 $/\$
152	20, 21, 151	syl2anc 661	. . . . 5
153		oddprm 14194	. . . . . . . . . 10 $\$
154	2, 153	syl 16	. . . . . . . . 9
155	6, 154	syl5eqel 2559	. . . . . . . 8
156	155	nnnn0d 10848	. . . . . . 7
157		hashfz1 12383	. . . . . . 7
158	156, 157	syl 16	. . . . . 6
159	55	nnnn0d 10848	. . . . . . 7
160		hashfz1 12383	. . . . . . 7
161	159, 160	syl 16	. . . . . 6
162	158, 161	oveq12d 6300	. . . . 5
163	152, 162	eqtrd 2508	. . . 4
164	132, 150, 163	3eqtr3d 2516	. . 3 $/\$ $/\$
165	164	oveq2d 6298	. 2 $/\$ $/\$
166	37, 48, 165	3eqtr2d 2514	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1379

wex 1596

wcel 1767

wne 2662 $\$ cdif 3473

cun 3474

cin 3475

wss 3476

c0 3785

csn 4027 class class class wbr 4447

copab 4504

cxp 4997

ccnv 4998

wrel 5004

cfv 5586 (class class class)co 6282

cen 7510

cfn 7513

cc 9486

cr 9487

c1 9489

caddc 9491

cmul 9493

clt 9624

cle 9625

cmin 9801

cneg 9802

cdiv 10202

cn 10532

c2 10581

cn0 10791

cz 10860

cuz 11078

crp 11216

cfz 11668

cexp 12130

chash 12369

cdivides 13843

cgcd 13999

cprime 14072

clgs 23297

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-rep 4558 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6574 ax-inf2 8054 ax-cnex 9544 ax-resscn 9545 ax-1cn 9546 ax-icn 9547 ax-addcl 9548 ax-addrcl 9549 ax-mulcl 9550 ax-mulrcl 9551 ax-mulcom 9552 ax-addass 9553 ax-mulass 9554 ax-distr 9555 ax-i2m1 9556 ax-1ne0 9557 ax-1rid 9558 ax-rnegex 9559 ax-rrecex 9560 ax-cnre 9561 ax-pre-lttri 9562 ax-pre-lttrn 9563 ax-pre-ltadd 9564 ax-pre-mulgt0 9565 ax-pre-sup 9566 ax-addf 9567 ax-mulf 9568

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-fal 1385 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-nel 2665 df-ral 2819 df-rex 2820 df-reu 2821 df-rmo 2822 df-rab 2823 df-v 3115 df-sbc 3332 df-csb 3436 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-pss 3492 df-nul 3786 df-if 3940 df-pw 4012 df-sn 4028 df-pr 4030 df-tp 4032 df-op 4034 df-uni 4246 df-int 4283 df-iun 4327 df-disj 4418 df-br 4448 df-opab 4506 df-mpt 4507 df-tr 4541 df-eprel 4791 df-id 4795 df-po 4800 df-so 4801 df-fr 4838 df-se 4839 df-we 4840 df-ord 4881 df-on 4882 df-lim 4883 df-suc 4884 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-res 5011 df-ima 5012 df-iota 5549 df-fun 5588 df-fn 5589 df-f 5590 df-f1 5591 df-fo 5592 df-f1o 5593 df-fv 5594 df-isom 5595 df-riota 6243 df-ov 6285 df-oprab 6286 df-mpt2 6287 df-of 6522 df-om 6679 df-1st 6781 df-2nd 6782 df-supp 6899 df-tpos 6952 df-recs 7039 df-rdg 7073 df-1o 7127 df-2o 7128 df-oadd 7131 df-er 7308 df-ec 7310 df-qs 7314 df-map 7419 df-en 7514 df-dom 7515 df-sdom 7516 df-fin 7517 df-fsupp 7826 df-sup 7897 df-oi 7931 df-card 8316 df-cda 8544 df-pnf 9626 df-mnf 9627 df-xr 9628 df-ltxr 9629 df-le 9630 df-sub 9803 df-neg 9804 df-div 10203 df-nn 10533 df-2 10590 df-3 10591 df-4 10592 df-5 10593 df-6 10594 df-7 10595 df-8 10596 df-9 10597 df-10 10598 df-n0 10792 df-z 10861 df-dec 10973 df-uz 11079 df-q 11179 df-rp 11217 df-fz 11669 df-fzo 11789 df-fl 11893 df-mod 11961 df-seq 12072 df-exp 12131 df-hash 12370 df-cj 12891 df-re 12892 df-im 12893 df-sqrt 13027 df-abs 13028 df-clim 13270 df-sum 13468 df-dvds 13844 df-gcd 14000 df-prm 14073 df-phi 14151 df-pc 14216 df-struct 14488 df-ndx 14489 df-slot 14490 df-base 14491 df-sets 14492 df-ress 14493 df-plusg 14564 df-mulr 14565 df-starv 14566 df-sca 14567 df-vsca 14568 df-ip 14569 df-tset 14570 df-ple 14571 df-ds 14573 df-unif 14574 df-0g 14693 df-gsum 14694 df-imas 14759 df-divs 14760 df-mnd 15728 df-mhm 15777 df-submnd 15778 df-grp 15858 df-minusg 15859 df-sbg 15860 df-mulg 15861 df-subg 15993 df-nsg 15994 df-eqg 15995 df-ghm 16060 df-cntz 16150 df-cmn 16596 df-abl 16597 df-mgp 16932 df-ur 16944 df-rng 16988 df-cring 16989 df-oppr 17056 df-dvdsr 17074 df-unit 17075 df-invr 17105 df-dvr 17116 df-rnghom 17148 df-drng 17181 df-field 17182 df-subrg 17210 df-lmod 17297 df-lss 17362 df-lsp 17401 df-sra 17601 df-rgmod 17602 df-lidl 17603 df-rsp 17604 df-2idl 17662 df-nzr 17688 df-rlreg 17702 df-domn 17703 df-idom 17704 df-cnfld 18192 df-zring 18257 df-zrh 18308 df-zn 18311 df-lgs 23298

This theorem is referenced by: lgsquad 23360

W3C validator