poimirlem1 - Mathbox for Brendan Leahy

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

Theorem poimirlem1 31934

Description: Lemma for poimir 31966- 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 5812	. . . . 5
3	1, 2	syl 17	. . . 4
4		poimir.0	. . . . . . . . 9
5	4	nncnd 10622	. . . . . . . 8
6		npcan1 10041	. . . . . . . 8
7	5, 6	syl 17	. . . . . . 7
8	4	nnzd 11036	. . . . . . . 8
9		peano2zm 10977	. . . . . . . 8
10		uzid 11170	. . . . . . . 8
11		peano2uz 11209	. . . . . . . 8
12	8, 9, 10, 11	4syl 19	. . . . . . 7
13	7, 12	eqeltrrd 2529	. . . . . 6
14		fzss2 11835	. . . . . 6
15	13, 14	syl 17	. . . . 5
16		poimirlem1.4	. . . . 5
17	15, 16	sseldd 3432	. . . 4
18	3, 17	ffvelrnd 6021	. . 3
19		fzp1elp1 11846	. . . . . 6
20	16, 19	syl 17	. . . . 5
21	7	oveq2d 6304	. . . . 5
22	20, 21	eleqtrd 2530	. . . 4
23	3, 22	ffvelrnd 6021	. . 3
24		imassrn 5178	. . . . . . . . . 10
25		frn 5733	. . . . . . . . . . 11
26	1, 2, 25	3syl 18	. . . . . . . . . 10
27	24, 26	syl5ss 3442	. . . . . . . . 9
28	27	sselda 3431	. . . . . . . 8 $/\$
29		poimirlem2.2	. . . . . . . . . . 11
30	29	ffvelrnda 6020	. . . . . . . . . 10 $/\$
31	30	zred 11037	. . . . . . . . 9 $/\$
32	31	ltp1d 10534	. . . . . . . . 9 $/\$
33	31, 32	ltned 9768	. . . . . . . 8 $/\$
34	28, 33	syldan 473	. . . . . . 7 $/\$
35		poimirlem2.1	. . . . . . . . . . 11
36		breq1 4404	. . . . . . . . . . . . . . 15
37		id 22	. . . . . . . . . . . . . . 15
38	36, 37	ifbieq1d 3903	. . . . . . . . . . . . . 14
39		elfzelz 11797	. . . . . . . . . . . . . . . . . 18
40	16, 39	syl 17	. . . . . . . . . . . . . . . . 17
41	40	zred 11037	. . . . . . . . . . . . . . . 16
42	41	ltm1d 10536	. . . . . . . . . . . . . . 15
43	42	iftrued 3888	. . . . . . . . . . . . . 14
44	38, 43	sylan9eqr 2506	. . . . . . . . . . . . 13 $/\$
45	44	csbeq1d 3369	. . . . . . . . . . . 12 $/\$
46	8, 9	syl 17	. . . . . . . . . . . . . . . 16
47		elfzm1b 11869	. . . . . . . . . . . . . . . 16 $/\$
48	40, 46, 47	syl2anc 666	. . . . . . . . . . . . . . 15
49	16, 48	mpbid 214	. . . . . . . . . . . . . 14
50		oveq2 6296	. . . . . . . . . . . . . . . . . . 19
51	50	imaeq2d 5167	. . . . . . . . . . . . . . . . . 18
52	51	xpeq1d 4856	. . . . . . . . . . . . . . . . 17
53	52	adantl 468	. . . . . . . . . . . . . . . 16 $/\$
54		oveq1 6295	. . . . . . . . . . . . . . . . . . . 20
55	40	zcnd 11038	. . . . . . . . . . . . . . . . . . . . 21
56		npcan1 10041	. . . . . . . . . . . . . . . . . . . . 21
57	55, 56	syl 17	. . . . . . . . . . . . . . . . . . . 20
58	54, 57	sylan9eqr 2506	. . . . . . . . . . . . . . . . . . 19 $/\$
59	58	oveq1d 6303	. . . . . . . . . . . . . . . . . 18 $/\$
60	59	imaeq2d 5167	. . . . . . . . . . . . . . . . 17 $/\$
61	60	xpeq1d 4856	. . . . . . . . . . . . . . . 16 $/\$
62	53, 61	uneq12d 3588	. . . . . . . . . . . . . . 15 $/\$
63	62	oveq2d 6304	. . . . . . . . . . . . . 14 $/\$
64	49, 63	csbied 3389	. . . . . . . . . . . . 13
65	64	adantr 467	. . . . . . . . . . . 12 $/\$
66	45, 65	eqtrd 2484	. . . . . . . . . . 11 $/\$
67	46	zcnd 11038	. . . . . . . . . . . . . . 15
68		npcan1 10041	. . . . . . . . . . . . . . 15
69	67, 68	syl 17	. . . . . . . . . . . . . 14
70		peano2zm 10977	. . . . . . . . . . . . . . 15
71		uzid 11170	. . . . . . . . . . . . . . 15
72		peano2uz 11209	. . . . . . . . . . . . . . 15
73	46, 70, 71, 72	4syl 19	. . . . . . . . . . . . . 14
74	69, 73	eqeltrrd 2529	. . . . . . . . . . . . 13
75		fzss2 11835	. . . . . . . . . . . . 13
76	74, 75	syl 17	. . . . . . . . . . . 12
77	76, 49	sseldd 3432	. . . . . . . . . . 11
78		ovex 6316	. . . . . . . . . . . 12
79	78	a1i 11	. . . . . . . . . . 11
80	35, 66, 77, 79	fvmptd 5952	. . . . . . . . . 10
81	80	fveq1d 5865	. . . . . . . . 9
82	81	adantr 467	. . . . . . . 8 $/\$
83		ffn 5726	. . . . . . . . . . . 12
84	29, 83	syl 17	. . . . . . . . . . 11
85	84	adantr 467	. . . . . . . . . 10 $/\$
86		1ex 9635	. . . . . . . . . . . . . . 15
87		fnconstg 5769	. . . . . . . . . . . . . . 15
88	86, 87	ax-mp 5	. . . . . . . . . . . . . 14
89		c0ex 9634	. . . . . . . . . . . . . . 15
90		fnconstg 5769	. . . . . . . . . . . . . . 15
91	89, 90	ax-mp 5	. . . . . . . . . . . . . 14
92	88, 91	pm3.2i 457	. . . . . . . . . . . . 13 $/\$
93		dff1o3 5818	. . . . . . . . . . . . . . . 16 $/\$
94	93	simprbi 466	. . . . . . . . . . . . . . 15
95		imain 5657	. . . . . . . . . . . . . . 15
96	1, 94, 95	3syl 18	. . . . . . . . . . . . . 14
97		fzdisj 11823	. . . . . . . . . . . . . . . . 17
98	42, 97	syl 17	. . . . . . . . . . . . . . . 16
99	98	imaeq2d 5167	. . . . . . . . . . . . . . 15
100		ima0 5182	. . . . . . . . . . . . . . 15
101	99, 100	syl6eq 2500	. . . . . . . . . . . . . 14
102	96, 101	eqtr3d 2486	. . . . . . . . . . . . 13
103		fnun 5680	. . . . . . . . . . . . 13 $/\$ $/\$
104	92, 102, 103	sylancr 668	. . . . . . . . . . . 12
105		elfzuz 11793	. . . . . . . . . . . . . . . . . . . 20
106	16, 105	syl 17	. . . . . . . . . . . . . . . . . . 19
107	57, 106	eqeltrd 2528	. . . . . . . . . . . . . . . . . 18
108		peano2zm 10977	. . . . . . . . . . . . . . . . . . . . . 22
109		uzid 11170	. . . . . . . . . . . . . . . . . . . . . 22
110		peano2uz 11209	. . . . . . . . . . . . . . . . . . . . . 22
111	40, 108, 109, 110	4syl 19	. . . . . . . . . . . . . . . . . . . . 21
112	57, 111	eqeltrrd 2529	. . . . . . . . . . . . . . . . . . . 20
113		peano2uz 11209	. . . . . . . . . . . . . . . . . . . 20
114		uzss 11176	. . . . . . . . . . . . . . . . . . . 20
115	112, 113, 114	3syl 18	. . . . . . . . . . . . . . . . . . 19
116		elfzuz3 11794	. . . . . . . . . . . . . . . . . . . . 21
117		eluzp1p1 11181	. . . . . . . . . . . . . . . . . . . . 21
118	16, 116, 117	3syl 18	. . . . . . . . . . . . . . . . . . . 20
119	7, 118	eqeltrrd 2529	. . . . . . . . . . . . . . . . . . 19
120	115, 119	sseldd 3432	. . . . . . . . . . . . . . . . . 18
121		fzsplit2 11821	. . . . . . . . . . . . . . . . . 18 $/\$
122	107, 120, 121	syl2anc 666	. . . . . . . . . . . . . . . . 17
123	57	oveq1d 6303	. . . . . . . . . . . . . . . . . 18
124	123	uneq2d 3587	. . . . . . . . . . . . . . . . 17
125	122, 124	eqtrd 2484	. . . . . . . . . . . . . . . 16
126	125	imaeq2d 5167	. . . . . . . . . . . . . . 15
127		imaundi 5247	. . . . . . . . . . . . . . 15
128	126, 127	syl6eq 2500	. . . . . . . . . . . . . 14
129		f1ofo 5819	. . . . . . . . . . . . . . 15
130		foima 5796	. . . . . . . . . . . . . . 15
131	1, 129, 130	3syl 18	. . . . . . . . . . . . . 14
132	128, 131	eqtr3d 2486	. . . . . . . . . . . . 13
133	132	fneq2d 5665	. . . . . . . . . . . 12
134	104, 133	mpbid 214	. . . . . . . . . . 11
135	134	adantr 467	. . . . . . . . . 10 $/\$
136		ovex 6316	. . . . . . . . . . 11
137	136	a1i 11	. . . . . . . . . 10 $/\$
138		inidm 3640	. . . . . . . . . 10
139		eqidd 2451	. . . . . . . . . 10 $/\$ $/\$
140	102	adantr 467	. . . . . . . . . . . . 13 $/\$
141		fzss2 11835	. . . . . . . . . . . . . . 15
142		imass2 5203	. . . . . . . . . . . . . . 15
143	119, 141, 142	3syl 18	. . . . . . . . . . . . . 14
144	143	sselda 3431	. . . . . . . . . . . . 13 $/\$
145		fvun2 5935	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
146	88, 91, 145	mp3an12 1353	. . . . . . . . . . . . 13 $/\$
147	140, 144, 146	syl2anc 666	. . . . . . . . . . . 12 $/\$
148	89	fvconst2 6118	. . . . . . . . . . . . 13
149	144, 148	syl 17	. . . . . . . . . . . 12 $/\$
150	147, 149	eqtrd 2484	. . . . . . . . . . 11 $/\$
151	150	adantr 467	. . . . . . . . . 10 $/\$ $/\$
152	85, 135, 137, 137, 138, 139, 151	ofval 6537	. . . . . . . . 9 $/\$ $/\$
153	28, 152	mpdan 673	. . . . . . . 8 $/\$
154	30	zcnd 11038	. . . . . . . . . 10 $/\$
155	154	addid1d 9830	. . . . . . . . 9 $/\$
156	28, 155	syldan 473	. . . . . . . 8 $/\$
157	82, 153, 156	3eqtrd 2488	. . . . . . 7 $/\$
158		breq1 4404	. . . . . . . . . . . . . . 15
159		oveq1 6295	. . . . . . . . . . . . . . 15
160	158, 159	ifbieq2d 3905	. . . . . . . . . . . . . 14
161	41	ltnrd 9766	. . . . . . . . . . . . . . 15
162	161	iffalsed 3891	. . . . . . . . . . . . . 14
163	160, 162	sylan9eqr 2506	. . . . . . . . . . . . 13 $/\$
164	163	csbeq1d 3369	. . . . . . . . . . . 12 $/\$
165		ovex 6316	. . . . . . . . . . . . 13
166		oveq2 6296	. . . . . . . . . . . . . . . . 17
167	166	imaeq2d 5167	. . . . . . . . . . . . . . . 16
168	167	xpeq1d 4856	. . . . . . . . . . . . . . 15
169		oveq1 6295	. . . . . . . . . . . . . . . . . 18
170	169	oveq1d 6303	. . . . . . . . . . . . . . . . 17
171	170	imaeq2d 5167	. . . . . . . . . . . . . . . 16
172	171	xpeq1d 4856	. . . . . . . . . . . . . . 15
173	168, 172	uneq12d 3588	. . . . . . . . . . . . . 14
174	173	oveq2d 6304	. . . . . . . . . . . . 13
175	165, 174	csbie 3388	. . . . . . . . . . . 12
176	164, 175	syl6eq 2500	. . . . . . . . . . 11 $/\$
177		1eluzge0 11199	. . . . . . . . . . . . 13
178		fzss1 11834	. . . . . . . . . . . . 13
179	177, 178	ax-mp 5	. . . . . . . . . . . 12
180	179, 16	sseldi 3429	. . . . . . . . . . 11
181		ovex 6316	. . . . . . . . . . . 12
182	181	a1i 11	. . . . . . . . . . 11
183	35, 176, 180, 182	fvmptd 5952	. . . . . . . . . 10
184	183	fveq1d 5865	. . . . . . . . 9
185	184	adantr 467	. . . . . . . 8 $/\$
186		fnconstg 5769	. . . . . . . . . . . . . . 15
187	86, 186	ax-mp 5	. . . . . . . . . . . . . 14
188		fnconstg 5769	. . . . . . . . . . . . . . 15
189	89, 188	ax-mp 5	. . . . . . . . . . . . . 14
190	187, 189	pm3.2i 457	. . . . . . . . . . . . 13 $/\$
191		imain 5657	. . . . . . . . . . . . . . . 16
192	1, 94, 191	3syl 18	. . . . . . . . . . . . . . 15
193		peano2re 9803	. . . . . . . . . . . . . . . . . . 19
194	41, 193	syl 17	. . . . . . . . . . . . . . . . . 18
195	194	ltp1d 10534	. . . . . . . . . . . . . . . . 17
196		fzdisj 11823	. . . . . . . . . . . . . . . . 17
197	195, 196	syl 17	. . . . . . . . . . . . . . . 16
198	197	imaeq2d 5167	. . . . . . . . . . . . . . 15
199	192, 198	eqtr3d 2486	. . . . . . . . . . . . . 14
200	199, 100	syl6eq 2500	. . . . . . . . . . . . 13
201		fnun 5680	. . . . . . . . . . . . 13 $/\$ $/\$
202	190, 200, 201	sylancr 668	. . . . . . . . . . . 12
203		fzsplit 11822	. . . . . . . . . . . . . . . . 17
204	22, 203	syl 17	. . . . . . . . . . . . . . . 16
205	204	imaeq2d 5167	. . . . . . . . . . . . . . 15
206		imaundi 5247	. . . . . . . . . . . . . . 15
207	205, 206	syl6eq 2500	. . . . . . . . . . . . . 14
208	207, 131	eqtr3d 2486	. . . . . . . . . . . . 13
209	208	fneq2d 5665	. . . . . . . . . . . 12
210	202, 209	mpbid 214	. . . . . . . . . . 11
211	210	adantr 467	. . . . . . . . . 10 $/\$
212	200	adantr 467	. . . . . . . . . . . . 13 $/\$
213		fzss1 11834	. . . . . . . . . . . . . . 15
214		imass2 5203	. . . . . . . . . . . . . . 15
215	106, 213, 214	3syl 18	. . . . . . . . . . . . . 14
216	215	sselda 3431	. . . . . . . . . . . . 13 $/\$
217		fvun1 5934	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
218	187, 189, 217	mp3an12 1353	. . . . . . . . . . . . 13 $/\$
219	212, 216, 218	syl2anc 666	. . . . . . . . . . . 12 $/\$
220	86	fvconst2 6118	. . . . . . . . . . . . 13
221	216, 220	syl 17	. . . . . . . . . . . 12 $/\$
222	219, 221	eqtrd 2484	. . . . . . . . . . 11 $/\$
223	222	adantr 467	. . . . . . . . . 10 $/\$ $/\$
224	85, 211, 137, 137, 138, 139, 223	ofval 6537	. . . . . . . . 9 $/\$ $/\$
225	28, 224	mpdan 673	. . . . . . . 8 $/\$
226	185, 225	eqtrd 2484	. . . . . . 7 $/\$
227	34, 157, 226	3netr4d 2700	. . . . . 6 $/\$
228	227	ralrimiva 2801	. . . . 5
229		fzpr 11848	. . . . . . . . 9
230	16, 39, 229	3syl 18	. . . . . . . 8
231	230	imaeq2d 5167	. . . . . . 7
232		f1ofn 5813	. . . . . . . . 9
233	1, 232	syl 17	. . . . . . . 8
234		fnimapr 5927	. . . . . . . 8 $/\$ $/\$
235	233, 17, 22, 234	syl3anc 1267	. . . . . . 7
236	231, 235	eqtrd 2484	. . . . . 6
237	236	raleqdv 2992	. . . . 5
238	228, 237	mpbid 214	. . . 4
239		fvex 5873	. . . . 5
240		fvex 5873	. . . . 5
241		fveq2 5863	. . . . . 6
242		fveq2 5863	. . . . . 6
243	241, 242	neeq12d 2684	. . . . 5
244		fveq2 5863	. . . . . 6
245		fveq2 5863	. . . . . 6
246	244, 245	neeq12d 2684	. . . . 5
247	239, 240, 243, 246	ralpr 4024	. . . 4 $/\$
248	238, 247	sylib 200	. . 3 $/\$
249	41	ltp1d 10534	. . . . 5
250	41, 249	ltned 9768	. . . 4
251		f1of1 5811	. . . . . . 7
252	1, 251	syl 17	. . . . . 6
253		f1veqaeq 6159	. . . . . 6 $/\$ $/\$
254	252, 17, 22, 253	syl12anc 1265	. . . . 5
255	254	necon3d 2644	. . . 4
256	250, 255	mpd 15	. . 3
257	243	anbi1d 710	. . . . 5 $/\$ $/\$
258		neeq1 2685	. . . . 5
259	257, 258	anbi12d 716	. . . 4 $/\$ $/\$ $/\$ $/\$
260		fveq2 5863	. . . . . . 7
261		fveq2 5863	. . . . . . 7
262	260, 261	neeq12d 2684	. . . . . 6
263	262	anbi2d 709	. . . . 5 $/\$ $/\$
264		neeq2 2686	. . . . 5
265	263, 264	anbi12d 716	. . . 4 $/\$ $/\$ $/\$ $/\$
266	259, 265	rspc2ev 3160	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
267	18, 23, 248, 256, 266	syl112anc 1271	. 2 $/\$ $/\$
268		dfrex2 2837	. . 3 $/\$ $/\$ $/\$ $/\$
269		fveq2 5863	. . . . . 6
270		fveq2 5863	. . . . . 6
271	269, 270	neeq12d 2684	. . . . 5
272	271	rmo4 3230	. . . 4 $/\$
273		dfral2 2834	. . . . . 6 $/\$ $/\$
274		df-ne 2623	. . . . . . . . 9
275	274	anbi2i 699	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
276		annim 427	. . . . . . . 8 $/\$ $/\$ $/\$
277	275, 276	bitri 253	. . . . . . 7 $/\$ $/\$ $/\$
278	277	rexbii 2888	. . . . . 6 $/\$ $/\$ $/\$
279	273, 278	xchbinxr 313	. . . . 5 $/\$ $/\$ $/\$
280	279	ralbii 2818	. . . 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 1443

