poimirlem1 - Mathbox for Brendan Leahy

	Mathbox for Brendan Leahy	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > poimirlem1		Structured version Unicode version

Theorem poimirlem1 31861

Description: Lemma for poimir 31893- the vertices on either side of a skipped vertex differ in at least two dimensions. (Contributed by Brendan Leahy, 21-Aug-2020.)

**Hypotheses**
Ref	Expression
poimir.0
poimirlem2.1
poimirlem2.2
poimirlem2.3
poimirlem1.4

**Assertion**
Ref	Expression
poimirlem1

Distinct variable groups:

Proof of Theorem poimirlem1 Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		poimirlem2.3	. . . . 5
2		f1of 5829	. . . . 5
3	1, 2	syl 17	. . . 4
4		poimir.0	. . . . . . . . 9
5	4	nncnd 10627	. . . . . . . 8
6		npcan1 10046	. . . . . . . 8
7	5, 6	syl 17	. . . . . . 7
8	4	nnzd 11041	. . . . . . . 8
9		peano2zm 10982	. . . . . . . 8
10		uzid 11175	. . . . . . . 8
11		peano2uz 11214	. . . . . . . 8
12	8, 9, 10, 11	4syl 19	. . . . . . 7
13	7, 12	eqeltrrd 2512	. . . . . 6
14		fzss2 11840	. . . . . 6
15	13, 14	syl 17	. . . . 5
16		poimirlem1.4	. . . . 5
17	15, 16	sseldd 3466	. . . 4
18	3, 17	ffvelrnd 6036	. . 3
19		fzp1elp1 11851	. . . . . 6
20	16, 19	syl 17	. . . . 5
21	7	oveq2d 6319	. . . . 5
22	20, 21	eleqtrd 2513	. . . 4
23	3, 22	ffvelrnd 6036	. . 3
24		imassrn 5196	. . . . . . . . . 10
25		frn 5750	. . . . . . . . . . 11
26	1, 2, 25	3syl 18	. . . . . . . . . 10
27	24, 26	syl5ss 3476	. . . . . . . . 9
28	27	sselda 3465	. . . . . . . 8 $/\$
29		poimirlem2.2	. . . . . . . . . . 11
30	29	ffvelrnda 6035	. . . . . . . . . 10 $/\$
31	30	zred 11042	. . . . . . . . 9 $/\$
32	31	ltp1d 10539	. . . . . . . . 9 $/\$
33	31, 32	ltned 9773	. . . . . . . 8 $/\$
34	28, 33	syldan 473	. . . . . . 7 $/\$
35		poimirlem2.1	. . . . . . . . . . 11
36		breq1 4424	. . . . . . . . . . . . . . 15
37		id 23	. . . . . . . . . . . . . . 15
38	36, 37	ifbieq1d 3933	. . . . . . . . . . . . . 14
39		elfzelz 11802	. . . . . . . . . . . . . . . . . 18
40	16, 39	syl 17	. . . . . . . . . . . . . . . . 17
41	40	zred 11042	. . . . . . . . . . . . . . . 16
42	41	ltm1d 10541	. . . . . . . . . . . . . . 15
43	42	iftrued 3918	. . . . . . . . . . . . . 14
44	38, 43	sylan9eqr 2486	. . . . . . . . . . . . 13 $/\$
45	44	csbeq1d 3403	. . . . . . . . . . . 12 $/\$
46	8, 9	syl 17	. . . . . . . . . . . . . . . 16
47		elfzm1b 11874	. . . . . . . . . . . . . . . 16 $/\$
48	40, 46, 47	syl2anc 666	. . . . . . . . . . . . . . 15
49	16, 48	mpbid 214	. . . . . . . . . . . . . 14
50		oveq2 6311	. . . . . . . . . . . . . . . . . . 19
51	50	imaeq2d 5185	. . . . . . . . . . . . . . . . . 18
52	51	xpeq1d 4874	. . . . . . . . . . . . . . . . 17
53	52	adantl 468	. . . . . . . . . . . . . . . 16 $/\$
54		oveq1 6310	. . . . . . . . . . . . . . . . . . . 20
55	40	zcnd 11043	. . . . . . . . . . . . . . . . . . . . 21
56		npcan1 10046	. . . . . . . . . . . . . . . . . . . . 21
57	55, 56	syl 17	. . . . . . . . . . . . . . . . . . . 20
58	54, 57	sylan9eqr 2486	. . . . . . . . . . . . . . . . . . 19 $/\$
59	58	oveq1d 6318	. . . . . . . . . . . . . . . . . 18 $/\$
60	59	imaeq2d 5185	. . . . . . . . . . . . . . . . 17 $/\$
61	60	xpeq1d 4874	. . . . . . . . . . . . . . . 16 $/\$
62	53, 61	uneq12d 3622	. . . . . . . . . . . . . . 15 $/\$
63	62	oveq2d 6319	. . . . . . . . . . . . . 14 $/\$
64	49, 63	csbied 3423	. . . . . . . . . . . . 13
65	64	adantr 467	. . . . . . . . . . . 12 $/\$
66	45, 65	eqtrd 2464	. . . . . . . . . . 11 $/\$
67	46	zcnd 11043	. . . . . . . . . . . . . . 15
68		npcan1 10046	. . . . . . . . . . . . . . 15
69	67, 68	syl 17	. . . . . . . . . . . . . 14
70		peano2zm 10982	. . . . . . . . . . . . . . 15
71		uzid 11175	. . . . . . . . . . . . . . 15
72		peano2uz 11214	. . . . . . . . . . . . . . 15
73	46, 70, 71, 72	4syl 19	. . . . . . . . . . . . . 14
74	69, 73	eqeltrrd 2512	. . . . . . . . . . . . 13
75		fzss2 11840	. . . . . . . . . . . . 13
76	74, 75	syl 17	. . . . . . . . . . . 12
77	76, 49	sseldd 3466	. . . . . . . . . . 11
78		ovex 6331	. . . . . . . . . . . 12
79	78	a1i 11	. . . . . . . . . . 11
80	35, 66, 77, 79	fvmptd 5968	. . . . . . . . . 10
81	80	fveq1d 5881	. . . . . . . . 9
82	81	adantr 467	. . . . . . . 8 $/\$
83		ffn 5744	. . . . . . . . . . . 12
84	29, 83	syl 17	. . . . . . . . . . 11
85	84	adantr 467	. . . . . . . . . 10 $/\$
86		1ex 9640	. . . . . . . . . . . . . . 15
87		fnconstg 5786	. . . . . . . . . . . . . . 15
88	86, 87	ax-mp 5	. . . . . . . . . . . . . 14
89		c0ex 9639	. . . . . . . . . . . . . . 15
90		fnconstg 5786	. . . . . . . . . . . . . . 15
91	89, 90	ax-mp 5	. . . . . . . . . . . . . 14
92	88, 91	pm3.2i 457	. . . . . . . . . . . . 13 $/\$
93		dff1o3 5835	. . . . . . . . . . . . . . . 16 $/\$
94	93	simprbi 466	. . . . . . . . . . . . . . 15
95		imain 5675	. . . . . . . . . . . . . . 15
96	1, 94, 95	3syl 18	. . . . . . . . . . . . . 14
97		fzdisj 11828	. . . . . . . . . . . . . . . . 17
98	42, 97	syl 17	. . . . . . . . . . . . . . . 16
99	98	imaeq2d 5185	. . . . . . . . . . . . . . 15
100		ima0 5200	. . . . . . . . . . . . . . 15
101	99, 100	syl6eq 2480	. . . . . . . . . . . . . 14
102	96, 101	eqtr3d 2466	. . . . . . . . . . . . 13
103		fnun 5698	. . . . . . . . . . . . 13 $/\$ $/\$
104	92, 102, 103	sylancr 668	. . . . . . . . . . . 12
105		elfzuz 11798	. . . . . . . . . . . . . . . . . . . 20
106	16, 105	syl 17	. . . . . . . . . . . . . . . . . . 19
107	57, 106	eqeltrd 2511	. . . . . . . . . . . . . . . . . 18
108		peano2zm 10982	. . . . . . . . . . . . . . . . . . . . . 22
109		uzid 11175	. . . . . . . . . . . . . . . . . . . . . 22
110		peano2uz 11214	. . . . . . . . . . . . . . . . . . . . . 22
111	40, 108, 109, 110	4syl 19	. . . . . . . . . . . . . . . . . . . . 21
112	57, 111	eqeltrrd 2512	. . . . . . . . . . . . . . . . . . . 20
113		peano2uz 11214	. . . . . . . . . . . . . . . . . . . 20
114		uzss 11181	. . . . . . . . . . . . . . . . . . . 20
115	112, 113, 114	3syl 18	. . . . . . . . . . . . . . . . . . 19
116		elfzuz3 11799	. . . . . . . . . . . . . . . . . . . . 21
117		eluzp1p1 11186	. . . . . . . . . . . . . . . . . . . . 21
118	16, 116, 117	3syl 18	. . . . . . . . . . . . . . . . . . . 20
119	7, 118	eqeltrrd 2512	. . . . . . . . . . . . . . . . . . 19
120	115, 119	sseldd 3466	. . . . . . . . . . . . . . . . . 18
121		fzsplit2 11826	. . . . . . . . . . . . . . . . . 18 $/\$
122	107, 120, 121	syl2anc 666	. . . . . . . . . . . . . . . . 17
123	57	oveq1d 6318	. . . . . . . . . . . . . . . . . 18
124	123	uneq2d 3621	. . . . . . . . . . . . . . . . 17
125	122, 124	eqtrd 2464	. . . . . . . . . . . . . . . 16
126	125	imaeq2d 5185	. . . . . . . . . . . . . . 15
127		imaundi 5265	. . . . . . . . . . . . . . 15
128	126, 127	syl6eq 2480	. . . . . . . . . . . . . 14
129		f1ofo 5836	. . . . . . . . . . . . . . 15
130		foima 5813	. . . . . . . . . . . . . . 15
131	1, 129, 130	3syl 18	. . . . . . . . . . . . . 14
132	128, 131	eqtr3d 2466	. . . . . . . . . . . . 13
133	132	fneq2d 5683	. . . . . . . . . . . 12
134	104, 133	mpbid 214	. . . . . . . . . . 11
135	134	adantr 467	. . . . . . . . . 10 $/\$
136		ovex 6331	. . . . . . . . . . 11
137	136	a1i 11	. . . . . . . . . 10 $/\$
138		inidm 3672	. . . . . . . . . 10
139		eqidd 2424	. . . . . . . . . 10 $/\$ $/\$
140	102	adantr 467	. . . . . . . . . . . . 13 $/\$
141		fzss2 11840	. . . . . . . . . . . . . . 15
142		imass2 5221	. . . . . . . . . . . . . . 15
143	119, 141, 142	3syl 18	. . . . . . . . . . . . . 14
144	143	sselda 3465	. . . . . . . . . . . . 13 $/\$
145		fvun2 5951	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
146	88, 91, 145	mp3an12 1351	. . . . . . . . . . . . 13 $/\$
147	140, 144, 146	syl2anc 666	. . . . . . . . . . . 12 $/\$
148	89	fvconst2 6133	. . . . . . . . . . . . 13
149	144, 148	syl 17	. . . . . . . . . . . 12 $/\$
150	147, 149	eqtrd 2464	. . . . . . . . . . 11 $/\$
151	150	adantr 467	. . . . . . . . . 10 $/\$ $/\$
152	85, 135, 137, 137, 138, 139, 151	ofval 6552	. . . . . . . . 9 $/\$ $/\$
153	28, 152	mpdan 673	. . . . . . . 8 $/\$
154	30	zcnd 11043	. . . . . . . . . 10 $/\$
155	154	addid1d 9835	. . . . . . . . 9 $/\$
156	28, 155	syldan 473	. . . . . . . 8 $/\$
157	82, 153, 156	3eqtrd 2468	. . . . . . 7 $/\$
158		breq1 4424	. . . . . . . . . . . . . . 15
159		oveq1 6310	. . . . . . . . . . . . . . 15
160	158, 159	ifbieq2d 3935	. . . . . . . . . . . . . 14
161	41	ltnrd 9771	. . . . . . . . . . . . . . 15
162	161	iffalsed 3921	. . . . . . . . . . . . . 14
163	160, 162	sylan9eqr 2486	. . . . . . . . . . . . 13 $/\$
164	163	csbeq1d 3403	. . . . . . . . . . . 12 $/\$
165		ovex 6331	. . . . . . . . . . . . 13
166		oveq2 6311	. . . . . . . . . . . . . . . . 17
167	166	imaeq2d 5185	. . . . . . . . . . . . . . . 16
168	167	xpeq1d 4874	. . . . . . . . . . . . . . 15
169		oveq1 6310	. . . . . . . . . . . . . . . . . 18
170	169	oveq1d 6318	. . . . . . . . . . . . . . . . 17
171	170	imaeq2d 5185	. . . . . . . . . . . . . . . 16
172	171	xpeq1d 4874	. . . . . . . . . . . . . . 15
173	168, 172	uneq12d 3622	. . . . . . . . . . . . . 14
174	173	oveq2d 6319	. . . . . . . . . . . . 13
175	165, 174	csbie 3422	. . . . . . . . . . . 12
176	164, 175	syl6eq 2480	. . . . . . . . . . 11 $/\$
177		1eluzge0 11204	. . . . . . . . . . . . 13
178		fzss1 11839	. . . . . . . . . . . . 13
179	177, 178	ax-mp 5	. . . . . . . . . . . 12
180	179, 16	sseldi 3463	. . . . . . . . . . 11
181		ovex 6331	. . . . . . . . . . . 12
182	181	a1i 11	. . . . . . . . . . 11
183	35, 176, 180, 182	fvmptd 5968	. . . . . . . . . 10
184	183	fveq1d 5881	. . . . . . . . 9
185	184	adantr 467	. . . . . . . 8 $/\$
186		fnconstg 5786	. . . . . . . . . . . . . . 15
187	86, 186	ax-mp 5	. . . . . . . . . . . . . 14
188		fnconstg 5786	. . . . . . . . . . . . . . 15
189	89, 188	ax-mp 5	. . . . . . . . . . . . . 14
190	187, 189	pm3.2i 457	. . . . . . . . . . . . 13 $/\$
191		imain 5675	. . . . . . . . . . . . . . . 16
192	1, 94, 191	3syl 18	. . . . . . . . . . . . . . 15
193		peano2re 9808	. . . . . . . . . . . . . . . . . . 19
194	41, 193	syl 17	. . . . . . . . . . . . . . . . . 18
195	194	ltp1d 10539	. . . . . . . . . . . . . . . . 17
196		fzdisj 11828	. . . . . . . . . . . . . . . . 17
197	195, 196	syl 17	. . . . . . . . . . . . . . . 16
198	197	imaeq2d 5185	. . . . . . . . . . . . . . 15
199	192, 198	eqtr3d 2466	. . . . . . . . . . . . . 14
200	199, 100	syl6eq 2480	. . . . . . . . . . . . 13
201		fnun 5698	. . . . . . . . . . . . 13 $/\$ $/\$
202	190, 200, 201	sylancr 668	. . . . . . . . . . . 12
203		fzsplit 11827	. . . . . . . . . . . . . . . . 17
204	22, 203	syl 17	. . . . . . . . . . . . . . . 16
205	204	imaeq2d 5185	. . . . . . . . . . . . . . 15
206		imaundi 5265	. . . . . . . . . . . . . . 15
207	205, 206	syl6eq 2480	. . . . . . . . . . . . . 14
208	207, 131	eqtr3d 2466	. . . . . . . . . . . . 13
209	208	fneq2d 5683	. . . . . . . . . . . 12
210	202, 209	mpbid 214	. . . . . . . . . . 11
211	210	adantr 467	. . . . . . . . . 10 $/\$
212	200	adantr 467	. . . . . . . . . . . . 13 $/\$
213		fzss1 11839	. . . . . . . . . . . . . . 15
214		imass2 5221	. . . . . . . . . . . . . . 15
215	106, 213, 214	3syl 18	. . . . . . . . . . . . . 14
216	215	sselda 3465	. . . . . . . . . . . . 13 $/\$
217		fvun1 5950	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
218	187, 189, 217	mp3an12 1351	. . . . . . . . . . . . 13 $/\$
219	212, 216, 218	syl2anc 666	. . . . . . . . . . . 12 $/\$
220	86	fvconst2 6133	. . . . . . . . . . . . 13
221	216, 220	syl 17	. . . . . . . . . . . 12 $/\$
222	219, 221	eqtrd 2464	. . . . . . . . . . 11 $/\$
223	222	adantr 467	. . . . . . . . . 10 $/\$ $/\$
224	85, 211, 137, 137, 138, 139, 223	ofval 6552	. . . . . . . . 9 $/\$ $/\$
225	28, 224	mpdan 673	. . . . . . . 8 $/\$
226	185, 225	eqtrd 2464	. . . . . . 7 $/\$
227	34, 157, 226	3netr4d 2730	. . . . . 6 $/\$
228	227	ralrimiva 2840	. . . . 5
229		fzpr 11853	. . . . . . . . 9
230	16, 39, 229	3syl 18	. . . . . . . 8
231	230	imaeq2d 5185	. . . . . . 7
232		f1ofn 5830	. . . . . . . . 9
233	1, 232	syl 17	. . . . . . . 8
234		fnimapr 5943	. . . . . . . 8 $/\$ $/\$
235	233, 17, 22, 234	syl3anc 1265	. . . . . . 7
236	231, 235	eqtrd 2464	. . . . . 6
237	236	raleqdv 3032	. . . . 5
238	228, 237	mpbid 214	. . . 4
239		fvex 5889	. . . . 5
240		fvex 5889	. . . . 5
241		fveq2 5879	. . . . . 6
242		fveq2 5879	. . . . . 6
243	241, 242	neeq12d 2704	. . . . 5
244		fveq2 5879	. . . . . 6
245		fveq2 5879	. . . . . 6
246	244, 245	neeq12d 2704	. . . . 5
247	239, 240, 243, 246	ralpr 4051	. . . 4 $/\$
248	238, 247	sylib 200	. . 3 $/\$
249	41	ltp1d 10539	. . . . 5
250	41, 249	ltned 9773	. . . 4
251		f1of1 5828	. . . . . . 7
252	1, 251	syl 17	. . . . . 6
253		f1veqaeq 6174	. . . . . 6 $/\$ $/\$
254	252, 17, 22, 253	syl12anc 1263	. . . . 5
255	254	necon3d 2649	. . . 4
256	250, 255	mpd 15	. . 3
257	243	anbi1d 710	. . . . 5 $/\$ $/\$
258		neeq1 2706	. . . . 5
259	257, 258	anbi12d 716	. . . 4 $/\$ $/\$ $/\$ $/\$
260		fveq2 5879	. . . . . . 7
261		fveq2 5879	. . . . . . 7
262	260, 261	neeq12d 2704	. . . . . 6
263	262	anbi2d 709	. . . . 5 $/\$ $/\$
264		neeq2 2708	. . . . 5
265	263, 264	anbi12d 716	. . . 4 $/\$ $/\$ $/\$ $/\$
266	259, 265	rspc2ev 3194	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
267	18, 23, 248, 256, 266	syl112anc 1269	. 2 $/\$ $/\$
268		dfrex2 2877	. . 3 $/\$ $/\$ $/\$ $/\$
269		fveq2 5879	. . . . . 6
270		fveq2 5879	. . . . . 6
271	269, 270	neeq12d 2704	. . . . 5
272	271	rmo4 3265	. . . 4 $/\$
273		dfral2 2873	. . . . . 6 $/\$ $/\$
274		df-ne 2621	. . . . . . . . 9
275	274	anbi2i 699	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
276		annim 427	. . . . . . . 8 $/\$ $/\$ $/\$
277	275, 276	bitri 253	. . . . . . 7 $/\$ $/\$ $/\$
278	277	rexbii 2928	. . . . . 6 $/\$ $/\$ $/\$
279	273, 278	xchbinxr 313	. . . . 5 $/\$ $/\$ $/\$
280	279	ralbii 2857	. . . 4 $/\$ $/\$ $/\$
281	272, 280	bitri 253	. . 3 $/\$ $/\$
282	268, 281	xchbinxr 313	. 2 $/\$ $/\$
283	267, 282	sylib 200	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 188 $/\$ wa 371

