Description: The function F does not always return real numbers, but it does on intervals of finite volume. (Contributed by Mario Carneiro, 26-Mar-2015) (Revised by AV, 13-Sep-2020)
Ref | Expression | ||
---|---|---|---|
Hypothesis | ioorf.1 | |
|
Assertion | ioorcl | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ioorf.1 | |
|
2 | 1 | ioorf | |
3 | 2 | ffvelrni | |
4 | 3 | adantr | |
5 | 4 | elin1d | |
6 | 1 | ioorval | |
7 | 6 | adantr | |
8 | iftrue | |
|
9 | 7 8 | sylan9eq | |
10 | 0re | |
|
11 | opelxpi | |
|
12 | 10 10 11 | mp2an | |
13 | 9 12 | eqeltrdi | |
14 | ioof | |
|
15 | ffn | |
|
16 | ovelrn | |
|
17 | 14 15 16 | mp2b | |
18 | 1 | ioorinv2 | |
19 | 18 | adantl | |
20 | ioorcl2 | |
|
21 | 20 | ancoms | |
22 | opelxpi | |
|
23 | 21 22 | syl | |
24 | 19 23 | eqeltrd | |
25 | fveq2 | |
|
26 | 25 | eleq1d | |
27 | neeq1 | |
|
28 | 26 27 | anbi12d | |
29 | fveq2 | |
|
30 | 29 | eleq1d | |
31 | 28 30 | imbi12d | |
32 | 24 31 | mpbiri | |
33 | 32 | a1i | |
34 | 33 | rexlimivv | |
35 | 17 34 | sylbi | |
36 | 35 | impl | |
37 | 13 36 | pm2.61dane | |
38 | 5 37 | elind | |