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 32005

Description: Lemma for poimir 32037- 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 5828	. . . . 5
3	1, 2	syl 17	. . . 4
4		poimir.0	. . . . . . . . 9
5	4	nncnd 10647	. . . . . . . 8
6		npcan1 10065	. . . . . . . 8
7	5, 6	syl 17	. . . . . . 7
8	4	nnzd 11062	. . . . . . . 8
9		peano2zm 11004	. . . . . . . 8
10		uzid 11197	. . . . . . . 8
11		peano2uz 11235	. . . . . . . 8
12	8, 9, 10, 11	4syl 19	. . . . . . 7
13	7, 12	eqeltrrd 2550	. . . . . 6
14		fzss2 11864	. . . . . 6
15	13, 14	syl 17	. . . . 5
16		poimirlem1.4	. . . . 5
17	15, 16	sseldd 3419	. . . 4
18	3, 17	ffvelrnd 6038	. . 3
19		fzp1elp1 11875	. . . . . 6
20	16, 19	syl 17	. . . . 5
21	7	oveq2d 6324	. . . . 5
22	20, 21	eleqtrd 2551	. . . 4
23	3, 22	ffvelrnd 6038	. . 3
24		imassrn 5185	. . . . . . . . . 10
25		frn 5747	. . . . . . . . . . 11
26	1, 2, 25	3syl 18	. . . . . . . . . 10
27	24, 26	syl5ss 3429	. . . . . . . . 9
28	27	sselda 3418	. . . . . . . 8 $/\$
29		poimirlem2.2	. . . . . . . . . . 11
30	29	ffvelrnda 6037	. . . . . . . . . 10 $/\$
31	30	zred 11063	. . . . . . . . 9 $/\$
32	31	ltp1d 10559	. . . . . . . . 9 $/\$
33	31, 32	ltned 9788	. . . . . . . 8 $/\$
34	28, 33	syldan 478	. . . . . . 7 $/\$
35		poimirlem2.1	. . . . . . . . . . 11
36		breq1 4398	. . . . . . . . . . . . . . 15
37		id 22	. . . . . . . . . . . . . . 15
38	36, 37	ifbieq1d 3895	. . . . . . . . . . . . . 14
39		elfzelz 11826	. . . . . . . . . . . . . . . . . 18
40	16, 39	syl 17	. . . . . . . . . . . . . . . . 17
41	40	zred 11063	. . . . . . . . . . . . . . . 16
42	41	ltm1d 10561	. . . . . . . . . . . . . . 15
43	42	iftrued 3880	. . . . . . . . . . . . . 14
44	38, 43	sylan9eqr 2527	. . . . . . . . . . . . 13 $/\$
45	44	csbeq1d 3356	. . . . . . . . . . . 12 $/\$
46	8, 9	syl 17	. . . . . . . . . . . . . . . 16
47		elfzm1b 11898	. . . . . . . . . . . . . . . 16 $/\$
48	40, 46, 47	syl2anc 673	. . . . . . . . . . . . . . 15
49	16, 48	mpbid 215	. . . . . . . . . . . . . 14
50		oveq2 6316	. . . . . . . . . . . . . . . . . . 19
51	50	imaeq2d 5174	. . . . . . . . . . . . . . . . . 18
52	51	xpeq1d 4862	. . . . . . . . . . . . . . . . 17
53	52	adantl 473	. . . . . . . . . . . . . . . 16 $/\$
54		oveq1 6315	. . . . . . . . . . . . . . . . . . . 20
55	40	zcnd 11064	. . . . . . . . . . . . . . . . . . . . 21
56		npcan1 10065	. . . . . . . . . . . . . . . . . . . . 21
57	55, 56	syl 17	. . . . . . . . . . . . . . . . . . . 20
58	54, 57	sylan9eqr 2527	. . . . . . . . . . . . . . . . . . 19 $/\$
59	58	oveq1d 6323	. . . . . . . . . . . . . . . . . 18 $/\$
60	59	imaeq2d 5174	. . . . . . . . . . . . . . . . 17 $/\$
61	60	xpeq1d 4862	. . . . . . . . . . . . . . . 16 $/\$
62	53, 61	uneq12d 3580	. . . . . . . . . . . . . . 15 $/\$
63	62	oveq2d 6324	. . . . . . . . . . . . . 14 $/\$
64	49, 63	csbied 3376	. . . . . . . . . . . . 13
65	64	adantr 472	. . . . . . . . . . . 12 $/\$
66	45, 65	eqtrd 2505	. . . . . . . . . . 11 $/\$
67	46	zcnd 11064	. . . . . . . . . . . . . . 15
68		npcan1 10065	. . . . . . . . . . . . . . 15
69	67, 68	syl 17	. . . . . . . . . . . . . 14
70		peano2zm 11004	. . . . . . . . . . . . . . 15
71		uzid 11197	. . . . . . . . . . . . . . 15
72		peano2uz 11235	. . . . . . . . . . . . . . 15
73	46, 70, 71, 72	4syl 19	. . . . . . . . . . . . . 14
74	69, 73	eqeltrrd 2550	. . . . . . . . . . . . 13
75		fzss2 11864	. . . . . . . . . . . . 13
76	74, 75	syl 17	. . . . . . . . . . . 12
77	76, 49	sseldd 3419	. . . . . . . . . . 11
78		ovex 6336	. . . . . . . . . . . 12
79	78	a1i 11	. . . . . . . . . . 11
80	35, 66, 77, 79	fvmptd 5969	. . . . . . . . . 10
81	80	fveq1d 5881	. . . . . . . . 9
82	81	adantr 472	. . . . . . . 8 $/\$
83		ffn 5739	. . . . . . . . . . . 12
84	29, 83	syl 17	. . . . . . . . . . 11
85	84	adantr 472	. . . . . . . . . 10 $/\$
86		1ex 9656	. . . . . . . . . . . . . . 15
87		fnconstg 5784	. . . . . . . . . . . . . . 15
88	86, 87	ax-mp 5	. . . . . . . . . . . . . 14
89		c0ex 9655	. . . . . . . . . . . . . . 15
90		fnconstg 5784	. . . . . . . . . . . . . . 15
91	89, 90	ax-mp 5	. . . . . . . . . . . . . 14
92	88, 91	pm3.2i 462	. . . . . . . . . . . . 13 $/\$
93		dff1o3 5834	. . . . . . . . . . . . . . . 16 $/\$
94	93	simprbi 471	. . . . . . . . . . . . . . 15
95		imain 5669	. . . . . . . . . . . . . . 15
96	1, 94, 95	3syl 18	. . . . . . . . . . . . . 14
97		fzdisj 11852	. . . . . . . . . . . . . . . . 17
98	42, 97	syl 17	. . . . . . . . . . . . . . . 16
99	98	imaeq2d 5174	. . . . . . . . . . . . . . 15
100		ima0 5189	. . . . . . . . . . . . . . 15
101	99, 100	syl6eq 2521	. . . . . . . . . . . . . 14
102	96, 101	eqtr3d 2507	. . . . . . . . . . . . 13
103		fnun 5692	. . . . . . . . . . . . 13 $/\$ $/\$
104	92, 102, 103	sylancr 676	. . . . . . . . . . . 12
105		elfzuz 11822	. . . . . . . . . . . . . . . . . . . 20
106	16, 105	syl 17	. . . . . . . . . . . . . . . . . . 19
107	57, 106	eqeltrd 2549	. . . . . . . . . . . . . . . . . 18
108		peano2zm 11004	. . . . . . . . . . . . . . . . . . . . . 22
109		uzid 11197	. . . . . . . . . . . . . . . . . . . . . 22
110		peano2uz 11235	. . . . . . . . . . . . . . . . . . . . . 22
111	40, 108, 109, 110	4syl 19	. . . . . . . . . . . . . . . . . . . . 21
112	57, 111	eqeltrrd 2550	. . . . . . . . . . . . . . . . . . . 20
113		peano2uz 11235	. . . . . . . . . . . . . . . . . . . 20
114		uzss 11203	. . . . . . . . . . . . . . . . . . . 20
115	112, 113, 114	3syl 18	. . . . . . . . . . . . . . . . . . 19
116		elfzuz3 11823	. . . . . . . . . . . . . . . . . . . . 21
117		eluzp1p1 11208	. . . . . . . . . . . . . . . . . . . . 21
118	16, 116, 117	3syl 18	. . . . . . . . . . . . . . . . . . . 20
119	7, 118	eqeltrrd 2550	. . . . . . . . . . . . . . . . . . 19
120	115, 119	sseldd 3419	. . . . . . . . . . . . . . . . . 18
121		fzsplit2 11850	. . . . . . . . . . . . . . . . . 18 $/\$
122	107, 120, 121	syl2anc 673	. . . . . . . . . . . . . . . . 17
123	57	oveq1d 6323	. . . . . . . . . . . . . . . . . 18
124	123	uneq2d 3579	. . . . . . . . . . . . . . . . 17
125	122, 124	eqtrd 2505	. . . . . . . . . . . . . . . 16
126	125	imaeq2d 5174	. . . . . . . . . . . . . . 15
127		imaundi 5254	. . . . . . . . . . . . . . 15
128	126, 127	syl6eq 2521	. . . . . . . . . . . . . 14
129		f1ofo 5835	. . . . . . . . . . . . . . 15
130		foima 5811	. . . . . . . . . . . . . . 15
131	1, 129, 130	3syl 18	. . . . . . . . . . . . . 14
132	128, 131	eqtr3d 2507	. . . . . . . . . . . . 13
133	132	fneq2d 5677	. . . . . . . . . . . 12
134	104, 133	mpbid 215	. . . . . . . . . . 11
135	134	adantr 472	. . . . . . . . . 10 $/\$
136		ovex 6336	. . . . . . . . . . 11
137	136	a1i 11	. . . . . . . . . 10 $/\$
138		inidm 3632	. . . . . . . . . 10
139		eqidd 2472	. . . . . . . . . 10 $/\$ $/\$
140	102	adantr 472	. . . . . . . . . . . . 13 $/\$
141		fzss2 11864	. . . . . . . . . . . . . . 15
142		imass2 5210	. . . . . . . . . . . . . . 15
143	119, 141, 142	3syl 18	. . . . . . . . . . . . . 14
144	143	sselda 3418	. . . . . . . . . . . . 13 $/\$
145		fvun2 5952	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
146	88, 91, 145	mp3an12 1380	. . . . . . . . . . . . 13 $/\$
147	140, 144, 146	syl2anc 673	. . . . . . . . . . . 12 $/\$
148	89	fvconst2 6136	. . . . . . . . . . . . 13
149	144, 148	syl 17	. . . . . . . . . . . 12 $/\$
150	147, 149	eqtrd 2505	. . . . . . . . . . 11 $/\$
151	150	adantr 472	. . . . . . . . . 10 $/\$ $/\$
152	85, 135, 137, 137, 138, 139, 151	ofval 6559	. . . . . . . . 9 $/\$ $/\$
153	28, 152	mpdan 681	. . . . . . . 8 $/\$
154	30	zcnd 11064	. . . . . . . . . 10 $/\$
155	154	addid1d 9851	. . . . . . . . 9 $/\$
156	28, 155	syldan 478	. . . . . . . 8 $/\$
157	82, 153, 156	3eqtrd 2509	. . . . . . 7 $/\$
158		breq1 4398	. . . . . . . . . . . . . . 15
159		oveq1 6315	. . . . . . . . . . . . . . 15
160	158, 159	ifbieq2d 3897	. . . . . . . . . . . . . 14
161	41	ltnrd 9786	. . . . . . . . . . . . . . 15
162	161	iffalsed 3883	. . . . . . . . . . . . . 14
163	160, 162	sylan9eqr 2527	. . . . . . . . . . . . 13 $/\$
164	163	csbeq1d 3356	. . . . . . . . . . . 12 $/\$
165		ovex 6336	. . . . . . . . . . . . 13
166		oveq2 6316	. . . . . . . . . . . . . . . . 17
167	166	imaeq2d 5174	. . . . . . . . . . . . . . . 16
168	167	xpeq1d 4862	. . . . . . . . . . . . . . 15
169		oveq1 6315	. . . . . . . . . . . . . . . . . 18
170	169	oveq1d 6323	. . . . . . . . . . . . . . . . 17
171	170	imaeq2d 5174	. . . . . . . . . . . . . . . 16
172	171	xpeq1d 4862	. . . . . . . . . . . . . . 15
173	168, 172	uneq12d 3580	. . . . . . . . . . . . . 14
174	173	oveq2d 6324	. . . . . . . . . . . . 13
175	165, 174	csbie 3375	. . . . . . . . . . . 12
176	164, 175	syl6eq 2521	. . . . . . . . . . 11 $/\$
177		1eluzge0 11226	. . . . . . . . . . . . 13
178		fzss1 11863	. . . . . . . . . . . . 13
179	177, 178	ax-mp 5	. . . . . . . . . . . 12
180	179, 16	sseldi 3416	. . . . . . . . . . 11
181		ovex 6336	. . . . . . . . . . . 12
182	181	a1i 11	. . . . . . . . . . 11
183	35, 176, 180, 182	fvmptd 5969	. . . . . . . . . 10
184	183	fveq1d 5881	. . . . . . . . 9
185	184	adantr 472	. . . . . . . 8 $/\$
186		fnconstg 5784	. . . . . . . . . . . . . . 15
187	86, 186	ax-mp 5	. . . . . . . . . . . . . 14
188		fnconstg 5784	. . . . . . . . . . . . . . 15
189	89, 188	ax-mp 5	. . . . . . . . . . . . . 14
190	187, 189	pm3.2i 462	. . . . . . . . . . . . 13 $/\$
191		imain 5669	. . . . . . . . . . . . . . . 16
192	1, 94, 191	3syl 18	. . . . . . . . . . . . . . 15
193		peano2re 9824	. . . . . . . . . . . . . . . . . . 19
194	41, 193	syl 17	. . . . . . . . . . . . . . . . . 18
195	194	ltp1d 10559	. . . . . . . . . . . . . . . . 17
196		fzdisj 11852	. . . . . . . . . . . . . . . . 17
197	195, 196	syl 17	. . . . . . . . . . . . . . . 16
198	197	imaeq2d 5174	. . . . . . . . . . . . . . 15
199	192, 198	eqtr3d 2507	. . . . . . . . . . . . . 14
200	199, 100	syl6eq 2521	. . . . . . . . . . . . 13
201		fnun 5692	. . . . . . . . . . . . 13 $/\$ $/\$
202	190, 200, 201	sylancr 676	. . . . . . . . . . . 12
203		fzsplit 11851	. . . . . . . . . . . . . . . . 17
204	22, 203	syl 17	. . . . . . . . . . . . . . . 16
205	204	imaeq2d 5174	. . . . . . . . . . . . . . 15
206		imaundi 5254	. . . . . . . . . . . . . . 15
207	205, 206	syl6eq 2521	. . . . . . . . . . . . . 14
208	207, 131	eqtr3d 2507	. . . . . . . . . . . . 13
209	208	fneq2d 5677	. . . . . . . . . . . 12
210	202, 209	mpbid 215	. . . . . . . . . . 11
211	210	adantr 472	. . . . . . . . . 10 $/\$
212	200	adantr 472	. . . . . . . . . . . . 13 $/\$
213		fzss1 11863	. . . . . . . . . . . . . . 15
214		imass2 5210	. . . . . . . . . . . . . . 15
215	106, 213, 214	3syl 18	. . . . . . . . . . . . . 14
216	215	sselda 3418	. . . . . . . . . . . . 13 $/\$
217		fvun1 5951	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
218	187, 189, 217	mp3an12 1380	. . . . . . . . . . . . 13 $/\$
219	212, 216, 218	syl2anc 673	. . . . . . . . . . . 12 $/\$
220	86	fvconst2 6136	. . . . . . . . . . . . 13
221	216, 220	syl 17	. . . . . . . . . . . 12 $/\$
222	219, 221	eqtrd 2505	. . . . . . . . . . 11 $/\$
223	222	adantr 472	. . . . . . . . . 10 $/\$ $/\$
224	85, 211, 137, 137, 138, 139, 223	ofval 6559	. . . . . . . . 9 $/\$ $/\$
225	28, 224	mpdan 681	. . . . . . . 8 $/\$
226	185, 225	eqtrd 2505	. . . . . . 7 $/\$
227	34, 157, 226	3netr4d 2720	. . . . . 6 $/\$
228	227	ralrimiva 2809	. . . . 5
229		fzpr 11877	. . . . . . . . 9
230	16, 39, 229	3syl 18	. . . . . . . 8
231	230	imaeq2d 5174	. . . . . . 7
232		f1ofn 5829	. . . . . . . . 9
233	1, 232	syl 17	. . . . . . . 8
234		fnimapr 5944	. . . . . . . 8 $/\$ $/\$
235	233, 17, 22, 234	syl3anc 1292	. . . . . . 7
236	231, 235	eqtrd 2505	. . . . . 6
237	236	raleqdv 2979	. . . . 5
238	228, 237	mpbid 215	. . . 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 4016	. . . 4 $/\$
248	238, 247	sylib 201	. . 3 $/\$
249	41	ltp1d 10559	. . . . 5
250	41, 249	ltned 9788	. . . 4
251		f1of1 5827	. . . . . . 7
252	1, 251	syl 17	. . . . . 6
253		f1veqaeq 6179	. . . . . 6 $/\$ $/\$
254	252, 17, 22, 253	syl12anc 1290	. . . . 5
255	254	necon3d 2664	. . . 4
256	250, 255	mpd 15	. . 3
257	243	anbi1d 719	. . . . 5 $/\$ $/\$
258		neeq1 2705	. . . . 5
259	257, 258	anbi12d 725	. . . 4 $/\$ $/\$ $/\$ $/\$
260		fveq2 5879	. . . . . . 7
261		fveq2 5879	. . . . . . 7
262	260, 261	neeq12d 2704	. . . . . 6
263	262	anbi2d 718	. . . . 5 $/\$ $/\$
264		neeq2 2706	. . . . 5
265	263, 264	anbi12d 725	. . . 4 $/\$ $/\$ $/\$ $/\$
266	259, 265	rspc2ev 3149	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
267	18, 23, 248, 256, 266	syl112anc 1296	. 2 $/\$ $/\$
268		dfrex2 2837	. . 3 $/\$ $/\$ $/\$ $/\$
269		fveq2 5879	. . . . . 6
270		fveq2 5879	. . . . . 6
271	269, 270	neeq12d 2704	. . . . 5
272	271	rmo4 3219	. . . 4 $/\$
273		dfral2 2835	. . . . . 6 $/\$ $/\$
274		df-ne 2643	. . . . . . . . 9
275	274	anbi2i 708	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
276		annim 432	. . . . . . . 8 $/\$ $/\$ $/\$
277	275, 276	bitri 257	. . . . . . 7 $/\$ $/\$ $/\$
278	277	rexbii 2881	. . . . . 6 $/\$ $/\$ $/\$
279	273, 278	xchbinxr 318	. . . . 5 $/\$ $/\$ $/\$
280	279	ralbii 2823	. . . 4 $/\$ $/\$ $/\$
281	272, 280	bitri 257	. . 3 $/\$ $/\$
282	268, 281	xchbinxr 318	. 2 $/\$ $/\$
283	267, 282	sylib 201	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 189 $/\$ wa 376