wcel 1886

wne 2621

wral 2736

wrex 2737

wrmo 2739

cvv 3044

csb 3362

cun 3401

cin 3402

wss 3403

c0 3730

cif 3880

csn 3967

cpr 3969 class class class wbr 4401

cmpt 4460

cxp 4831

ccnv 4832

crn 4834

cima 4836

wfun 5575

wfn 5576

wf 5577

wf1 5578

wfo 5579

wf1o 5580

cfv 5581 (class class class)co 6288

cof 6526

cc 9534

cr 9535

cc0 9536

c1 9537

caddc 9539

clt 9672

cmin 9857

cn 10606

cz 10934

cuz 11156

cfz 11781

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1668 ax-4 1681 ax-5 1757 ax-6 1804 ax-7 1850 ax-8 1888 ax-9 1895 ax-10 1914 ax-11 1919 ax-12 1932 ax-13 2090 ax-ext 2430 ax-rep 4514 ax-sep 4524 ax-nul 4533 ax-pow 4580 ax-pr 4638 ax-un 6580 ax-cnex 9592 ax-resscn 9593 ax-1cn 9594 ax-icn 9595 ax-addcl 9596 ax-addrcl 9597 ax-mulcl 9598 ax-mulrcl 9599 ax-mulcom 9600 ax-addass 9601 ax-mulass 9602 ax-distr 9603 ax-i2m1 9604 ax-1ne0 9605 ax-1rid 9606 ax-rnegex 9607 ax-rrecex 9608 ax-cnre 9609 ax-pre-lttri 9610 ax-pre-lttrn 9611 ax-pre-ltadd 9612 ax-pre-mulgt0 9613

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 985 df-3an 986 df-tru 1446 df-ex 1663 df-nf 1667 df-sb 1797 df-eu 2302 df-mo 2303 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2580 df-ne 2623 df-nel 2624 df-ral 2741 df-rex 2742 df-reu 2743 df-rmo 2744 df-rab 2745 df-v 3046 df-sbc 3267 df-csb 3363 df-dif 3406 df-un 3408 df-in 3410 df-ss 3417 df-pss 3419 df-nul 3731 df-if 3881 df-pw 3952 df-sn 3968 df-pr 3970 df-tp 3972 df-op 3974 df-uni 4198 df-iun 4279 df-br 4402 df-opab 4461 df-mpt 4462 df-tr 4497 df-eprel 4744 df-id 4748 df-po 4754 df-so 4755 df-fr 4792 df-we 4794 df-xp 4839 df-rel 4840 df-cnv 4841 df-co 4842 df-dm 4843 df-rn 4844 df-res 4845 df-ima 4846 df-pred 5379 df-ord 5425 df-on 5426 df-lim 5427 df-suc 5428 df-iota 5545 df-fun 5583 df-fn 5584 df-f 5585 df-f1 5586 df-fo 5587 df-f1o 5588 df-fv 5589 df-riota 6250 df-ov 6291 df-oprab 6292 df-mpt2 6293 df-of 6528 df-om 6690 df-1st 6790 df-2nd 6791 df-wrecs 7025 df-recs 7087 df-rdg 7125 df-er 7360 df-en 7567 df-dom 7568 df-sdom 7569 df-pnf 9674 df-mnf 9675 df-xr 9676 df-ltxr 9677 df-le 9678 df-sub 9859 df-neg 9860 df-nn 10607 df-n0 10867 df-z 10935 df-uz 11157 df-fz 11782

This theorem is referenced by: poimirlem8 31941 poimirlem18 31951 poimirlem21 31954 poimirlem22 31955

W3C validator