lgsquadlem3 - Metamath Proof Explorer

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

Theorem lgsquadlem3 22821

Description: Lemma for lgsquad 22822. (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 2719	. . . . 5
5		lgsquad.5	. . . . 5
6		lgsquad.4	. . . . 5
7		eleq1 2523	. . . . . . . . . 10
8		eleq1 2523	. . . . . . . . . 10
9	7, 8	bi2anan9 868	. . . . . . . . 9 $/\$ $/\$ $/\$
10		ancom 450	. . . . . . . . 9 $/\$ $/\$
11	9, 10	syl6bb 261	. . . . . . . 8 $/\$ $/\$ $/\$
12		oveq1 6200	. . . . . . . . 9
13		oveq1 6200	. . . . . . . . 9
14	12, 13	breqan12d 4408	. . . . . . . 8 $/\$
15	11, 14	anbi12d 710	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
16	15	ancoms 453	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
17	16	cbvopabv 4462	. . . . 5 $/\$ $/\$ $/\$ $/\$
18	1, 2, 4, 5, 6, 17	lgsquadlem2 22820	. . . 4 $/\$ $/\$
19		relopab 5067	. . . . . . . 8 $/\$ $/\$
20		fzfid 11905	. . . . . . . . . 10
21		fzfid 11905	. . . . . . . . . 10
22		xpfi 7687	. . . . . . . . . 10 $/\$
23	20, 21, 22	syl2anc 661	. . . . . . . . 9
24		opabssxp 5012	. . . . . . . . 9 $/\$ $/\$
25		ssfi 7637	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
26	23, 24, 25	sylancl 662	. . . . . . . 8 $/\$ $/\$
27		cnven 7488	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
28	19, 26, 27	sylancr 663	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
29		cnvopab 5339	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
30	28, 29	syl6breq 4432	. . . . . 6 $/\$ $/\$ $/\$ $/\$
31		hasheni 12229	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
32	30, 31	syl 16	. . . . 5 $/\$ $/\$ $/\$ $/\$
33	32	oveq2d 6209	. . . 4 $/\$ $/\$ $/\$ $/\$
34	18, 33	eqtr4d 2495	. . 3 $/\$ $/\$
35		lgsquad.6	. . . 4 $/\$ $/\$
36	2, 1, 3, 6, 5, 35	lgsquadlem2 22820	. . 3
37	34, 36	oveq12d 6211	. 2 $/\$ $/\$
38		neg1cn 10529	. . . 4
39	38	a1i 11	. . 3
40		opabssxp 5012	. . . . . 6 $/\$ $/\$
41	35, 40	eqsstri 3487	. . . . 5
42		ssfi 7637	. . . . 5 $/\$
43	23, 41, 42	sylancl 662	. . . 4
44		hashcl 12236	. . . 4
45	43, 44	syl 16	. . 3
46		hashcl 12236	. . . 4 $/\$ $/\$ $/\$ $/\$
47	26, 46	syl 16	. . 3 $/\$ $/\$
48	39, 45, 47	expaddd 12120	. 2 $/\$ $/\$ $/\$ $/\$
49	1	eldifad 3441	. . . . . . . . . . . . . . . . 17
50	49	adantr 465	. . . . . . . . . . . . . . . 16 $/\$ $/\$
51		prmnn 13877	. . . . . . . . . . . . . . . 16
52	50, 51	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$
53		oddprm 13993	. . . . . . . . . . . . . . . . . . . . . 22 $\$
54	1, 53	syl 16	. . . . . . . . . . . . . . . . . . . . 21
55	5, 54	syl5eqel 2543	. . . . . . . . . . . . . . . . . . . 20
56	55	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
57	56	nnzd 10850	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
58		prmz 13878	. . . . . . . . . . . . . . . . . . . 20
59	50, 58	syl 16	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
60		peano2zm 10792	. . . . . . . . . . . . . . . . . . 19
61	59, 60	syl 16	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
62	56	nnred 10441	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
63	61	zred 10851	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
64		prmuz2 13892	. . . . . . . . . . . . . . . . . . . . . . . 24
65	50, 64	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
66		uz2m1nn 11033	. . . . . . . . . . . . . . . . . . . . . . 23
67	65, 66	syl 16	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
68	67	nnrpd 11130	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
69		rphalflt 11121	. . . . . . . . . . . . . . . . . . . . 21
70	68, 69	syl 16	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
71	5, 70	syl5eqbr 4426	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
72	62, 63, 71	ltled 9626	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
73		eluz2 10971	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
74	57, 61, 72, 73	syl3anbrc 1172	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
75		fzss2 11608	. . . . . . . . . . . . . . . . 17
76	74, 75	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$
77		simprr 756	. . . . . . . . . . . . . . . 16 $/\$ $/\$
78	76, 77	sseldd 3458	. . . . . . . . . . . . . . 15 $/\$ $/\$
79		fzm1ndvds 13696	. . . . . . . . . . . . . . 15 $/\$
80	52, 78, 79	syl2anc 661	. . . . . . . . . . . . . 14 $/\$ $/\$
81	4	adantr 465	. . . . . . . . . . . . . . . 16 $/\$ $/\$
82	2	eldifad 3441	. . . . . . . . . . . . . . . . . 18
83	82	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
84		prmrp 13898	. . . . . . . . . . . . . . . . 17 $/\$
85	50, 83, 84	syl2anc 661	. . . . . . . . . . . . . . . 16 $/\$ $/\$
86	81, 85	mpbird 232	. . . . . . . . . . . . . . 15 $/\$ $/\$
87		prmz 13878	. . . . . . . . . . . . . . . . 17
88	83, 87	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$
89		elfzelz 11563	. . . . . . . . . . . . . . . . 17
90	89	ad2antll 728	. . . . . . . . . . . . . . . 16 $/\$ $/\$
91		coprmdvds 13899	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
92	59, 88, 90, 91	syl3anc 1219	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
93	86, 92	mpan2d 674	. . . . . . . . . . . . . 14 $/\$ $/\$
94	80, 93	mtod 177	. . . . . . . . . . . . 13 $/\$ $/\$
95		prmnn 13877	. . . . . . . . . . . . . . . . 17
96	83, 95	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$
97	96	nncnd 10442	. . . . . . . . . . . . . . 15 $/\$ $/\$
98		elfznn 11588	. . . . . . . . . . . . . . . . 17
99	98	ad2antll 728	. . . . . . . . . . . . . . . 16 $/\$ $/\$
100	99	nncnd 10442	. . . . . . . . . . . . . . 15 $/\$ $/\$
101	97, 100	mulcomd 9511	. . . . . . . . . . . . . 14 $/\$ $/\$
102	101	breq2d 4405	. . . . . . . . . . . . 13 $/\$ $/\$
103	94, 102	mtbid 300	. . . . . . . . . . . 12 $/\$ $/\$
104		elfzelz 11563	. . . . . . . . . . . . . . . 16
105	104	ad2antrl 727	. . . . . . . . . . . . . . 15 $/\$ $/\$
106		dvdsmul2 13666	. . . . . . . . . . . . . . 15 $/\$
107	105, 59, 106	syl2anc 661	. . . . . . . . . . . . . 14 $/\$ $/\$
108		breq2 4397	. . . . . . . . . . . . . 14
109	107, 108	syl5ibcom 220	. . . . . . . . . . . . 13 $/\$ $/\$
110	109	necon3bd 2660	. . . . . . . . . . . 12 $/\$ $/\$
111	103, 110	mpd 15	. . . . . . . . . . 11 $/\$ $/\$
112		elfznn 11588	. . . . . . . . . . . . . . 15
113	112	ad2antrl 727	. . . . . . . . . . . . . 14 $/\$ $/\$
114	113, 52	nnmulcld 10473	. . . . . . . . . . . . 13 $/\$ $/\$
115	114	nnred 10441	. . . . . . . . . . . 12 $/\$ $/\$
116	99, 96	nnmulcld 10473	. . . . . . . . . . . . 13 $/\$ $/\$
117	116	nnred 10441	. . . . . . . . . . . 12 $/\$ $/\$
118	115, 117	lttri2d 9617	. . . . . . . . . . 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 4456	. . . . . 6 $/\$ $/\$ $\/$ $/\$
125		unopab 4468	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
126	35	uneq2i 3608	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
127		andi 862	. . . . . . . 8 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $/\$
128	127	opabbii 4457	. . . . . . 7 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $/\$
129	125, 126, 128	3eqtr4i 2490	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $\/$
130		df-xp 4947	. . . . . 6 $/\$
131	124, 129, 130	3eqtr4g 2517	. . . . 5 $/\$ $/\$
132	131	fveq2d 5796	. . . 4 $/\$ $/\$
133		inopab 5071	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
134	35	ineq2i 3650	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
135		anandi 824	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
136	135	opabbii 4457	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
137	133, 134, 136	3eqtr4i 2490	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
138		ltnsym2 9578	. . . . . . . . . . . 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 1820	. . . . . . . 8 $/\$ $/\$ $/\$
144	143	nexdv 1820	. . . . . . 7 $/\$ $/\$ $/\$
145		opabn0 4720	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
146	145	necon1bbii 2712	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
147	144, 146	sylib 196	. . . . . 6 $/\$ $/\$ $/\$
148	137, 147	syl5eq 2504	. . . . 5 $/\$ $/\$
149		hashun 12256	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
150	26, 43, 148, 149	syl3anc 1219	. . . 4 $/\$ $/\$ $/\$ $/\$
151		hashxp 12307	. . . . . 6 $/\$
152	20, 21, 151	syl2anc 661	. . . . 5
153		oddprm 13993	. . . . . . . . . 10 $\$
154	2, 153	syl 16	. . . . . . . . 9
155	6, 154	syl5eqel 2543	. . . . . . . 8
156	155	nnnn0d 10740	. . . . . . 7
157		hashfz1 12227	. . . . . . 7
158	156, 157	syl 16	. . . . . 6
159	55	nnnn0d 10740	. . . . . . 7
160		hashfz1 12227	. . . . . . 7
161	159, 160	syl 16	. . . . . 6
162	158, 161	oveq12d 6211	. . . . 5
163	152, 162	eqtrd 2492	. . . 4
164	132, 150, 163	3eqtr3d 2500	. . 3 $/\$ $/\$
165	164	oveq2d 6209	. 2 $/\$ $/\$
166	37, 48, 165	3eqtr2d 2498	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1370

wex 1587

wcel 1758

wne 2644 $\$ cdif 3426

cun 3427

cin 3428

wss 3429

c0 3738

csn 3978 class class class wbr 4393

copab 4450

cxp 4939

ccnv 4940

wrel 4946

cfv 5519 (class class class)co 6193

cen 7410

cfn 7413

cc 9384

cr 9385

c1 9387

caddc 9389

cmul 9391

clt 9522

cle 9523

cmin 9699

cneg 9700

cdiv 10097

cn 10426

c2 10475

cn0 10683

cz 10750

cuz 10965

crp 11095

cfz 11547

cexp 11975

chash 12213

cdivides 13646

cgcd 13801

cprime 13874

clgs 22759

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1952 ax-ext 2430 ax-rep 4504 ax-sep 4514 ax-nul 4522 ax-pow 4571 ax-pr 4632 ax-un 6475 ax-inf2 7951 ax-cnex 9442 ax-resscn 9443 ax-1cn 9444 ax-icn 9445 ax-addcl 9446 ax-addrcl 9447 ax-mulcl 9448 ax-mulrcl 9449 ax-mulcom 9450 ax-addass 9451 ax-mulass 9452 ax-distr 9453 ax-i2m1 9454 ax-1ne0 9455 ax-1rid 9456 ax-rnegex 9457 ax-rrecex 9458 ax-cnre 9459 ax-pre-lttri 9460 ax-pre-lttrn 9461 ax-pre-ltadd 9462 ax-pre-mulgt0 9463 ax-pre-sup 9464 ax-addf 9465 ax-mulf 9466

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-fal 1376 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2264 df-mo 2265 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2601 df-ne 2646 df-nel 2647 df-ral 2800 df-rex 2801 df-reu 2802 df-rmo 2803 df-rab 2804 df-v 3073 df-sbc 3288 df-csb 3390 df-dif 3432 df-un 3434 df-in 3436 df-ss 3443 df-pss 3445 df-nul 3739 df-if 3893 df-pw 3963 df-sn 3979 df-pr 3981 df-tp 3983 df-op 3985 df-uni 4193 df-int 4230 df-iun 4274 df-disj 4364 df-br 4394 df-opab 4452 df-mpt 4453 df-tr 4487 df-eprel 4733 df-id 4737 df-po 4742 df-so 4743 df-fr 4780 df-se 4781 df-we 4782 df-ord 4823 df-on 4824 df-lim 4825 df-suc 4826 df-xp 4947 df-rel 4948 df-cnv 4949 df-co 4950 df-dm 4951 df-rn 4952 df-res 4953 df-ima 4954 df-iota 5482 df-fun 5521 df-fn 5522 df-f 5523 df-f1 5524 df-fo 5525 df-f1o 5526 df-fv 5527 df-isom 5528 df-riota 6154 df-ov 6196 df-oprab 6197 df-mpt2 6198 df-of 6423 df-om 6580 df-1st 6680 df-2nd 6681 df-supp 6794 df-tpos 6848 df-recs 6935 df-rdg 6969 df-1o 7023 df-2o 7024 df-oadd 7027 df-er 7204 df-ec 7206 df-qs 7210 df-map 7319 df-en 7414 df-dom 7415 df-sdom 7416 df-fin 7417 df-fsupp 7725 df-sup 7795 df-oi 7828 df-card 8213 df-cda 8441 df-pnf 9524 df-mnf 9525 df-xr 9526 df-ltxr 9527 df-le 9528 df-sub 9701 df-neg 9702 df-div 10098 df-nn 10427 df-2 10484 df-3 10485 df-4 10486 df-5 10487 df-6 10488 df-7 10489 df-8 10490 df-9 10491 df-10 10492 df-n0 10684 df-z 10751 df-dec 10860 df-uz 10966 df-q 11058 df-rp 11096 df-fz 11548 df-fzo 11659 df-fl 11752 df-mod 11819 df-seq 11917 df-exp 11976 df-hash 12214 df-cj 12699 df-re 12700 df-im 12701 df-sqr 12835 df-abs 12836 df-clim 13077 df-sum 13275 df-dvds 13647 df-gcd 13802 df-prm 13875 df-phi 13952 df-pc 14015 df-struct 14287 df-ndx 14288 df-slot 14289 df-base 14290 df-sets 14291 df-ress 14292 df-plusg 14362 df-mulr 14363 df-starv 14364 df-sca 14365 df-vsca 14366 df-ip 14367 df-tset 14368 df-ple 14369 df-ds 14371 df-unif 14372 df-0g 14491 df-gsum 14492 df-imas 14557 df-divs 14558 df-mnd 15526 df-mhm 15575 df-submnd 15576 df-grp 15656 df-minusg 15657 df-sbg 15658 df-mulg 15659 df-subg 15789 df-nsg 15790 df-eqg 15791 df-ghm 15856 df-cntz 15946 df-cmn 16392 df-abl 16393 df-mgp 16706 df-ur 16718 df-rng 16762 df-cring 16763 df-oppr 16830 df-dvdsr 16848 df-unit 16849 df-invr 16879 df-dvr 16890 df-rnghom 16921 df-drng 16949 df-field 16950 df-subrg 16978 df-lmod 17065 df-lss 17129 df-lsp 17168 df-sra 17368 df-rgmod 17369 df-lidl 17370 df-rsp 17371 df-2idl 17429 df-nzr 17455 df-rlreg 17469 df-domn 17470 df-idom 17471 df-cnfld 17937 df-zring 18002 df-zrh 18053 df-zn 18056 df-lgs 22760

This theorem is referenced by: lgsquad 22822

W3C validator