poimirlem27 - Mathbox for Brendan Leahy

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

Theorem poimirlem27 33436

Description: Lemma for poimir 33442 showing that the difference between admissible faces in the whole cube and admissible faces on the back face is even. Equation (7) of [Kulpa] p. 548. (Contributed by Brendan Leahy, 21-Aug-2020.)

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

**Assertion**
Ref	Expression
poimirlem27	..^ $\$ ..^ $/\$ $/\$

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

Proof of Theorem poimirlem27 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fzfi 12771	. . . . . 6
2		fzfi 12771	. . . . . 6
3		mapfi 8262	. . . . . 6 $/\$
4	1, 2, 3	mp2an 708	. . . . 5
5		fzfi 12771	. . . . 5
6		mapfi 8262	. . . . 5 $/\$
7	4, 5, 6	mp2an 708	. . . 4
8	7	a1i 11	. . 3
9		2z 11409	. . . 4
10	9	a1i 11	. . 3
11		fzofi 12773	. . . . . . . 8 ..^
12		mapfi 8262	. . . . . . . 8 ..^ $/\$ ..^
13	11, 2, 12	mp2an 708	. . . . . . 7 ..^
14		mapfi 8262	. . . . . . . . 9 $/\$
15	2, 2, 14	mp2an 708	. . . . . . . 8
16		f1of 6137	. . . . . . . . . 10
17	16	ss2abi 3674	. . . . . . . . 9
18		ovex 6678	. . . . . . . . . 10
19	18, 18	mapval 7869	. . . . . . . . 9
20	17, 19	sseqtr4i 3638	. . . . . . . 8
21		ssfi 8180	. . . . . . . 8 $/\$
22	15, 20, 21	mp2an 708	. . . . . . 7
23		xpfi 8231	. . . . . . 7 ..^ $/\$ ..^
24	13, 22, 23	mp2an 708	. . . . . 6 ..^
25		fzfi 12771	. . . . . 6
26		xpfi 8231	. . . . . 6 ..^ $/\$ ..^
27	24, 25, 26	mp2an 708	. . . . 5 ..^
28		rabfi 8185	. . . . 5 ..^ ..^ $/\$ $/\$ $/\$
29	27, 28	ax-mp 5	. . . 4 ..^ $/\$ $/\$ $/\$
30		hashcl 13147	. . . . 5 ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
31	30	nn0zd 11480	. . . 4 ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
32	29, 31	mp1i 13	. . 3 $/\$ ..^ $/\$ $/\$ $/\$
33		dfrex2 2996	. . . . 5 ..^ $/\$ $/\$ ..^ $/\$ $/\$
34		nfv 1843	. . . . . 6 $/\$
35		nfcv 2764	. . . . . . 7
36		nfcv 2764	. . . . . . 7
37		nfcv 2764	. . . . . . . 8
38		nfrab1 3122	. . . . . . . 8 ..^ $/\$ $/\$ $/\$
39	37, 38	nffv 6198	. . . . . . 7 ..^ $/\$ $/\$ $/\$
40	35, 36, 39	nfbr 4699	. . . . . 6 ..^ $/\$ $/\$ $/\$
41		neq0 3930	. . . . . . . . . . . 12 ..^ ..^
42		iddvds 14995	. . . . . . . . . . . . . . . . 17
43	9, 42	ax-mp 5	. . . . . . . . . . . . . . . 16
44		vex 3203	. . . . . . . . . . . . . . . . . . 19
45		hashsng 13159	. . . . . . . . . . . . . . . . . . 19
46	44, 45	ax-mp 5	. . . . . . . . . . . . . . . . . 18
47	46	oveq2i 6661	. . . . . . . . . . . . . . . . 17
48		df-2 11079	. . . . . . . . . . . . . . . . 17
49	47, 48	eqtr4i 2647	. . . . . . . . . . . . . . . 16
50	43, 49	breqtrri 4680	. . . . . . . . . . . . . . 15
51		rabfi 8185	. . . . . . . . . . . . . . . . . . . 20 ..^ ..^
52		diffi 8192	. . . . . . . . . . . . . . . . . . . 20 ..^ ..^ $\$
53	27, 51, 52	mp2b 10	. . . . . . . . . . . . . . . . . . 19 ..^ $\$
54		snfi 8038	. . . . . . . . . . . . . . . . . . 19
55		incom 3805	. . . . . . . . . . . . . . . . . . . 20 ..^ $\$ ..^ $\$
56		disjdif 4040	. . . . . . . . . . . . . . . . . . . 20 ..^ $\$
57	55, 56	eqtri 2644	. . . . . . . . . . . . . . . . . . 19 ..^ $\$
58		hashun 13171	. . . . . . . . . . . . . . . . . . 19 ..^ $\$ $/\$ $/\$ ..^ $\$ ..^ $\$ ..^ $\$
59	53, 54, 57, 58	mp3an 1424	. . . . . . . . . . . . . . . . . 18 ..^ $\$ ..^ $\$
60		difsnid 4341	. . . . . . . . . . . . . . . . . . 19 ..^ ..^ $\$ ..^
61	60	fveq2d 6195	. . . . . . . . . . . . . . . . . 18 ..^ ..^ $\$ ..^
62	59, 61	syl5eqr 2670	. . . . . . . . . . . . . . . . 17 ..^ ..^ $\$ ..^
63	62	adantl 482	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ ..^ ..^ $\$ ..^
64		poimir.0	. . . . . . . . . . . . . . . . . . . 20
65	64	ad3antrrr 766	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ ..^
66		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
67	66	breq2d 4665	. . . . . . . . . . . . . . . . . . . . . . . . . 26
68	67	ifbid 4108	. . . . . . . . . . . . . . . . . . . . . . . . 25
69	68	csbeq1d 3540	. . . . . . . . . . . . . . . . . . . . . . . 24
70		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
71	70	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . . 26
72	70	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
73	72	imaeq1d 5465	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
74	73	xpeq1d 5138	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
75	72	imaeq1d 5465	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
76	75	xpeq1d 5138	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
77	74, 76	uneq12d 3768	. . . . . . . . . . . . . . . . . . . . . . . . . 26
78	71, 77	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . . 25
79	78	csbeq2dv 3992	. . . . . . . . . . . . . . . . . . . . . . . 24
80	69, 79	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . 23
81	80	mpteq2dv 4745	. . . . . . . . . . . . . . . . . . . . . 22
82		breq1 4656	. . . . . . . . . . . . . . . . . . . . . . . . . 26
83		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . 26
84		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . . . 26
85	82, 83, 84	ifbieq12d 4113	. . . . . . . . . . . . . . . . . . . . . . . . 25
86	85	csbeq1d 3540	. . . . . . . . . . . . . . . . . . . . . . . 24
87		oveq2 6658	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
88	87	imaeq2d 5466	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
89	88	xpeq1d 5138	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
90		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
91	90	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
92	91	imaeq2d 5466	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
93	92	xpeq1d 5138	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
94	89, 93	uneq12d 3768	. . . . . . . . . . . . . . . . . . . . . . . . . 26
95	94	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . 25
96	95	cbvcsbv 3539	. . . . . . . . . . . . . . . . . . . . . . . 24
97	86, 96	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . . 23
98	97	cbvmptv 4750	. . . . . . . . . . . . . . . . . . . . . 22
99	81, 98	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . 21
100	99	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . 20
101	100	cbvrabv 3199	. . . . . . . . . . . . . . . . . . 19 ..^ ..^
102		elmapi 7879	. . . . . . . . . . . . . . . . . . . 20
103	102	ad3antlr 767	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ ..^
104		simpr 477	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ ..^ ..^
105		simpl 473	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
106	105	ralimi 2952	. . . . . . . . . . . . . . . . . . . . 21 $/\$
107	106	ad2antlr 763	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ ..^
108		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . 24
109	108	neeq1d 2853	. . . . . . . . . . . . . . . . . . . . . . 23
110	109	rexbidv 3052	. . . . . . . . . . . . . . . . . . . . . 22
111		fveq1 6190	. . . . . . . . . . . . . . . . . . . . . . . 24
112	111	neeq1d 2853	. . . . . . . . . . . . . . . . . . . . . . 23
113	112	cbvrexv 3172	. . . . . . . . . . . . . . . . . . . . . 22
114	110, 113	syl6bb 276	. . . . . . . . . . . . . . . . . . . . 21
115	114	rspccva 3308	. . . . . . . . . . . . . . . . . . . 20 $/\$
116	107, 115	sylan 488	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ ..^ $/\$
117		simpr 477	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
118	117	ralimi 2952	. . . . . . . . . . . . . . . . . . . . 21 $/\$
119	118	ad2antlr 763	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ ..^
120	108	neeq1d 2853	. . . . . . . . . . . . . . . . . . . . . . 23
121	120	rexbidv 3052	. . . . . . . . . . . . . . . . . . . . . 22
122	111	neeq1d 2853	. . . . . . . . . . . . . . . . . . . . . . 23
123	122	cbvrexv 3172	. . . . . . . . . . . . . . . . . . . . . 22
124	121, 123	syl6bb 276	. . . . . . . . . . . . . . . . . . . . 21
125	124	rspccva 3308	. . . . . . . . . . . . . . . . . . . 20 $/\$
126	119, 125	sylan 488	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ ..^ $/\$
127	65, 101, 103, 104, 116, 126	poimirlem22 33431	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ ..^ ..^
128		eldifsn 4317	. . . . . . . . . . . . . . . . . . . 20 ..^ $\$ ..^ $/\$
129	128	eubii 2492	. . . . . . . . . . . . . . . . . . 19 ..^ $\$ ..^ $/\$
130	53	elexi 3213	. . . . . . . . . . . . . . . . . . . 20 ..^ $\$
131		euhash1 13208	. . . . . . . . . . . . . . . . . . . 20 ..^ $\$ ..^ $\$ ..^ $\$
132	130, 131	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ..^ $\$ ..^ $\$
133		df-reu 2919	. . . . . . . . . . . . . . . . . . 19 ..^ ..^ $/\$
134	129, 132, 133	3bitr4ri 293	. . . . . . . . . . . . . . . . . 18 ..^ ..^ $\$
135	127, 134	sylib 208	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ ..^ ..^ $\$
136	135	oveq1d 6665	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ ..^ ..^ $\$
137	63, 136	eqtr3d 2658	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ ..^ ..^
138	50, 137	syl5breqr 4691	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ ..^ ..^
139	138	ex 450	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ ..^ ..^
140	139	exlimdv 1861	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ ..^ ..^
141	41, 140	syl5bi 232	. . . . . . . . . . 11 $/\$ $/\$ $/\$ ..^ ..^
142		dvds0 14997	. . . . . . . . . . . . . 14
143	9, 142	ax-mp 5	. . . . . . . . . . . . 13
144		hash0 13158	. . . . . . . . . . . . 13
145	143, 144	breqtrri 4680	. . . . . . . . . . . 12
146		fveq2 6191	. . . . . . . . . . . 12 ..^ ..^
147	145, 146	syl5breqr 4691	. . . . . . . . . . 11 ..^ ..^
148	141, 147	pm2.61d2 172	. . . . . . . . . 10 $/\$ $/\$ $/\$ ..^
149	148	ex 450	. . . . . . . . 9 $/\$ $/\$ ..^
150	149	adantld 483	. . . . . . . 8 $/\$ $/\$ $/\$ ..^
151		iba 524	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
152	151	rabbidv 3189	. . . . . . . . . 10 $/\$ $/\$ ..^ ..^ $/\$ $/\$ $/\$
153	152	fveq2d 6195	. . . . . . . . 9 $/\$ $/\$ ..^ ..^ $/\$ $/\$ $/\$
154	153	breq2d 4665	. . . . . . . 8 $/\$ $/\$ ..^ ..^ $/\$ $/\$ $/\$
155	150, 154	mpbidi 231	. . . . . . 7 $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
156	155	a1d 25	. . . . . 6 $/\$ ..^ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
157	34, 40, 156	rexlimd 3026	. . . . 5 $/\$ ..^ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
158	33, 157	syl5bir 233	. . . 4 $/\$ ..^ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
159		simpr 477	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
160	159	con3i 150	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
161	160	ralimi 2952	. . . . . . 7 ..^ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
162		rabeq0 3957	. . . . . . 7 ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
163	161, 162	sylibr 224	. . . . . 6 ..^ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
164	163	fveq2d 6195	. . . . 5 ..^ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
165	145, 164	syl5breqr 4691	. . . 4 ..^ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
166	158, 165	pm2.61d2 172	. . 3 $/\$ ..^ $/\$ $/\$ $/\$
167	8, 10, 32, 166	fsumdvds 15030	. 2 ..^ $/\$ $/\$ $/\$
168		rabfi 8185	. . . . 5 ..^ ..^ $\$
169	27, 168	ax-mp 5	. . . 4 ..^ $\$
170		simp1 1061	. . . . . . 7 $/\$ $/\$
171		sneq 4187	. . . . . . . . . . . . 13
172	171	difeq2d 3728	. . . . . . . . . . . 12 $\$ $\$
173		difun2 4048	. . . . . . . . . . . . 13 $\$ $\$
174	64	nnnn0d 11351	. . . . . . . . . . . . . . . . . 18
175		nn0uz 11722	. . . . . . . . . . . . . . . . . 18
176	174, 175	syl6eleq 2711	. . . . . . . . . . . . . . . . 17
177		fzm1 12420	. . . . . . . . . . . . . . . . 17 $\/$
178	176, 177	syl 17	. . . . . . . . . . . . . . . 16 $\/$
179		elun 3753	. . . . . . . . . . . . . . . . 17 $\/$
180		velsn 4193	. . . . . . . . . . . . . . . . . 18
181	180	orbi2i 541	. . . . . . . . . . . . . . . . 17 $\/$ $\/$
182	179, 181	bitri 264	. . . . . . . . . . . . . . . 16 $\/$
183	178, 182	syl6bbr 278	. . . . . . . . . . . . . . 15
184	183	eqrdv 2620	. . . . . . . . . . . . . 14
185	184	difeq1d 3727	. . . . . . . . . . . . 13 $\$ $\$
186	64	nnzd 11481	. . . . . . . . . . . . . . 15
187		uzid 11702	. . . . . . . . . . . . . . 15
188		uznfz 12423	. . . . . . . . . . . . . . 15
189	186, 187, 188	3syl 18	. . . . . . . . . . . . . 14
190		disjsn 4246	. . . . . . . . . . . . . . 15
191		disj3 4021	. . . . . . . . . . . . . . 15 $\$
192	190, 191	bitr3i 266	. . . . . . . . . . . . . 14 $\$
193	189, 192	sylib 208	. . . . . . . . . . . . 13 $\$
194	173, 185, 193	3eqtr4a 2682	. . . . . . . . . . . 12 $\$
195	172, 194	sylan9eqr 2678	. . . . . . . . . . 11 $/\$ $\$
196	195	rexeqdv 3145	. . . . . . . . . 10 $/\$ $\$
197	196	biimprd 238	. . . . . . . . 9 $/\$ $\$
198	197	ralimdv 2963	. . . . . . . 8 $/\$ $\$
199	198	expimpd 629	. . . . . . 7 $/\$ $\$
200	170, 199	sylan2i 687	. . . . . 6 $/\$ $/\$ $/\$ $\$
201	200	adantr 481	. . . . 5 $/\$ ..^ $/\$ $/\$ $/\$ $\$
202	201	ss2rabdv 3683	. . . 4 ..^ $/\$ $/\$ $/\$ ..^ $\$
203		hashssdif 13200	. . . 4 ..^ $\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^ $\$ ..^ $\$ $\$ ..^ $/\$ $/\$ $/\$ ..^ $\$ ..^ $/\$ $/\$ $/\$
204	169, 202, 203	sylancr 695	. . 3 ..^ $\$ $\$ ..^ $/\$ $/\$ $/\$ ..^ $\$ ..^ $/\$ $/\$ $/\$
205	64	adantr 481	. . . . . . . . . 10 $/\$ ..^
206		poimirlem28.1	. . . . . . . . . 10
207		poimirlem28.2	. . . . . . . . . . 11 $/\$
208	207	adantlr 751	. . . . . . . . . 10 $/\$ ..^ $/\$
209		xp1st 7198	. . . . . . . . . . . 12 ..^ ..^
210		xp1st 7198	. . . . . . . . . . . 12 ..^ ..^
211		elmapi 7879	. . . . . . . . . . . 12 ..^ ..^
212	209, 210, 211	3syl 18	. . . . . . . . . . 11 ..^ ..^
213	212	adantl 482	. . . . . . . . . 10 $/\$ ..^ ..^
214		xp2nd 7199	. . . . . . . . . . . . 13 ..^
215		fvex 6201	. . . . . . . . . . . . . 14
216		f1oeq1 6127	. . . . . . . . . . . . . 14
217	215, 216	elab 3350	. . . . . . . . . . . . 13
218	214, 217	sylib 208	. . . . . . . . . . . 12 ..^
219	209, 218	syl 17	. . . . . . . . . . 11 ..^
220	219	adantl 482	. . . . . . . . . 10 $/\$ ..^
221		xp2nd 7199	. . . . . . . . . . 11 ..^
222	221	adantl 482	. . . . . . . . . 10 $/\$ ..^
223	205, 206, 208, 213, 220, 222	poimirlem24 33433	. . . . . . . . 9 $/\$ ..^ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
224	209	adantl 482	. . . . . . . . . 10 $/\$ ..^ ..^
225		1st2nd2 7205	. . . . . . . . . . . . . . 15 ..^
226	225	csbeq1d 3540	. . . . . . . . . . . . . 14 ..^
227	226	eqeq2d 2632	. . . . . . . . . . . . 13 ..^
228	227	rexbidv 3052	. . . . . . . . . . . 12 ..^ $\$ $\$
229	228	ralbidv 2986	. . . . . . . . . . 11 ..^ $\$ $\$
230	229	anbi1d 741	. . . . . . . . . 10 ..^ $\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
231	224, 230	syl 17	. . . . . . . . 9 $/\$ ..^ $\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
232	223, 231	bitr4d 271	. . . . . . . 8 $/\$ ..^ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
233		frn 6053	. . . . . . . . . . . . . . 15
234	102, 233	syl 17	. . . . . . . . . . . . . 14
235	234	anim2i 593	. . . . . . . . . . . . 13 $/\$ $/\$
236		dfss3 3592	. . . . . . . . . . . . . 14
237		vex 3203	. . . . . . . . . . . . . . . 16
238		eqid 2622	. . . . . . . . . . . . . . . . 17
239	238	elrnmpt 5372	. . . . . . . . . . . . . . . 16
240	237, 239	ax-mp 5	. . . . . . . . . . . . . . 15
241	240	ralbii 2980	. . . . . . . . . . . . . 14
242	236, 241	sylbb 209	. . . . . . . . . . . . 13
243		1eluzge0 11732	. . . . . . . . . . . . . . . . 17
244		fzss1 12380	. . . . . . . . . . . . . . . . 17
245		ssralv 3666	. . . . . . . . . . . . . . . . 17
246	243, 244, 245	mp2b 10	. . . . . . . . . . . . . . . 16
247	64	nncnd 11036	. . . . . . . . . . . . . . . . . . . . . . . 24
248		npcan1 10455	. . . . . . . . . . . . . . . . . . . . . . . 24
249	247, 248	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23
250		peano2zm 11420	. . . . . . . . . . . . . . . . . . . . . . . . 25
251	186, 250	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24
252		uzid 11702	. . . . . . . . . . . . . . . . . . . . . . . 24
253		peano2uz 11741	. . . . . . . . . . . . . . . . . . . . . . . 24
254	251, 252, 253	3syl 18	. . . . . . . . . . . . . . . . . . . . . . 23
255	249, 254	eqeltrrd 2702	. . . . . . . . . . . . . . . . . . . . . 22
256		fzss2 12381	. . . . . . . . . . . . . . . . . . . . . 22
257	255, 256	syl 17	. . . . . . . . . . . . . . . . . . . . 21
258	257	sselda 3603	. . . . . . . . . . . . . . . . . . . 20 $/\$
259	258	adantlr 751	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
260		simplr 792	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
261		ssel2 3598	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
262		elmapi 7879	. . . . . . . . . . . . . . . . . . . . . . 23
263	261, 262	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
264	260, 263	sylan 488	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
265		poimirlem28.3	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
266		elfzelz 12342	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
267	266	zred 11482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
268	267	ltnrd 10171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
269		breq1 4656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
270	269	notbid 308	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
271	268, 270	syl5ibcom 235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
272	271	necon2ad 2809	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
273	272	3ad2ant1 1082	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
274	273	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
275	265, 274	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
276	275	3exp2 1285	. . . . . . . . . . . . . . . . . . . . . . . 24
277	276	imp31 448	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
278	277	necon2d 2817	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
279	278	adantllr 755	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
280	264, 279	syldan 487	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
281	280	reximdva 3017	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
282	259, 281	syldan 487	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
283	282	ralimdva 2962	. . . . . . . . . . . . . . . . 17 $/\$
284	283	imp 445	. . . . . . . . . . . . . . . 16 $/\$ $/\$
285	246, 284	sylan2 491	. . . . . . . . . . . . . . 15 $/\$ $/\$
286	285	biantrurd 529	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
287		nnuz 11723	. . . . . . . . . . . . . . . . . . . . . 22
288	64, 287	syl6eleq 2711	. . . . . . . . . . . . . . . . . . . . 21
289		fzm1 12420	. . . . . . . . . . . . . . . . . . . . 21 $\/$
290	288, 289	syl 17	. . . . . . . . . . . . . . . . . . . 20 $\/$
291		elun 3753	. . . . . . . . . . . . . . . . . . . . 21 $\/$
292	180	orbi2i 541	. . . . . . . . . . . . . . . . . . . . 21 $\/$ $\/$
293	291, 292	bitri 264	. . . . . . . . . . . . . . . . . . . 20 $\/$
294	290, 293	syl6bbr 278	. . . . . . . . . . . . . . . . . . 19
295	294	eqrdv 2620	. . . . . . . . . . . . . . . . . 18
296	295	raleqdv 3144	. . . . . . . . . . . . . . . . 17
297		ralunb 3794	. . . . . . . . . . . . . . . . 17 $/\$
298	296, 297	syl6bb 276	. . . . . . . . . . . . . . . 16 $/\$
299		fveq2 6191	. . . . . . . . . . . . . . . . . . . . 21
300	299	neeq1d 2853	. . . . . . . . . . . . . . . . . . . 20
301	300	rexbidv 3052	. . . . . . . . . . . . . . . . . . 19
302	301	ralsng 4218	. . . . . . . . . . . . . . . . . 18
303	64, 302	syl 17	. . . . . . . . . . . . . . . . 17
304	303	anbi2d 740	. . . . . . . . . . . . . . . 16 $/\$ $/\$
305	298, 304	bitrd 268	. . . . . . . . . . . . . . 15 $/\$
306	305	ad2antrr 762	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
307		0z 11388	. . . . . . . . . . . . . . . . . . . . . . 23
308		1z 11407	. . . . . . . . . . . . . . . . . . . . . . 23
309		fzshftral 12428	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
310	307, 308, 309	mp3an13 1415	. . . . . . . . . . . . . . . . . . . . . 22
311	186, 250, 310	3syl 18	. . . . . . . . . . . . . . . . . . . . 21
312		0p1e1 11132	. . . . . . . . . . . . . . . . . . . . . . . 24
313	312	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23
314	313, 249	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . 22
315	314	raleqdv 3144	. . . . . . . . . . . . . . . . . . . . 21
316	311, 315	bitrd 268	. . . . . . . . . . . . . . . . . . . 20
317		ovex 6678	. . . . . . . . . . . . . . . . . . . . . . 23
318		eqeq1 2626	. . . . . . . . . . . . . . . . . . . . . . . 24
319	318	rexbidv 3052	. . . . . . . . . . . . . . . . . . . . . . 23
320	317, 319	sbcie 3470	. . . . . . . . . . . . . . . . . . . . . 22
321	320	ralbii 2980	. . . . . . . . . . . . . . . . . . . . 21
322		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . 24
323	322	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . . . 23
324	323	rexbidv 3052	. . . . . . . . . . . . . . . . . . . . . 22
325	324	cbvralv 3171	. . . . . . . . . . . . . . . . . . . . 21
326	321, 325	bitri 264	. . . . . . . . . . . . . . . . . . . 20
327	316, 326	syl6bb 276	. . . . . . . . . . . . . . . . . . 19
328	327	biimpa 501	. . . . . . . . . . . . . . . . . 18 $/\$
329	328	adantlr 751	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
330		poimirlem28.4	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
331	330	necomd 2849	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
332	331	3exp2 1285	. . . . . . . . . . . . . . . . . . . . . . . 24
333	332	imp31 448	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
334	333	necon2d 2817	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
335	334	adantllr 755	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
336	264, 335	syldan 487	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
337	336	reximdva 3017	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
338	337	ralimdva 2962	. . . . . . . . . . . . . . . . . 18 $/\$
339	338	imp 445	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
340	329, 339	syldan 487	. . . . . . . . . . . . . . . 16 $/\$ $/\$
341	340	biantrud 528	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
342		r19.26 3064	. . . . . . . . . . . . . . 15 $/\$ $/\$
343	341, 342	syl6bbr 278	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
344	286, 306, 343	3bitr2d 296	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
345	235, 242, 344	syl2an 494	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
346	345	pm5.32da 673	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
347	346	anbi2d 740	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
348	347	rexbidva 3049	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
349	348	adantr 481	. . . . . . . 8 $/\$ ..^ $/\$ $/\$ $/\$ $/\$ $/\$
350	194	rexeqdv 3145	. . . . . . . . . . . . . . . . . . 19 $\$
351	350	biimpd 219	. . . . . . . . . . . . . . . . . 18 $\$
352	351	ralimdv 2963	. . . . . . . . . . . . . . . . 17 $\$
353	172	rexeqdv 3145	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
354	353	ralbidv 2986	. . . . . . . . . . . . . . . . . 18 $\$ $\$
355	354	imbi1d 331	. . . . . . . . . . . . . . . . 17 $\$ $\$
356	352, 355	syl5ibrcom 237	. . . . . . . . . . . . . . . 16 $\$
357	356	com23 86	. . . . . . . . . . . . . . 15 $\$
358	357	imp 445	. . . . . . . . . . . . . 14 $/\$ $\$
359	358	adantrd 484	. . . . . . . . . . . . 13 $/\$ $\$ $/\$ $/\$
360	359	pm4.71rd 667	. . . . . . . . . . . 12 $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
361		an12 838	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
362		3anass 1042	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
363	362	anbi2i 730	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
364	361, 363	bitr4i 267	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
365	360, 364	syl6bb 276	. . . . . . . . . . 11 $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
366	365	notbid 308	. . . . . . . . . 10 $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
367	366	pm5.32da 673	. . . . . . . . 9 $\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$
368	367	adantr 481	. . . . . . . 8 $/\$ ..^ $\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$
369	232, 349, 368	3bitr3d 298	. . . . . . 7 $/\$ ..^ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$
370	369	rabbidva 3188	. . . . . 6 ..^ $/\$ $/\$ $/\$ ..^ $\$ $/\$ $/\$ $/\$ $/\$
371		iunrab 4567	. . . . . 6 ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
372		difrab 3901	. . . . . 6 ..^ $\$ $\$ ..^ $/\$ $/\$ $/\$ ..^ $\$ $/\$ $/\$ $/\$ $/\$
373	370, 371, 372	3eqtr4g 2681	. . . . 5 ..^ $/\$ $/\$ $/\$ ..^ $\$ $\$ ..^ $/\$ $/\$ $/\$
374	373	fveq2d 6195	. . . 4 ..^ $/\$ $/\$ $/\$ ..^ $\$ $\$ ..^ $/\$ $/\$ $/\$
375	27, 28	mp1i 13	. . . . 5 $/\$ ..^ $/\$ $/\$ $/\$
376		simpl 473	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
377	376	a1i 11	. . . . . . . . . . 11 ..^ $/\$ $/\$ $/\$
378	377	ss2rabi 3684	. . . . . . . . . 10 ..^ $/\$ $/\$ $/\$ ..^
379	378	sseli 3599	. . . . . . . . 9 ..^ $/\$ $/\$ $/\$ ..^
380		fveq2 6191	. . . . . . . . . . . . . . . . . 18
381	380	breq2d 4665	. . . . . . . . . . . . . . . . 17
382	381	ifbid 4108	. . . . . . . . . . . . . . . 16
383	382	csbeq1d 3540	. . . . . . . . . . . . . . 15
384		fveq2 6191	. . . . . . . . . . . . . . . . . 18
385	384	fveq2d 6195	. . . . . . . . . . . . . . . . 17
386	384	fveq2d 6195	. . . . . . . . . . . . . . . . . . . 20
387	386	imaeq1d 5465	. . . . . . . . . . . . . . . . . . 19
388	387	xpeq1d 5138	. . . . . . . . . . . . . . . . . 18
389	386	imaeq1d 5465	. . . . . . . . . . . . . . . . . . 19
390	389	xpeq1d 5138	. . . . . . . . . . . . . . . . . 18
391	388, 390	uneq12d 3768	. . . . . . . . . . . . . . . . 17
392	385, 391	oveq12d 6668	. . . . . . . . . . . . . . . 16
393	392	csbeq2dv 3992	. . . . . . . . . . . . . . 15
394	383, 393	eqtrd 2656	. . . . . . . . . . . . . 14
395	394	mpteq2dv 4745	. . . . . . . . . . . . 13
396	395	eqeq2d 2632	. . . . . . . . . . . 12
397		eqcom 2629	. . . . . . . . . . . 12
398	396, 397	syl6bb 276	. . . . . . . . . . 11
399	398	elrab 3363	. . . . . . . . . 10 ..^ ..^ $/\$
400	399	simprbi 480	. . . . . . . . 9 ..^
401	379, 400	syl 17	. . . . . . . 8 ..^ $/\$ $/\$ $/\$
402	401	rgen 2922	. . . . . . 7 ..^ $/\$ $/\$ $/\$
403	402	rgenw 2924	. . . . . 6 ..^ $/\$ $/\$ $/\$
404		invdisj 4638	. . . . . 6 ..^ $/\$ $/\$ $/\$ Disj ..^ $/\$ $/\$ $/\$
405	403, 404	mp1i 13	. . . . 5 Disj ..^ $/\$ $/\$ $/\$
406	8, 375, 405	hashiun 14554	. . . 4 ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
407	374, 406	eqtr3d 2658	. . 3 ..^ $\$ $\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
408		fo1st 7188	. . . . . . . . . . . . 13
409		fofun 6116	. . . . . . . . . . . . 13
410	408, 409	ax-mp 5	. . . . . . . . . . . 12
411		ssv 3625	. . . . . . . . . . . . 13 ..^ $/\$ $/\$ $/\$
412		fof 6115	. . . . . . . . . . . . . . 15
413	408, 412	ax-mp 5	. . . . . . . . . . . . . 14
414	413	fdmi 6052	. . . . . . . . . . . . 13
415	411, 414	sseqtr4i 3638	. . . . . . . . . . . 12 ..^ $/\$ $/\$ $/\$
416		fores 6124	. . . . . . . . . . . 12 $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
417	410, 415, 416	mp2an 708	. . . . . . . . . . 11 ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
418		fveq2 6191	. . . . . . . . . . . . . . . . . 18
419	418	eqeq1d 2624	. . . . . . . . . . . . . . . . 17
420		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . 22
421	420	csbeq1d 3540	. . . . . . . . . . . . . . . . . . . . 21
422	421	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . 20
423	422	rexbidv 3052	. . . . . . . . . . . . . . . . . . 19
424	423	ralbidv 2986	. . . . . . . . . . . . . . . . . 18
425	420	fveq2d 6195	. . . . . . . . . . . . . . . . . . . 20
426	425	fveq1d 6193	. . . . . . . . . . . . . . . . . . 19
427	426	eqeq1d 2624	. . . . . . . . . . . . . . . . . 18
428	420	fveq2d 6195	. . . . . . . . . . . . . . . . . . . 20
429	428	fveq1d 6193	. . . . . . . . . . . . . . . . . . 19
430	429	eqeq1d 2624	. . . . . . . . . . . . . . . . . 18
431	424, 427, 430	3anbi123d 1399	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
432	419, 431	anbi12d 747	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
433	432	rexrab 3370	. . . . . . . . . . . . . . 15 ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ $/\$
434		xp1st 7198	. . . . . . . . . . . . . . . . . . . . 21 ..^ ..^
435	434	anim1i 592	. . . . . . . . . . . . . . . . . . . 20 ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
436		eleq1 2689	. . . . . . . . . . . . . . . . . . . . 21 ..^ ..^
437		csbeq1a 3542	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
438	437	eqcoms 2630	. . . . . . . . . . . . . . . . . . . . . . . . . 26
439	438	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . . . . 25
440	439	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . . . . . 24
441	440	rexbidv 3052	. . . . . . . . . . . . . . . . . . . . . . 23
442	441	ralbidv 2986	. . . . . . . . . . . . . . . . . . . . . 22
443		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . 24
444	443	fveq1d 6193	. . . . . . . . . . . . . . . . . . . . . . 23
445	444	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . . 22
446		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . 24
447	446	fveq1d 6193	. . . . . . . . . . . . . . . . . . . . . . 23
448	447	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . . 22
449	442, 445, 448	3anbi123d 1399	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
450	436, 449	anbi12d 747	. . . . . . . . . . . . . . . . . . . 20 ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
451	435, 450	syl5ibcom 235	. . . . . . . . . . . . . . . . . . 19 ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
452	451	adantrl 752	. . . . . . . . . . . . . . . . . 18 ..^ $/\$ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
453	452	expimpd 629	. . . . . . . . . . . . . . . . 17 ..^ $/\$ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
454	453	rexlimiv 3027	. . . . . . . . . . . . . . . 16 ..^ $/\$ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
455		nn0fz0 12437	. . . . . . . . . . . . . . . . . . . . 21
456	174, 455	sylib 208	. . . . . . . . . . . . . . . . . . . 20
457		opelxpi 5148	. . . . . . . . . . . . . . . . . . . 20 ..^ $/\$ ..^
458	456, 457	sylan2 491	. . . . . . . . . . . . . . . . . . 19 ..^ $/\$ ..^
459	458	ancoms 469	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ ..^
460		opelxp2 5151	. . . . . . . . . . . . . . . . . . . . 21 ..^
461		op2ndg 7181	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
462	461	biantrurd 529	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
463		op1stg 7180	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
464		csbeq1a 3542	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
465	464	eqcoms 2630	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
466	465	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
467	463, 466	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
468	467	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
469	468	rexbidv 3052	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
470	469	ralbidv 2986	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
471	463	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
472	471	fveq1d 6193	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
473	472	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
474	463	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
475	474	fveq1d 6193	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
476	475	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
477	470, 473, 476	3anbi123d 1399	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
478	463	biantrud 528	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
479	462, 477, 478	3bitr3d 298	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
480	44, 460, 479	sylancr 695	. . . . . . . . . . . . . . . . . . . 20 ..^ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
481	480	biimpa 501	. . . . . . . . . . . . . . . . . . 19 ..^ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
482		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . 23
483	482	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . . 22
484		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
485	484	csbeq1d 3540	. . . . . . . . . . . . . . . . . . . . . . . . . 26
486	485	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . . . . . . 25
487	486	rexbidv 3052	. . . . . . . . . . . . . . . . . . . . . . . 24
488	487	ralbidv 2986	. . . . . . . . . . . . . . . . . . . . . . 23
489	484	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . 25
490	489	fveq1d 6193	. . . . . . . . . . . . . . . . . . . . . . . 24
491	490	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . . . 23
492	484	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . 25
493	492	fveq1d 6193	. . . . . . . . . . . . . . . . . . . . . . . 24
494	493	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . . . 23
495	488, 491, 494	3anbi123d 1399	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
496	483, 495	anbi12d 747	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
497	484	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . 21
498	496, 497	anbi12d 747	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
499	498	rspcev 3309	. . . . . . . . . . . . . . . . . . 19 ..^ $/\$ $/\$ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ $/\$
500	481, 499	syldan 487	. . . . . . . . . . . . . . . . . 18 ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ $/\$
501	459, 500	sylan 488	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ $/\$
502	501	expl 648	. . . . . . . . . . . . . . . 16 ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ $/\$
503	454, 502	impbid2 216	. . . . . . . . . . . . . . 15 ..^ $/\$ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
504	433, 503	syl5bb 272	. . . . . . . . . . . . . 14 ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
505	504	abbidv 2741	. . . . . . . . . . . . 13 ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
506		dfimafn 6245	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
507	410, 415, 506	mp2an 708	. . . . . . . . . . . . . 14 ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
508		nfv 1843	. . . . . . . . . . . . . . . . . 18
509		nfcv 2764	. . . . . . . . . . . . . . . . . . . 20
510		nfcsb1v 3549	. . . . . . . . . . . . . . . . . . . . . 22
511	510	nfeq2 2780	. . . . . . . . . . . . . . . . . . . . 21
512	509, 511	nfrex 3007	. . . . . . . . . . . . . . . . . . . 20
513	509, 512	nfral 2945	. . . . . . . . . . . . . . . . . . 19
514		nfv 1843	. . . . . . . . . . . . . . . . . . 19
515		nfv 1843	. . . . . . . . . . . . . . . . . . 19
516	513, 514, 515	nf3an 1831	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
517	508, 516	nfan 1828	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
518		nfcv 2764	. . . . . . . . . . . . . . . . 17 ..^
519	517, 518	nfrab 3123	. . . . . . . . . . . . . . . 16 ..^ $/\$ $/\$ $/\$
520		nfv 1843	. . . . . . . . . . . . . . . 16
521	519, 520	nfrex 3007	. . . . . . . . . . . . . . 15 ..^ $/\$ $/\$ $/\$
522		nfv 1843	. . . . . . . . . . . . . . 15 ..^ $/\$ $/\$ $/\$
523		eqeq2 2633	. . . . . . . . . . . . . . . 16
524	523	rexbidv 3052	. . . . . . . . . . . . . . 15 ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
525	521, 522, 524	cbvab 2746	. . . . . . . . . . . . . 14 ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
526	507, 525	eqtri 2644	. . . . . . . . . . . . 13 ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
527		df-rab 2921	. . . . . . . . . . . . 13 ..^ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
528	505, 526, 527	3eqtr4g 2681	. . . . . . . . . . . 12 ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$
529		foeq3 6113	. . . . . . . . . . . 12 ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$
530	528, 529	syl 17	. . . . . . . . . . 11 ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$
531	417, 530	mpbii 223	. . . . . . . . . 10 ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$
532		fof 6115	. . . . . . . . . 10 ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$
533	531, 532	syl 17	. . . . . . . . 9 ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$
534		fvres 6207	. . . . . . . . . . . 12 ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
535		fvres 6207	. . . . . . . . . . . 12 ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
536	534, 535	eqeqan12d 2638	. . . . . . . . . . 11 ..^ $/\$ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
537		simpl 473	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
538	537	a1i 11	. . . . . . . . . . . . . . 15 ..^ $/\$ $/\$ $/\$
539	538	ss2rabi 3684	. . . . . . . . . . . . . 14 ..^ $/\$ $/\$ $/\$ ..^
540	539	sseli 3599	. . . . . . . . . . . . 13 ..^ $/\$ $/\$ $/\$ ..^
541	419	elrab 3363	. . . . . . . . . . . . 13 ..^ ..^ $/\$
542	540, 541	sylib 208	. . . . . . . . . . . 12 ..^ $/\$ $/\$ $/\$ ..^ $/\$
543	539	sseli 3599	. . . . . . . . . . . . 13 ..^ $/\$ $/\$ $/\$ ..^
544		fveq2 6191	. . . . . . . . . . . . . . 15
545	544	eqeq1d 2624	. . . . . . . . . . . . . 14
546	545	elrab 3363	. . . . . . . . . . . . 13 ..^ ..^ $/\$
547	543, 546	sylib 208	. . . . . . . . . . . 12 ..^ $/\$ $/\$ $/\$ ..^ $/\$
548		eqtr3 2643	. . . . . . . . . . . . . 14 $/\$
549		xpopth 7207	. . . . . . . . . . . . . . . . 17 ..^ $/\$ ..^ $/\$
550	549	biimpd 219	. . . . . . . . . . . . . . . 16 ..^ $/\$ ..^ $/\$
551	550	ancomsd 470	. . . . . . . . . . . . . . 15 ..^ $/\$ ..^ $/\$
552	551	expdimp 453	. . . . . . . . . . . . . 14 ..^ $/\$ ..^ $/\$
553	548, 552	sylan2 491	. . . . . . . . . . . . 13 ..^ $/\$ ..^ $/\$ $/\$
554	553	an4s 869	. . . . . . . . . . . 12 ..^ $/\$ $/\$ ..^ $/\$
555	542, 547, 554	syl2an 494	. . . . . . . . . . 11 ..^ $/\$ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
556	536, 555	sylbid 230	. . . . . . . . . 10 ..^ $/\$ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
557	556	rgen2a 2977	. . . . . . . . 9 ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
558	533, 557	jctir 561	. . . . . . . 8 ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
559		dff13 6512	. . . . . . . 8 ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
560	558, 559	sylibr 224	. . . . . . 7 ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$
561		df-f1o 5895	. . . . . . 7 ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$
562	560, 531, 561	sylanbrc 698	. . . . . 6 ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$
563		rabfi 8185	. . . . . . . . 9 ..^ ..^ $/\$ $/\$ $/\$
564	27, 563	ax-mp 5	. . . . . . . 8 ..^ $/\$ $/\$ $/\$
565	564	elexi 3213	. . . . . . 7 ..^ $/\$ $/\$ $/\$
566	565	f1oen 7976	. . . . . 6 ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$
567	562, 566	syl 17	. . . . 5 ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$
568		rabfi 8185	. . . . . . 7 ..^ ..^ $/\$ $/\$
569	24, 568	ax-mp 5	. . . . . 6 ..^ $/\$ $/\$
570		hashen 13135	. . . . . 6 ..^ $/\$ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$
571	564, 569, 570	mp2an 708	. . . . 5 ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$
572	567, 571	sylibr 224	. . . 4 ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$
573	572	oveq2d 6666	. . 3 ..^ $\$ ..^ $/\$ $/\$ $/\$ ..^ $\$ ..^ $/\$ $/\$
574	204, 407, 573	3eqtr3d 2664	. 2 ..^ $/\$ $/\$ $/\$ ..^ $\$ ..^ $/\$ $/\$
575	167, 574	breqtrd 4679	1 ..^ $\$ ..^ $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1483

wex 1704

wcel 1990

weu 2470

cab 2608

wne 2794

wral 2912

wrex 2913

wreu 2914

crab 2916

cvv 3200

wsbc 3435

csb 3533 $\$ cdif 3571

cun 3572

cin 3573

wss 3574

c0 3915

cif 4086

csn 4177

cop 4183

ciun 4520 Disj wdisj 4620 class class class wbr 4653

cmpt 4729

cxp 5112

cdm 5114

crn 5115

cres 5116

cima 5117

wfun 5882

wf 5884

wf1 5885

wfo 5886

wf1o 5887

cfv 5888 (class class class)co 6650

cof 6895

c1st 7166

c2nd 7167

cmap 7857

cen 7952

cfn 7955

cc 9934

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

csu 14416

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: poimirlem28 33437

W3C validator