poimirlem7 - Mathbox for Brendan Leahy

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

Theorem poimirlem7 33416

Description: Lemma for poimir 33442, similar to poimirlem6 33415, but for vertices after the opposite vertex. (Contributed by Brendan Leahy, 21-Aug-2020.)

**Hypotheses**
Ref	Expression
poimir.0
poimirlem22.s	..^
poimirlem9.1
poimirlem9.2
poimirlem7.3

**Assertion**
Ref	Expression
poimirlem7

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

**Proof of Theorem poimirlem7**
Step	Hyp	Ref	Expression
1		poimirlem9.1	. . . . . . . 8
2		elrabi 3359	. . . . . . . . 9 ..^ ..^
3		poimirlem22.s	. . . . . . . . 9 ..^
4	2, 3	eleq2s 2719	. . . . . . . 8 ..^
5	1, 4	syl 17	. . . . . . 7 ..^
6		xp1st 7198	. . . . . . 7 ..^ ..^
7	5, 6	syl 17	. . . . . 6 ..^
8		xp2nd 7199	. . . . . 6 ..^
9	7, 8	syl 17	. . . . 5
10		fvex 6201	. . . . . 6
11		f1oeq1 6127	. . . . . 6
12	10, 11	elab 3350	. . . . 5
13	9, 12	sylib 208	. . . 4
14		f1of 6137	. . . 4
15	13, 14	syl 17	. . 3
16		poimirlem9.2	. . . . . . . . 9
17		elfznn 12370	. . . . . . . . 9
18	16, 17	syl 17	. . . . . . . 8
19	18	peano2nnd 11037	. . . . . . 7
20	19	peano2nnd 11037	. . . . . 6
21		nnuz 11723	. . . . . 6
22	20, 21	syl6eleq 2711	. . . . 5
23		fzss1 12380	. . . . 5
24	22, 23	syl 17	. . . 4
25		poimirlem7.3	. . . 4
26	24, 25	sseldd 3604	. . 3
27	15, 26	ffvelrnd 6360	. 2
28		xp1st 7198	. . . . . . . . . . . . 13 ..^ ..^
29	7, 28	syl 17	. . . . . . . . . . . 12 ..^
30		elmapfn 7880	. . . . . . . . . . . 12 ..^
31	29, 30	syl 17	. . . . . . . . . . 11
32	31	adantr 481	. . . . . . . . . 10 $/\$
33		1ex 10035	. . . . . . . . . . . . . . 15
34		fnconstg 6093	. . . . . . . . . . . . . . 15
35	33, 34	ax-mp 5	. . . . . . . . . . . . . 14
36		c0ex 10034	. . . . . . . . . . . . . . 15
37		fnconstg 6093	. . . . . . . . . . . . . . 15
38	36, 37	ax-mp 5	. . . . . . . . . . . . . 14
39	35, 38	pm3.2i 471	. . . . . . . . . . . . 13 $/\$
40		dff1o3 6143	. . . . . . . . . . . . . . . . 17 $/\$
41	40	simprbi 480	. . . . . . . . . . . . . . . 16
42	13, 41	syl 17	. . . . . . . . . . . . . . 15
43		imain 5974	. . . . . . . . . . . . . . 15
44	42, 43	syl 17	. . . . . . . . . . . . . 14
45		elfzelz 12342	. . . . . . . . . . . . . . . . . . . 20
46	25, 45	syl 17	. . . . . . . . . . . . . . . . . . 19
47	46	zred 11482	. . . . . . . . . . . . . . . . . 18
48	47	ltm1d 10956	. . . . . . . . . . . . . . . . 17
49		fzdisj 12368	. . . . . . . . . . . . . . . . 17
50	48, 49	syl 17	. . . . . . . . . . . . . . . 16
51	50	imaeq2d 5466	. . . . . . . . . . . . . . 15
52		ima0 5481	. . . . . . . . . . . . . . 15
53	51, 52	syl6eq 2672	. . . . . . . . . . . . . 14
54	44, 53	eqtr3d 2658	. . . . . . . . . . . . 13
55		fnun 5997	. . . . . . . . . . . . 13 $/\$ $/\$
56	39, 54, 55	sylancr 695	. . . . . . . . . . . 12
57	46	zcnd 11483	. . . . . . . . . . . . . . . . . . . 20
58		npcan1 10455	. . . . . . . . . . . . . . . . . . . 20
59	57, 58	syl 17	. . . . . . . . . . . . . . . . . . 19
60		1red 10055	. . . . . . . . . . . . . . . . . . . . . 22
61	20	nnred 11035	. . . . . . . . . . . . . . . . . . . . . . 23
62	19	nnred 11035	. . . . . . . . . . . . . . . . . . . . . . . 24
63	19	nnge1d 11063	. . . . . . . . . . . . . . . . . . . . . . . 24
64	62	ltp1d 10954	. . . . . . . . . . . . . . . . . . . . . . . 24
65	60, 62, 61, 63, 64	lelttrd 10195	. . . . . . . . . . . . . . . . . . . . . . 23
66		elfzle1 12344	. . . . . . . . . . . . . . . . . . . . . . . 24
67	25, 66	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23
68	60, 61, 47, 65, 67	ltletrd 10197	. . . . . . . . . . . . . . . . . . . . . 22
69	60, 47, 68	ltled 10185	. . . . . . . . . . . . . . . . . . . . 21
70		elnnz1 11403	. . . . . . . . . . . . . . . . . . . . 21 $/\$
71	46, 69, 70	sylanbrc 698	. . . . . . . . . . . . . . . . . . . 20
72	71, 21	syl6eleq 2711	. . . . . . . . . . . . . . . . . . 19
73	59, 72	eqeltrd 2701	. . . . . . . . . . . . . . . . . 18
74		peano2zm 11420	. . . . . . . . . . . . . . . . . . . . . . 23
75	46, 74	syl 17	. . . . . . . . . . . . . . . . . . . . . 22
76		uzid 11702	. . . . . . . . . . . . . . . . . . . . . 22
77		peano2uz 11741	. . . . . . . . . . . . . . . . . . . . . 22
78	75, 76, 77	3syl 18	. . . . . . . . . . . . . . . . . . . . 21
79	59, 78	eqeltrrd 2702	. . . . . . . . . . . . . . . . . . . 20
80		uzss 11708	. . . . . . . . . . . . . . . . . . . 20
81	79, 80	syl 17	. . . . . . . . . . . . . . . . . . 19
82		elfzuz3 12339	. . . . . . . . . . . . . . . . . . . 20
83	25, 82	syl 17	. . . . . . . . . . . . . . . . . . 19
84	81, 83	sseldd 3604	. . . . . . . . . . . . . . . . . 18
85		fzsplit2 12366	. . . . . . . . . . . . . . . . . 18 $/\$
86	73, 84, 85	syl2anc 693	. . . . . . . . . . . . . . . . 17
87	59	oveq1d 6665	. . . . . . . . . . . . . . . . . 18
88	87	uneq2d 3767	. . . . . . . . . . . . . . . . 17
89	86, 88	eqtrd 2656	. . . . . . . . . . . . . . . 16
90	89	imaeq2d 5466	. . . . . . . . . . . . . . 15
91		imaundi 5545	. . . . . . . . . . . . . . 15
92	90, 91	syl6eq 2672	. . . . . . . . . . . . . 14
93		f1ofo 6144	. . . . . . . . . . . . . . . 16
94	13, 93	syl 17	. . . . . . . . . . . . . . 15
95		foima 6120	. . . . . . . . . . . . . . 15
96	94, 95	syl 17	. . . . . . . . . . . . . 14
97	92, 96	eqtr3d 2658	. . . . . . . . . . . . 13
98	97	fneq2d 5982	. . . . . . . . . . . 12
99	56, 98	mpbid 222	. . . . . . . . . . 11
100	99	adantr 481	. . . . . . . . . 10 $/\$
101		ovexd 6680	. . . . . . . . . 10 $/\$
102		inidm 3822	. . . . . . . . . 10
103		eqidd 2623	. . . . . . . . . 10 $/\$ $/\$
104		imaundi 5545	. . . . . . . . . . . . . . . . . 18
105		fzpred 12389	. . . . . . . . . . . . . . . . . . . 20
106	83, 105	syl 17	. . . . . . . . . . . . . . . . . . 19
107	106	imaeq2d 5466	. . . . . . . . . . . . . . . . . 18
108		f1ofn 6138	. . . . . . . . . . . . . . . . . . . . 21
109	13, 108	syl 17	. . . . . . . . . . . . . . . . . . . 20
110		fnsnfv 6258	. . . . . . . . . . . . . . . . . . . 20 $/\$
111	109, 26, 110	syl2anc 693	. . . . . . . . . . . . . . . . . . 19
112	111	uneq1d 3766	. . . . . . . . . . . . . . . . . 18
113	104, 107, 112	3eqtr4a 2682	. . . . . . . . . . . . . . . . 17
114	113	xpeq1d 5138	. . . . . . . . . . . . . . . 16
115		xpundir 5172	. . . . . . . . . . . . . . . 16
116	114, 115	syl6eq 2672	. . . . . . . . . . . . . . 15
117	116	uneq2d 3767	. . . . . . . . . . . . . 14
118		un12 3771	. . . . . . . . . . . . . 14
119	117, 118	syl6eq 2672	. . . . . . . . . . . . 13
120	119	fveq1d 6193	. . . . . . . . . . . 12
121	120	ad2antrr 762	. . . . . . . . . . 11 $/\$ $/\$
122		fnconstg 6093	. . . . . . . . . . . . . . . . 17
123	36, 122	ax-mp 5	. . . . . . . . . . . . . . . 16
124	35, 123	pm3.2i 471	. . . . . . . . . . . . . . 15 $/\$
125		imain 5974	. . . . . . . . . . . . . . . . 17
126	42, 125	syl 17	. . . . . . . . . . . . . . . 16
127	75	zred 11482	. . . . . . . . . . . . . . . . . . . 20
128		peano2re 10209	. . . . . . . . . . . . . . . . . . . . 21
129	47, 128	syl 17	. . . . . . . . . . . . . . . . . . . 20
130	47	ltp1d 10954	. . . . . . . . . . . . . . . . . . . 20
131	127, 47, 129, 48, 130	lttrd 10198	. . . . . . . . . . . . . . . . . . 19
132		fzdisj 12368	. . . . . . . . . . . . . . . . . . 19
133	131, 132	syl 17	. . . . . . . . . . . . . . . . . 18
134	133	imaeq2d 5466	. . . . . . . . . . . . . . . . 17
135	134, 52	syl6eq 2672	. . . . . . . . . . . . . . . 16
136	126, 135	eqtr3d 2658	. . . . . . . . . . . . . . 15
137		fnun 5997	. . . . . . . . . . . . . . 15 $/\$ $/\$
138	124, 136, 137	sylancr 695	. . . . . . . . . . . . . 14
139		imaundi 5545	. . . . . . . . . . . . . . . 16
140		imadif 5973	. . . . . . . . . . . . . . . . . 18 $\$ $\$
141	42, 140	syl 17	. . . . . . . . . . . . . . . . 17 $\$ $\$
142		fzsplit 12367	. . . . . . . . . . . . . . . . . . . . 21
143	26, 142	syl 17	. . . . . . . . . . . . . . . . . . . 20
144	143	difeq1d 3727	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
145		difundir 3880	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$ $\$
146		fzsplit2 12366	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
147	73, 79, 146	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . 24
148	59	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . 26
149		fzsn 12383	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
150	46, 149	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26
151	148, 150	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . 25
152	151	uneq2d 3767	. . . . . . . . . . . . . . . . . . . . . . . 24
153	147, 152	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . 23
154	153	difeq1d 3727	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$
155		difun2 4048	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $\$
156	127, 47	ltnled 10184	. . . . . . . . . . . . . . . . . . . . . . . . . 26
157	48, 156	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . 25
158		elfzle2 12345	. . . . . . . . . . . . . . . . . . . . . . . . 25
159	157, 158	nsyl 135	. . . . . . . . . . . . . . . . . . . . . . . 24
160		difsn 4328	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
161	159, 160	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 $\$
162	155, 161	syl5eq 2668	. . . . . . . . . . . . . . . . . . . . . 22 $\$
163	154, 162	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . 21 $\$
164	47, 129	ltnled 10184	. . . . . . . . . . . . . . . . . . . . . . . 24
165	130, 164	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . 23
166		elfzle1 12344	. . . . . . . . . . . . . . . . . . . . . . 23
167	165, 166	nsyl 135	. . . . . . . . . . . . . . . . . . . . . 22
168		difsn 4328	. . . . . . . . . . . . . . . . . . . . . 22 $\$
169	167, 168	syl 17	. . . . . . . . . . . . . . . . . . . . 21 $\$
170	163, 169	uneq12d 3768	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
171	145, 170	syl5eq 2668	. . . . . . . . . . . . . . . . . . 19 $\$
172	144, 171	eqtrd 2656	. . . . . . . . . . . . . . . . . 18 $\$
173	172	imaeq2d 5466	. . . . . . . . . . . . . . . . 17 $\$
174	111	eqcomd 2628	. . . . . . . . . . . . . . . . . 18
175	96, 174	difeq12d 3729	. . . . . . . . . . . . . . . . 17 $\$ $\$
176	141, 173, 175	3eqtr3d 2664	. . . . . . . . . . . . . . . 16 $\$
177	139, 176	syl5eqr 2670	. . . . . . . . . . . . . . 15 $\$
178	177	fneq2d 5982	. . . . . . . . . . . . . 14 $\$
179	138, 178	mpbid 222	. . . . . . . . . . . . 13 $\$
180		eldifsn 4317	. . . . . . . . . . . . . . 15 $\$ $/\$
181	180	biimpri 218	. . . . . . . . . . . . . 14 $/\$ $\$
182	181	ancoms 469	. . . . . . . . . . . . 13 $/\$ $\$
183		disjdif 4040	. . . . . . . . . . . . . 14 $\$
184		fnconstg 6093	. . . . . . . . . . . . . . . 16
185	36, 184	ax-mp 5	. . . . . . . . . . . . . . 15
186		fvun2 6270	. . . . . . . . . . . . . . 15 $/\$ $\$ $/\$ $\$ $/\$ $\$
187	185, 186	mp3an1 1411	. . . . . . . . . . . . . 14 $\$ $/\$ $\$ $/\$ $\$
188	183, 187	mpanr1 719	. . . . . . . . . . . . 13 $\$ $/\$ $\$
189	179, 182, 188	syl2an 494	. . . . . . . . . . . 12 $/\$ $/\$
190	189	anassrs 680	. . . . . . . . . . 11 $/\$ $/\$
191	121, 190	eqtrd 2656	. . . . . . . . . 10 $/\$ $/\$
192	32, 100, 101, 101, 102, 103, 191	ofval 6906	. . . . . . . . 9 $/\$ $/\$
193		fnconstg 6093	. . . . . . . . . . . . . . 15
194	33, 193	ax-mp 5	. . . . . . . . . . . . . 14
195	194, 123	pm3.2i 471	. . . . . . . . . . . . 13 $/\$
196		imain 5974	. . . . . . . . . . . . . . 15
197	42, 196	syl 17	. . . . . . . . . . . . . 14
198		fzdisj 12368	. . . . . . . . . . . . . . . . 17
199	130, 198	syl 17	. . . . . . . . . . . . . . . 16
200	199	imaeq2d 5466	. . . . . . . . . . . . . . 15
201	200, 52	syl6eq 2672	. . . . . . . . . . . . . 14
202	197, 201	eqtr3d 2658	. . . . . . . . . . . . 13
203		fnun 5997	. . . . . . . . . . . . 13 $/\$ $/\$
204	195, 202, 203	sylancr 695	. . . . . . . . . . . 12
205	143	imaeq2d 5466	. . . . . . . . . . . . . . 15
206		imaundi 5545	. . . . . . . . . . . . . . 15
207	205, 206	syl6eq 2672	. . . . . . . . . . . . . 14
208	207, 96	eqtr3d 2658	. . . . . . . . . . . . 13
209	208	fneq2d 5982	. . . . . . . . . . . 12
210	204, 209	mpbid 222	. . . . . . . . . . 11
211	210	adantr 481	. . . . . . . . . 10 $/\$
212		imaundi 5545	. . . . . . . . . . . . . . . . . 18
213	153	imaeq2d 5466	. . . . . . . . . . . . . . . . . 18
214	111	uneq2d 3767	. . . . . . . . . . . . . . . . . 18
215	212, 213, 214	3eqtr4a 2682	. . . . . . . . . . . . . . . . 17
216	215	xpeq1d 5138	. . . . . . . . . . . . . . . 16
217		xpundir 5172	. . . . . . . . . . . . . . . 16
218	216, 217	syl6eq 2672	. . . . . . . . . . . . . . 15
219	218	uneq1d 3766	. . . . . . . . . . . . . 14
220		un23 3772	. . . . . . . . . . . . . . 15
221	220	equncomi 3759	. . . . . . . . . . . . . 14
222	219, 221	syl6eq 2672	. . . . . . . . . . . . 13
223	222	fveq1d 6193	. . . . . . . . . . . 12
224	223	ad2antrr 762	. . . . . . . . . . 11 $/\$ $/\$
225		fnconstg 6093	. . . . . . . . . . . . . . . 16
226	33, 225	ax-mp 5	. . . . . . . . . . . . . . 15
227		fvun2 6270	. . . . . . . . . . . . . . 15 $/\$ $\$ $/\$ $\$ $/\$ $\$
228	226, 227	mp3an1 1411	. . . . . . . . . . . . . 14 $\$ $/\$ $\$ $/\$ $\$
229	183, 228	mpanr1 719	. . . . . . . . . . . . 13 $\$ $/\$ $\$
230	179, 182, 229	syl2an 494	. . . . . . . . . . . 12 $/\$ $/\$
231	230	anassrs 680	. . . . . . . . . . 11 $/\$ $/\$
232	224, 231	eqtrd 2656	. . . . . . . . . 10 $/\$ $/\$
233	32, 211, 101, 101, 102, 103, 232	ofval 6906	. . . . . . . . 9 $/\$ $/\$
234	192, 233	eqtr4d 2659	. . . . . . . 8 $/\$ $/\$
235	234	an32s 846	. . . . . . 7 $/\$ $/\$
236	235	anasss 679	. . . . . 6 $/\$ $/\$
237		fveq2 6191	. . . . . . . . . . . . . . . . . 18
238	237	breq2d 4665	. . . . . . . . . . . . . . . . 17
239	238	ifbid 4108	. . . . . . . . . . . . . . . 16
240	239	csbeq1d 3540	. . . . . . . . . . . . . . 15
241		fveq2 6191	. . . . . . . . . . . . . . . . . 18
242	241	fveq2d 6195	. . . . . . . . . . . . . . . . 17
243	241	fveq2d 6195	. . . . . . . . . . . . . . . . . . . 20
244	243	imaeq1d 5465	. . . . . . . . . . . . . . . . . . 19
245	244	xpeq1d 5138	. . . . . . . . . . . . . . . . . 18
246	243	imaeq1d 5465	. . . . . . . . . . . . . . . . . . 19
247	246	xpeq1d 5138	. . . . . . . . . . . . . . . . . 18
248	245, 247	uneq12d 3768	. . . . . . . . . . . . . . . . 17
249	242, 248	oveq12d 6668	. . . . . . . . . . . . . . . 16
250	249	csbeq2dv 3992	. . . . . . . . . . . . . . 15
251	240, 250	eqtrd 2656	. . . . . . . . . . . . . 14
252	251	mpteq2dv 4745	. . . . . . . . . . . . 13
253	252	eqeq2d 2632	. . . . . . . . . . . 12
254	253, 3	elrab2 3366	. . . . . . . . . . 11 ..^ $/\$
255	254	simprbi 480	. . . . . . . . . 10
256	1, 255	syl 17	. . . . . . . . 9
257		breq1 4656	. . . . . . . . . . . . . 14
258	257	adantl 482	. . . . . . . . . . . . 13 $/\$
259		oveq1 6657	. . . . . . . . . . . . . 14
260		sub1m1 11284	. . . . . . . . . . . . . . . . 17
261	57, 260	syl 17	. . . . . . . . . . . . . . . 16
262	261	oveq1d 6665	. . . . . . . . . . . . . . 15
263	75	zcnd 11483	. . . . . . . . . . . . . . . 16
264		npcan1 10455	. . . . . . . . . . . . . . . 16
265	263, 264	syl 17	. . . . . . . . . . . . . . 15
266	262, 265	eqtr3d 2658	. . . . . . . . . . . . . 14
267	259, 266	sylan9eqr 2678	. . . . . . . . . . . . 13 $/\$
268	258, 267	ifbieq2d 4111	. . . . . . . . . . . 12 $/\$
269	18	nncnd 11036	. . . . . . . . . . . . . . . . 17
270		add1p1 11283	. . . . . . . . . . . . . . . . 17
271	269, 270	syl 17	. . . . . . . . . . . . . . . 16
272	271, 67	eqbrtrrd 4677	. . . . . . . . . . . . . . 15
273	18	nnred 11035	. . . . . . . . . . . . . . . . 17
274		2re 11090	. . . . . . . . . . . . . . . . . 18
275		leaddsub 10504	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
276	274, 275	mp3an2 1412	. . . . . . . . . . . . . . . . 17 $/\$
277	273, 47, 276	syl2anc 693	. . . . . . . . . . . . . . . 16
278	60, 47	posdifd 10614	. . . . . . . . . . . . . . . . . . . . . 22
279	68, 278	mpbid 222	. . . . . . . . . . . . . . . . . . . . 21
280		elnnz 11387	. . . . . . . . . . . . . . . . . . . . 21 $/\$
281	75, 279, 280	sylanbrc 698	. . . . . . . . . . . . . . . . . . . 20
282		nnm1nn0 11334	. . . . . . . . . . . . . . . . . . . 20
283	281, 282	syl 17	. . . . . . . . . . . . . . . . . . 19
284	261, 283	eqeltrrd 2702	. . . . . . . . . . . . . . . . . 18
285	284	nn0red 11352	. . . . . . . . . . . . . . . . 17
286	273, 285	lenltd 10183	. . . . . . . . . . . . . . . 16
287	277, 286	bitrd 268	. . . . . . . . . . . . . . 15
288	272, 287	mpbid 222	. . . . . . . . . . . . . 14
289	288	iffalsed 4097	. . . . . . . . . . . . 13
290	289	adantr 481	. . . . . . . . . . . 12 $/\$
291	268, 290	eqtrd 2656	. . . . . . . . . . 11 $/\$
292	291	csbeq1d 3540	. . . . . . . . . 10 $/\$
293		oveq2 6658	. . . . . . . . . . . . . . . . 17
294	293	imaeq2d 5466	. . . . . . . . . . . . . . . 16
295	294	xpeq1d 5138	. . . . . . . . . . . . . . 15
296	295	adantl 482	. . . . . . . . . . . . . 14 $/\$
297		oveq1 6657	. . . . . . . . . . . . . . . . . 18
298	297, 59	sylan9eqr 2678	. . . . . . . . . . . . . . . . 17 $/\$
299	298	oveq1d 6665	. . . . . . . . . . . . . . . 16 $/\$
300	299	imaeq2d 5466	. . . . . . . . . . . . . . 15 $/\$
301	300	xpeq1d 5138	. . . . . . . . . . . . . 14 $/\$
302	296, 301	uneq12d 3768	. . . . . . . . . . . . 13 $/\$
303	302	oveq2d 6666	. . . . . . . . . . . 12 $/\$
304	75, 303	csbied 3560	. . . . . . . . . . 11
305	304	adantr 481	. . . . . . . . . 10 $/\$
306	292, 305	eqtrd 2656	. . . . . . . . 9 $/\$
307		poimir.0	. . . . . . . . . . 11
308		nnm1nn0 11334	. . . . . . . . . . 11
309	307, 308	syl 17	. . . . . . . . . 10
310	307	nnred 11035	. . . . . . . . . . . 12
311	47	lem1d 10957	. . . . . . . . . . . . 13
312		elfzle2 12345	. . . . . . . . . . . . . 14
313	25, 312	syl 17	. . . . . . . . . . . . 13
314	127, 47, 310, 311, 313	letrd 10194	. . . . . . . . . . . 12
315	127, 310, 60, 314	lesub1dd 10643	. . . . . . . . . . 11
316	261, 315	eqbrtrrd 4677	. . . . . . . . . 10
317		elfz2nn0 12431	. . . . . . . . . 10 $/\$ $/\$
318	284, 309, 316, 317	syl3anbrc 1246	. . . . . . . . 9
319		ovexd 6680	. . . . . . . . 9
320	256, 306, 318, 319	fvmptd 6288	. . . . . . . 8
321	320	fveq1d 6193	. . . . . . 7
322	321	adantr 481	. . . . . 6 $/\$ $/\$
323		breq1 4656	. . . . . . . . . . . . . 14
324	323	adantl 482	. . . . . . . . . . . . 13 $/\$
325		oveq1 6657	. . . . . . . . . . . . . 14
326	325, 59	sylan9eqr 2678	. . . . . . . . . . . . 13 $/\$
327	324, 326	ifbieq2d 4111	. . . . . . . . . . . 12 $/\$
328	62	lep1d 10955	. . . . . . . . . . . . . . . 16
329	62, 61, 47, 328, 67	letrd 10194	. . . . . . . . . . . . . . 15
330		1re 10039	. . . . . . . . . . . . . . . . . 18
331		leaddsub 10504	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
332	330, 331	mp3an2 1412	. . . . . . . . . . . . . . . . 17 $/\$
333	273, 47, 332	syl2anc 693	. . . . . . . . . . . . . . . 16
334	273, 127	lenltd 10183	. . . . . . . . . . . . . . . 16
335	333, 334	bitrd 268	. . . . . . . . . . . . . . 15
336	329, 335	mpbid 222	. . . . . . . . . . . . . 14
337	336	iffalsed 4097	. . . . . . . . . . . . 13
338	337	adantr 481	. . . . . . . . . . . 12 $/\$
339	327, 338	eqtrd 2656	. . . . . . . . . . 11 $/\$
340	339	csbeq1d 3540	. . . . . . . . . 10 $/\$
341		oveq2 6658	. . . . . . . . . . . . . . . . 17
342	341	imaeq2d 5466	. . . . . . . . . . . . . . . 16
343	342	xpeq1d 5138	. . . . . . . . . . . . . . 15
344		oveq1 6657	. . . . . . . . . . . . . . . . . 18
345	344	oveq1d 6665	. . . . . . . . . . . . . . . . 17
346	345	imaeq2d 5466	. . . . . . . . . . . . . . . 16
347	346	xpeq1d 5138	. . . . . . . . . . . . . . 15
348	343, 347	uneq12d 3768	. . . . . . . . . . . . . 14
349	348	oveq2d 6666	. . . . . . . . . . . . 13
350	349	adantl 482	. . . . . . . . . . . 12 $/\$
351	25, 350	csbied 3560	. . . . . . . . . . 11
352	351	adantr 481	. . . . . . . . . 10 $/\$
353	340, 352	eqtrd 2656	. . . . . . . . 9 $/\$
354	281	nnnn0d 11351	. . . . . . . . . 10
355	47, 310, 60, 313	lesub1dd 10643	. . . . . . . . . 10
356		elfz2nn0 12431	. . . . . . . . . 10 $/\$ $/\$
357	354, 309, 355, 356	syl3anbrc 1246	. . . . . . . . 9
358		ovexd 6680	. . . . . . . . 9
359	256, 353, 357, 358	fvmptd 6288	. . . . . . . 8
360	359	fveq1d 6193	. . . . . . 7
361	360	adantr 481	. . . . . 6 $/\$ $/\$
362	236, 322, 361	3eqtr4d 2666	. . . . 5 $/\$ $/\$
363	362	expr 643	. . . 4 $/\$
364	363	necon1d 2816	. . 3 $/\$
365		elmapi 7879	. . . . . . . . . . 11 ..^ ..^
366	29, 365	syl 17	. . . . . . . . . 10 ..^
367	366, 27	ffvelrnd 6360	. . . . . . . . 9 ..^
368		elfzonn0 12512	. . . . . . . . 9 ..^
369	367, 368	syl 17	. . . . . . . 8
370	369	nn0red 11352	. . . . . . 7
371	370	ltp1d 10954	. . . . . . 7
372	370, 371	ltned 10173	. . . . . 6
373	320	fveq1d 6193	. . . . . . 7
374		ovexd 6680	. . . . . . . . 9
375		eqidd 2623	. . . . . . . . 9 $/\$
376		fzss1 12380	. . . . . . . . . . . . . 14
377	72, 376	syl 17	. . . . . . . . . . . . 13
378		eluzfz1 12348	. . . . . . . . . . . . . 14
379	83, 378	syl 17	. . . . . . . . . . . . 13
380		fnfvima 6496	. . . . . . . . . . . . 13 $/\$ $/\$
381	109, 377, 379, 380	syl3anc 1326	. . . . . . . . . . . 12
382		fvun2 6270	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
383	35, 38, 382	mp3an12 1414	. . . . . . . . . . . 12 $/\$
384	54, 381, 383	syl2anc 693	. . . . . . . . . . 11
385	36	fvconst2 6469	. . . . . . . . . . . 12
386	381, 385	syl 17	. . . . . . . . . . 11
387	384, 386	eqtrd 2656	. . . . . . . . . 10
388	387	adantr 481	. . . . . . . . 9 $/\$
389	31, 99, 374, 374, 102, 375, 388	ofval 6906	. . . . . . . 8 $/\$
390	27, 389	mpdan 702	. . . . . . 7
391	369	nn0cnd 11353	. . . . . . . 8
392	391	addid1d 10236	. . . . . . 7
393	373, 390, 392	3eqtrd 2660	. . . . . 6
394	359	fveq1d 6193	. . . . . . 7
395		fzss2 12381	. . . . . . . . . . . . . 14
396	83, 395	syl 17	. . . . . . . . . . . . 13
397		elfz1end 12371	. . . . . . . . . . . . . 14
398	71, 397	sylib 208	. . . . . . . . . . . . 13
399		fnfvima 6496	. . . . . . . . . . . . 13 $/\$ $/\$
400	109, 396, 398, 399	syl3anc 1326	. . . . . . . . . . . 12
401		fvun1 6269	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
402	194, 123, 401	mp3an12 1414	. . . . . . . . . . . 12 $/\$
403	202, 400, 402	syl2anc 693	. . . . . . . . . . 11
404	33	fvconst2 6469	. . . . . . . . . . . 12
405	400, 404	syl 17	. . . . . . . . . . 11
406	403, 405	eqtrd 2656	. . . . . . . . . 10
407	406	adantr 481	. . . . . . . . 9 $/\$
408	31, 210, 374, 374, 102, 375, 407	ofval 6906	. . . . . . . 8 $/\$
409	27, 408	mpdan 702	. . . . . . 7
410	394, 409	eqtrd 2656	. . . . . 6
411	372, 393, 410	3netr4d 2871	. . . . 5
412		fveq2 6191	. . . . . 6
413		fveq2 6191	. . . . . 6
414	412, 413	neeq12d 2855	. . . . 5
415	411, 414	syl5ibrcom 237	. . . 4
416	415	adantr 481	. . 3 $/\$
417	364, 416	impbid 202	. 2 $/\$
418	27, 417	riota5 6637	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 196 $/\$ wa 384

wceq 1483

wcel 1990

cab 2608

wne 2794

crab 2916

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

cima 5117

wfun 5882

wfn 5883

wf 5884

wfo 5886

wf1o 5887

cfv 5888

crio 6610 (class class class)co 6650

cof 6895

c1st 7166

c2nd 7167

cmap 7857

cc 9934

cr 9935

cc0 9936

c1 9937

caddc 9939

clt 10074

cle 10075

cmin 10266

cn 11020

c2 11070

cn0 11292

cz 11377

cuz 11687

cfz 12326 ..^cfzo 12465

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-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-map 7859 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-2 11079 df-n0 11293 df-z 11378 df-uz 11688 df-fz 12327 df-fzo 12466

This theorem is referenced by: poimirlem8 33417

W3C validator