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

Theorem poimirlem26 32030
 Description: Lemma for poimir 32037 showing an even difference between the number of admissible faces and the number of admissible simplices. Equation (6) of [Kulpa] p. 548. (Contributed by Brendan Leahy, 21-Aug-2020.)
Hypotheses
Ref Expression
poimir.0
poimirlem28.1
poimirlem28.2
Assertion
Ref Expression
poimirlem26 ..^ ..^
Distinct variable groups:   ,,,,,   ,   ,   ,,,,   ,,,,,   ,,,,,,   ,,,,,   ,,,
Allowed substitution hints:   ()   ()   (,,)

Proof of Theorem poimirlem26
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fzofi 12225 . . . . . 6 ..^
2 fzfi 12223 . . . . . 6
3 mapfi 7888 . . . . . 6 ..^ ..^
41, 2, 3mp2an 686 . . . . 5 ..^
5 mapfi 7888 . . . . . . 7
62, 2, 5mp2an 686 . . . . . 6
7 f1of 5828 . . . . . . . 8
87ss2abi 3487 . . . . . . 7
9 ovex 6336 . . . . . . . 8
109, 9mapval 7502 . . . . . . 7
118, 10sseqtr4i 3451 . . . . . 6
12 ssfi 7810 . . . . . 6
136, 11, 12mp2an 686 . . . . 5
144, 13pm3.2i 462 . . . 4 ..^
15 xpfi 7860 . . . 4 ..^ ..^
1614, 15mp1i 13 . . 3 ..^
17 2z 10993 . . . 4
1817a1i 11 . . 3
19 snfi 7668 . . . . . . 7
20 fzfi 12223 . . . . . . . 8
21 rabfi 7814 . . . . . . . 8
2220, 21ax-mp 5 . . . . . . 7
23 xpfi 7860 . . . . . . 7
2419, 22, 23mp2an 686 . . . . . 6
25 hashcl 12576 . . . . . 6
2624, 25ax-mp 5 . . . . 5
2726nn0zi 10986 . . . 4
2827a1i 11 . . 3 ..^
29 poimir.0 . . . . . . . . . 10
3029adantr 472 . . . . . . . . 9 ..^
3130adantr 472 . . . . . . . 8 ..^
32 nfv 1769 . . . . . . . . . 10
33 nfcsb1v 3365 . . . . . . . . . . 11
3433nfeq2 2627 . . . . . . . . . 10
3532, 34nfim 2023 . . . . . . . . 9
36 oveq2 6316 . . . . . . . . . . . . . . 15
3736imaeq2d 5174 . . . . . . . . . . . . . 14
3837xpeq1d 4862 . . . . . . . . . . . . 13
39 oveq1 6315 . . . . . . . . . . . . . . . 16
4039oveq1d 6323 . . . . . . . . . . . . . . 15
4140imaeq2d 5174 . . . . . . . . . . . . . 14
4241xpeq1d 4862 . . . . . . . . . . . . 13
4338, 42uneq12d 3580 . . . . . . . . . . . 12
4443oveq2d 6324 . . . . . . . . . . 11
4544eqeq2d 2481 . . . . . . . . . 10
46 csbeq1a 3358 . . . . . . . . . . 11
4746eqeq2d 2481 . . . . . . . . . 10
4845, 47imbi12d 327 . . . . . . . . 9
49 nfv 1769 . . . . . . . . . . 11
50 nfcsb1v 3365 . . . . . . . . . . . 12
5150nfeq2 2627 . . . . . . . . . . 11
5249, 51nfim 2023 . . . . . . . . . 10
53 fveq2 5879 . . . . . . . . . . . . 13
54 fveq2 5879 . . . . . . . . . . . . . . . 16
5554imaeq1d 5173 . . . . . . . . . . . . . . 15
5655xpeq1d 4862 . . . . . . . . . . . . . 14
5754imaeq1d 5173 . . . . . . . . . . . . . . 15
5857xpeq1d 4862 . . . . . . . . . . . . . 14
5956, 58uneq12d 3580 . . . . . . . . . . . . 13
6053, 59oveq12d 6326 . . . . . . . . . . . 12
6160eqeq2d 2481 . . . . . . . . . . 11
62 csbeq1a 3358 . . . . . . . . . . . 12
6362eqeq2d 2481 . . . . . . . . . . 11
6461, 63imbi12d 327 . . . . . . . . . 10
65 poimirlem28.1 . . . . . . . . . 10
6652, 64, 65chvar 2119 . . . . . . . . 9
6735, 48, 66chvar 2119 . . . . . . . 8
68 simpll 768 . . . . . . . . 9 ..^
69 poimirlem28.2 . . . . . . . . 9
7068, 69sylan 479 . . . . . . . 8 ..^
71 xp1st 6842 . . . . . . . . . 10 ..^ ..^
72 elmapi 7511 . . . . . . . . . 10 ..^ ..^
7371, 72syl 17 . . . . . . . . 9 ..^ ..^
7473ad2antlr 741 . . . . . . . 8 ..^ ..^
75 xp2nd 6843 . . . . . . . . . 10 ..^
76 fvex 5889 . . . . . . . . . . 11
77 f1oeq1 5818 . . . . . . . . . . 11
7876, 77elab 3173 . . . . . . . . . 10
7975, 78sylib 201 . . . . . . . . 9 ..^
8079ad2antlr 741 . . . . . . . 8 ..^
81 nfcv 2612 . . . . . . . . . . . . 13
82 nfcv 2612 . . . . . . . . . . . . . 14
8382, 33nfcsb 3367 . . . . . . . . . . . . 13
8481, 83nfne 2742 . . . . . . . . . . . 12
85 nfcv 2612 . . . . . . . . . . . . . . 15
8685, 50, 62cbvcsb 3354 . . . . . . . . . . . . . 14
8746csbeq2dv 3785 . . . . . . . . . . . . . 14
8886, 87syl5eq 2517 . . . . . . . . . . . . 13
8988neeq2d 2703 . . . . . . . . . . . 12
9084, 89rspc 3130 . . . . . . . . . . 11
9190impcom 437 . . . . . . . . . 10
9291adantll 728 . . . . . . . . 9 ..^
93 1st2nd2 6849 . . . . . . . . . . 11 ..^
9493csbeq1d 3356 . . . . . . . . . 10 ..^
9594ad3antlr 745 . . . . . . . . 9 ..^
9692, 95neeqtrd 2712 . . . . . . . 8 ..^
9731, 67, 70, 74, 80, 96poimirlem25 32029 . . . . . . 7 ..^
98 nfv 1769 . . . . . . . . . . . . . 14
9983nfeq2 2627 . . . . . . . . . . . . . 14
10088eqeq2d 2481 . . . . . . . . . . . . . 14
10198, 99, 100cbvrex 3002 . . . . . . . . . . . . 13
10294eqeq2d 2481 . . . . . . . . . . . . . 14 ..^
103102rexbidv 2892 . . . . . . . . . . . . 13 ..^
104101, 103syl5rbb 266 . . . . . . . . . . . 12 ..^
105104ralbidv 2829 . . . . . . . . . . 11 ..^
106 iba 511 . . . . . . . . . . 11
107105, 106sylan9bb 714 . . . . . . . . . 10 ..^
108107rabbidv 3022 . . . . . . . . 9 ..^
109108fveq2d 5883 . . . . . . . 8 ..^
110109adantll 728 . . . . . . 7 ..^
11197, 110breqtrd 4420 . . . . . 6 ..^
112111ex 441 . . . . 5 ..^
113 dvds0 14395 . . . . . . . 8
11417, 113ax-mp 5 . . . . . . 7
115 hash0 12586 . . . . . . 7
116114, 115breqtrri 4421 . . . . . 6
117 simpr 468 . . . . . . . . . 10
118117con3i 142 . . . . . . . . 9
119118ralrimivw 2810 . . . . . . . 8
120 rabeq0 3757 . . . . . . . 8
121119, 120sylibr 217 . . . . . . 7
122121fveq2d 5883 . . . . . 6
123116, 122syl5breqr 4432 . . . . 5
124112, 123pm2.61d1 164 . . . 4 ..^
125 hashxp 12647 . . . . . 6
12619, 22, 125mp2an 686 . . . . 5
127 vex 3034 . . . . . . 7
128 hashsng 12587 . . . . . . 7
129127, 128ax-mp 5 . . . . . 6
130129oveq1i 6318 . . . . 5
131 hashcl 12576 . . . . . . . 8
13222, 131ax-mp 5 . . . . . . 7
133132nn0cni 10905 . . . . . 6
134133mulid2i 9664 . . . . 5
135126, 130, 1343eqtri 2497 . . . 4
136124, 135syl6breqr 4436 . . 3 ..^
13716, 18, 28, 136fsumdvds 14425 . 2 ..^
1384, 13, 15mp2an 686 . . . . . 6 ..^
139 xpfi 7860 . . . . . 6 ..^ ..^
140138, 20, 139mp2an 686 . . . . 5 ..^
141 rabfi 7814 . . . . 5 ..^ ..^
142140, 141ax-mp 5 . . . 4 ..^
14329nncnd 10647 . . . . . . . . . . . 12
144 npcan1 10065 . . . . . . . . . . . 12
145143, 144syl 17 . . . . . . . . . . 11
146 nnm1nn0 10935 . . . . . . . . . . . . . 14
14729, 146syl 17 . . . . . . . . . . . . 13
148147nn0zd 11061 . . . . . . . . . . . 12
149 uzid 11197 . . . . . . . . . . . 12
150 peano2uz 11235 . . . . . . . . . . . 12
151148, 149, 1503syl 18 . . . . . . . . . . 11
152145, 151eqeltrrd 2550 . . . . . . . . . 10
153 fzss2 11864 . . . . . . . . . 10
154 ssralv 3479 . . . . . . . . . 10
155152, 153, 1543syl 18 . . . . . . . . 9
156155adantr 472 . . . . . . . 8
157 raldifb 3562 . . . . . . . . . . . 12
158 nfv 1769 . . . . . . . . . . . . . . 15
159 nfcsb1v 3365 . . . . . . . . . . . . . . . 16
160159nfeq2 2627 . . . . . . . . . . . . . . 15
161158, 160nfan 2031 . . . . . . . . . . . . . 14
162 nfv 1769 . . . . . . . . . . . . . 14
163161, 162nfan 2031 . . . . . . . . . . . . 13
164 nnel 2752 . . . . . . . . . . . . . . . . 17
165 elsn 3973 . . . . . . . . . . . . . . . . 17
166164, 165bitri 257 . . . . . . . . . . . . . . . 16
167 csbeq1a 3358 . . . . . . . . . . . . . . . . . . . . 21
168167eqeq2d 2481 . . . . . . . . . . . . . . . . . . . 20
169168biimparc 495 . . . . . . . . . . . . . . . . . . 19
17029nnred 10646 . . . . . . . . . . . . . . . . . . . . . . . . . 26
171170ltm1d 10561 . . . . . . . . . . . . . . . . . . . . . . . . 25
172147nn0red 10950 . . . . . . . . . . . . . . . . . . . . . . . . . 26
173172, 170ltnled 9799 . . . . . . . . . . . . . . . . . . . . . . . . 25
174171, 173mpbid 215 . . . . . . . . . . . . . . . . . . . . . . . 24
175 elfzle2 11829 . . . . . . . . . . . . . . . . . . . . . . . 24
176174, 175nsyl 125 . . . . . . . . . . . . . . . . . . . . . . 23
177 eleq1 2537 . . . . . . . . . . . . . . . . . . . . . . . 24
178177notbid 301 . . . . . . . . . . . . . . . . . . . . . . 23
179176, 178syl5ibrcom 230 . . . . . . . . . . . . . . . . . . . . . 22
180179con2d 119 . . . . . . . . . . . . . . . . . . . . 21
181180imp 436 . . . . . . . . . . . . . . . . . . . 20
182 eqeq2 2482 . . . . . . . . . . . . . . . . . . . . 21
183182notbid 301 . . . . . . . . . . . . . . . . . . . 20
184181, 183syl5ibcom 228 . . . . . . . . . . . . . . . . . . 19
185169, 184syl5 32 . . . . . . . . . . . . . . . . . 18
186185expdimp 444 . . . . . . . . . . . . . . . . 17
187186an32s 821 . . . . . . . . . . . . . . . 16
188166, 187syl5bi 225 . . . . . . . . . . . . . . 15
189 idd 24 . . . . . . . . . . . . . . 15
190188, 189jad 167 . . . . . . . . . . . . . 14
191190adantr 472 . . . . . . . . . . . . 13
192163, 191ralimdaa 2801 . . . . . . . . . . . 12
193157, 192syl5bir 226 . . . . . . . . . . 11
194193con3d 140 . . . . . . . . . 10
195 dfrex2 2837 . . . . . . . . . 10
196 dfrex2 2837 . . . . . . . . . 10
197194, 195, 1963imtr4g 278 . . . . . . . . 9
198197ralimdva 2805 . . . . . . . 8
199156, 198syld 44 . . . . . . 7
200199expimpd 614 . . . . . 6
201200adantr 472 . . . . 5 ..^
202201ss2rabdv 3496 . . . 4 ..^ ..^
203 hashssdif 12627 . . . 4 ..^ ..^ ..^ ..^ ..^ ..^ ..^
204142, 202, 203sylancr 676 . . 3 ..^ ..^ ..^ ..^
205 xp2nd 6843 . . . . . . . 8 ..^
206 df-ne 2643 . . . . . . . . . . . 12
207206ralbii 2823 . . . . . . . . . . 11
208 ralnex 2834 . . . . . . . . . . 11
209207, 208bitri 257 . . . . . . . . . 10
21029nnnn0d 10949 . . . . . . . . . . . . . . . . . . 19
211 nn0uz 11217 . . . . . . . . . . . . . . . . . . 19
212210, 211syl6eleq 2559 . . . . . . . . . . . . . . . . . 18
213145, 212eqeltrd 2549 . . . . . . . . . . . . . . . . 17
214 fzsplit2 11850 . . . . . . . . . . . . . . . . 17
215213, 152, 214syl2anc 673 . . . . . . . . . . . . . . . 16
216145oveq1d 6323 . . . . . . . . . . . . . . . . . 18
21729nnzd 11062 . . . . . . . . . . . . . . . . . . 19
218 fzsn 11866 . . . . . . . . . . . . . . . . . . 19
219217, 218syl 17 . . . . . . . . . . . . . . . . . 18
220216, 219eqtrd 2505 . . . . . . . . . . . . . . . . 17
221220uneq2d 3579 . . . . . . . . . . . . . . . 16
222215, 221eqtrd 2505 . . . . . . . . . . . . . . 15
223222raleqdv 2979 . . . . . . . . . . . . . 14
224 difss 3549 . . . . . . . . . . . . . . . . . 18
225 ssrexv 3480 . . . . . . . . . . . . . . . . . 18
226224, 225ax-mp 5 . . . . . . . . . . . . . . . . 17
227226ralimi 2796 . . . . . . . . . . . . . . . 16
228227biantrurd 516 . . . . . . . . . . . . . . 15
229 ralunb 3606 . . . . . . . . . . . . . . 15
230228, 229syl6rbbr 272 . . . . . . . . . . . . . 14
231223, 230sylan9bb 714 . . . . . . . . . . . . 13
232231adantlr 729 . . . . . . . . . . . 12
233 nn0fz0 11916 . . . . . . . . . . . . . . . 16
234210, 233sylib 201 . . . . . . . . . . . . . . 15
235234ad2antrr 740 . . . . . . . . . . . . . 14
236 eqeq1 2475 . . . . . . . . . . . . . . . . 17
237236rexbidv 2892 . . . . . . . . . . . . . . . 16
238237rspcva 3134 . . . . . . . . . . . . . . 15
239 nfv 1769 . . . . . . . . . . . . . . . . 17
240 nfcv 2612 . . . . . . . . . . . . . . . . . 18
241 nfre1 2846 . . . . . . . . . . . . . . . . . 18
242240, 241nfral 2789 . . . . . . . . . . . . . . . . 17
243239, 242nfan 2031 . . . . . . . . . . . . . . . 16
244 eleq1 2537 . . . . . . . . . . . . . . . . . . . . . . . 24
245244notbid 301 . . . . . . . . . . . . . . . . . . . . . . 23
246176, 245syl5ibcom 228 . . . . . . . . . . . . . . . . . . . . . 22
247246ad3antrrr 744 . . . . . . . . . . . . . . . . . . . . 21
248 eldifsn 4088 . . . . . . . . . . . . . . . . . . . . . . . 24
249 diffi 7821 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
25020, 249ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
251 ssrab2 3500 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
252 ssdomg 7633 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
253250, 251, 252mp2 9 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
254 snssi 4107 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
255 hashssdif 12627 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
25620, 254, 255sylancr 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
257 ax-1cn 9615 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
258 addsub 9906 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
259257, 257, 258mp3an23 1382 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
260143, 259syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
261 hashfz0 12645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
262210, 261syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
263 fvex 5889 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
264 hashsng 12587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
265263, 264mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
266262, 265oveq12d 6326 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
267 hashfz0 12645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
26829, 146, 2673syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
269260, 266, 2683eqtr4d 2515 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
270256, 269sylan9eqr 2527 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
271 fzfi 12223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
272 hashen 12568 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32