Description: Fermat's theorem on stationary points. A point U which is a local maximum has derivative equal to zero. (Contributed by Mario Carneiro, 1-Sep-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | dvferm.a | |
|
dvferm.b | |
||
dvferm.u | |
||
dvferm.s | |
||
dvferm.d | |
||
dvferm.r | |
||
Assertion | dvferm | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dvferm.a | |
|
2 | dvferm.b | |
|
3 | dvferm.u | |
|
4 | dvferm.s | |
|
5 | dvferm.d | |
|
6 | dvferm.r | |
|
7 | ne0i | |
|
8 | ndmioo | |
|
9 | 8 | necon1ai | |
10 | 3 7 9 | 3syl | |
11 | 10 | simpld | |
12 | ioossre | |
|
13 | 12 3 | sselid | |
14 | 13 | rexrd | |
15 | eliooord | |
|
16 | 3 15 | syl | |
17 | 16 | simpld | |
18 | 11 14 17 | xrltled | |
19 | iooss1 | |
|
20 | 11 18 19 | syl2anc | |
21 | ssralv | |
|
22 | 20 6 21 | sylc | |
23 | 1 2 3 4 5 22 | dvferm1 | |
24 | 10 | simprd | |
25 | 16 | simprd | |
26 | 14 24 25 | xrltled | |
27 | iooss2 | |
|
28 | 24 26 27 | syl2anc | |
29 | ssralv | |
|
30 | 28 6 29 | sylc | |
31 | 1 2 3 4 5 30 | dvferm2 | |
32 | dvfre | |
|
33 | 1 2 32 | syl2anc | |
34 | 33 5 | ffvelrnd | |
35 | 0re | |
|
36 | letri3 | |
|
37 | 34 35 36 | sylancl | |
38 | 23 31 37 | mpbir2and | |