Description: Restriction of a derivative. Note that our definition of derivative df-dv would still make sense if we demanded that x be an element of the domain instead of an interior point of the domain, but then it is possible for a non-differentiable function to have two different derivatives at a single point x when restricted to different subsets containing x ; a classic example is the absolute value function restricted to [ 0 , +oo ) and ( -oo , 0 ] . (Contributed by Mario Carneiro, 8-Aug-2014) (Revised by Mario Carneiro, 9-Feb-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | dvres.k | |
|
dvres.t | |
||
Assertion | dvres | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dvres.k | |
|
2 | dvres.t | |
|
3 | reldv | |
|
4 | relres | |
|
5 | simpll | |
|
6 | simplr | |
|
7 | inss1 | |
|
8 | fssres | |
|
9 | 6 7 8 | sylancl | |
10 | resres | |
|
11 | ffn | |
|
12 | fnresdm | |
|
13 | 6 11 12 | 3syl | |
14 | 13 | reseq1d | |
15 | 10 14 | eqtr3id | |
16 | 15 | feq1d | |
17 | 9 16 | mpbid | |
18 | simprl | |
|
19 | 7 18 | sstrid | |
20 | 5 17 19 | dvcl | |
21 | 20 | ex | |
22 | 5 6 18 | dvcl | |
23 | 22 | ex | |
24 | 23 | adantld | |
25 | eqid | |
|
26 | 5 | adantr | |
27 | 6 | adantr | |
28 | 18 | adantr | |
29 | simplrr | |
|
30 | simpr | |
|
31 | 1 2 25 26 27 28 29 30 | dvreslem | |
32 | 31 | ex | |
33 | 21 24 32 | pm5.21ndd | |
34 | vex | |
|
35 | 34 | brresi | |
36 | 33 35 | bitr4di | |
37 | 3 4 36 | eqbrrdiv | |