poimirlem28 - Mathbox for Brendan Leahy

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

Theorem poimirlem28 33437

Description: Lemma for poimir 33442, a variant of Sperner's lemma. (Contributed by Brendan Leahy, 21-Aug-2020.)

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

**Assertion**
Ref	Expression
poimirlem28	..^

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

Proof of Theorem poimirlem28 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		poimir.0	. . . . . 6
2	1	nnnn0d 11351	. . . . 5
3	1	nnred 11035	. . . . . 6
4	3	leidd 10594	. . . . 5
5	2, 2, 4	3jca 1242	. . . 4 $/\$ $/\$
6		oveq2 6658	. . . . . . . . . . . . . . . 16
7		fz10 12362	. . . . . . . . . . . . . . . 16
8	6, 7	syl6eq 2672	. . . . . . . . . . . . . . 15
9	8	oveq2d 6666	. . . . . . . . . . . . . 14 ..^ ..^
10		fzofi 12773	. . . . . . . . . . . . . . . 16 ..^
11		map0e 7895	. . . . . . . . . . . . . . . 16 ..^ ..^
12	10, 11	ax-mp 5	. . . . . . . . . . . . . . 15 ..^
13		df1o2 7572	. . . . . . . . . . . . . . 15
14	12, 13	eqtri 2644	. . . . . . . . . . . . . 14 ..^
15	9, 14	syl6eq 2672	. . . . . . . . . . . . 13 ..^
16		eqidd 2623	. . . . . . . . . . . . . . . . 17
17	16, 8, 8	f1oeq123d 6133	. . . . . . . . . . . . . . . 16
18		eqid 2622	. . . . . . . . . . . . . . . . 17
19		f1o00 6171	. . . . . . . . . . . . . . . . 17 $/\$
20	18, 19	mpbiran2 954	. . . . . . . . . . . . . . . 16
21	17, 20	syl6bb 276	. . . . . . . . . . . . . . 15
22	21	abbidv 2741	. . . . . . . . . . . . . 14
23		df-sn 4178	. . . . . . . . . . . . . 14
24	22, 23	syl6eqr 2674	. . . . . . . . . . . . 13
25	15, 24	xpeq12d 5140	. . . . . . . . . . . 12 ..^
26		0ex 4790	. . . . . . . . . . . . 13
27	26, 26	xpsn 6407	. . . . . . . . . . . 12
28	25, 27	syl6req 2673	. . . . . . . . . . 11 ..^
29		elsni 4194	. . . . . . . . . . . . . . . . . . 19
30	26, 26	op1std 7178	. . . . . . . . . . . . . . . . . . 19
31	29, 30	syl 17	. . . . . . . . . . . . . . . . . 18
32	31	oveq1d 6665	. . . . . . . . . . . . . . . . 17
33		f0 6086	. . . . . . . . . . . . . . . . . . . 20
34		ffn 6045	. . . . . . . . . . . . . . . . . . . 20
35	33, 34	mp1i 13	. . . . . . . . . . . . . . . . . . 19
36	26	a1i 11	. . . . . . . . . . . . . . . . . . 19
37		inidm 3822	. . . . . . . . . . . . . . . . . . 19
38		0fv 6227	. . . . . . . . . . . . . . . . . . . 20
39	38	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$
40	35, 35, 36, 36, 37, 39, 39	offval 6904	. . . . . . . . . . . . . . . . . 18
41		mpt0 6021	. . . . . . . . . . . . . . . . . 18
42	40, 41	syl6eq 2672	. . . . . . . . . . . . . . . . 17
43	32, 42	eqtrd 2656	. . . . . . . . . . . . . . . 16
44	43	uneq1d 3766	. . . . . . . . . . . . . . 15
45		uncom 3757	. . . . . . . . . . . . . . . 16
46		un0 3967	. . . . . . . . . . . . . . . 16
47	45, 46	eqtri 2644	. . . . . . . . . . . . . . 15
48	44, 47	syl6req 2673	. . . . . . . . . . . . . 14
49	48	csbeq1d 3540	. . . . . . . . . . . . 13
50	49	eqeq2d 2632	. . . . . . . . . . . 12
51		oveq2 6658	. . . . . . . . . . . . . . 15
52		0z 11388	. . . . . . . . . . . . . . . 16
53		fzsn 12383	. . . . . . . . . . . . . . . 16
54	52, 53	ax-mp 5	. . . . . . . . . . . . . . 15
55	51, 54	syl6eq 2672	. . . . . . . . . . . . . 14
56		oveq2 6658	. . . . . . . . . . . . . . . . . . . . . . 23
57	56	imaeq2d 5466	. . . . . . . . . . . . . . . . . . . . . 22
58	57	xpeq1d 5138	. . . . . . . . . . . . . . . . . . . . 21
59	58	uneq2d 3767	. . . . . . . . . . . . . . . . . . . 20
60	59	oveq2d 6666	. . . . . . . . . . . . . . . . . . 19
61		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . 22
62		0p1e1 11132	. . . . . . . . . . . . . . . . . . . . . 22
63	61, 62	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . 21
64	63	oveq1d 6665	. . . . . . . . . . . . . . . . . . . 20
65	64	xpeq1d 5138	. . . . . . . . . . . . . . . . . . 19
66	60, 65	uneq12d 3768	. . . . . . . . . . . . . . . . . 18
67	66	csbeq1d 3540	. . . . . . . . . . . . . . . . 17
68	67	eqeq2d 2632	. . . . . . . . . . . . . . . 16
69	55, 68	rexeqbidv 3153	. . . . . . . . . . . . . . 15
70		c0ex 10034	. . . . . . . . . . . . . . . 16
71		oveq2 6658	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
72	71, 7	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . . . . . 26
73	72	imaeq2d 5466	. . . . . . . . . . . . . . . . . . . . . . . . 25
74		ima0 5481	. . . . . . . . . . . . . . . . . . . . . . . . 25
75	73, 74	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . . . 24
76	75	xpeq1d 5138	. . . . . . . . . . . . . . . . . . . . . . 23
77		0xp 5199	. . . . . . . . . . . . . . . . . . . . . . 23
78	76, 77	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . 22
79		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
80	79, 62	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
81	80	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
82	81, 7	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . . . . . 26
83	82	imaeq2d 5466	. . . . . . . . . . . . . . . . . . . . . . . . 25
84	83, 74	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . . . 24
85	84	xpeq1d 5138	. . . . . . . . . . . . . . . . . . . . . . 23
86		0xp 5199	. . . . . . . . . . . . . . . . . . . . . . 23
87	85, 86	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . 22
88	78, 87	uneq12d 3768	. . . . . . . . . . . . . . . . . . . . 21
89		un0 3967	. . . . . . . . . . . . . . . . . . . . 21
90	88, 89	syl6eq 2672	. . . . . . . . . . . . . . . . . . . 20
91	90	oveq2d 6666	. . . . . . . . . . . . . . . . . . 19
92	91	uneq1d 3766	. . . . . . . . . . . . . . . . . 18
93	92	csbeq1d 3540	. . . . . . . . . . . . . . . . 17
94	93	eqeq2d 2632	. . . . . . . . . . . . . . . 16
95	70, 94	rexsn 4223	. . . . . . . . . . . . . . 15
96	69, 95	syl6bb 276	. . . . . . . . . . . . . 14
97	55, 96	raleqbidv 3152	. . . . . . . . . . . . 13
98		eqeq1 2626	. . . . . . . . . . . . . 14
99	70, 98	ralsn 4222	. . . . . . . . . . . . 13
100	97, 99	syl6rbb 277	. . . . . . . . . . . 12
101	50, 100	sylan9bbr 737	. . . . . . . . . . 11 $/\$
102	28, 101	rabeqbidva 3196	. . . . . . . . . 10 ..^
103	102	eqcomd 2628	. . . . . . . . 9 ..^
104	103	fveq2d 6195	. . . . . . . 8 ..^
105	104	breq2d 4665	. . . . . . 7 ..^
106	105	notbid 308	. . . . . 6 ..^
107	106	imbi2d 330	. . . . 5 ..^
108		oveq2 6658	. . . . . . . . . . . 12
109	108	oveq2d 6666	. . . . . . . . . . 11 ..^ ..^
110		eqidd 2623	. . . . . . . . . . . . 13
111	110, 108, 108	f1oeq123d 6133	. . . . . . . . . . . 12
112	111	abbidv 2741	. . . . . . . . . . 11
113	109, 112	xpeq12d 5140	. . . . . . . . . 10 ..^ ..^
114		oveq2 6658	. . . . . . . . . . 11
115		oveq2 6658	. . . . . . . . . . . . . . . . . . 19
116	115	imaeq2d 5466	. . . . . . . . . . . . . . . . . 18
117	116	xpeq1d 5138	. . . . . . . . . . . . . . . . 17
118	117	uneq2d 3767	. . . . . . . . . . . . . . . 16
119	118	oveq2d 6666	. . . . . . . . . . . . . . 15
120		oveq1 6657	. . . . . . . . . . . . . . . . 17
121	120	oveq1d 6665	. . . . . . . . . . . . . . . 16
122	121	xpeq1d 5138	. . . . . . . . . . . . . . 15
123	119, 122	uneq12d 3768	. . . . . . . . . . . . . 14
124	123	csbeq1d 3540	. . . . . . . . . . . . 13
125	124	eqeq2d 2632	. . . . . . . . . . . 12
126	114, 125	rexeqbidv 3153	. . . . . . . . . . 11
127	114, 126	raleqbidv 3152	. . . . . . . . . 10
128	113, 127	rabeqbidv 3195	. . . . . . . . 9 ..^ ..^
129	128	fveq2d 6195	. . . . . . . 8 ..^ ..^
130	129	breq2d 4665	. . . . . . 7 ..^ ..^
131	130	notbid 308	. . . . . 6 ..^ ..^
132	131	imbi2d 330	. . . . 5 ..^ ..^
133		oveq2 6658	. . . . . . . . . . . 12
134	133	oveq2d 6666	. . . . . . . . . . 11 ..^ ..^
135		eqidd 2623	. . . . . . . . . . . . 13
136	135, 133, 133	f1oeq123d 6133	. . . . . . . . . . . 12
137	136	abbidv 2741	. . . . . . . . . . 11
138	134, 137	xpeq12d 5140	. . . . . . . . . 10 ..^ ..^
139		oveq2 6658	. . . . . . . . . . 11
140		oveq2 6658	. . . . . . . . . . . . . . . . . . 19
141	140	imaeq2d 5466	. . . . . . . . . . . . . . . . . 18
142	141	xpeq1d 5138	. . . . . . . . . . . . . . . . 17
143	142	uneq2d 3767	. . . . . . . . . . . . . . . 16
144	143	oveq2d 6666	. . . . . . . . . . . . . . 15
145		oveq1 6657	. . . . . . . . . . . . . . . . 17
146	145	oveq1d 6665	. . . . . . . . . . . . . . . 16
147	146	xpeq1d 5138	. . . . . . . . . . . . . . 15
148	144, 147	uneq12d 3768	. . . . . . . . . . . . . 14
149	148	csbeq1d 3540	. . . . . . . . . . . . 13
150	149	eqeq2d 2632	. . . . . . . . . . . 12
151	139, 150	rexeqbidv 3153	. . . . . . . . . . 11
152	139, 151	raleqbidv 3152	. . . . . . . . . 10
153	138, 152	rabeqbidv 3195	. . . . . . . . 9 ..^ ..^
154	153	fveq2d 6195	. . . . . . . 8 ..^ ..^
155	154	breq2d 4665	. . . . . . 7 ..^ ..^
156	155	notbid 308	. . . . . 6 ..^ ..^
157	156	imbi2d 330	. . . . 5 ..^ ..^
158		oveq2 6658	. . . . . . . . . . . 12
159	158	oveq2d 6666	. . . . . . . . . . 11 ..^ ..^
160		eqidd 2623	. . . . . . . . . . . . 13
161	160, 158, 158	f1oeq123d 6133	. . . . . . . . . . . 12
162	161	abbidv 2741	. . . . . . . . . . 11
163	159, 162	xpeq12d 5140	. . . . . . . . . 10 ..^ ..^
164		oveq2 6658	. . . . . . . . . . 11
165		oveq2 6658	. . . . . . . . . . . . . . . . . . 19
166	165	imaeq2d 5466	. . . . . . . . . . . . . . . . . 18
167	166	xpeq1d 5138	. . . . . . . . . . . . . . . . 17
168	167	uneq2d 3767	. . . . . . . . . . . . . . . 16
169	168	oveq2d 6666	. . . . . . . . . . . . . . 15
170		oveq1 6657	. . . . . . . . . . . . . . . . 17
171	170	oveq1d 6665	. . . . . . . . . . . . . . . 16
172	171	xpeq1d 5138	. . . . . . . . . . . . . . 15
173	169, 172	uneq12d 3768	. . . . . . . . . . . . . 14
174	173	csbeq1d 3540	. . . . . . . . . . . . 13
175	174	eqeq2d 2632	. . . . . . . . . . . 12
176	164, 175	rexeqbidv 3153	. . . . . . . . . . 11
177	164, 176	raleqbidv 3152	. . . . . . . . . 10
178	163, 177	rabeqbidv 3195	. . . . . . . . 9 ..^ ..^
179	178	fveq2d 6195	. . . . . . . 8 ..^ ..^
180	179	breq2d 4665	. . . . . . 7 ..^ ..^
181	180	notbid 308	. . . . . 6 ..^ ..^
182	181	imbi2d 330	. . . . 5 ..^ ..^
183		n2dvds1 15104	. . . . . . 7
184		opex 4932	. . . . . . . . . 10
185		hashsng 13159	. . . . . . . . . 10
186	184, 185	ax-mp 5	. . . . . . . . 9
187		nnuz 11723	. . . . . . . . . . . . . . . . 17
188	1, 187	syl6eleq 2711	. . . . . . . . . . . . . . . 16
189		eluzfz1 12348	. . . . . . . . . . . . . . . 16
190	188, 189	syl 17	. . . . . . . . . . . . . . 15
191		poimirlem28.5	. . . . . . . . . . . . . . . . 17
192	191	nnnn0d 11351	. . . . . . . . . . . . . . . 16
193		0elfz 12436	. . . . . . . . . . . . . . . 16
194		fconst6g 6094	. . . . . . . . . . . . . . . 16
195	192, 193, 194	3syl 18	. . . . . . . . . . . . . . 15
196	70	fvconst2 6469	. . . . . . . . . . . . . . . 16
197	190, 196	syl 17	. . . . . . . . . . . . . . 15
198	190, 195, 197	3jca 1242	. . . . . . . . . . . . . 14 $/\$ $/\$
199		nfv 1843	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
200		nfcsb1v 3549	. . . . . . . . . . . . . . . . 17
201	200	nfeq1 2778	. . . . . . . . . . . . . . . 16
202	199, 201	nfim 1825	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
203		ovex 6678	. . . . . . . . . . . . . . . 16
204		snex 4908	. . . . . . . . . . . . . . . 16
205	203, 204	xpex 6962	. . . . . . . . . . . . . . 15
206		feq1 6026	. . . . . . . . . . . . . . . . . 18
207		fveq1 6190	. . . . . . . . . . . . . . . . . . 19
208	207	eqeq1d 2624	. . . . . . . . . . . . . . . . . 18
209	206, 208	3anbi23d 1402	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
210	209	anbi2d 740	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
211		csbeq1a 3542	. . . . . . . . . . . . . . . . 17
212	211	eqeq1d 2624	. . . . . . . . . . . . . . . 16
213	210, 212	imbi12d 334	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
214		1ex 10035	. . . . . . . . . . . . . . . . 17
215		eleq1 2689	. . . . . . . . . . . . . . . . . . . 20
216		fveq2 6191	. . . . . . . . . . . . . . . . . . . . 21
217	216	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . 20
218	215, 217	3anbi13d 1401	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
219	218	anbi2d 740	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
220		breq2 4657	. . . . . . . . . . . . . . . . . 18
221	219, 220	imbi12d 334	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
222		poimirlem28.3	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
223	214, 221, 222	vtocl 3259	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
224		poimirlem28.2	. . . . . . . . . . . . . . . . . 18 $/\$
225		elfznn0 12433	. . . . . . . . . . . . . . . . . 18
226		nn0lt10b 11439	. . . . . . . . . . . . . . . . . 18
227	224, 225, 226	3syl 18	. . . . . . . . . . . . . . . . 17 $/\$
228	227	3ad2antr2 1227	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
229	223, 228	mpbid 222	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
230	202, 205, 213, 229	vtoclf 3258	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
231	198, 230	mpdan 702	. . . . . . . . . . . . 13
232	231	eqcomd 2628	. . . . . . . . . . . 12
233	232	ralrimivw 2967	. . . . . . . . . . 11
234		rabid2 3118	. . . . . . . . . . 11
235	233, 234	sylibr 224	. . . . . . . . . 10
236	235	fveq2d 6195	. . . . . . . . 9
237	186, 236	syl5eqr 2670	. . . . . . . 8
238	237	breq2d 4665	. . . . . . 7
239	183, 238	mtbii 316	. . . . . 6
240	239	a1i 11	. . . . 5
241		2z 11409	. . . . . . . . . . . . 13
242		fzfi 12771	. . . . . . . . . . . . . . . . 17
243		mapfi 8262	. . . . . . . . . . . . . . . . 17 ..^ $/\$ ..^
244	10, 242, 243	mp2an 708	. . . . . . . . . . . . . . . 16 ..^
245		ovex 6678	. . . . . . . . . . . . . . . . . . 19
246	245, 245	mapval 7869	. . . . . . . . . . . . . . . . . 18
247		mapfi 8262	. . . . . . . . . . . . . . . . . . 19 $/\$
248	242, 242, 247	mp2an 708	. . . . . . . . . . . . . . . . . 18
249	246, 248	eqeltrri 2698	. . . . . . . . . . . . . . . . 17
250		f1of 6137	. . . . . . . . . . . . . . . . . 18
251	250	ss2abi 3674	. . . . . . . . . . . . . . . . 17
252		ssfi 8180	. . . . . . . . . . . . . . . . 17 $/\$
253	249, 251, 252	mp2an 708	. . . . . . . . . . . . . . . 16
254		xpfi 8231	. . . . . . . . . . . . . . . 16 ..^ $/\$ ..^
255	244, 253, 254	mp2an 708	. . . . . . . . . . . . . . 15 ..^
256		rabfi 8185	. . . . . . . . . . . . . . 15 ..^ ..^
257		hashcl 13147	. . . . . . . . . . . . . . 15 ..^ ..^
258	255, 256, 257	mp2b 10	. . . . . . . . . . . . . 14 ..^
259	258	nn0zi 11402	. . . . . . . . . . . . 13 ..^
260		rabfi 8185	. . . . . . . . . . . . . . 15 ..^ ..^ $/\$ $/\$
261		hashcl 13147	. . . . . . . . . . . . . . 15 ..^ $/\$ $/\$ ..^ $/\$ $/\$
262	255, 260, 261	mp2b 10	. . . . . . . . . . . . . 14 ..^ $/\$ $/\$
263	262	nn0zi 11402	. . . . . . . . . . . . 13 ..^ $/\$ $/\$
264	241, 259, 263	3pm3.2i 1239	. . . . . . . . . . . 12 $/\$ ..^ $/\$ ..^ $/\$ $/\$
265		nn0p1nn 11332	. . . . . . . . . . . . . . . 16
266	265	ad2antrl 764	. . . . . . . . . . . . . . 15 $/\$ $/\$
267		uneq1 3760	. . . . . . . . . . . . . . . 16
268	267	csbeq1d 3540	. . . . . . . . . . . . . . 15
269	70	fconst 6091	. . . . . . . . . . . . . . . . . . . . . . . 24
270	269	jctr 565	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
271	265	nnred 11035	. . . . . . . . . . . . . . . . . . . . . . . . 25
272	271	ltp1d 10954	. . . . . . . . . . . . . . . . . . . . . . . 24
273		fzdisj 12368	. . . . . . . . . . . . . . . . . . . . . . . 24
274	272, 273	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23
275		fun 6066	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
276	270, 274, 275	syl2anr 495	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
277	276	adantlr 751	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
278	277	adantl 482	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
279	265	peano2nnd 11037	. . . . . . . . . . . . . . . . . . . . . . . . . 26
280	279, 187	syl6eleq 2711	. . . . . . . . . . . . . . . . . . . . . . . . 25
281	280	ad2antrl 764	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
282		nn0z 11400	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
283	1	nnzd 11481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
284		zltp1le 11427	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
285	282, 283, 284	syl2anr 495	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
286	285	biimpa 501	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
287	286	anasss 679	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
288	282	peano2zd 11485	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
289	288	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
290		eluz 11701	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
291	289, 283, 290	syl2anr 495	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
292	287, 291	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
293		fzsplit2 12366	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
294	281, 292, 293	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
295	294	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
296	192, 193	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25
297	296	snssd 4340	. . . . . . . . . . . . . . . . . . . . . . . 24
298		ssequn2 3786	. . . . . . . . . . . . . . . . . . . . . . . 24
299	297, 298	sylib 208	. . . . . . . . . . . . . . . . . . . . . . 23
300	299	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
301	295, 300	feq23d 6040	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
302	301	adantrr 753	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
303	278, 302	mpbid 222	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
304		nfv 1843	. . . . . . . . . . . . . . . . . . . . 21 $/\$
305		nfcsb1v 3549	. . . . . . . . . . . . . . . . . . . . . 22
306	305	nfel1 2779	. . . . . . . . . . . . . . . . . . . . 21
307	304, 306	nfim 1825	. . . . . . . . . . . . . . . . . . . 20 $/\$
308		vex 3203	. . . . . . . . . . . . . . . . . . . . 21
309		ovex 6678	. . . . . . . . . . . . . . . . . . . . . 22
310	309, 204	xpex 6962	. . . . . . . . . . . . . . . . . . . . 21
311	308, 310	unex 6956	. . . . . . . . . . . . . . . . . . . 20
312		feq1 6026	. . . . . . . . . . . . . . . . . . . . . 22
313	312	anbi2d 740	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
314		csbeq1a 3542	. . . . . . . . . . . . . . . . . . . . . 22
315	314	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . 21
316	313, 315	imbi12d 334	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
317	307, 311, 316, 224	vtoclf 3258	. . . . . . . . . . . . . . . . . . 19 $/\$
318	303, 317	syldan 487	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
319	318	anassrs 680	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
320		elfznn0 12433	. . . . . . . . . . . . . . . . 17
321	319, 320	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
322	265	nnnn0d 11351	. . . . . . . . . . . . . . . . . 18
323	322	adantr 481	. . . . . . . . . . . . . . . . 17 $/\$
324	323	ad2antlr 763	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
325		leloe 10124	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\/$
326	271, 3, 325	syl2anr 495	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\/$
327	285, 326	bitrd 268	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\/$
328	327	biimpd 219	. . . . . . . . . . . . . . . . . . 19 $/\$ $\/$
329	328	imdistani 726	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $\/$
330	329	anasss 679	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $\/$
331		simplll 798	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
332	279	nnge1d 11063	. . . . . . . . . . . . . . . . . . . . . . . 24
333	332	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
334		zltp1le 11427	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
335	288, 283, 334	syl2anr 495	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
336	335	biimpa 501	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
337	288	peano2zd 11485	. . . . . . . . . . . . . . . . . . . . . . . . 25
338		1z 11407	. . . . . . . . . . . . . . . . . . . . . . . . . 26
339		elfz 12332	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
340	338, 339	mp3an2 1412	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
341	337, 283, 340	syl2anr 495	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
342	341	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
343	333, 336, 342	mpbir2and 957	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
344	343	adantlr 751	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
345		nn0re 11301	. . . . . . . . . . . . . . . . . . . . . . . . 25
346	345	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
347	271	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
348	3	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
349	345	ltp1d 10954	. . . . . . . . . . . . . . . . . . . . . . . . 25
350	349	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
351		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
352	346, 347, 348, 350, 351	lttrd 10198	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
353	352	adantlr 751	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
354		anass 681	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$
355	303	anassrs 680	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
356	354, 355	sylanb 489	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
357	356	an32s 846	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
358	353, 357	syldan 487	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
359		ffn 6045	. . . . . . . . . . . . . . . . . . . . . . . 24
360	359	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
361	274	ad3antlr 767	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
362		eluz 11701	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
363	337, 283, 362	syl2anr 495	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
364	363	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
365	336, 364	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
366		eluzfz1 12348	. . . . . . . . . . . . . . . . . . . . . . . . 25
367	365, 366	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
368	367	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
369		fnconstg 6093	. . . . . . . . . . . . . . . . . . . . . . . . 25
370	70, 369	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24
371		fvun2 6270	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
372	370, 371	mp3an2 1412	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
373	360, 361, 368, 372	syl12anc 1324	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
374	70	fvconst2 6469	. . . . . . . . . . . . . . . . . . . . . . 23
375	368, 374	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
376	373, 375	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
377		nfv 1843	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
378		nfcv 2764	. . . . . . . . . . . . . . . . . . . . . . . 24
379		nfcv 2764	. . . . . . . . . . . . . . . . . . . . . . . 24
380	305, 378, 379	nfbr 4699	. . . . . . . . . . . . . . . . . . . . . . 23
381	377, 380	nfim 1825	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
382		fveq1 6190	. . . . . . . . . . . . . . . . . . . . . . . . . 26
383	382	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . . . . . 25
384	312, 383	3anbi23d 1402	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$
385	384	anbi2d 740	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
386	314	breq1d 4663	. . . . . . . . . . . . . . . . . . . . . . 23
387	385, 386	imbi12d 334	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
388		ovex 6678	. . . . . . . . . . . . . . . . . . . . . . 23
389		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . . . . 26
390		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
391	390	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . . . . . . 26
392	389, 391	3anbi13d 1401	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$
393	392	anbi2d 740	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
394		breq2 4657	. . . . . . . . . . . . . . . . . . . . . . . 24
395	393, 394	imbi12d 334	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
396	388, 395, 222	vtocl 3259	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
397	381, 311, 387, 396	vtoclf 3258	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
398	331, 344, 358, 376, 397	syl13anc 1328	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
399	354, 319	sylanb 489	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
400	399	an32s 846	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
401		elfzelz 12342	. . . . . . . . . . . . . . . . . . . . . . 23
402	400, 401	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
403	353, 402	syldan 487	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
404	288	ad3antlr 767	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
405		zleltp1 11428	. . . . . . . . . . . . . . . . . . . . 21 $/\$
406	403, 404, 405	syl2anc 693	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
407	398, 406	mpbird 247	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
408	349	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
409		breq2 4657	. . . . . . . . . . . . . . . . . . . . . . 23
410	409	biimpac 503	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
411	408, 410	sylan 488	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
412		elfzle2 12345	. . . . . . . . . . . . . . . . . . . . . 22
413	400, 412	syl 17	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
414	411, 413	syldan 487	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
415		simpr 477	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
416	414, 415	breqtrrd 4681	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
417	407, 416	jaodan 826	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $\/$
418	417	an32s 846	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\/$ $/\$
419	330, 418	sylan 488	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
420		elfz2nn0 12431	. . . . . . . . . . . . . . . 16 $/\$ $/\$
421	321, 324, 419, 420	syl3anbrc 1246	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
422		fzss2 12381	. . . . . . . . . . . . . . . . . . . 20
423	292, 422	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
424	423	sselda 3603	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
425	424	3ad2antr1 1226	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
426	355	3ad2antr2 1227	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
427	359	ad2antll 765	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
428	274	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
429		simprl 794	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
430		fvun1 6269	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
431	370, 430	mp3an2 1412	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
432	427, 428, 429, 431	syl12anc 1324	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
433	432	adantlrr 757	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
434	433	3adantr3 1222	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
435		simpr3 1069	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
436	434, 435	eqtrd 2656	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
437	425, 426, 436	3jca 1242	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
438		nfv 1843	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
439		nfcv 2764	. . . . . . . . . . . . . . . . . . . 20
440	305, 378, 439	nfbr 4699	. . . . . . . . . . . . . . . . . . 19
441	438, 440	nfim 1825	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
442		fveq1 6190	. . . . . . . . . . . . . . . . . . . . . 22
443	442	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . 21
444	312, 443	3anbi23d 1402	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
445	444	anbi2d 740	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
446	314	breq1d 4663	. . . . . . . . . . . . . . . . . . 19
447	445, 446	imbi12d 334	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
448	441, 311, 447, 222	vtoclf 3258	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
449	448	adantlr 751	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
450	437, 449	syldan 487	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
451		simp1 1061	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
452	424	anasss 679	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
453	451, 452	sylanr2 685	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
454		simp2 1062	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
455	454, 303	sylanr2 685	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
456	432	3adantr3 1222	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
457		simpr3 1069	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
458	456, 457	eqtrd 2656	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
459	458	anasss 679	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
460	459	adantrlr 759	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
461	453, 455, 460	3jca 1242	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
462		nfv 1843	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
463		nfcv 2764	. . . . . . . . . . . . . . . . . . . 20
464	305, 463	nfne 2894	. . . . . . . . . . . . . . . . . . 19
465	462, 464	nfim 1825	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
466	442	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . 21
467	312, 466	3anbi23d 1402	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
468	467	anbi2d 740	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
469	314	neeq1d 2853	. . . . . . . . . . . . . . . . . . 19
470	468, 469	imbi12d 334	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
471		poimirlem28.4	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
472	465, 311, 470, 471	vtoclf 3258	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
473	461, 472	syldan 487	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
474	473	anassrs 680	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
475	266, 268, 421, 450, 474	poimirlem27 33436	. . . . . . . . . . . . . 14 $/\$ $/\$ ..^ $\$ ..^ $/\$ $/\$
476	266, 268, 421	poimirlem26 33435	. . . . . . . . . . . . . 14 $/\$ $/\$ ..^ $\$ ..^
477		fzfi 12771	. . . . . . . . . . . . . . . . . . 19
478		xpfi 8231	. . . . . . . . . . . . . . . . . . 19 ..^ $/\$ ..^
479	255, 477, 478	mp2an 708	. . . . . . . . . . . . . . . . . 18 ..^
480		rabfi 8185	. . . . . . . . . . . . . . . . . 18 ..^ ..^ $\$
481		hashcl 13147	. . . . . . . . . . . . . . . . . 18 ..^ $\$ ..^ $\$
482	479, 480, 481	mp2b 10	. . . . . . . . . . . . . . . . 17 ..^ $\$
483	482	nn0zi 11402	. . . . . . . . . . . . . . . 16 ..^ $\$
484		zsubcl 11419	. . . . . . . . . . . . . . . 16 ..^ $\$ $/\$ ..^ $/\$ $/\$ ..^ $\$ ..^ $/\$ $/\$
485	483, 263, 484	mp2an 708	. . . . . . . . . . . . . . 15 ..^ $\$ ..^ $/\$ $/\$
486		zsubcl 11419	. . . . . . . . . . . . . . . 16 ..^ $\$ $/\$ ..^ ..^ $\$ ..^
487	483, 259, 486	mp2an 708	. . . . . . . . . . . . . . 15 ..^ $\$ ..^
488		dvds2sub 15016	. . . . . . . . . . . . . . 15 $/\$ ..^ $\$ ..^ $/\$ $/\$ $/\$ ..^ $\$ ..^ ..^ $\$ ..^ $/\$ $/\$ $/\$ ..^ $\$ ..^ ..^ $\$ ..^ $/\$ $/\$ ..^ $\$ ..^
489	241, 485, 487, 488	mp3an 1424	. . . . . . . . . . . . . 14 ..^ $\$ ..^ $/\$ $/\$ $/\$ ..^ $\$ ..^ ..^ $\$ ..^ $/\$ $/\$ ..^ $\$ ..^
490	475, 476, 489	syl2anc 693	. . . . . . . . . . . . 13 $/\$ $/\$ ..^ $\$ ..^ $/\$ $/\$ ..^ $\$ ..^
491	482	nn0cni 11304	. . . . . . . . . . . . . 14 ..^ $\$
492	262	nn0cni 11304	. . . . . . . . . . . . . 14 ..^ $/\$ $/\$
493	258	nn0cni 11304	. . . . . . . . . . . . . 14 ..^
494		nnncan1 10317	. . . . . . . . . . . . . 14 ..^ $\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^ ..^ $\$ ..^ $/\$ $/\$ ..^ $\$ ..^ ..^ ..^ $/\$ $/\$
495	491, 492, 493, 494	mp3an 1424	. . . . . . . . . . . . 13 ..^ $\$ ..^ $/\$ $/\$ ..^ $\$ ..^ ..^ ..^ $/\$ $/\$
496	490, 495	syl6breq 4694	. . . . . . . . . . . 12 $/\$ $/\$ ..^ ..^ $/\$ $/\$
497		dvdssub2 15023	. . . . . . . . . . . 12 $/\$ ..^ $/\$ ..^ $/\$ $/\$ $/\$ ..^ ..^ $/\$ $/\$ ..^ ..^ $/\$ $/\$
498	264, 496, 497	sylancr 695	. . . . . . . . . . 11 $/\$ $/\$ ..^ ..^ $/\$ $/\$
499		nn0cn 11302	. . . . . . . . . . . . . . . . . . . 20
500		pncan1 10454	. . . . . . . . . . . . . . . . . . . 20
501	499, 500	syl 17	. . . . . . . . . . . . . . . . . . 19
502	501	oveq2d 6666	. . . . . . . . . . . . . . . . . 18
503	502	rexeqdv 3145	. . . . . . . . . . . . . . . . . 18
504	502, 503	raleqbidv 3152	. . . . . . . . . . . . . . . . 17
505	504	3anbi1d 1403	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
506	505	rabbidv 3189	. . . . . . . . . . . . . . 15 ..^ $/\$ $/\$ ..^ $/\$ $/\$
507	506	fveq2d 6195	. . . . . . . . . . . . . 14 ..^ $/\$ $/\$ ..^ $/\$ $/\$
508	507	ad2antrl 764	. . . . . . . . . . . . 13 $/\$ $/\$ ..^ $/\$ $/\$ ..^ $/\$ $/\$
509	1	adantr 481	. . . . . . . . . . . . . . 15 $/\$ $/\$
510	191	adantr 481	. . . . . . . . . . . . . . 15 $/\$ $/\$
511		simprl 794	. . . . . . . . . . . . . . 15 $/\$ $/\$
512		simprr 796	. . . . . . . . . . . . . . 15 $/\$ $/\$
513	509, 510, 511, 512	poimirlem4 33413	. . . . . . . . . . . . . 14 $/\$ $/\$ ..^ ..^ $/\$ $/\$
514		fzfi 12771	. . . . . . . . . . . . . . . . . 18
515		mapfi 8262	. . . . . . . . . . . . . . . . . 18 ..^ $/\$ ..^
516	10, 514, 515	mp2an 708	. . . . . . . . . . . . . . . . 17 ..^
517		ovex 6678	. . . . . . . . . . . . . . . . . . . 20
518	517, 517	mapval 7869	. . . . . . . . . . . . . . . . . . 19
519		mapfi 8262	. . . . . . . . . . . . . . . . . . . 20 $/\$
520	514, 514, 519	mp2an 708	. . . . . . . . . . . . . . . . . . 19
521	518, 520	eqeltrri 2698	. . . . . . . . . . . . . . . . . 18
522		f1of 6137	. . . . . . . . . . . . . . . . . . 19
523	522	ss2abi 3674	. . . . . . . . . . . . . . . . . 18
524		ssfi 8180	. . . . . . . . . . . . . . . . . 18 $/\$
525	521, 523, 524	mp2an 708	. . . . . . . . . . . . . . . . 17
526		xpfi 8231	. . . . . . . . . . . . . . . . 17 ..^ $/\$ ..^
527	516, 525, 526	mp2an 708	. . . . . . . . . . . . . . . 16 ..^
528		rabfi 8185	. . . . . . . . . . . . . . . 16 ..^ ..^
529	527, 528	ax-mp 5	. . . . . . . . . . . . . . 15 ..^
530		rabfi 8185	. . . . . . . . . . . . . . . 16 ..^ ..^ $/\$ $/\$
531	255, 530	ax-mp 5	. . . . . . . . . . . . . . 15 ..^ $/\$ $/\$
532		hashen 13135	. . . . . . . . . . . . . . 15 ..^ $/\$ ..^ $/\$ $/\$ ..^ ..^ $/\$ $/\$ ..^ ..^ $/\$ $/\$
533	529, 531, 532	mp2an 708	. . . . . . . . . . . . . 14 ..^ ..^ $/\$ $/\$ ..^ ..^ $/\$ $/\$
534	513, 533	sylibr 224	. . . . . . . . . . . . 13 $/\$ $/\$ ..^ ..^ $/\$ $/\$
535	508, 534	eqtr4d 2659	. . . . . . . . . . . 12 $/\$ $/\$ ..^ $/\$ $/\$ ..^
536	535	breq2d 4665	. . . . . . . . . . 11 $/\$ $/\$ ..^ $/\$ $/\$ ..^
537	498, 536	bitrd 268	. . . . . . . . . 10 $/\$ $/\$ ..^ ..^
538	537	biimpd 219	. . . . . . . . 9 $/\$ $/\$ ..^ ..^
539	538	con3d 148	. . . . . . . 8 $/\$ $/\$ ..^ ..^
540	539	expcom 451	. . . . . . 7 $/\$ ..^ ..^
541	540	a2d 29	. . . . . 6 $/\$ ..^ ..^
542	541	3adant1 1079	. . . . 5 $/\$ $/\$ ..^ ..^
543	107, 132, 157, 182, 240, 542	fnn0ind 11476	. . . 4 $/\$ $/\$ ..^
544	5, 543	mpcom 38	. . 3 ..^
545		dvds0 14997	. . . . . . . 8
546	241, 545	ax-mp 5	. . . . . . 7
547		hash0 13158	. . . . . . 7
548	546, 547	breqtrri 4680	. . . . . 6
549		fveq2 6191	. . . . . 6 ..^ ..^
550	548, 549	syl5breqr 4691	. . . . 5 ..^ ..^
551	3	ltp1d 10954	. . . . . . . . . . . . . . . . . 18
552	283	peano2zd 11485	. . . . . . . . . . . . . . . . . . 19
553		fzn 12357	. . . . . . . . . . . . . . . . . . 19 $/\$
554	552, 283, 553	syl2anc 693	. . . . . . . . . . . . . . . . . 18
555	551, 554	mpbid 222	. . . . . . . . . . . . . . . . 17
556	555	xpeq1d 5138	. . . . . . . . . . . . . . . 16
557	556, 86	syl6eq 2672	. . . . . . . . . . . . . . 15
558	557	uneq2d 3767	. . . . . . . . . . . . . 14
559		un0 3967	. . . . . . . . . . . . . 14
560	558, 559	syl6eq 2672	. . . . . . . . . . . . 13
561	560	csbeq1d 3540	. . . . . . . . . . . 12
562		ovex 6678	. . . . . . . . . . . . 13
563		poimirlem28.1	. . . . . . . . . . . . 13
564	562, 563	csbie 3559	. . . . . . . . . . . 12
565	561, 564	syl6eq 2672	. . . . . . . . . . 11
566	565	eqeq2d 2632	. . . . . . . . . 10
567	566	rexbidv 3052	. . . . . . . . 9
568	567	ralbidv 2986	. . . . . . . 8
569	568	rabbidv 3189	. . . . . . 7 ..^ ..^
570	569	fveq2d 6195	. . . . . 6 ..^ ..^
571	570	breq2d 4665	. . . . 5 ..^ ..^
572	550, 571	syl5ibr 236	. . . 4 ..^ ..^
573	572	necon3bd 2808	. . 3 ..^ ..^
574	544, 573	mpd 15	. 2 ..^
575		rabn0 3958	. 2 ..^ ..^
576	574, 575	sylib 208	1 ..^

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1483

