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 33410

Description: Lemma for poimir 33442- 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 6137	. . . . 5
3	1, 2	syl 17	. . . 4
4		poimir.0	. . . . . . . . 9
5	4	nncnd 11036	. . . . . . . 8
6		npcan1 10455	. . . . . . . 8
7	5, 6	syl 17	. . . . . . 7
8	4	nnzd 11481	. . . . . . . 8
9		peano2zm 11420	. . . . . . . 8
10		uzid 11702	. . . . . . . 8
11		peano2uz 11741	. . . . . . . 8
12	8, 9, 10, 11	4syl 19	. . . . . . 7
13	7, 12	eqeltrrd 2702	. . . . . 6
14		fzss2 12381	. . . . . 6
15	13, 14	syl 17	. . . . 5
16		poimirlem1.4	. . . . 5
17	15, 16	sseldd 3604	. . . 4
18	3, 17	ffvelrnd 6360	. . 3
19		fzp1elp1 12394	. . . . . 6
20	16, 19	syl 17	. . . . 5
21	7	oveq2d 6666	. . . . 5
22	20, 21	eleqtrd 2703	. . . 4
23	3, 22	ffvelrnd 6360	. . 3
24		imassrn 5477	. . . . . . . . . 10
25		frn 6053	. . . . . . . . . . 11
26	1, 2, 25	3syl 18	. . . . . . . . . 10
27	24, 26	syl5ss 3614	. . . . . . . . 9
28	27	sselda 3603	. . . . . . . 8 $/\$
29		poimirlem2.2	. . . . . . . . . . 11
30	29	ffvelrnda 6359	. . . . . . . . . 10 $/\$
31	30	zred 11482	. . . . . . . . 9 $/\$
32	31	ltp1d 10954	. . . . . . . . 9 $/\$
33	31, 32	ltned 10173	. . . . . . . 8 $/\$
34	28, 33	syldan 487	. . . . . . 7 $/\$
35		poimirlem2.1	. . . . . . . . . . 11
36		breq1 4656	. . . . . . . . . . . . . . 15
37		id 22	. . . . . . . . . . . . . . 15
38	36, 37	ifbieq1d 4109	. . . . . . . . . . . . . 14
39		elfzelz 12342	. . . . . . . . . . . . . . . . . 18
40	16, 39	syl 17	. . . . . . . . . . . . . . . . 17
41	40	zred 11482	. . . . . . . . . . . . . . . 16
42	41	ltm1d 10956	. . . . . . . . . . . . . . 15
43	42	iftrued 4094	. . . . . . . . . . . . . 14
44	38, 43	sylan9eqr 2678	. . . . . . . . . . . . 13 $/\$
45	44	csbeq1d 3540	. . . . . . . . . . . 12 $/\$
46	8, 9	syl 17	. . . . . . . . . . . . . . . 16
47		elfzm1b 12418	. . . . . . . . . . . . . . . 16 $/\$
48	40, 46, 47	syl2anc 693	. . . . . . . . . . . . . . 15
49	16, 48	mpbid 222	. . . . . . . . . . . . . 14
50		oveq2 6658	. . . . . . . . . . . . . . . . . . 19
51	50	imaeq2d 5466	. . . . . . . . . . . . . . . . . 18
52	51	xpeq1d 5138	. . . . . . . . . . . . . . . . 17
53	52	adantl 482	. . . . . . . . . . . . . . . 16 $/\$
54		oveq1 6657	. . . . . . . . . . . . . . . . . . . 20
55	40	zcnd 11483	. . . . . . . . . . . . . . . . . . . . 21
56		npcan1 10455	. . . . . . . . . . . . . . . . . . . . 21
57	55, 56	syl 17	. . . . . . . . . . . . . . . . . . . 20
58	54, 57	sylan9eqr 2678	. . . . . . . . . . . . . . . . . . 19 $/\$
59	58	oveq1d 6665	. . . . . . . . . . . . . . . . . 18 $/\$
60	59	imaeq2d 5466	. . . . . . . . . . . . . . . . 17 $/\$
61	60	xpeq1d 5138	. . . . . . . . . . . . . . . 16 $/\$
62	53, 61	uneq12d 3768	. . . . . . . . . . . . . . 15 $/\$
63	62	oveq2d 6666	. . . . . . . . . . . . . 14 $/\$
64	49, 63	csbied 3560	. . . . . . . . . . . . 13
65	64	adantr 481	. . . . . . . . . . . 12 $/\$
66	45, 65	eqtrd 2656	. . . . . . . . . . 11 $/\$
67	46	zcnd 11483	. . . . . . . . . . . . . . 15
68		npcan1 10455	. . . . . . . . . . . . . . 15
69	67, 68	syl 17	. . . . . . . . . . . . . 14
70		peano2zm 11420	. . . . . . . . . . . . . . 15
71		uzid 11702	. . . . . . . . . . . . . . 15
72		peano2uz 11741	. . . . . . . . . . . . . . 15
73	46, 70, 71, 72	4syl 19	. . . . . . . . . . . . . 14
74	69, 73	eqeltrrd 2702	. . . . . . . . . . . . 13
75		fzss2 12381	. . . . . . . . . . . . 13
76	74, 75	syl 17	. . . . . . . . . . . 12
77	76, 49	sseldd 3604	. . . . . . . . . . 11
78		ovexd 6680	. . . . . . . . . . 11
79	35, 66, 77, 78	fvmptd 6288	. . . . . . . . . 10
80	79	fveq1d 6193	. . . . . . . . 9
81	80	adantr 481	. . . . . . . 8 $/\$
82		ffn 6045	. . . . . . . . . . . 12
83	29, 82	syl 17	. . . . . . . . . . 11
84	83	adantr 481	. . . . . . . . . 10 $/\$
85		1ex 10035	. . . . . . . . . . . . . . 15
86		fnconstg 6093	. . . . . . . . . . . . . . 15
87	85, 86	ax-mp 5	. . . . . . . . . . . . . 14
88		c0ex 10034	. . . . . . . . . . . . . . 15
89		fnconstg 6093	. . . . . . . . . . . . . . 15
90	88, 89	ax-mp 5	. . . . . . . . . . . . . 14
91	87, 90	pm3.2i 471	. . . . . . . . . . . . 13 $/\$
92		dff1o3 6143	. . . . . . . . . . . . . . . 16 $/\$
93	92	simprbi 480	. . . . . . . . . . . . . . 15
94		imain 5974	. . . . . . . . . . . . . . 15
95	1, 93, 94	3syl 18	. . . . . . . . . . . . . 14
96		fzdisj 12368	. . . . . . . . . . . . . . . . 17
97	42, 96	syl 17	. . . . . . . . . . . . . . . 16
98	97	imaeq2d 5466	. . . . . . . . . . . . . . 15
99		ima0 5481	. . . . . . . . . . . . . . 15
100	98, 99	syl6eq 2672	. . . . . . . . . . . . . 14
101	95, 100	eqtr3d 2658	. . . . . . . . . . . . 13
102		fnun 5997	. . . . . . . . . . . . 13 $/\$ $/\$
103	91, 101, 102	sylancr 695	. . . . . . . . . . . 12
104		elfzuz 12338	. . . . . . . . . . . . . . . . . . . 20
105	16, 104	syl 17	. . . . . . . . . . . . . . . . . . 19
106	57, 105	eqeltrd 2701	. . . . . . . . . . . . . . . . . 18
107		peano2zm 11420	. . . . . . . . . . . . . . . . . . . . . 22
108		uzid 11702	. . . . . . . . . . . . . . . . . . . . . 22
109		peano2uz 11741	. . . . . . . . . . . . . . . . . . . . . 22
110	40, 107, 108, 109	4syl 19	. . . . . . . . . . . . . . . . . . . . 21
111	57, 110	eqeltrrd 2702	. . . . . . . . . . . . . . . . . . . 20
112		peano2uz 11741	. . . . . . . . . . . . . . . . . . . 20
113		uzss 11708	. . . . . . . . . . . . . . . . . . . 20
114	111, 112, 113	3syl 18	. . . . . . . . . . . . . . . . . . 19
115		elfzuz3 12339	. . . . . . . . . . . . . . . . . . . . 21
116		eluzp1p1 11713	. . . . . . . . . . . . . . . . . . . . 21
117	16, 115, 116	3syl 18	. . . . . . . . . . . . . . . . . . . 20
118	7, 117	eqeltrrd 2702	. . . . . . . . . . . . . . . . . . 19
119	114, 118	sseldd 3604	. . . . . . . . . . . . . . . . . 18
120		fzsplit2 12366	. . . . . . . . . . . . . . . . . 18 $/\$
121	106, 119, 120	syl2anc 693	. . . . . . . . . . . . . . . . 17
122	57	oveq1d 6665	. . . . . . . . . . . . . . . . . 18
123	122	uneq2d 3767	. . . . . . . . . . . . . . . . 17
124	121, 123	eqtrd 2656	. . . . . . . . . . . . . . . 16
125	124	imaeq2d 5466	. . . . . . . . . . . . . . 15
126		imaundi 5545	. . . . . . . . . . . . . . 15
127	125, 126	syl6eq 2672	. . . . . . . . . . . . . 14
128		f1ofo 6144	. . . . . . . . . . . . . . 15
129		foima 6120	. . . . . . . . . . . . . . 15
130	1, 128, 129	3syl 18	. . . . . . . . . . . . . 14
131	127, 130	eqtr3d 2658	. . . . . . . . . . . . 13
132	131	fneq2d 5982	. . . . . . . . . . . 12
133	103, 132	mpbid 222	. . . . . . . . . . 11
134	133	adantr 481	. . . . . . . . . 10 $/\$
135		ovexd 6680	. . . . . . . . . 10 $/\$
136		inidm 3822	. . . . . . . . . 10
137		eqidd 2623	. . . . . . . . . 10 $/\$ $/\$
138	101	adantr 481	. . . . . . . . . . . . 13 $/\$
139		fzss2 12381	. . . . . . . . . . . . . . 15
140		imass2 5501	. . . . . . . . . . . . . . 15
141	118, 139, 140	3syl 18	. . . . . . . . . . . . . 14
142	141	sselda 3603	. . . . . . . . . . . . 13 $/\$
143		fvun2 6270	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
144	87, 90, 143	mp3an12 1414	. . . . . . . . . . . . 13 $/\$
145	138, 142, 144	syl2anc 693	. . . . . . . . . . . 12 $/\$
146	88	fvconst2 6469	. . . . . . . . . . . . 13
147	142, 146	syl 17	. . . . . . . . . . . 12 $/\$
148	145, 147	eqtrd 2656	. . . . . . . . . . 11 $/\$
149	148	adantr 481	. . . . . . . . . 10 $/\$ $/\$
150	84, 134, 135, 135, 136, 137, 149	ofval 6906	. . . . . . . . 9 $/\$ $/\$
151	28, 150	mpdan 702	. . . . . . . 8 $/\$
152	30	zcnd 11483	. . . . . . . . . 10 $/\$
153	152	addid1d 10236	. . . . . . . . 9 $/\$
154	28, 153	syldan 487	. . . . . . . 8 $/\$
155	81, 151, 154	3eqtrd 2660	. . . . . . 7 $/\$
156		breq1 4656	. . . . . . . . . . . . . . 15
157		oveq1 6657	. . . . . . . . . . . . . . 15
158	156, 157	ifbieq2d 4111	. . . . . . . . . . . . . 14
159	41	ltnrd 10171	. . . . . . . . . . . . . . 15
160	159	iffalsed 4097	. . . . . . . . . . . . . 14
161	158, 160	sylan9eqr 2678	. . . . . . . . . . . . 13 $/\$
162	161	csbeq1d 3540	. . . . . . . . . . . 12 $/\$
163		ovex 6678	. . . . . . . . . . . . 13
164		oveq2 6658	. . . . . . . . . . . . . . . . 17
165	164	imaeq2d 5466	. . . . . . . . . . . . . . . 16
166	165	xpeq1d 5138	. . . . . . . . . . . . . . 15
167		oveq1 6657	. . . . . . . . . . . . . . . . . 18
168	167	oveq1d 6665	. . . . . . . . . . . . . . . . 17
169	168	imaeq2d 5466	. . . . . . . . . . . . . . . 16
170	169	xpeq1d 5138	. . . . . . . . . . . . . . 15
171	166, 170	uneq12d 3768	. . . . . . . . . . . . . 14
172	171	oveq2d 6666	. . . . . . . . . . . . 13
173	163, 172	csbie 3559	. . . . . . . . . . . 12
174	162, 173	syl6eq 2672	. . . . . . . . . . 11 $/\$
175		1eluzge0 11732	. . . . . . . . . . . . 13
176		fzss1 12380	. . . . . . . . . . . . 13
177	175, 176	ax-mp 5	. . . . . . . . . . . 12
178	177, 16	sseldi 3601	. . . . . . . . . . 11
179		ovexd 6680	. . . . . . . . . . 11
180	35, 174, 178, 179	fvmptd 6288	. . . . . . . . . 10
181	180	fveq1d 6193	. . . . . . . . 9
182	181	adantr 481	. . . . . . . 8 $/\$
183		fnconstg 6093	. . . . . . . . . . . . . . 15
184	85, 183	ax-mp 5	. . . . . . . . . . . . . 14
185		fnconstg 6093	. . . . . . . . . . . . . . 15
186	88, 185	ax-mp 5	. . . . . . . . . . . . . 14
187	184, 186	pm3.2i 471	. . . . . . . . . . . . 13 $/\$
188		imain 5974	. . . . . . . . . . . . . . . 16
189	1, 93, 188	3syl 18	. . . . . . . . . . . . . . 15
190		peano2re 10209	. . . . . . . . . . . . . . . . . . 19
191	41, 190	syl 17	. . . . . . . . . . . . . . . . . 18
192	191	ltp1d 10954	. . . . . . . . . . . . . . . . 17
193		fzdisj 12368	. . . . . . . . . . . . . . . . 17
194	192, 193	syl 17	. . . . . . . . . . . . . . . 16
195	194	imaeq2d 5466	. . . . . . . . . . . . . . 15
196	189, 195	eqtr3d 2658	. . . . . . . . . . . . . 14
197	196, 99	syl6eq 2672	. . . . . . . . . . . . 13
198		fnun 5997	. . . . . . . . . . . . 13 $/\$ $/\$
199	187, 197, 198	sylancr 695	. . . . . . . . . . . 12
200		fzsplit 12367	. . . . . . . . . . . . . . . . 17
201	22, 200	syl 17	. . . . . . . . . . . . . . . 16
202	201	imaeq2d 5466	. . . . . . . . . . . . . . 15
203		imaundi 5545	. . . . . . . . . . . . . . 15
204	202, 203	syl6eq 2672	. . . . . . . . . . . . . 14
205	204, 130	eqtr3d 2658	. . . . . . . . . . . . 13
206	205	fneq2d 5982	. . . . . . . . . . . 12
207	199, 206	mpbid 222	. . . . . . . . . . 11
208	207	adantr 481	. . . . . . . . . 10 $/\$
209	197	adantr 481	. . . . . . . . . . . . 13 $/\$
210		fzss1 12380	. . . . . . . . . . . . . . 15
211		imass2 5501	. . . . . . . . . . . . . . 15
212	105, 210, 211	3syl 18	. . . . . . . . . . . . . 14
213	212	sselda 3603	. . . . . . . . . . . . 13 $/\$
214		fvun1 6269	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
215	184, 186, 214	mp3an12 1414	. . . . . . . . . . . . 13 $/\$
216	209, 213, 215	syl2anc 693	. . . . . . . . . . . 12 $/\$
217	85	fvconst2 6469	. . . . . . . . . . . . 13
218	213, 217	syl 17	. . . . . . . . . . . 12 $/\$
219	216, 218	eqtrd 2656	. . . . . . . . . . 11 $/\$
220	219	adantr 481	. . . . . . . . . 10 $/\$ $/\$
221	84, 208, 135, 135, 136, 137, 220	ofval 6906	. . . . . . . . 9 $/\$ $/\$
222	28, 221	mpdan 702	. . . . . . . 8 $/\$
223	182, 222	eqtrd 2656	. . . . . . 7 $/\$
224	34, 155, 223	3netr4d 2871	. . . . . 6 $/\$
225	224	ralrimiva 2966	. . . . 5
226		fzpr 12396	. . . . . . . . 9
227	16, 39, 226	3syl 18	. . . . . . . 8
228	227	imaeq2d 5466	. . . . . . 7
229		f1ofn 6138	. . . . . . . . 9
230	1, 229	syl 17	. . . . . . . 8
231		fnimapr 6262	. . . . . . . 8 $/\$ $/\$
232	230, 17, 22, 231	syl3anc 1326	. . . . . . 7
233	228, 232	eqtrd 2656	. . . . . 6
234	233	raleqdv 3144	. . . . 5
235	225, 234	mpbid 222	. . . 4
236		fvex 6201	. . . . 5
237		fvex 6201	. . . . 5
238		fveq2 6191	. . . . . 6
239		fveq2 6191	. . . . . 6
240	238, 239	neeq12d 2855	. . . . 5
241		fveq2 6191	. . . . . 6
242		fveq2 6191	. . . . . 6
243	241, 242	neeq12d 2855	. . . . 5
244	236, 237, 240, 243	ralpr 4238	. . . 4 $/\$
245	235, 244	sylib 208	. . 3 $/\$
246	41	ltp1d 10954	. . . . 5
247	41, 246	ltned 10173	. . . 4
248		f1of1 6136	. . . . . . 7
249	1, 248	syl 17	. . . . . 6
250		f1veqaeq 6514	. . . . . 6 $/\$ $/\$
251	249, 17, 22, 250	syl12anc 1324	. . . . 5
252	251	necon3d 2815	. . . 4
253	247, 252	mpd 15	. . 3
254	240	anbi1d 741	. . . . 5 $/\$ $/\$
255		neeq1 2856	. . . . 5
256	254, 255	anbi12d 747	. . . 4 $/\$ $/\$ $/\$ $/\$
257		fveq2 6191	. . . . . . 7
258		fveq2 6191	. . . . . . 7
259	257, 258	neeq12d 2855	. . . . . 6
260	259	anbi2d 740	. . . . 5 $/\$ $/\$
261		neeq2 2857	. . . . 5
262	260, 261	anbi12d 747	. . . 4 $/\$ $/\$ $/\$ $/\$
263	256, 262	rspc2ev 3324	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
264	18, 23, 245, 253, 263	syl112anc 1330	. 2 $/\$ $/\$
265		dfrex2 2996	. . 3 $/\$ $/\$ $/\$ $/\$
266		fveq2 6191	. . . . . 6
267		fveq2 6191	. . . . . 6
268	266, 267	neeq12d 2855	. . . . 5
269	268	rmo4 3399	. . . 4 $/\$
270		dfral2 2994	. . . . . 6 $/\$ $/\$
271		df-ne 2795	. . . . . . . . 9
272	271	anbi2i 730	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
273		annim 441	. . . . . . . 8 $/\$ $/\$ $/\$
274	272, 273	bitri 264	. . . . . . 7 $/\$ $/\$ $/\$
275	274	rexbii 3041	. . . . . 6 $/\$ $/\$ $/\$
276	270, 275	xchbinxr 325	. . . . 5 $/\$ $/\$ $/\$
277	276	ralbii 2980	. . . 4 $/\$ $/\$ $/\$
278	269, 277	bitri 264	. . 3 $/\$ $/\$
279	265, 278	xchbinxr 325	. 2 $/\$ $/\$
280	264, 279	sylib 208	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 196 $/\$ wa 384

wceq 1483

wcel 1990

wne 2794

wral 2912

wrex 2913

wrmo 2915

cvv 3200

csb 3533

cun 3572

cin 3573

wss 3574

c0 3915

cif 4086

csn 4177

cpr 4179 class class class wbr 4653

cmpt 4729

cxp 5112

ccnv 5113

crn 5115

cima 5117

wfun 5882

wfn 5883

wf 5884

wf1 5885

wfo 5886

wf1o 5887

cfv 5888 (class class class)co 6650

cof 6895

cc 9934

cr 9935

cc0 9936

c1 9937

caddc 9939

clt 10074

cmin 10266

cn 11020

cz 11377

cuz 11687

cfz 12326

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-of 6897 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-er 7742 df-en 7956 df-dom 7957 df-sdom 7958 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-nn 11021 df-n0 11293 df-z 11378 df-uz 11688 df-fz 12327

This theorem is referenced by: poimirlem8 33417 poimirlem18 33427 poimirlem21 33430 poimirlem22 33431

W3C validator