poimirlem19 - Mathbox for Brendan Leahy

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

Theorem poimirlem19 33428

Description: Lemma for poimir 33442 establishing the vertices of the simplex in poimirlem20 33429. (Contributed by Brendan Leahy, 21-Aug-2020.)

**Hypotheses**
Ref	Expression
poimir.0
poimirlem22.s	..^
poimirlem22.1
poimirlem22.2
poimirlem22.3	$/\$
poimirlem21.4

**Assertion**
Ref	Expression
poimirlem19

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

**Proof of Theorem poimirlem19**
Step	Hyp	Ref	Expression
1		poimirlem22.2	. . 3
2		fveq2 6191	. . . . . . . . . . 11
3	2	breq2d 4665	. . . . . . . . . 10
4	3	ifbid 4108	. . . . . . . . 9
5	4	csbeq1d 3540	. . . . . . . 8
6		fveq2 6191	. . . . . . . . . . 11
7	6	fveq2d 6195	. . . . . . . . . 10
8	6	fveq2d 6195	. . . . . . . . . . . . 13
9	8	imaeq1d 5465	. . . . . . . . . . . 12
10	9	xpeq1d 5138	. . . . . . . . . . 11
11	8	imaeq1d 5465	. . . . . . . . . . . 12
12	11	xpeq1d 5138	. . . . . . . . . . 11
13	10, 12	uneq12d 3768	. . . . . . . . . 10
14	7, 13	oveq12d 6668	. . . . . . . . 9
15	14	csbeq2dv 3992	. . . . . . . 8
16	5, 15	eqtrd 2656	. . . . . . 7
17	16	mpteq2dv 4745	. . . . . 6
18	17	eqeq2d 2632	. . . . 5
19		poimirlem22.s	. . . . 5 ..^
20	18, 19	elrab2 3366	. . . 4 ..^ $/\$
21	20	simprbi 480	. . 3
22	1, 21	syl 17	. 2
23		elrabi 3359	. . . . . . . . . . . 12 ..^ ..^
24	23, 19	eleq2s 2719	. . . . . . . . . . 11 ..^
25	1, 24	syl 17	. . . . . . . . . 10 ..^
26		xp1st 7198	. . . . . . . . . 10 ..^ ..^
27	25, 26	syl 17	. . . . . . . . 9 ..^
28		xp1st 7198	. . . . . . . . 9 ..^ ..^
29	27, 28	syl 17	. . . . . . . 8 ..^
30		elmapfn 7880	. . . . . . . 8 ..^
31	29, 30	syl 17	. . . . . . 7
32	31	adantr 481	. . . . . 6 $/\$
33		1ex 10035	. . . . . . . . . 10
34		fnconstg 6093	. . . . . . . . . 10
35	33, 34	ax-mp 5	. . . . . . . . 9
36		c0ex 10034	. . . . . . . . . 10
37		fnconstg 6093	. . . . . . . . . 10
38	36, 37	ax-mp 5	. . . . . . . . 9
39	35, 38	pm3.2i 471	. . . . . . . 8 $/\$
40		xp2nd 7199	. . . . . . . . . . . . 13 ..^
41	27, 40	syl 17	. . . . . . . . . . . 12
42		fvex 6201	. . . . . . . . . . . . 13
43		f1oeq1 6127	. . . . . . . . . . . . 13
44	42, 43	elab 3350	. . . . . . . . . . . 12
45	41, 44	sylib 208	. . . . . . . . . . 11
46		dff1o3 6143	. . . . . . . . . . . 12 $/\$
47	46	simprbi 480	. . . . . . . . . . 11
48	45, 47	syl 17	. . . . . . . . . 10
49		imain 5974	. . . . . . . . . 10
50	48, 49	syl 17	. . . . . . . . 9
51		elfznn0 12433	. . . . . . . . . . . . . 14
52	51	nn0red 11352	. . . . . . . . . . . . 13
53	52	ltp1d 10954	. . . . . . . . . . . 12
54		fzdisj 12368	. . . . . . . . . . . 12
55	53, 54	syl 17	. . . . . . . . . . 11
56	55	imaeq2d 5466	. . . . . . . . . 10
57		ima0 5481	. . . . . . . . . 10
58	56, 57	syl6eq 2672	. . . . . . . . 9
59	50, 58	sylan9req 2677	. . . . . . . 8 $/\$
60		fnun 5997	. . . . . . . 8 $/\$ $/\$
61	39, 59, 60	sylancr 695	. . . . . . 7 $/\$
62		imaundi 5545	. . . . . . . . 9
63		nn0p1nn 11332	. . . . . . . . . . . . . . 15
64	51, 63	syl 17	. . . . . . . . . . . . . 14
65		nnuz 11723	. . . . . . . . . . . . . 14
66	64, 65	syl6eleq 2711	. . . . . . . . . . . . 13
67	66	adantl 482	. . . . . . . . . . . 12 $/\$
68		poimir.0	. . . . . . . . . . . . . . . 16
69	68	nncnd 11036	. . . . . . . . . . . . . . 15
70		npcan1 10455	. . . . . . . . . . . . . . 15
71	69, 70	syl 17	. . . . . . . . . . . . . 14
72	71	adantr 481	. . . . . . . . . . . . 13 $/\$
73		elfzuz3 12339	. . . . . . . . . . . . . . 15
74		peano2uz 11741	. . . . . . . . . . . . . . 15
75	73, 74	syl 17	. . . . . . . . . . . . . 14
76	75	adantl 482	. . . . . . . . . . . . 13 $/\$
77	72, 76	eqeltrrd 2702	. . . . . . . . . . . 12 $/\$
78		fzsplit2 12366	. . . . . . . . . . . 12 $/\$
79	67, 77, 78	syl2anc 693	. . . . . . . . . . 11 $/\$
80	79	imaeq2d 5466	. . . . . . . . . 10 $/\$
81		f1ofo 6144	. . . . . . . . . . . 12
82		foima 6120	. . . . . . . . . . . 12
83	45, 81, 82	3syl 18	. . . . . . . . . . 11
84	83	adantr 481	. . . . . . . . . 10 $/\$
85	80, 84	eqtr3d 2658	. . . . . . . . 9 $/\$
86	62, 85	syl5eqr 2670	. . . . . . . 8 $/\$
87	86	fneq2d 5982	. . . . . . 7 $/\$
88	61, 87	mpbid 222	. . . . . 6 $/\$
89		ovexd 6680	. . . . . 6 $/\$
90		inidm 3822	. . . . . 6
91		eqidd 2623	. . . . . 6 $/\$ $/\$
92		eqidd 2623	. . . . . 6 $/\$ $/\$
93	32, 88, 89, 89, 90, 91, 92	offval 6904	. . . . 5 $/\$
94		elmapi 7879	. . . . . . . . . . . . 13 ..^ ..^
95	29, 94	syl 17	. . . . . . . . . . . 12 ..^
96	95	ffvelrnda 6359	. . . . . . . . . . 11 $/\$ ..^
97		elfzonn0 12512	. . . . . . . . . . 11 ..^
98	96, 97	syl 17	. . . . . . . . . 10 $/\$
99	98	nn0cnd 11353	. . . . . . . . 9 $/\$
100	99	adantlr 751	. . . . . . . 8 $/\$ $/\$
101		ax-1cn 9994	. . . . . . . . . 10
102		0cn 10032	. . . . . . . . . 10
103	101, 102	keepel 4155	. . . . . . . . 9
104	103	a1i 11	. . . . . . . 8 $/\$ $/\$
105		snssi 4339	. . . . . . . . . . 11
106	101, 105	ax-mp 5	. . . . . . . . . 10
107		snssi 4339	. . . . . . . . . . 11
108	102, 107	ax-mp 5	. . . . . . . . . 10
109	106, 108	unssi 3788	. . . . . . . . 9
110	33	fconst 6091	. . . . . . . . . . . . 13
111	36	fconst 6091	. . . . . . . . . . . . 13
112	110, 111	pm3.2i 471	. . . . . . . . . . . 12 $/\$
113		simpr 477	. . . . . . . . . . . . . . . . . . . . 21 $/\$
114	68	nnzd 11481	. . . . . . . . . . . . . . . . . . . . . . 23
115		1z 11407	. . . . . . . . . . . . . . . . . . . . . . . 24
116		peano2z 11418	. . . . . . . . . . . . . . . . . . . . . . . 24
117	115, 116	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23
118	114, 117	jctil 560	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
119		elfzelz 12342	. . . . . . . . . . . . . . . . . . . . . . 23
120	119, 115	jctir 561	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
121		fzsubel 12377	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
122	118, 120, 121	syl2an 494	. . . . . . . . . . . . . . . . . . . . 21 $/\$
123	113, 122	mpbid 222	. . . . . . . . . . . . . . . . . . . 20 $/\$
124	101, 101	pncan3oi 10297	. . . . . . . . . . . . . . . . . . . . 21
125	124	oveq1i 6660	. . . . . . . . . . . . . . . . . . . 20
126	123, 125	syl6eleq 2711	. . . . . . . . . . . . . . . . . . 19 $/\$
127	126	ralrimiva 2966	. . . . . . . . . . . . . . . . . 18
128		simpr 477	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
129		peano2zm 11420	. . . . . . . . . . . . . . . . . . . . . . . . 25
130	114, 129	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24
131	130, 115	jctil 560	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
132		elfzelz 12342	. . . . . . . . . . . . . . . . . . . . . . . 24
133	132, 115	jctir 561	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
134		fzaddel 12375	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
135	131, 133, 134	syl2an 494	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
136	128, 135	mpbid 222	. . . . . . . . . . . . . . . . . . . . 21 $/\$
137	71	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . 22
138	137	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 $/\$
139	136, 138	eleqtrd 2703	. . . . . . . . . . . . . . . . . . . 20 $/\$
140	119	zcnd 11483	. . . . . . . . . . . . . . . . . . . . . . 23
141	132	zcnd 11483	. . . . . . . . . . . . . . . . . . . . . . 23
142		subadd2 10285	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
143	101, 142	mp3an2 1412	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
144		eqcom 2629	. . . . . . . . . . . . . . . . . . . . . . . 24
145		eqcom 2629	. . . . . . . . . . . . . . . . . . . . . . . 24
146	143, 144, 145	3bitr4g 303	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
147	140, 141, 146	syl2anr 495	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
148	147	ralrimiva 2966	. . . . . . . . . . . . . . . . . . . . 21
149	148	adantl 482	. . . . . . . . . . . . . . . . . . . 20 $/\$
150		reu6i 3397	. . . . . . . . . . . . . . . . . . . 20 $/\$
151	139, 149, 150	syl2anc 693	. . . . . . . . . . . . . . . . . . 19 $/\$
152	151	ralrimiva 2966	. . . . . . . . . . . . . . . . . 18
153		eqid 2622	. . . . . . . . . . . . . . . . . . 19
154	153	f1ompt 6382	. . . . . . . . . . . . . . . . . 18 $/\$
155	127, 152, 154	sylanbrc 698	. . . . . . . . . . . . . . . . 17
156		f1osng 6177	. . . . . . . . . . . . . . . . . 18 $/\$
157	33, 68, 156	sylancr 695	. . . . . . . . . . . . . . . . 17
158	68	nnred 11035	. . . . . . . . . . . . . . . . . . . . 21
159	158	ltm1d 10956	. . . . . . . . . . . . . . . . . . . 20
160	130	zred 11482	. . . . . . . . . . . . . . . . . . . . 21
161	160, 158	ltnled 10184	. . . . . . . . . . . . . . . . . . . 20
162	159, 161	mpbid 222	. . . . . . . . . . . . . . . . . . 19
163		elfzle2 12345	. . . . . . . . . . . . . . . . . . 19
164	162, 163	nsyl 135	. . . . . . . . . . . . . . . . . 18
165		disjsn 4246	. . . . . . . . . . . . . . . . . 18
166	164, 165	sylibr 224	. . . . . . . . . . . . . . . . 17
167		1re 10039	. . . . . . . . . . . . . . . . . . . . . 22
168	167	ltp1i 10927	. . . . . . . . . . . . . . . . . . . . 21
169	117	zrei 11383	. . . . . . . . . . . . . . . . . . . . . 22
170	167, 169	ltnlei 10158	. . . . . . . . . . . . . . . . . . . . 21
171	168, 170	mpbi 220	. . . . . . . . . . . . . . . . . . . 20
172		elfzle1 12344	. . . . . . . . . . . . . . . . . . . 20
173	171, 172	mto 188	. . . . . . . . . . . . . . . . . . 19
174		disjsn 4246	. . . . . . . . . . . . . . . . . . 19
175	173, 174	mpbir 221	. . . . . . . . . . . . . . . . . 18
176		f1oun 6156	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
177	175, 176	mpanr1 719	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
178	155, 157, 166, 177	syl21anc 1325	. . . . . . . . . . . . . . . 16
179		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . 23
180	173, 179	mtbiri 317	. . . . . . . . . . . . . . . . . . . . . 22
181	180	necon2ai 2823	. . . . . . . . . . . . . . . . . . . . 21
182		ifnefalse 4098	. . . . . . . . . . . . . . . . . . . . 21
183	181, 182	syl 17	. . . . . . . . . . . . . . . . . . . 20
184	183	mpteq2ia 4740	. . . . . . . . . . . . . . . . . . 19
185	184	uneq1i 3763	. . . . . . . . . . . . . . . . . 18
186	33	a1i 11	. . . . . . . . . . . . . . . . . . 19
187		ssv 3625	. . . . . . . . . . . . . . . . . . . 20
188	187, 68	sseldi 3601	. . . . . . . . . . . . . . . . . . 19
189	68, 65	syl6eleq 2711	. . . . . . . . . . . . . . . . . . . . 21
190		fzpred 12389	. . . . . . . . . . . . . . . . . . . . 21
191	189, 190	syl 17	. . . . . . . . . . . . . . . . . . . 20
192		uncom 3757	. . . . . . . . . . . . . . . . . . . 20
193	191, 192	syl6req 2673	. . . . . . . . . . . . . . . . . . 19
194		iftrue 4092	. . . . . . . . . . . . . . . . . . . 20
195	194	adantl 482	. . . . . . . . . . . . . . . . . . 19 $/\$
196	186, 188, 193, 195	fmptapd 6437	. . . . . . . . . . . . . . . . . 18
197	185, 196	syl5eqr 2670	. . . . . . . . . . . . . . . . 17
198	71, 189	eqeltrd 2701	. . . . . . . . . . . . . . . . . . 19
199		uzid 11702	. . . . . . . . . . . . . . . . . . . . 21
200		peano2uz 11741	. . . . . . . . . . . . . . . . . . . . 21
201	130, 199, 200	3syl 18	. . . . . . . . . . . . . . . . . . . 20
202	71, 201	eqeltrrd 2702	. . . . . . . . . . . . . . . . . . 19
203		fzsplit2 12366	. . . . . . . . . . . . . . . . . . 19 $/\$
204	198, 202, 203	syl2anc 693	. . . . . . . . . . . . . . . . . 18
205	71	oveq1d 6665	. . . . . . . . . . . . . . . . . . . 20
206		fzsn 12383	. . . . . . . . . . . . . . . . . . . . 21
207	114, 206	syl 17	. . . . . . . . . . . . . . . . . . . 20
208	205, 207	eqtrd 2656	. . . . . . . . . . . . . . . . . . 19
209	208	uneq2d 3767	. . . . . . . . . . . . . . . . . 18
210	204, 209	eqtr2d 2657	. . . . . . . . . . . . . . . . 17
211	197, 193, 210	f1oeq123d 6133	. . . . . . . . . . . . . . . 16
212	178, 211	mpbid 222	. . . . . . . . . . . . . . 15
213		f1oco 6159	. . . . . . . . . . . . . . 15 $/\$
214	45, 212, 213	syl2anc 693	. . . . . . . . . . . . . 14
215		dff1o3 6143	. . . . . . . . . . . . . . 15 $/\$
216	215	simprbi 480	. . . . . . . . . . . . . 14
217		imain 5974	. . . . . . . . . . . . . 14
218	214, 216, 217	3syl 18	. . . . . . . . . . . . 13
219	64	nnred 11035	. . . . . . . . . . . . . . . . 17
220	219	ltp1d 10954	. . . . . . . . . . . . . . . 16
221		fzdisj 12368	. . . . . . . . . . . . . . . 16
222	220, 221	syl 17	. . . . . . . . . . . . . . 15
223	222	imaeq2d 5466	. . . . . . . . . . . . . 14
224		ima0 5481	. . . . . . . . . . . . . 14
225	223, 224	syl6eq 2672	. . . . . . . . . . . . 13
226	218, 225	sylan9req 2677	. . . . . . . . . . . 12 $/\$
227		fun 6066	. . . . . . . . . . . 12 $/\$ $/\$
228	112, 226, 227	sylancr 695	. . . . . . . . . . 11 $/\$
229		imaundi 5545	. . . . . . . . . . . . 13
230	64	peano2nnd 11037	. . . . . . . . . . . . . . . . . 18
231	230, 65	syl6eleq 2711	. . . . . . . . . . . . . . . . 17
232	231	adantl 482	. . . . . . . . . . . . . . . 16 $/\$
233		eluzp1p1 11713	. . . . . . . . . . . . . . . . . . 19
234	73, 233	syl 17	. . . . . . . . . . . . . . . . . 18
235	234	adantl 482	. . . . . . . . . . . . . . . . 17 $/\$
236	72, 235	eqeltrrd 2702	. . . . . . . . . . . . . . . 16 $/\$
237		fzsplit2 12366	. . . . . . . . . . . . . . . 16 $/\$
238	232, 236, 237	syl2anc 693	. . . . . . . . . . . . . . 15 $/\$
239	238	imaeq2d 5466	. . . . . . . . . . . . . 14 $/\$
240		f1ofo 6144	. . . . . . . . . . . . . . . 16
241		foima 6120	. . . . . . . . . . . . . . . 16
242	214, 240, 241	3syl 18	. . . . . . . . . . . . . . 15
243	242	adantr 481	. . . . . . . . . . . . . 14 $/\$
244	239, 243	eqtr3d 2658	. . . . . . . . . . . . 13 $/\$
245	229, 244	syl5eqr 2670	. . . . . . . . . . . 12 $/\$
246	245	feq2d 6031	. . . . . . . . . . 11 $/\$
247	228, 246	mpbid 222	. . . . . . . . . 10 $/\$
248	247	ffvelrnda 6359	. . . . . . . . 9 $/\$ $/\$
249	109, 248	sseldi 3601	. . . . . . . 8 $/\$ $/\$
250	100, 104, 249	subadd23d 10414	. . . . . . 7 $/\$ $/\$
251		oveq2 6658	. . . . . . . . . 10
252	251	eqeq1d 2624	. . . . . . . . 9
253		oveq2 6658	. . . . . . . . . 10
254	253	eqeq1d 2624	. . . . . . . . 9
255		1m1e0 11089	. . . . . . . . . . . . 13
256		f1ofn 6138	. . . . . . . . . . . . . . . . . . . 20
257	45, 256	syl 17	. . . . . . . . . . . . . . . . . . 19
258	257	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$
259		imassrn 5477	. . . . . . . . . . . . . . . . . . . 20
260		f1of 6137	. . . . . . . . . . . . . . . . . . . . . 22
261	212, 260	syl 17	. . . . . . . . . . . . . . . . . . . . 21
262		frn 6053	. . . . . . . . . . . . . . . . . . . . 21
263	261, 262	syl 17	. . . . . . . . . . . . . . . . . . . 20
264	259, 263	syl5ss 3614	. . . . . . . . . . . . . . . . . . 19
265	264	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$
266		eqidd 2623	. . . . . . . . . . . . . . . . . . . . 21
267		eluzfz1 12348	. . . . . . . . . . . . . . . . . . . . . 22
268	189, 267	syl 17	. . . . . . . . . . . . . . . . . . . . 21
269	266, 195, 268, 68	fvmptd 6288	. . . . . . . . . . . . . . . . . . . 20
270	269	adantr 481	. . . . . . . . . . . . . . . . . . 19 $/\$
271		f1ofn 6138	. . . . . . . . . . . . . . . . . . . . . 22
272	212, 271	syl 17	. . . . . . . . . . . . . . . . . . . . 21
273	272	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$
274		fzss2 12381	. . . . . . . . . . . . . . . . . . . . 21
275	236, 274	syl 17	. . . . . . . . . . . . . . . . . . . 20 $/\$
276		eluzfz1 12348	. . . . . . . . . . . . . . . . . . . . . 22
277	66, 276	syl 17	. . . . . . . . . . . . . . . . . . . . 21
278	277	adantl 482	. . . . . . . . . . . . . . . . . . . 20 $/\$
279		fnfvima 6496	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
280	273, 275, 278, 279	syl3anc 1326	. . . . . . . . . . . . . . . . . . 19 $/\$
281	270, 280	eqeltrrd 2702	. . . . . . . . . . . . . . . . . 18 $/\$
282		fnfvima 6496	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
283	258, 265, 281, 282	syl3anc 1326	. . . . . . . . . . . . . . . . 17 $/\$
284		imaco 5640	. . . . . . . . . . . . . . . . 17
285	283, 284	syl6eleqr 2712	. . . . . . . . . . . . . . . 16 $/\$
286		fnconstg 6093	. . . . . . . . . . . . . . . . . 18
287	33, 286	ax-mp 5	. . . . . . . . . . . . . . . . 17
288		fnconstg 6093	. . . . . . . . . . . . . . . . . 18
289	36, 288	ax-mp 5	. . . . . . . . . . . . . . . . 17
290		fvun1 6269	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
291	287, 289, 290	mp3an12 1414	. . . . . . . . . . . . . . . 16 $/\$
292	226, 285, 291	syl2anc 693	. . . . . . . . . . . . . . 15 $/\$
293	33	fvconst2 6469	. . . . . . . . . . . . . . . 16
294	285, 293	syl 17	. . . . . . . . . . . . . . 15 $/\$
295	292, 294	eqtrd 2656	. . . . . . . . . . . . . 14 $/\$
296	295	oveq1d 6665	. . . . . . . . . . . . 13 $/\$
297		fzss1 12380	. . . . . . . . . . . . . . . . . 18
298	66, 297	syl 17	. . . . . . . . . . . . . . . . 17
299	298	adantl 482	. . . . . . . . . . . . . . . 16 $/\$
300		eluzfz2 12349	. . . . . . . . . . . . . . . . 17
301	236, 300	syl 17	. . . . . . . . . . . . . . . 16 $/\$
302		fnfvima 6496	. . . . . . . . . . . . . . . 16 $/\$ $/\$
303	258, 299, 301, 302	syl3anc 1326	. . . . . . . . . . . . . . 15 $/\$
304		fvun2 6270	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
305	35, 38, 304	mp3an12 1414	. . . . . . . . . . . . . . 15 $/\$
306	59, 303, 305	syl2anc 693	. . . . . . . . . . . . . 14 $/\$
307	36	fvconst2 6469	. . . . . . . . . . . . . . 15
308	303, 307	syl 17	. . . . . . . . . . . . . 14 $/\$
309	306, 308	eqtrd 2656	. . . . . . . . . . . . 13 $/\$
310	255, 296, 309	3eqtr4a 2682	. . . . . . . . . . . 12 $/\$
311		fveq2 6191	. . . . . . . . . . . . . 14
312	311	oveq1d 6665	. . . . . . . . . . . . 13
313		fveq2 6191	. . . . . . . . . . . . 13
314	312, 313	eqeq12d 2637	. . . . . . . . . . . 12
315	310, 314	syl5ibrcom 237	. . . . . . . . . . 11 $/\$
316	315	imp 445	. . . . . . . . . 10 $/\$ $/\$
317	316	adantlr 751	. . . . . . . . 9 $/\$ $/\$ $/\$
318	249	subid1d 10381	. . . . . . . . . . 11 $/\$ $/\$
319	318	adantr 481	. . . . . . . . . 10 $/\$ $/\$ $/\$
320		eldifsn 4317	. . . . . . . . . . . . . 14 $\$ $/\$
321		df-ne 2795	. . . . . . . . . . . . . . 15
322	321	anbi2i 730	. . . . . . . . . . . . . 14 $/\$ $/\$
323	320, 322	bitri 264	. . . . . . . . . . . . 13 $\$ $/\$
324		fnconstg 6093	. . . . . . . . . . . . . . . . . 18
325	36, 324	ax-mp 5	. . . . . . . . . . . . . . . . 17
326	35, 325	pm3.2i 471	. . . . . . . . . . . . . . . 16 $/\$
327		imain 5974	. . . . . . . . . . . . . . . . . 18
328	48, 327	syl 17	. . . . . . . . . . . . . . . . 17
329		fzdisj 12368	. . . . . . . . . . . . . . . . . . . 20
330	53, 329	syl 17	. . . . . . . . . . . . . . . . . . 19
331	330	imaeq2d 5466	. . . . . . . . . . . . . . . . . 18
332	331, 57	syl6eq 2672	. . . . . . . . . . . . . . . . 17
333	328, 332	sylan9req 2677	. . . . . . . . . . . . . . . 16 $/\$
334		fnun 5997	. . . . . . . . . . . . . . . 16 $/\$ $/\$
335	326, 333, 334	sylancr 695	. . . . . . . . . . . . . . 15 $/\$
336		imaundi 5545	. . . . . . . . . . . . . . . . 17
337	204, 209	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . 24
338	337	difeq1d 3727	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $\$
339		difun2 4048	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $\$
340	338, 339	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$
341		difsn 4328	. . . . . . . . . . . . . . . . . . . . . . 23 $\$
342	164, 341	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 $\$
343	340, 342	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . 21 $\$
344	343	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\$
345	73	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 $/\$
346		fzsplit2 12366	. . . . . . . . . . . . . . . . . . . . 21 $/\$
347	67, 345, 346	syl2anc 693	. . . . . . . . . . . . . . . . . . . 20 $/\$
348	344, 347	eqtrd 2656	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$
349	348	imaeq2d 5466	. . . . . . . . . . . . . . . . . 18 $/\$ $\$
350		imadif 5973	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
351	48, 350	syl 17	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
352		elfz1end 12371	. . . . . . . . . . . . . . . . . . . . . . . 24
353	68, 352	sylib 208	. . . . . . . . . . . . . . . . . . . . . . 23
354		fnsnfv 6258	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
355	257, 353, 354	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . 22
356	355	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . 21
357	83, 356	difeq12d 3729	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
358	351, 357	eqtrd 2656	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
359	358	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$ $\$ $\$
360	349, 359	eqtr3d 2658	. . . . . . . . . . . . . . . . 17 $/\$ $\$
361	336, 360	syl5eqr 2670	. . . . . . . . . . . . . . . 16 $/\$ $\$
362	361	fneq2d 5982	. . . . . . . . . . . . . . 15 $/\$ $\$
363	335, 362	mpbid 222	. . . . . . . . . . . . . 14 $/\$ $\$
364		incom 3805	. . . . . . . . . . . . . . . 16 $\$ $\$
365		disjdif 4040	. . . . . . . . . . . . . . . 16 $\$
366	364, 365	eqtri 2644	. . . . . . . . . . . . . . 15 $\$
367		fnconstg 6093	. . . . . . . . . . . . . . . . . 18
368	33, 367	ax-mp 5	. . . . . . . . . . . . . . . . 17
369		fvun1 6269	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $/\$ $\$ $/\$ $\$
370	368, 369	mp3an2 1412	. . . . . . . . . . . . . . . 16 $\$ $/\$ $\$ $/\$ $\$
371		fnconstg 6093	. . . . . . . . . . . . . . . . . 18
372	36, 371	ax-mp 5	. . . . . . . . . . . . . . . . 17
373		fvun1 6269	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $/\$ $\$ $/\$ $\$
374	372, 373	mp3an2 1412	. . . . . . . . . . . . . . . 16 $\$ $/\$ $\$ $/\$ $\$
375	370, 374	eqtr4d 2659	. . . . . . . . . . . . . . 15 $\$ $/\$ $\$ $/\$ $\$
376	366, 375	mpanr1 719	. . . . . . . . . . . . . 14 $\$ $/\$ $\$
377	363, 376	sylan 488	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
378	323, 377	sylan2br 493	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
379	378	anassrs 680	. . . . . . . . . . 11 $/\$ $/\$ $/\$
380		imaundi 5545	. . . . . . . . . . . . . . . . . . 19
381		imaco 5640	. . . . . . . . . . . . . . . . . . . 20
382		imaco 5640	. . . . . . . . . . . . . . . . . . . 20
383	381, 382	uneq12i 3765	. . . . . . . . . . . . . . . . . . 19
384	380, 383	eqtri 2644	. . . . . . . . . . . . . . . . . 18
385		fzpred 12389	. . . . . . . . . . . . . . . . . . . . . 22
386	66, 385	syl 17	. . . . . . . . . . . . . . . . . . . . 21
387		uncom 3757	. . . . . . . . . . . . . . . . . . . . 21
388	386, 387	syl6eq 2672	. . . . . . . . . . . . . . . . . . . 20
389	388	imaeq2d 5466	. . . . . . . . . . . . . . . . . . 19
390	389	adantl 482	. . . . . . . . . . . . . . . . . 18 $/\$
391		elfzelz 12342	. . . . . . . . . . . . . . . . . . . . . . 23
392	124	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25
393		zcn 11382	. . . . . . . . . . . . . . . . . . . . . . . . . 26
394		pncan1 10454	. . . . . . . . . . . . . . . . . . . . . . . . . 26
395	393, 394	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25
396	392, 395	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . 24
397		elfzelz 12342	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
398	397	zcnd 11483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
399		pncan1 10454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
400	398, 399	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
401	400	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
402	401	ibir 257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
403	402	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
404		peano2z 11418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
405	404, 117	jctil 560	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
406	397	peano2zd 11485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
407	406, 115	jctir 561	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
408		fzsubel 12377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
409	405, 407, 408	syl2an 494	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
410	403, 409	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
411	400	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
412	411	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
413		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
414	413	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
415	414	rspcev 3309	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
416	410, 412, 415	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
417	416	ex 450	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
418		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
419		elfzelz 12342	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
420	419, 115	jctir 561	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
421		fzsubel 12377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
422	405, 420, 421	syl2an 494	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
423	418, 422	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
424		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
425	423, 424	syl5ibrcom 237	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
426	425	rexlimdva 3031	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
427	417, 426	impbid 202	. . . . . . . . . . . . . . . . . . . . . . . . . 26
428		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
429		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
430	429	elrnmpt 5372	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
431	428, 430	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . 26
432	427, 431	syl6bbr 278	. . . . . . . . . . . . . . . . . . . . . . . . 25
433	432	eqrdv 2620	. . . . . . . . . . . . . . . . . . . . . . . 24
434	396, 433	eqtr3d 2658	. . . . . . . . . . . . . . . . . . . . . . 23
435	391, 434	syl 17	. . . . . . . . . . . . . . . . . . . . . 22
436	435	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 $/\$
437		df-ima 5127	. . . . . . . . . . . . . . . . . . . . . 22
438		uzid 11702	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
439		peano2uz 11741	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
440	115, 438, 439	mp2b 10	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
441		fzss1 12380	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
442	440, 441	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . 26
443	442, 275	syl5ss 3614	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
444	443	resmptd 5452	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
445		elfzle1 12344	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
446	171, 445	mto 188	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
447		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
448	446, 447	mtbiri 317	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
449	448	necon2ai 2823	. . . . . . . . . . . . . . . . . . . . . . . . . 26
450	449, 182	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25
451	450	mpteq2ia 4740	. . . . . . . . . . . . . . . . . . . . . . . 24
452	444, 451	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
453	452	rneqd 5353	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
454	437, 453	syl5eq 2668	. . . . . . . . . . . . . . . . . . . . 21 $/\$
455	436, 454	eqtr4d 2659	. . . . . . . . . . . . . . . . . . . 20 $/\$
456	455	imaeq2d 5466	. . . . . . . . . . . . . . . . . . 19 $/\$
457	269	sneqd 4189	. . . . . . . . . . . . . . . . . . . . . . 23
458		fnsnfv 6258	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
459	272, 268, 458	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . 23
460	457, 459	eqtr3d 2658	. . . . . . . . . . . . . . . . . . . . . 22
461	460	imaeq2d 5466	. . . . . . . . . . . . . . . . . . . . 21
462	355, 461	eqtrd 2656	. . . . . . . . . . . . . . . . . . . 20
463	462	adantr 481	. . . . . . . . . . . . . . . . . . 19 $/\$
464	456, 463	uneq12d 3768	. . . . . . . . . . . . . . . . . 18 $/\$
465	384, 390, 464	3eqtr4a 2682	. . . . . . . . . . . . . . . . 17 $/\$
466	465	xpeq1d 5138	. . . . . . . . . . . . . . . 16 $/\$
467		xpundir 5172	. . . . . . . . . . . . . . . 16
468	466, 467	syl6eq 2672	. . . . . . . . . . . . . . 15 $/\$
469		imaco 5640	. . . . . . . . . . . . . . . . 17
470		df-ima 5127	. . . . . . . . . . . . . . . . . . . 20
471		fzss1 12380	. . . . . . . . . . . . . . . . . . . . . . . 24
472	232, 471	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
473	472	resmptd 5452	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
474		1red 10055	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
475	64	nnzd 11481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
476	475	peano2zd 11485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
477	476	zred 11482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
478	64	nnge1d 11063	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
479	474, 219, 477, 478, 220	lelttrd 10195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
480	474, 477	ltnled 10184	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
481	479, 480	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
482		elfzle1 12344	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
483	481, 482	nsyl 135	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
484		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
485	484	notbid 308	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
486	483, 485	syl5ibrcom 237	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
487	486	necon2ad 2809	. . . . . . . . . . . . . . . . . . . . . . . . . 26
488	487	imp 445	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
489	488, 182	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
490	489	mpteq2dva 4744	. . . . . . . . . . . . . . . . . . . . . . 23
491	490	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
492	473, 491	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . 21 $/\$
493	492	rneqd 5353	. . . . . . . . . . . . . . . . . . . 20 $/\$
494	470, 493	syl5eq 2668	. . . . . . . . . . . . . . . . . . 19 $/\$
495		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . 23
496	495	elrnmpt 5372	. . . . . . . . . . . . . . . . . . . . . 22
497	428, 496	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21
498		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
499	114, 476	anim12ci 591	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
500		elfzelz 12342	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
501	500, 115	jctir 561	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
502		fzsubel 12377	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
503	499, 501, 502	syl2an 494	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
504	498, 503	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
505		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . . 24
506	504, 505	syl5ibrcom 237	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
507	506	rexlimdva 3031	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
508		elfzelz 12342	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
509	508	zcnd 11483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
510	509, 399	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
511	510	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
512	511	ibir 257	. . . . . . . . . . . . . . . . . . . . . . . . . 26
513	512	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
514	508	peano2zd 11485	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
515	514, 115	jctir 561	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
516		fzsubel 12377	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
517	499, 515, 516	syl2an 494	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
518	513, 517	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
519	510	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . . . . 25
520	519	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
521	414	rspcev 3309	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
522	518, 520, 521	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
523	522	ex 450	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
524	507, 523	impbid 202	. . . . . . . . . . . . . . . . . . . . 21 $/\$
525	497, 524	syl5bb 272	. . . . . . . . . . . . . . . . . . . 20 $/\$
526	525	eqrdv 2620	. . . . . . . . . . . . . . . . . . 19 $/\$
527	64	nncnd 11036	. . . . . . . . . . . . . . . . . . . . . 22
528		pncan1 10454	. . . . . . . . . . . . . . . . . . . . . 22
529	527, 528	syl 17	. . . . . . . . . . . . . . . . . . . . 21
530	529	oveq1d 6665	. . . . . . . . . . . . . . . . . . . 20
531	530	adantl 482	. . . . . . . . . . . . . . . . . . 19 $/\$
532	494, 526, 531	3eqtrd 2660	. . . . . . . . . . . . . . . . . 18 $/\$
533	532	imaeq2d 5466	. . . . . . . . . . . . . . . . 17 $/\$
534	469, 533	syl5eq 2668	. . . . . . . . . . . . . . . 16 $/\$
535	534	xpeq1d 5138	. . . . . . . . . . . . . . 15 $/\$
536	468, 535	uneq12d 3768	. . . . . . . . . . . . . 14 $/\$
537		un23 3772	. . . . . . . . . . . . . 14
538	536, 537	syl6eq 2672	. . . . . . . . . . . . 13 $/\$
539	538	fveq1d 6193	. . . . . . . . . . . 12 $/\$
540	539	ad2antrr 762	. . . . . . . . . . 11 $/\$ $/\$ $/\$
541		imaundi 5545	. . . . . . . . . . . . . . . . . 18
542		fzsplit2 12366	. . . . . . . . . . . . . . . . . . . . 21 $/\$
543	234, 202, 542	syl2anr 495	. . . . . . . . . . . . . . . . . . . 20 $/\$
544	208	uneq2d 3767	. . . . . . . . . . . . . . . . . . . . 21
545	544	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$
546	543, 545	eqtrd 2656	. . . . . . . . . . . . . . . . . . 19 $/\$
547	546	imaeq2d 5466	. . . . . . . . . . . . . . . . . 18 $/\$
548	355	adantr 481	. . . . . . . . . . . . . . . . . . 19 $/\$
549	548	uneq2d 3767	. . . . . . . . . . . . . . . . . 18 $/\$
550	541, 547, 549	3eqtr4a 2682	. . . . . . . . . . . . . . . . 17 $/\$
551	550	xpeq1d 5138	. . . . . . . . . . . . . . . 16 $/\$
552		xpundir 5172	. . . . . . . . . . . . . . . 16
553	551, 552	syl6eq 2672	. . . . . . . . . . . . . . 15 $/\$
554	553	uneq2d 3767	. . . . . . . . . . . . . 14 $/\$
555		unass 3770	. . . . . . . . . . . . . 14
556	554, 555	syl6eqr 2674	. . . . . . . . . . . . 13 $/\$
557	556	fveq1d 6193	. . . . . . . . . . . 12 $/\$
558	557	ad2antrr 762	. . . . . . . . . . 11 $/\$ $/\$ $/\$
559	379, 540, 558	3eqtr4d 2666	. . . . . . . . . 10 $/\$ $/\$ $/\$
560	319, 559	eqtrd 2656	. . . . . . . . 9 $/\$ $/\$ $/\$
561	252, 254, 317, 560	ifbothda 4123	. . . . . . . 8 $/\$ $/\$
562	561	oveq2d 6666	. . . . . . 7 $/\$ $/\$
563	250, 562	eqtr2d 2657	. . . . . 6 $/\$ $/\$
564	563	mpteq2dva 4744	. . . . 5 $/\$
565	93, 564	eqtrd 2656	. . . 4 $/\$
566	52	adantl 482	. . . . . . . . 9 $/\$
567	160	adantr 481	. . . . . . . . 9 $/\$
568	158	adantr 481	. . . . . . . . 9 $/\$
569		elfzle2 12345	. . . . . . . . . 10
570	569	adantl 482	. . . . . . . . 9 $/\$
571	159	adantr 481	. . . . . . . . 9 $/\$
572	566, 567, 568, 570, 571	lelttrd 10195	. . . . . . . 8 $/\$
573		poimirlem21.4	. . . . . . . . 9
574	573	adantr 481	. . . . . . . 8 $/\$
575	572, 574	breqtrrd 4681	. . . . . . 7 $/\$
576	575	iftrued 4094	. . . . . 6 $/\$
577	576	csbeq1d 3540	. . . . 5 $/\$
578		vex 3203	. . . . . 6
579		oveq2 6658	. . . . . . . . . 10
580	579	imaeq2d 5466	. . . . . . . . 9
581	580	xpeq1d 5138	. . . . . . . 8
582		oveq1 6657	. . . . . . . . . . 11
583	582	oveq1d 6665	. . . . . . . . . 10
584	583	imaeq2d 5466	. . . . . . . . 9
585	584	xpeq1d 5138	. . . . . . . 8
586	581, 585	uneq12d 3768	. . . . . . 7
587	586	oveq2d 6666	. . . . . 6
588	578, 587	csbie 3559	. . . . 5
589	577, 588	syl6eq 2672	. . . 4 $/\$
590		ovexd 6680	. . . . 5 $/\$ $/\$
591		fvexd 6203	. . . . 5 $/\$ $/\$
592		eqidd 2623	. . . . 5 $/\$
593		ffn 6045	. . . . . . 7
594	247, 593	syl 17	. . . . . 6 $/\$
595		nfcv 2764	. . . . . . . . . . 11
596		nfmpt1 4747	. . . . . . . . . . 11
597	595, 596	nfco 5287	. . . . . . . . . 10
598		nfcv 2764	. . . . . . . . . 10
599	597, 598	nfima 5474	. . . . . . . . 9
600		nfcv 2764	. . . . . . . . 9
601	599, 600	nfxp 5142	. . . . . . . 8
602		nfcv 2764	. . . . . . . . . 10
603	597, 602	nfima 5474	. . . . . . . . 9
604		nfcv 2764	. . . . . . . . 9
605	603, 604	nfxp 5142	. . . . . . . 8
606	601, 605	nfun 3769	. . . . . . 7
607	606	dffn5f 6252	. . . . . 6
608	594, 607	sylib 208	. . . . 5 $/\$
609	89, 590, 591, 592, 608	offval2 6914	. . . 4 $/\$
610	565, 589, 609	3eqtr4rd 2667	. . 3 $/\$
611	610	mpteq2dva 4744	. 2
612	22, 611	eqtr4d 2659	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

wral 2912

wrex 2913

wreu 2914

crab 2916

cvv 3200

csb 3533 $\$ cdif 3571

cun 3572

cin 3573

wss 3574

c0 3915

cif 4086

csn 4177

cop 4183 class class class wbr 4653

cmpt 4729

cxp 5112

ccnv 5113

crn 5115

cres 5116

cima 5117

ccom 5118

wfun 5882

wfn 5883

wf 5884

wfo 5886

wf1o 5887

cfv 5888 (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

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

This theorem is referenced by: poimirlem20 33429

W3C validator