Proof of Theorem poimirlem9
Step | Hyp | Ref
| Expression |
1 | | resundi 5410 |
. . . 4
|
2 | | poimir.0 |
. . . . . . . . . . . . 13
|
3 | 2 | nncnd 11036 |
. . . . . . . . . . . 12
|
4 | | npcan1 10455 |
. . . . . . . . . . . 12
|
5 | 3, 4 | syl 17 |
. . . . . . . . . . 11
|
6 | 2 | nnzd 11481 |
. . . . . . . . . . . 12
|
7 | | peano2zm 11420 |
. . . . . . . . . . . 12
|
8 | | uzid 11702 |
. . . . . . . . . . . 12
|
9 | | peano2uz 11741 |
. . . . . . . . . . . 12
|
10 | 6, 7, 8, 9 | 4syl 19 |
. . . . . . . . . . 11
|
11 | 5, 10 | eqeltrrd 2702 |
. . . . . . . . . 10
|
12 | | fzss2 12381 |
. . . . . . . . . 10
|
13 | 11, 12 | syl 17 |
. . . . . . . . 9
|
14 | | poimirlem9.2 |
. . . . . . . . 9
|
15 | 13, 14 | sseldd 3604 |
. . . . . . . 8
|
16 | | fzp1elp1 12394 |
. . . . . . . . . 10
|
17 | 14, 16 | syl 17 |
. . . . . . . . 9
|
18 | 5 | oveq2d 6666 |
. . . . . . . . 9
|
19 | 17, 18 | eleqtrd 2703 |
. . . . . . . 8
|
20 | 15, 19 | prssd 4354 |
. . . . . . 7
|
21 | | undif 4049 |
. . . . . . 7
|
22 | 20, 21 | sylib 208 |
. . . . . 6
|
23 | 22 | reseq2d 5396 |
. . . . 5
|
24 | | poimirlem9.3 |
. . . . . . . 8
|
25 | | elrabi 3359 |
. . . . . . . . 9
..^
..^ |
26 | | poimirlem22.s |
. . . . . . . . 9
..^ |
27 | 25, 26 | eleq2s 2719 |
. . . . . . . 8
..^ |
28 | | xp1st 7198 |
. . . . . . . 8
..^ ..^ |
29 | | xp2nd 7199 |
. . . . . . . 8
..^ |
30 | 24, 27, 28, 29 | 4syl 19 |
. . . . . . 7
|
31 | | fvex 6201 |
. . . . . . . 8
|
32 | | f1oeq1 6127 |
. . . . . . . 8
|
33 | 31, 32 | elab 3350 |
. . . . . . 7
|
34 | 30, 33 | sylib 208 |
. . . . . 6
|
35 | | f1ofn 6138 |
. . . . . 6
|
36 | | fnresdm 6000 |
. . . . . 6
|
37 | 34, 35, 36 | 3syl 18 |
. . . . 5
|
38 | 23, 37 | eqtrd 2656 |
. . . 4
|
39 | 1, 38 | syl5eqr 2670 |
. . 3
|
40 | | 2lt3 11195 |
. . . . . 6
|
41 | | 2re 11090 |
. . . . . . 7
|
42 | | 3re 11094 |
. . . . . . 7
|
43 | 41, 42 | ltnlei 10158 |
. . . . . 6
|
44 | 40, 43 | mpbi 220 |
. . . . 5
|
45 | | df-pr 4180 |
. . . . . . . . . . . 12
|
46 | 45 | coeq2i 5282 |
. . . . . . . . . . 11
|
47 | | coundi 5636 |
. . . . . . . . . . 11
|
48 | 46, 47 | eqtri 2644 |
. . . . . . . . . 10
|
49 | | poimirlem9.1 |
. . . . . . . . . . . . . . . . . . . 20
|
50 | | elrabi 3359 |
. . . . . . . . . . . . . . . . . . . . 21
..^
..^ |
51 | 50, 26 | eleq2s 2719 |
. . . . . . . . . . . . . . . . . . . 20
..^ |
52 | | xp1st 7198 |
. . . . . . . . . . . . . . . . . . . 20
..^ ..^ |
53 | | xp2nd 7199 |
. . . . . . . . . . . . . . . . . . . 20
..^ |
54 | 49, 51, 52, 53 | 4syl 19 |
. . . . . . . . . . . . . . . . . . 19
|
55 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . 20
|
56 | | f1oeq1 6127 |
. . . . . . . . . . . . . . . . . . . 20
|
57 | 55, 56 | elab 3350 |
. . . . . . . . . . . . . . . . . . 19
|
58 | 54, 57 | sylib 208 |
. . . . . . . . . . . . . . . . . 18
|
59 | | f1of1 6136 |
. . . . . . . . . . . . . . . . . 18
|
60 | 58, 59 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
61 | 19 | snssd 4340 |
. . . . . . . . . . . . . . . . 17
|
62 | | f1ores 6151 |
. . . . . . . . . . . . . . . . 17
|
63 | 60, 61, 62 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
64 | | f1of 6137 |
. . . . . . . . . . . . . . . 16
|
65 | 63, 64 | syl 17 |
. . . . . . . . . . . . . . 15
|
66 | | f1ofn 6138 |
. . . . . . . . . . . . . . . . . 18
|
67 | 58, 66 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
68 | | fnsnfv 6258 |
. . . . . . . . . . . . . . . . 17
|
69 | 67, 19, 68 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
70 | 69 | feq3d 6032 |
. . . . . . . . . . . . . . 15
|
71 | 65, 70 | mpbird 247 |
. . . . . . . . . . . . . 14
|
72 | | eqid 2622 |
. . . . . . . . . . . . . . 15
|
73 | | fvex 6201 |
. . . . . . . . . . . . . . . 16
|
74 | | ovex 6678 |
. . . . . . . . . . . . . . . 16
|
75 | 73, 74 | fsn 6402 |
. . . . . . . . . . . . . . 15
|
76 | 72, 75 | mpbir 221 |
. . . . . . . . . . . . . 14
|
77 | | fco2 6059 |
. . . . . . . . . . . . . 14
|
78 | 71, 76, 77 | sylancl 694 |
. . . . . . . . . . . . 13
|
79 | | fvex 6201 |
. . . . . . . . . . . . . 14
|
80 | 79 | fconst2 6470 |
. . . . . . . . . . . . 13
|
81 | 78, 80 | sylib 208 |
. . . . . . . . . . . 12
|
82 | 73, 79 | xpsn 6407 |
. . . . . . . . . . . 12
|
83 | 81, 82 | syl6eq 2672 |
. . . . . . . . . . 11
|
84 | 83 | uneq1d 3766 |
. . . . . . . . . 10
|
85 | 48, 84 | syl5eq 2668 |
. . . . . . . . 9
|
86 | | elfznn 12370 |
. . . . . . . . . . . . . . . . 17
|
87 | 14, 86 | syl 17 |
. . . . . . . . . . . . . . . 16
|
88 | 87 | nnred 11035 |
. . . . . . . . . . . . . . 15
|
89 | 88 | ltp1d 10954 |
. . . . . . . . . . . . . . 15
|
90 | 88, 89 | ltned 10173 |
. . . . . . . . . . . . . 14
|
91 | 90 | necomd 2849 |
. . . . . . . . . . . . 13
|
92 | | f1veqaeq 6514 |
. . . . . . . . . . . . . . 15
|
93 | 60, 19, 15, 92 | syl12anc 1324 |
. . . . . . . . . . . . . 14
|
94 | 93 | necon3d 2815 |
. . . . . . . . . . . . 13
|
95 | 91, 94 | mpd 15 |
. . . . . . . . . . . 12
|
96 | 95 | neneqd 2799 |
. . . . . . . . . . 11
|
97 | 73, 79 | opth 4945 |
. . . . . . . . . . . 12
|
98 | 97 | simprbi 480 |
. . . . . . . . . . 11
|
99 | 96, 98 | nsyl 135 |
. . . . . . . . . 10
|
100 | 90 | neneqd 2799 |
. . . . . . . . . . 11
|
101 | 73, 79 | opth1 4944 |
. . . . . . . . . . 11
|
102 | 100, 101 | nsyl 135 |
. . . . . . . . . 10
|
103 | | opex 4932 |
. . . . . . . . . . . . . . 15
|
104 | 103 | snid 4208 |
. . . . . . . . . . . . . 14
|
105 | | elun1 3780 |
. . . . . . . . . . . . . 14
|
106 | 104, 105 | ax-mp 5 |
. . . . . . . . . . . . 13
|
107 | | eleq2 2690 |
. . . . . . . . . . . . 13
|
108 | 106, 107 | mpbii 223 |
. . . . . . . . . . . 12
|
109 | 103 | elpr 4198 |
. . . . . . . . . . . . 13
|
110 | | oran 517 |
. . . . . . . . . . . . 13
|
111 | 109, 110 | bitri 264 |
. . . . . . . . . . . 12
|
112 | 108, 111 | sylib 208 |
. . . . . . . . . . 11
|
113 | 112 | necon2ai 2823 |
. . . . . . . . . 10
|
114 | 99, 102, 113 | syl2anc 693 |
. . . . . . . . 9
|
115 | 85, 114 | eqnetrd 2861 |
. . . . . . . 8
|
116 | | fnressn 6425 |
. . . . . . . . . . . 12
|
117 | 67, 15, 116 | syl2anc 693 |
. . . . . . . . . . 11
|
118 | | fnressn 6425 |
. . . . . . . . . . . 12
|
119 | 67, 19, 118 | syl2anc 693 |
. . . . . . . . . . 11
|
120 | 117, 119 | uneq12d 3768 |
. . . . . . . . . 10
|
121 | | df-pr 4180 |
. . . . . . . . . . . 12
|
122 | 121 | reseq2i 5393 |
. . . . . . . . . . 11
|
123 | | resundi 5410 |
. . . . . . . . . . 11
|
124 | 122, 123 | eqtri 2644 |
. . . . . . . . . 10
|
125 | | df-pr 4180 |
. . . . . . . . . 10
|
126 | 120, 124,
125 | 3eqtr4g 2681 |
. . . . . . . . 9
|
127 | | poimirlem9.4 |
. . . . . . . . . . 11
|
128 | 2, 26, 49, 14, 24 | poimirlem8 33417 |
. . . . . . . . . . . . 13
|
129 | | uneq12 3762 |
. . . . . . . . . . . . . 14
|
130 | | resundi 5410 |
. . . . . . . . . . . . . . . 16
|
131 | 22 | reseq2d 5396 |
. . . . . . . . . . . . . . . . 17
|
132 | | fnresdm 6000 |
. . . . . . . . . . . . . . . . . 18
|
133 | 58, 66, 132 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
|
134 | 131, 133 | eqtrd 2656 |
. . . . . . . . . . . . . . . 16
|
135 | 130, 134 | syl5eqr 2670 |
. . . . . . . . . . . . . . 15
|
136 | 39, 135 | eqeq12d 2637 |
. . . . . . . . . . . . . 14
|
137 | 129, 136 | syl5ib 234 |
. . . . . . . . . . . . 13
|
138 | 128, 137 | mpan2d 710 |
. . . . . . . . . . . 12
|
139 | 138 | necon3d 2815 |
. . . . . . . . . . 11
|
140 | 127, 139 | mpd 15 |
. . . . . . . . . 10
|
141 | 140 | necomd 2849 |
. . . . . . . . 9
|
142 | 126, 141 | eqnetrrd 2862 |
. . . . . . . 8
|
143 | | prex 4909 |
. . . . . . . . . . . 12
|
144 | 55, 143 | coex 7118 |
. . . . . . . . . . 11
|
145 | | prex 4909 |
. . . . . . . . . . 11
|
146 | 31 | resex 5443 |
. . . . . . . . . . 11
|
147 | | hashtpg 13267 |
. . . . . . . . . . 11
|
148 | 144, 145,
146, 147 | mp3an 1424 |
. . . . . . . . . 10
|
149 | 148 | biimpi 206 |
. . . . . . . . 9
|
150 | 149 | 3expia 1267 |
. . . . . . . 8
|
151 | 115, 142,
150 | syl2anc 693 |
. . . . . . 7
|
152 | | prex 4909 |
. . . . . . . . . . . . 13
|
153 | | prex 4909 |
. . . . . . . . . . . . 13
|
154 | 152, 153 | mapval 7869 |
. . . . . . . . . . . 12
|
155 | | prfi 8235 |
. . . . . . . . . . . . 13
|
156 | | prfi 8235 |
. . . . . . . . . . . . 13
|
157 | | mapfi 8262 |
. . . . . . . . . . . . 13
|
158 | 155, 156,
157 | mp2an 708 |
. . . . . . . . . . . 12
|
159 | 154, 158 | eqeltrri 2698 |
. . . . . . . . . . 11
|
160 | | f1of 6137 |
. . . . . . . . . . . 12
|
161 | 160 | ss2abi 3674 |
. . . . . . . . . . 11
|
162 | | ssfi 8180 |
. . . . . . . . . . 11
|
163 | 159, 161,
162 | mp2an 708 |
. . . . . . . . . 10
|
164 | 19, 15 | prssd 4354 |
. . . . . . . . . . . . . . 15
|
165 | | f1ores 6151 |
. . . . . . . . . . . . . . 15
|
166 | 60, 164, 165 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
167 | | fnimapr 6262 |
. . . . . . . . . . . . . . . 16
|
168 | 67, 19, 15, 167 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
|
169 | 168 | f1oeq3d 6134 |
. . . . . . . . . . . . . 14
|
170 | 166, 169 | mpbid 222 |
. . . . . . . . . . . . 13
|
171 | | f1oprg 6181 |
. . . . . . . . . . . . . . 15
|
172 | 73, 74, 74, 73, 171 | mp4an 709 |
. . . . . . . . . . . . . 14
|
173 | 90, 91, 172 | syl2anc 693 |
. . . . . . . . . . . . 13
|
174 | | f1oco 6159 |
. . . . . . . . . . . . 13
|
175 | 170, 173,
174 | syl2anc 693 |
. . . . . . . . . . . 12
|
176 | | rnpropg 5615 |
. . . . . . . . . . . . . . 15
|
177 | 73, 74, 176 | mp2an 708 |
. . . . . . . . . . . . . 14
|
178 | 177 | eqimssi 3659 |
. . . . . . . . . . . . 13
|
179 | | cores 5638 |
. . . . . . . . . . . . 13
|
180 | | f1oeq1 6127 |
. . . . . . . . . . . . 13
|
181 | 178, 179,
180 | mp2b 10 |
. . . . . . . . . . . 12
|
182 | 175, 181 | sylib 208 |
. . . . . . . . . . 11
|
183 | 95 | necomd 2849 |
. . . . . . . . . . . . 13
|
184 | | fvex 6201 |
. . . . . . . . . . . . . 14
|
185 | | f1oprg 6181 |
. . . . . . . . . . . . . 14
|
186 | 73, 184, 74, 79, 185 | mp4an 709 |
. . . . . . . . . . . . 13
|
187 | 90, 183, 186 | syl2anc 693 |
. . . . . . . . . . . 12
|
188 | | prcom 4267 |
. . . . . . . . . . . . 13
|
189 | | f1oeq3 6129 |
. . . . . . . . . . . . 13
|
190 | 188, 189 | ax-mp 5 |
. . . . . . . . . . . 12
|
191 | 187, 190 | sylib 208 |
. . . . . . . . . . 11
|
192 | | f1of1 6136 |
. . . . . . . . . . . . . 14
|
193 | 34, 192 | syl 17 |
. . . . . . . . . . . . 13
|
194 | | f1ores 6151 |
. . . . . . . . . . . . 13
|
195 | 193, 20, 194 | syl2anc 693 |
. . . . . . . . . . . 12
|
196 | | dff1o3 6143 |
. . . . . . . . . . . . . . . . 17
|
197 | 196 | simprbi 480 |
. . . . . . . . . . . . . . . 16
|
198 | | imadif 5973 |
. . . . . . . . . . . . . . . 16
|
199 | 34, 197, 198 | 3syl 18 |
. . . . . . . . . . . . . . 15
|
200 | | f1ofo 6144 |
. . . . . . . . . . . . . . . . . 18
|
201 | | foima 6120 |
. . . . . . . . . . . . . . . . . 18
|
202 | 34, 200, 201 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
|
203 | | f1ofo 6144 |
. . . . . . . . . . . . . . . . . 18
|
204 | | foima 6120 |
. . . . . . . . . . . . . . . . . 18
|
205 | 58, 203, 204 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
|
206 | 202, 205 | eqtr4d 2659 |
. . . . . . . . . . . . . . . 16
|
207 | 128 | rneqd 5353 |
. . . . . . . . . . . . . . . . 17
|
208 | | df-ima 5127 |
. . . . . . . . . . . . . . . . 17
|
209 | | df-ima 5127 |
. . . . . . . . . . . . . . . . 17
|
210 | 207, 208,
209 | 3eqtr4g 2681 |
. . . . . . . . . . . . . . . 16
|
211 | 206, 210 | difeq12d 3729 |
. . . . . . . . . . . . . . 15
|
212 | | dff1o3 6143 |
. . . . . . . . . . . . . . . . . 18
|
213 | 212 | simprbi 480 |
. . . . . . . . . . . . . . . . 17
|
214 | | imadif 5973 |
. . . . . . . . . . . . . . . . 17
|
215 | 58, 213, 214 | 3syl 18 |
. . . . . . . . . . . . . . . 16
|
216 | | dfin4 3867 |
. . . . . . . . . . . . . . . . . 18
|
217 | | sseqin2 3817 |
. . . . . . . . . . . . . . . . . . 19
|
218 | 20, 217 | sylib 208 |
. . . . . . . . . . . . . . . . . 18
|
219 | 216, 218 | syl5eqr 2670 |
. . . . . . . . . . . . . . . . 17
|
220 | 219 | imaeq2d 5466 |
. . . . . . . . . . . . . . . 16
|
221 | 215, 220 | eqtr3d 2658 |
. . . . . . . . . . . . . . 15
|
222 | 199, 211,
221 | 3eqtrd 2660 |
. . . . . . . . . . . . . 14
|
223 | 219 | imaeq2d 5466 |
. . . . . . . . . . . . . 14
|
224 | | fnimapr 6262 |
. . . . . . . . . . . . . . . 16
|
225 | 67, 15, 19, 224 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
|
226 | 225, 188 | syl6eq 2672 |
. . . . . . . . . . . . . 14
|
227 | 222, 223,
226 | 3eqtr3d 2664 |
. . . . . . . . . . . . 13
|
228 | 227 | f1oeq3d 6134 |
. . . . . . . . . . . 12
|
229 | 195, 228 | mpbid 222 |
. . . . . . . . . . 11
|
230 | | ssabral 3673 |
. . . . . . . . . . . 12
|
231 | | f1oeq1 6127 |
. . . . . . . . . . . . 13
|
232 | | f1oeq1 6127 |
. . . . . . . . . . . . 13
|
233 | | f1oeq1 6127 |
. . . . . . . . . . . . 13
|
234 | 144, 145,
146, 231, 232, 233 | raltp 4240 |
. . . . . . . . . . . 12
|
235 | 230, 234 | bitri 264 |
. . . . . . . . . . 11
|
236 | 182, 191,
229, 235 | syl3anbrc 1246 |
. . . . . . . . . 10
|
237 | | hashss 13197 |
. . . . . . . . . 10
|
238 | 163, 236,
237 | sylancr 695 |
. . . . . . . . 9
|
239 | 153 | enref 7988 |
. . . . . . . . . . . 12
|
240 | | hashprg 13182 |
. . . . . . . . . . . . . . . 16
|
241 | 79, 184, 240 | mp2an 708 |
. . . . . . . . . . . . . . 15
|
242 | 95, 241 | sylib 208 |
. . . . . . . . . . . . . 14
|
243 | | hashprg 13182 |
. . . . . . . . . . . . . . . 16
|
244 | 73, 74, 243 | mp2an 708 |
. . . . . . . . . . . . . . 15
|
245 | 90, 244 | sylib 208 |
. . . . . . . . . . . . . 14
|
246 | 242, 245 | eqtr4d 2659 |
. . . . . . . . . . . . 13
|
247 | | hashen 13135 |
. . . . . . . . . . . . . 14
|
248 | 155, 156,
247 | mp2an 708 |
. . . . . . . . . . . . 13
|
249 | 246, 248 | sylib 208 |
. . . . . . . . . . . 12
|
250 | | hashfacen 13238 |
. . . . . . . . . . . 12
|
251 | 239, 249,
250 | sylancr 695 |
. . . . . . . . . . 11
|
252 | 153, 153 | mapval 7869 |
. . . . . . . . . . . . . 14
|
253 | | mapfi 8262 |
. . . . . . . . . . . . . . 15
|
254 | 156, 156,
253 | mp2an 708 |
. . . . . . . . . . . . . 14
|
255 | 252, 254 | eqeltrri 2698 |
. . . . . . . . . . . . 13
|
256 | | f1of 6137 |
. . . . . . . . . . . . . 14
|
257 | 256 | ss2abi 3674 |
. . . . . . . . . . . . 13
|
258 | | ssfi 8180 |
. . . . . . . . . . . . 13
|
259 | 255, 257,
258 | mp2an 708 |
. . . . . . . . . . . 12
|
260 | | hashen 13135 |
. . . . . . . . . . . 12
|
261 | 163, 259,
260 | mp2an 708 |
. . . . . . . . . . 11
|
262 | 251, 261 | sylibr 224 |
. . . . . . . . . 10
|
263 | | hashfac 13242 |
. . . . . . . . . . . 12
|
264 | 156, 263 | ax-mp 5 |
. . . . . . . . . . 11
|
265 | 245 | fveq2d 6195 |
. . . . . . . . . . . 12
|
266 | | fac2 13066 |
. . . . . . . . . . . 12
|
267 | 265, 266 | syl6eq 2672 |
. . . . . . . . . . 11
|
268 | 264, 267 | syl5eq 2668 |
. . . . . . . . . 10
|
269 | 262, 268 | eqtrd 2656 |
. . . . . . . . 9
|
270 | 238, 269 | breqtrd 4679 |
. . . . . . . 8
|
271 | | breq1 4656 |
. . . . . . . 8
|
272 | 270, 271 | syl5ibcom 235 |
. . . . . . 7
|
273 | 151, 272 | syld 47 |
. . . . . 6
|
274 | 273 | necon1bd 2812 |
. . . . 5
|
275 | 44, 274 | mpi 20 |
. . . 4
|
276 | | coires1 5653 |
. . . . 5
|
277 | 128, 276 | syl6eqr 2674 |
. . . 4
|
278 | 275, 277 | uneq12d 3768 |
. . 3
|
279 | 39, 278 | eqtr3d 2658 |
. 2
|
280 | | coundi 5636 |
. 2
|
281 | 279, 280 | syl6eqr 2674 |
1
|