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

Theorem poimirlem6 32010
 Description: Lemma for poimir 32037 establishing, for a face of a simplex defined by a walk along the edges of an -cube, the single dimension in which successive vertices before the opposite vertex differ. (Contributed by Brendan Leahy, 21-Aug-2020.)
Hypotheses
Ref Expression
poimir.0
poimirlem22.s ..^
poimirlem9.1
poimirlem9.2
poimirlem6.3
Assertion
Ref Expression
poimirlem6
Distinct variable groups:   ,,,,   ,,,   ,,,   ,,,   ,,,   ,,,   ,   ,,,,   ,,   ,,   ,   ,,   ,   ,,,,
Allowed substitution hints:   ()   ()   ()

Proof of Theorem poimirlem6
StepHypRef Expression
1 poimirlem9.1 . . . . . . . 8
2 elrabi 3181 . . . . . . . . 9 ..^ ..^
3 poimirlem22.s . . . . . . . . 9 ..^
42, 3eleq2s 2567 . . . . . . . 8 ..^
51, 4syl 17 . . . . . . 7 ..^
6 xp1st 6842 . . . . . . 7 ..^ ..^
75, 6syl 17 . . . . . 6 ..^
8 xp2nd 6843 . . . . . 6 ..^
97, 8syl 17 . . . . 5
10 fvex 5889 . . . . . 6
11 f1oeq1 5818 . . . . . 6
1210, 11elab 3173 . . . . 5
139, 12sylib 201 . . . 4
14 f1of 5828 . . . 4
1513, 14syl 17 . . 3
16 poimirlem9.2 . . . . . . . . 9
17 elfznn 11854 . . . . . . . . 9
1816, 17syl 17 . . . . . . . 8
1918nnzd 11062 . . . . . . 7
20 peano2zm 11004 . . . . . . 7
2119, 20syl 17 . . . . . 6
22 poimir.0 . . . . . . 7
2322nnzd 11062 . . . . . 6
2421zred 11063 . . . . . . 7
2518nnred 10646 . . . . . . 7
2622nnred 10646 . . . . . . 7
2725lem1d 10562 . . . . . . 7
28 nnm1nn0 10935 . . . . . . . . . 10
2922, 28syl 17 . . . . . . . . 9
3029nn0red 10950 . . . . . . . 8
31 elfzle2 11829 . . . . . . . . 9
3216, 31syl 17 . . . . . . . 8
3326lem1d 10562 . . . . . . . 8
3425, 30, 26, 32, 33letrd 9809 . . . . . . 7
3524, 25, 26, 27, 34letrd 9809 . . . . . 6
36 eluz2 11188 . . . . . 6
3721, 23, 35, 36syl3anbrc 1214 . . . . 5
38 fzss2 11864 . . . . 5
3937, 38syl 17 . . . 4
40 poimirlem6.3 . . . 4
4139, 40sseldd 3419 . . 3
4215, 41ffvelrnd 6038 . 2
43 xp1st 6842 . . . . . . . . . . . . 13 ..^ ..^
447, 43syl 17 . . . . . . . . . . . 12 ..^
45 elmapfn 7512 . . . . . . . . . . . 12 ..^
4644, 45syl 17 . . . . . . . . . . 11
4746adantr 472 . . . . . . . . . 10
48 1ex 9656 . . . . . . . . . . . . . . 15
49 fnconstg 5784 . . . . . . . . . . . . . . 15
5048, 49ax-mp 5 . . . . . . . . . . . . . 14
51 c0ex 9655 . . . . . . . . . . . . . . 15
52 fnconstg 5784 . . . . . . . . . . . . . . 15
5351, 52ax-mp 5 . . . . . . . . . . . . . 14
5450, 53pm3.2i 462 . . . . . . . . . . . . 13
55 dff1o3 5834 . . . . . . . . . . . . . . . . 17
5655simprbi 471 . . . . . . . . . . . . . . . 16
5713, 56syl 17 . . . . . . . . . . . . . . 15
58 imain 5669 . . . . . . . . . . . . . . 15
5957, 58syl 17 . . . . . . . . . . . . . 14
60 elfznn 11854 . . . . . . . . . . . . . . . . . . . 20
6140, 60syl 17 . . . . . . . . . . . . . . . . . . 19
6261nnred 10646 . . . . . . . . . . . . . . . . . 18
6362ltm1d 10561 . . . . . . . . . . . . . . . . 17
64 fzdisj 11852 . . . . . . . . . . . . . . . . 17
6563, 64syl 17 . . . . . . . . . . . . . . . 16
6665imaeq2d 5174 . . . . . . . . . . . . . . 15
67 ima0 5189 . . . . . . . . . . . . . . 15
6866, 67syl6eq 2521 . . . . . . . . . . . . . 14
6959, 68eqtr3d 2507 . . . . . . . . . . . . 13
70 fnun 5692 . . . . . . . . . . . . 13
7154, 69, 70sylancr 676 . . . . . . . . . . . 12
7261nncnd 10647 . . . . . . . . . . . . . . . . . . . 20
73 npcan1 10065 . . . . . . . . . . . . . . . . . . . 20
7472, 73syl 17 . . . . . . . . . . . . . . . . . . 19
75 nnuz 11218 . . . . . . . . . . . . . . . . . . . 20
7661, 75syl6eleq 2559 . . . . . . . . . . . . . . . . . . 19
7774, 76eqeltrd 2549 . . . . . . . . . . . . . . . . . 18
78 nnm1nn0 10935 . . . . . . . . . . . . . . . . . . . . . . . . 25
7961, 78syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24
8079nn0zd 11061 . . . . . . . . . . . . . . . . . . . . . . 23
81 uzid 11197 . . . . . . . . . . . . . . . . . . . . . . 23
8280, 81syl 17 . . . . . . . . . . . . . . . . . . . . . 22
83 peano2uz 11235 . . . . . . . . . . . . . . . . . . . . . 22
8482, 83syl 17 . . . . . . . . . . . . . . . . . . . . 21
8574, 84eqeltrrd 2550 . . . . . . . . . . . . . . . . . . . 20
86 uzss 11203 . . . . . . . . . . . . . . . . . . . 20
8785, 86syl 17 . . . . . . . . . . . . . . . . . . 19
8861nnzd 11062 . . . . . . . . . . . . . . . . . . . 20
89 elfzle2 11829 . . . . . . . . . . . . . . . . . . . . . 22
9040, 89syl 17 . . . . . . . . . . . . . . . . . . . . 21
9162, 24, 26, 90, 35letrd 9809 . . . . . . . . . . . . . . . . . . . 20
92 eluz2 11188 . . . . . . . . . . . . . . . . . . . 20
9388, 23, 91, 92syl3anbrc 1214 . . . . . . . . . . . . . . . . . . 19
9487, 93sseldd 3419 . . . . . . . . . . . . . . . . . 18
95 fzsplit2 11850 . . . . . . . . . . . . . . . . . 18
9677, 94, 95syl2anc 673 . . . . . . . . . . . . . . . . 17
9774oveq1d 6323 . . . . . . . . . . . . . . . . . 18
9897uneq2d 3579 . . . . . . . . . . . . . . . . 17
9996, 98eqtrd 2505 . . . . . . . . . . . . . . . 16
10099imaeq2d 5174 . . . . . . . . . . . . . . 15
101 imaundi 5254 . . . . . . . . . . . . . . 15
102100, 101syl6eq 2521 . . . . . . . . . . . . . 14
103 f1ofo 5835 . . . . . . . . . . . . . . . 16
10413, 103syl 17 . . . . . . . . . . . . . . 15
105 foima 5811 . . . . . . . . . . . . . . 15
106104, 105syl 17 . . . . . . . . . . . . . 14
107102, 106eqtr3d 2507 . . . . . . . . . . . . 13
108107fneq2d 5677 . . . . . . . . . . . 12
10971, 108mpbid 215 . . . . . . . . . . 11
110109adantr 472 . . . . . . . . . 10
111 ovex 6336 . . . . . . . . . . 11
112111a1i 11 . . . . . . . . . 10
113 inidm 3632 . . . . . . . . . 10
114 eqidd 2472 . . . . . . . . . 10
115 imaundi 5254 . . . . . . . . . . . . . . . . . 18
116 fzpred 11870 . . . . . . . . . . . . . . . . . . . 20
11793, 116syl 17 . . . . . . . . . . . . . . . . . . 19
118117imaeq2d 5174 . . . . . . . . . . . . . . . . . 18
119 f1ofn 5829 . . . . . . . . . . . . . . . . . . . . 21
12013, 119syl 17 . . . . . . . . . . . . . . . . . . . 20
121 fnsnfv 5940 . . . . . . . . . . . . . . . . . . . 20
122120, 41, 121syl2anc 673 . . . . . . . . . . . . . . . . . . 19
123122uneq1d 3578 . . . . . . . . . . . . . . . . . 18
124115, 118, 1233eqtr4a 2531 . . . . . . . . . . . . . . . . 17
125124xpeq1d 4862 . . . . . . . . . . . . . . . 16
126 xpundir 4893 . . . . . . . . . . . . . . . 16
127125, 126syl6eq 2521 . . . . . . . . . . . . . . 15
128127uneq2d 3579 . . . . . . . . . . . . . 14
129 un12 3583 . . . . . . . . . . . . . 14
130128, 129syl6eq 2521 . . . . . . . . . . . . 13
131130fveq1d 5881 . . . . . . . . . . . 12
132131ad2antrr 740 . . . . . . . . . . 11
133 fnconstg 5784 . . . . . . . . . . . . . . . . 17
13451, 133ax-mp 5 . . . . . . . . . . . . . . . 16
13550, 134pm3.2i 462 . . . . . . . . . . . . . . 15
136 imain 5669 . . . . . . . . . . . . . . . . 17
13757, 136syl 17 . . . . . . . . . . . . . . . 16
13879nn0red 10950 . . . . . . . . . . . . . . . . . . . 20
139 peano2re 9824 . . . . . . . . . . . . . . . . . . . . 21
14062, 139syl 17 . . . . . . . . . . . . . . . . . . . 20
14162ltp1d 10559 . . . . . . . . . . . . . . . . . . . 20
142138, 62, 140, 63, 141lttrd 9813 . . . . . . . . . . . . . . . . . . 19
143 fzdisj 11852 . . . . . . . . . . . . . . . . . . 19
144142, 143syl 17 . . . . . . . . . . . . . . . . . 18
145144imaeq2d 5174 . . . . . . . . . . . . . . . . 17
146145, 67syl6eq 2521 . . . . . . . . . . . . . . . 16
147137, 146eqtr3d 2507 . . . . . . . . . . . . . . 15
148 fnun 5692 . . . . . . . . . . . . . . 15
149135, 147, 148sylancr 676 . . . . . . . . . . . . . 14
150 imaundi 5254 . . . . . . . . . . . . . . . 16
151 imadif 5668 . . . . . . . . . . . . . . . . . 18
15257, 151syl 17 . . . . . . . . . . . . . . . . 17
153 fzsplit 11851 . . . . . . . . . . . . . . . . . . . . 21
15441, 153syl 17 . . . . . . . . . . . . . . . . . . . 20
155154difeq1d 3539 . . . . . . . . . . . . . . . . . . 19
156 difundir 3687 . . . . . . . . . . . . . . . . . . . 20
157 fzsplit2 11850 . . . . . . . . . . . . . . . . . . . . . . . . 25
15877, 85, 157syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . 24
15974oveq1d 6323 . . . . . . . . . . . . . . . . . . . . . . . . . 26
160 fzsn 11866 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
16188, 160syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26
162159, 161eqtrd 2505 . . . . . . . . . . . . . . . . . . . . . . . . 25
163162uneq2d 3579 . . . . . . . . . . . . . . . . . . . . . . . 24
164158, 163eqtrd 2505 . . . . . . . . . . . . . . . . . . . . . . 23
165164difeq1d 3539 . . . . . . . . . . . . . . . . . . . . . 22
166 difun2 3838 . . . . . . . . . . . . . . . . . . . . . . 23
167138, 62ltnled 9799 . . . . . . . . . . . . . . . . . . . . . . . . . 26
16863, 167mpbid 215 . . . . . . . . . . . . . . . . . . . . . . . . 25
169 elfzle2 11829 . . . . . . . . . . . . . . . . . . . . . . . . 25
170168, 169nsyl 125 . . . . . . . . . . . . . . . . . . . . . . . 24
171 difsn 4097 . . . . . . . . . . . . . . . . . . . . . . . 24
172170, 171syl 17 . . . . . . . . . . . . . . . . . . . . . . 23
173166, 172syl5eq 2517 . . . . . . . . . . . . . . . . . . . . . 22
174165, 173eqtrd 2505 . . . . . . . . . . . . . . . . . . . . 21
17562, 140ltnled 9799 . . . . . . . . . . . . . . . . . . . . . . . 24
176141, 175mpbid 215 . . . . . . . . . . . . . . . . . . . . . . 23
177 elfzle1 11828 . . . . . . . . . . . . . . . . . . . . . . 23
178176, 177nsyl 125 . . . . . . . . . . . . . . . . . . . . . 22
179 difsn 4097 . . . . . . . . . . . . . . . . . . . . . 22
180178, 179syl 17 . . . . . . . . . . . . . . . . . . . . 21
181174, 180uneq12d 3580 . . . . . . . . . . . . . . . . . . . 20
182156, 181syl5eq 2517 . . . . . . . . . . . . . . . . . . 19
183155, 182eqtrd 2505 . . . . . . . . . . . . . . . . . 18
184183imaeq2d 5174 . . . . . . . . . . . . . . . . 17
185122eqcomd 2477 . . . . . . . . . . . . . . . . . 18
186106, 185difeq12d 3541 . . . . . . . . . . . . . . . . 17
187152, 184, 1863eqtr3d 2513 . . . . . . . . . . . . . . . 16
188150, 187syl5eqr 2519 . . . . . . . . . . . . . . 15
189188fneq2d 5677 . . . . . . . . . . . . . 14
190149, 189mpbid 215 . . . . . . . . . . . . 13
191 eldifsn 4088 . . . . . . . . . . . . . . 15
192191biimpri 211 . . . . . . . . . . . . . 14
193192ancoms 460 . . . . . . . . . . . . 13
194 disjdif 3830 . . . . . . . . . . . . . 14
195 fnconstg 5784 . . . . . . . . . . . . . . . 16
19651, 195ax-mp 5 . . . . . . . . . . . . . . 15
197 fvun2 5952 . . . . . . . . . . . . . . 15
198196, 197mp3an1 1377 . . . . . . . . . . . . . 14
199194, 198mpanr1 697 . . . . . . . . . . . . 13
200190, 193, 199syl2an 485 . . . . . . . . . . . 12
201200anassrs 660 . . . . . . . . . . 11
202132, 201eqtrd 2505 . . . . . . . . . 10
20347, 110, 112, 112, 113, 114, 202ofval 6559 . . . . . . . . 9
204 fnconstg 5784 . . . . . . . . . . . . . . 15
20548, 204ax-mp 5 . . . . . . . . . . . . . 14
206205, 134pm3.2i 462 . . . . . . . . . . . . 13
207 imain 5669 . . . . . . . . . . . . . . 15
20857, 207syl 17 . . . . . . . . . . . . . 14
209 fzdisj 11852 . . . . . . . . . . . . . . . . 17
210141, 209syl 17 . . . . . . . . . . . . . . . 16
211210imaeq2d 5174 . . . . . . . . . . . . . . 15
212211, 67syl6eq 2521 . . . . . . . . . . . . . 14
213208, 212eqtr3d 2507 . . . . . . . . . . . . 13
214 fnun 5692 . . . . . . . . . . . . 13
215206, 213, 214sylancr 676 . . . . . . . . . . . 12
216154imaeq2d 5174 . . . . . . . . . . . . . . 15
217 imaundi 5254 . . . . . . . . . . . . . . 15
218216, 217syl6eq 2521 . . . . . . . . . . . . . 14
219218, 106eqtr3d 2507 . . . . . . . . . . . . 13
220219fneq2d 5677 . . . . . . . . . . . 12
221215, 220mpbid 215 . . . . . . . . . . 11
222221adantr 472 . . . . . . . . . 10
223 imaundi 5254 . . . . . . . . . . . . . . . . . 18
224164imaeq2d 5174 . . . . . . . . . . . . . . . . . 18
225122uneq2d 3579 . . . . . . . . . . . . . . . . . 18
226223, 224, 2253eqtr4a 2531 . . . . . . . . . . . . . . . . 17
227226xpeq1d 4862 . . . . . . . . . . . . . . . 16
228 xpundir 4893 . . . . . . . . . . . . . . . 16
229227, 228syl6eq 2521 . . . . . . . . . . . . . . 15
230229uneq1d 3578 . . . . . . . . . . . . . 14
231 un23 3584 . . . . . . . . . . . . . . 15
232231equncomi 3571 . . . . . . . . . . . . . 14
233230, 232syl6eq 2521 . . . . . . . . . . . . 13
234233fveq1d 5881 . . . . . . . . . . . 12
235234ad2antrr 740 . . . . . . . . . . 11
236 fnconstg 5784 . . . . . . . . . . . . . . . 16
23748, 236ax-mp 5 . . . . . . . . . . . . . . 15
238 fvun2 5952 . . . . . . . . . . . . . . 15
239237, 238mp3an1 1377 . . . . . . . . . . . . . 14
240194, 239mpanr1 697 . . . . . . . . . . . . 13
241190, 193, 240syl2an 485 . . . . . . . . . . . 12
242241anassrs 660 . . . . . . . . . . 11
243235, 242eqtrd 2505 . . . . . . . . . 10
24447, 222, 112, 112, 113, 114, 243ofval 6559 . . . . . . . . 9
245203, 244eqtr4d 2508 . . . . . . . 8
246245an32s 821 . . . . . . 7
247246anasss 659 . . . . . 6
248 fveq2 5879 . . . . . . . . . . . . . . . . . 18
249248breq2d 4407 . . . . . . . . . . . . . . . . 17
250249ifbid 3894 . . . . . . . . . . . . . . . 16
251250csbeq1d 3356 . . . . . . . . . . . . . . 15
252 fveq2 5879 . . . . . . . . . . . . . . . . . 18
253252fveq2d 5883 . . . . . . . . . . . . . . . . 17
254252fveq2d 5883 . . . . . . . . . . . . . . . . . . . 20
255254imaeq1d 5173 . . . . . . . . . . . . . . . . . . 19
256255xpeq1d 4862 . . . . . . . . . . . . . . . . . 18
257254imaeq1d 5173 . . . . . . . . . . . . . . . . . . 19
258257xpeq1d 4862 . . . . . . . . . . . . . . . . . 18
259256, 258uneq12d 3580 . . . . . . . . . . . . . . . . 17
260253, 259oveq12d 6326 . . . . . . . . . . . . . . . 16