wcel 1990

cab 2608

wne 2794

wral 2912

wrex 2913

crab 2916

cvv 3200

csb 3533 $\$ cdif 3571

cun 3572

cin 3573

wss 3574

c0 3915

csn 4177

cop 4183 class class class wbr 4653

cmpt 4729

cxp 5112

cima 5117

wfn 5883

wf 5884

wf1o 5887

cfv 5888 (class class class)co 6650

cof 6895

c1st 7166

c2nd 7167

c1o 7553

cmap 7857

cen 7952

cfn 7955

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

chash 13117

cdvds 14983

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-inf2 8538 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 ax-pre-sup 10014

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 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-int 4476 df-iun 4522 df-disj 4621 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-se 5074 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-isom 5897 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-2o 7561 df-oadd 7564 df-er 7742 df-map 7859 df-pm 7860 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-sup 8348 df-oi 8415 df-card 8765 df-cda 8990 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-n0 11293 df-xnn0 11364 df-z 11378 df-uz 11688 df-rp 11833 df-fz 12327 df-fzo 12466 df-seq 12802 df-exp 12861 df-fac 13061 df-bc 13090 df-hash 13118 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-clim 14219 df-sum 14417 df-dvds 14984

This theorem is referenced by: poimirlem32 33441

W3C validator