Step |
Hyp |
Ref |
Expression |
1 |
|
itg2gt0cn.2 |
|
2 |
|
itg2gt0cn.3 |
|
3 |
|
itg2gt0cn.5 |
|
4 |
|
itg2gt0cn.cn |
|
5 |
|
0xr |
|
6 |
|
imassrn |
|
7 |
2
|
frnd |
|
8 |
|
icossxr |
|
9 |
7 8
|
sstrdi |
|
10 |
6 9
|
sstrid |
|
11 |
|
supxrcl |
|
12 |
10 11
|
syl |
|
13 |
|
ltrelxr |
|
14 |
13
|
ssbri |
|
15 |
1 14
|
syl |
|
16 |
|
brxp |
|
17 |
15 16
|
sylib |
|
18 |
|
ioon0 |
|
19 |
17 18
|
syl |
|
20 |
1 19
|
mpbird |
|
21 |
3
|
ralrimiva |
|
22 |
|
r19.2z |
|
23 |
20 21 22
|
syl2anc |
|
24 |
|
supxrlub |
|
25 |
10 5 24
|
sylancl |
|
26 |
2
|
ffnd |
|
27 |
|
ioossre |
|
28 |
|
breq2 |
|
29 |
28
|
rexima |
|
30 |
26 27 29
|
sylancl |
|
31 |
25 30
|
bitrd |
|
32 |
23 31
|
mpbird |
|
33 |
|
qbtwnxr |
|
34 |
5 12 32 33
|
mp3an2i |
|
35 |
|
qre |
|
36 |
35
|
adantr |
|
37 |
|
simpr |
|
38 |
36 37
|
elrpd |
|
39 |
38
|
anim1i |
|
40 |
39
|
anasss |
|
41 |
|
simplr |
|
42 |
|
rpxr |
|
43 |
|
supxrlub |
|
44 |
10 42 43
|
syl2an |
|
45 |
|
breq2 |
|
46 |
45
|
rexima |
|
47 |
26 27 46
|
sylancl |
|
48 |
47
|
adantr |
|
49 |
44 48
|
bitrd |
|
50 |
5
|
a1i |
|
51 |
|
ioorp |
|
52 |
|
ioossicc |
|
53 |
51 52
|
eqsstrri |
|
54 |
53
|
sseli |
|
55 |
|
0e0iccpnf |
|
56 |
|
ifcl |
|
57 |
54 55 56
|
sylancl |
|
58 |
57
|
adantr |
|
59 |
58
|
fmpttd |
|
60 |
|
itg2cl |
|
61 |
59 60
|
syl |
|
62 |
61
|
ad5antlr |
|
63 |
|
ifcl |
|
64 |
54 55 63
|
sylancl |
|
65 |
64
|
adantr |
|
66 |
65
|
fmpttd |
|
67 |
|
itg2cl |
|
68 |
66 67
|
syl |
|
69 |
68
|
ad5antlr |
|
70 |
|
rpre |
|
71 |
70
|
ad4antlr |
|
72 |
|
ioombl |
|
73 |
|
mblvol |
|
74 |
72 73
|
ax-mp |
|
75 |
|
elioore |
|
76 |
75
|
ad3antlr |
|
77 |
|
rpre |
|
78 |
77
|
adantl |
|
79 |
76 78
|
resubcld |
|
80 |
79
|
adantr |
|
81 |
79
|
rexrd |
|
82 |
81
|
adantr |
|
83 |
17
|
simpld |
|
84 |
83
|
ad5antr |
|
85 |
17
|
simprd |
|
86 |
85
|
ad5antr |
|
87 |
83
|
ad4antr |
|
88 |
|
xrltnle |
|
89 |
81 87 88
|
syl2anc |
|
90 |
89
|
biimpar |
|
91 |
1
|
ad5antr |
|
92 |
|
xrre2 |
|
93 |
82 84 86 90 91 92
|
syl32anc |
|
94 |
80 93
|
ifclda |
|
95 |
85
|
ad5antr |
|
96 |
78 76
|
readdcld |
|
97 |
96
|
adantr |
|
98 |
|
mnfxr |
|
99 |
98
|
a1i |
|
100 |
|
mnfle |
|
101 |
83 100
|
syl |
|
102 |
99 83 85 101 1
|
xrlelttrd |
|
103 |
102
|
ad5antr |
|
104 |
|
simpr |
|
105 |
|
xrre |
|
106 |
95 97 103 104 105
|
syl22anc |
|
107 |
96
|
adantr |
|
108 |
106 107
|
ifclda |
|
109 |
76
|
rexrd |
|
110 |
85
|
ad4antr |
|
111 |
|
rpgt0 |
|
112 |
111
|
adantl |
|
113 |
78 76
|
ltsubposd |
|
114 |
112 113
|
mpbid |
|
115 |
|
eliooord |
|
116 |
115
|
simprd |
|
117 |
116
|
ad3antlr |
|
118 |
81 109 110 114 117
|
xrlttrd |
|
119 |
78 76
|
ltaddpos2d |
|
120 |
112 119
|
mpbid |
|
121 |
79 76 96 114 120
|
lttrd |
|
122 |
|
breq2 |
|
123 |
|
breq2 |
|
124 |
122 123
|
ifboth |
|
125 |
118 121 124
|
syl2anc |
|
126 |
1
|
ad4antr |
|
127 |
96
|
rexrd |
|
128 |
115
|
simpld |
|
129 |
128
|
ad3antlr |
|
130 |
87 109 127 129 120
|
xrlttrd |
|
131 |
|
breq2 |
|
132 |
|
breq2 |
|
133 |
131 132
|
ifboth |
|
134 |
126 130 133
|
syl2anc |
|
135 |
|
breq1 |
|
136 |
|
breq1 |
|
137 |
135 136
|
ifboth |
|
138 |
125 134 137
|
syl2anc |
|
139 |
94 108 138
|
ltled |
|
140 |
|
ovolioo |
|
141 |
94 108 139 140
|
syl3anc |
|
142 |
74 141
|
syl5eq |
|
143 |
108 94
|
resubcld |
|
144 |
142 143
|
eqeltrd |
|
145 |
|
rpgt0 |
|
146 |
145
|
ad4antlr |
|
147 |
94 108
|
posdifd |
|
148 |
138 147
|
mpbid |
|
149 |
148 142
|
breqtrrd |
|
150 |
71 144 146 149
|
mulgt0d |
|
151 |
|
iooin |
|
152 |
87 110 81 127 151
|
syl22anc |
|
153 |
152
|
eleq2d |
|
154 |
153
|
ifbid |
|
155 |
154
|
mpteq2dv |
|
156 |
155
|
fveq2d |
|
157 |
|
rpge0 |
|
158 |
|
elrege0 |
|
159 |
70 157 158
|
sylanbrc |
|
160 |
159
|
ad4antlr |
|
161 |
|
itg2const |
|
162 |
72 144 160 161
|
mp3an2i |
|
163 |
156 162
|
eqtrd |
|
164 |
150 163
|
breqtrrd |
|
165 |
164
|
adantr |
|
166 |
59
|
ad5antlr |
|
167 |
66
|
ad5antlr |
|
168 |
|
fvoveq1 |
|
169 |
168
|
breq1d |
|
170 |
169
|
imbrov2fvoveq |
|
171 |
170
|
rspccva |
|
172 |
|
breq1 |
|
173 |
|
breq1 |
|
174 |
70
|
leidd |
|
175 |
174
|
ad6antlr |
|
176 |
75
|
ad4antlr |
|
177 |
77
|
ad2antlr |
|
178 |
176 177
|
resubcld |
|
179 |
178
|
rexrd |
|
180 |
177 176
|
readdcld |
|
181 |
180
|
rexrd |
|
182 |
|
elioo2 |
|
183 |
179 181 182
|
syl2anc |
|
184 |
|
3anass |
|
185 |
183 184
|
bitrdi |
|
186 |
|
simpr |
|
187 |
75
|
ad5antlr |
|
188 |
186 187
|
resubcld |
|
189 |
77
|
ad3antlr |
|
190 |
188 189
|
absltd |
|
191 |
189
|
renegcld |
|
192 |
187 191 186
|
ltaddsub2d |
|
193 |
187
|
recnd |
|
194 |
189
|
recnd |
|
195 |
193 194
|
negsubd |
|
196 |
195
|
breq1d |
|
197 |
192 196
|
bitr3d |
|
198 |
186 187 189
|
ltsubaddd |
|
199 |
197 198
|
anbi12d |
|
200 |
190 199
|
bitrd |
|
201 |
200
|
pm5.32da |
|
202 |
185 201
|
bitr4d |
|
203 |
202
|
biimpa |
|
204 |
|
pm3.35 |
|
205 |
204
|
ancoms |
|
206 |
70
|
ad6antlr |
|
207 |
|
rge0ssre |
|
208 |
2
|
ad4antr |
|
209 |
208
|
ffvelrnda |
|
210 |
207 209
|
sseldi |
|
211 |
210
|
adantr |
|
212 |
2
|
adantr |
|
213 |
212
|
ffvelrnda |
|
214 |
207 213
|
sseldi |
|
215 |
75 214
|
sylan2 |
|
216 |
215
|
ad3antrrr |
|
217 |
210 216
|
resubcld |
|
218 |
70
|
ad2antlr |
|
219 |
215 218
|
resubcld |
|
220 |
219
|
ad3antrrr |
|
221 |
217 220
|
absltd |
|
222 |
215
|
recnd |
|
223 |
|
rpcn |
|
224 |
223
|
ad2antlr |
|
225 |
222 224
|
negsubdi2d |
|
226 |
225
|
ad3antrrr |
|
227 |
226
|
breq1d |
|
228 |
227
|
anbi1d |
|
229 |
221 228
|
bitrd |
|
230 |
229
|
simprbda |
|
231 |
215
|
ad4antr |
|
232 |
206 211 231
|
ltsub1d |
|
233 |
230 232
|
mpbird |
|
234 |
206 211 233
|
ltled |
|
235 |
205 234
|
sylan2 |
|
236 |
235
|
an4s |
|
237 |
203 236
|
syldan |
|
238 |
237
|
iftrued |
|
239 |
175 238
|
breqtrrd |
|
240 |
|
0le0 |
|
241 |
|
breq2 |
|
242 |
|
breq2 |
|
243 |
241 242
|
ifboth |
|
244 |
157 240 243
|
sylancl |
|
245 |
244
|
ad6antlr |
|
246 |
172 173 239 245
|
ifbothda |
|
247 |
171 246
|
sylan2 |
|
248 |
247
|
anassrs |
|
249 |
|
iftrue |
|
250 |
249
|
adantl |
|
251 |
|
iftrue |
|
252 |
251
|
adantl |
|
253 |
248 250 252
|
3brtr4d |
|
254 |
253
|
ex |
|
255 |
240
|
a1i |
|
256 |
|
iffalse |
|
257 |
|
iffalse |
|
258 |
255 256 257
|
3brtr4d |
|
259 |
254 258
|
pm2.61d1 |
|
260 |
|
elin |
|
261 |
|
ifbi |
|
262 |
260 261
|
ax-mp |
|
263 |
|
ifan |
|
264 |
262 263
|
eqtri |
|
265 |
|
fveq2 |
|
266 |
265
|
breq2d |
|
267 |
266
|
elrab |
|
268 |
|
ifbi |
|
269 |
267 268
|
ax-mp |
|
270 |
|
ifan |
|
271 |
269 270
|
eqtri |
|
272 |
259 264 271
|
3brtr4g |
|
273 |
272
|
ralrimivw |
|
274 |
|
reex |
|
275 |
274
|
a1i |
|
276 |
57
|
ad6antlr |
|
277 |
64
|
ad6antlr |
|
278 |
|
eqidd |
|
279 |
|
eqidd |
|
280 |
275 276 277 278 279
|
ofrfval2 |
|
281 |
273 280
|
mpbird |
|
282 |
|
itg2le |
|
283 |
166 167 281 282
|
syl3anc |
|
284 |
50 62 69 165 283
|
xrltletrd |
|
285 |
4
|
ad3antrrr |
|
286 |
|
simplr |
|
287 |
|
fssres |
|
288 |
27 287
|
mpan2 |
|
289 |
|
fss |
|
290 |
207 289
|
mpan2 |
|
291 |
2 288 290
|
3syl |
|
292 |
291
|
adantr |
|
293 |
292
|
ffvelrnda |
|
294 |
293 218
|
resubcld |
|
295 |
294
|
adantr |
|
296 |
218 293
|
posdifd |
|
297 |
296
|
biimpa |
|
298 |
295 297
|
elrpd |
|
299 |
|
cncfi |
|
300 |
285 286 298 299
|
syl3anc |
|
301 |
300
|
ex |
|
302 |
|
fvres |
|
303 |
302
|
breq2d |
|
304 |
303
|
adantl |
|
305 |
|
fvres |
|
306 |
305
|
adantl |
|
307 |
302
|
ad2antlr |
|
308 |
306 307
|
oveq12d |
|
309 |
308
|
fveq2d |
|
310 |
302
|
oveq1d |
|
311 |
310
|
ad2antlr |
|
312 |
309 311
|
breq12d |
|
313 |
312
|
imbi2d |
|
314 |
313
|
ralbidva |
|
315 |
314
|
rexbidv |
|
316 |
301 304 315
|
3imtr3d |
|
317 |
316
|
imp |
|
318 |
284 317
|
r19.29a |
|
319 |
318
|
rexlimdva2 |
|
320 |
49 319
|
sylbid |
|
321 |
320
|
imp |
|
322 |
66
|
ad2antlr |
|
323 |
|
icossicc |
|
324 |
|
fss |
|
325 |
2 323 324
|
sylancl |
|
326 |
325
|
ad2antrr |
|
327 |
|
breq1 |
|
328 |
|
breq1 |
|
329 |
267
|
simprbi |
|
330 |
329
|
adantl |
|
331 |
2
|
ffvelrnda |
|
332 |
|
elrege0 |
|
333 |
331 332
|
sylib |
|
334 |
333
|
simprd |
|
335 |
334
|
adantr |
|
336 |
327 328 330 335
|
ifbothda |
|
337 |
336
|
ralrimiva |
|
338 |
337
|
ad2antrr |
|
339 |
274
|
a1i |
|
340 |
64
|
ad3antlr |
|
341 |
|
fvexd |
|
342 |
|
eqidd |
|
343 |
2
|
feqmptd |
|
344 |
343
|
ad2antrr |
|
345 |
339 340 341 342 344
|
ofrfval2 |
|
346 |
338 345
|
mpbird |
|
347 |
|
itg2le |
|
348 |
322 326 346 347
|
syl3anc |
|
349 |
41 321 348
|
jca32 |
|
350 |
349
|
expl |
|
351 |
40 350
|
syl5 |
|
352 |
351
|
reximdv2 |
|
353 |
68
|
adantl |
|
354 |
|
itg2cl |
|
355 |
325 354
|
syl |
|
356 |
355
|
adantr |
|
357 |
|
xrltletr |
|
358 |
5 353 356 357
|
mp3an2i |
|
359 |
358
|
rexlimdva |
|
360 |
352 359
|
syld |
|
361 |
34 360
|
mpd |
|