wceq 1452

wcel 1904

wne 2641

wral 2756

wrex 2757

wrmo 2759

cvv 3031

csb 3349

cun 3388

cin 3389

wss 3390

c0 3722

cif 3872

csn 3959

cpr 3961 class class class wbr 4395

cmpt 4454

cxp 4837

ccnv 4838

crn 4840

cima 4842

wfun 5583

wfn 5584

wf 5585

wf1 5586

wfo 5587

wf1o 5588

cfv 5589 (class class class)co 6308

cof 6548

cc 9555

cr 9556

cc0 9557

c1 9558

caddc 9560

clt 9693

cmin 9880

cn 10631

cz 10961

cuz 11182

cfz 11810

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-rep 4508 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-cnex 9613 ax-resscn 9614 ax-1cn 9615 ax-icn 9616 ax-addcl 9617 ax-addrcl 9618 ax-mulcl 9619 ax-mulrcl 9620 ax-mulcom 9621 ax-addass 9622 ax-mulass 9623 ax-distr 9624 ax-i2m1 9625 ax-1ne0 9626 ax-1rid 9627 ax-rnegex 9628 ax-rrecex 9629 ax-cnre 9630 ax-pre-lttri 9631 ax-pre-lttrn 9632 ax-pre-ltadd 9633 ax-pre-mulgt0 9634

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-nel 2644 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-iun 4271 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-of 6550 df-om 6712 df-1st 6812 df-2nd 6813 df-wrecs 7046 df-recs 7108 df-rdg 7146 df-er 7381 df-en 7588 df-dom 7589 df-sdom 7590 df-pnf 9695 df-mnf 9696 df-xr 9697 df-ltxr 9698 df-le 9699 df-sub 9882 df-neg 9883 df-nn 10632 df-n0 10894 df-z 10962 df-uz 11183 df-fz 11811

This theorem is referenced by: poimirlem8 32012 poimirlem18 32022 poimirlem21 32025 poimirlem22 32026

W3C validator