poimirlem2 - Mathbox for Brendan Leahy

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

Theorem poimirlem2 33411

Description: Lemma for poimir 33442- consecutive vertices differ in at most one dimension. (Contributed by Brendan Leahy, 21-Aug-2020.)

**Hypotheses**
Ref	Expression
poimir.0
poimirlem2.1
poimirlem2.2
poimirlem2.3
poimirlem2.4
poimirlem2.5	$\$

**Assertion**
Ref	Expression
poimirlem2

Distinct variable groups:

Proof of Theorem poimirlem2 Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		poimirlem2.3	. . . . . . . . . . . . . . . 16
2		dff1o3 6143	. . . . . . . . . . . . . . . . 17 $/\$
3	2	simprbi 480	. . . . . . . . . . . . . . . 16
4	1, 3	syl 17	. . . . . . . . . . . . . . 15
5		imadif 5973	. . . . . . . . . . . . . . 15 $\$ $\$
6	4, 5	syl 17	. . . . . . . . . . . . . 14 $\$ $\$
7		poimirlem2.4	. . . . . . . . . . . . . . . . . . . 20
8		fzp1elp1 12394	. . . . . . . . . . . . . . . . . . . 20
9	7, 8	syl 17	. . . . . . . . . . . . . . . . . . 19
10		poimir.0	. . . . . . . . . . . . . . . . . . . . . 22
11	10	nncnd 11036	. . . . . . . . . . . . . . . . . . . . 21
12		npcan1 10455	. . . . . . . . . . . . . . . . . . . . 21
13	11, 12	syl 17	. . . . . . . . . . . . . . . . . . . 20
14	13	oveq2d 6666	. . . . . . . . . . . . . . . . . . 19
15	9, 14	eleqtrd 2703	. . . . . . . . . . . . . . . . . 18
16		fzsplit 12367	. . . . . . . . . . . . . . . . . 18
17	15, 16	syl 17	. . . . . . . . . . . . . . . . 17
18	17	difeq1d 3727	. . . . . . . . . . . . . . . 16 $\$ $\$
19		difundir 3880	. . . . . . . . . . . . . . . . 17 $\$ $\$ $\$
20		elfzuz 12338	. . . . . . . . . . . . . . . . . . . . . 22
21	7, 20	syl 17	. . . . . . . . . . . . . . . . . . . . 21
22		fzsuc 12388	. . . . . . . . . . . . . . . . . . . . 21
23	21, 22	syl 17	. . . . . . . . . . . . . . . . . . . 20
24	23	difeq1d 3727	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
25		difun2 4048	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
26		elfzelz 12342	. . . . . . . . . . . . . . . . . . . . . . . . . 26
27	7, 26	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25
28	27	zred 11482	. . . . . . . . . . . . . . . . . . . . . . . 24
29	28	ltp1d 10954	. . . . . . . . . . . . . . . . . . . . . . 23
30	27	peano2zd 11485	. . . . . . . . . . . . . . . . . . . . . . . . 25
31	30	zred 11482	. . . . . . . . . . . . . . . . . . . . . . . 24
32	28, 31	ltnled 10184	. . . . . . . . . . . . . . . . . . . . . . 23
33	29, 32	mpbid 222	. . . . . . . . . . . . . . . . . . . . . 22
34		elfzle2 12345	. . . . . . . . . . . . . . . . . . . . . 22
35	33, 34	nsyl 135	. . . . . . . . . . . . . . . . . . . . 21
36		difsn 4328	. . . . . . . . . . . . . . . . . . . . 21 $\$
37	35, 36	syl 17	. . . . . . . . . . . . . . . . . . . 20 $\$
38	25, 37	syl5eq 2668	. . . . . . . . . . . . . . . . . . 19 $\$
39	24, 38	eqtrd 2656	. . . . . . . . . . . . . . . . . 18 $\$
40	31	ltp1d 10954	. . . . . . . . . . . . . . . . . . . . 21
41		peano2re 10209	. . . . . . . . . . . . . . . . . . . . . . 23
42	31, 41	syl 17	. . . . . . . . . . . . . . . . . . . . . 22
43	31, 42	ltnled 10184	. . . . . . . . . . . . . . . . . . . . 21
44	40, 43	mpbid 222	. . . . . . . . . . . . . . . . . . . 20
45		elfzle1 12344	. . . . . . . . . . . . . . . . . . . 20
46	44, 45	nsyl 135	. . . . . . . . . . . . . . . . . . 19
47		difsn 4328	. . . . . . . . . . . . . . . . . . 19 $\$
48	46, 47	syl 17	. . . . . . . . . . . . . . . . . 18 $\$
49	39, 48	uneq12d 3768	. . . . . . . . . . . . . . . . 17 $\$ $\$
50	19, 49	syl5eq 2668	. . . . . . . . . . . . . . . 16 $\$
51	18, 50	eqtrd 2656	. . . . . . . . . . . . . . 15 $\$
52	51	imaeq2d 5466	. . . . . . . . . . . . . 14 $\$
53	6, 52	eqtr3d 2658	. . . . . . . . . . . . 13 $\$
54		imaundi 5545	. . . . . . . . . . . . 13
55	53, 54	syl6eq 2672	. . . . . . . . . . . 12 $\$
56	55	eleq2d 2687	. . . . . . . . . . 11 $\$
57		eldif 3584	. . . . . . . . . . 11 $\$ $/\$
58		elun 3753	. . . . . . . . . . 11 $\/$
59	56, 57, 58	3bitr3g 302	. . . . . . . . . 10 $/\$ $\/$
60	59	adantr 481	. . . . . . . . 9 $/\$ $/\$ $\/$
61		imassrn 5477	. . . . . . . . . . . . . . . 16
62		f1of 6137	. . . . . . . . . . . . . . . . . 18
63	1, 62	syl 17	. . . . . . . . . . . . . . . . 17
64		frn 6053	. . . . . . . . . . . . . . . . 17
65	63, 64	syl 17	. . . . . . . . . . . . . . . 16
66	61, 65	syl5ss 3614	. . . . . . . . . . . . . . 15
67	66	sselda 3603	. . . . . . . . . . . . . 14 $/\$
68		poimirlem2.2	. . . . . . . . . . . . . . . . . 18
69		ffn 6045	. . . . . . . . . . . . . . . . . 18
70	68, 69	syl 17	. . . . . . . . . . . . . . . . 17
71	70	adantr 481	. . . . . . . . . . . . . . . 16 $/\$
72		1ex 10035	. . . . . . . . . . . . . . . . . . . . 21
73		fnconstg 6093	. . . . . . . . . . . . . . . . . . . . 21
74	72, 73	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20
75		c0ex 10034	. . . . . . . . . . . . . . . . . . . . 21
76		fnconstg 6093	. . . . . . . . . . . . . . . . . . . . 21
77	75, 76	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20
78	74, 77	pm3.2i 471	. . . . . . . . . . . . . . . . . . 19 $/\$
79		imain 5974	. . . . . . . . . . . . . . . . . . . . 21
80	4, 79	syl 17	. . . . . . . . . . . . . . . . . . . 20
81		fzdisj 12368	. . . . . . . . . . . . . . . . . . . . . . 23
82	29, 81	syl 17	. . . . . . . . . . . . . . . . . . . . . 22
83	82	imaeq2d 5466	. . . . . . . . . . . . . . . . . . . . 21
84		ima0 5481	. . . . . . . . . . . . . . . . . . . . 21
85	83, 84	syl6eq 2672	. . . . . . . . . . . . . . . . . . . 20
86	80, 85	eqtr3d 2658	. . . . . . . . . . . . . . . . . . 19
87		fnun 5997	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
88	78, 86, 87	sylancr 695	. . . . . . . . . . . . . . . . . 18
89		imaundi 5545	. . . . . . . . . . . . . . . . . . . 20
90	10	nnzd 11481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
91		peano2zm 11420	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
92	90, 91	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
93		uzid 11702	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
94	92, 93	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
95		peano2uz 11741	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
96	94, 95	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26
97	13, 96	eqeltrrd 2702	. . . . . . . . . . . . . . . . . . . . . . . . 25
98		fzss2 12381	. . . . . . . . . . . . . . . . . . . . . . . . 25
99	97, 98	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24
100	99, 7	sseldd 3604	. . . . . . . . . . . . . . . . . . . . . . 23
101		fzsplit 12367	. . . . . . . . . . . . . . . . . . . . . . 23
102	100, 101	syl 17	. . . . . . . . . . . . . . . . . . . . . 22
103	102	imaeq2d 5466	. . . . . . . . . . . . . . . . . . . . 21
104		f1ofo 6144	. . . . . . . . . . . . . . . . . . . . . . 23
105	1, 104	syl 17	. . . . . . . . . . . . . . . . . . . . . 22
106		foima 6120	. . . . . . . . . . . . . . . . . . . . . 22
107	105, 106	syl 17	. . . . . . . . . . . . . . . . . . . . 21
108	103, 107	eqtr3d 2658	. . . . . . . . . . . . . . . . . . . 20
109	89, 108	syl5eqr 2670	. . . . . . . . . . . . . . . . . . 19
110	109	fneq2d 5982	. . . . . . . . . . . . . . . . . 18
111	88, 110	mpbid 222	. . . . . . . . . . . . . . . . 17
112	111	adantr 481	. . . . . . . . . . . . . . . 16 $/\$
113		fzfid 12772	. . . . . . . . . . . . . . . 16 $/\$
114		inidm 3822	. . . . . . . . . . . . . . . 16
115		eqidd 2623	. . . . . . . . . . . . . . . 16 $/\$ $/\$
116		fvun1 6269	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
117	74, 77, 116	mp3an12 1414	. . . . . . . . . . . . . . . . . . 19 $/\$
118	86, 117	sylan 488	. . . . . . . . . . . . . . . . . 18 $/\$
119	72	fvconst2 6469	. . . . . . . . . . . . . . . . . . 19
120	119	adantl 482	. . . . . . . . . . . . . . . . . 18 $/\$
121	118, 120	eqtrd 2656	. . . . . . . . . . . . . . . . 17 $/\$
122	121	adantr 481	. . . . . . . . . . . . . . . 16 $/\$ $/\$
123	71, 112, 113, 113, 114, 115, 122	ofval 6906	. . . . . . . . . . . . . . 15 $/\$ $/\$
124		fnconstg 6093	. . . . . . . . . . . . . . . . . . . . 21
125	72, 124	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20
126		fnconstg 6093	. . . . . . . . . . . . . . . . . . . . 21
127	75, 126	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20
128	125, 127	pm3.2i 471	. . . . . . . . . . . . . . . . . . 19 $/\$
129		imain 5974	. . . . . . . . . . . . . . . . . . . . 21
130	4, 129	syl 17	. . . . . . . . . . . . . . . . . . . 20
131		fzdisj 12368	. . . . . . . . . . . . . . . . . . . . . . 23
132	40, 131	syl 17	. . . . . . . . . . . . . . . . . . . . . 22
133	132	imaeq2d 5466	. . . . . . . . . . . . . . . . . . . . 21
134	133, 84	syl6eq 2672	. . . . . . . . . . . . . . . . . . . 20
135	130, 134	eqtr3d 2658	. . . . . . . . . . . . . . . . . . 19
136		fnun 5997	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
137	128, 135, 136	sylancr 695	. . . . . . . . . . . . . . . . . 18
138		imaundi 5545	. . . . . . . . . . . . . . . . . . . 20
139	17	imaeq2d 5466	. . . . . . . . . . . . . . . . . . . . 21
140	139, 107	eqtr3d 2658	. . . . . . . . . . . . . . . . . . . 20
141	138, 140	syl5eqr 2670	. . . . . . . . . . . . . . . . . . 19
142	141	fneq2d 5982	. . . . . . . . . . . . . . . . . 18
143	137, 142	mpbid 222	. . . . . . . . . . . . . . . . 17
144	143	adantr 481	. . . . . . . . . . . . . . . 16 $/\$
145		uzid 11702	. . . . . . . . . . . . . . . . . . . . . . 23
146	27, 145	syl 17	. . . . . . . . . . . . . . . . . . . . . 22
147		peano2uz 11741	. . . . . . . . . . . . . . . . . . . . . 22
148	146, 147	syl 17	. . . . . . . . . . . . . . . . . . . . 21
149		fzss2 12381	. . . . . . . . . . . . . . . . . . . . 21
150	148, 149	syl 17	. . . . . . . . . . . . . . . . . . . 20
151		imass2 5501	. . . . . . . . . . . . . . . . . . . 20
152	150, 151	syl 17	. . . . . . . . . . . . . . . . . . 19
153	152	sselda 3603	. . . . . . . . . . . . . . . . . 18 $/\$
154		fvun1 6269	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
155	125, 127, 154	mp3an12 1414	. . . . . . . . . . . . . . . . . . . 20 $/\$
156	135, 155	sylan 488	. . . . . . . . . . . . . . . . . . 19 $/\$
157	72	fvconst2 6469	. . . . . . . . . . . . . . . . . . . 20
158	157	adantl 482	. . . . . . . . . . . . . . . . . . 19 $/\$
159	156, 158	eqtrd 2656	. . . . . . . . . . . . . . . . . 18 $/\$
160	153, 159	syldan 487	. . . . . . . . . . . . . . . . 17 $/\$
161	160	adantr 481	. . . . . . . . . . . . . . . 16 $/\$ $/\$
162	71, 144, 113, 113, 114, 115, 161	ofval 6906	. . . . . . . . . . . . . . 15 $/\$ $/\$
163	123, 162	eqtr4d 2659	. . . . . . . . . . . . . 14 $/\$ $/\$
164	67, 163	mpdan 702	. . . . . . . . . . . . 13 $/\$
165		imassrn 5477	. . . . . . . . . . . . . . . 16
166	165, 65	syl5ss 3614	. . . . . . . . . . . . . . 15
167	166	sselda 3603	. . . . . . . . . . . . . 14 $/\$
168	70	adantr 481	. . . . . . . . . . . . . . . 16 $/\$
169	111	adantr 481	. . . . . . . . . . . . . . . 16 $/\$
170		fzfid 12772	. . . . . . . . . . . . . . . 16 $/\$
171		eqidd 2623	. . . . . . . . . . . . . . . 16 $/\$ $/\$
172		uzid 11702	. . . . . . . . . . . . . . . . . . . . . . 23
173	30, 172	syl 17	. . . . . . . . . . . . . . . . . . . . . 22
174		peano2uz 11741	. . . . . . . . . . . . . . . . . . . . . 22
175	173, 174	syl 17	. . . . . . . . . . . . . . . . . . . . 21
176		fzss1 12380	. . . . . . . . . . . . . . . . . . . . 21
177	175, 176	syl 17	. . . . . . . . . . . . . . . . . . . 20
178		imass2 5501	. . . . . . . . . . . . . . . . . . . 20
179	177, 178	syl 17	. . . . . . . . . . . . . . . . . . 19
180	179	sselda 3603	. . . . . . . . . . . . . . . . . 18 $/\$
181		fvun2 6270	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
182	74, 77, 181	mp3an12 1414	. . . . . . . . . . . . . . . . . . . 20 $/\$
183	86, 182	sylan 488	. . . . . . . . . . . . . . . . . . 19 $/\$
184	75	fvconst2 6469	. . . . . . . . . . . . . . . . . . . 20
185	184	adantl 482	. . . . . . . . . . . . . . . . . . 19 $/\$
186	183, 185	eqtrd 2656	. . . . . . . . . . . . . . . . . 18 $/\$
187	180, 186	syldan 487	. . . . . . . . . . . . . . . . 17 $/\$
188	187	adantr 481	. . . . . . . . . . . . . . . 16 $/\$ $/\$
189	168, 169, 170, 170, 114, 171, 188	ofval 6906	. . . . . . . . . . . . . . 15 $/\$ $/\$
190	143	adantr 481	. . . . . . . . . . . . . . . 16 $/\$
191		fvun2 6270	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
192	125, 127, 191	mp3an12 1414	. . . . . . . . . . . . . . . . . . 19 $/\$
193	135, 192	sylan 488	. . . . . . . . . . . . . . . . . 18 $/\$
194	75	fvconst2 6469	. . . . . . . . . . . . . . . . . . 19
195	194	adantl 482	. . . . . . . . . . . . . . . . . 18 $/\$
196	193, 195	eqtrd 2656	. . . . . . . . . . . . . . . . 17 $/\$
197	196	adantr 481	. . . . . . . . . . . . . . . 16 $/\$ $/\$
198	168, 190, 170, 170, 114, 171, 197	ofval 6906	. . . . . . . . . . . . . . 15 $/\$ $/\$
199	189, 198	eqtr4d 2659	. . . . . . . . . . . . . 14 $/\$ $/\$
200	167, 199	mpdan 702	. . . . . . . . . . . . 13 $/\$
201	164, 200	jaodan 826	. . . . . . . . . . . 12 $/\$ $\/$
202	201	adantlr 751	. . . . . . . . . . 11 $/\$ $/\$ $\/$
203		poimirlem2.1	. . . . . . . . . . . . . . 15
204	203	adantr 481	. . . . . . . . . . . . . 14 $/\$
205		vex 3203	. . . . . . . . . . . . . . . . 17
206		ovex 6678	. . . . . . . . . . . . . . . . 17
207	205, 206	ifex 4156	. . . . . . . . . . . . . . . 16
208	207	a1i 11	. . . . . . . . . . . . . . 15 $/\$ $/\$
209		breq1 4656	. . . . . . . . . . . . . . . . . . . . . 22
210	209	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 $/\$
211		simpr 477	. . . . . . . . . . . . . . . . . . . . 21 $/\$
212		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . 22
213	27	zcnd 11483	. . . . . . . . . . . . . . . . . . . . . . 23
214		npcan1 10455	. . . . . . . . . . . . . . . . . . . . . . 23
215	213, 214	syl 17	. . . . . . . . . . . . . . . . . . . . . 22
216	212, 215	sylan9eqr 2678	. . . . . . . . . . . . . . . . . . . . 21 $/\$
217	210, 211, 216	ifbieq12d 4113	. . . . . . . . . . . . . . . . . . . 20 $/\$
218	217	adantlr 751	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
219		poimirlem2.5	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$
220	219	eldifad 3586	. . . . . . . . . . . . . . . . . . . . . . . . 25
221		elfzelz 12342	. . . . . . . . . . . . . . . . . . . . . . . . 25
222	220, 221	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24
223		zltlem1 11430	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
224	222, 27, 223	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . 23
225	222	zred 11482	. . . . . . . . . . . . . . . . . . . . . . . 24
226		peano2zm 11420	. . . . . . . . . . . . . . . . . . . . . . . . . 26
227	27, 226	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25
228	227	zred 11482	. . . . . . . . . . . . . . . . . . . . . . . 24
229	225, 228	lenltd 10183	. . . . . . . . . . . . . . . . . . . . . . 23
230	224, 229	bitrd 268	. . . . . . . . . . . . . . . . . . . . . 22
231	230	biimpa 501	. . . . . . . . . . . . . . . . . . . . 21 $/\$
232	231	iffalsed 4097	. . . . . . . . . . . . . . . . . . . 20 $/\$
233	232	adantr 481	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
234	218, 233	eqtrd 2656	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
235	234	eqeq2d 2632	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
236	235	biimpa 501	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
237		oveq2 6658	. . . . . . . . . . . . . . . . . . . 20
238	237	imaeq2d 5466	. . . . . . . . . . . . . . . . . . 19
239	238	xpeq1d 5138	. . . . . . . . . . . . . . . . . 18
240		oveq1 6657	. . . . . . . . . . . . . . . . . . . . 21
241	240	oveq1d 6665	. . . . . . . . . . . . . . . . . . . 20
242	241	imaeq2d 5466	. . . . . . . . . . . . . . . . . . 19
243	242	xpeq1d 5138	. . . . . . . . . . . . . . . . . 18
244	239, 243	uneq12d 3768	. . . . . . . . . . . . . . . . 17
245	244	oveq2d 6666	. . . . . . . . . . . . . . . 16
246	236, 245	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
247	208, 246	csbied 3560	. . . . . . . . . . . . . 14 $/\$ $/\$
248		elfzm1b 12418	. . . . . . . . . . . . . . . . 17 $/\$
249	27, 90, 248	syl2anc 693	. . . . . . . . . . . . . . . 16
250	100, 249	mpbid 222	. . . . . . . . . . . . . . 15
251	250	adantr 481	. . . . . . . . . . . . . 14 $/\$
252		ovexd 6680	. . . . . . . . . . . . . 14 $/\$
253	204, 247, 251, 252	fvmptd 6288	. . . . . . . . . . . . 13 $/\$
254	253	fveq1d 6193	. . . . . . . . . . . 12 $/\$
255	254	adantr 481	. . . . . . . . . . 11 $/\$ $/\$ $\/$
256	207	a1i 11	. . . . . . . . . . . . . . 15 $/\$ $/\$
257		breq1 4656	. . . . . . . . . . . . . . . . . . . 20
258		id 22	. . . . . . . . . . . . . . . . . . . 20
259		oveq1 6657	. . . . . . . . . . . . . . . . . . . 20
260	257, 258, 259	ifbieq12d 4113	. . . . . . . . . . . . . . . . . . 19
261		ltnsym 10135	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
262	225, 28, 261	syl2anc 693	. . . . . . . . . . . . . . . . . . . . 21
263	262	imp 445	. . . . . . . . . . . . . . . . . . . 20 $/\$
264	263	iffalsed 4097	. . . . . . . . . . . . . . . . . . 19 $/\$
265	260, 264	sylan9eqr 2678	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
266	265	eqeq2d 2632	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
267	266	biimpa 501	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
268		oveq2 6658	. . . . . . . . . . . . . . . . . . . 20
269	268	imaeq2d 5466	. . . . . . . . . . . . . . . . . . 19
270	269	xpeq1d 5138	. . . . . . . . . . . . . . . . . 18
271		oveq1 6657	. . . . . . . . . . . . . . . . . . . . 21
272	271	oveq1d 6665	. . . . . . . . . . . . . . . . . . . 20
273	272	imaeq2d 5466	. . . . . . . . . . . . . . . . . . 19
274	273	xpeq1d 5138	. . . . . . . . . . . . . . . . . 18
275	270, 274	uneq12d 3768	. . . . . . . . . . . . . . . . 17
276	275	oveq2d 6666	. . . . . . . . . . . . . . . 16
277	267, 276	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
278	256, 277	csbied 3560	. . . . . . . . . . . . . 14 $/\$ $/\$
279		1eluzge0 11732	. . . . . . . . . . . . . . . . 17
280		fzss1 12380	. . . . . . . . . . . . . . . . 17
281	279, 280	ax-mp 5	. . . . . . . . . . . . . . . 16
282	281, 7	sseldi 3601	. . . . . . . . . . . . . . 15
283	282	adantr 481	. . . . . . . . . . . . . 14 $/\$
284		ovexd 6680	. . . . . . . . . . . . . 14 $/\$
285	204, 278, 283, 284	fvmptd 6288	. . . . . . . . . . . . 13 $/\$
286	285	fveq1d 6193	. . . . . . . . . . . 12 $/\$
287	286	adantr 481	. . . . . . . . . . 11 $/\$ $/\$ $\/$
288	202, 255, 287	3eqtr4d 2666	. . . . . . . . . 10 $/\$ $/\$ $\/$
289	288	ex 450	. . . . . . . . 9 $/\$ $\/$
290	60, 289	sylbid 230	. . . . . . . 8 $/\$ $/\$
291	290	expdimp 453	. . . . . . 7 $/\$ $/\$
292	291	necon1ad 2811	. . . . . 6 $/\$ $/\$
293		elimasni 5492	. . . . . . . 8
294		eqcom 2629	. . . . . . . . 9
295		f1ofn 6138	. . . . . . . . . . 11
296	1, 295	syl 17	. . . . . . . . . 10
297		fnbrfvb 6236	. . . . . . . . . 10 $/\$
298	296, 15, 297	syl2anc 693	. . . . . . . . 9
299	294, 298	syl5bb 272	. . . . . . . 8
300	293, 299	syl5ibr 236	. . . . . . 7
301	300	ad2antrr 762	. . . . . 6 $/\$ $/\$
302	292, 301	syld 47	. . . . 5 $/\$ $/\$
303	302	ralrimiva 2966	. . . 4 $/\$
304		fvex 6201	. . . . 5
305		eqeq2 2633	. . . . . . 7
306	305	imbi2d 330	. . . . . 6
307	306	ralbidv 2986	. . . . 5
308	304, 307	spcev 3300	. . . 4
309	303, 308	syl 17	. . 3 $/\$
310		imadif 5973	. . . . . . . . . . . . . . 15 $\$ $\$
311	4, 310	syl 17	. . . . . . . . . . . . . 14 $\$ $\$
312	102	difeq1d 3727	. . . . . . . . . . . . . . . 16 $\$ $\$
313		difundir 3880	. . . . . . . . . . . . . . . . 17 $\$ $\$ $\$
314	215, 21	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . 22
315		uzid 11702	. . . . . . . . . . . . . . . . . . . . . . . . 25
316	227, 315	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24
317		peano2uz 11741	. . . . . . . . . . . . . . . . . . . . . . . 24
318	316, 317	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23
319	215, 318	eqeltrrd 2702	. . . . . . . . . . . . . . . . . . . . . 22
320		fzsplit2 12366	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
321	314, 319, 320	syl2anc 693	. . . . . . . . . . . . . . . . . . . . 21
322	215	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . 23
323		fzsn 12383	. . . . . . . . . . . . . . . . . . . . . . . 24
324	27, 323	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23
325	322, 324	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . 22
326	325	uneq2d 3767	. . . . . . . . . . . . . . . . . . . . 21
327	321, 326	eqtrd 2656	. . . . . . . . . . . . . . . . . . . 20
328	327	difeq1d 3727	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
329		difun2 4048	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
330	28	ltm1d 10956	. . . . . . . . . . . . . . . . . . . . . . 23
331	228, 28	ltnled 10184	. . . . . . . . . . . . . . . . . . . . . . 23
332	330, 331	mpbid 222	. . . . . . . . . . . . . . . . . . . . . 22
333		elfzle2 12345	. . . . . . . . . . . . . . . . . . . . . 22
334	332, 333	nsyl 135	. . . . . . . . . . . . . . . . . . . . 21
335		difsn 4328	. . . . . . . . . . . . . . . . . . . . 21 $\$
336	334, 335	syl 17	. . . . . . . . . . . . . . . . . . . 20 $\$
337	329, 336	syl5eq 2668	. . . . . . . . . . . . . . . . . . 19 $\$
338	328, 337	eqtrd 2656	. . . . . . . . . . . . . . . . . 18 $\$
339		elfzle1 12344	. . . . . . . . . . . . . . . . . . . 20
340	33, 339	nsyl 135	. . . . . . . . . . . . . . . . . . 19
341		difsn 4328	. . . . . . . . . . . . . . . . . . 19 $\$
342	340, 341	syl 17	. . . . . . . . . . . . . . . . . 18 $\$
343	338, 342	uneq12d 3768	. . . . . . . . . . . . . . . . 17 $\$ $\$
344	313, 343	syl5eq 2668	. . . . . . . . . . . . . . . 16 $\$
345	312, 344	eqtrd 2656	. . . . . . . . . . . . . . 15 $\$
346	345	imaeq2d 5466	. . . . . . . . . . . . . 14 $\$
347	311, 346	eqtr3d 2658	. . . . . . . . . . . . 13 $\$
348		imaundi 5545	. . . . . . . . . . . . 13
349	347, 348	syl6eq 2672	. . . . . . . . . . . 12 $\$
350	349	eleq2d 2687	. . . . . . . . . . 11 $\$
351		eldif 3584	. . . . . . . . . . 11 $\$ $/\$
352		elun 3753	. . . . . . . . . . 11 $\/$
353	350, 351, 352	3bitr3g 302	. . . . . . . . . 10 $/\$ $\/$
354	353	adantr 481	. . . . . . . . 9 $/\$ $/\$ $\/$
355		imassrn 5477	. . . . . . . . . . . . . . . 16
356	355, 65	syl5ss 3614	. . . . . . . . . . . . . . 15
357	356	sselda 3603	. . . . . . . . . . . . . 14 $/\$
358	70	adantr 481	. . . . . . . . . . . . . . . 16 $/\$
359		fnconstg 6093	. . . . . . . . . . . . . . . . . . . . 21
360	72, 359	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20
361		fnconstg 6093	. . . . . . . . . . . . . . . . . . . . 21
362	75, 361	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20
363	360, 362	pm3.2i 471	. . . . . . . . . . . . . . . . . . 19 $/\$
364		imain 5974	. . . . . . . . . . . . . . . . . . . . 21
365	4, 364	syl 17	. . . . . . . . . . . . . . . . . . . 20
366		fzdisj 12368	. . . . . . . . . . . . . . . . . . . . . . 23
367	330, 366	syl 17	. . . . . . . . . . . . . . . . . . . . . 22
368	367	imaeq2d 5466	. . . . . . . . . . . . . . . . . . . . 21
369	368, 84	syl6eq 2672	. . . . . . . . . . . . . . . . . . . 20
370	365, 369	eqtr3d 2658	. . . . . . . . . . . . . . . . . . 19
371		fnun 5997	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
372	363, 370, 371	sylancr 695	. . . . . . . . . . . . . . . . . 18
373		imaundi 5545	. . . . . . . . . . . . . . . . . . . 20
374		uzss 11708	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
375	319, 374	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
376		elfzuz3 12339	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
377	7, 376	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
378	375, 377	sseldd 3604	. . . . . . . . . . . . . . . . . . . . . . . . . 26
379		peano2uz 11741	. . . . . . . . . . . . . . . . . . . . . . . . . 26
380	378, 379	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25
381	13, 380	eqeltrrd 2702	. . . . . . . . . . . . . . . . . . . . . . . 24
382		fzsplit2 12366	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
383	314, 381, 382	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . 23
384	215	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . 24
385	384	uneq2d 3767	. . . . . . . . . . . . . . . . . . . . . . 23
386	383, 385	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . 22
387	386	imaeq2d 5466	. . . . . . . . . . . . . . . . . . . . 21
388	387, 107	eqtr3d 2658	. . . . . . . . . . . . . . . . . . . 20
389	373, 388	syl5eqr 2670	. . . . . . . . . . . . . . . . . . 19
390	389	fneq2d 5982	. . . . . . . . . . . . . . . . . 18
391	372, 390	mpbid 222	. . . . . . . . . . . . . . . . 17
392	391	adantr 481	. . . . . . . . . . . . . . . 16 $/\$
393		fzfid 12772	. . . . . . . . . . . . . . . 16 $/\$
394		eqidd 2623	. . . . . . . . . . . . . . . 16 $/\$ $/\$
395		fvun1 6269	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
396	360, 362, 395	mp3an12 1414	. . . . . . . . . . . . . . . . . . 19 $/\$
397	370, 396	sylan 488	. . . . . . . . . . . . . . . . . 18 $/\$
398	72	fvconst2 6469	. . . . . . . . . . . . . . . . . . 19
399	398	adantl 482	. . . . . . . . . . . . . . . . . 18 $/\$
400	397, 399	eqtrd 2656	. . . . . . . . . . . . . . . . 17 $/\$
401	400	adantr 481	. . . . . . . . . . . . . . . 16 $/\$ $/\$
402	358, 392, 393, 393, 114, 394, 401	ofval 6906	. . . . . . . . . . . . . . 15 $/\$ $/\$
403	111	adantr 481	. . . . . . . . . . . . . . . 16 $/\$
404		fzss2 12381	. . . . . . . . . . . . . . . . . . . . 21
405	319, 404	syl 17	. . . . . . . . . . . . . . . . . . . 20
406		imass2 5501	. . . . . . . . . . . . . . . . . . . 20
407	405, 406	syl 17	. . . . . . . . . . . . . . . . . . 19
408	407	sselda 3603	. . . . . . . . . . . . . . . . . 18 $/\$
409	408, 121	syldan 487	. . . . . . . . . . . . . . . . 17 $/\$
410	409	adantr 481	. . . . . . . . . . . . . . . 16 $/\$ $/\$
411	358, 403, 393, 393, 114, 394, 410	ofval 6906	. . . . . . . . . . . . . . 15 $/\$ $/\$
412	402, 411	eqtr4d 2659	. . . . . . . . . . . . . 14 $/\$ $/\$
413	357, 412	mpdan 702	. . . . . . . . . . . . 13 $/\$
414		imassrn 5477	. . . . . . . . . . . . . . . 16
415	414, 65	syl5ss 3614	. . . . . . . . . . . . . . 15
416	415	sselda 3603	. . . . . . . . . . . . . 14 $/\$
417	70	adantr 481	. . . . . . . . . . . . . . . 16 $/\$
418	391	adantr 481	. . . . . . . . . . . . . . . 16 $/\$
419		fzfid 12772	. . . . . . . . . . . . . . . 16 $/\$
420		eqidd 2623	. . . . . . . . . . . . . . . 16 $/\$ $/\$
421		fzss1 12380	. . . . . . . . . . . . . . . . . . . . 21
422	148, 421	syl 17	. . . . . . . . . . . . . . . . . . . 20
423		imass2 5501	. . . . . . . . . . . . . . . . . . . 20
424	422, 423	syl 17	. . . . . . . . . . . . . . . . . . 19
425	424	sselda 3603	. . . . . . . . . . . . . . . . . 18 $/\$
426		fvun2 6270	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
427	360, 362, 426	mp3an12 1414	. . . . . . . . . . . . . . . . . . . 20 $/\$
428	370, 427	sylan 488	. . . . . . . . . . . . . . . . . . 19 $/\$
429	75	fvconst2 6469	. . . . . . . . . . . . . . . . . . . 20
430	429	adantl 482	. . . . . . . . . . . . . . . . . . 19 $/\$
431	428, 430	eqtrd 2656	. . . . . . . . . . . . . . . . . 18 $/\$
432	425, 431	syldan 487	. . . . . . . . . . . . . . . . 17 $/\$
433	432	adantr 481	. . . . . . . . . . . . . . . 16 $/\$ $/\$
434	417, 418, 419, 419, 114, 420, 433	ofval 6906	. . . . . . . . . . . . . . 15 $/\$ $/\$
435	111	adantr 481	. . . . . . . . . . . . . . . 16 $/\$
436	186	adantr 481	. . . . . . . . . . . . . . . 16 $/\$ $/\$
437	417, 435, 419, 419, 114, 420, 436	ofval 6906	. . . . . . . . . . . . . . 15 $/\$ $/\$
438	434, 437	eqtr4d 2659	. . . . . . . . . . . . . 14 $/\$ $/\$
439	416, 438	mpdan 702	. . . . . . . . . . . . 13 $/\$
440	413, 439	jaodan 826	. . . . . . . . . . . 12 $/\$ $\/$
441	440	adantlr 751	. . . . . . . . . . 11 $/\$ $/\$ $\/$
442	203	adantr 481	. . . . . . . . . . . . . 14 $/\$
443	207	a1i 11	. . . . . . . . . . . . . . 15 $/\$ $/\$
444	217	adantlr 751	. . . . . . . . . . . . . . . 16 $/\$ $/\$
445		lttr 10114	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
446	228, 28, 225, 445	syl3anc 1326	. . . . . . . . . . . . . . . . . . . 20 $/\$
447	330, 446	mpand 711	. . . . . . . . . . . . . . . . . . 19
448	447	imp 445	. . . . . . . . . . . . . . . . . 18 $/\$
449	448	iftrued 4094	. . . . . . . . . . . . . . . . 17 $/\$
450	449	adantr 481	. . . . . . . . . . . . . . . 16 $/\$ $/\$
451	444, 450	eqtrd 2656	. . . . . . . . . . . . . . 15 $/\$ $/\$
452		simpll 790	. . . . . . . . . . . . . . . 16 $/\$ $/\$
453		oveq2 6658	. . . . . . . . . . . . . . . . . . . . 21
454	453	imaeq2d 5466	. . . . . . . . . . . . . . . . . . . 20
455	454	xpeq1d 5138	. . . . . . . . . . . . . . . . . . 19
456	455	adantl 482	. . . . . . . . . . . . . . . . . 18 $/\$
457		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . 22
458	457, 215	sylan9eqr 2678	. . . . . . . . . . . . . . . . . . . . 21 $/\$
459	458	oveq1d 6665	. . . . . . . . . . . . . . . . . . . 20 $/\$
460	459	imaeq2d 5466	. . . . . . . . . . . . . . . . . . 19 $/\$
461	460	xpeq1d 5138	. . . . . . . . . . . . . . . . . 18 $/\$
462	456, 461	uneq12d 3768	. . . . . . . . . . . . . . . . 17 $/\$
463	462	oveq2d 6666	. . . . . . . . . . . . . . . 16 $/\$
464	452, 463	sylan 488	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
465	443, 451, 464	csbied2 3561	. . . . . . . . . . . . . 14 $/\$ $/\$
466	250	adantr 481	. . . . . . . . . . . . . 14 $/\$
467		ovexd 6680	. . . . . . . . . . . . . 14 $/\$
468	442, 465, 466, 467	fvmptd 6288	. . . . . . . . . . . . 13 $/\$
469	468	fveq1d 6193	. . . . . . . . . . . 12 $/\$
470	469	adantr 481	. . . . . . . . . . 11 $/\$ $/\$ $\/$
471	207	a1i 11	. . . . . . . . . . . . . . . 16 $/\$
472		iftrue 4092	. . . . . . . . . . . . . . . . . . . 20
473	260, 472	sylan9eqr 2678	. . . . . . . . . . . . . . . . . . 19 $/\$
474	473	eqeq2d 2632	. . . . . . . . . . . . . . . . . 18 $/\$
475	474	biimpa 501	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
476	475, 245	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$
477	471, 476	csbied 3560	. . . . . . . . . . . . . . 15 $/\$
478	477	adantll 750	. . . . . . . . . . . . . 14 $/\$ $/\$
479	282	adantr 481	. . . . . . . . . . . . . 14 $/\$
480		ovexd 6680	. . . . . . . . . . . . . 14 $/\$
481	442, 478, 479, 480	fvmptd 6288	. . . . . . . . . . . . 13 $/\$
482	481	fveq1d 6193	. . . . . . . . . . . 12 $/\$
483	482	adantr 481	. . . . . . . . . . 11 $/\$ $/\$ $\/$
484	441, 470, 483	3eqtr4d 2666	. . . . . . . . . 10 $/\$ $/\$ $\/$
485	484	ex 450	. . . . . . . . 9 $/\$ $\/$
486	354, 485	sylbid 230	. . . . . . . 8 $/\$ $/\$
487	486	expdimp 453	. . . . . . 7 $/\$ $/\$
488	487	necon1ad 2811	. . . . . 6 $/\$ $/\$
489		elimasni 5492	. . . . . . . 8
490		eqcom 2629	. . . . . . . . 9
491		fnbrfvb 6236	. . . . . . . . . 10 $/\$
492	296, 100, 491	syl2anc 693	. . . . . . . . 9
493	490, 492	syl5bb 272	. . . . . . . 8
494	489, 493	syl5ibr 236	. . . . . . 7
495	494	ad2antrr 762	. . . . . 6 $/\$ $/\$
496	488, 495	syld 47	. . . . 5 $/\$ $/\$
497	496	ralrimiva 2966	. . . 4 $/\$
498		fvex 6201	. . . . 5
499		eqeq2 2633	. . . . . . 7
500	499	imbi2d 330	. . . . . 6
501	500	ralbidv 2986	. . . . 5
502	498, 501	spcev 3300	. . . 4
503	497, 502	syl 17	. . 3 $/\$
504		eldifsni 4320	. . . . 5 $\$
505	219, 504	syl 17	. . . 4
506	225, 28	lttri2d 10176	. . . 4 $\/$
507	505, 506	mpbid 222	. . 3 $\/$
508	309, 503, 507	mpjaodan 827	. 2
509		nfv 1843	. . . 4
510	509	rmo2 3526	. . 3
511		rmoeq1 3141	. . . 4
512	107, 511	syl 17	. . 3
513	510, 512	syl5bbr 274	. 2
514	508, 513	mpbid 222	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 196 $\/$ wo 383 $/\$ wa 384

wceq 1483

wex 1704

wcel 1990

wne 2794

wral 2912

wrmo 2915

cvv 3200

csb 3533 $\$ cdif 3571

cun 3572

cin 3573

wss 3574

c0 3915

cif 4086

csn 4177 class class class wbr 4653

cmpt 4729

cxp 5112

ccnv 5113

crn 5115

cima 5117

wfun 5882

wfn 5883

wf 5884

wfo 5886

wf1o 5887

cfv 5888 (class class class)co 6650

cof 6895

cfn 7955

cc 9934

cr 9935

cc0 9936

c1 9937

caddc 9939

clt 10074

cle 10075

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-1o 7560 df-er 7742 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 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