poimirlem25 - Mathbox for Brendan Leahy

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

Theorem poimirlem25 33434

Description: Lemma for poimir 33442 stating that for a given simplex such that no vertex maps to

, the number of admissible faces is even. (Contributed by Brendan Leahy, 21-Aug-2020.)

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

**Assertion**
Ref	Expression
poimirlem25	$\$

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

Proof of Theorem poimirlem25 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		neq0 3930	. . 3 $\$ $\$
2		2z 11409	. . . . . . . 8
3		iddvds 14995	. . . . . . . 8
4	2, 3	ax-mp 5	. . . . . . 7
5		df-2 11079	. . . . . . 7
6	4, 5	breqtri 4678	. . . . . 6
7		vex 3203	. . . . . . . . . 10
8		fzfi 12771	. . . . . . . . . . . . 13
9		rabfi 8185	. . . . . . . . . . . . 13 $\$
10	8, 9	ax-mp 5	. . . . . . . . . . . 12 $\$
11		diffi 8192	. . . . . . . . . . . 12 $\$ $\$ $\$
12	10, 11	ax-mp 5	. . . . . . . . . . 11 $\$ $\$
13		neldifsn 4321	. . . . . . . . . . 11 $\$ $\$
14	12, 13	pm3.2i 471	. . . . . . . . . 10 $\$ $\$ $/\$ $\$ $\$
15		hashunsng 13181	. . . . . . . . . 10 $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
16	7, 14, 15	mp2 9	. . . . . . . . 9 $\$ $\$ $\$ $\$
17		difsnid 4341	. . . . . . . . . 10 $\$ $\$ $\$ $\$
18	17	fveq2d 6195	. . . . . . . . 9 $\$ $\$ $\$ $\$
19	16, 18	syl5eqr 2670	. . . . . . . 8 $\$ $\$ $\$ $\$
20	19	adantl 482	. . . . . . 7 $/\$ $\$ $\$ $\$ $\$
21		sneq 4187	. . . . . . . . . . . . 13
22	21	difeq2d 3728	. . . . . . . . . . . 12 $\$ $\$
23	22	rexeqdv 3145	. . . . . . . . . . 11 $\$ $\$
24	23	ralbidv 2986	. . . . . . . . . 10 $\$ $\$
25	24	elrab 3363	. . . . . . . . 9 $\$ $/\$ $\$
26		poimirlem25.5	. . . . . . . . . . . . . . . . 17 $/\$
27	26	ralrimiva 2966	. . . . . . . . . . . . . . . 16
28		nfcv 2764	. . . . . . . . . . . . . . . . . 18
29		nfcsb1v 3549	. . . . . . . . . . . . . . . . . 18
30	28, 29	nfne 2894	. . . . . . . . . . . . . . . . 17
31		csbeq1a 3542	. . . . . . . . . . . . . . . . . 18
32	31	neeq2d 2854	. . . . . . . . . . . . . . . . 17
33	30, 32	rspc 3303	. . . . . . . . . . . . . . . 16
34	27, 33	mpan9 486	. . . . . . . . . . . . . . 15 $/\$
35		nesym 2850	. . . . . . . . . . . . . . 15
36	34, 35	sylib 208	. . . . . . . . . . . . . 14 $/\$
37		nfv 1843	. . . . . . . . . . . . . . . . . 18 $/\$
38	29	nfel1 2779	. . . . . . . . . . . . . . . . . 18
39	37, 38	nfim 1825	. . . . . . . . . . . . . . . . 17 $/\$
40		eleq1 2689	. . . . . . . . . . . . . . . . . . 19
41	40	anbi2d 740	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
42	31	eleq1d 2686	. . . . . . . . . . . . . . . . . 18
43	41, 42	imbi12d 334	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
44		poimirlem25.3	. . . . . . . . . . . . . . . . . . . . 21 ..^
45		ovex 6678	. . . . . . . . . . . . . . . . . . . . . 22 ..^
46		ovex 6678	. . . . . . . . . . . . . . . . . . . . . 22
47	45, 46	elmap 7886	. . . . . . . . . . . . . . . . . . . . 21 ..^ ..^
48	44, 47	sylibr 224	. . . . . . . . . . . . . . . . . . . 20 ..^
49		poimirlem25.4	. . . . . . . . . . . . . . . . . . . . 21
50		fzfi 12771	. . . . . . . . . . . . . . . . . . . . . . . 24
51		f1oexrnex 7115	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
52	50, 51	mpan2 707	. . . . . . . . . . . . . . . . . . . . . . 23
53		f1oeq1 6127	. . . . . . . . . . . . . . . . . . . . . . . 24
54	53	elabg 3351	. . . . . . . . . . . . . . . . . . . . . . 23
55	52, 54	syl 17	. . . . . . . . . . . . . . . . . . . . . 22
56	55	ibir 257	. . . . . . . . . . . . . . . . . . . . 21
57	49, 56	syl 17	. . . . . . . . . . . . . . . . . . . 20
58		opelxpi 5148	. . . . . . . . . . . . . . . . . . . 20 ..^ $/\$ ..^
59	48, 57, 58	syl2anc 693	. . . . . . . . . . . . . . . . . . 19 ..^
60	59	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$ ..^
61		nfcv 2764	. . . . . . . . . . . . . . . . . . 19
62		nfv 1843	. . . . . . . . . . . . . . . . . . . 20 $/\$
63		nfcsb1v 3549	. . . . . . . . . . . . . . . . . . . . 21
64	63	nfel1 2779	. . . . . . . . . . . . . . . . . . . 20
65	62, 64	nfim 1825	. . . . . . . . . . . . . . . . . . 19 $/\$
66		csbeq1a 3542	. . . . . . . . . . . . . . . . . . . . 21
67	66	eleq1d 2686	. . . . . . . . . . . . . . . . . . . 20
68	67	imbi2d 330	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
69		elun 3753	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\/$
70		fzofzp1 12565	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^
71		elsni 4194	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
72	71	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
73	72	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
74	70, 73	syl5ibrcom 237	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^
75		elfzonn0 12512	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ..^
76	75	nn0cnd 11353	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ..^
77	76	addid1d 10236	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^
78		elfzofz 12485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^
79	77, 78	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^
80		elsni 4194	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
81	80	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
82	81	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
83	79, 82	syl5ibrcom 237	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^
84	74, 83	jaod 395	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^ $\/$
85	69, 84	syl5bi 232	. . . . . . . . . . . . . . . . . . . . . . . . 25 ..^
86	85	imp 445	. . . . . . . . . . . . . . . . . . . . . . . 24 ..^ $/\$
87	86	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 ..^ $/\$ $/\$ ..^ $/\$
88		xp1st 7198	. . . . . . . . . . . . . . . . . . . . . . . . 25 ..^ ..^
89		elmapi 7879	. . . . . . . . . . . . . . . . . . . . . . . . 25 ..^ ..^
90	88, 89	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ..^ ..^
91	90	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ..^ $/\$ ..^
92		xp2nd 7199	. . . . . . . . . . . . . . . . . . . . . . . . 25 ..^
93		fvex 6201	. . . . . . . . . . . . . . . . . . . . . . . . . 26
94		f1oeq1 6127	. . . . . . . . . . . . . . . . . . . . . . . . . 26
95	93, 94	elab 3350	. . . . . . . . . . . . . . . . . . . . . . . . 25
96	92, 95	sylib 208	. . . . . . . . . . . . . . . . . . . . . . . 24 ..^
97		1ex 10035	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
98	97	fconst 6091	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
99		c0ex 10034	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
100	99	fconst 6091	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
101	98, 100	pm3.2i 471	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
102		dff1o3 6143	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
103		imain 5974	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
104	102, 103	simplbiim 659	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
105		elfznn0 12433	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
106	105	nn0red 11352	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
107	106	ltp1d 10954	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
108		fzdisj 12368	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
109	107, 108	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
110	109	imaeq2d 5466	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
111		ima0 5481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
112	110, 111	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
113	104, 112	sylan9req 2677	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
114		fun 6066	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
115	101, 113, 114	sylancr 695	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
116		nn0p1nn 11332	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
117	105, 116	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
118		nnuz 11723	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
119	117, 118	syl6eleq 2711	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
120		elfzuz3 12339	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
121		fzsplit2 12366	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
122	119, 120, 121	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
123	122	imaeq2d 5466	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
124		imaundi 5545	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
125	123, 124	syl6req 2673	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
126		f1ofo 6144	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
127		foima 6120	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
128	126, 127	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
129	125, 128	sylan9eqr 2678	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
130	129	feq2d 6031	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
131	115, 130	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
132	96, 131	sylan 488	. . . . . . . . . . . . . . . . . . . . . . 23 ..^ $/\$
133		fzfid 12772	. . . . . . . . . . . . . . . . . . . . . . 23 ..^ $/\$
134		inidm 3822	. . . . . . . . . . . . . . . . . . . . . . 23
135	87, 91, 132, 133, 133, 134	off 6912	. . . . . . . . . . . . . . . . . . . . . 22 ..^ $/\$
136		ovex 6678	. . . . . . . . . . . . . . . . . . . . . . 23
137		feq1 6026	. . . . . . . . . . . . . . . . . . . . . . . . 25
138	137	anbi2d 740	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
139		poimirlem28.1	. . . . . . . . . . . . . . . . . . . . . . . . 25
140	139	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . . . . 24
141	138, 140	imbi12d 334	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
142		poimirlem28.2	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
143	136, 141, 142	vtocl 3259	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
144	135, 143	sylan2 491	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$
145	144	an12s 843	. . . . . . . . . . . . . . . . . . . 20 ..^ $/\$ $/\$
146	145	ex 450	. . . . . . . . . . . . . . . . . . 19 ..^ $/\$
147	61, 65, 68, 146	vtoclgaf 3271	. . . . . . . . . . . . . . . . . 18 ..^ $/\$
148	60, 147	mpcom 38	. . . . . . . . . . . . . . . . 17 $/\$
149	39, 43, 148	chvar 2262	. . . . . . . . . . . . . . . 16 $/\$
150		poimir.0	. . . . . . . . . . . . . . . . . . . 20
151	150	nnnn0d 11351	. . . . . . . . . . . . . . . . . . 19
152		nn0uz 11722	. . . . . . . . . . . . . . . . . . 19
153	151, 152	syl6eleq 2711	. . . . . . . . . . . . . . . . . 18
154		fzm1 12420	. . . . . . . . . . . . . . . . . 18 $\/$
155	153, 154	syl 17	. . . . . . . . . . . . . . . . 17 $\/$
156	155	adantr 481	. . . . . . . . . . . . . . . 16 $/\$ $\/$
157	149, 156	mpbid 222	. . . . . . . . . . . . . . 15 $/\$ $\/$
158	157	ord 392	. . . . . . . . . . . . . 14 $/\$
159	36, 158	mt3d 140	. . . . . . . . . . . . 13 $/\$
160	159	adantrr 753	. . . . . . . . . . . 12 $/\$ $/\$ $\$
161		fzfi 12771	. . . . . . . . . . . . . . 15
162	150	nncnd 11036	. . . . . . . . . . . . . . . . . . 19
163		1cnd 10056	. . . . . . . . . . . . . . . . . . 19
164	162, 163, 163	addsubd 10413	. . . . . . . . . . . . . . . . . 18
165		hashfz0 13219	. . . . . . . . . . . . . . . . . . . 20
166	151, 165	syl 17	. . . . . . . . . . . . . . . . . . 19
167	166	oveq1d 6665	. . . . . . . . . . . . . . . . . 18
168		nnm1nn0 11334	. . . . . . . . . . . . . . . . . . 19
169		hashfz0 13219	. . . . . . . . . . . . . . . . . . 19
170	150, 168, 169	3syl 18	. . . . . . . . . . . . . . . . . 18
171	164, 167, 170	3eqtr4rd 2667	. . . . . . . . . . . . . . . . 17
172		hashdifsn 13202	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$
173	8, 172	mpan 706	. . . . . . . . . . . . . . . . . 18 $\$
174	173	eqcomd 2628	. . . . . . . . . . . . . . . . 17 $\$
175	171, 174	sylan9eq 2676	. . . . . . . . . . . . . . . 16 $/\$ $\$
176		diffi 8192	. . . . . . . . . . . . . . . . . 18 $\$
177	8, 176	ax-mp 5	. . . . . . . . . . . . . . . . 17 $\$
178		hashen 13135	. . . . . . . . . . . . . . . . 17 $/\$ $\$ $\$ $\$
179	161, 177, 178	mp2an 708	. . . . . . . . . . . . . . . 16 $\$ $\$
180	175, 179	sylib 208	. . . . . . . . . . . . . . 15 $/\$ $\$
181		phpreu 33393	. . . . . . . . . . . . . . 15 $/\$ $\$ $\$ $\$
182	161, 180, 181	sylancr 695	. . . . . . . . . . . . . 14 $/\$ $\$ $\$
183	182	biimpd 219	. . . . . . . . . . . . 13 $/\$ $\$ $\$
184	183	impr 649	. . . . . . . . . . . 12 $/\$ $/\$ $\$ $\$
185		nfv 1843	. . . . . . . . . . . . . . 15
186		nfcsb1v 3549	. . . . . . . . . . . . . . . 16
187	186	nfeq2 2780	. . . . . . . . . . . . . . 15
188		csbeq1a 3542	. . . . . . . . . . . . . . . 16
189	188	eqeq2d 2632	. . . . . . . . . . . . . . 15
190	185, 187, 189	cbvreu 3169	. . . . . . . . . . . . . 14 $\$ $\$
191		eqeq1 2626	. . . . . . . . . . . . . . 15
192	191	reubidv 3126	. . . . . . . . . . . . . 14 $\$ $\$
193	190, 192	syl5bb 272	. . . . . . . . . . . . 13 $\$ $\$
194	193	rspcv 3305	. . . . . . . . . . . 12 $\$ $\$
195	160, 184, 194	sylc 65	. . . . . . . . . . 11 $/\$ $/\$ $\$ $\$
196		an32 839	. . . . . . . . . . . . . . . 16 $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
197	196	biimpi 206	. . . . . . . . . . . . . . 15 $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
198	197	adantll 750	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
199		eqeq2 2633	. . . . . . . . . . . . . . . . . . . . . 22
200		rexsns 4217	. . . . . . . . . . . . . . . . . . . . . . 23
201	29	nfeq2 2780	. . . . . . . . . . . . . . . . . . . . . . . . 25
202	31	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . . . . . . 25
203	201, 202	sbciegf 3467	. . . . . . . . . . . . . . . . . . . . . . . 24
204	7, 203	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23
205	200, 204	bitri 264	. . . . . . . . . . . . . . . . . . . . . 22
206		rexsns 4217	. . . . . . . . . . . . . . . . . . . . . . 23
207		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . 24
208	187, 189	sbciegf 3467	. . . . . . . . . . . . . . . . . . . . . . . 24
209	207, 208	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23
210	206, 209	bitri 264	. . . . . . . . . . . . . . . . . . . . . 22
211	199, 205, 210	3bitr4g 303	. . . . . . . . . . . . . . . . . . . . 21
212	211	orbi1d 739	. . . . . . . . . . . . . . . . . . . 20 $\/$ $\$ $\$ $\/$ $\$ $\$
213		rexun 3793	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$ $\/$ $\$ $\$
214		rexun 3793	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$ $\/$ $\$ $\$
215	212, 213, 214	3bitr4g 303	. . . . . . . . . . . . . . . . . . 19 $\$ $\$ $\$ $\$
216	215	adantl 482	. . . . . . . . . . . . . . . . . 18 $/\$ $\$ $/\$ $\$ $\$ $\$ $\$
217		eldifsni 4320	. . . . . . . . . . . . . . . . . . . . . 22 $\$
218	217	necomd 2849	. . . . . . . . . . . . . . . . . . . . 21 $\$
219		dif32 3891	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $\$ $\$ $\$
220	219	uneq2i 3764	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$ $\$ $\$
221		snssi 4339	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $\$
222		eldifsn 4317	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $/\$
223		undif 4049	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $\$ $\$ $\$
224	221, 222, 223	3imtr3i 280	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\$ $\$ $\$
225	220, 224	syl5eq 2668	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $\$ $\$
226	218, 225	sylan2 491	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\$ $\$ $\$ $\$
227	226	rexeqdv 3145	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$ $\$ $\$ $\$
228	227	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$ $\$ $/\$ $\$ $\$ $\$
229		snssi 4339	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
230		undif 4049	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$ $\$ $\$
231	229, 230	sylib 208	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$ $\$ $\$
232	231	rexeqdv 3145	. . . . . . . . . . . . . . . . . . 19 $\$ $\$ $\$ $\$
233	232	ad2antlr 763	. . . . . . . . . . . . . . . . . 18 $/\$ $\$ $/\$ $\$ $\$ $\$
234	216, 228, 233	3bitr3d 298	. . . . . . . . . . . . . . . . 17 $/\$ $\$ $/\$ $\$ $\$
235	234	ralbidv 2986	. . . . . . . . . . . . . . . 16 $/\$ $\$ $/\$ $\$ $\$
236	235	biimpar 502	. . . . . . . . . . . . . . 15 $/\$ $\$ $/\$ $/\$ $\$ $\$
237	236	an32s 846	. . . . . . . . . . . . . 14 $/\$ $\$ $/\$ $\$ $/\$ $\$
238	198, 237	sylan 488	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
239		simpl 473	. . . . . . . . . . . . . . . . . 18 $/\$ $\$
240	239	anim2i 593	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$ $/\$
241		necom 2847	. . . . . . . . . . . . . . . . . . . . . . . . . 26
242	241	biimpi 206	. . . . . . . . . . . . . . . . . . . . . . . . 25
243	242	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
244	243	anim2i 593	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
245		eldifsn 4317	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $/\$
246	245	anbi2i 730	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $\$ $/\$ $/\$
247	244, 246, 222	3imtr4i 281	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\$ $\$
248	247	adantll 750	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\$ $\$
249	248	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\$ $/\$ $\$ $\$
250	29	nfel1 2779	. . . . . . . . . . . . . . . . . . . . . . . . . 26
251	37, 250	nfim 1825	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
252	31	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . . . . . . 26
253	41, 252	imbi12d 334	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
254	26	necomd 2849	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
255	254	neneqd 2799	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
256		fzm1 12420	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\/$
257	153, 256	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\/$
258	257	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $\/$
259	148, 258	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\/$
260	259	ord 392	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
261	255, 260	mt3d 140	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
262	251, 253, 261	chvar 2262	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
263	262	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $\$ $/\$ $\$
264		eldifi 3732	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$
265		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
266	265	anbi2d 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
267		sneq 4187	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
268	267	difeq2d 3728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$ $\$
269	268	breq2d 4665	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $\$
270	266, 269	imbi12d 334	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\$ $/\$ $\$
271	270, 180	chvarv 2263	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $\$
272	264, 271	sylan2 491	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $\$ $\$
273	272	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $\$ $\$
274		phpreu 33393	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $\$ $\$ $\$
275	161, 274	mpan 706	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $\$ $\$
276	275	biimpa 501	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $/\$ $\$ $\$
277	273, 276	sylan 488	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $\$ $/\$ $\$ $\$
278		eqeq1 2626	. . . . . . . . . . . . . . . . . . . . . . . . . 26
279	278	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $\$
280	201, 279	reubida 3124	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$
281	280	rspcv 3305	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $\$
282	263, 277, 281	sylc 65	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\$ $/\$ $\$ $\$
283		reurmo 3161	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$
284	282, 283	syl 17	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\$ $/\$ $\$ $\$
285		nfv 1843	. . . . . . . . . . . . . . . . . . . . . 22
286	285	rmo3 3528	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$ $\$ $/\$
287	284, 286	sylib 208	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $/\$
288		equcomi 1944	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
289	288	csbeq1d 3540	. . . . . . . . . . . . . . . . . . . . . . . . . 26
290		sbsbc 3439	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
291		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
292		sbceqg 3984	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
293	29	csbconstgf 3545	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
294	293	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
295	292, 294	bitrd 268	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
296	291, 295	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
297	290, 296	bitri 264	. . . . . . . . . . . . . . . . . . . . . . . . . 26
298	289, 297	sylibr 224	. . . . . . . . . . . . . . . . . . . . . . . . 25
299	298	biantrud 528	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
300	299	bicomd 213	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
301		eqeq2 2633	. . . . . . . . . . . . . . . . . . . . . . 23
302	300, 301	imbi12d 334	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
303	302	rspcv 3305	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$ $/\$
304	303	ralimdv 2963	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$ $\$ $/\$ $\$
305	249, 287, 304	sylc 65	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $\$ $/\$ $\$ $\$
306		dif32 3891	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $\$ $\$ $\$
307	306	eleq2i 2693	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$ $\$ $\$
308		eldifsn 4317	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$ $\$ $/\$
309		eldifsn 4317	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$ $\$ $/\$
310	307, 308, 309	3bitr3ri 291	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $/\$ $\$ $/\$
311	310	imbi1i 339	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $/\$ $\$ $/\$
312		impexp 462	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $/\$ $\$
313		impexp 462	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $/\$ $\$
314	311, 312, 313	3bitr3ri 291	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
315	314	albii 1747	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
316		con34b 306	. . . . . . . . . . . . . . . . . . . . . . 23
317		df-ne 2795	. . . . . . . . . . . . . . . . . . . . . . . 24
318	317	imbi1i 339	. . . . . . . . . . . . . . . . . . . . . . 23
319	316, 318	bitr4i 267	. . . . . . . . . . . . . . . . . . . . . 22
320	319	ralbii 2980	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
321		df-ral 2917	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
322	320, 321	bitri 264	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
323		df-ral 2917	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
324	315, 322, 323	3bitr4i 292	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
325	305, 324	sylib 208	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\$ $/\$ $\$ $\$
326		df-ne 2795	. . . . . . . . . . . . . . . . . . . . . 22
327	326	imbi1i 339	. . . . . . . . . . . . . . . . . . . . 21
328		con34b 306	. . . . . . . . . . . . . . . . . . . . 21
329	327, 328	bitr4i 267	. . . . . . . . . . . . . . . . . . . 20
330		ancr 572	. . . . . . . . . . . . . . . . . . . 20 $/\$
331	329, 330	sylbi 207	. . . . . . . . . . . . . . . . . . 19 $/\$
332	331	ralimi 2952	. . . . . . . . . . . . . . . . . 18 $\$ $\$ $/\$
333	325, 332	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$ $/\$ $\$ $\$ $/\$
334	240, 333	sylanl1 682	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $/\$
335	201, 278	rexbid 3051	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
336	335	rspcva 3307	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$ $\$
337	262, 336	sylan 488	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\$ $\$
338	337	anasss 679	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$ $\$
339	338	ad2antrr 762	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$
340		rexim 3008	. . . . . . . . . . . . . . . 16 $\$ $/\$ $\$ $\$ $/\$
341	334, 339, 340	sylc 65	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $/\$
342		rexex 3002	. . . . . . . . . . . . . . 15 $\$ $/\$ $/\$
343	341, 342	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$
344	29, 186	nfeq 2776	. . . . . . . . . . . . . . 15
345	188	eqeq2d 2632	. . . . . . . . . . . . . . 15
346	344, 345	equsexv 2109	. . . . . . . . . . . . . 14 $/\$
347	343, 346	sylib 208	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
348	238, 347	impbida 877	. . . . . . . . . . . 12 $/\$ $/\$ $\$ $/\$ $\$ $\$
349	348	reubidva 3125	. . . . . . . . . . 11 $/\$ $/\$ $\$ $\$ $\$ $\$
350	195, 349	mpbid 222	. . . . . . . . . 10 $/\$ $/\$ $\$ $\$ $\$
351		an32 839	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$ $/\$ $\$ $/\$
352	245	anbi1i 731	. . . . . . . . . . . . . 14 $\$ $/\$ $\$ $/\$ $/\$ $\$
353		sneq 4187	. . . . . . . . . . . . . . . . . . 19
354	353	difeq2d 3728	. . . . . . . . . . . . . . . . . 18 $\$ $\$
355	354	rexeqdv 3145	. . . . . . . . . . . . . . . . 17 $\$ $\$
356	355	ralbidv 2986	. . . . . . . . . . . . . . . 16 $\$ $\$
357	356	elrab 3363	. . . . . . . . . . . . . . 15 $\$ $/\$ $\$
358	357	anbi1i 731	. . . . . . . . . . . . . 14 $\$ $/\$ $/\$ $\$ $/\$
359	351, 352, 358	3bitr4i 292	. . . . . . . . . . . . 13 $\$ $/\$ $\$ $\$ $/\$
360		eldifsn 4317	. . . . . . . . . . . . 13 $\$ $\$ $\$ $/\$
361	359, 360	bitr4i 267	. . . . . . . . . . . 12 $\$ $/\$ $\$ $\$ $\$
362	361	eubii 2492	. . . . . . . . . . 11 $\$ $/\$ $\$ $\$ $\$
363		df-reu 2919	. . . . . . . . . . 11 $\$ $\$ $\$ $/\$ $\$
364		euhash1 13208	. . . . . . . . . . . 12 $\$ $\$ $\$ $\$ $\$ $\$
365	12, 364	ax-mp 5	. . . . . . . . . . 11 $\$ $\$ $\$ $\$
366	362, 363, 365	3bitr4i 292	. . . . . . . . . 10 $\$ $\$ $\$ $\$
367	350, 366	sylib 208	. . . . . . . . 9 $/\$ $/\$ $\$ $\$ $\$
368	25, 367	sylan2b 492	. . . . . . . 8 $/\$ $\$ $\$ $\$
369	368	oveq1d 6665	. . . . . . 7 $/\$ $\$ $\$ $\$
370	20, 369	eqtr3d 2658	. . . . . 6 $/\$ $\$ $\$
371	6, 370	syl5breqr 4691	. . . . 5 $/\$ $\$ $\$
372	371	ex 450	. . . 4 $\$ $\$
373	372	exlimdv 1861	. . 3 $\$ $\$
374	1, 373	syl5bi 232	. 2 $\$ $\$
375		dvds0 14997	. . . . 5
376	2, 375	ax-mp 5	. . . 4
377		hash0 13158	. . . 4
378	376, 377	breqtrri 4680	. . 3
379		fveq2 6191	. . 3 $\$ $\$
380	378, 379	syl5breqr 4691	. 2 $\$ $\$
381	374, 380	pm2.61d2 172	1 $\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wal 1481

wceq 1483

wex 1704

wsb 1880

wcel 1990

weu 2470

cab 2608

wne 2794

wral 2912

wrex 2913

wreu 2914

wrmo 2915

crab 2916

cvv 3200

wsbc 3435

csb 3533 $\$ cdif 3571

cun 3572

cin 3573

wss 3574

c0 3915

csn 4177

cop 4183 class class class wbr 4653

cxp 5112

ccnv 5113

cima 5117

wfun 5882

wf 5884

wfo 5886

wf1o 5887

cfv 5888 (class class class)co 6650

cof 6895

c1st 7166

c2nd 7167

cmap 7857

cen 7952

cfn 7955

cc0 9936

c1 9937

caddc 9939

clt 10074

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-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013

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

This theorem is referenced by: poimirlem26 33435

W3C validator