Description: Restriction of a derivative to an open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | dvresioo | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-resscn | |
|
2 | 1 | a1i | |
3 | simpr | |
|
4 | simpl | |
|
5 | ioossre | |
|
6 | 5 | a1i | |
7 | eqid | |
|
8 | 7 | tgioo2 | |
9 | 7 8 | dvres | |
10 | 2 3 4 6 9 | syl22anc | |
11 | ioontr | |
|
12 | 11 | reseq2i | |
13 | 10 12 | eqtrdi | |