Step | Hyp | Ref
| Expression |
1 | | poimirlem9.3 |
. . . . . . . 8
|
2 | | elrabi 3359 |
. . . . . . . . 9
..^
..^ |
3 | | poimirlem22.s |
. . . . . . . . 9
..^ |
4 | 2, 3 | eleq2s 2719 |
. . . . . . . 8
..^ |
5 | 1, 4 | syl 17 |
. . . . . . 7
..^ |
6 | | xp1st 7198 |
. . . . . . 7
..^ ..^ |
7 | 5, 6 | syl 17 |
. . . . . 6
..^ |
8 | | xp2nd 7199 |
. . . . . 6
..^ |
9 | 7, 8 | syl 17 |
. . . . 5
|
10 | | fvex 6201 |
. . . . . 6
|
11 | | f1oeq1 6127 |
. . . . . 6
|
12 | 10, 11 | elab 3350 |
. . . . 5
|
13 | 9, 12 | sylib 208 |
. . . 4
|
14 | | f1ofn 6138 |
. . . 4
|
15 | 13, 14 | syl 17 |
. . 3
|
16 | | difss 3737 |
. . 3
|
17 | | fnssres 6004 |
. . 3
|
18 | 15, 16, 17 | sylancl 694 |
. 2
|
19 | | poimirlem9.1 |
. . . . . . . 8
|
20 | | elrabi 3359 |
. . . . . . . . 9
..^
..^ |
21 | 20, 3 | eleq2s 2719 |
. . . . . . . 8
..^ |
22 | 19, 21 | syl 17 |
. . . . . . 7
..^ |
23 | | xp1st 7198 |
. . . . . . 7
..^ ..^ |
24 | 22, 23 | syl 17 |
. . . . . 6
..^ |
25 | | xp2nd 7199 |
. . . . . 6
..^ |
26 | 24, 25 | syl 17 |
. . . . 5
|
27 | | fvex 6201 |
. . . . . 6
|
28 | | f1oeq1 6127 |
. . . . . 6
|
29 | 27, 28 | elab 3350 |
. . . . 5
|
30 | 26, 29 | sylib 208 |
. . . 4
|
31 | | f1ofn 6138 |
. . . 4
|
32 | 30, 31 | syl 17 |
. . 3
|
33 | | fnssres 6004 |
. . 3
|
34 | 32, 16, 33 | sylancl 694 |
. 2
|
35 | | poimirlem9.2 |
. . . . . . . . . . . 12
|
36 | | fzp1elp1 12394 |
. . . . . . . . . . . 12
|
37 | 35, 36 | syl 17 |
. . . . . . . . . . 11
|
38 | | poimir.0 |
. . . . . . . . . . . . . 14
|
39 | 38 | nncnd 11036 |
. . . . . . . . . . . . 13
|
40 | | npcan1 10455 |
. . . . . . . . . . . . 13
|
41 | 39, 40 | syl 17 |
. . . . . . . . . . . 12
|
42 | 41 | oveq2d 6666 |
. . . . . . . . . . 11
|
43 | 37, 42 | eleqtrd 2703 |
. . . . . . . . . 10
|
44 | | fzsplit 12367 |
. . . . . . . . . 10
|
45 | 43, 44 | syl 17 |
. . . . . . . . 9
|
46 | 45 | difeq1d 3727 |
. . . . . . . 8
|
47 | | difundir 3880 |
. . . . . . . . 9
|
48 | | elfznn 12370 |
. . . . . . . . . . . . . . . . . 18
|
49 | 35, 48 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
50 | 49 | nncnd 11036 |
. . . . . . . . . . . . . . . 16
|
51 | | npcan1 10455 |
. . . . . . . . . . . . . . . 16
|
52 | 50, 51 | syl 17 |
. . . . . . . . . . . . . . 15
|
53 | | nnuz 11723 |
. . . . . . . . . . . . . . . 16
|
54 | 49, 53 | syl6eleq 2711 |
. . . . . . . . . . . . . . 15
|
55 | 52, 54 | eqeltrd 2701 |
. . . . . . . . . . . . . 14
|
56 | 49 | nnzd 11481 |
. . . . . . . . . . . . . . . . . 18
|
57 | | peano2zm 11420 |
. . . . . . . . . . . . . . . . . 18
|
58 | 56, 57 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
59 | | uzid 11702 |
. . . . . . . . . . . . . . . . 17
|
60 | | peano2uz 11741 |
. . . . . . . . . . . . . . . . 17
|
61 | 58, 59, 60 | 3syl 18 |
. . . . . . . . . . . . . . . 16
|
62 | 52, 61 | eqeltrrd 2702 |
. . . . . . . . . . . . . . 15
|
63 | | peano2uz 11741 |
. . . . . . . . . . . . . . 15
|
64 | 62, 63 | syl 17 |
. . . . . . . . . . . . . 14
|
65 | | fzsplit2 12366 |
. . . . . . . . . . . . . 14
|
66 | 55, 64, 65 | syl2anc 693 |
. . . . . . . . . . . . 13
|
67 | 52 | oveq1d 6665 |
. . . . . . . . . . . . . . 15
|
68 | | fzpr 12396 |
. . . . . . . . . . . . . . . 16
|
69 | 56, 68 | syl 17 |
. . . . . . . . . . . . . . 15
|
70 | 67, 69 | eqtrd 2656 |
. . . . . . . . . . . . . 14
|
71 | 70 | uneq2d 3767 |
. . . . . . . . . . . . 13
|
72 | 66, 71 | eqtrd 2656 |
. . . . . . . . . . . 12
|
73 | 72 | difeq1d 3727 |
. . . . . . . . . . 11
|
74 | 49 | nnred 11035 |
. . . . . . . . . . . . . . . . 17
|
75 | 74 | ltm1d 10956 |
. . . . . . . . . . . . . . . 16
|
76 | 58 | zred 11482 |
. . . . . . . . . . . . . . . . 17
|
77 | 76, 74 | ltnled 10184 |
. . . . . . . . . . . . . . . 16
|
78 | 75, 77 | mpbid 222 |
. . . . . . . . . . . . . . 15
|
79 | | elfzle2 12345 |
. . . . . . . . . . . . . . 15
|
80 | 78, 79 | nsyl 135 |
. . . . . . . . . . . . . 14
|
81 | | difsn 4328 |
. . . . . . . . . . . . . 14
|
82 | 80, 81 | syl 17 |
. . . . . . . . . . . . 13
|
83 | | peano2re 10209 |
. . . . . . . . . . . . . . . . . 18
|
84 | 74, 83 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
85 | 74 | ltp1d 10954 |
. . . . . . . . . . . . . . . . 17
|
86 | 76, 74, 84, 75, 85 | lttrd 10198 |
. . . . . . . . . . . . . . . 16
|
87 | 76, 84 | ltnled 10184 |
. . . . . . . . . . . . . . . 16
|
88 | 86, 87 | mpbid 222 |
. . . . . . . . . . . . . . 15
|
89 | | elfzle2 12345 |
. . . . . . . . . . . . . . 15
|
90 | 88, 89 | nsyl 135 |
. . . . . . . . . . . . . 14
|
91 | | difsn 4328 |
. . . . . . . . . . . . . 14
|
92 | 90, 91 | syl 17 |
. . . . . . . . . . . . 13
|
93 | 82, 92 | ineq12d 3815 |
. . . . . . . . . . . 12
|
94 | | difun2 4048 |
. . . . . . . . . . . . 13
|
95 | | df-pr 4180 |
. . . . . . . . . . . . . 14
|
96 | 95 | difeq2i 3725 |
. . . . . . . . . . . . 13
|
97 | | difundi 3879 |
. . . . . . . . . . . . 13
|
98 | 94, 96, 97 | 3eqtrri 2649 |
. . . . . . . . . . . 12
|
99 | | inidm 3822 |
. . . . . . . . . . . 12
|
100 | 93, 98, 99 | 3eqtr3g 2679 |
. . . . . . . . . . 11
|
101 | 73, 100 | eqtrd 2656 |
. . . . . . . . . 10
|
102 | | peano2re 10209 |
. . . . . . . . . . . . . . . . 17
|
103 | 84, 102 | syl 17 |
. . . . . . . . . . . . . . . 16
|
104 | 84 | ltp1d 10954 |
. . . . . . . . . . . . . . . 16
|
105 | 74, 84, 103, 85, 104 | lttrd 10198 |
. . . . . . . . . . . . . . 15
|
106 | 74, 103 | ltnled 10184 |
. . . . . . . . . . . . . . 15
|
107 | 105, 106 | mpbid 222 |
. . . . . . . . . . . . . 14
|
108 | | elfzle1 12344 |
. . . . . . . . . . . . . 14
|
109 | 107, 108 | nsyl 135 |
. . . . . . . . . . . . 13
|
110 | | difsn 4328 |
. . . . . . . . . . . . 13
|
111 | 109, 110 | syl 17 |
. . . . . . . . . . . 12
|
112 | 84, 103 | ltnled 10184 |
. . . . . . . . . . . . . . 15
|
113 | 104, 112 | mpbid 222 |
. . . . . . . . . . . . . 14
|
114 | | elfzle1 12344 |
. . . . . . . . . . . . . 14
|
115 | 113, 114 | nsyl 135 |
. . . . . . . . . . . . 13
|
116 | | difsn 4328 |
. . . . . . . . . . . . 13
|
117 | 115, 116 | syl 17 |
. . . . . . . . . . . 12
|
118 | 111, 117 | ineq12d 3815 |
. . . . . . . . . . 11
|
119 | 95 | difeq2i 3725 |
. . . . . . . . . . . 12
|
120 | | difundi 3879 |
. . . . . . . . . . . 12
|
121 | 119, 120 | eqtr2i 2645 |
. . . . . . . . . . 11
|
122 | | inidm 3822 |
. . . . . . . . . . 11
|
123 | 118, 121,
122 | 3eqtr3g 2679 |
. . . . . . . . . 10
|
124 | 101, 123 | uneq12d 3768 |
. . . . . . . . 9
|
125 | 47, 124 | syl5eq 2668 |
. . . . . . . 8
|
126 | 46, 125 | eqtrd 2656 |
. . . . . . 7
|
127 | 126 | eleq2d 2687 |
. . . . . 6
|
128 | | elun 3753 |
. . . . . 6
|
129 | 127, 128 | syl6bb 276 |
. . . . 5
|
130 | 129 | biimpa 501 |
. . . 4
|
131 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . 22
|
132 | 131 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . . 21
|
133 | 132 | ifbid 4108 |
. . . . . . . . . . . . . . . . . . . 20
|
134 | 133 | csbeq1d 3540 |
. . . . . . . . . . . . . . . . . . 19
|
135 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . 22
|
136 | 135 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . 21
|
137 | 135 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
138 | 137 | imaeq1d 5465 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
139 | 138 | xpeq1d 5138 |
. . . . . . . . . . . . . . . . . . . . . 22
|
140 | 137 | imaeq1d 5465 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
141 | 140 | xpeq1d 5138 |
. . . . . . . . . . . . . . . . . . . . . 22
|
142 | 139, 141 | uneq12d 3768 |
. . . . . . . . . . . . . . . . . . . . 21
|
143 | 136, 142 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . 20
|
144 | 143 | csbeq2dv 3992 |
. . . . . . . . . . . . . . . . . . 19
|
145 | 134, 144 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . 18
|
146 | 145 | mpteq2dv 4745 |
. . . . . . . . . . . . . . . . 17
|
147 | 146 | eqeq2d 2632 |
. . . . . . . . . . . . . . . 16
|
148 | 147, 3 | elrab2 3366 |
. . . . . . . . . . . . . . 15
..^
|
149 | 148 | simprbi 480 |
. . . . . . . . . . . . . 14
|
150 | 19, 149 | syl 17 |
. . . . . . . . . . . . 13
|
151 | | xp1st 7198 |
. . . . . . . . . . . . . . . 16
..^ ..^ |
152 | 24, 151 | syl 17 |
. . . . . . . . . . . . . . 15
..^ |
153 | | elmapi 7879 |
. . . . . . . . . . . . . . 15
..^ ..^ |
154 | 152, 153 | syl 17 |
. . . . . . . . . . . . . 14
..^ |
155 | | elfzoelz 12470 |
. . . . . . . . . . . . . . 15
..^
|
156 | 155 | ssriv 3607 |
. . . . . . . . . . . . . 14
..^ |
157 | | fss 6056 |
. . . . . . . . . . . . . 14
..^ ..^
|
158 | 154, 156,
157 | sylancl 694 |
. . . . . . . . . . . . 13
|
159 | 38, 150, 158, 30, 35 | poimirlem1 33410 |
. . . . . . . . . . . 12
|
160 | 38 | adantr 481 |
. . . . . . . . . . . . . . 15
|
161 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
162 | 161 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
163 | 162 | ifbid 4108 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
164 | 163 | csbeq1d 3540 |
. . . . . . . . . . . . . . . . . . . . . 22
|
165 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
166 | 165 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
167 | 165 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
168 | 167 | imaeq1d 5465 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
169 | 168 | xpeq1d 5138 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
170 | 167 | imaeq1d 5465 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
171 | 170 | xpeq1d 5138 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
172 | 169, 171 | uneq12d 3768 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
173 | 166, 172 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
174 | 173 | csbeq2dv 3992 |
. . . . . . . . . . . . . . . . . . . . . 22
|
175 | 164, 174 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . 21
|
176 | 175 | mpteq2dv 4745 |
. . . . . . . . . . . . . . . . . . . 20
|
177 | 176 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . 19
|
178 | 177, 3 | elrab2 3366 |
. . . . . . . . . . . . . . . . . 18
..^
|
179 | 178 | simprbi 480 |
. . . . . . . . . . . . . . . . 17
|
180 | 1, 179 | syl 17 |
. . . . . . . . . . . . . . . 16
|
181 | 180 | adantr 481 |
. . . . . . . . . . . . . . 15
|
182 | | xp1st 7198 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^ |
183 | 7, 182 | syl 17 |
. . . . . . . . . . . . . . . . . 18
..^ |
184 | | elmapi 7879 |
. . . . . . . . . . . . . . . . . 18
..^ ..^ |
185 | 183, 184 | syl 17 |
. . . . . . . . . . . . . . . . 17
..^ |
186 | | fss 6056 |
. . . . . . . . . . . . . . . . 17
..^ ..^
|
187 | 185, 156,
186 | sylancl 694 |
. . . . . . . . . . . . . . . 16
|
188 | 187 | adantr 481 |
. . . . . . . . . . . . . . 15
|
189 | 13 | adantr 481 |
. . . . . . . . . . . . . . 15
|
190 | 35 | adantr 481 |
. . . . . . . . . . . . . . 15
|
191 | | xp2nd 7199 |
. . . . . . . . . . . . . . . . 17
..^ |
192 | 5, 191 | syl 17 |
. . . . . . . . . . . . . . . 16
|
193 | | eldifsn 4317 |
. . . . . . . . . . . . . . . . 17
|
194 | 193 | biimpri 218 |
. . . . . . . . . . . . . . . 16
|
195 | 192, 194 | sylan 488 |
. . . . . . . . . . . . . . 15
|
196 | 160, 181,
188, 189, 190, 195 | poimirlem2 33411 |
. . . . . . . . . . . . . 14
|
197 | 196 | ex 450 |
. . . . . . . . . . . . 13
|
198 | 197 | necon1bd 2812 |
. . . . . . . . . . . 12
|
199 | 159, 198 | mpd 15 |
. . . . . . . . . . 11
|
200 | 199 | oveq1d 6665 |
. . . . . . . . . 10
|
201 | 200 | oveq2d 6666 |
. . . . . . . . 9
|
202 | 201 | eleq2d 2687 |
. . . . . . . 8
|
203 | 202 | biimpar 502 |
. . . . . . 7
|
204 | 38 | adantr 481 |
. . . . . . . 8
|
205 | 1 | adantr 481 |
. . . . . . . 8
|
206 | 199, 35 | eqeltrd 2701 |
. . . . . . . . 9
|
207 | 206 | adantr 481 |
. . . . . . . 8
|
208 | | simpr 477 |
. . . . . . . 8
|
209 | 204, 3, 205, 207, 208 | poimirlem6 33415 |
. . . . . . 7
|
210 | 203, 209 | syldan 487 |
. . . . . 6
|
211 | 38 | adantr 481 |
. . . . . . 7
|
212 | 19 | adantr 481 |
. . . . . . 7
|
213 | 35 | adantr 481 |
. . . . . . 7
|
214 | | simpr 477 |
. . . . . . 7
|
215 | 211, 3, 212, 213, 214 | poimirlem6 33415 |
. . . . . 6
|
216 | 210, 215 | eqtr3d 2658 |
. . . . 5
|
217 | 199 | oveq1d 6665 |
. . . . . . . . . . 11
|
218 | 217 | oveq1d 6665 |
. . . . . . . . . 10
|
219 | 218 | oveq1d 6665 |
. . . . . . . . 9
|
220 | 219 | eleq2d 2687 |
. . . . . . . 8
|
221 | 220 | biimpar 502 |
. . . . . . 7
|
222 | 38 | adantr 481 |
. . . . . . . 8
|
223 | 1 | adantr 481 |
. . . . . . . 8
|
224 | 206 | adantr 481 |
. . . . . . . 8
|
225 | | simpr 477 |
. . . . . . . 8
|
226 | 222, 3, 223, 224, 225 | poimirlem7 33416 |
. . . . . . 7
|
227 | 221, 226 | syldan 487 |
. . . . . 6
|
228 | 38 | adantr 481 |
. . . . . . 7
|
229 | 19 | adantr 481 |
. . . . . . 7
|
230 | 35 | adantr 481 |
. . . . . . 7
|
231 | | simpr 477 |
. . . . . . 7
|
232 | 228, 3, 229, 230, 231 | poimirlem7 33416 |
. . . . . 6
|
233 | 227, 232 | eqtr3d 2658 |
. . . . 5
|
234 | 216, 233 | jaodan 826 |
. . . 4
|
235 | 130, 234 | syldan 487 |
. . 3
|
236 | | fvres 6207 |
. . . 4
|
237 | 236 | adantl 482 |
. . 3
|
238 | | fvres 6207 |
. . . 4
|
239 | 238 | adantl 482 |
. . 3
|
240 | 235, 237,
239 | 3eqtr4d 2666 |
. 2
|
241 | 18, 34, 240 | eqfnfvd 6314 |
1
|