wceq 1438

wcel 1869

wne 2619

wral 2776

wrex 2777

wrmo 2779

cvv 3082

csb 3396

cun 3435

cin 3436

wss 3437

c0 3762

cif 3910

csn 3997

cpr 3999 class class class wbr 4421

cmpt 4480

cxp 4849

ccnv 4850

crn 4852

cima 4854

wfun 5593

wfn 5594

wf 5595

wf1 5596

wfo 5597

wf1o 5598

cfv 5599 (class class class)co 6303

cof 6541

cc 9539

cr 9540

cc0 9541

c1 9542

caddc 9544

clt 9677

cmin 9862

cn 10611

cz 10939

cuz 11161

cfz 11786

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1666 ax-4 1679 ax-5 1749 ax-6 1795 ax-7 1840 ax-8 1871 ax-9 1873 ax-10 1888 ax-11 1893 ax-12 1906 ax-13 2054 ax-ext 2401 ax-rep 4534 ax-sep 4544 ax-nul 4553 ax-pow 4600 ax-pr 4658 ax-un 6595 ax-cnex 9597 ax-resscn 9598 ax-1cn 9599 ax-icn 9600 ax-addcl 9601 ax-addrcl 9602 ax-mulcl 9603 ax-mulrcl 9604 ax-mulcom 9605 ax-addass 9606 ax-mulass 9607 ax-distr 9608 ax-i2m1 9609 ax-1ne0 9610 ax-1rid 9611 ax-rnegex 9612 ax-rrecex 9613 ax-cnre 9614 ax-pre-lttri 9615 ax-pre-lttrn 9616 ax-pre-ltadd 9617 ax-pre-mulgt0 9618

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 984 df-3an 985 df-tru 1441 df-ex 1661 df-nf 1665 df-sb 1788 df-eu 2270 df-mo 2271 df-clab 2409 df-cleq 2415 df-clel 2418 df-nfc 2573 df-ne 2621 df-nel 2622 df-ral 2781 df-rex 2782 df-reu 2783 df-rmo 2784 df-rab 2785 df-v 3084 df-sbc 3301 df-csb 3397 df-dif 3440 df-un 3442 df-in 3444 df-ss 3451 df-pss 3453 df-nul 3763 df-if 3911 df-pw 3982 df-sn 3998 df-pr 4000 df-tp 4002 df-op 4004 df-uni 4218 df-iun 4299 df-br 4422 df-opab 4481 df-mpt 4482 df-tr 4517 df-eprel 4762 df-id 4766 df-po 4772 df-so 4773 df-fr 4810 df-we 4812 df-xp 4857 df-rel 4858 df-cnv 4859 df-co 4860 df-dm 4861 df-rn 4862 df-res 4863 df-ima 4864 df-pred 5397 df-ord 5443 df-on 5444 df-lim 5445 df-suc 5446 df-iota 5563 df-fun 5601 df-fn 5602 df-f 5603 df-f1 5604 df-fo 5605 df-f1o 5606 df-fv 5607 df-riota 6265 df-ov 6306 df-oprab 6307 df-mpt2 6308 df-of 6543 df-om 6705 df-1st 6805 df-2nd 6806 df-wrecs 7034 df-recs 7096 df-rdg 7134 df-er 7369 df-en 7576 df-dom 7577 df-sdom 7578 df-pnf 9679 df-mnf 9680 df-xr 9681 df-ltxr 9682 df-le 9683 df-sub 9864 df-neg 9865 df-nn 10612 df-n0 10872 df-z 10940 df-uz 11162 df-fz 11787

This theorem is referenced by: poimirlem8 31868 poimirlem18 31878 poimirlem21 31881 poimirlem22 31882

W3C validator